Chapter 13
The History Monad
13.1 Keeping the past
A rewrite theory that discards its past is irreversible precisely because a configuration may have many predecessors. Recording which step was taken restores a unique one. That is the whole idea, and packaging it gives the mirror image of Chapter 12.
\(\Hist\) sends a continued interactive GSLT \(G\) to the theory whose configurations are pairs of a configuration of \(G\) and a word in the free monoid of rewrite events, with each rewrite additionally appending its own event to the word.
\(\Hist\) is the writer monad over the free monoid of rewrite events. Its unit attaches the empty history; its multiplication concatenates.
\((\Hist, \eta, \mu)\) is a monad on \(\catciGSLT\), and the evident functor installing the log is left adjoint to the functor stripping it, with induced monad \(\Hist\).
13.2 The free history is the reversible tree
The free history makes the graph of computation paths out of a term into a tree: it is the universal cover of the reduction graph, and reversibility is exactly its unique-parent property.
This is the structural content of the construction and it explains the erasures. An erasure of history is a monad quotient, and these form a lattice between the reversible cover and the irreversible base. The injective erasures compress the log without folding the tree; the identifying ones fold it, closing loops so that paths revisit states. Such an intermediate object is a quotient of the reduction graph’s fundamental group by a chosen set of loops — an intermediate cover — with the order-forgetting (Mazurkiewicz) erasure folding exactly the commuting concurrent steps.
Chapter 34 is this construction under a physical reading. The reversible envelope \(\GSLT^\dagger\) built there is \(\Hist\GSLT\) with the backward rules written down, and the reason writing them down costs nothing is Proposition 13.2: on a tree the inverse of a step is determined, not chosen. The lattice of erasures is what that chapter’s physics needs and does not have a name for — an intermediate cover is a coarse-graining, and which loops one is permitted to close is which histories one can afford to forget.
13.3 The ledger law
Underneath the covering-space picture sits an invariant needing no cohomology. Write \(\sigma\) for the fuel remaining and \(\kappa\) for the fuel recorded as spent. Then \[\sigma + \kappa = \sigma_0 ,\] initial fuel equals fuel remaining plus fuel recorded spent: a potential-plus-kinetic invariant of a cost-accounted, history-keeping run. Its one-way breakage under erasure is Landauer’s principle [49] — the history one may erase for free is exactly the redundant, state-recoverable part.
13.4 The duality, and a third column
The two constructions are ledgers of the same time axis, read in opposite directions. The next chapter adds a third of the same family, which is why the table has room for it.
| Cost \(\Cost\) | History \(\Hist\) | Weight \(\Wgt_{\Semi}\) | |
|---|---|---|---|
| adjoined structure | token stack | event word | table of rates |
| indexed by | signatures | events | formulae refining a rule |
| behavior along \(\longrightarrow\) | drains | accrues | is rewritten |
| records | what remains | what was spent | how fast, and how often |
| free object | fully funded run | universal cover | — |
| physical reading | bounded causality | recorded causality | rated causality |
| monad? | yes | yes | not claimed |
A GSLT gives causality. \(\Cost\) gives bounded causality. \(\Hist\) gives the ability to record bounded causality. \(\Wgt_{\Semi}\) gives a rate at which bounded causality proceeds, which is the difference between a transition system and something one can sample from. Running \(\Cost\) on an \(\Hist\)-equipped model gives the cost of making the recording, and the levels are worth keeping distinct rather than collapsing: the stacking \(\Cost\Hist\Cost\Hist\cdots\) is meaningful, and its fixed point is an object of interest we do not pursue here.
The last row of the table is the honest one. \(\Cost\) and \(\Hist\) come with free–forgetful resolutions and hence with multiplications; the weight construction is presented in Chapter 14 as an endofunctor only, and Remark 14.3 says what would have to be settled to say more. The graded where-clause of that chapter’s second half is not an endofunctor on the category of theories at all but a change to the term language of one theory, which is why it does not appear in the table: it is the object the endofunctor was approximating.
As in Remark 12.4, a sufficiently expressive base theory can encode the logging apparatus into itself, performing the record-keeping with its own computation. The same caveat applies: this is a different erasure from forgetting, and we note rather than develop it.