On the Notion of Restriction in the Partial Lambda Calculus
by
Svitan Gaborovič
Fac. Civ. Eng. Maribor, Slovenia

The notion of restriction arises naturally when treating partial functions. It is formulated as an equational theory. Especially interesting is the notion of restriction in the scope of the partial lambda calculus where it is an important part of the syntax.

The partial lambda calculus was defined by Moggi in his thesis. Moggi proved the \beta_p reduction is confluent on the set of p\lambda-terms. \beta_p\eta_p-reduction is confluent modulo an equivalence and congruence relation between terms which is induced by the theory of restrictions (denoted \thicksim _\lceil). Pérez proved the theory of restriction is decidable and conjectured the confluence of \beta_p-reduction modulo this relation on the whole set of \lambda_p-terms.

Our intention is to study the notion of restriction in the scope of the partial lambda calculus. The idea is as follows. We impose directionality in the use of \thicksim _\lceil by defining a relation of reduction (denoted \underset\lceil --> ) so that \thicksim _\lceil is a reflexive, symmetric, and transitive closure of it. Nevertheless \underset\lceil --> is not a term rewriting it has some nice properties making it a useful tool for investigating the syntax of the partial lambda calculus. The results we get cast some light to the proof of the Pérez's conjecture.

Date received: March 14, 2000

Copyright © 2000 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # caex-00.