Geometry of interaction
(Creation of the page, introduction) |
m (style corrections) |
||
| Line 1: | Line 1: | ||
| − | 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 [[Coherent semantics|denotationnal]] or [[Categorical semantics|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 ''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 [[Coherent semantics|denotationnal]] or [[Categorical semantics|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 <math>MELL</math> 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 [[Light linear logics|implicit complexity]] |
+ | The first instance of the GoI, that will be described in details in this article, was restricted to the <math>MELL</math> 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 [[Light linear logics|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 <math>MELL</math> fragment has been reformulated in the framework of traced monoidal categories following an idea originally proposed by Joyal. |
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 <math>MELL</math> fragment has been reformulated in the framework of traced monoidal categories following an idea originally proposed by Joyal. |
||
Revision as of 16:47, 28 March 2009
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.
