Theoretical Pearls:Representing ‘undefined’ in lambda calculus

Publisher Website
Google Scholar
Abstract
Let ψ be a partial recursive function (of one argument) with λ-defining termF∈Λ°. This means There are several proposals for whatF⌜n⌝ should be in case ψ(n) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman).These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.

This publication has 5 references indexed in Scilit: