Geometry of interaction
Encyclopedia
The geometry of interaction (GoI) was introduced by Jean-Yves Girard
shortly after his work on Linear Logic
. In linear logic
, proofs can be seen as some kind of networks instead of the flat tree structure of sequent calculus
. To distinguish the real proof net
s from all the possible networks, Girard devised a criterium involving trips in the network. Trips can in fact be seen as some kind of operator 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.
At the same time, Lamping had given a hard to understand algorithm to compute the optimal reduction strategy for the lambda calculus
. Gonthier, Abadi and Levy have further shown that GoI allows better analysis of Lamping's algorithm. This work on the lambda calculus
has been independently carried by Danos and Regnier, Asperti and Guerrini. GoI work had a strong influence on game semantics
for linear logic
and PCF
.
GoI has been applied by Mackie to deep compiler optimisation for lambda calculi. A bounded version of GoI dubbed the Geometry of Synthesis has been used by Ghica to compile higher-order programming languages directly into static circuits.
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
shortly after his work on Linear Logic
Linear logic
Linear logic is a substructural logic proposed by 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...
. In linear logic
Linear logic
Linear logic is a substructural logic proposed by 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...
, proofs can be seen as some kind of networks instead of the flat tree structure of sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. To distinguish the real proof net
Proof net
In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiates proofs: irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and the order of rules applied...
s from all the possible networks, Girard devised a criterium involving trips in the network. Trips can in fact be seen as some kind of operator 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.
At the same time, Lamping had given a hard to understand algorithm to compute the optimal reduction strategy for the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
. Gonthier, Abadi and Levy have further shown that GoI allows better analysis of Lamping's algorithm. This work on the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
has been independently carried by Danos and Regnier, Asperti and Guerrini. GoI work had a strong influence on game semantics
Game semantics
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
for linear logic
Linear logic
Linear logic is a substructural logic proposed by 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...
and PCF
Programming language for Computable Functions
In computer science, Programming Computable Functions,"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions" . Programming Computable Functions is used by . It is also referred to as Programming with Computable Functions or Programming language...
.
GoI has been applied by Mackie to deep compiler optimisation for lambda calculi. A bounded version of GoI dubbed the Geometry of Synthesis has been used by Ghica to compile higher-order programming languages directly into static circuits.
External links
- GoI tutorial given at Siena 07 by Laurent Regnier, in the Linear Logic workshop, http://iml.univ-mrs.fr/~regnier/articles/siena07.pdf
Articles
- Dan R. Ghica. Function Interface Models for Hardware Compilation (invited tutorial paper) MEMOCODE 2011. ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign Cambridge, UK. July 11-13, 2011 http://www.cs.bham.ac.uk/~drg/papers/memocode11.pdf