The theory behind versioning

You have a workflow that has been running for three days. It has charged two customers and is waiting on a third payment. Now you need to ship a new version of its code: the new code renames a command, changes a payload from a bare number to a record, and adds a risk check the old runs never recorded. What happens to the run that is already in flight?

Most durable execution systems answer that question with conventions and careful code review. Hopskip answers it with mathematics, and this page explains that mathematics from the ground up. No background is assumed. Every idea arrives in the same order: the concrete problem, a picture, plain words, and only then the notation. The notation is worth the space it takes, because it is what turns “we think this migration is safe” into a check a machine can run before anything is touched. But you can treat every formula as decoration and still follow the page: each one is restated in words immediately after it appears, and the footnotes carry the proofs for readers who want them.

Two practical notes. This page is the one place in the documentation where the formal vocabulary appears; everywhere else the same ideas go by their everyday names (event graph, mapping, backfill, replay check), and the dictionary at the end maps between the two. And nothing here is required to operate the system. The versioning concepts page describes it as an operator meets it, and the formal account in the repository is the authority where the two disagree.

The running example

One example runs through the whole page. A workflow type billing moves from version 3 to version 4, with three changes:

the command type PaymentCmd is renamed to ChargeCmd,
its payload changes from an integer amount to a record {amount, currency},
a new event type RiskCheck is added, computed for old runs from data they already recorded.

An execution started under version 3 is mid-flight when version 4 registers: it has recorded a start event, two charge commands, and their results, and it is waiting on a third.

The migration problem in one picture: version 4 registers while this execution is still running. Version 4 does not know the name PaymentCmd, expects a different payload, and requires one RiskCheck per run. The recorded events have to be translated into that world without losing what they say.

The whole page answers one question: what does it mean, exactly, to move this execution across that change, and how can a machine check the answer before anything is touched.

What is actually recorded

Start from the data. A workflow version does not record arbitrary bytes. It records events with structure: an auth result exists because it answers a specific charge command, a charge command exists because a specific start event issued it, and those “because” links are as much a part of the data as the payloads. A version publishes that structure as its event schema.

A schema has three parts:

Objects: the event types. Start, PaymentCmd, AuthResult, RiskCheck.
Arrows: the derivations between them. An arrow $answers : AuthResult \to PaymentCmd$ says every auth result determines which charge it answers. (Read $f : A \to B$ as “f is an arrow from A to B”.)
Path equalities: declared facts that two different routes compute the same thing, such as “the total derived per order equals the total derived per line, summed”.

Arrows compose. If $f : A \to B$ and $g : B \to C$ , there is an arrow $g \circ f : A \to C$ , read “g after f”. That composite has to behave like the two-step route it names, so a schema requires two laws:

{id}_{B} \circ f = f = f \circ {id}_{A} h \circ (g \circ f) = (h \circ g) \circ f

Read these as: every type has a do-nothing arrow $id$ that composes away, and chaining arrows is associative, so a three-step route means the same thing however you parenthesize it. Objects, composable arrows, and these two laws are the definition of a category. That is all a category is: a typed graph with a composition rule that behaves. When the schema also declares path equalities, the formal name is a finitely presented category: generators (the types and direct derivations) plus relations (the equalities).

Here are the schemas of the two versions in the running example, and the patch’s mapping drawn between them:

The two schemas as categories. Boxes are objects (event types), solid arrows are morphisms (derivations). The dashed accent arrows are the patch's mapping P: each old type lands on a new type, and each old derivation lands on a derivation in D with matching endpoints. RiskCheck has no preimage: the old world never recorded one.

Why categories rather than plain graphs? Because the mapping between versions has to respect composition. Suppose RiskCheck followed from Start through an intermediate type. After the mapping renames and retypes everything, the translated RiskCheck must still follow from the translated Start through the translated intermediate. A map of graphs can send every node and every edge somewhere sensible and still break the chained routes. A structure-preserving map of categories cannot:

P (g \circ f) = P (g) \circ P (f) P ({id}_{A}) = {id}_{P (A)}

A map $P$ satisfying these two equations is a functor. Read them as: the mapping sends two-step routes to two-step routes and do-nothing arrows to do-nothing arrows. That requirement is the entire content of the translation well-formedness check that runs at patch registration, and the check is finite because it only has to look at the generators: verify each arrow lands on a route with matching endpoints, and each declared equality still holds. Composition takes care of the rest.

