A characterization of terms of the λI-calculus having a normal form

Publisher Website
Google Scholar
Abstract
The theorem proved in this paper answers some transitivity questions (in the geometric sense) for the type free λ-calculus: Which objects can be mapped on all other objects? How much can an object do by applying it to other objects (see footnote 2)? The main result is that, for closed terms of the λ I-calculus, the following conditions are equivalent: (a) M has a normal form. (b) FM = I for some λI-term F. (c) MN 1 … Nn = I for some λI-terms N 1 …, Nn . By the same method it follows that if M is a closed term of the λK-calculus having a normal form, then for some λI-terms (sic) N 1, …, Nn , MN 1… Nn = I is provable in the λK-calculus. The theorem of Böhm [2] states that if M 1, M 2 are terms of the λK-calculus having different βη-normal forms, then ∀A 1, A 2 ∃N 1, …, NnMiN 1 … Nn = Ai is provable in the λK-βη-calculus for i = 1, 2. As a consequence of this it was shown (implicitly) in [1, 3.2.20 1/2 (1)] that if M has a normal form, then for some λK-terms N 1, …, Nn , MN 1 … Nn =I is provable in the λK-calculus. It was not clear that this also could be proved for the λK-calculus since the proof of the theorem of Böhm essentially made use of λK-terms. We conjecture that, using the results of this paper, the full theorem of Böhm can be proved for the λI-calculus.

This publication has 0 references indexed in Scilit: