Geometry of interaction

From LLWiki
Revision as of 16:47, 28 March 2009 by Laurent Regnier (Talk | contribs)

Jump to: navigation, search

The geometry of interaction, GoI in short, was defined in the early nineties by Girard as an interpretation of linear logic into operators algebra: formulae were interpreted by Hilbert spaces and proofs by partial isometries. This was a striking novelty as it was the first time that a mathematical model of logic (lambda-calculus) didn't interpret proofs by morphisms and the composition of proofs (allowed by the cut rule) by composition of morphisms, as it is the case in denotationnal or categorical semantics. Instead the GoI was claimed to be an operational semantics as it interpreted cut elimination as a mathematical process, namely the computation of a series, the execution formula that is the solution of a feed-back equation.

The first instance of the GoI, that will be described in details in this article, was restricted to the MELL fragment of linear logic (Multiplicative and Exponential fragment) which is enough to encode lambda-calculus. Since then Girard proposed several improvements: firstly the extension to the additive connectives known as Geometry of Interaction 3 and more recently a complete reformulation using Von Neumann algebras that allows to deal with some aspects of implicit complexity

The GoI has been a source of inspiration for various authors. Danos and Regnier have reformulated the original model exhibiting its combinatorial nature using a theory of reduction of paths in proof-nets and showing the link with abstract machines. It has been used in the theory of sharing reduction for lambda-calculus in the Abadi-Gonthier-Lévy reformulation and simplification of Lamping's representation of sharing. It was shown to be related to game semantics and more precisely to the Abramsky-Jagadeesan-Malacaria model of PCF. Finally the original GoI for the MELL fragment has been reformulated in the framework of traced monoidal categories following an idea originally proposed by Joyal.

Personal tools