Equality a machine can decide

Declaring path equalities creates a question the system must answer constantly: are these two derivation paths equal? In a general finitely presented category this question is undecidable. It contains the word problem for finitely presented monoids, which Post proved unsolvable in 1947,¹ and a versioning system that had to answer it in full could check nothing. This model refuses to leave any check undecidable, so it restricts which equalities a schema may declare.

The restriction: every path equality must orient into a rewrite rule that makes paths smaller in a fixed ordering, shortlex (fewer steps first, ties broken alphabetically). A rule like

perOrder ⟶ sum \circ perLine

says the left side rewrites to the right. The registration checker verifies the decrease for every rule, one by one. If every rule decreases and every place where two rules could compete joins again,² the rules form a terminating, confluent rewriting system: repeatedly applying them always stops, and always stops at the same answer regardless of order. Write $\hat{p}$ for the normal form of a path $p$ , the result of rewriting until no rule applies. Then the undecidable question collapses to a string comparison:

p = q ⟺ \hat{p} = \hat{q}

Both halves are machine-checked. Termination is proven with an explicit fuel bound: a path over $k$ letters embeds into the natural numbers in a way that strictly decreases with every rule, so normalization finishes within a bound computed from the path. Confluence follows from the finite overlap check plus Newman’s lemma.³ A schema whose equalities do not orient this way is rejected at registration. This is the same restriction categorical database systems (CQL) adopted, for the same reason.

One execution, one small database

Schemas describe shape; now the data itself. One recorded execution is, to the model, structured data shaped exactly like the schema:

to each event type $A$ , a finite set $x (A)$ of its recorded occurrences;
to each derivation $f : A \to B$ , a function $x (f) : x (A) \to x (B)$ saying which occurrence of $B$ each occurrence of $A$ was derived from.

The assignment has to respect the schema’s composition and equalities:

x (g \circ f) = x (g) \circ x (f) p = q ⟹ x (p) = x (q)

Read as: the two-step derivation function is the composite of the one-step ones, and paths the schema declares equal induce the same function on the data. An assignment satisfying these equations is a functor $x : 𝐂 \to 𝐒 𝐞 𝐭$ , also called a copresheaf on $𝐂$ ; this model calls it a history. The useful reading is the mundane one: a history is a small database that conforms to the schema, one database per execution. Event types are its tables, derivations are its foreign keys, and path equalities are its integrity constraints.

The running example as a history x on C. Each table holds the recorded occurrences of one event type; each arrow is a derivation function (r1 answers c1, both commands were issued by s1). The instance satisfies the schema's path equalities the way a database satisfies its constraints.

Finiteness matters. Because each table is finite, every question the model asks about a history is a computation over finite data, so per-execution migration checking is possible at all: the checks run over one execution’s tables, not over the schema in the abstract.

Patches: translating the schema

A patch from version 3 to version 4 carries a mapping: what each old event type becomes, and what each old derivation becomes. Formally the mapping is a functor $P : 𝐂 \to 𝐃$ from the old schema category to the new one. Each old type lands on a new type ( $PaymentCmd \mapsto ChargeCmd$ ), each old derivation lands on a route in the new schema with matching endpoints, and every declared equality in the old schema must still hold after translation:

p = q in 𝐂 ⟹ P (p) = P (q) in 𝐃

Read as: the translation is a dictionary that also translates grammar, so facts derivable before remain derivable after. A dictionary that mapped words but broke sentences would move data without moving meaning, and the two functor laws plus this equality check are what forbid that. The check is finite: the registration checker verifies it on the generators only.

Old types with no image under $P$ are dropped. New types outside the image, RiskCheck in the example, must be classified explicitly as placeholder or backfilled; an unclassified new type is a registration error.

The plain form gives every old type exactly one new type. Some patches need less: one old type may map to several new ones, or to none. The planned extension replaces the function with a translation table (formally a profunctor), where each row relates an old type to zero or more new types. Tables compose by a quotienting operation called a coend, which is what makes multi-hop migration (version 3 straight to version 5, skipping the intermediate deploy) a single composed table.⁴ The plain functor form embeds into this one without breaking stored patch manifests.

