Chapter 17
What Goes Into a Logic
This chapter is where the constructions that feed the OSLF functor — Operational Semantics in Logical Form, the machinery that manufactures a modal logic out of a rewrite theory rather than bolting one on beside it — are gathered. At present it contains one of them, in full: the construction of space from term structure, which the rest of this book uses more than any other and which has until now been assumed rather than built. The remaining ingredients — the SOS presentation the functor consumes, the adjunction it factors through, and the sense in which its output is the internal language of the theory it came from — belong here too, and are not yet written. The reader should treat the chapter as load-bearing but unfinished, and should not conclude from its brevity that the OSLF construction is brief.
17.1 The agent needs a where
Everything so far has been a theory of state and of evolution. A grammar says which configurations are possible, an equational quotient says which of them are the same, and a collection of rewrites says how one becomes another. That is enough to have a time: Chapter 29 read time off paths through the synchronization tree, and Chapter 28 read reversible time off paths that carry their own history.
It is not yet enough to have a space. An agent working out its situation needs to know not only what is happening but where — where the event is, where its environment is relative to itself, whether two things that just happened happened near each other or far apart. And the agent cannot be handed a space, because there is nothing to hand it one. It has its theory of state and evolution and nothing else. Whatever space it has, it must read off what it already has.
The good news is that what it already has is not featureless. Terms have structure. They are trees, and once the equational quotient is imposed, graphs: constructors at the nodes, subterms in the argument positions. That structure is the only candidate for a notion of space available to an agent confined to its own theory, and it is also, as it happens, a good one. It is combinatorial, so it needs no external manifold or metric to make sense of. It carries adjacency for free: two argument positions of the same constructor are next to each other. It supports locality: a rewrite at one place leaves the surrounding structure alone. And it is the structure the agent’s hypotheses already speak about, so nothing has to be added to the hypothesis language to let the agent say where.
17.2 One-holed contexts, and the derivative of a type
Chapter 16 already introduced contexts: terms with a distinguished hole, written \(K[-]\), with \(K[P]\) the result of plugging \(P\) into it. There the interest was in minimal contexts, because minimal contexts are what make a bisimulation a congruence. Here the interest is in contexts as a family — in the type of all of them.
That type has a striking description, due in its modern form to Huet and to McBride [111, 112]. Huet observed that navigating a tree while retaining the ability to rebuild it requires carrying the surroundings along as a first-class object, and called the resulting data structure a zipper. McBride identified what the zipper is: the type of one-holed contexts over a type \(T\) is the formal derivative \(\partial T\), computed by exactly the rules one learns in a first calculus course, read type-theoretically. The derivative of a sum is the sum of the derivatives; the derivative of a product obeys the Leibniz rule; the derivative of a recursive type unfolds by the chain rule.
Let \(\terms(\GSLT)\) be the term type of a GSLT \(\GSLT\), presented as a polynomial functor over its signature. Its context type is the formal derivative \(\partial \terms(\GSLT)\), whose inhabitants are the one-holed contexts \(K[-]\) of Chapter 16.
The derivative is not an analogy here. It is the same calculation, and it is worth pausing on the fact that the rule which tells you the derivative of \(x^n\) is \(nx^{n-1}\) is, read as a statement about types, the observation that an \(n\)-tuple has exactly \(n\) places you can put a hole in and an \((n-1)\)-tuple left over when you do. This is developed at length elsewhere [113]; what is needed here is only the type and the plugging operation.
17.3 A context is a shape; it is not a place
It is tempting to stop here and call a context a location. The temptation should be resisted, and the reason is instructive.
Consider the context \(\lambda x.[-]\). Does it locate the subterm \(N\) inside \(\lambda x.(M\,N)\)? It does not, or rather it does not do so uniquely: the same context sits equally well around the subterm \(P\) inside \(\lambda x.(M\,(N\,P))\), and around indefinitely many others. A context tells you what the surroundings look like. It does not tell you which surroundings, of which term, you are in the middle of. It is a shape, and a shape is not a place.
What locates is the pair.
A splitting of a term \(s \in \terms(\GSLT)\) is a pair \((K, t) \in \partial\terms(\GSLT) \times \terms(\GSLT)\) with \(K[t] = s\). Write \(\Split(\GSLT) = \partial\terms(\GSLT) \times \terms(\GSLT)\) for the type of all splittings. The plug map \[\Plug : \Split(\GSLT) \longrightarrow \terms(\GSLT), \qquad (K,t) \mapsto K[t]\] sends a splitting to the term it reconstructs, forgetting where the cut was. A location in \(s\) is a point of the fibre \(\Plug^{-1}(s)\).
So a location is not a thing found inside a term. It is a way of cutting the term in two, and the location is the cut.
The pattern is one mathematics has used before, and it is worth naming because it makes the definition feel less like a technicality. Dedekind does not locate \(\sqrt{2}\) by exhibiting a rational. He locates it by partitioning \(\mathbb{Q}\) into two halves, with \(\sqrt{2}\) the gap between them. Conway’s surreal numbers make the move constitutive: every number is a pair \((L \mid R)\) of left and right sets, and is nothing but the gap they specify [56]. In each case neither half names the point; the partition does. The analogy is structural rather than identifying — a Dedekind cut splits a densely ordered set and a splitting splits a tree-shaped one, with a plug relation between the halves that the ordered case has no use for — but the shape of the idea is the same. A place is a way of dividing a whole, and the division is the place.
17.4 Fire: the events available now
Not every cut is interesting. Most of them are inert: nothing can happen there, because nothing at that cut matches the left-hand side of any rule. The interactive structure of Chapter 8 tells us which cuts are not inert.
Recall that in an interactive GSLT the base rewrites — those with no hypotheses above the line, the ground events of the theory — all share a distinguished family \(K\) of head constructors. In the lambda calculus that family is application; in the \(\pi\)- and rho calculi it is parallel composition. A splitting is where something can happen exactly when its subterm side exposes such a redex.
\(\Fire(\GSLT) \subseteq \Split(\GSLT)\) is the sub-bundle of splittings \((K,t)\) for which \(t\) matches the left-hand side of some base rewrite of \(\GSLT\), with \(K\) the context in which that rewrite is to fire. A point of \(\Fire(\GSLT)\) is an available event: an interaction that can happen at this cut, in this state, now.
\(\Fire\) is much smaller than \(\Split\). Events are sparse; at any given moment almost every way of cutting a state in two is a way of cutting it at a place where nothing is going on. Sparseness is not a defect of the construction but the content of it: it is what makes the difference between a state in which anything might happen and a state in which specific things might.
Two consequences follow immediately, and they are the reason to have bothered.
First, the fibre of \(\Fire\) over a state \(s\) — the set of available events at \(s\) — is the discrete analog of the tangent space at \(s\). It is the set of directions in which the state can move. A path through the synchronization tree, in which each step is the firing of a base rule at some available cut, is then the discrete analog of an integral curve of a vector field. Time, which Chapter 29 obtained from paths, is motion through this structure.
Second, the program/environment cut is no longer a metaphor. In an interactive GSLT with symmetric head constructors, we said that which side is the program and which the environment is a perspectival fact rather than a fact about the situation. We can now say what the perspective is: it is a splitting. The cut tells you where the program — the subterm the base rule consumes — meets the environment — the context in which the consuming happens. Location and interaction are the same notion viewed at different resolutions.
17.5 Space and time from one object
Put the two together.
Time is the path through the discrete tangent structure. Space is the structure of cuts the path passes through.
Both are read off the same object: the term structure of states, differentiated and then restricted to the events that are actually available. Neither is prior to the other and neither is imported. They share an origin, and the origin is the compression of causal structure into rule form that a GSLT already is.
This is a substantial departure from how physical theories are normally set up, and the departure is worth stating plainly because the rest of this book depends on it. In the standard picture, space is given — a manifold, a lattice, a Hilbert space — and the dynamics is then defined on that pre-given arena. Here there is no arena. The derivative of the term type produces one out of the theory of computation, and the events restrict it to the part of it that matters. The dynamics does not live in a space; it makes one.
17.6 What is still missing
Two things, and both are wanted before the OSLF construction can be given in full.
The first is a metric. Everything above is combinatorial. The cuts are there, adjacency is there, locality is there, but nothing yet says that two states which behave almost identically are near each other, and that is the notion of nearness a predicting agent actually needs. The stratified distance of Chapter 21 is one answer, built for a scientist with a budget; whether it is the answer that falls out of this construction, or merely one compatible with it, is open.
The second is the functor itself. What has been built here is the raw material: a type of locations, a sub-bundle of events, and a plug map relating them to states. OSLF consumes material of this kind and returns a modal logic whose formulae characterize behavior up to bisimulation. Chapter 16 gave the logic; it did not give the manufacture. Until the manufacture is written down, the reader is entitled to regard the logic as postulated, and several of the arguments that depend on it — including one in Chapter 68 that matters a great deal — as resting on a construction this book has described but not exhibited.
One thing can be said about the logic without waiting for its manufacture, and the next chapter says it. A predicate over names does not only describe; it delimits, and a delimited collection of names is a region. Regions are what the rest of this book counts in, owns, and pays to visit, and it costs very little to make them expressive enough to be worth having.