Geometry of Interaction

Origin. Jean-Yves Girard, "Geometry of interaction I: interpretation of System F" (1989), and the sequence through GoI V (1989–2011). Danos and Regnier's "Local and asynchronous beta-reduction" (1993, 1995) gave the path-algebra reading; Abramsky, Haghverdi, and Scott's "Geometry of interaction and linear combinatory algebras" (2002) gave the categorical axiomatization; Mackie's The Geometry of Interaction Machine (1995) built a compiler from it.

Models. Denotational semantics assigns a proof a static value. GoI assigns it a dynamics: an operator, and cut elimination becomes the computation of a feedback loop rather than a rewriting of syntax. A proof is a permutation of the wires of its own conclusion, and normalizing it means solving an equation, not applying a rule. The point is that cut elimination has a mathematics of its own, independent of the syntax it eliminates.

Formalism.

Proofs as operators: A proof of ⊢ Γ is interpreted as a partial isometry u on a Hilbert space ℓ²(ℕ), or as an element of a linear combinatory algebra in the axiomatized version.

Cut as feedback: Cutting two proofs u, σ gives the execution formula: EX(u, σ) = (1 − σ²) · u · (1 − σu)⁻¹ · (1 − σ²) The inverse is the feedback loop; σ encodes the cut links. Nilpotency of σu is what makes the series converge — and nilpotency is exactly strong normalization.

Strong normalization = nilpotency: The proof normalizes iff σu is nilpotent iff the series terminates. A syntactic property becomes an operator-algebraic one.

Paths and the token machine (Danos–Regnier): Read the proof net as a graph and send a token through it. Regular paths = the executions that survive; they are exactly the ones the operator computes. GoI is the algebra of persistent paths under reduction — the invariants of cut elimination.

Categorical axiomatization (Abramsky–Haghverdi–Scott): A traced monoidal category with a reflexive object. The trace is the feedback; the Int construction (Joyal–Street–Verity) builds the GoI category. So GoI is not about Hilbert spaces: it is about trace, and the operator model is one instance.

Locality: The execution formula is local and asynchronous: no global rewriting step. This is what made GoI implementable — the GoI machine executes proofs without normalizing them.

Symbols.

Metatheory. That strong normalization is nilpotency is the theorem the subject is for: a proof-theoretic property that ordinarily needs a combinatorial induction becomes an algebraic condition on an operator, and the induction disappears. The categorical account then shows the Hilbert space was inessential — trace is the primitive, and the Int construction manufactures a GoI interpretation from any traced monoidal category, which is why the same machinery reappears in quantum computation, in token machines, and in the semantics of feedback. Girard's later work extends the programme past logic into transcendental syntax; the mathematics has outlived the original application.

Applies to. Linear logic and proof nets. Compilation of functional languages without an environment — the GoI machine. Traced monoidal categories and feedback. Quantum computation, where the traced structure is the same. Implicit computational complexity, where nilpotency bounds are complexity bounds.

Limitations. The execution formula is opaque: it computes the right answer and does not explain it, and the operator-algebraic presentation gives few people the intuitions Girard had. Only the multiplicative fragment is fully understood — exponentials require substantial extra machinery and the treatments do not agree. The GoI machine was a proof of concept and no faster than a conventional one. And Girard's papers are famously unreadable, which has kept the subject small relative to its depth.

© 2026 Lingenic LLC