What a Language Presentation Is, and Why It Comes First

The rest of this book builds a mind out of computations, and then asks what such a mind can know, what physics it finds itself inside, and how anything of the kind could have got started on a planet. Every one of those arguments spends the same coin. This part mints it.

The coin is a way of writing down a language — not a program, not a machine, but a language — that is regular enough to be handed to a machine rather than to a human implementer. A grammar, a set of equations saying which terms are the same, and a set of rewrite rules saying how one term becomes another. That triple is a graph-structured lambda theory, and the claim of this part is that once you have one, an astonishing amount comes free: a notion of interaction, a meter that charges for it, a log that remembers it, a logic that describes it, and a type system that checks it.

6.1 Why this order

An earlier arrangement of this material put the physics first. It began with a rewrite theory, hung weights and costs on the rewrite steps, recovered least action and conservation, and only much later introduced anything that could be called an agent — at which point the agent arrived as a placeholder, a thing that has theories and can afford some number of experiments.

That order encodes a claim we no longer believe: that the world comes first and the knower is a late arrival in it. The difficulty is not philosophical delicacy. It is that under the earlier order the physics is presented as though it were the only one, and the learner as though it had been dropped into it. Both halves of that picture are wrong in the same way. A GSLT does not come with a physics; it comes with a space of possible physics, and which one you get depends on what further axioms you are willing to impose. A learner does not arrive in a world; it is made of the same material as the world and pays the same prices. Part Part IV makes the first point, and it can only make it after Part Part II has made the second.

So the order here is: machinery, then mind, then the physics the mind finds itself inside, then what the mind can do that a Turing machine cannot, then how such a thing could have arisen. This part is the machinery. It is deliberately the driest part of the book, and a reader who wants the argument rather than the apparatus may read Chapters 7, 8 and 9 for the three definitions, skim Chapter 11 for the shape of the cost construction, read Chapter 14 for what a metered language actually looks like, and go on to Part Part II, returning here when a construction is invoked that they want to see built.

6.2 The three definitions, in advance

The development proceeds by two strengthenings of a very thin starting notion, and it is worth saying now what each buys, because the discipline of adding structure only when a construction needs it makes the sequence harder to see from inside.

A GSLT

is any rewrite theory whatever: a signature, equations, rewrites. Nothing in it says the theory is about computation, or that anything interacts with anything. This is enough for the category of Chapter 10 and for the type generation of Chapter 19.

An interactive GSLT

names the site at which two things meet — application in the \(\lambda\)-calculus, parallel composition in rho — and distinguishes the base rule that fires there from the context rules that say when it may. This is what lets us speak of an agent and its environment without smuggling in a homunculus: the boundary is drawn by the rules, at runtime, and either side of an interaction may be the program.

A continued interactive GSLT

presents that site as a cut which can be metered: the interaction is factored so that there is a well-defined place to put a charge, and continuations become metered thunks. This is what makes Chapter 11 possible, and with it everything in this book that depends on a learner having a budget — which is to say everything in this book.

The examples matter as much as the definitions, including the ones that fail. A Turing machine is a GSLT and is not interactive; a \(\lambda\)-calculus is interactive with an asymmetric site; rho is interactive with a symmetric one. Chapter 8 is largely an argument about which is which and why the distinction is not a technicality.

6.3 Running example: the rho calculus

Throughout we use the rho calculus [1] as the running example, because it exhibits in compact form nearly every feature at issue: reflection, so that processes and names are mutually definable and a term can carry a quotation of another term; parallel composition, so that the interaction site is symmetric; and a single synchronization rule that will serve as the prototype for causal structure, for replication, and for the act of one computation eating another.

The grammar is \[\begin{align} P, Q &\;::=\; 0 \;\mid\; \mathtt{for}(y \leftarrow x)\,P \;\mid\; x!(Q) \;\mid\; P \mid Q \;\mid\; {*}x \\ x, y &\;::=\; @P \end{align}\] where \(y\) in \(\mathtt{for}(y \leftarrow x)\,P\) is bound. Structural equivalence \(\equiv\) is the smallest equivalence relation containing \(\alpha\)-equivalence and making \((P,\,|\,,0)\) a commutative monoid. The single reduction rule is \[\mathtt{for}(y \leftarrow x)\,P \;\mid\; x!(Q) \;\rewrite\; P\{@Q / y\}.\]

Three features of this calculus do disproportionate work later. Reflection means the quote of a process is a name, so a term can hold code it has not run — which is what makes the genetics of Chapter 23 possible, since crossover is an operation on quoted code. Names are the only locations there are, so a namespace is a region, and a logic of namespaces is a logic of places — which is what Chapter 21 needs when a specimen affords exactly one measurement and hypotheses must therefore be about kinds. And the comm rule is one definitional step from a crossover operator, which is the observation Part Part VI builds on.

6.4 Organization of this part

Chapter 7 gives the definition and argues for its two halves — why lambda theories rather than Lawvere theories, why the rewrites are adjoined rather than enriched. Chapters 8 and 9 give the two strengthenings, with the examples that separate them. Chapter 10 assembles the category, whose morphisms preserve bisimulation over context-labelled transitions. Chapters 11 and 12 give the two constructions on it that the rest of the book uses constantly: the cost monad, which meters a theory, and the history monad, which logs it. Chapter 14 exhibits the cost construction concretely, as a metered rho calculus in which token stacks are first-class terms and acceptance is a linear proof rather than a run to completion. Chapter 15 asks the question that metering raises and does not answer — when do many kinds of resource admit a single number? — and finds that the condition is exactly the absence of arbitrage. Chapters 16 and 17 turn to the logic: the labelled transition system a theory induces, the context-decorated modal logic over it, and an accounting of what still has to be supplied before that logic can be said to have been manufactured rather than postulated. Chapter 19 closes the part with the construction that does the manufacturing for type systems: OSLF and the Hypercube, which read a theory’s own rewrite rules and return a family of type systems for it.