Chapter 20
Instruments: Making Structure Visible to Bisimulation
The previous chapter generated a logic from a presentation. This one settles a question about that logic which, left open, would quietly undermine everything the next part builds on it — and which a reader who knows the concurrency literature will raise on sight.
20.1 Two claims that look inconsistent
A generated logic is worth generating only if it is adequate: logical equivalence should coincide with the calculus’s observational equivalence. Chapter 19 was careful to say that adequacy is a property of the logic one asks for rather than of the generator, and that a logic missing conjunction or negation will not have it. What that section did not address is a sharper objection, which does not turn on missing connectives at all.
The generated logic has a structural layer: one connective per term constructor, with \[P \sat C(\varphi_1,\dots,\varphi_n) \iff P =_{\eqs} C(t_1,\dots,t_n) \text{ with } t_i \sat \varphi_i \text{ for each } i .\] When the constructor in question is the interaction cut, and the cut is subject to associativity, commutativity and a unit, this connective is a separating conjunction: \(P \sat \varphi \Par \psi\) holds exactly when \(P\) admits some decomposition into two parts satisfying \(\varphi\) and \(\psi\) respectively. And that existential over decompositions is not a step. No modality expresses it, because nothing happened.
So one wants to assert both of \[\begin{align} \text{logical equivalence} \;&=\; \text{observational equivalence}, \tag{A}\label{ox:eq:A}\\ \text{the structural layer} \;&\subsetneq\; \text{observational equivalence}. \tag{B}\label{ox:eq:B} \end{align}\] Read carelessly these are inconsistent, and a careful reader will say so. The book asserts both. (A) is what Chapter 19 wants and what the Wigner argument of Chapter 21 leans on. (B) appears in Chapter 21 too, where the strict refinement of context-labeled bisimulation by the spatial layer is offered as the reason the ecology needs a narrower class of morphisms than \(\catGSLT\) supplies.
A referee put it to me exactly this way, and was right to. If structural inspection is an admissible observation, then interaction was never the whole observational ceiling; and if it is not, those predicates should not be among the scientist’s senses. One cannot have it both ways without saying more.
20.2 The resolution
There is no such thing as the observational equivalence of a calculus independent of what the observer is permitted to do.
(B) is a statement about bisimilarity in a theory \(\GSLT\) where the observer may build contexts out of \(\GSLT\)’s own constructors and watch what happens. (A) is a statement about bisimilarity in a theory where the observer additionally holds instruments for taking terms apart. These are two members of a family. Exhibit the index and there is nothing to reconcile.
The construction that exhibits the index is the subject of this chapter. Its slogan:
Make every term former an interaction. Bisimulation observes interactions. Therefore bisimulation observes every term former.
The phenomenon is not new. Caires observed the apparent gain in discriminating power in the spatial logic for the \(\pi\)-calculus [43, 44], and within a few years results in that community established that suitable behavioral equivalences see what the spatial connectives see, so that spatial logics need not be counted intensional [28, 29]. Those results are semantic: they exhibit a calculus, show that its observational equivalence is characterized by a spatial logic, and the extra separating power comes from features of that calculus. What follows is instead syntactic. It is a transformation of presentations: read the signature, adjoin some atoms, add three rules per constructor, stop. It applies to any interactive GSLT meeting the conditions of §20.3 rather than to one calculus, and — this is the part that matters here — because it is mechanical in the presentation, it composes with the machinery of Chapter 19, which is also mechanical in the presentation. Adequacy then becomes the statement that two functions of the same argument agree, rather than a coincidence to be checked calculus by calculus.
An earlier version of this material braided three claims together tightly enough that a weakness in one looked like a weakness in all three. They are: operational reconstruction, what the enlarged transition system can distinguish (§20.5); logical expressiveness, what the generated structural language can distinguish (§20.6); and observer capability, which instruments a given observer actually holds (§20.8, §20.10). They are proved separately below and should be cited separately.
It is not being claimed that structural inspection was interaction all along. That would be slippery. The form of observation remains transition observation; what changes is that the set of observable transitions has been enlarged, and the enlargement is exactly what supplies the additional discriminating power. The defensible statement is that structural observation can be represented as interaction, after conservatively extending the observer’s transition theory with destructuring actions. An architecture that appeals to this construction should say its observer holds instruments, not that its instruments were never instruments.
20.3 What is fixed, and what is a parameter
Fix an interactive GSLT \(\GSLT = (\Sigma, \eqs, \rules)\) in the sense of Chapter 8: a signature, a set of equations, a set of rewrite rules, and a distinguished binary constructor \(\Cut\) — the cut — such that the left-hand side of every rule is of the form \(\Cut(l_1,l_2)\) up to \(=_{\eqs}\). Parallel composition plays this role for CCS, the \(\pi\)-calculus, the ambient calculus and \(\rhoc\); application plays it for the \(\lambda\)-calculus.
20.3.1 Labels are minimal enabling contexts
Chapter 16 fixed the label discipline: a transition \(P \xrightarrow{K} Q\) is asserted when \(K\) is a least context enabling a rewrite. Two refinements of that chapter’s presentation are used here and are stated in Remarks 16.1 and 16.2 there: minimality is a universal property rather than a subterm condition, and labels carrying process payloads are matched up to the bisimilarity being defined rather than syntactically.
Minimality is not a technical convenience. It is what keeps a label from carrying the whole term. A transition system labeled by arbitrary enabling contexts would be so informative that matching labels would nearly force syntactic agreement, and the equivalence it induced would already sit at or near \(=_{\eqs}\) — collapsing the very distinction this chapter exists to draw. We return to this in §20.7, where it does real work.
\(\GSLT\) has all redex-relative pushouts, so that the derived transition system exists.
\(\GSLT\) comes equipped with a class \(\mathcal{A}\) of contexts, containing those built from the rewrite constructors, such that context-labeled bisimilarity is a congruence with respect to \(\mathcal{A}\), and observations are restricted to \(\mathcal{A}\).
Both are inherited from [27], where establishing them for the theories of interest is work in progress; everything below is conditional on them. They are conditions rather than theorems deliberately. We are interested only in context-labeled transition graphs that make bisimulation a congruence. Barbed bisimulation, which obtains congruence by quantifying over contexts and a calculus-specific notion of observable, does not generalize across interactive GSLTs and is not used. Deriving labels from contexts so that congruence holds by construction is the whole point of the Leifer–Milner apparatus [2].
Condition 20.2 is not idle. For \(\rhoc\), congruence holds 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)\): communication turns on name equality, not on bisimilarity, so \(p \bisim q\) with \(p \neq q\) gives \(@p \neq @q\) and the two contexts behave differently. §20.10 returns to what this costs the present construction.
20.3.2 Admissible equational theories
The results need \(\eqs\) to admit a well-founded notion of decomposition. Better to isolate the conditions than to discover them mid-proof.
For a term \(P\) let \(|P|\) be the number of constructor occurrences and \(\mu(P) = \min\{\,|Q| : Q =_{\eqs} P\,\}\). A representative attaining the minimum is lean.
\(\eqs\) is admissible when:
- (E1) Well-founded.
Every \(=_{\eqs}\)-class of closed terms contains a lean representative.
- (E2) Hereditary.
If \(C(\vec t\,)\) is lean then each \(t_i\) is lean, and for \(n \ge 1\) we have \(\mu(t_i) < \mu(C(\vec t\,))\).
- (E3) Sorted.
\(\eqs\) relates only terms of the same sort.
It is tempting to say instead that \(\eqs\) is size-respecting on the presentations of interest. It is not. The unit law \(P \Par \mathbf{0} = P\) is not size-respecting, and it is one of the equations doing the most work below, since it is what makes \(P \Par \mathbf{0}\) one of the decompositions the separating conjunction quantifies over. (E1)–(E2) are the repair. They say nothing about how many decompositions a term has — possibly infinitely many — only that one may always descend along a lean one. Associativity, commutativity and unit for the cut satisfy them.
20.4 The construction
The cut is binary; constructors have arbitrary arity and heterogeneous argument sorts. To present the arguments of an \(n\)-ary constructor to the cut they must be gathered into one operand.
One might encode the arguments as a list and appeal to Turing completeness to supply the list former. That would be wrong twice over. Computability guarantees the ability to represent data; it does not supply an internal coding function injective modulo an arbitrary \(\eqs\), and injectivity modulo \(=_{\eqs}\) is exactly what the reconstruction below needs. And a general lambda theory is many-sorted, so a homogeneous list cannot hold heterogeneous arguments without a universal code sort, which is a further construction choice. The repair is simpler than the thing repaired: freely adjoin an argument former per signature profile. Free adjunction gives correct sorting and injectivity by construction, introduces no encoding choice, and keeps Turing completeness out of the chapter entirely.
Let \(\Ob \subseteq \Sigma\) be an observation signature. The observer extension \(\Obs(\GSLT,\Ob) = (\Sigma^{\Ob}, \eqs, \rules^{\Ob})\) is given by:
for each \(C \in \Ob\) of profile \(\tau_1 \times \cdots \times \tau_n \to \tau\), a fresh sort \(A_C\) and a freely adjoined former \(\args_C : \tau_1 \times \cdots \times \tau_n \to A_C\);
nullary probe atoms \(\Ask_C\), \(\Bld_C\) and \(\Get_{C,i}\) for \(1 \le i \le n\);
the cut overloaded so that \(\Cut(\Ask_C, t)\), \(\Cut(\Get_{C,i}, a)\) and \(\Cut(\Bld_C, a)\) are well formed for \(t : \tau\) and \(a : A_C\);
\(\eqs\) unchanged;
\(\rules^{\Ob} = \rules \cup \{\,\mathrm{ask}_C,\ \mathrm{get}_{C,i},\ \mathrm{bld}_C : C \in \Ob\,\}\) where \[\begin{align*} \mathrm{ask}_C &: \;\; \Cut(\Ask_C,\, C(x_1,\dots,x_n)) \;\rewrite\; \args_C(x_1,\dots,x_n),\\ \mathrm{get}_{C,i} &: \;\; \Cut(\Get_{C,i},\, \args_C(x_1,\dots,x_n)) \;\rewrite\; x_i,\\ \mathrm{bld}_C &: \;\; \Cut(\Bld_C,\, \args_C(x_1,\dots,x_n)) \;\rewrite\; C(x_1,\dots,x_n). \end{align*}\]
Rules of \(\rules\) are proper; the rest are administrative. Write \(\GSLT^{+}\) for \(\Obs(\GSLT,\Sigma)\).
Four comments on the shape of this definition, because each records a choice that could have gone otherwise.
The cut is overloaded rather than a fresh eliminator introduced.
This is the point of the whole construction. The cut is not an arbitrary constructor; it is the one the transition relation is indexed on, the one that defines what it means for two things to meet. A probe placed in interaction position turns a structural question into a rendezvous, and a rendezvous is what a derived transition system is built to observe.
Every administrative rule is interaction-headed by construction.
Its left-hand side is literally a cut. Putting the constructor being opened on the left of the arrow instead would force an appeal to a unit for the cut, and a special case for cuts without one. Putting the probe on the left removes the case distinction: the observer supplies the context, so no unit is needed anywhere.
The probe atoms are indexed.
It is \(\Ask_C\) rather than a single \(\Ask\) that makes the label of an opening transition record which constructor was found, and \(\Get_{C,i}\) rather than a single \(\Get\) that makes projection record which argument was taken. That is what carries the information the reconstruction needs.
The build rule is used in no proof below.
The rule \(\mathrm{bld}_C\) is present so that the extension supplies construction as well as deconstruction, and so that the observer’s instruments form a coherent kit rather than a one-way mirror.
\(\Obs(\GSLT,\Ob)\) is a GSLT, is interactive with the same cut, and reflects proper transitions: for \(\Sigma\)-terms \(P,P'\) and \(\rho \in \rules\), \(P \xrightarrow{K} P'\) in \(\GSLT\) iff the same holds in \(\Obs(\GSLT,\Ob)\).
Every rule of \(\rules^{\Ob}\) has a left-hand side of the form \(\Cut(-,-)\): those of \(\rules\) by hypothesis, the administrative ones by construction. Reflection of proper transitions holds because \(\rules^{\Ob} \supseteq \rules\) and the adjoined formers are mentioned in no rule of \(\rules\), so no \(\rules\)-redex is created or destroyed by their presence, and the relative pushouts computed for \(\rules\)-redexes are unchanged.
One may prefer a presentation with no equations, orienting each equation of \(\eqs\) in both directions and adding both to the administrative rules. The two presentations agree up to administrative steps. We keep \(\eqs\) as equations because doing so localizes the source of nondeterminism: with \(\eqs\) retained, the branching of \(\mathrm{ask}_C\) comes from \(\eqs\)-matching, which is exactly the existential over decompositions that the separating conjunction quantifies. It is worth stressing that these must be pairs. Orienting the equations in one direction only would let bisimilarity fall below \(=_{\eqs}\) onto raw syntax, which overshoots: the structural connectives respect \(=_{\eqs}\), so a relation finer than \(=_{\eqs}\) is finer than the logic, and adequacy fails from the other side.
20.5 Reconstruction
Let \(P\) be a \(\Sigma^{\Ob}\)-term and \(C \in \Ob\) be \(n\)-ary. Then \[P \xrightarrow{\;\Cut(\Ask_C,\,-)\;} \args_C(t_1,\dots,t_n) \quad\text{iff}\quad P =_{\eqs} C(t_1,\dots,t_n),\] and \(\Cut(\Ask_C,-)\) is a least context enabling \(\mathrm{ask}_C\) at \(P\). Consequently the \(\Ask_C\)-labeled transitions of \(P\) enumerate exactly the top-level \(\eqs\)-decompositions of \(P\) at \(C\). Likewise \(\args_C(\vec t\,)\) has the single transition \(\xrightarrow{\Cut(\Get_{C,i},-)} t_i\) with that label.
The redex \(\Cut(\Ask_C, C(\vec x))\) is formed from \(P\) by the context \(\Cut(\Ask_C,-)\) exactly when \(P =_{\eqs} C(\vec t\,)\); no smaller context enables it, since the rule’s left-hand side requires the probe, and no larger one is minimal. Matching is up to \(=_{\eqs}\), which is where the enumeration comes from. For \(\mathrm{get}\), \(\args_C\) is freely adjoined, so \(\args_C(\vec t\,) =_{\eqs} \args_C(\vec s\,)\) iff \(t_i =_{\eqs} s_i\) for all \(i\), and the projection is deterministic.
This is the lemma that does the work, and it is worth pausing on what it says in the case that motivated the difficulty. Take \(C\) to be the cut with \(\eqs\) containing associativity, commutativity and unit. Then \(P\)’s \(\Ask_{\Cut}\)-labeled transitions are in bijection with the ways of writing \(P\) as \(Q \Par R\) — including \(P \Par \mathbf{0}\) and \(\mathbf{0} \Par P\), and every rebracketing and permutation of a parallel product. The existential over splits in \(P \sat \varphi \Par \psi\) has become an existential over transitions. Everything else in this chapter is bookkeeping.
If \(P =_{\eqs} Q\) then \(P \bisim_{\Obs(\GSLT,\Ob)} Q\).
Transitions are defined up to \(=_{\eqs}\), so \(=_{\eqs}\)-equal terms have identical labeled transition sets, and the identity relation on \(=_{\eqs}\)-classes is a bisimulation.
Trivial as stated, and stated anyway, because it fixes the lower bound of the calibration: the enlargement must not push bisimilarity below the equational theory, or it overshoots the logic. It is also the property against which the alternative presentation of Remark 20.5 must be checked.
Let \(\GSLT\) satisfy Conditions 20.1 and 20.2 with \(\eqs\) admissible, and let \(\Ob = \Sigma\). Then for closed \(\Sigma\)-terms \(P,Q\), \[P \bisim_{\GSLT^{+}} Q \iff P =_{\eqs} Q .\]
(\(\Leftarrow\)) is Lemma 20.2.
(\(\Rightarrow\)) By strong induction on \(\mu(P)\), with induction hypothesis: for all closed \(P',Q'\) with \(\mu(P') < \mu(P)\), if \(P' \bisim_{\GSLT^{+}} Q'\) then \(P' =_{\eqs} Q'\). Note that the hypothesis constrains only the left argument, which is what allows the right-hand witnesses produced below to be arbitrary representatives rather than lean ones.
Let \(P \bisim_{\GSLT^{+}} Q\) and choose a lean representative \(C(t_1,\dots,t_n)\) of \(P\), which exists by (E1). By Lemma 20.1, \(P \xrightarrow{\Cut(\Ask_C,-)} \args_C(t_1,\dots,t_n)\). Since \(P \bisim_{\GSLT^{+}} Q\), the term \(Q\) must match this step with a label related to \(\Cut(\Ask_C,-)\). That label has no process payload — \(\Ask_C\) is a nullary atom and the hole is the only other position — so label matching is identity on the constructor skeleton, and \(Q\)’s matching label is \(\Cut(\Ask_C,-)\) itself. Distinct constructors carry distinct atoms, so no other opening rule could have matched. By Lemma 20.1 again, \(Q =_{\eqs} C(s_1,\dots,s_n)\) for some \(\vec s\), and \(\args_C(\vec t\,) \bisim_{\GSLT^{+}} \args_C(\vec s\,)\).
Now apply \(\Get_{C,i}\). By Lemma 20.1 each side has exactly one transition with label \(\Cut(\Get_{C,i},-)\), to \(t_i\) and \(s_i\) respectively, so \(t_i \bisim_{\GSLT^{+}} s_i\) for each \(i\).
By (E2) each \(t_i\) is lean and, for \(n \ge 1\), \(\mu(t_i) < \mu(P)\). The induction hypothesis gives \(t_i =_{\eqs} s_i\), whence \(P =_{\eqs} C(\vec t\,) =_{\eqs} C(\vec s\,) =_{\eqs} Q\). For \(n = 0\) the constructor is nullary and \(P =_{\eqs} C =_{\eqs} Q\) directly.
Theorem 20.1 is a statement about \(\bisim_{\GSLT^{+}}\) restricted to closed \(\Sigma\)-terms. The relation itself is defined on all of the extended signature’s terms, where it also identifies \(\args_C(\vec t\,)\) with \(\args_C(\vec s\,)\) exactly when the components agree. The distinction matters in Proposition 20.2.
A term with replication has infinitely many \(\eqs\)-decompositions and therefore infinitely many \(\Ask_{\Cut}\)-labeled transitions. Nothing in the proof requires image-finiteness: the induction is on \(\mu\), not on transition depth, and no Hennessy–Milner style characterization is invoked. §20.6 is what makes this safe on the logical side as well.
For a binding constructor the arguments are abstractions rather than closed terms, and Theorem 20.1 as proved does not cover them. It would need \(\alpha\)-equivalence to be part of \(\eqs\) and (E1)–(E2) to hold of the resulting classes, a notion of transition beneath a binder, and a statement of what \(\Cut(\Ask_C,-)\) means when \(C\) binds. The lambda-theoretic setting should supply all three — an abstraction is a term of the theory, so the induction has somewhere to go — but expecting is not proving. The theorem is therefore stated for the first-order fragment. This is the largest gap between what this chapter proves and what it would like to prove, and it is listed as such in the front matter.
\(\bisim_{\GSLT^{++}}\) and \(\bisim_{\GSLT^{+}}\) agree on the terms of \(\Sigma^{\Sigma}\).
Since \(\GSLT^{++}\) has more rules than \(\GSLT^{+}\), monotonicity (Proposition 20.4) gives \(\bisim_{\GSLT^{++}} \subseteq \bisim_{\GSLT^{+}}\). For the converse we exhibit a bisimulation rather than invoke Theorem 20.1 on both sides, which would be a domain mismatch of the kind Remark 20.6 warns about.
Take \(\mathcal{R} = \bisim_{\GSLT^{+}}\) and check the additional transitions. The constructors adjoined by Definition 20.3 are of two kinds. The probe atoms are nullary: their \(\mathrm{ask}\) rules have targets with no components, so the transition carries no information beyond the identity of the atom, which \(\bisim_{\GSLT^{+}}\) already fixes, since \(\Cut(\Ask_C,-)\) appears in labels. The argument formers are not nullary, but the \(\Get_{C,i}\) rules of \(\GSLT^{+}\) already project every one of their components, so the second-round opening transition is matched whenever the first-round projections are, and adds no separating power. Hence \(\bisim_{\GSLT^{+}}\) satisfies the \(\GSLT^{++}\) matching conditions.
This is not a side remark. It is the reason \(\Obs\) is a construction rather than the first stage of a colimit, and it turns on a design decision that could have gone the other way: the probes are nullary and the argument formers are exhaustively projected. Introduce a family of \(n\)-ary destructors with partial projections instead and the ladder is real.
20.6 Separation
The operational side is done. The logical side is a separate question. It would be convenient to import it from the literature, but those are theorems about particular spatial logics and particular calculi, and since the point here is to generalize past the calculus-by-calculus treatment, borrowing the key step defeats the purpose. We prove what is needed directly.
Let \(\eqs\) be admissible. Then for closed \(\Sigma\)-terms \(P,Q\), \[P =_{\mathcal{L}_{\mathrm{s}}(\GSLT)} Q \iff P =_{\eqs} Q ,\] where \(\mathcal{L}_{\mathrm{s}}(\GSLT)\) is the structural fragment of the generated logic.
(\(\Leftarrow\)) Satisfaction of structural connectives is defined up to \(=_{\eqs}\).
(\(\Rightarrow\)) We construct a characteristic formula. For closed \(P\), by (E1) choose a lean representative \(C(t_1,\dots,t_n)\) and set \[\chi_P \;:=\; C(\chi_{t_1},\dots,\chi_{t_n}),\] well defined by induction on \(\mu\), using (E2) for the descent, with \(\chi_P := C\) for nullary \(C\).
We claim \(Q \sat \chi_P\) iff \(Q =_{\eqs} P\). If \(Q \sat C(\chi_{t_1},\dots,\chi_{t_n})\) then \(Q =_{\eqs} C(s_1,\dots,s_n)\) with \(s_i \sat \chi_{t_i}\), so by induction \(s_i =_{\eqs} t_i\), so \(Q =_{\eqs} C(\vec t\,) =_{\eqs} P\). Conversely \(P \sat \chi_P\) by construction. Hence if \(P \neq_{\eqs} Q\) then \(\chi_P\) separates them.
Three things. The argument is self-contained: no separation result is imported at a generality its source does not support. The image-finiteness objection dissolves, because the argument goes from the logic to \(=_{\eqs}\) directly by characteristic formulae and never passes through a Hennessy–Milner characterization of bisimulation, which is where image-finiteness or infinitary conjunction would have been needed. And the hypotheses are visible: separation holds exactly for admissible \(\eqs\), so a presentation whose equational theory fails (E1)–(E2) is one for which nothing is claimed. Note also that no boolean structure was used — \(\chi_P\) is purely structural.
Under the hypotheses of Theorems 20.1 and 20.2, for closed \(\Sigma\)-terms \[=_{\mathcal{L}_{\mathrm{s}}(\GSLT)} \;=\; =_{\eqs} \;=\; \bisim_{\GSLT^{+}} .\] The structural fragment generated from \(\GSLT\) is adequate for context-labeled bisimulation in \(\GSLT^{+}\).
That is the statement (A) should have been all along. It is adequacy with an index.
20.7 The gap is really there
Corollary 20.1 would be worthless if bisimilarity in \(\GSLT\) were already \(=_{\eqs}\), since the construction would then close a gap that was not there. The same observation settles that and supplies (B) for our relation rather than the literature’s.
Let \(\GSLT\) contain two distinct nullary constructors \(c,d\) of the same sort occurring in no rule of \(\rules\) and in no equation of \(\eqs\). Then \(c \bisim_{\GSLT} d\) and \(c \neq_{\eqs} d\), so \(\bisim_{\GSLT^{+}} \subsetneq \bisim_{\GSLT}\).
Neither \(c\) nor \(d\) occurs in any left-hand side, so neither contributes a redex, and for any context \(D\) the transitions of \(D[c]\) and \(D[d]\) are in label-preserving bijection with those of \(D[-]\)’s own redexes. Hence \(\{(c,d)\} \cup {=_{\eqs}}\) extends to a bisimulation. They are \(=_{\eqs}\)-distinct by hypothesis, so by Theorem 20.1 they are not \(\bisim_{\GSLT^{+}}\)-related, witnessed by \(\Cut(\Ask_c,-)\).
The example is deliberately austere: it shows the gap is nonempty for essentially any signature carrying inert data, without relying on a coincidence of the equational theory.
In a presentation with replication as a primitive constructor and \(\eqs\) not containing the unfolding law, \(!P\) and \(!P \Par P\) are behaviorally indistinguishable and \(=_{\eqs}\)-distinct, so they witness the gap. If \(\eqs\) does contain the unfolding law they are \(=_{\eqs}\)-equal and witness nothing. The size of the gap is a property of the presentation, not of the calculus informally described — a point worth carrying to any argument in this book that turns on what a spatial connective can see.
Proposition 20.3 depends on labels being minimal. Were labels arbitrary enabling contexts, a label would carry essentially the whole surrounding term, matching would force near-syntactic agreement, and bisimilarity in \(\GSLT\) would sit at or near \(=_{\eqs}\) — leaving no gap to close and no content to Corollary 20.1. The label discipline of Chapter 16 is therefore not a technical preliminary but a load-bearing part of the statement.
20.8 The dial
Nothing forces the construction to be run on the whole signature. The point of Definition 20.3 taking \(\Ob\) as a parameter is that the observer’s instruments are part of the data.
If \(\Ob \subseteq \Ob'\) then \(\bisim_{\Obs(\GSLT,\Ob')} \subseteq \bisim_{\Obs(\GSLT,\Ob)}\), with \(\bisim_{\Obs(\GSLT,\varnothing)} = \bisim_{\GSLT}\) and, under the hypotheses of Theorem 20.1, \(\bisim_{\Obs(\GSLT,\Sigma)} = {=_{\eqs}}\) on closed \(\Sigma\)-terms.
The administrative rules in \(\Obs(\GSLT,\Ob')\) but not \(\Obs(\GSLT,\Ob)\) carry fresh probe atoms, hence fresh labels, and add transitions that must be matched; the largest relation satisfying more conditions is contained in the largest relation satisfying fewer. The endpoints are Proposition 20.1 and Theorem 20.1.
This is the sharp form of the resolution promised in §20.2. There is no single observational bisimulation against which a spatial logic must be measured. Observational equivalence is indexed by the destructuring capabilities admitted to the observer, and (A) and (B) name the two ends of the resulting family.
What does not follow, tempting as it is, is that the fragment of the logic retaining structural connectives only for \(\Ob\) is adequate for \(\bisim_{\Obs(\GSLT,\Ob)}\).
For \(\Ob \subseteq \Sigma\), \(\bisim_{\Obs(\GSLT,\Ob)}\) coincides with logical equivalence in the fragment of the generated logic whose structural connectives are those of \(\Ob\).
The obstacle is real. A formula may inspect an opened constructor sitting underneath an unopened one; equations may relate terms whose roots lie on opposite sides of \(\Ob\); and a binder may move material across an apparent structural boundary. None of that is handled by relativizing Theorem 20.1.
Conjecture 20.1 holds when \(\Ob\) is closed under the subterm relation of lean representatives — that is, when every constructor that can occur beneath a constructor of \(\Ob\) in a lean term is itself in \(\Ob\).
Under that condition the descent in the proofs of Theorems 20.1 and 20.2 never leaves \(\Ob\), so both arguments run verbatim with \(\Sigma\) replaced by \(\Ob\) and \(=_{\eqs}\) replaced by its restriction to the \(\Ob\)-generated subalgebra.
I suspect Conjecture 20.1 is the most interesting statement in the vicinity, and that its proof would say something about how partial structural knowledge composes.
An agent observing its environment faces three different limits, and collapsing them causes trouble downstream. There is the ideal observer with the full observation signature, whose reach is \(=_{\eqs}\). There is the capability-limited observer, holding some \(\Ob \subsetneq \Sigma\), whose reach is the corresponding point of Proposition 20.4. And there is the budget-limited observer, who holds instruments it cannot afford to use, whose reach is smaller again and is not characterized here at all. Adequacy is a claim about the first. Chapter 21 distinguishes the first and the third and will need the second as well.
20.9 Two cautions for anything built on this
20.9.1 Transitions and derivations
Lemma 20.1 says the \(\Ask_C\)-labeled transitions of \(P\) enumerate its decompositions. The transition relation is extensional: \(P \xrightarrow{K} P'\) holds when a witnessing \(\eqs\)-match exists. If two distinct \(\eqs\)-matches yield the same label and the same target up to \(=_{\eqs}\), they are one transition and two derivations.
For bisimulation this is immaterial — only existence is used. For any quantitative lift it is not: weights and costs attach to derivations, and a construction that collapses derivational multiplicity will misprice. Chapter 13 is careful about this on its own account, taking a redex to be a selection rather than a term up to congruence; anyone composing the two constructions should carry the derivation structure explicitly rather than the relation.
20.9.2 Cost is bounded by depth, not equal to it
In a cost-accounted GSLT every rewrite carries a price, and administrative rules are rewrites like any other. It is tempting to conclude that the price of evaluating a structural formula of depth \(d\) is a function of \(d\), so that pricing schedules stipulated elsewhere in this book become derived step counts. That is too quick. Nesting depth bounds the length of the longest sequential destructuring path, but the cost of checking depends further on branching: a conjunction requires two subchecks, a negation may require exhausting a search, and a separating conjunction may enumerate many \(\eqs\)-decompositions before finding one that works, or all of them before concluding that none does. Sharing and caching move the figure again.
The defensible statement is that depth bounds sequential destructuring depth, while actual checking cost depends additionally on branching and on the evaluation strategy for the boolean layer. This is worth stating plainly because Chapter 21 prices perception by formula depth and is explicit that the schedule is a choice; the present chapter says why no other answer was available, rather than leaving the choice looking like an oversight.
20.10 The construction is not capability-safe
This is stated plainly rather than hedged, because a reader who knows object-capability discipline will see it in Definition 20.3 and will want to know whether we noticed.
Unrestricted opening destroys encapsulation. Any observer may form \(\Cut(\Ask_C,-)\), so any term whatever may be taken apart, and \(\Get_{C,i}\) then yields the arguments as data. In a calculus where an opaque reference is the unit of authority, this is fatal: open the reference and harvest whatever authority its contents carry. Confinement fails, and with it every argument that depends on it.
The repair is known in outline. Mike Stay’s suggestion is that constructors and destructors should each take a capability token, so that the right to build and the right to open are held rather than ambient. There are two readings — a permission, licensing the rule, or a brand, so that building stamps the term and opening checks the stamp — and the second is the more useful, since it makes legibility a property of the term rather than a global property of the world. The token must gate the whole kit rather than opening alone, since an observer able to take an administrative step should be able to take its converse.
Remark 20.4 obtained the argument formers by free adjunction. That cannot be done again here. Unforgeability is not a claim about what can be computed, nor about what can be adjoined, but about what a context can write down: in a signature of freely adjoined constructors every term is writable by anybody, which is precisely why free adjunction was safe for the argument formers and is useless for a token. A genuine source of privacy must be imported — restriction, in the general case, giving a factory of the shape \(\mathsf{let}\ c = \mathsf{freshCap}()\ \mathsf{in}\ P\). Reflective calculi, in which a name is a quoted process, may be able to discharge the import internally; whether quotation originates privacy or merely propagates it from a seed is not settled here. Note that Chapter 21’s freshness-by-quotation result does not settle it either: not every interactive GSLT has a quote.
Whatever the factory is, Definition 20.3 must not be applied to it. Give it an opening rule and a token can be taken apart; if it can be taken apart it can be rebuilt; if it can be rebuilt it can be forged; and if it can be forged nothing is a capability. So the capability-safe version of the construction is not “the observer extension, with a caveat” but “the observer extension on \(\Ob \subseteq \Sigma \setminus F\), where \(F\) is the minting apparatus” — and the exclusion is what makes the rest of it safe. It is tempting to say the factory is the unique constructor admitting no destructor. That is more than can be supported: a system may carry several fresh-name generators, sealed abstract types, or independent minting authorities, and in nominal presentations freshness is a binder rather than a constructor at all. The property that matters is not uniqueness but that the mechanism generating unforgeable authority is not itself generically destructible.
20.10.1 Reflection, and an inherited restriction
The congruence restriction of §20.3 — no hole beneath the quote — is inherited here and constrains \(\Ob\). The opening rule for the quote, \(\Cut(\Ask_{@}, @(p)) \rewrite \args_{@}(p)\), does not itself place a hole beneath \(@\): the hole is beside the quote, not inside it. So one does not expect it to disturb congruence. But it is a genuine addition to the context class, and whether \(\mathcal{A}\) extended by the administrative contexts still supports congruence is a question for the machinery of [27] rather than for assertion here. A reader wanting a safe default may take \(\Ob\) to exclude the quote, at the cost of leaving the name predicate outside the correspondence of Corollary 20.1.
20.11 What this settles, and where it is spent
Adequacy claims survive contact with intensionality results.
A generated spatial–behavioral logic may be asserted adequate, provided the assertion names the relation: bisimulation in the observer extension for a stated \(\Ob\), not in the base. Assertions that omit the index are not wrong so much as ambiguous, and the ambiguity is what invites the objection of §20.1. Chapter 19’s discussion of adequacy should be read with this index supplied.
Spatial and behavioral addresses coincide.
In \(\Obs(\GSLT,\Ob)\) a decomposition site is a redex position, so constructions identifying a structural locus with a modal label — Chapter 21 has one, where crossover loci are matched against modal labels — are well typed rather than analogical. This does not supply an enabling theorem: a locus that is a redex position for an administrative rule need not correspond to a proper step reachable in \(\GSLT\), and claims about reachability still require their own argument. The construction makes the identification meaningful; it does not make it true.
Morphisms.
Where the morphisms of a category of GSLTs preserve bisimulation (Chapter 10), an assignment depending on spatial structure is not functorial, and the usual repair is to narrow the morphism class by hand to maps preserving the generated logic. Under Theorem 20.1 the narrowing is not a narrowing: logic-preserving maps of \(\GSLT\) are exactly bisimulation-preserving maps of \(\GSLT^{+}\), and the repair becomes functoriality on the image of \(\Obs(-,\Sigma)\). Chapter 21 states this where it is needed.
And a warning.
Example 20.1 is the one to carry forward. How much the spatial layer sees over and above bisimulation is a fact about the presentation, not about the calculus one has in mind. Two presentations of what a working programmer would call the same language can sit at different points of Proposition 20.4. Wherever this book argues from what a structural predicate can detect, that argument is presentation-relative, and the presentation is a modeling choice like any other.