Partiality in Logic and Computation - Aspects of Undefinedness

Abstract. A central theme in this thesis is the notion of undefinedness. Two forms of this notion are examined: undefinedness in existence, and undefinedness in information. The first form arises in case of ``error'', the second in case of non-terminating computations. The difference between both kinds is fundamental, identifying them leads to inconsistency. In part I of the thesis a first order partial logic with existence predicate is developed, i.e., in this logic one can express undefinedness in existence. The logic is based on a translation of partial terms to standard first order logic, resulting in an axiomatic presentation which is more elegant than the systems known from the literature. The translation is used to prove soundness and completeness. The logic is extended with a partialised form of Hilbert's \epsilon-operator. We use this operator to define lambda abstraction in first order logic. The extended logic is then used to describe a Zermelo-Fraenkel style theory for partial functions (called AFT). Conceptually, the theory AFT is based on an analysis of the process of mathematical abstraction in set theory, and a reformulation of this process for partial functions. The theories AFT and ZFC are interpretable in each other. A consequence of this is that AFT is a foundation for mathematics in the same way as ZFC-Set Theory is. In part II a programming language is described (in the form of a simply typed lambda calculus) in which one can compute with the first form of undefinedness in a straightforward way. In this calculus the possibility of the second form of undefinedness arises from the presence of recursion, in the form of a \mu-abstractor. Using this abstractor one can define various kinds of fixed point combinators (Curry's fpc, Turing's fpc, parameterized fpc's) in an elegant way, both in typed lambda calculus as well as in untyped lambda calculus. In the framework of this programming language we analyse the second form of undefinedness (i.e. undefinedness in information) in three different stages:

Evaluate a term and see whether it yields some kind of normal form. This leads to a unifying definition of normal forms, head normal forms, and weak head normal forms. It also leads to a unification of results on leftmost reduction.
Use a term in some context and see whether it can have a contribution to the outcome of a computation. This leads to the notion of ``usability''. This notion generalises the notion of solvability from the untyped lambda calculus, and formalises the informal notion of meaningfulness. The genericity lemma holds for unusable terms, and all unusable terms can be consistently identified. There is a remarkable difference between solvability and usability: in the untyped lambda calculus the solvable terms are the same as the terms with a head normal form, whereas in typed lambda calculus the usable terms lie ``between'' terms with a normal form and terms with a head normal form.
Equate a term to some other term and see whether an inconsistency arises. This leads to some generalisations of results from the untyped lambda calculus, like a generalisation of the easiness of \Omega. We formulate some general conditions on the question whether some extension of the (typed or untyped) lambda calculus is consistent. As an application of these results we mention that the consistency of the identification of Curry's and Turing's fixed point combinators can now be proved in an elegant proof theoretical way.

For the full thesis (postscript version): click Doctoral Dissertation (177+10 pages).

Bibliographic details, given in BIBTeX-format:

  @phdthesis{phd
  ,author = "Kuper, J."
  ,title  = "Partiality in Logic and Computation -- Aspects of Undefinedness"
  ,year   = 1994
  ,isbn   = "90-9006865-1"
  ,school = "University of Twente, Dept INF, Enschede, The Netherlands"
  }

Back to my home page.