Theory DSL: denotational semantics

In plain terms

The theory DSL is what you use to declare a new protocol’s schema language. You write down the basic kinds of thing the protocol talks about (its sorts), the constructors that build them (its operations), and the equations they satisfy. The DSL compiles to a generalized algebraic theory (GAT) that the rest of panproto consumes uniformly.

This page pins down what a GAT presentation is, what category it generates, and what counts as a valid presentation.

Surface syntax

The Nickel surface (canonical authoring form). JSON and YAML surfaces are isomorphic via serde. Every document carries an id, a description, and exactly one body variant (theory, morphism, composition, protocol, bundle, class, instance, or inductive type).

A bare theory body:

{
  id = "dev.example.thgraph",
  description = "Directed multigraph with identity edges",
  theory = "ThGraph",
  sorts = [ { name = "Vertex" }, { name = "Edge" } ],
  ops = [
    { name = "src", inputs = [{ name = "e", sort = "Edge" }], output = "Vertex" },
    { name = "tgt", inputs = [{ name = "e", sort = "Edge" }], output = "Vertex" },
    { name = "id",  inputs = [{ name = "v", sort = "Vertex" }], output = "Edge" },
  ],
  equations = [
    { name = "src-id", lhs = "src(id(v))", rhs = "v", context = [{ name = "v", sort = "Vertex" }] },
    { name = "tgt-id", lhs = "tgt(id(v))", rhs = "v", context = [{ name = "v", sort = "Vertex" }] },
  ],
}

The full grammar is in crates/panproto-theory-dsl/src/document.rs.

Abstract syntax

pub struct TheoryDocument {
    pub id: String,
    pub description: String,
    pub body: TheoryBody,
}

pub enum TheoryBody {
    Theory(TheorySpec),
    Morphism(MorphismSpec),
    Composition(CompositionBody),
    Protocol(Box<ProtocolSpec>),
    Bundle(Box<BundleSpec>),
    Class(ClassSpec),
    Instance(InstanceSpec),
    Inductive(InductiveSpec),
}

pub struct TheorySpec {
    pub theory: String,                       // theory name
    pub extends: Vec<String>,                 // parent theories
    pub imports: Vec<ImportSpec>,             // imports with optional aliases
    pub sorts: Vec<SortSpec>,                 // sort declarations (with dependent params)
    pub ops: Vec<OpSpec>,                     // operation declarations
    pub equations: Vec<EquationSpec>,         // judgemental equalities
    pub directed_equations: Vec<DirectedEqSpec>,  // rewrite rules
    pub policies: Vec<PolicySpec>,            // conflict policies
}

The DSL document compiles to panproto_gat::Theory (and, for non-Theory bodies, to TheoryMorphism or Protocol). The intermediate surface types (TheorySpec, OpSpec, etc.) are deserialisation targets, not the categorical objects; the categorical objects are the GAT types.

Sort, operation, and equation judgements

A sort is well-formed in a theory context $Θ$ when it appears in the sort list:

$\frac{S \in sorts ( Θ )}{Θ ⊢ S sort} (sort-wf)$

An operation is well-typed when its inputs are well-typed sorts and its output is a well-typed sort dependent on the inputs:

$\frac{Θ ⊢ S _{1} sort \dots Θ ⊢ S _{n} sort Θ , x _{1} : S _{1} , \dots , x _{n} : S _{n} ⊢ T sort}{Θ ⊢ f : ( x _{1} : S _{1} , \dots , x _{n} : S _{n} ) \to T op} (op-wf)$

An equation is well-formed when both sides type-check at the same sort under the same context:

$\frac{Θ ; Γ ⊢ t _{1} : T Θ ; Γ ⊢ t _{2} : T}{Θ ⊢ t _{1} = t _{2} : T [ Γ ] eqn} (eqn-wf)$

Semantic domain

The semantic universe is $CwF$ , the (2-)category of categories with families (Cartmell-style: contexts as objects, substitutions as morphisms, types and terms forming a presheaf over substitutions). The denotational semantics is the functor

$[[\cdot]] : TheoryDocument \to CwF$

defined by case on the document body (with the bundle case mapping to a tuple of CwFs). For the bare theory case:

$[[TheoryDocument {body = Theory (T)}]] = CwF (T)$

where $CwF (T)$ is the initial CwF satisfying the sort, operation, and equation declarations of $T$ . Initiality is the semantic content of the GAT construction: for every CwF $C$ that interprets $T$ ’s sorts and operations and validates its equations, there is a unique structure-preserving functor $CwF (T) \to C$ . The GAT presentation framework is due to Cartmell (Cartmell (1986)), and the category-with-families packaging of dependent type theory is Dybjer’s (Dybjer (1996)); the two compose to give the initial-model semantics used here.

A schema in panproto is a model of $CwF (T)$ in the CwF of finite sets and functions: equivalently, a CwF morphism $CwF (T) \to FinSet$ .

Semantic equations for the body cases

$[[Theory (T)]] [[Morphism (M : T_{1} \to T_{2})]] [[Composition (compose = {r, b, [c_{1}, \dots, c_{k}]})]] [[Class (C)]] [[Instance (I : C \to T)]] [[Inductive (D)]] [[Protocol (P)]] [[Bundle (B)]] = CwF (T) = F_{M} : CwF (T_{1}) \to CwF (T_{2}) = CwF (colim (b, c_{1}, \dots, c_{k})) = CwF (class - to - theory (C)) = F_{I} : CwF (class - to - theory (C)) \to CwF (T) = CwF (inductive - to - theory (D)) = (CwF (P . schema_theory), CwF (P . instance_theory), Edge (P)) = x \in B \prod [[x]]$

where $colim$ is the iterated pushout described under Pushouts and merge and the auxiliary class-to-theory and inductive-to-theory are the desugarings implemented in panproto-theory-dsl/src/compile_class.rs and compile_inductive.rs.

The interpretation of the composition body factors through the colimit construction in $Th$ : $[[T_{1} +_{S} T_{2}]] = [[T_{1}]] +_{[[S]]} [[T_{2}]]$ , exploiting the fact that $CwF$ preserves the relevant colimits.

Soundness and registration

A protocol registration is the construction of a colimit diagram. If any pushout step in the diagram fails to satisfy the universal property (because two equations contradict on a shared sort), registration panics with a message naming the failing intermediate step:

panic: colimit ThGraph + ThConstraint over ThVertex failed:
       equation `src(id(v)) = v` contradicts `src(id(v)) = source(v)`

This is a build-time bug in the theory composition; the panic is intentional. See crates/panproto-protocols/src/theories.rs.

What is intentionally not modelled

Higher dimensions. The DSL is for 1-categorical GATs only. We do not model homotopical structure, 2-cells, or coherent equations.
Infinitary signatures. Operations have finite arity. There is no way to declare an operation that takes an unbounded list of arguments.
Term rewriting decidability. Equation orientation and confluence are the user’s responsibility; the colimit construction does not check for a complete rewriting system.

Keyboard shortcuts

panproto