A notation for lambda terms 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. 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.