A notation for lambda terms is described that is useful in contexts where the intensions of these terms need to be manipulated. The scheme of de Bruijn is used for eliminating variable names, thus obviating α-conversion in comparing terms. A category of terms is provided that can encode other terms together with substitutions to be performed on them. The notion of an environment is used to realize this 'delaying' of substitutions. However, the precise environment mechanism employed here is more complex than the usual one because the ability to examine subterms embedded under abstractions has to be supported. The representation presented permits a β-contraction to be realized via an atomic step that generates a substitution and associated steps that percolate this substitution over the structure of a term. Operations on terms are provided that allow for the combination and hence the simultaneous performance of substitutions. Our notation eventually provides a basis for efficient realizations of β-reduction and also serves as a means for interleaving steps inherent in this operation with steps in other operations such as higher-order unification. Manipulations on our terms are described through a system of rewrite rules whose correspondence to the usual notion of β-reduction is exhibited and exploited in establishing confluence and other similar properties. Our notation is similar in spirit to recent proposals deriving from the Categorical Combinators of Curien, and the relationship to these is discussed. Refinements to our notation and their use in describing manipulations on lambda terms are considered in a companion paper.
Bibliographical noteFunding Information:
We are gratefult o P.-L. Curien for commentso n an earlierv ersiono f this paper. Suggestionfsr om reviewersh avel eadt o significanitm provementins presentationJo.h n Hannana nd an reviewero f an early presentatioonf the ideash ere (in ) madeu s awareo f relatedr esearchS. timulusw asp rovidedt o the first authorb y Mike O’Donnell and his studentbs y their participationin an expositiono f thesei deasi n Spring 1991. Work on this paperh as been supportedb y NSF grantsC CR-89-05825a nd CCR-92-08465.
- Confluence and noetherianity properties
- Explicit substitution notations
- Lambda calculus
- Lambda terms as representation devices