Chapter 29
Causal Structure and Time
29.1 Closed and Open Synchronization Trees
The synchronization tree of a term comes in two varieties, reflecting two different notions of how a term can evolve: autonomously, and under interaction with an environment. The distinction is fundamental and ramifies throughout the framework.
The closed synchronization tree \(\mathcal{ST}_c(P)\) of a term \(P \in \terms(\GSLT)\) is the directed graph whose:
nodes are equivalence classes of terms reachable from \(P\) by autonomous rewrites \(\rewrite^*\), requiring no external context;
edges are labeled by rewrite rule instances: there is an edge \(Q \xrightarrow{r} Q'\) whenever \(Q \rewrite_r Q'\) by firing rule \(r\) without any surrounding context.
A term has a nontrivial closed synchronization tree if and only if it contains a redex — a sub-term that matches the left-hand side of some rule \(r\) without context. Terms with no available autonomous rewrite (normal forms, or terms awaiting a communication partner) have a trivial closed tree consisting of a single node.
The open synchronization tree \(\mathcal{ST}_o(P)\) of a term \(P \in \terms(\GSLT)\) is the directed graph whose:
nodes are equivalence classes of terms reachable from \(P\) via transitions in the Milner–Sewell–Leifer labeled transition system;
edges are labeled by minimal contexts: there is an edge \(Q \xrightarrow{K} Q'\) whenever \(K[Q] \rewrite Q'\) for minimal context \(K\).
Every term has a potentially rich open synchronization tree, even if its closed tree is trivial: a term that does nothing alone may exhibit complex behavior when placed in the right environment.
The closed tree records what a term does as a program — its autonomous computational behavior. The open tree records what a term does as a function of its environment — the full range of behaviors it can exhibit when placed in contexts. A term with a trivial closed tree but rich open tree is a pure interface: it does nothing alone but responds to everything. In the Rho calculus, \(x!(Q)\) is exactly this: it has no autonomous rewrite, but in the context \(\mathtt{for}(y \leftarrow x)P \mid [-]\) it fires immediately.
The open synchronization tree is precisely the tree unfolding of the Milner–Sewell–Leifer labeled transition system. The minimal contexts labeling its edges are the same minimal contexts that generate the context-decorated HML of Section 16. The open tree and the HML logic are two faces of the same structure: the tree is the extensional record of all transitions; the logic is the intensional language for describing them.
29.2 The Synchronization Trees as Causal Graphs
Both \(\mathcal{ST}_c(P)\) and \(\mathcal{ST}_o(P)\) are directed graphs whose transitive closures are partial orders. Each is a causal set in the sense of Bombelli–Lee–Sorkin: a locally finite partial order in which \(Q \leq Q'\) means “\(Q\) can causally influence \(Q'\).” The closed tree encodes autonomous causal influence; the open tree encodes interactive causal influence mediated by the environment.
The transitive closure of \(\mathcal{ST}_c(P)\) is a partial order on autonomously reachable terms. The transitive closure of \(\mathcal{ST}_o(P)\) is a partial order on interactively reachable terms and extends the closed order: \(\mathcal{ST}_c(P) \subseteq \mathcal{ST}_o(P)\) as directed graphs.
29.3 Causal Time
The autonomous causal distances are path lengths in \(\mathcal{ST}_c(P)\): \[\begin{align} d^c_{\min}(P, Q) &= \min\bigl\{|\gamma| \;\mid\; \gamma \text{ is an autonomous rewrite path from } P \text{ to } Q\bigr\} \\ d^c_{\max}(P, Q) &= \max\bigl\{|\gamma| \;\mid\; \gamma \text{ is an autonomous rewrite path from } P \text{ to } Q\bigr\} \end{align}\] The interactive causal distances are path lengths in \(\mathcal{ST}_o(P)\): \[\begin{align} d^o_{\min}(P, Q) &= \min\bigl\{|\gamma| \;\mid\; \gamma \text{ is a context-labeled path from } P \text{ to } Q\bigr\} \\ d^o_{\max}(P, Q) &= \max\bigl\{|\gamma| \;\mid\; \gamma \text{ is a context-labeled path from } P \text{ to } Q\bigr\} \end{align}\] where \(|\gamma|\) is the number of steps in \(\gamma\), equal to the nesting depth of the context labels along the path.
\(d^c_{\min}\) is autonomous proper time: the irreducible causal depth an agent traverses without environmental assistance. \(d^o_{\min}\) is interactive proper time: the minimum number of environmental interactions required to reach a target term. The width of an interval in either order measures causal concurrency, directly related to the width of parallel composition in the Rho calculus. The two notions coincide for terms where all behavior is eventually triggered autonomously, and diverge for terms that are pure interfaces awaiting environmental interaction.