Chapter 28
The Reversibility Construction
In a bare GSLT, rewrite rules are directed: once a term \(P\) reduces to \(Q\), there is in general no canonical way to recover \(P\) from \(Q\). This irreversibility is the computational analogue of thermodynamic time-asymmetry, and a physics needs it undone — we want a theory whose laws are time-symmetric and whose arrow of time lives somewhere else.
The construction that does this is already in the book. It is Chapter 12’s history monad, and this chapter is what that monad looks like when it is read as physics rather than as bookkeeping.
28.1 The envelope is the free history
Let \(\GSLT = (\terms, \eqs, \rules)\). The reversible envelope \(\GSLT^\dagger\) has:
terms the configurations of \(\Hist\GSLT\) — pairs \(\langle P, \trace \rangle\) of a current term and a word in the free monoid of rewrite events, written here as \(\trace = r_1(l_1) \cdot r_2(l_2) \cdots r_n(l_n)\) with \(l_i\) the specific left-hand side matched at step \(i\);
forward rules \(r^+\), the rewrites of \(\Hist\GSLT\): \(\langle l_r, \trace \rangle \rewrite \langle r_r,\, r(l_r) \cdot \trace \rangle\);
backward rules \(r^-\), their inverses: \(\langle r_r,\, r(l_r) \cdot \trace \rangle \rewrite \langle l_r, \trace \rangle\);
\(\eqs^\dagger\) lifting \(\equiv\) to the current-term component, leaving traces invariant.
The first two clauses are \(\Hist\GSLT\) verbatim. Only the third is new, and the point of stating the construction this way is that the third clause is free.
Given the forward rules of \(\Hist\GSLT\), the family \(\{r^-\}\) is the unique family of rules inverting them. Adding it therefore involves no choice.
By Proposition 12.2 the free history is the universal cover of the reduction graph, hence a tree: every configuration \(\langle P, \trace \rangle\) with \(\trace \neq \eps\) has exactly one parent, read off the head of \(\trace\). A rule inverting \(r^+\) must send that configuration to that parent, and \(r^-\) does.
Proposition 28.1 says \(\GSLT^\dagger\) is the free groupoid on the tree \(\Hist\GSLT\): formally inverting the arrows of a tree imposes no relations, because there are no loops for the inverses to interact with. This is the whole reason the reversibility construction is cheap. Reversibility is not something bought by adding structure to a theory. It is what a theory already looks like once it stops throwing its past away, and the history monad is the operation of stopping.
Two morphisms come with the monad rather than needing separate proof. The unit \(\eta : \GSLT \to \GSLT^\dagger\), \(P \mapsto \langle P, \eps \rangle\), is \(\Hist\)’s unit; the projection \(\pi : \GSLT^\dagger \to \GSLT\), \(\langle P, \trace \rangle \mapsto P\), is the functor stripping the log from Proposition 12.1. That \(\pi \circ \eta = \mathrm{id}_{\GSLT}\) is one of that adjunction’s triangle identities.
28.2 Reading it as physics
A term \(\langle P, \eps \rangle\) is an initial condition: it has no causal past. A term \(\langle P, \trace \rangle\) with \(\trace \neq \eps\) is a term with a recorded history. The time-asymmetry present in \(\GSLT\) (forward rules only) disappears in \(\GSLT^\dagger\): the laws are symmetric, and the arrow of time is entirely encoded in the boundary condition (\(\trace = \eps\) for the initial state). This is precisely the modern understanding of the thermodynamic arrow of time.
That remark is what this chapter adds, and it is worth being exact about which part of it the mathematics supplies. That the laws are symmetric is Construction 28.1. That the asymmetry has to go somewhere is Proposition 12.2: a tree has a root, and the root is the boundary condition. What is not supplied is any reason the actual world’s boundary condition should be \(\trace = \eps\) rather than something else, and nothing here should be read as offering one.
\(\GSLT^\dagger\) sits at the top of a lattice, and the rungs below it are the physics. Chapter 12 observes that erasures of history are monad quotients forming a lattice between the reversible cover and the irreversible base, each intermediate object a quotient of the reduction graph’s fundamental group by a chosen set of loops. Read physically, an intermediate cover is a coarse-graining: a description that keeps enough of the past to run backwards through some transitions and not others. Which loops one is permitted to close is which histories one can afford to forget — and by the ledger law \(\sigma + \kappa = \sigma_0\) of that chapter, together with Landauer’s principle, the affordable erasures are exactly the state-recoverable ones. The fully reversible envelope is the limiting case in which nothing is forgotten and nothing is paid for. An observer at an intermediate cover has a time-asymmetric physics not because the laws are asymmetric but because it cannot afford the receipts.
Nothing in this chapter assigns a value to a rewrite. Weights, costs and the semiring in which they live arrive in Chapter 30, and the composite object — terms \(\langle P, \trace, \vect{A}\rangle\) carrying a history and an account — is Construction 34.1. That composite is \(\Cost\) applied to \(\Hist\), and Chapter 12 notes that the order of application is meaningful. No distributive law between the two monads is stated anywhere in this book, so “a cost-accounted theory with recorded histories” should be read as the two constructions applied in the order Construction 34.1 applies them, and not as a canonical object.