## The Partial Lambda Calculus

**E. Moggi**
*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.

Previous |

Index |

Next