Mathematical chronology
The formal record surrounding Respecting Equality, in time rather than dependency order.
What is dated here is the source, not the mathematics. Dates locate explicit formulations useful to a contemporary reader; they are not claims of first discovery, global knowledge, or historical transmission. Each entry is here because its mathematical statement materially sharpens something on the paper.
c. 300 BCEEuclid VII — number as a multitude of units same structure
Elements VII begins: a unit is that by virtue of which a thing is called one; a number is a multitude composed of units. The paper's §6 makes that structural reading literal by quotienting finite sets only by relabelling.
Paper: 6.1–6.3.
1901 / 1907Weber / Silberstein — Maxwell's two fields form one complex field same identity
Writing the electromagnetic field as F = E + iB combines the two vacuum evolution equations into one complex equation. The paper uses the same exact identification after deriving the quarter-turn σ²=-1 as the reversible complex structure.
Paper: §7.
1931Gödel — syntax becomes arithmetic lineage
Finite expressions and proofs can be coded by natural numbers. Arithmetic can therefore operate on representations of formal derivations and receive representations of its own expressions as ordinary data.
The important baseline shift is larger than incompleteness alone: symbolic procedure and arithmetic data are explicitly intertranslatable.
Paper: representability is isolated at 4.5–4.9.
1934Curry — implication already has function structure lineage
Combinatory logic relates functionality/type structure to implication. Howard will later make the identification systematic: logical construction and typed term construction are one syntax.
1936Church–Rosser computation — reduction order need not determine result used
Lambda computation is rewriting by substitution. Church–Rosser proves divergent beta-reductions joinable, so a normal form, when it exists, is unique.
Already computation need not mean one privileged instruction sequence. But this is only confluence: overlapping beta-redexes can require several steps to reconverge. §5 later uses a stronger local geometry.
1936Church, Kleene, Turing computation — program descriptions are data lineage
Lambda-definability, recursiveness, and machine computation converge extensionally. A program has a finite description; a universal evaluator consumes such a description as data and realizes the function it denotes.
The positive identification matters as much as undecidability: code, data, interpretation, and universal execution inhabit one mathematical universe.
Paper: halting is one diagonal instance at 4.10.
1942Newman computation — random descent fixes the number of steps same theorem shape
For an abstract reduction relation, the local quasi-diamond
implies random descent: when a normal form exists, every maximal reduction reaches it in the same number of steps. “Same result” and “same distance to the result” are distinct rewriting properties.
Paper: 5.11–5.13 gives the diamond and a checked self-contained peel/equalLength proof.
1948Shannon information — information loss has a number used
Uncertainty and information become quantitative. When an observation merges possibilities, the surviving fibre can be measured rather than merely called “loss.”
Paper: effect-cost in §3; separated from reduction length at 5.7.
1952Huffman cost — representation has exact path cost used
Weighted external path length of a binary merge tree is minimized by repeatedly combining the two smallest weights. With unit leaves, this is the balanced sum.
1936–1952Kleene — coding, interpretation, specialization, self-reference lineage
Recursive-function theory makes the code/data identification operational. Numbered programs can be universally evaluated; a code can be specialized to fixed arguments to produce another code; recursion/fixed-point theorems construct programs whose behavior refers to their own description.
The point is positive, not merely prohibitive: self-reference is constructible once programs, codes, and interpreter live in one arithmetic.
Paper: positive Lawvere/Kleene reading at 4.12, then Rice at 4.13.
1957Bellman cost — optimality is a distance equation used
Dynamic programming makes optimal cost satisfy a local recurrence: the optimal value at a state is the immediate step cost plus the optimal value of a successor, minimized over available successors. For unit edges this becomes the potential inequality used throughout the paper.
This is independent of random descent: the diamond says every normalizing route has the same length; a saturated potential certifies a shortest route even where the diamond fails.
1961Landauer information — erased distinctions have thermodynamic cost used
Logical irreversibility is tied to a minimum thermodynamic price. Bennett later supplies the complementary operational fact: computation can be organized reversibly apart from information actually discarded.
Paper: abstract zero-on-reversibles first in §3; physical reading at 5.9.
1969Howard — proofs are programs; normalization is execution used
The verbs prove, decide, compute, and answer need not name four engines; they can differ only in the requested type.
Paper: 5.1–5.3.
1969Lawvere diagonal — the diagonal is one fixed-point construction used
Let e : A → (A → B) contain every row. For g : B → B, form
If d=e(a₀), evaluating at its own index gives d(a₀)=g(d(a₀)), a fixed point. A fixed-point-free g forbids the table. Cantor, Russell, Tarski and halting are choices of this construction; read positively it builds self-reference. Gödel additionally consumes representability and consistency hypotheses.
Paper: 4.2–4.15.
1970sMartin-Löf equality — equality is executable substitution used
Dependent type theory internalizes equality. An inhabitant p : x ≡ y transports an inhabitant of a dependent family from the fibre over x to the fibre over y.
J says arbitrary identity can be handled from the reflexive case. The paper goes underneath this interface by explicitly contracting Σ[y∈A](x≡y).
Paper: 0.8–0.10.
1970sLévy computation — copied syntax can still be one computation lineage
If R contains a redex, substitution creates two reducible occurrences. A residual tracks what remains of a redex after another contraction; residual/copy ancestry groups occurrences into families with one computational origin.
Lévy optimality means essential family work is not redundantly performed. It is not minimum machine instructions or wall-clock time.
Paper: prior notion behind sharing at 5.24; distinct from random descent/equal length.
1987Girard computation — copying becomes explicit logical structure lineage
Linear logic stops hiding unrestricted copying and discard inside ambient structural rules. Proof nets expose normalization graphically; Geometry of Interaction reads proof dynamics through execution paths.
Proof nets, Lamping graphs, and interaction nets remain distinct constructions; the resource geometry ordinary syntax hides is now explicit.
1990Lamping computation — Lévy-family sharing becomes local graph reduction lineage
Lévy identifies which copied occurrences are one work-family. Lamping gives a local graphical implementation: fan/sharing structure carries duplication history so common work need not be blindly copied and recomputed, while copies can separate when their contexts require it.
Paper: immediate lineage of 5.24.
1990Lafont computation — local interaction structurally has the diamond used
An interaction-net cell has one principal port. A redex is an active pair: two principal ports joined. Two distinct active pairs therefore cannot share a cell; reducing one leaves the other available unchanged.
With Newman's random-descent observation, equal normalizing length follows. §5 proves the chain directly as a checked term: diamond → peel → equal length → minimality.
1996BOHM computation — optimal higher-order sharing is an implemented machine context
The Bologna Optimal Higher-order Machine implements a functional-language core using a variant of Lamping's optimal graph reduction, with graph reduction, garbage collection, and benchmarks. The Lévy/Lamping line is already executable machinery, not merely a semantic criterion.
1997Lafont computation — universal computation in three agents and six rules context
Interaction combinators compress universal distributed computation to a tiny local interaction algebra. The point is not numerology: general computation can be represented so execution consists entirely of microscopic active-pair rewrites.
1998Asperti–Guerrini computation — optimal implementation is a mature theory context
The Optimal Implementation of Functional Programming Languages systematizes Lévy optimality, Lamping sharing graphs, readback/correctness, proof-net and Geometry-of-Interaction interpretations, complexity, Interaction Systems, and implementation.
This matters terminologically: “optimal reduction” already has a precise family-sharing meaning. The paper's step-optimal statement is different: fixed interaction-net endpoints determine trace length by random descent.
1998Hofmann–Streicher equality — identity need not be proof-irrelevant lineage
The groupoid interpretation gives intensional identity nontrivial compositional structure: identity witnesses behave like arrows with composition and inverse. Identity can carry geometry rather than merely certify a Boolean fact.
2000sVoevodsky equality — equivalence is identity of types used
Univalence internalizes equivalence as identity. Stated axiomatically, however, it does not by itself give a normalizer a computational rule for transport along arbitrary univalence witnesses.
Paper: univalence is the opening interface; computational form arrives below.
2014Bezem–Coquand–Huber equality — equivalence becomes equality in a constructive cubical model lineage
A model of dependent type theory in cubical sets gives paths explicit formal dimensions and explains how to transform an equivalence between types into equality in a constructive metalogic.
The paper itself describes this as a step toward a computational interpretation of univalence.
2016 / 2018CCHM equality — univalence computes used
Cohen, Coquand, Huber, and Mörtberg give a cubical type theory where the De Morgan interval, composition/filling, and Glue make univalence internal and computational.
This is the crucial modern interface: equivalent types are not merely propositionally related; the identification can be executed as the equivalence itself.
2026Respecting Equality — the two formal lines meet this page
Two independently developed formal lines are available at once. On the equality side, equivalence has become executable identity. On the reduction side, shared higher-order work is explicit and the chosen local machine has random descent: fixed endpoints fix the interaction count. The paper identifies their common structure and proves the resulting inference statement on-page.
Result here. A declaration is normalized while respecting its available identities: reversible structure is transport; information destruction is a separate effect-cost; the declaration carries its available identities into reduction, so equivalent presentations are reachable inside the same computation; and the resulting primitive interaction count is fixed by the declaration—least over every reachable presentation and every normalizing schedule. The paper then works the consequences through number, divisibility/logic, reversible complex field dynamics, Boolean fibres/search, and ordering without changing the construction.
The claim is not delegated to this chronology: the core terms and reductions are checked on the page itself →