# Geometry of interaction

(Difference between revisions)
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 a proof of $A\limp B$ as a morphism from (the space interpreting) A to the (space interpreting) B and proof composition (cut rule) as the composition of morphisms. Rather the proof was interpreted as an operator acting on (the space interpreting) $A\limp B$, that is a morphism from $A\limp B$ to $A\limp B$. For proof composition the problem was then, given an operator on $A\limp B$ and another one on $B\limp C$ to construct a new operator on $A\limp C$. This problem was originally expressed as a feedback equation solved by the execution formula. The fact that the execution formula has some formal analogies with Kleene's formula for recursive functions allowed to claim that GoI was an operational semantics, as opposed to traditionnal denotational semantics.