Chapter 16
The Labeled Transition System and Context-Decorated HML
16.1 Minimal Contexts and the LTS
To obtain a bisimulation that is a congruence for a GSLT, we follow the approach of Milner, Sewell, and Leifer [2]. The key idea is to label transitions not merely by actions but by minimal reactive contexts — the smallest environments needed to trigger a given reduction.
A context \(K[-]\) for a GSLT \(\GSLT\) is a term of \(\terms(\GSLT)\) with a distinguished hole \([-]\). The application \(K[P]\) substitutes \(P\) for the hole. A context is minimal for a term \(P\) and rule \(r\) if:
\(K[P] \rewrite_r Q\) for some \(Q\);
there is no proper sub-context \(K'\) of \(K\) satisfying (i).
The Milner–Sewell–Leifer construction produces, for any GSLT \(\GSLT\), a labeled transition system \(\lts(\GSLT)\) in which transitions are labeled by minimal contexts: \[P \xrightarrow{K} Q \quad\text{iff}\quad K[P] \rewrite Q.\]
Three refinements of that statement are needed before it can be leaned on, and the book leans on it heavily. They are recorded here rather than where they bite.
The subterm formulation above is the readable one, and it is not quite the working one. Leifer and Milner define minimality by a universal property: a transition \(P \xrightarrow{K} d[r]\) is asserted when \(l \rewrite r\) is a rule and \(d[l] = K[P]\) is an idempotent relative pushout in the relevant slice category, so that \(K\) is a least enabling context in the categorical sense rather than merely one with no proper enabling subterm [2]. The two agree in easy cases and the universal property is what supports the congruence proof.
There is a second departure. Leifer and Milner’s reactive systems fix a distinguished object as the domain of the pushouts, which in practice restricts attention to ground terms. [27] observes that the proofs do not depend on it and adopts an open version. That is what a GSLT needs, since a lambda theory’s terms carry variables and its contexts have interfaces rather than a single ground sort.
The existence of the pushouts is not free. It is a hypothesis about the theory, verified for particular theories rather than for GSLTs at large, and it is listed among this book’s unproved assumptions in the front matter.
In a higher-order setting a minimal enabling context still carries processes: for \(\rhoc\) the labels have the shape \(-\Par\mathrm{in}(n,\lambda x.q)\) with \(q\) an arbitrary process. Matching such labels syntactically yields a relation known to be too fine [120]. The remedy, which this book adopts throughout, is to compare labels position by position, relating constructor skeletons by identity and process payloads by the bisimilarity being defined. The functional whose greatest fixed point this is remains monotone — the relation occurs only positively — so Knaster–Tarski still applies and the definition is sound.
It is usual to summarise the construction as “the induced bisimulation is a congruence”. Unqualified, that is false for the theory this book cares about most. Congruence holds with respect to a class \(\mathcal{A}\) of admissible contexts, and observations must be restricted to the same class. For \(\rhoc\), [27] proves congruence under \(\mathrm{out}(n,-)\), \(\mathrm{in}(n,-)\), \(-\Par-\) and \(\ast(@(-))\), and must exclude contexts with a hole under the quote, such as \(\mathrm{out}(@(-),z)\). The reason is exactly reflection: communication turns on name equality rather than on bisimilarity, so \(p \bisim q\) with \(p \neq q\) gives \(@p \neq @q\), and the two contexts behave differently.
This is not a blemish to be apologised for. Making the admissible class a parameter is what allows one theorem to cover both the congruence result for a calculus and the comparison of two calculi, where the admissible contexts are the image of the source’s — which is precisely the shape Definition 10.1 takes in Chapter 10. The restriction was discovered three times as an obstacle before it could be recognised as a component.
16.2 Context-Decorated Hennessy–Milner Logic
The formulae of context-decorated Hennessy–Milner logic \(\HML(\ctx)\) are generated by: \[\phi, \psi \;::=\; \top \;\mid\; \bot \;\mid\; \phi \wedge \psi \;\mid\; \neg\phi \;\mid\; \langle K \rangle \phi\] where \(K\) ranges over contexts of \(\GSLT\). The satisfaction relation is: \[u \sat \langle K \rangle \phi \quad\text{iff}\quad K[u] \rewrite u' \;\text{ in one step, and }\; u' \sat \phi.\]
For any GSLT \(\GSLT\) equipped with the Milner–Sewell–Leifer LTS: \[u \bisim v \quad\Longleftrightarrow\quad \forall \phi \in \HML(\ctx),\; u \sat \phi \Leftrightarrow v \sat \phi.\]
\(\HML(\ctx)\) as defined above has modalities and boolean structure and nothing else. The generated logics of Chapter 19 have in addition a structural layer, one connective per term constructor, and the theorem above says nothing about it — nor could it, since a decomposition is not a step. The structural layer is strictly more discriminating than \(\bisim\) in general, and the resulting apparent conflict with adequacy is the subject of Chapter 20. Everywhere this book says “adequate” of a generated logic with structural connectives, the relation intended is the one that chapter supplies.
16.3 The Logical Metric
Fix an enumeration \((\phi_n)_{n \in \NN}\) of the formulae of \(\HML(\ctx)\), ordered compatibly with the partial order on contexts (smaller contexts appearing earlier).
\[d_{\HML}(u, v) \;=\; 2^{-n}, \quad\text{where}\quad n = \min\bigl\{k \;\mid\; u \sat \phi_k \not\Leftrightarrow v \sat \phi_k\bigr\}.\] If \(u \bisim v\), set \(d_{\HML}(u, v) = 0\).
\(d_{\HML}\) is an ultrametric on \(\terms(\GSLT)/{\bisim}\). Terms differing only in behaviors triggered by large (expensive) contexts are closer under \(d_{\HML}\) than terms differing in behaviors triggered by small (cheap) contexts. This is the locality principle: local distinguishability weighs more than global.