Fully Complete Minimal PER Models for the Simply Typed lambda-Calculus

Abstract We show how to build a fully complete model for the maximal theory of the simply typed λ-calculus with k ground constants, λ k. This is obtained by linear realizability over an affine combinatory algebra of partial involutions from natural numbers into natural numbers. For simplicitly, we give the details of the construction of a fully complete model for λ k extended with ground permutations. The fully complete minimal model for λ k can be obtained by carrying out the previous construction over a suitable subalgebra of partial involutions. The full completeness result is then put to use in order to prove some simple results on the maximal theory.

Authors

• Samson Abramsky
• Marina Lenisa

Keywords

No keywords are indexed for this paper.