Theoretical Pearls:Representing ‘undefined’ in lambda calculus
1992 ◽
Vol 2
(3)
◽
pp. 367-374
◽
Keyword(s):
AbstractLet ψ be a partial recursive function (of one argument) with λ-defining termF∈Λ°. This meansThere 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.
1991 ◽
Vol 1
(2)
◽
pp. 229-233
◽
2014 ◽
Vol 24
(6)
◽
Keyword(s):
1958 ◽
Vol 1
(3)
◽
pp. 183-191
◽
Keyword(s):
1985 ◽
Vol 28
(1)
◽
pp. 1-7
◽