Carry-forward: the migration that invents the least

Given the mapping $P$ and a history $x$ on the old schema, migration has to decide what history to record on the new schema. Many answers are possible: copy the data and invent nothing, copy it and fabricate plausible-looking values, copy it and delete what does not fit. The model picks a specific one and can call it canonical rather than heuristic, and that is the central fact of the data layer.

The answer is the left Kan extension of $x$ along $P$ , written $Σ_{P} x$ . In words: copy every recorded occurrence across through $P$ , then wherever the new schema demands something the old data cannot supply, fill the position with a fresh placeholder value, and invent nothing else. For the running example: both charge commands and both results copy across under their new names, and the new schema’s demand for one RiskCheck per run gets a placeholder, because the old history recorded nothing of the kind.

Carry-forward of the running example. Primed rows are the copied occurrences under their new types. The one invented element is p1: the free placeholder the new schema's total edge riskOf forces into existence, because the old history recorded no RiskCheck. A backfill later replaces it, or the patch declares it stays blank for old runs.

What makes this “the” answer rather than “an” answer is a uniqueness property. Let $Δ_{P}$ be the operation that re-tags new-version data as old-version data (no computation, just relabeling), and write $hom (x, y)$ for all structure-respecting maps from $x$ to $y$ . Then for any other migration candidate $y$ :

hom (Σ_{P} x, y) ≅ hom (x, Δ_{P} y) naturally in y

Read as: any other way $y$ of putting the old data into the new schema receives exactly one comparison map from $Σ_{P} x$ . Carry-forward is the least migration consistent with the mapping: it changes nothing you did not ask for, and every other reasonable migration factors through it uniquely. That uniqueness is why the model can call copy-forward-with-placeholders the canonical migration instead of one heuristic among several.

The algorithm that computes $Σ_{P} x$ is the chase, borrowed from database theory: find an unsatisfied demand of the new schema, add the forced elements or merge the forced duplicates, repeat until no demands remain. Two facts about this loop are proven, not assumed:

It terminates, with an explicit bound. The proof supplies a size measure $Φ$ : the total weight of the instance’s outstanding demands, each weighted by what discharging it will eventually cause. Every fill step strictly decreases $Φ$ , and $Φ$ is a natural number, so the loop finishes within $Φ (I_{0})$ steps.⁵
The bound requires acyclicity, and that requirement is sharp. The proof assumes the schema’s total derivation edges form no cycle. If they do, the loop provably can fail to stop: a cycle of total edges lets each pass force new elements forever, and the mechanization proves the non-saturation on such a schema as a control case. In the engine, a step budget proportional to history size turns any schema that violates the condition into a registration-time error instead of a hung migration. Where the total edges are acyclic the budget is a backstop, never the mechanism.

Backfills: placeholders that earn their values

Free migration is honest but lazy. A placeholder says: the new schema wants a RiskCheck here and the old data does not have one. A backfill replaces the placeholder with a value computed from the old history: in the example, a function over the recorded start event and charge commands that produces the risk assessment version 4 would have recorded.

There is a second canonical migration in which every demanded value is actually produced, written $Π_{P}$ . Together with $Δ_{P}$ from the last section, the three form a chain:

Σ_{P} ⊣ Δ_{P} ⊣ Π_{P}

The symbol $⊣$ is read “is left adjoint to”.⁶ In words: $Σ_{P}$ gives the least migration consistent with the mapping, $Δ_{P}$ just re-tags, and $Π_{P}$ gives the most demanding one. A backfill is a step from the first toward the second, taken on purpose: for each new type, the patch either supplies a total function over the old history or declines with a stated reason, and the declined runs are reported, never guessed into.

The middle operation is the one that keeps old readers working during a rolling deploy: $Δ_{P}$ re-tags new-version data so an old reader sees the migrated history through old eyes. This is what the “view as previous version” operation does. And the comparison that matters for rollback is the unit of the first adjunction, the canonical map

η_{x} : x ⟶ Δ_{P} (Σ_{P} x)

Read as: the old history, compared against its own shadow after migrating forward and re-tagging as old. Whether rollback is exact is a question about this one map.

Rollback exactness

