Journal of Functional Programming

Table of Contents - 1992 - Volume 2, Issue 03  

Articles

Theoretical Pearls: Representing ‘undefined’ in lambda calculus

Henk Barendregta1

a1 Faculty of Mathematics and Computer Science, Catholic University Nijmegen, Toernooiveld 1, 6525 ED, The Netherlands (e-mail: henk@cs.kun.nl)

Abstract

Let ψ be a partial recursive function (of one argument) with λ-defining term Fxs2208Λ°. This means

S0956796800000447eqnU1

There are several proposals for what Fxs231Cnxs231D 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.