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.

Symbol	Unicode	Name	Meaning
σ	U+03C3	Sigma / Cut operator	The permutation encoding the cut links
ℓ	U+2113	Script small l	The ℓ² of the Hilbert space of square-summable sequences
²	U+00B2	Superscript two	Exponent in ℓ² and in σ²
ℕ	U+2115	Natural numbers	Index set of the Hilbert space basis
−	U+2212	Minus	Subtraction in the factors 1 − σ² and 1 − σu
·	U+00B7	Multiplication	Composition of operators in the execution formula
⁻	U+207B	Superscript minus	The inverse (1 − σu)⁻¹, the feedback loop
¹	U+00B9	Superscript one	Exponent of the inverse
⊢	U+22A2	Turnstile	Derivability of the one-sided sequent ⊢ Γ
Γ	U+0393	Gamma	The context, a multiset of formulas
×	U+00D7	Cartesian product	The pairing ℕ × ℕ → ℕ coding the exponentials
EX	—	Execution formula	The feedback computation replacing cut elimination
!	—	Bang / Exponential	Linear logic's reuse modality, coded by the pairing
ℓ²(ℕ)	—	Hilbert space	The original model; proofs are partial isometries on it
u	—	Proof operator	The partial isometry interpreting a proof
Tr	—	Trace	The categorical feedback operator
Int(C)	—	Int construction	Builds the GoI category from a traced one
1	—	Identity operator	Unit of the operator algebra

Metatheory. Girard's theorem in "Geometry of Interaction I" (1989) is that the execution formula is invariant under cut elimination and that σu is nilpotent exactly when the proof is strongly normalizing, so a property proved by combinatorial induction becomes a condition on an operator; the associativity of execution is what makes the interpretation independent of the order in which cuts are eliminated. Danos and Regnier showed the operator computes exactly the persistent, or regular, paths of the proof net — the paths that survive every reduction sequence — which identifies the algebra with a combinatorial invariant of the net. Abramsky, Haghverdi and Scott (2002) axiomatized the construction: a GoI situation in a traced symmetric monoidal category with a reflexive object yields a linear combinatory algebra, and the Int construction of Joyal, Street and Verity (1996) produces the compact closed category in which the interpretation lives. The Hilbert space is therefore one instance of trace rather than the subject matter.

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 defined by a series that converges only when σu is nilpotent, so the interpretation is partial: a non-normalizing proof or an untyped looping term has no value, and GoI is a semantics of terminating computation rather than a denotational model with a bottom element. Correspondingly the trace in the operator model is only partially defined, so the axiomatization is over a partially traced category rather than a genuinely traced one. Only the multiplicative fragment is settled; the exponentials require an auxiliary coding of ℕ × ℕ into ℕ that is chosen rather than canonical, and the several treatments give inequivalent interpretations of !. No full completeness result is available for the operator model, so there are operators satisfying the constraints that no proof denotes. The GoI machine matched conventional implementations without outperforming them.