Chapter 10
Continued Interactive GSLTs
Interactivity names a site. The constructions of Part Part I need more: they need to be able to intervene at the site — to interpose a token, to record an event, to attach a guard. Three further conditions suffice, and this section isolates them.
10.1 Section-equipped
The first condition concerns the relationship between a term and its congruence class. Let \(T\) be the free syntax of the interacting sort and \(\widehat{T} = T/{\equiv}\) its quotient by structural congruence. Two maps relate them:
the quotient \(T \twoheadrightarrow \widehat{T}\), respecting \(\equiv\), invertible up to congruence. This is the structure a name constructor exposes when channels are taken up to \(\equiv\) — in rho, \(@P\) with \(@P = @Q \iff P \equiv Q\).
a section \(\cf : \widehat{T} \to T\), a choice of canonical representative per class.
An interactive GSLT is section-equipped when it comes with a computable section \(\cf : \widehat{T} \to T\) of its \(\equiv\)-quotient — equivalently, a computable canonical-form function on the interacting sort.
The condition is sharper than it looks, and the \(\lambda\)-calculus is the test that shows why. The \(\lambda\)-calculus has no analogue of the quote constructor \(@\). It passes anyway, because what is required is not a channel constructor but a section: for \(\lambda\) the congruence is \(\alpha\) and a canonical representative of each \(\alpha\)-class is the de Bruijn encoding [118]. Rho fuses the quotient and the section into one operator viewed two ways; \(\lambda\) pulls them apart; the requirement is identical in both.
10.2 Wrappability
The second condition asks that the contraction tolerate having its operands decorated. Anticipating Chapter 12, write \(\Tw\) for a sort of wrapped terms.
The contraction \(\compute\) is wrappable when it is well-sorted as an operation on wrapped continuations, \(\compute : \Surf \times \Surf \times \Tw \times \Tw \to \Tw \times \Tw\) — equivalently, when \(\compute\) is definable on decorated continuations, mapping decorated inputs to decorated outputs.
The condition is mild for substitution-like contractions: substituting a wrapped term into a position yields a wrapped term, so \(\compute\) preserves the sort for free and need not know that wrapping exists. It excludes contractions that inspect and dismantle their operands — an opaque contraction returning bare residuals would violate it.
10.3 The definition
A continued interactive GSLT is an interactive GSLT equipped with:
a presentation of its dynamics in interaction-cut form \((\dagger)\), naming \(K, K_p, K_e, K'\) and the partial contraction \(\compute\);
a section (Definition 10.1); and
wrappability (Definition 10.2).
We write \(\catciGSLT\) for the resulting category, whose morphisms are theory maps that are bisimulation-preserving on the interacting sort and quote-faithful: injective on the reachable signature keys.
The adjective names a strict strengthening. Clauses (i)–(iii) are data and conditions added on top of an interactive GSLT, not a restriction of it; forgetting them recovers the underlying interactive GSLT.
\(U : \catciGSLT \to \catiGSLT\) sends a continued interactive GSLT to its underlying interactive GSLT, discarding the cut presentation, the section, and the wrappability witness, and acts as the identity on the underlying theory map of a morphism.
\(U\) is faithful but neither full nor essentially surjective. Hence \(\catciGSLT\) is a genuine, proper subcategory of \(\catiGSLT\): strictly more structure on objects, strictly fewer morphisms between them.
Faithful, not full. \(U\) forgets no information about a morphism’s action, so it is faithful. It is not full because a \(\catciGSLT\)-morphism must additionally be quote-faithful: an \(\catiGSLT\)-morphism that is bisimulation-preserving yet collapses two distinct signature keys is a map between the underlying objects with no lift.
Not essentially surjective. Clause (i) requires the dynamics to factor as contact then contraction, which a theory with non-local or unfactorable rewrites need not; clause (ii) requires a computable section, which a theory with undecidable structural congruence lacks; clause (iii) requires the contraction to preserve wrapping. An interactive GSLT failing any of these has no preimage.
The \(\lambda\)-calculus is an object of \(\catiGSLT\) as such: terms, \(\alpha\), \(\beta\). It becomes an object of \(\catciGSLT\) only once one chooses the added structure — the de Bruijn section for (ii), the degenerate-\(K_e\) presentation of \(\beta\) for (i), substitution-on-thunks for (iii). The same underlying calculus sits at both levels, witnessing that “continued” is added structure and not a property read off the interactive GSLT alone.
10.4 How the examples are examples
The instances are usefully ordered by how much information the contraction moves from the environment continuation into the program continuation. Four modes occur: no migration (CCS, interaction categories), migration by binding (rho, \(\pi\), \(\lambda\)), migration by spatial restructuring (ambients), and migration as interface composition.
Table 10.1 records the interaction-cut data of each running example, and Table 10.2 records whether that data satisfies the successive conditions. The final column of Table 10.2 is the discrimination the two strengthenings were introduced to make.
| Instance | \(K\) | \(E\) on \(K\) | \(I\), \(J\) | \(C_p\) / \(C_e\) | \(\compute\) (migration) |
|---|---|---|---|---|---|
| Calculator | — | — | — | — | no interaction rule |
| [2pt] CCS | \({\mid}\) | AC | \(a\), \(\bar a\) | \(P\) / \(Q\) | pure release \(P \mid Q\) (none) |
| [2pt] Interaction cats. | \(\circ\) | — | shared interface | proc. / proc. | interface composition (none) |
| [2pt] rho, \(\pi\) (sync) | \({\mid}\) | AC | \(x\), \(x\) | \(\lambda y.P\) / \([Q_1,Q_2]\) | pseudo-app. \(P\{Q_1/y\} \mid Q_2\) (binding) |
| [2pt] rho, \(\pi\) (async) | \({\mid}\) | AC | \(x\), \(x\) | \(\lambda y.P\) / \([Q,-]\) | pseudo-app. \(P\{Q/y\}\) (binding) |
| [2pt] \(\lambda\) | \(\mathrm{App}\) | free | \(x\), \(-\) | \(\lambda x.M\) / \(N\) | application \(M\{N/x\}\) (binding) |
| [2pt] Ambients | \({\mid}\) | AC | \(n\), \(n\) | \(P\) / \(Q\) | boundary dissolve/move (spatial) |
| [2pt] Turing | none | — | — | — | control/tape heterogeneous |
| [2pt] Moore | none | — | — | — | control/stream heterogeneous |
| [2pt] Mealy | none | — | — | — | control/stream heterogeneous |
| Instance | GSLT | has \(K\)-rule | section \(\cf\) | wrappable | Verdict |
|---|---|---|---|---|---|
| Calculator | — | normal form | — | GSLT only | |
| CCS | normal form for AC \(\mid\) | continued interactive | |||
| Interaction cats. | interface normal form | continued interactive | |||
| rho, \(\pi\) (sync) | normal form for AC \(\mid\) | continued interactive | |||
| rho, \(\pi\) (async) | normal form for AC \(\mid\) | continued interactive | |||
| \(\lambda\) | de Bruijn | continued interactive\(^\ast\) | |||
| Ambients | normal form for AC \(\mid\) | continued interactive | |||
| Turing | — | — | — | GSLT only | |
| Moore | — | — | — | GSLT only | |
| Mealy | — | — | — | GSLT only |
Two readings of the tables are worth making explicit.
First, the calculator row and the three machine rows fail for different reasons, and the tables record the difference. The calculator has no interaction rule because it has no notion of a program meeting an environment at all — it is a language of closed expressions. The machines have a notion of the control meeting something, but the something is of the wrong sort. Both end at “GSLT only,” and a reader who wanted to know which of the two situations obtains would have to look at the \(K\) column.
Second, \(\lambda\) is the only row whose verdict carries a caveat, and the caveat is the content of Proposition 10.1. Nothing about the \(\lambda\)-calculus as ordinarily presented determines a section; de Bruijn is a choice, and a different choice — a different canonical form for \(\alpha\)-classes — would give a different object of \(\catciGSLT\) over the same object of \(\catiGSLT\). This is what it means for \(U\) to fail to be essentially surjective on the nose while being surjective on the underlying calculi one cares about.