Geometry of interaction
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 that is 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 a mathematical 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 fragement 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.
