Undo/redo. Cursor position in a text editor. The call stack. These are all zippers — Huet's 1997 observation that a data structure can be decomposed into a hole (the current focus) and two complementary contexts: what came before, what comes after. Navigation is moving the hole.
We've been building something that looks like a zipper for the last several posts without calling it one. The tropical semiring accumulates past firings into a compressed summary. The predicate layer in every model we've built — guards, win detection, turn enforcement — constrains what fires next, given the current marking. The marking itself sits between them: the output of accumulation, the input to constraint.
That's a zipper. The marking is the hole. And the hole is not just a value — it is the universe relative to which past and future are both defined.
There are two established ways to handle time in a type system, and both miss something.
Schultz and Spivak's temporal type theory treats time as a parameter — an interval you index over. Rich and compositional, but the current moment has no special status. It's just a point on the coordinate.
Prior's tense logic treats past and future as modalities — operators that shift perspective relative to an implicit now. Expressive, but the boundary between past and future is a semantic convention, not a structural fact.
Both smuggle the present in through the side door.
A Petri net doesn't. In a DDM simulation, on every step you read the marking, check guards, fire a transition, update the marking. The marking is not derived from anything. It is not a point on a timeline. It is the thing the computation is about, locally, right now. Change the marking and you are in a different universe — different history is relevant, different transitions are enabled.
The marking is the present moment, and the present moment is a universe. The zipper makes this structural.
The left context is closed. Every transition that has fired contributes to it, but we don't store the trace — we summarize it. The tropical semiring (max-plus algebra) accumulates firing history as a matrix of longest paths. This is memory in the precise algebraic sense: a lossy compression that preserves exactly what the future needs to know. Fast-forward is matrix multiplication. Past firings are irreversible, and the tropical core is the proof.
The tropical semiring is not chosen for convenience. Simulate a Petri net iteratively and the past has been tropical all along — max-plus accumulation is what the left context does. We documented this in Tropical Petri Nets without using the zipper framing, but the structure was already there.
The right context is open. Guards constrain what can fire next, given the current marking. The future is not stored — it is computed fresh from the hole on every step. When the marking changes, the right context recomputes. This is the predicate layer we build in every model: win detection, turn enforcement, balance checks.
The hole — the marking — is the tense boundary. It is simultaneously the output of tropical accumulation and the argument to the predicate layer. It is where the two universes meet.
| Left Context | Hole | Right Context | |
|---|---|---|---|
| Structure | Tropical core | Marking | Predicate layer |
| Tense | Past | Present | Future |
| Operation | Accumulate | Focus | Constrain |
| Property | Closed, irreversible | Boundary | Open, recomputed |
The standard categorical treatment of Petri nets maps them into a free symmetric monoidal category. Tokens become objects. Firing sequences become morphisms. Composition is well-defined.
The hole disappears.
In the SMC encoding there is no privileged present. The current marking is smeared across the morphism structure — just another configuration, related to others by transition morphisms. Everything is homogeneous. The zipper has been flattened into a path.
This is the right encoding for process structure — it's a theorem about what compositions are valid. But it was never a foundation for computation. Every serious computational use of Petri nets — workflow engines, protocol stacks, ZK circuits — has to bolt mutable execution state onto the immutable categorical skeleton.
The zipper framing gives the diagnosis: you cannot focus without a hole, and the SMC encoding has no hole.
The tic-tac-toe model is small enough to see completely and structured enough to show the point. Every layer of the net maps to a layer of the zipper — not as analogy but as a specific partition of places.
Nine places, P00 through P22. Each holds a token if the cell is empty. One more place — Next — holds the turn token. That's the complete present-tense state of the game. Every other layer is defined relative to this marking.
X00 is enabled if and only if P00 has a token (cell empty) and Next is unmarked (X's turn). Same logic for all eighteen move transitions. This is the predicate layer — computed fresh from the hole, never stored. When the marking changes, the right context recomputes.
Win detection guards sit here too, typed against the current state of the history layer.
Every move transition does two things: consumes the token from the board place (P00 goes empty) and deposits a token into a history place (_X00 gets marked). History places are write-once — a token arrives and never leaves.
Above the history places sit the pattern collectors we built in the original post. X_has_top_row fires when _X00, _X01, and _X02 are all marked. Three tokens in, one structural token out. This is tropical composition — the pattern collector summarizes moves into a verdict without replaying them.
The terminal places win_x and win_o are the end of the left context. Once marked, the right context collapses. No transitions are enabled. The zipper stops.
X plays center. X11 fires.
P11 loses its token — the hole updates_X11 gains a token — the left context growsNext gains a token — turn passes to OX11 disabled, O transitions checked against new marking_X11 has one more input satisfiedOne step to the right. The past absorbed a firing. The future recomputed against the new present. This is all that ever happens.
| Layer | Places | Role |
|---|---|---|
| Left context | _X00–_X22, _O00–_O22, pattern collectors, win_x, win_o |
Accumulate, summarize, absorb |
| Hole | P00–P22, Next |
Current board, current turn |
| Right context | Transitions X00–X22, O00–O22 + guards |
Recompute from marking |
The earned compression post already documented this split as the core-observer decomposition. The zipper framing adds the temporal interpretation: core places accumulate (past), the marking is the boundary (present), and the observer predicates constrain (future).
Zero-knowledge proofs are inherently past-tense. A ZK proof witnesses that a valid execution occurred — it proves membership in the left context. The prover shows that the tropical core accumulated correctly. The verifier checks the summary without replaying the trace.
We built this in ZK Petri Nets, ZK Tic-Tac-Toe, and Bitwrap. The structure maps directly:
Blockchain engineers already build this way. Proof and execution are different things. Past and future are structurally asymmetric. The current state is the only thing connecting them. The zipper is the formal account of what they already know operationally.
Three traditions, one gap, one structure.
| Schultz-Spivak | Prior | Zipper | |
|---|---|---|---|
| Time as | Parameter | Modality | Universe |
| Present | Point on index | Implicit | The hole |
| Past | Interval endpoint | □ operator | Tropical context |
| Future | Interval endpoint | ◇ operator | Predicate context |
| Boundary | Derived | Conventional | The type |
The zipper doesn't add time to a type system. It recognizes that execution state already has this shape — the present is a universe, the past is tropical, the future is predicate — and names the structure.
The tic-tac-toe model already had all three layers. The tropical analysis already identified the left context's algebra. The core-observer split already found the boundary. This post labels the places.
The past is tropical. The future is predicate. The present is where they meet — and the present is not a point on a timeline. It is the universe that makes the timeline legible.
Related: Tropical Petri Nets · The Incidence Reduction · Earned Compression · Symmetric Monoidal Categories