Rollback through a patch is carry-forward followed by view-as-old: migrate to version 4, then look at the result through version 3’s schema. It is exact precisely when that round trip loses nothing:

Δ_{P} (Σ_{P} x) ≅ x

Read as: migrating forward and viewing back returns the original history, nothing blurred and nothing lost. Formally, the unit $η_{x}$ is invertible on this execution. Losslessness is not automatic, and the engine tracks its two conditions separately, per execution:

R1, the image condition. Every event appended after migration has a preimage type under the mapping and a payload determined through the mapped derivations. The first event without one closes the window.
R2, the injectivity condition. The mapping sends this execution’s occurrences one-to-one: no two old occurrences land on one new occurrence, and nothing is deleted without archival. A patch that merges events closes the window at migration time, before any new event is recorded.

The pair of forward and backward migrations obeying the round-trip laws is a delta lens, the standard formal object for a bidirectional synchronization that does not lose data.⁷ A rollback that has become inexact is a lens whose laws no longer hold at that execution, and the window records the first event that broke them. That event is exactly the “rollback expired at event N” the product surfaces.

Behavior: what the code does

So far everything has been about data: what is recorded and how it translates. The other half of migration is the code.

Model a workflow version as a step function. At any moment a running workflow is waiting: it has issued commands whose results have not arrived, and it listens on some signal channels. Call that collection of in-flight business the pending context $Γ$ . Each time the environment delivers an event $e$ (a result, a signal, a timer), the code reacts:

