Chapter 32
Extended Modal Operators
The decoration is, at present, external data attached to the rules. We now show that it can be internalized into the logic itself by extending the modal operators to carry the dynamical state of a transition.
Because Chapter 30 replaced the weight map and the cost map by a single semiring-valued decoration, the extended operator is correspondingly simpler than the version this chapter previously carried: it holds one value, not two. Where both an amplitude and a charge are wanted at once, one takes \(\Semi\) to be a product semiring — say \(\CC \times (\Real\cup\{\infty\})^k\) — and the two coordinates ride together. Nothing about the logic changes when they do.
The formulae of extended HML are generated by adding to Definition 16.2 the operator \[\langle K,\, \dec,\, \dec^{\dagger},\, \vect{A} \rangle\,\phi\] where \(K\) is a minimal context as before, \(\dec \in R\) is the forward decoration of the transition, \(\dec^{\dagger} \in R\) its reversal, and \(\vect{A}\) the account available at the surface on which the step draws. The satisfaction clause is \[\langle P, \trace, \vect{A} \rangle \;\sat\; \langle K, \dec, \dec^{\dagger}, \vect{A}_0 \rangle\,\phi\] just when:
\(K[P]\) evolves in one step via some rule \(r\) to \(P'\), with redex \(u\);
the decoration assigns \(\dec_r(u) = \dec\), where \(\dec_r(u)\) is evaluated at the unique witness \(\phi_r(u)\) supplied by the partition discipline (Proposition 13.1);
the reversal satisfies \(\dec^{\dagger} = \overline{\dec}\) in the complex coordinate and \(\dec^{\dagger} = \dec\) in the tropical coordinates — a debit reversed is a credit of the same size; see Remark 32.1 on the status of the first of these;
\(\vect{A}_0 = \vect{A}\), the account recorded in the formula being the one the step actually draws on;
the step is affordable in the tropical coordinates, and the drawer holds the capability to the account (Remark 31.8);
\(\langle P', \trace', \vect{A} - \dec \rangle \sat \phi\), the subtraction taken in the tropical coordinates only.
Clause (iii) is stated here in the form the earlier presentation used, and in the complex coordinate it should be read as a stipulation rather than as something the construction supplies. Chapter 33 builds the complex instance as a dissipative generator, in which the reverse of a jump is the adjoint of its jump operator and not a conjugated decoration attached to a reversed step, and the forward-versus-backward asymmetry lives in the dissipator rather than in a relation between two numbers. The two readings agree on the tropical coordinates, where reversal is simply sign, and they have not been reconciled on the complex one. A reader tracking the complex apparatus through this book should treat \(\dec^{\dagger} = \overline{\dec}\) as notation carried forward, and Definition 13.11 as what is actually built.
32.1 Internalization of the Decoration
In extended HML the decoration is recoverable from the logic: \(\dec_r(\phi) = \dec\) where \(\phi = \langle K, \dec, \dec^{\dagger}, \vect{A}\rangle\,\psi\). The decorated rewrite rules and the extended modal logic are two presentations of the same structure.
This is a small instance of a pattern that recurs throughout this book, and it is worth naming here because it will be doing heavy work later. Structure attached to a calculus from outside can often be pushed back inside it, and the two erasures — forgetting the decoration and internalising it — are genuinely different operations with different costs [108]. Forgetting loses information. Internalising loses nothing but has to be paid for in expressiveness of the host. When the Pledge insisted that rods and clocks belong inside the model rather than outside it, this is the operation it was asking for.
32.2 Factorization: State vs. Rule
The parameters of the extended operator decompose into two classes:
| State-dependent | Rule-dependent |
|---|---|
| \(K\) (from MSL applied to the current term) | \(\dec\) (from the decoration on the rule) |
| \(\vect{A}\) (the account at the surface) | \(\dec^{\dagger}\) (its reversal) |
This is the natural decomposition of the extended logic into observables — what can be measured now — and dynamics — how the system evolves. Note that with a dynamic decoration (Definition 30.4) the boundary moves: the table travels with the state, so part of what was rule-dependent becomes state-dependent, and the logic sees the difference. That is the same relocation Theorem 13.1 performs on the state space, seen from inside the logic instead of from outside the chain.
32.3 Located accounts
The account \(\vect{A}\) was previously described as being either global — one budget for the whole term — or local, with each parallel component carrying its own, a communication then debiting “from a shared pool or by negotiated transfer, depending on the resource semantics chosen.” That framing is the source of the defect recorded in Remark 31.8, and it should be retired. The global/local distinction is about where the arithmetic happens; the distinction that matters is about who is entitled to do it.
In the rho calculus the two questions have the same answer, because a location is a name. An account is a message on a channel; the right to draw on it is the right to receive on that channel; and since fresh channels are unforgeable, entitlement is possession rather than adjacency. The extended operator therefore records the account at a surface, and clause (v) of Definition 32.1 asks two independent questions — is there enough, and may this drawer draw — where the earlier presentation asked only the first.
Two consequences are worth flagging. Conservation laws become genuinely local, since each located account is conserved separately and transfers between them are visible as communications rather than as bookkeeping. And the spatial and temporal structures cease to be independent coordinates, for the reason given in Remark 31.9: a draw now requires both proximity and availability. The logic is the natural place to observe this, since a modality that records a located account is recording a fact about space and a fact about time in a single operator.