We show that the principal types of the closed terms of the affine fragment of $\lambda$-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as partial involutions, in a natural Geometry of Interaction model \`a la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterising those partial involutions which are denotations of combinatory terms.
翻译:我们证明,在简单类型规则下,$\lambda$-演算仿射片段封闭项的主类型在结构上同构于它们在自然几何交互模型(à la Abramsky)中作为部分对合的解释。这允许用初等方式解释几何交互中出现的略显笨拙的线性应用概念,即通过使用交替统一算法在主类型之间进行消解。作为结果,我们针对纯仿射片段,为Abramsky提出的关于刻画作为组合子项指称的部分对合这一开放问题提供了答案。