step (Γ, e) = Done | Wait (B, Γ^{'})

Read as: given the current pending context and a delivered event, the version either completes, or issues a batch $B$ of new commands and keeps waiting with an updated context $Γ^{'}$ . A function of this shape, state in and observation-plus-next-state out, is called a coalgebra. The environment chooses which event arrives next, so a version is nondeterministic from the outside and deterministic from the inside: given the delivered event, the reaction is fixed. That inside determinism is what the sandbox enforces, and it is what makes replay a meaningful check at all.

Unfold the step function along every possible delivery order and you get the behavior tree of the version: the tree of all its possible futures, one path per interleaving. The model takes no quotient by interleaving, because code may lawfully branch on arrival order. Formally the tree is the image of the step function in the final coalgebra of the behavior functor: the most general object defined by nothing but “what can happen next”.⁸

The step function unrolled along every delivery order. The accent path is the recorded history h: issue c3, then c3 completes. Everything below the node the path ends at is the residual, the Brzozowski derivative of the behavior by h: the futures still open to this execution. Migration must hand the execution to new code whose tree agrees on the recorded path.

Two versions are bisimilar when no experiment can tell them apart:

b_{1} \sim b_{2} ⟺ on every input they react identically, and their continuations satisfy \sim

Read as: every future of one is a future of the other, forever. Migration needs the one-sided version: a simulation from the old behavior to the new, meaning the new version can imitate every step the recorded past took. The patch stores that witness as its replay plan, represented not as a function on all paths but as the composite action of the patch’s verbs applied pointwise along the history. In words: the replay plan is a proof-shaped object showing that every step the old run took has a matching step the new code can take.

The last piece ties behavior to recorded data. Given a recorded history $h$ , what remains to do is the residual of the behavior at $h$ : the subtree that starts where the recorded past ends. It is written $\partial_{h} b$ and called the Brzozowski derivative of $b$ , after the construction that computes what remains of a regular expression after consuming a prefix:

\partial_{e} (b) = the subtree after e arrives \partial_{h \cdot e} (b) = \partial_{e} (\partial_{h} (b))

The migration soundness theorem then says that a migrated execution’s future is exactly the derivative of the new behavior at the translated history:

future (migrated run) = \partial_{P (h)} (b_{new})

The past is accounted for, and the future is the new code’s.

The replay check, as one picture

The per-execution check compares two routes at every step of the recorded history. Route one: replay the old code on the recorded past, then translate the reaction it issues. Route two: translate the recorded past first, then replay the new code on it. The check demands the two routes agree at every position, comparing issued batches as id-indexed maps over decoded values:

translate \circ {replay}_{old} = {replay}_{new} \circ translate

The replay check, one square per history position. Commutation says translating-then-replaying equals replaying-then-translating. A failed square has a location and a batch diff: which command ids are missing, extra, or changed.

Equations of this shape are called naturality squares, and the check verifies this one position by position, reporting the first square that fails to commute together with the offending batch diff. There is no generic “nondeterminism detected” outcome anywhere in the system, because divergence is always a square that fails, and a square that fails has a location.

Codecs: bytes that read back

Payloads cross the migration boundary as decoded values, not bytes, and the decoding itself needs a guarantee. A payload codec (JSON, a binary encoding) is a prism in the optics sense: a partial, invertible reference into bytes, a pair of functions $enc : T \to Bytes$ and $dec : Bytes \to Either DecodeError T$ obeying one law:

dec (enc (v)) = Right (v)

Read as: what it writes, it reads back. Encoding then decoding is the identity on every value the codec accepts, and decoding failure is information, not corruption. The law is not statically checkable in general, so it is property-tested at registration on generated values rather than proven. That is one of the listed assumptions in the trusted base below.

Format versus meaning

Every patch factors uniquely, up to isomorphism, into a vertical part that only re-encodes (codec reassignments, no semantic change) and a horizontal part that changes meaning:

p = v \circ h = h^{'} \circ v^{'}

Read as: format changes and meaning changes split the way “renaming a file” and “editing a file” split, and doing them in either order converges to the same result. The convergence is the interchange theorem, and it is proven. This is why a format-only patch needs no replay check and never interferes with a later meaning change, and why lazy and eager re-encoding are observationally equivalent: the envelope tag, not the timing, decides how bytes are read.

Deploy order across services

When two services exchange events, a version change on one side changes what the pair can say to each other mid-rollout. The model arranges versions on a grid: deployed schemas as objects, contracts as horizontal arrows between service-version pairs, patches as vertical arrows upgrading a service. A mid-rollout state, one service upgraded and its counterparty not, is a square in this grid. Two kinds of arrows plus compatible squares is a double category.

One upgrade square. Horizontal arrows are contracts between deployed schemas; vertical arrows are patches. The two dashed paths are the rollout routes through the square, each passing through one mixed-version corner: orders-first goes through (orders@2, pay@1), payments-first through (orders@1, pay@2). Each corner needs a route: evidence that the mixed pair can still communicate. Which routes exist decides the deploy order.

“Can these two still talk mid-rollout” is the existence of a square filler: a translation occupying the square that makes both routes around it agree. When either order works, the two canonical fillers are called the companion and the conjoint of the patch. The plan safety theorem states:

a deployment plan is valid ⟺ every square it reaches has a filler

Read as: the checker’s four verdicts (either order, A first, B first, cut over together) are a complete case analysis of filler availability, so validating a rollout order is a typing question, not a search. The equivalence, both directions, is proven, and it covers rollback steps as well as upgrade steps.

What is proven, and what is assumed

The architecture is translation validation, the stance from verified compilers: prove the validator correct once, then validate each artifact mechanically.⁹ The proof surface is fixed: the registration checker, the verb algebra’s obligations, the rollback tracking, the deploy-order calculus, and the engine’s commit protocol. Individual patches are never proven; they are checked by machinery that is.

The theorems establish one invariant, the replay invariant:

replay (h) = h after every operation

Deliver an event, crash and resume, migrate, roll back, re-encode: replaying the recorded history afterwards reproduces it exactly, pending context included. Ten theorems say each operation preserves it, that rollback through an open window is the identity, that no command is resolved twice under any interleaving, that certified patches migrate everything the verb algebra promises, that format-only patches are inert, and that a validated plan never strands a pair without a filler. The behavior layer is mechanized over interaction trees with parameterized coinduction; the data layer, finitary by construction, is mechanized, extracted, and differentially tested against the production kernel in CI, so the two cannot drift.

No honest proof is unconditional. The trusted base is exhaustive and short:

storage provides the atomic write the commit protocol uses, bridged by a model-checked refinement of the implemented protocol against its atomic specification, and exercised by fault injection on a real system;
codec round-trip laws hold beyond the sampled generator, property-tested, not proven;
workflow code is deterministic given delivered events, enforced by the sandbox, not by convention;
the production kernel agrees with the extracted proofs’ kernel, an empirical fact maintained by differential testing.

Everything else is a theorem. A soundness claim conditioned on an enumerated base like this is the strongest form of “proven correct” there is; the model says so explicitly and claims nothing more.

The dictionary

The surface vocabulary used everywhere else, and the formal object each names:

Surface term	Formal object
event graph	finitely presented category: event types as objects, derivations as arrows, declared path equalities
history	finite instance: a functor $x : 𝐂 \to 𝐒 𝐞 𝐭$ (a copresheaf), one per execution
mapping (in a patch)	functor $P$ between schema categories; the relation-style extension is a profunctor, composed by coends
carry data forward	left Kan extension $Σ_{P} x$ along the mapping, computed by the chase, terminating with the explicit bound
placeholder	the free element $Σ_{P}$ introduces where the target schema demands structure the source cannot supply
backfill	refinement of the free migration toward the right adjoint $Π_{P}$ : every demanded value produced
view as previous version	the pullback $Δ_{P}$ , middle of the adjoint triple $Σ_{P} ⊣ Δ_{P} ⊣ Π_{P}$
rollback available	invertibility of the unit $η_{x}$ on this instance; the R1/R2 tracking is a delta-lens discipline
behavior of a version	coalgebra of a dependent polynomial functor over pending contexts; its behavior tree is the image in the final coalgebra
replay plan	simulation of the old behavior by the new, stored as the composite action of the patch’s verbs
replay check	commutation of the naturality square between old-code replay and new-code replay on the translated history
what remains after a history	the Brzozowski derivative $\partial_{h} b$ of the behavior tree
format change vs meaning change	the vertical/horizontal factorization: patches fiber over semantic schemas, and the two never interfere
codec	a prism onto bytes; the round-trip law is the prism law, property-tested at registration
deploy-order check	square fillers in a double category whose objects are deployed schemas, horizontal arrows are contracts, vertical arrows are patches; the two canonical routes are companion and conjoint translations
the checker itself	translation validation: the validator is proven correct once, each patch validated mechanically at registration and migration time

Reading list

The load-bearing references, in reading order, each with what to read it for:

Spivak, Functorial data migration (2012). The Δ/Σ/Π triple for data migration; the shape of the whole data layer.
Fagin, Kolaitis, Miller, Popa, Data exchange (2005). The chase as used here, in schema-mapping form.
Schultz, Spivak, Vasilakopoulou, Wisnesky, Algebraic databases (2017). The CQL system, whose decidability restrictions this model shares.
Rutten, Universal coalgebra (2000). Step functions, final coalgebras, bisimulation: the vocabulary of the behavior layer.
Milner, Communication and Concurrency (1989). Simulation as the witness of “can imitate”.
Brzozowski, Derivatives of regular expressions (1964). The derivative, read here as “remaining futures”.
Xia, Zakowski, He, Hur, Malecha, Pierce, Zdancewic, Interaction trees (2020). The coinductive representation the mechanization uses for behaviors.
Hur, Neis, Dreyer, Vafeiadis, The power of parameterization in coinductive proof (2013). The coinductive proof technique behind the behavior theorems.
Diskin, Xiong, Czarnecki (2011) and Johnson, Rosebrugh (2013), on delta lenses. The rollback round-trip laws.
Wood, Abstract pro arrows I (1982) and Grandis, Paré (1999). Equipments and double categories: the deploy grid’s squares, companions, and conjoints.
Pickering, Gibbons, Wu, Profunctor optics (2017). Prisms, the formal packaging of codecs.
Pnueli, Siegel, Singerman, Translation validation (1998) and Tristan, Leroy (2008). Prove the validator once, check every run: the verification stance of the whole model.

Each reference backs a specific claim in the model; the formal account in the repository carries the exact mapping.

A monoid is a set with an associative multiplication and a unit element; equivalently, a category with exactly one object, whose elements are arrows from that object to itself. A finite presentation writes down generators and equations between words, such as $a b = b a$ , and the word problem asks: given two words, do the equations prove them equal? Post showed in 1947 that there are finite presentations for which no algorithm can answer this in general. Since a monoid is a one-object category, path equality in unrestricted finitely presented categories inherits the undecidability. ↩
A critical pair is a place where two rewrite rules can both fire on overlapping input. Suppose the rules include $f \circ g \to h$ and $g \circ k \to m$ . On the path $f \circ g \circ k$ both apply: rewriting the left overlap gives $h \circ k$ , rewriting the right gives $f \circ m$ . The pair joins if $h \circ k$ and $f \circ m$ rewrite to the same normal form. A finite presentation has finitely many overlaps, so the checker can enumerate all of them. ↩
Newman’s lemma (1942): if rewriting always terminates, then local confluence implies full confluence. Local confluence: whenever one step can go two ways, $a \leftarrow c \to b$ , the two results can be rewritten back together, $a \to^{*} d \leftarrow^{*} b$ for some $d$ . Full confluence: any two rewrite sequences from the same start can be rejoined, no matter how long. The proof is well-founded induction on the termination measure: at a peak, step down each side, join the steps locally, and apply the induction hypothesis to the smaller peaks that remain. Termination is load-bearing; without it, local joins can fail to extend globally. ↩
The composition of two translation tables $P$ (from $𝐂$ to $𝐃$ ) and $Q$ (from $𝐃$ to $𝐄$ ) is

$\begin{matrix} (Q \otimes P) (c, e) & = \int^{d \in 𝐃} P (c, d) \times Q (d, e) \end{matrix}$

Read as: relate $c$ to $e$ through some intermediate $d$ , quotienting by the choice of $d$ so the composite does not depend on it. The integral sign is the coend, a colimit over the middle object. The analogy to keep: tables compose the way matrices multiply, with the sum replaced by the quotient and multiplication by pairing. ↩
The measure $Φ (I)$ is a weighted sum over the instance’s unfinished obligations, where an obligation’s weight accounts for the obligations discharging it will spawn. Because the schema’s total edges are acyclic, spawned obligations sit strictly deeper in the derivation order and carry strictly smaller weight, so every chase step decreases $Φ$ in $ℕ$ , and $ℕ$ has no infinite descending chains. Acyclicity is exactly what makes this work. Take two types $A$ and $B$ with total edges $f : A \to B$ and $g : B \to A$ , and seed a history with one element $a_{0}$ of $A$ : the chase must supply $f (a_{0}) = b_{0}$ , then $g (b_{0}) = a_{1}$ , then $f (a_{1}) = b_{1}$ , and unless an equality forces $a_{1} = a_{0}$ the instance grows forever. The mechanization proves this non-saturation as a control case, so the bound is not taken on faith. ↩
The naming comes from linear algebra. A matrix $A$ has an adjoint $A^{*}$ characterized by $⟨ A v, w ⟩ = ⟨ v, A^{*} w ⟩$ : applying $A$ on one side of the inner product is the same as applying $A^{*}$ on the other. The category-theoretic version replaces inner products with collections of maps: $hom (Σ_{P} x, y) ≅ hom (x, Δ_{P} y)$ . Each side is the best approximation of the other from its own world. The unit comes for free: set $y = Σ_{P} x$ and track the identity map across the isomorphism, and out falls $η_{x} : x \to Δ_{P} (Σ_{P} x)$ . ↩
A delta lens packages a forward pass and a backward pass with laws that keep them honest. In engine terms: view back what you migrated and you get the original ( $Δ_{P} (Σ_{P} x) ≅ x$ while the window is open), and re-migrating a viewed-back history agrees with the migration you started with, so the round trip invents nothing. R1 and R2 are the per-execution conditions that keep the first law alive as new events arrive; the first event violating either is the point of no return. ↩
The behavior functor describes one step of interaction: given a pending context, observe the reaction and the next context. Its final coalgebra is the largest system of behaviors, quotiented by nothing: two states are equal in it exactly when they are bisimilar, so equality in the tree is observational equivalence. The mechanization represents these trees as interaction trees, a coinductive datatype for programs that converse with an environment, and proves the behavior theorems by parameterized coinduction. If internal nondeterminism ever entered the model, the representation would move to choice trees: a planned revision with a known target, not an open question. ↩
Pnueli, Siegel, and Singerman introduced translation validation in 1998 for optimizing compilers: rather than prove the compiler correct once and for all, prove a checker that inspects each compilation and verifies the output matches the input. The versioning model applies the same stance to migrations. The registration checker and the replay check are proven correct once; every patch and every migration is then validated by them mechanically, per artifact, at registration and at migration time. ↩