proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...

, the Geometry of Interaction (GoI) was introduced by

Jean-Yves Girard Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the Éc ...

shortly after his work on

linear logic Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the ...

. In linear logic,

proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a co ...

s can be seen as various kinds of networks as opposed to the flat tree structures of

sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautolog ...

. To distinguish the real proof nets from all the possible networks, Girard devised a criterion involving trips in the network. Trips can in fact be seen as some kind of

operator Operator may refer to: Mathematics * A symbol indicating a mathematical operation * Logical operator or logical connective in mathematical logic * Operator (mathematics), mapping that acts on elements of a space to produce elements of another sp ...

acting on the proof. Drawing from this observation, Girard described directly this operator from the proof and has given a formula, the so-called ''execution formula'', encoding the process of cut elimination at the level of operators. Subsequent constructions by Girard proposed variants in which proofs are represented as flows, or operators in

von Neumann algebra In mathematics, a von Neumann algebra or W*-algebra is a *-algebra of bounded operators on a Hilbert space that is closed in the weak operator topology and contains the identity operator. It is a special type of C*-algebra. Von Neumann al ...

s. Those models were later generalised by Seiller's Interaction Graphs models. One of the first significant applications of GoI was a better analysis of Lamping's algorithm for optimal reduction for the

lambda calculus In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...

. GoI had a strong influence on

game semantics Game semantics is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on Game theory, game-theoretic concepts, such as the existence of a winning strategy for a player. In this ...

for

and PCF. Beyond the dynamic interpretation of proofs, geometry of interaction constructions provide models of

, or fragments thereof. This aspect has been extensively studied by Seiller under the name of linear realisability, a version of

realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...

accounting for linearity. GoI has been applied to deep compiler optimisation for lambda calculi. A bounded version of GoI dubbed the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits.Dan R. Ghica. Function Interface Models for Hardware Compilation. MEMOCODE 2011

/ref>

References

Further reading