Chapter 34
Synthesis: The Full Structure
We now collect the constructions and state what has and has not been established.
34.1 The Dictionary
The status column carries the same convention as the preview table of Chapter 27: con for a construction, true by definition of the objects involved; thm for a theorem with a hypothesis that can fail; cnj for a conjecture. A dictionary without such a column invites the reader to grant every row the same authority, and the rows do not have the same authority.
The structural correspondences first:
{1.3}
| GSLT concept | Physical concept | Status |
|---|---|---|
| Term | State / initial condition | con |
| Rewrite rule | Law of motion | con |
| Rewrite sequence (path) | Trajectory | con |
| Synchronization tree | Causal graph / light cone | con |
| \(d_{\min}(P,Q)\) | Proper time / causal depth | con |
| \(d_{\max}(P,Q)\) | Complexity of history | con |
| Width of \([P,Q]\) | Degree of causal concurrency | con |
| Equations \(\eqs\) | Gauge equivalence | con |
| \(\GSLT^\dagger\) | Time-symmetric theory | con |
| Empty trace \(\eps\) | Initial condition (no causal past) | con |
| \(d_{\HML}\) | Metric on state space | con |
The decoration, and what choosing its semiring chooses:
{1.3}
| GSLT concept | Physical concept | Status |
|---|---|---|
| Decoration \(\dec\), semiring \(\Semi\) | Choice of dynamical theory | con |
| tropical instance | Action functional | con |
| \(\min\) over paths | Principle of least action | thm |
| complex instance | Path amplitude \(e^{iS[\gamma]/\hbar}\) | con |
| sum over paths | Feynman path integral | con |
| cancellation of paths | Quantum interference | cnj |
| Dynamic decoration | Field with its own dynamics | con |
Conservation, dissipation, memory, and authority:
{1.3}
| GSLT concept | Physical concept | Status |
|---|---|---|
| Conversion system | Interconvertible resource kinds | con |
| No-arbitrage | Existence of an energy function | thm |
| Virtual token \(\nu\) | Energy, as a Noether charge | thm |
| Hodge split of \(\ell\) | Energy versus circulation | thm |
| \(\bt(\Gamma)\) | Degrees of arbitrage freedom | thm |
| Dissipation \(\theta\) | Second law; free energy (exergy) | thm |
| Starvation as absorbing set | Mortality | thm |
| Ledger law \(\sigma + \kappa = \sigma_0\) | Potential plus kinetic | thm |
| Holonomy \(\hol(\gamma)\) | Failure of energy to be a state function | thm |
| Erasure bounded by holonomy | Landauer’s principle | thm |
| Located token stack | Capability; who may spend | con |
| Location entangles \(K\) with the stack | Spacetime, not space \(\times\) time | cnj |
| \(\nu\) generates a reduction step | Hamiltonian | cnj |
| Symmetry of the decoration | Noether current | cnj |
Counting the column is instructive. The constructions are numerous and cheap; they say that the framework can express the physics, which was never seriously in doubt. The theorems are fewer and are the reason to care: each has a hypothesis that can fail, and each says that something familiar from physics is forced by something structural about computation. The conjectures are the three places where the analogy is currently doing work the mathematics has not yet done, and two of the three concern the same missing object — a generator.
34.2 The Main Construction
Given a GSLT \(\GSLT = (\terms, \eqs, \rules)\), a semiring \(\Semi\), a refinement-complete decoration \(\dec\), and a conversion system on the resource kinds, define \(\GSLT^{\dagger\dec}\) with:
terms the triples \(\langle P, \trace, \vect{A}\rangle\), where \(\vect{A}\) is a family of located accounts, one per surface holding a stack;
rules the forward steps (drawing \(\dec_r(u)\) from the account at the drawing surface, recording the decoration in the trace) and their reversals;
\(\eqs\) lifted to the current-term component.
The extended HML of Definition 32.1 internalizes the decoration as logical data.
In \(\GSLT^{\dagger\dec}\):
Ledger. Fuel remaining plus fuel recorded spent is invariant: \(\sigma(t) + \kappa(t) = \sigma_0\) (Proposition 31.5). This holds by construction.
Value. If the conversion system is arbitrage-free, the total virtual-token value \(\nu\) is invariant under every engine operation (Proposition 31.3); if it is lossy, \(\nu\) is a Lyapunov function and the honest scalar is free energy (Proposition 31.4). This has a hypothesis and can fail.
Memory. Energy descends to the folded history exactly when the folded loops carry no holonomy (Theorem 31.2); conservation therefore sets a lower bound on retained history, coinciding with the Landauer bound (Remark 31.7).
Time-reversal. Reversing the trace and applying the reversal \(\dec^{\dagger}\) is an automorphism of \(\GSLT^{\dagger\dec}\).
Probability conservation is not on this list. Unitarity would require the amplitudes at each state to be normalised and the paths to be poolable, and Remark 33.2 is the reason the second condition is not available.
34.3 From Construction to Code
The construction is algorithmic at every stage. For a given GSLT:
Represent terms as algebraic data types in the implementation language.
Compute minimal contexts via the Milner–Sewell–Leifer algorithm on the rewrite rules; store as a context lattice.
Evaluate HML formulae against a term, and check refinement-completeness of the intended decoration domain — if the most refined witness is not unique, the decoration is not well defined and the implementation will silently choose.
Attach the decoration to each rule as a map from formula identifiers into the chosen semiring, together with the table updates if the decoration is dynamic.
Locate the accounts. Every stack lives on a channel; none floats free. This is a correctness requirement, not an optimisation.
Extend terms with trace and accounts, implementing forward and backward rules as the reversible rewrite system.
Simulate in the stochastic instance via Gillespie: compute exit rates, sample the next transition and waiting time, advance the term, update the table, draw on the account, record the trace. By Theorem 13.1 the object being stepped is a chain over configurations rather than over terms, and by Theorem 13.3 the same loop at a nonzero Hamiltonian is a quantum-jump unravelling, so the last step is one procedure and not two.
Each step is a well-defined computational procedure, and steps 4–7 are implemented for the specific case of MeTTaIL rewrite rules [32].