Chapter 10
The Category of GSLTs
Part III consists of constructions that take a theory and produce a theory. To say anything about such constructions — that they are functorial, that they are monads, that they have adjoints — we need a category of theories. This section builds it, and the build is less routine than one might expect: the obvious definition is wrong, and the way it is wrong is instructive.
10.1 The naive definition and three defects
The obvious move is to take objects to be GSLTs and morphisms to be signature-preserving translations that preserve bisimulation. Three things go wrong.
The constant map.
Send every term to \(0\). This preserves signatures trivially and preserves bisimulation trivially, since the image has no transitions to fail to match. It is a morphism from anything to anything, and its presence means the category orders nothing.
Milner’s encoding is not a map of terms.
The canonical encoding of the \(\lambda\)-calculus into the \(\pi\)-calculus [125] — the very construction that established the modern practice of comparing calculi — sends a \(\lambda\)-term not to a \(\pi\)-term but to a \(\pi\)-term parameterised by a name: \(\sem{M}_u\), the process that realises \(M\) and reports its result on \(u\). Signature preservation does not typecheck, because \(\mathrm{App}\) is not sent to any single \(\pi\) operator; it is sent to a construction involving restriction, parallel composition, and output. Requiring morphisms to be signature homomorphisms excludes the motivating example.
Ambient contexts observe too much.
Suppose one encodes \(\pi\) into rho. A rho context may quote a process, compare quotations, and generally observe the syntactic form of what it is handed — capabilities no \(\pi\) context has. Bisimulation computed over all rho contexts will therefore separate the images of \(\pi\)-terms that no \(\pi\) context can separate. Under the naive definition, no interesting encoding is ever bisimulation-preserving, for a reason that has nothing to do with the encoding.
10.2 Contexts as the primary structure
The three defects have one cure. The first says we need a non-degeneracy condition; the second says terms are the wrong primitive; the third says the observer must be restricted to what the source can express. Taking contexts rather than terms as primary addresses all three at once, because a term is a nullary context, and because the observers of a term are exactly the contexts one can place around it.
A theory presents a symmetric multicategory of contexts. Its objects are interfaces, recording the sort of a hole, its binding stage, and its interaction surface. Its multimorphisms are contexts with holes of the given interfaces and a result of the given interface; composition is plugging. Terms are the nullary contexts.
Transitions are then labelled by contexts: rather than \(P \to P'\), we record \(P \xrightarrow{\;C\;} P'\), meaning that placing \(P\) in the context \(C\) enables the step. Bisimulation is taken over these context-labelled transitions.
A morphism of GSLTs is a pseudofunctor of context multicategories that is bisimulation-preserving for context-labelled transitions, where the bisimulation on the target is computed only over the image of the source’s contexts.
Each clause repairs one defect. Because the map is defined on contexts and terms are nullary contexts, an encoding like Milner’s — which sends a term to a context-parameterised process — is expressible: the parameterisation is the interface. Because bisimulation on the target is computed over the image, the ambient-observation defect disappears by construction; the encoded \(\pi\)-terms are compared by the encoded \(\pi\) contexts, which is the comparison one meant to make. And the constant map is excluded by the non-degeneracy conditions of the next subsection.
Definition 10.1 has two clauses that look independent — a map of contexts, and a restriction of the target’s observers to the image — and they are not. Spelling this out is due to [27], and the spelling makes the definition parse.
In a context-labelled transition system the labels are contexts. So “preserves context-labelled bisimulation” presupposes a map on labels, and a map on terms does not determine one: two encodings agreeing on every term may realise a given source context differently in the target and preserve different relations. The honest shape of a morphism is therefore a pair \((F,\Phi)\), with \(\Phi\) a functor on context multicategories, \(F\) the map on terms, an equivariance condition \[F(c[\vec t\,]) \;\bisim\; \Phi(c)[F\vec t\,] ,\] and preservation of transitions along \(\Phi\). Given that, the admissible observer class of the target is not a further stipulation: it is \(\mathrm{im}\,\Phi\). What Definition 10.1 calls computing bisimulation over the image of the source’s contexts is a consequence of naming \(\Phi\), not a second clause.
Two details are recorded and not chased. The equivariance square should commute up to \(\bisim\) rather than on the nose — the equations governing restriction force this — which pushes the structure into a bicategory; and faithfulness of \(\Phi\) should be a property distinguishing embeddings rather than part of morphism-hood, or the category has too few morphisms for the free/forgetful adjunctions of the next three chapters to survive.
\(\catGSLT\) is the category whose \(0\)-cells are GSLTs and whose morphisms are the maps of Definition 10.1: bisimulation-preserving for the context-labelled transition relation, which is thereby a congruence.
This is the official definition for the remainder of the document. The additional conditions imposed by particular constructions — quote-faithfulness for the cost functor of Chapter 11, preservation of \(\Pr\) and \(\rsq\) for the type-system functor of Chapter 19 — are stated where those constructions need them, and are refinements of Definition 10.1 rather than rivals to it.
10.3 Hosting and exhausting
Two conditions prevent the comparison from being trivial.
A morphism \(F : G \to H\) is hosting (faithful) when the target can run the source: the encoding reflects as well as preserves the context-labelled transition structure, so that no branching present in \(G\) is lost in \(H\).
\(F : G \to H\) is exhausting (dense) when the target is nothing the source cannot assemble: every context of \(H\) relevant to the image is, up to the equivalence, in the image of a context of \(G\).
The parenthesised words above are not decoration. Once a morphism is the pair \((F,\Phi)\) of Remark 10.1, hosting and exhausting are conditions on \(\Phi\) and on nothing else: hosting is faithfulness of \(\Phi\), and exhausting is density of \(\Phi\) — every target context relevant to the image lies in \(\mathrm{im}\,\Phi\) up to the equivalence. What had to be described in two sentences of prose becomes two words of category theory, and the pair of conditions turns out to be doing what such pairs usually do.
This has a consequence worth flagging for Chapter 64, where the same pair reappears as a criterion of notational adequacy: if hosting and exhausting are faithfulness and density, then that criterion is a statement about a functor between categories of contexts, and is in principle provable rather than merely evocative.
The constant map fails hosting immediately. Together the conditions induce a preorder on theories whose degrees refine Turing completeness rather than replacing it: the classical notion is recovered as the trace collapse, obtained by coarsening context-labelled bisimulation all the way to the input/output relation.
Expressiveness comparisons between computational models are conventionally anchored to Turing completeness. For functions this works. For interactive systems it does not, because Turing completeness is a statement about the input/output relation, and the input/output relation is the coarsest invariant in the linear-time/branching-time spectrum [128], while the equivalences that matter for interaction sit at the other end. Calculi of identical Turing power are routinely separated by uniform-encoding criteria, so the yardstick is measuring something other than what is being compared.
The obvious repair — demand behavioural rather than computational universality — merely relocates the problem, since the arbiter of which behavioural equivalence to use is an adequate modal logic, and the logical apparatus available in the ambient setting is inherited from the \(\lambda\)-calculus. An absolute notion is quietly \(\lambda\)-relative. Definition 10.1 replaces the yardstick with a relative property: fix a probe and ask what that probe can see.
The same preference for intensional over extensional comparison has a consequence for complexity theory that we record without pursuing. Equivalence of regular languages is PSPACE-complete, while the corresponding bisimulation problem is polynomial; equivalence of context-free languages is undecidable, while the corresponding bisimulation problem is tractable. We want the witnesses, not the extensions they give rise to. Infinitary objects like languages cannot be grasped directly, so an intensional representation is needed — and once one has an intensional representation, one has a bisimulation problem rather than a language-comparison problem.
The three sections that follow have the same shape. Each takes a theory presented as an interaction cut and produces another such theory, decorated with apparatus. Each is a monad. Each resolves through a free/forgetful adjunction that installs and removes the apparatus. And in each case, when the base theory is sufficiently expressive, the apparatus can alternatively be encoded back into the base — so that the base performs the metering, or the logging, or the checking, with its own computation. We note that possibility where it arises and do not develop it.