The Partial Lambda Calculus

Abstract: This thesis investigates various formal systems for reasoning about partial functions or partial elements, with particular emphasis on lambda calculi for partial functions. Beeson's (intuitionistic) logic of partial terms (LPT) is taken as the basic formal system and some of its metamathematical properties are established (for later application). Three different flavours of Scott's logic of partial elements (LPE) are considered and it is shown that they are conservative extensions of LPT. This result, we argue, corroborates the choice of LPT as the basic formal system.

Variants of LPT are introduced for reasoning about partial terms with a restriction operator \upharpoonright, monotonic partial functions (monLPT), lambda-terms lambda_p-calculus) and lambda Y-terms lambda_p mu Y-calculus). The expressive powers of some (in)equational fragments are compared in LPT and its variants. Two equational formal systems are related to some of the logics above: Obtulowicz's p-equational logic is related to LPT+ \upharpoonright and Plotkin's lambda_v-calculus is related to one flavour of LPE.

The deductive powers of LPT and its variants are compared, using various techniques (among them logical relations). The main conclusion drawn from this comparison is that there are four different lambda calculi for partial functions: intuitionistic or classical, partial or monotonic partial functions.

An (in)equational presentation of the intuitionistic lambda calculus for (monotonic) partial functions is given as an extension of p-equational logic. We conjecture that there is no equational presentation of the classical lambda_p-calculus. Via a special kind of diamond property, the (in)equational formal system is characterized in terms of beta-reductiion for partial functions and some decidabiliity problems are solved.
Ph.D. thesis - price £8.50

LFCS report ECS-LFCS-88-63 (also published as CST-53-88)

This is a 351-page PhD thesis which is available as a 521kb gzipped PostScript file.