{\bf (Revision of CS-1993-22.)} A Notation for Lambda Terms I: A Generalization of Environments
摘要
%A notation for lambda terms is described that is useful in contexts %where the intensions of these terms need to be manipulated. This %notation uses the scheme of de Bruijn for eliminating variable names, %thus obviating $\alpha$-conversion in comparing terms. This %notation also provides for a class of terms 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. The %precise mechanism employed here is, however, more complex than the %usual environment mechanism because it has to support the ability to %examine subterms embedded under abstractions. The representation %presented permits a $\beta$-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. %The operations on terms that are described also include ones for %combining substitutions so that they might be performed %simultaneously. Our notation eventually provides a basis for efficient %realizations of $\beta$-reduction and also serves as a means for %interleaving steps inherent in this operation with steps in other %operations such as higher-order unification. The various %manipulations on terms in our notation are described through a system %of rewrite rules. The correspondence of this rewrite system to the %usual notion of $\beta$-reduction is exhibited and is used in %establishing confluence and other properties pertaining to it. %There have been other proposals recently that are similar in spirit to %the one presented here, and the relationship between these is %discussed. Refinements to our notation and rewrite system and the %use of these in describing manipulations on lambda terms are %considered in detail in a companion paper.