Discussion and Future Directions

36.1 Relation to Existing Work

The reversibility construction is closely related to the work of Danos and Krivine on reversible CCS [5] and to Phillips and Ulidowski’s reversible process calculi. The present contribution is to show that this construction lifts uniformly to all GSLTs, and that the history it records is not merely a device for running backwards but a structure with its own arithmetic — the erasure lattice and the ledger law of Chapter 31.

The causal set interpretation connects to the causal set programme in quantum gravity [6]. The present framework gives a generative presentation of causal sets, via rewrite rules, rather than the axiomatic presentation standard in the physics literature.

Noticing physical structure in the dynamics of cut elimination is not new, and it is worth situating this part of the book in the older programme rather than claiming to open the register. Girard’s Geometry of Interaction took cut elimination as a dynamics and pursued it through operator algebras precisely in search of such correspondences; the categorical Geometry of Interaction abstracted that dynamics into traced monoidal structure; and the line continues into categorical quantum mechanics, where the same interaction structure yields a semiring of scalars and a Born rule [91]. The semiring parametrisation of Chapter 30 is a small contribution to that tradition, not a departure from it.

The context-decorated HML and the Milner–Sewell–Leifer construction are established; what is new here is their use as the index set for the decoration, and the internalization of dynamical data into the modal operators.

36.2 What This Part Does Not Establish

It is worth collecting the negative results, since they are more useful than the positive ones for anyone wishing to push the programme forward.

1. There is no Legendre transform here, and there is no pair of objects between which one could be taken. An earlier presentation posed the invertibility of such a transform as an open question; the question was ill-posed, since the two maps it related were one map at two semirings. It is withdrawn rather than answered.

2. There is no variational principle in the complex instance. Least action is available in the tropical instance (Proposition 30.1) and the relation between the two is the relation between tropicalisation and a classical limit, which we have not made precise.

3. There is no interference between rewrites, for two structural reasons rather than one (Remark 33.3). There is a slot for coherence in the equations a presentation declines to quotient (Section 33.3), and nothing here says which equations a physical theory would withhold, or where the hopping amplitudes would come from.

4. There is no equivalence appropriate to a theory with a nonzero Hamiltonian. Rate bisimulation serves at \(H = 0\) and transfers to the complex case there without further work; when coherences are present, a relation on configurations must respect them, and we have no candidate.

5. There is no action relating the geometric and matter parts of a weighting. Remark 30.4 observes that the propensity splits canonically into a factor depending on where in a term an interaction sits and a factor depending on what is transferred. A field theory is what one gets when the two are forced to determine one another, and forcing them is not attempted here.

6. There is no generator. The conserved charge is established; that it also generates reduction is Conjecture 31.1 and Conjecture 31.2, which approach the same missing object from the two sides of the ledger law.

36.3 Open Questions

1. Universality of the reversibility envelope. Is \(\GSLT^\dagger\) the minimal reversible GSLT receiving a morphism from \(\GSLT\) — does \(\eta : \GSLT \to \GSLT^\dagger\) satisfy a universal property in \(\mathbf{GSLT}\)?

2. Symplectic structure. The ledger law \(\sigma + \kappa = \sigma_0\) suggests a conjugate pair more concretely than the earlier phase-space analogy did: \(\sigma\), the fuel not yet spent, against \(\kappa\), the record of what has been. Does the space of bisimulation classes carry a symplectic form for which these are conjugate coordinates, and is the erasure lattice a lattice of Lagrangian submanifolds?

3. Does the nearness relation obey a field equation? Remark 31.9 observes that located authority couples the spatial and temporal structures. Cut elimination redistributes information, which changes which cuts are enabled, which selects the next redistribution. That is the shape of Einstein’s intuition, with the information distribution in the role of the source and the nearness structure in the role of the metric. Whether the coupling satisfies anything one would recognise as a field equation is entirely open.

4. Which erasure is the physical state space? Corollary 31.1 asserts a coarsest energy-conserving grade. Its existence in full generality depends on the erasure lattice possessing the relevant joins, which is known under finiteness of the reduction graph and not in general.

5. The rho calculus case. The involution \({*}{@}P = P\) suggests the rho calculus is closer to self-dual than most GSLTs. Can the reversibility envelope be built with less added structure, exploiting this symmetry?

6. Noether, made precise. Can every symmetry of the equations \(\eqs\) be shown to correspond to a conserved component of the account? The deflationary reading of Chapter 31 gives one instance — path-independence of conversion yielding the virtual token — and it is the only one we have.