A Notation for Lambda Terms:

A Generalization of Environments*

Gopalan Nadathur  Debra Sue Wilson
Department of Computer Science  IBM Corporation
Ryerson Hall, 1100 E 58th Street  TCJA/B631 D106
University of Chicago  4102 S. Miami Blvd.
Chicago, IL 60637  Research Triangle Park, NC 27706

              gopalan@cs.uchicago.edu         debwilson@vnet.ibm.com

Abstract

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.

Keywords: Lambda calculus, lambda terms as representation devices, explicit substitution notations, confluence and noetherianity properties.

* This paper is a revised version of Technical Report CS-1994-03, Department of Computer Science, Duke University and is to appear in Theoretical Computer Science.

1 Introduction

This paper concerns a notation for the terms in a lambda calculus that can serve as a basis for efficient implementations of operations on such terms. Traditionally, lambda terms have been used as a vehicle for performing computations, and the representation of these terms and the design of efficient evaluators for the lambda calculus in this context have received considerable attention. Our interest, however, is in a situation where lambda terms are used as a representational device. This interest is motivated primarily by implementation questions pertaining to λProlog, a logic programming language that employs the terms of a typed lambda calculus as its data structures [31]. We believe, however, that this issue is of wider concern, given the number of computer systems and programming languages in existence today that use some variety of the lambda calculus in representing and manipulating formal objects such as formulas, programs and proofs [5, 7, 8, 15, 18, 28, 35, 36].

Lambda terms have been found to be useful as data structures because of their ability to represent naturally the notion of binding that is part of the syntax of several kinds of objects [6, 23, 28, 34, 37]. Consider, for instance, the task of representing the quantified formula ∀x((p x)∨(q x)) in which p and q are predicate names. Observing that a quantifier plays the dual role of determining a scope and of making a predication, this formula can be rendered fairly transparently into the lambda term (all (λx ((p x) or (q x)))); in this term, all is a constant that represents universal quantification and or is an (infix) constant representing disjunction. Using such a representation makes the implementation of several logical operations on formulas relatively straightforward. For example, consider the operation of instantiation. Under the chosen representation, instantiating a ‘formula’ of the form (all P) by t is given simply by the term (P t). The actual task of substitution is carried out with all the necessary renamings by the β-reduction operation on lambda terms. As another example, suppose that we wish to determine if a given formula has a certain structure; such an operation would be relevant, for instance, to the construction of a theorem prover. The notion of unifying lambda terms provides a powerful tool for performing such ‘template matching’. Thus, consider the term (all (λx ((P x) or (Q x)))) in which P and Q are variables. This term matches with any formula whose top-level structure is that of a universal quantification over a disjunction and thus ‘recognizes’ such formulas. In contrast, the term (all (λx ((P x) or Q))) requires also that the second disjunct not contain the quantified variable and thus serves as a sharper discriminator.^{1}

Our interest in this paper is in a suitable representation for lambda terms, assuming that they are to be used in the manner outlined above. The intended application obviously places constraints on the kinds of representations that might be considered. For example, the applications of interest generally require the comparison of the structures of lambda terms. The chosen representation must therefore make this structure readily available. At a more detailed level, the comparison of lambda terms must ignore the particular names used for bound variables. To cater to this need, the representation that is used must permit equality up to α-convertibility to be determined easily. Finally, an operation of obvious importance is β-reduction, and any reasonable representation must enable this to be performed efficiently. For reasons that we discuss in Section 4, the representation that is used must support two requirements relative to this operation: first, it should be possible to perform the substitutions generated by β-contractions in a lazy manner and, second, it should be possible to perform β-contractions under abstractions as well as to percolate substitutions generated by it into such contexts.

1The notion of unification (used in an informal sense here) is intelligible only in the context of certain typed versions of the lambda calculus. We do not discuss the issue of typing explicitly here since the main concerns of this paper are orthogonal to it.

We describe a notation for lambda terms in this paper that provides a basis for meeting these various requirements. The starting point for our notation is a scheme suggested by de Bruijn [3] for eliminating variable names from terms. To provide a means for delaying substitutions, we utilize the notion of an environment. However, a direct use of this device as developed in the context of implementations of functional programming languages is not possible; the complicating factor is the need for performing substitutions and β-contractions under abstractions. The notation we describe embellishes the notion of an environment in a manner designed to overcome this difficulty. At a level of detail, our proposal shares features with the data structures used in [2] in implementing a normalization procedure. However, in a manner akin to other recent proposals deriving from the Categorical Combinators of Curien [1, 10, 13], it has the characteristic of reflecting the idea of an environment into the notation itself. There are two advantages to adopting this course. First, the resulting notation is fine-grained enough to support a wide variety of reduction procedures on lambda terms, and the analysis undertaken here makes it easy to verify the correctness of these procedures. Second, using such a notation makes it possible to intermingle what are traditionally conceived of as steps within β-contraction with other operations such as those needed in higherorder unification [20]. There is, in fact, a concrete realization of the second idea: the notation developed here is actually being used in this fashion in an implementation of λProlog [30].

The remainder of this paper is organized as follows. The next section summarizes prior logical notions that are used in this paper. Section 3 reviews the de Bruijn notation for lambda terms. We describe our notation for lambda terms in Section 4 and also present the rewrite rules that are intended to mimic β-reduction in its context. We then study the properties of our notation. In Section 5 we describe a well founded partial ordering relation on our terms that is useful in establishing termination properties of subsets of our rules and in constructing inductive arguments. In the following section, we analyze a particular subset of our rewrite rules whose purpose is, roughly, that of reducing terms in our notation that encapsulate substitutions into ones in de Bruijn’s notation. We show that every sequence of rewritings using these rules eventually produces the anticipated de Bruijn term from any given term in our notation. In Section 7, we examine the correspondence between the usual notion of β-reduction and our system of rewrite rules. We show here that every β-reduction sequence on de Bruijn terms can be mimicked within our notation and, conversely, any rewrite sequence on our terms can be projected onto a β-reduction sequence on the underlying de Bruijn terms. The advantage of our notation can then be appreciated as follows: it defines a β-contraction operation that is a truly atomic and it provides a fine-grained control over the substitution process. In Section 8, we utilize the projection onto de Bruijn terms to show the confluence of our rewrite system. The method of proof we use is similar in spirit to that referred to as the interpretation method in [17] and used in [17] and [39] in establishing confluence properties of a combinator calculus. In the concluding section of this paper, we discuss the relationship of our work to that of others, especially that in [1] and [13].

2 Logical preliminaries

We are concerned in this paper with systems for rewriting expressions. Each such rewrite system is specified by a set of rule schemata. A rule schema has the form l → r where l and r are expression schemata referred to as the lefthand side and the righthand side of the rule schema, respectively. For example, the system we describe in Section 4 contains the schema:

[[(t_{1} t_{2}), ol, nl, e]] → ([[t_{1}, ol, nl, e]] [[t_{2}, ol, nl, e]]).

In these schema, t_{1}, t_{2}, ol, nl and e represent metalanguage variables ranging over appropriately defined categories of expressions. Particular rules may be obtained from this schema by suitably instantiating these variables. All our rule schemata satisfy the property that any syntactic variable appearing in the righthand side already appears in the lefthand side.

Given a notion of subexpressions within the relevant expression language, a rule schema defines a relation between expressions as follows: t_{1} is related to t_{2} by the rule schema if t_{2} is the result of replacing some subexpression s_{1} of t_{1} by s_{2} where s_{1} → s_{2} is an instance of the schema. We refer to occurrences in expressions of instances of the lefthand side of a rule schema as redex occurrences of the schema. The qualification by the rule schema may be omitted if it is clear from the context. Alternatively, a special name may be used to signify the correspondence to the rule schema.

The relation corresponding to a rule schema is referred to as the one that is generated by it. The relation generated by a collection of rule schemata is the union of the relations generated by each schema in the collection. Let ⊳ denote such a relation. We will usually write t ⊳ r to signify that t is related to s by virtue of ⊳. The reflexive and transitive closure of ⊳ will be denoted by ⊳^{∗}, a relation that will, once again, be written in infix form. Intuitively, t⊳^{∗}s signifies that t can be rewritten to s by a (possibly empty) sequence of applications of the relevant rule schemata. In accordance with this viewpoint, we refer to the relation ⊳ as a rewrite or reduction relation and we say that t ⊳-reduces to s if t⊳^{∗}s.

A notion of concern with regard to a rewrite relation ⊳ is that of a ⊳-normal form. An expression t is in this form if there is no expression s such that t ⊳ s. That is, t contains no redex occurrences of any of the rule schemata that generate ⊳. A ⊳-normal form of an expression r is an expression t such that r ⊳-reduces to t and t is in ⊳-normal form. The existence and uniqueness of normal forms for expressions are issues that are of interest for a variety of reasons. For example, rewrite rules are often used as a means for computing. Their use in this capacity is meaningful only if the result of performing the computation — the normal form, if it exists — is independent of the method of carrying out the computation. This will be the case if normal forms are unique. In a sense more pertinent to this paper, a collection of rewrite rule schemata is usually intended as a set of equality axioms in a given logical system. Using them to rewrite expressions is useful in this context only if this somehow helps in determining equality. This is indeed the case if a unique normal form exists for every expression: the equality of two expressions can then be determined by reducing them to their normal forms and comparing these.

A rewrite relation ⊳ is noetherian if and only if there is no infinite sequence of the form t_{1} ⊳ t_{2} ⊳ ⋯ ⊳ t_{n} ⊳ ⋯, i.e., if and only if every sequence of rewritings relative to ⊳ terminates. If ⊳ is noetherian, a ⊳-normal form must exist for every expression. In showing that such a form is unique, the notion of confluence is useful. The relation ⊳ is said to be confluent if, given any expressions t, s_{1} and s_{2} such that t⊳^{∗}s_{1} and t⊳^{∗}s_{2}, there must be some expression r such that s_{1}⊳^{∗}r and s_{2}⊳^{∗}r. Confluence is of interest because of the following proposition whose proof is straightforward.

Proposition 2.1 If ⊳ is a confluent reduction relation, then if a ⊳-normal form exists for any expression, it must be unique.

A rewrite relation ⊳ is said to be locally confluent if, whenever t⊳s_{1} and t⊳s_{2} for expressions t, s_{1} and s_{2}, there must be some expression r such that s_{1}⊳^{∗}r and s_{2}⊳^{∗}r. Local confluence is related to confluence by the following proposition, a proof for which may be found in [21].

Proposition 2.2 A noetherian reduction relation is confluent if and only if it is locally confluent.

In showing that a reduction relation is locally confluent, an observation in [25] that is generalized in [21] may be used. To describe this observation, we need the following definition.

Definition 2.3 An expression t constitutes a nontrivial overlap of rule schemata R_{1} and R_{2} at a subexpression s of t if (a) t is a redex occurrence of R_{1}, (b) s is a redex occurrence of R_{2} and also does not occur within the instantiation of a schema variable when t is matched with R_{1}, and (c) either s is distinct from t or R_{1} is distinct from R_{2}. Let r_{1} be the expression that results from rewriting t using R_{1} and let r_{2} result from t by rewriting s using R_{2}. Then the pair ⟨r_{1}, r_{2}⟩ is referred to as the conflict pair relative to the overlap in question. The conflict pairs of a collection of rule schemata R is the set of the conflict pairs obtained by considering all possible nontrivial overlaps between the elements of R.

The conflict pairs as defined here constitute all the ground instances of the critical pairs of a rewrite system in the sense of [21]. We use the notion of critical pairs only at a metalanguage level to avoid a consideration of expressions containing variables.

The observation that is critical to showing local confluence is now the following:

Theorem 2.4 Let ⊳ be a reduction relation generated by the collection R of rule schemata. Then ⊳ is locally confluent if and only if for every conflict pair ⟨r_{1}, r_{2}⟩ of R there is some expression s such that r_{1}⊳^{∗}s and r_{2}⊳^{∗}s.

Proof. (Adapted from [21].) Only the ‘if’ part in nontrivial and needs argument. Let t be any expression and let t_{1} and t_{2} be the result of rewriting, respectively, the subexpressions s_{1} and s_{2} in t using the members R_{1} and R_{2} of R. To show that R is locally confluent, we need to show that there is some expression r such that t_{1}⊳^{∗}r and t_{2}⊳^{∗}r. We consider the various possibilities for s_{1} and s_{2} and show that this must be the case. If s_{1} and s_{2} appear in disjoint parts of t, this is obvious: there is a ‘residue’ of s_{2} in t_{1} and similarly of s_{1} in t_{2} and a common expression is obtained by rewriting the first of these (in t_{1}) using R_{2} and the second (in t_{2}) using R_{1}. So suppose that one of s_{1} and s_{2} is a subexpression of the other. Without loss of generality, let s_{2} be a subexpression of s_{1}. Now, if s_{1} is identical to s_{2} and R_{1} = R_{2}, then t_{1} = t_{2} and the desired conclusion is immediately reached. If s_{2} is a subexpression of a part of s_{1} that is matched with a schema variable in R_{1}, a little additional argument suffices. On the one hand, the rewriting step that produces t_{1} will create a finite number of copies of s_{2} in t_{1} and on the other hand rewriting s_{2} produces in t_{2} a subexpression s′_{1} that is still a redex occurrence of R_{1}. It is easily seen that using R_{2} repeatedly to rewrite the copies of s_{2} in t_{1} and R_{1} to rewrite s′_{1} in t_{2} produces a common expression. The only remaining situation is the one where s_{2} is a subexpression of s_{1} that matches with a part of R_{1} distinct from a schema variable and where either s_{1} is distinct from s_{2} or R_{1} is distinct from R_{2}. However, in this case s_{1} constitutes a nontrivial overlap of R_{1} and R_{2} at s_{2}. Let r_{1} result from rewriting s_{1} using R_{1} and let r_{2} result from s_{1} by rewriting the subexpression s_{2} using R_{2}. Then ⟨r_{1}, r_{2}⟩ constitutes a conflict pair of R and, by assumption, there is an expression s such that r_{1}⊳^{∗}s and r_{2}⊳^{∗}s. Let r be the expression obtained from t by replacing the subexpression s_{1} by s. It must then be the case that t_{1}⊳^{∗}r and t_{2}⊳^{∗}r.

□

3 The de Bruijn notation

Conventional presentations of the lambda calculus utilize a scheme that requires names for bound (and free) variables (e.g. see [19]). This choice is well-motivated from the perspective of human readability but is not well-suited to machine implementations for at least two reasons. First, it is difficult to systematize the care that must be exercised within this notation in preventing the inadvertent capture of free variables in the course of performing substitutions generated by β-reduction. Second, the determination of identity of two terms is complicated by the need to consider renamings for bound variables. The ‘nameless’ notation proposed by de Bruijn [3] provides an elegant way of dealing with the first problem and it eliminates the second by rendering lambda terms in the conventional notation that differ only in the names of bound variables into a common form. This notation is central to the discussions in this paper and we therefore outline it below.

We begin with the definition of lambda terms in the de Bruijn notation.

Definition 3.1 The collection of de Bruijn terms, denoted by the syntactic category ⟨DT erm⟩, is given by the rule

⟨DT erm⟩ ::= ⟨Cons⟩ | #⟨Index⟩ | (⟨DT erm⟩ ⟨DT erm⟩) | (λ ⟨DT erm⟩)

where ⟨Cons⟩ is a category corresponding to a predetermined set of constant symbols and ⟨Index⟩ is the category of positive numbers. A de Bruijn term of the form (i) #i is referred to as an index or a variable reference, (ii) (λ t) is called an abstraction and (iii) (t_{1} t_{2}) is referred to as an application. The subterm or subexpression relation on de Bruijn terms is given recursively as follows: Each term is a subterm of itself. If t is of the form (λ t′), then each subterm of t′ is also a subterm of t. If t is of the form (t_{1} t_{2}), then each subterm of t_{1} and of t_{2} is also a subterm of t.

A bound variable occurrence within the conventional scheme for writing lambda terms is represented in the de Bruijn notation by an index that counts the number of abstractions between the occurrence and the abstraction binding it. Thus, the term (λx ((λy (y x)) x)) in conventional presentations is written in the de Bruijn notation as (λ ((λ (#1 #2)) #1)). An alternative, more complete, exposition of the correspondence is the following. We think of the level of a subterm in a term as the number of abstractions in the term within which the subterm is embedded. We also assume a fixed listing of the free variables with respect to which we can talk of the n-th free variable. Then, a variable reference #i occurring at level j in a term corresponds to a bound variable if j ≥ i. Further, in this case, it represents a variable that is bound by the abstraction at level (j − i) within which the variable reference occurs. In the case that i > j, the index #i represents a free variable, and, in fact, the (i − j)-th free variable. It is easily seen that lambda terms that are α-convertible in the conventional notation correspond to the same term under this scheme.

An important operation on lambda terms is that of substitution. In the context of the de Bruijn notation, a generalized notion of substitution — that of substituting terms for all the free variables — is given by the following definition.

Definition 3.2 Let t be a de Bruijn term and let s_{1}, s_{2}, s_{3}, … represent an infinite sequence of de Bruijn terms. Then the result of simultaneously substituting s_{i} for the i-th free variable in t for i ≥ 1 is denoted by S(t; s_{1}, s_{2}, s_{3}, …) and is defined recursively as follows:

(1) S(c; s_{1}, s_{2}, s_{3}, …) = c, for any constant c, (2) S(#i; s_{1}, s_{2}, s_{3}, …) = s_{i} for any variable reference #i,

(3) S((t_{1} t_{2}); s_{1}, s_{2}, s_{3}, …) = (S(t_{1}; s_{1}, s_{2}, s_{3}, …) S(t_{2}; s_{1}, s_{2}, s_{3}, …)), and

(4) S((λ t); s_{1}, s_{2}, s_{3}, …) = (λ S(t; #1, s′_{1}, s′_{2}, s′_{3}, …)) where, for i ≥ 1, s′_{i} = S(s_{i}; #2, #3, #4, …).

We shall use the expression S(t; s_{1}, s_{2}, s_{3}, …) as a meta-notation for the term it denotes.

Towards understanding the above definition, we note that within a term of the form (λ t), the first free variable is actually denoted by the index #2, the second by #3 and so on. This requires, in (4) above, that the indices for free variables within the terms s_{1}, s_{2}, s_{3}, … being substituted into (λ t) be “incremented” by 1 prior to substitution into t. Further, the index #1 must remain unchanged within t and it is the indices #2,#3,… that must be substituted for.

We will need to consider the effect of cascading substitutions of the above kind. An observation made in [3] is useful in this context. The term denoted by S(S(t; s_{1}, s_{2}, s_{3}, …); s′_{1}, s′_{2}, s′_{3}, …) is produced by first replacing every index in t with some term s_{i}, and then substituting the terms s′_{1}, s′_{2}, s′_{3}, … into the result. Thus the s′_{i} terms will only be substituted into occurrences of the s_{j} terms, and the effect of this substitution can be precomputed. This is formalized in the following proposition taken from [3].

Proposition 3.3 Given de Bruijn terms t, s_{1}, t_{1}, s_{2}, t_{2}, s_{3}, t_{3} …

S(S(t; s_{1}, s_{2}, s_{3}, …); t_{1}, t_{2}, t_{3}, …) = S(t; u_{1}, u_{2}, u_{3}, …)

where, for i ≥ 1, u_{i} = S(s_{i}; t_{1}, t_{2}, t_{3}, …).

The substitution operation is useful in defining the notion of ⊳_{β}-reduction, also referred to simply as β-reduction.

Definition 3.4 The β-contraction rule schema is the following

((λ t_{1}) t_{2}) → S(t_{1}; t_{2}, #1, #2, …)

where t_{1} and t_{2} are schema variables for de Bruijn terms. The relation (on de Bruijn terms) generated by this rule schema is denoted by ⊳_{β} and is called β-contraction. An instance of the lefthand side of the rule schema is called a β-redex.

When a β-contraction is performed, the β-redex is replaced by the term which results from substituting t_{2} for the first free variable in t_{1} and adjusting the remaining indices. In the next section a notation will be introduced which decouples the generation and performance of the substitution by, in essence, moving the meta-notation S(t_{1}; t_{2}, #1, #2, …) into the term representation. The following theorem states a property of commutativity between β-reduction and the substitution operation that will be useful in analyzing this notation.

Theorem 3.5 Let t_{0}, t_{1}, t_{2}, … be de Bruijn terms.

(i) If t_{0}⊳_{β}^{∗}t′_{0}, then S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}^{∗}S(t′_{0}; t_{1}, t_{2}, t_{3}, …).

(ii) If, for i ≥ 1, t_{i}⊳_{β}^{∗}t′_{i}, then S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}^{∗}S(t_{0}; t′_{1}, t′_{2}, t′_{3}, …)

Proof. (i) It suffices to show that if t_{0}⊳_{β}t′_{0} then S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}S(t′_{0}; t_{1}, t_{2}, t_{3}, …). We do this by an induction on the structure of t_{0}. Note first that t_{0} must be either an abstraction or an application. Suppose t_{0} is an abstraction. In particular, let t_{0} = (λ s). Then the redex that is rewritten must be a subterm of s. The desired conclusion now follows from Definition 3.2 and the inductive hypothesis. If t_{0} is an application, there are two possibilities. In the first case, t_{0} is not the redex rewritten. In this case we again use Definition 3.2 and the inductive hypothesis to reach the desired conclusion. In the other case, t_{0} is of the form ((λ s_{1}) s_{2}) and, correspondingly, t′_{0} is the term S(s_{1}; s_{2}, #1, #2, …). Now, assuming that, for i ≥ 1, t′_{i} = S(t_{i}; #2, #3, #4, …),

S(t_{0}; t_{1}, t_{2}, t_{3} …) = ((λ S(s_{1}; #1, t′_{1}, t′_{2}, …)) S(s_{2}; t_{1}, t_{2}, t_{3}, …))

But then

S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}S(S(s_{1}; #1, t′_{1}, t′_{2}, …); S(s_{2}; t_{1}, t_{2}, t_{3}, …), #1, #2, …).

Using Proposition 3.3,

S(S(s_{1}; #1, t′_{1}, t′_{2}, …); S(s_{2}; t_{1}, t_{2}, t_{3}, …), #1, #2, …) = S(s_{1}; S(s_{2}; t_{1}, t_{2}, t_{3}, …), t′′_{1}, t′′_{2}, …),

where t′′_{i} = S(t′_{i}; S(s_{2}; t_{1}, t_{2}, t_{3}, …), #1, #2, …). Noting the definition of t′_{i} and using Proposition 3.3 again, it can be seen that t′′_{i} = t_{i}. Thus, S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}S(s_{1}; S(s_{2}; t_{1}, t_{2}, t_{3}, …), t_{1}, t_{2}, …). On the other hand, again using (Proposition 3.3),

S(t′_{0}; t_{1}, t_{2}, t_{3}, …) = S(S(s_{1}; s_{2}, #1, #2, …); t_{1}, t_{2}, t_{3}, …) = S(s_{1}; S(s_{2}; t_{1}, t_{2}, t_{3}, …), t_{1}, t_{2}, …).

Thus, even in this case, S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}S(t′_{0}; t_{1}, t_{2}, t_{3}, …).

(ii) The proof is again by induction on the structure of t_{0}. The constant and index cases are immediate and the application case is handled by a straightforward recourse to Definition 3.2 and the inductive hypothesis. The only remaining case is that when t_{0} is of the form (λ s). In this case

S(t_{0}; t_{1}, t_{2}, t_{3}, …) = (λ S(s; #1, u_{1}, u_{2}, …))

where u_{i} = S(t_{i}; #2, #3, #4, …). By (i), for i ≥ 1, u_{i}⊳_{β}^{∗}S(t′_{i}; #2, #3, #4, …). Using the inductive hypothesis and Definition 3.2, it now follows easily that S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}^{∗}S(t_{0}; t′_{1}, t′_{2}, t′_{3}, …)

□

The following corollary is proved by using Theorem 3.5 twice.^{2} Corollary 3.6 Let t_{0}, t_{1}, t_{2}, … be de Bruijn terms and, for i ≥ 0, let t_{i}⊳_{β}^{∗}t′_{i}. Then

2This corollary generalizes a theorem in [3] that is used in proving the Church-Rosser Theorem for β-reduction.

S(t_{0}; t_{1}, t_{2}, t_{3}, …)⊳_{β}^{∗}S(t′_{0}; t′_{1}, t′_{2}, t′_{3}, …).

Finally, we observe the celebrated Church-Rosser Theorem for β-reduction. A proof of it in the context of the de Bruijn notation appears in [3].

Proposition 3.7 The relation ⊳_{β} is confluent.

4 Incorporating environments into terms

The de Bruijn notation is useful in contexts where the intensions of lambda terms have to be examined because it makes it unnecessary to consider α-conversion. However, the operation of substitution necessitated by β-contraction is a fairly complex one even within this notation. From a practical perspective, it is useful to obtain some control over this operation and, in particular, to be able to perform it lazily. For instance, consider the task of determining whether the two terms

((λ (λ (λ ((#3 #2) s)))) (λ #1)) and ((λ (λ (λ ((#3 #1) t)))) (λ #1))

are equal modulo the rules of λ-conversion; s and t denote arbitrary terms here. It might be concluded that they are not, by observing that these terms reduce to (λ (λ (#2 s′))) and (λ (λ (#1 t′))), where s′ and t′ result from s and t by appropriate substitutions. Notice that it is enough to determine that the heads of these terms are distinct without explicitly performing the potentially costly operation of substitution on the arguments. Along a different direction, we observe that the structures of terms have to be traversed while attempting to reduce them to normal forms as well as in performing the substitutions generated by each β-contraction. By delaying substitutions, it may be possible to combine these traversals, thereby leading to gains in efficiency. Thus, consider the term ((λ ((λ t_{1}) t_{2})) t_{3}) where t_{1}, t_{2} and t_{3} represent arbitrary terms. Let t′_{2} be the result of substituting t_{3} for the ‘first’ free variable in t_{2} and decrementing the indices of all the other free variables by one. Now, in reducing the given term to a normal form, it is necessary to substitute t′_{2} and t_{3} for the the first and second free variables in t_{1} and to decrement the indices of all the other free variables by two. All these substitutions can be achieved in one traversal over the structure of t_{1} provided we have a fine-grained control over the way each substitution is carried out. An observation of this kind is, in fact, exploited in the implementation of β-reduction in [2].

In contexts where the lambda calculus is employed as a vehicle for computation, the use of an environment that describes bindings for free variables suffices for delaying substitutions. In situations where the de Bruijn notation is utilized, this device is adequate only because the structure of terms embedded within abstractions need not be explored. Thus, if a term is produced in the course of β-reduction that has an abstraction at the outermost level, then the term may be combined with its environment and returned as a closure; this idea is used, for instance, in [9].

However, this assumption is not appropriate in contexts where lambda terms are used as a means for representation. As an example, consider again the task of determining whether the two terms

((λ (λ (λ ((#3 #2) s)))) (λ #1)) and ((λ (λ (λ ((#3 #1) t)))) (λ #1))

are equal. In ascertaining that they are not, it is necessary to propagate a substitution generated by a β-contraction under an abstraction and also to contract β-redexes embedded inside abstractions. The idea of an environment cannot be adapted naively to yield a delaying mechanism relative to these requirements. For instance, if a term of the form ((λ t) s) is embedded within abstractions, it is to be expected that (λ t) contains free variables. Hence, if the result of β-contracting this term is to be encoded by the term t and an ‘environment’, the environment must record not just the substitution of s for the first free variable but also the ‘decrementing’ of the indices corresponding to all the other free variables. Similar observations can be made about propagating substitutions under abstractions.

While the usual idea of an environment cannot be employed directly, a generalization of this notion suffices even in the context of interest. We describe a notation for lambda terms in this section that incorporates such a generalization into the de Bruijn representation for these terms. Our notation provides a means for capturing the generation of the substitution corresponding to a β-contraction in a truly atomic step. This operation is then combined with rules for ‘reading’ terms to realize the full effect of the complex substitution operation described in Section 3.

4.1 Informal description of an enhanced notation

Before presenting the details of our notation, we explain the main ideas that underlie it. Our objective is to include a new category of expressions within our terms that will encode ‘suspended’ forms of substitutions that are to be performed over de Bruijn terms. An encoding of the substitution operation described in Definition 3.2 in its full generality is difficult: this would require the representation in a finite structure of simultaneous substitutions for an infinite number of variable references. Fortunately, we need to deal only with the kinds of substitutions that arise through β-contractions and the subsequent propagation of these by virtue of Definition 3.2. Such substitutions exhibit a pattern that can be exploited in providing finite representations for them. In particular, they all have the form S(t; s_{1}, s_{2}, s_{3}, …) where, for some finite i ≥ 1, it is the case that the sequence s_{i}, s_{i+1}, s_{i+2}, … is one of consecutive positive integers. The outcome of such a substitution is completely determined by the starting point of this sequence, the terms up to s_{i} that are not part of this sequence and, finally, the term t into which the substitutions are to be performed.

Let us look at the particular kind of situations that are to be treated to understand how exactly these items of information may be recorded. In the simplest case, the task is that of encoding the alterations that must be made to the variable references within a term t to account for the rewriting of a β-redex inside whose ‘left’ subterm t is embedded. Thus, suppose that the β-redex we wish to rewrite is

((λ … (λ … (λ … t …) …) s);

we have elided much of the term in this depiction, indicating only those aspects of its shape that are relevant to the present discussion. Rewriting this term produces a term of the form

(… (λ … (λ … t′ …) …).

Our goal is to provide a means for representing of the term t′ that appears in this expression as the term t together with the substitutions that are to be performed on it.

The variable references within t can be factored into two groups: those that correspond to free variables relative to the given β-redex (but that may possibly be bound in a larger context), and those that correspond to variables bound by one of the abstractions contained within the β-redex. Given a term in a particular context, let us refer to the number of abstractions enclosing that term as its embedding level. For example, assuming that every abstraction within the displayed β-redex has been explicitly depicted, the embedding level of t relative to this β-redex is 3. Rewriting a β-redex eliminates an abstraction and thus changes the embedding level for t; in the particular case considered, this becomes 2. Let us refer to the embedding levels before and after the rewriting step as the old and new embedding levels and let us denote them by ol and nl respectively. Now, the variable references in t that are in the first group are precisely those of the form #i where i > ol.^{3} Further, these references need to be rewritten to #j where j = (i − ol) + nl to reflect the fact that they are now free variables relative to a new embedding level. Thus, recording the old and new embedding levels with t determines both the variable references in the first group and the substitutions that must be made for them.

The variable references in the second group are finite in number and substitutions for them can be recorded in an environment. To use a concrete syntax, the term t′ in the situation considered might be represented by an expression of the form [[t, ol, nl, e]], where e encodes the appropriate environment. Note that the number of entries in this environment must be identical to the old embedding level. At a level of detail, the environment can be maintained as a list whose elements are in reverse order to the (old) embedding level of the abstractions they correspond to. The virtue of using this order is that the substitution pertaining to the variable reference #i is given by the i-th element of the list. The environment must, in general, contain information pertaining to two different kinds of abstractions: those that persist in the new term and those that disappear as a result of a β-contraction. The information present must suffice, in the first case, for computing a new value for a variable reference bound by the relevant abstraction and, in the second case, for determining the term to replace it with. One quantity that needs to be maintained in either situation is the new embedding level at the relevant abstraction. (For abstractions that persist, we intend this to be the new embedding level just within the scope of the abstraction.) We refer to this quantity as the index of the corresponding element of the environment and note that certain ‘consistency’ properties must hold over the list of indices of environment elements: they must form a non-increasing sequence and none of them should be greater than the new embedding level at the term into which the substitutions are being made. Now, for an abstraction that is not eliminated by a β-contraction, the index is the only information that needs to be retained in the environment: the new value of a variable reference corresponding to this abstraction can be calculated as one greater than the difference between this index and the new embedding level at the variable reference. At a concrete level, this information can be recorded through an entry of the form @l where l + 1 is the value of the index. For an abstraction that disappears due to a β-contraction, it suffices to maintain an entry of the form (s, l) where s is a term and l is the index. Such an entry signals that a variable reference that corresponds to it is to be replaced by s. However, the indices corresponding to some of the free variables in s may have to be renumbered. The particular interpretation is that s is a term that used to appear at an embedding level of l, but is now to be inserted at the (new) embedding level nl. The actual term to be substituted in is, therefore, given by the expression [[s, 0, (nl − l), nil]] in which nil represents the empty environment.

3This assumes, of course, that the variable reference is not embedded within further abstractions in t. This assumption is dispensed with by considering the old and new embedding levels at the variable reference occurrence.

The enhanced syntax for terms that we have outlined up to this point can be used to realize βcontraction through a genuinely atomic step. For example, suppose we wish to rewrite the β-redex ((λ t) s). Such a rewriting might consist of producing the term [[t, 1, 0, (s, 0) :: nil]]; an environment whose first element is et and whose remaining elements are given by e is denoted here by the expression et :: e. We refer to a term of this kind as a suspension to indicate that it encodes a substitution that has yet to be computed. In calculating the de Bruijn term that corresponds to this term, it is necessary to ‘push’ the suspended substitution over the structure of t. We have already indicated how this is to be done in the case that t is a variable reference. The case when t is a constant is also easily handled. If t is a term of the form (t_{1} t_{2}), the substitution can be distributed over t_{1} and t_{2} by generating the term ([[t_{1}, 1, 0, (s, 0) :: nil]] [[t_{2}, 1, 0, (s, 0) :: nil]]). Finally, in the case that t is of the form (λ t_{1}), the suspended substitution can be lowered into the abstraction by generating the term (λ [[t_{1}, 2, 1, @0 :: (s, 0) :: nil]]). It is interesting to contrast the treatment of abstraction here with that in Definition 3.2. We note specifically that our scheme does not renumber the variable references in the terms in the environment each time an abstraction is descended into but, rather, does this in one swoop when actual replacements are performed.

In the above discussion, we have implicitly assumed that t is a de Bruijn term in a term of the form [[t, ol, nl, e]]. However, it is possible for t to itself be a suspension. One approach to dealing with this situation is that we first expose a top-level structure for t that is akin to that of a de Bruijn term and then attempt to propagate the outer substitution over this. While this approach suffices for simulating β-reduction, it does not allow for the combination of substitution walks.

To understand this, let us reconsider the reduction of the term ((λ ((λ t_{1}) t_{2})) t_{3}) to normal form. Two β-redexes have been exhibited in this term, and the rewriting of the inner one of these can be carried out either before or after the substitution generated by rewriting the outer one has been propagated over it. Depending on the order chosen (and assuming only the minimal propagation of substitutions) we obtain one of the two terms

[[[[t_{1}, 1, 0, (t_{2}, 0) :: nil]], 1, 0, (t_{3}, 0) :: nil]] or
[[[[t_{1}, 2, 1, @0 :: (t_{3}, 0) :: nil]], 1, 0, ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: nil]].

Reducing either of these terms to a de Bruijn term based on the approach just suggested is tantamount to substituting t_{3} and (a possibly modified version of) t_{2} into t_{1} in two separate walks.

In order to support the combination of substitution walks, it is necessary to provide a means for rewriting a term of the form [[[[t, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]] into one of the form [[t, ol′, nl′, e′]]. Notice that e′ here represents a ‘merging’ of the environments e_{1} and e_{2}. In determining the exact shape of the new term, it is important to observe that e_{1} and e_{2} represent substitutions for overlapping sequences of abstractions within which t is embedded. The generation of the two suspensions can, in fact, be visualized as follows: first, a walk is made over ol_{1} abstractions immediately enclosing t, recording substitutions for each of them and leaving behind nl_{1} enclosing abstractions. Then a walk is made over ol_{2} abstractions immediately enclosing the suspension [[t_{1}, ol_{1}, nl_{1}, e_{1}]] in the new term, recording substitutions for each of them in e_{2} and leaving behind nl_{2} abstractions. Notice that the ol_{2} abstractions relevant to the second walk is coextensive with some final segment of the nl_{1} abstractions left behind after the first walk and includes additional abstractions if ol_{2} > nl_{1}.

Based on the image just evoked, it is not difficult to see what ol′ in the term representing the combination of the two suspensions, should be: these suspensions together represent a walk over ol_{1} enclosing abstractions in the case that ol_{2} ≤ nl_{1} and ol_{1} +(ol_{2} −nl_{1}) abstractions otherwise and, clearly, ol′ should be the appropriate one of these values. In a similar fashion, it can be observed that the number of abstractions eventually left behind is nl_{2} or nl_{2} + (nl_{1} − ol_{2}) depending on whether or not nl_{1} ≤ ol_{2}, and this determines the value of nl′.

Thus, only the structure of the merged environment e′ remains to be described. We denote this environment by the expression {{e_{1}, nl_{1}, ol_{2}, e_{2}}} to indicate the components of the inner and outer suspensions that determine its value. Notice that, in this expression, the ‘length’ of e_{2} is exactly ol_{2} and the indices of the elements of e_{1} are bounded by nl_{1}. Now, e′ has a length at least that of e_{1} and its length is greater than this only if ol_{2} > nl_{1}. In the case that its length is greater than ol_{1}, its elements beyond the ol_{1}-th one are exactly the last (ol_{2} − nl_{1}) elements of e_{2}. As for the first ol_{1} elements of e′, these must be the ones in e_{1} modified to take into account the substitutions encoded in e_{2}. To understand the precise shape of these elements, suppose that e_{1} has the form et :: e′_{1}. The first element of the merged environment will then be a modified form of et that we will write as ⟨⟨et, nl_{1}, ol_{2}, e_{2}⟩⟩ to indicate, once again, the components determining its value. By the abstraction height of et let us mean the difference between nl_{1} and the index of et. Let this quantity be h in the present context. A little thought reveals the following: et represents a substitution in e_{1} for an abstraction that lies within the scope of those scanned in generating the substitutions in e_{2} only if h is less than ol_{2}. Thus, only when this condition is satisfied must et be changed before inclusion in the merged environment. The nature of the change depends on the kind of element et is. If it is of the form @l, then it corresponds to an abstraction that persists after the walk that generates the suspension [[t, ol_{1}, nl_{1}, e_{1}]] and the substitution for this abstraction in the merged environment must be the one contained for it in the environment e_{2}. However, the index of this entry from e_{2} will have to be ‘normalized’ if the merged environment represents substitutions for a longer sequence of abstractions than does the outer abstraction. This is true exactly when nl_{1} is greater than ol_{2} and, in this case, the index of the entry must be increased by nl_{1} − ol_{2}. If et is an element of the form (t, l), then it represents a component of e_{1} that is obtained from rewriting a β-redex that is within the scope of the outermost ol_{2} − h abstractions considered in generating e_{2}. Removing the first h elements from e_{2} produces an environment that encodes substitutions for these abstractions in the outer suspension. Let us denote this truncated part of e_{2} by e_{h} and let the index of the first entry in it be l′. The ‘term’ component of the relevant entry in the merged environment must obviously be t modified by the substitutions in e_{h} and is, in fact, given precisely by the expression [[t, ol_{2} − h, l′, e_{h}]]. Finally, it is easily observed that the index of this entry should be l′, normalized as before in the case that nl_{1} is greater than ol_{2}.

We provide a concrete illustration of the combination of suspensions by considering the term

[[[[t_{1}, 1, 0, (t_{2}, 0) :: nil]], 1, 0, (t_{3}, 0) :: nil]]

that results through β-contraction from the term ((λ ((λ t_{1}) t_{2})) t_{3}). Based on the above discussions, this term might be denoted by the expression [[t_{1}, 2, 0, {{(t_{2}, 0) :: nil, 0, 1, (t_{3}, 0) :: nil}}]] in which the precise shape of the merged environment has to be spelled out. The length of this environment is obviously 2 and its second element must be identical to (t_{3}, 0), the first element of the outer environment. The first element is, on the other hand, given by the value of ⟨⟨(t_{2}, 0), 0, 1, (t_{3}, 0) :: nil⟩⟩. Now, the abstraction height of (t_{2}, 0) is 0 and so the term component of the value of ⟨⟨(t_{2}, 0), 0, 1, (t_{3}, 0) :: nil⟩⟩ should be [[t_{2}, 1, 0, (t_{3}, 0) :: nil]]; intuitively, the effect of the entire outer environment must be reflected on t_{2} in computing the relevant term in the merged environment. The index of this environment element must be identical to that of (t_{3}, 0). Thus, the merged suspension may be written out in detail as

[[t_{1}, 2, 0, ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: (t_{3}, 0) :: nil]].

We had observed earlier that the term ((λ ((λ t_{1}) t_{2})) t_{3}) could also have been rewritten to

[[[[t_{1}, 2, 1, @0 :: (t_{3}, 0) :: nil]], 1, 0, ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: nil]].

Merging the two environments in this term produces the same term as that obtained through the reduction sequence considered earlier, as the reader is invited to verify.

In our discussions of the combination of suspensions, we have acted as though the objective is to calculate the final merged form in one step. Adopting this viewpoint is useful in presenting the intuition governing the computation but, because of the complexity of the merging process, runs counter to our overarching goal of providing a fine-grained control over β-reduction and substitution. The actual notation that we describe corrects this situation by permitting the merging computation to be broken up into a sequence of atomic steps that can be intermingled with other computations on the term. It may be useful to “compile” a sequence of such steps into a larger step that is easy to carry out and that has practical benefits such as providing for the combination of substitution walks. A compilation of this kind can be achieved through the identification of derived or admissible rules for our notation. This matter is discussed in [29].

4.2 A modified syntax for terms

At a formal level, the main addition to the syntax of de Bruijn terms that yields our notation is that of a suspension. In presenting this category of terms, it is necessary to also explain the structure of environments and environment terms. The syntax of these various expressions is given as follows:

Definition 4.1 The categories of suspension terms, environments and environment terms, denoted by ⟨ST erm⟩, ⟨Env⟩ and ⟨ET erm⟩, are defined by the following syntax rules:

⟨ST erm⟩ ::= ⟨Cons⟩ | #⟨Index⟩ | (⟨ST erm⟩ ⟨ST erm⟩) |
(λ ⟨ST erm⟩) | [[⟨ST erm⟩, ⟨Nat⟩, ⟨Nat⟩, ⟨Env⟩]]
⟨Env⟩ ::= nil | ⟨ET erm⟩ :: ⟨Env⟩ | {{⟨Env⟩, ⟨Nat⟩, ⟨Nat⟩, ⟨Env⟩}}
⟨ET erm⟩ ::= @⟨Nat⟩ | (⟨ST erm⟩, ⟨Nat⟩) | ⟨⟨⟨ET erm⟩, ⟨Nat⟩, ⟨Nat⟩, ⟨Env⟩⟩⟩.

We assume that ⟨Cons⟩ and ⟨Index⟩ are as in Definition 3.1 and that ⟨Nat⟩ is the category of natural numbers. We refer to the expressions described by these rules collectively as suspension expressions.

The class of suspension terms obviously includes all the de Bruijn terms. By an extension of terminology, we shall refer to suspension terms of the form #i, (λ t) and (t_{1} t_{2}) as indices or variable references, abstractions and applications, respectively. The qualification ‘suspension’ applied to our terms and expressions is intended to distinguish them from similar notions in the context of the de Bruijn notation. We shall henceforth drop this qualification assuming that we are talking about terms and expressions in the new notation unless otherwise stated.

Definition 4.2 The immediate subexpression(s) of an expression x are given as follows:

(1) If x is a term, then if (a) x is (t_{1} t_{2}), these are t_{1} and t_{2}, (b) if x is (λ t), this is t, and (c) if x is [[t, ol, nl, e]], these are t and e.

(2) If x an environment, then (a) if x is et :: e, these are et and e, and (b) if x is {{e_{1}, i, j, e_{2}}}, these are e_{1} and e_{2}.

(3) If x is an environment term, then (a) if x is (t, l), then this is t, and (b) if x is ⟨⟨et, i, j, e⟩⟩, then these are et and e.

The subexpressions of an expression are the expression itself and the subexpressions of its immediate subexpressions. We sometimes use the term subterm when the subexpression in question is a term. A proper subexpression of an expression x is any subexpression distinct from x.

The syntax of environments and environment terms includes forms of expressions that are useful in capturing the merging of suspensions. In analyzing the properties of our notation it will often be convenient to exclude such expressions and consider only those environments that correspond transparently to a list of bindings. This class of expressions is identified by the following definition.

Definition 4.3 A simple expression is an expression that does not have subexpressions of the form ⟨⟨et, j, k, e⟩⟩ or {{e_{1}, j, k, e_{2}}}. If the expression in question is a term, an environment or an environment term, it may be referred to as a simple term, a simple environment or a simple environment term, respectively. Note that a simple environment e is either nil or of the form et_{1} :: et_{2} :: …:: et_{n} :: nil. In the latter case, for 1 ≤ i ≤ n, we write e[i] to denote et_{i}; observe that e[i] must itself be of the form @l or (t, l). Further, for 1 ≤ j ≤ n, we write e{j} to denote the environment et_{j} :: …:: et_{n} :: nil.

An expression of the form {{e_{1}, i, j, e_{2}}} encodes the merging of the environments e_{1} and e_{2}. This environment has at least as many elements as e_{1} has and may have more if the number of abstractions considered in generating e_{2} is greater than i, the count of the abstractions left behind after the generation of e_{1}. The following definition is, thus, an obvious formalization of a familiar notion. The symbol ^{.} used in it denotes the subtraction operation on natural numbers.

Definition 4.4 The length of an environment e, denoted by len(e), is given as follows: (a) if e is nil then len(e) = 0; (b) if e is et :: e′ then len(e) = len(e′) + 1; and (c) if e is {{e_{1}, i, j, e_{2}}} then len(e) = len(e_{1}) + (len(e_{2}) ^{.} i).

By the l-th index of an environment we intend to denote the index of the l-th element of the environment if it has such an element and the quantity 0 otherwise. We make this notion as well as that of the index of an environment term precise below. The details of this definition as they relate to expressions of the form {{e_{1}, i, j, e_{2}}} and ⟨⟨et, i, j, e⟩⟩ are a reflection of the simple environments and environment terms that they are intended to correspond to.

Definition 4.5 The index of an environment term et, denoted by ind(et), and, for each natural number l, the l-th index of an environment e, denoted by ind_{l}(e), are defined simultaneously by structural induction on expressions as follows^{4}:

(i) If et is @m then ind(et) = m + 1. (ii) If et is (t′, m) then ind(et) = m. (iii) If et is ⟨⟨et′, j, k, e⟩⟩, let m = (j ^{.} ind(et′)). Then

ind(et) = \{ \begin{matrix}ind_{m}(e) + (j ^{.} k) & if len(e) > m \\ ind(et′) & otherwise. \end{matrix}

(iv) If e is nil then ind_{l}(e) = 0.

(v) If e is et :: e′ then ind_{0}(e) = ind(et) and ind_{l+1}(e) = ind_{l}(e′). (vi) If e is {{e_{1}, j, k, e_{2}}}, let m = (j ^{.} ind_{l}(e_{1})) and l_{1} = len(e_{1}). Then

ind_{l}(e) = \{ \begin{matrix}ind_{m}(e_{2}) + (j ^{.} k) & if l < l_{1} and len(e_{2}) > m \\ ind_{l}(e_{1}) & if l < l_{1} and len(e_{2}) ≤ m \\ ind_{(l−l_{1}+j)}(e_{2}) & if l ≥ l_{1}. \end{matrix}

The index of an environment, denoted by ind(e), is ind_{0}(e).

In our informal discussions, we had noted certain constraints that are satisfied by suspension expressions when these are used in the intended fashion. These constraints will be useful in later analysis and we therefore formulate them as wellformedness conditions on our expressions. Definition 4.6 An expression is well formed if the following conditions hold of every subexpression s of the expression:

(i) If s is of the form [[t, ol, nl, e]] then len(e) = ol and ind(e) ≤ nl. (ii) If s is of the form et :: e then ind(e) ≤ ind(et). (iii) If s is of the form ⟨⟨et, j, k, e⟩⟩ then len(e) = k and ind(et) ≤ j. (iv) If s is of the form {{e_{1}, j, k, e_{2}}} then len(e_{2}) = k and ind(e_{1}) ≤ j.

The following additional constraint on environments is a consequence of the ones in Definition 4.6.

4For environment terms and environments that are well formed in the sense of Definition 4.6, the ^{.} operation in the definitions of m that appear in items (iii) and (vi) in this definition may be replaced by simple subtraction.

(β_{s}) ((λ t_{1}) t_{2}) → [[t_{1}, 1, 0, (t_{2}, 0) :: nil]]

Figure 1: The β_{s}-contraction rule schema

Lemma 4.7 Let e be a well formed environment. Then ind_{i}(e) ≥ 0. Further, for i ≥ len(e), ind_{i}(e) = 0. Finally, for any natural numbers i, j such that i < j, it is the case that ind_{i}(e) ≥ ind_{j}(e).

Proof. By an induction on the structure of e, using Definition 4.5. The details are straightforward and hence omitted.

□

We henceforth consider only well formed expressions and this qualification is assumed implicitly whenever we speak of terms, environments, environment terms or expressions.

4.3 Rules for rewriting expressions

Suspensions, as we have explained informally, are intended to provide for a laziness in the substitution operation needed in β-contraction. This understanding is now formalized through the presentation of a suitable collection of rewrite rules. We divide these rules into three categories in this presentation: the β_{s}-contraction rules that generate suspensions, the reading rules that propagate suspended substitutions over terms and the merging rules that enable the combination of suspensions. Rules in each of these categories are obtained from the schemata that appear in Figures 1–3, respectively. The following tokens, used in these schemata perhaps with subscripts or superscripts, are to be interpreted as schema variables for the indicated syntactic categories: c for constants, t for terms, et for environment terms, e for environments, i and j for positive numbers and ol, nl, l, m and n for natural numbers. The applicability of several of the rule schemata are dependent on ‘side’ conditions that are presented together with them. Further, in determining the relevant instance of the righthand side of some of the rule schemata, simple arithmetic operations may have to be performed on components of the expression matching the lefthand side. In the discussions that follow, we shall often include these arithmetic operations within the expression being written. Using this convention, rule (m1) in Figure 3 may also be written as

[[[[t_{1}, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]] → [[t_{1}, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]].

Given the syntax of expressions, this convention is really an abuse of notation. However, this abuse is harmless and unambiguous and is, in addition, extremely convenient.

Definition 4.8 The reduction relations generated by the rule schemata in Figure 1, 2 and 3 are denoted by ⊳_{β_{s}}, ⊳_{r} and ⊳_{m} respectively. The union of the relations ⊳_{r} and ⊳_{m} is denoted by ⊳_{rm}, the union of ⊳_{r} and ⊳_{β_{s}} by ⊳_{rβ_{s}} and the union of ⊳_{r}, ⊳_{m} and ⊳_{β_{s}} by ⊳_{rmβ_{s}}.

(r1) [[c, ol, nl, e]] → c,

provided c is a constant.

(r2) [[#i, 0, nl, nil]] → #j,

where j = i + nl.

(r3) [[#1, ol, nl, @l :: e]] → #j,

where j = nl − l.

(r4) [[#1, ol, nl, (t, l) :: e]] → [[t, 0, nl′, nil]],

where nl′ = nl − l.

(r5) [[#i, ol, nl, et :: e]] → [[#i′, ol′, nl, e]],

where i′ = i − 1 and ol′ = ol − 1, provided i > 1.

(r6) [[(t_{1} t_{2}), ol, nl, e]] → ([[t_{1}, ol, nl, e]] [[t_{2}, ol, nl, e]]). (r7) [[(λ t), ol, nl, e]] → (λ [[t, ol′, nl′, @nl :: e]]),

where ol′ = ol + 1 and nl′ = nl + 1.

Figure 2: Rule schemata for reading suspensions (m1) [[[[t, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]] → [[t, ol′, nl′, {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]],

where ol′ = ol_{1} + (ol_{2} ^{.} nl_{1}) and nl′ = nl_{2} + (nl_{1} ^{.} ol_{2}).

(m2) {{nil, nl, 0, nil}} → nil. (m3) {{nil, nl, ol, et :: e}} → {{nil, nl′, ol′, e}},

where nl, ol ≥ 1, nl′ = nl − 1 and ol′ = ol − 1.

(m4) {{nil, 0, ol, e}} → e. (m5) {{et :: e_{1}, nl, ol, e_{2}}} → ⟨⟨et, nl, ol, e_{2}⟩⟩ :: {{e_{1}, nl, ol, e_{2}}}. (m6) ⟨⟨et, nl, 0, nil⟩⟩ → et. (m7) ⟨⟨@n, nl, ol, @l :: e⟩⟩ → @m,

where m = l + (nl ^{.} ol), provided nl = n + 1.

(m8) ⟨⟨@n, nl, ol, (t, l) :: e⟩⟩ → (t, m),

where m = l + (nl ^{.} ol), provided nl = n + 1.

(m9) ⟨⟨(t, nl), nl, ol, et :: e⟩⟩ → ([[t, ol, l′, et :: e]], m)

where l′ = ind(et) and m = l′ + (nl ^{.} ol).

(m10) ⟨⟨et, nl, ol, et′ :: e⟩⟩ → ⟨⟨et, nl′, ol′, e⟩⟩,

where nl′ = nl − 1 and ol′ = ol − 1, provided nl ≠ ind(et). Figure 3: Rule schemata for merging suspensions

The legitimacy of the above definition is dependent on our rewrite rules producing well formed expressions from well formed expressions. The following sequence of observations culminating in Theorem 4.12 establishes this fact.

Lemma 4.9 If e_{1} is an environment and e_{1} ⊳_{rmβ_{s}}e_{2} then len(e_{1}) = len(e_{2}).

Proof. Let e_{1} be an environment. Then the following fact is easily established by induction on the structure of e_{1}: if x_{1} is a subexpression of e_{1} and x_{2} is an expression of the same type as x_{1} such that len(x_{1}) = len(x_{2}) in the case that x_{1} is an environment, and if e_{2} is obtained from e_{1} by replacing x_{1} by x_{2}, then len(e_{1}) = len(e_{2}). The desired conclusion would then follow if whenever x_{1} is an environment and x_{1} → x_{2} is an instance of one of the rule schemata in Figures 1–3, then len(x_{1}) = len(x_{2}). This can be seen to be the case by inspecting the relevant schemata, namely (m2), (m3), (m4) and (m5).

□

Lemma 4.10 Let x_{1} → x_{2} be an instance of some schema in Figures 1–3. If x_{1} is an environment term then ind(x_{1}) = ind(x_{2}). If x_{1} is an environment, then, for every natural number l, ind_{l}(x_{1}) = ind_{l}(x_{2}).

Proof. By a routine inspection of the relevant rule schemata, namely (m2)–(m10).

□

Lemma 4.11 If x_{1} is an environment term or an environment and x_{1} ⊳_{rmβ_{s}}x_{2}, then ind(x_{1}) = ind(x_{2}).

Proof. Let x_{1} and x_{2} both be environment terms or environments with the following property: if x_{1} is an environment term then ind(x_{1}) = ind(x_{2}) and if x_{1} is an environment then, for every natural number l, ind_{l}(x_{1}) = ind_{l}(x_{2}). The following facts are easily established by a simultaneous induction on the structure of expressions: If y_{1} is an environment term with x_{1} as a subexpression and y_{2} results from y_{1} by replacing x_{1} by x_{2}, then ind(y_{1}) = ind(y_{2}). If y_{1} is an environment instead and y_{2} results from it by a similar replacement, then, for every natural number l, ind_{l}(y_{1}) = ind_{l}(y_{2}). The desired conclusion now follows easily from Lemma 4.10.

□

Theorem 4.12 Let x be a well formed expression and let y be such that x⊳_{r}y, x⊳_{m}y, x⊳_{β_{s}}y, x⊳_{rm}y, x⊳_{rβ_{s}}y or x ⊳_{rmβ_{s}}y. Then y is a well formed expression.

Proof. It is sufficient to show that this property holds if x ⊳_{rmβ_{s}}y. Given Lemmas 4.9 and 4.11, this would be true if whenever x_{1} is a well formed expression and x_{1} → x_{2} is an instance of some schema in Figures 1–3, then x_{2} is well formed. This is verified by an inspection of the relevant schemata. The argument is routine in all cases except those of schemata (m1) and (m5). In the case of (m1), i.e., when the rule is

[[[[t_{1}, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]] → [[t, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]],

some care is needed in verifying that ind({{e_{1}, nl_{1}, ol_{2}, e_{2}}}) ≤ nl_{2} + (nl_{1} ^{.} ol_{2}). In the case when len(e_{1}) = 0 or len(e_{1}) > 0 and len(e_{2}) > (nl_{1} − ind_{0}(e_{1})), this follows from the fact that ind_{l}(e_{2}) ≤ nl_{2}. In the only remaining case, ind_{0}(e_{1}) ≤ (nl_{1} − len(e_{2})). Noting that in this case ind({{e_{1}, nl_{1}, ol_{2}, e_{2}}}) = ind_{0}(e_{1}) and that len(e_{2}) = ol_{2}, the desired conclusion is obtained. In the case of (m5), i.e., when the rule is

{{et :: e_{1}, j, k, e_{2}}} → ⟨⟨et, j, k, e_{2}⟩⟩ :: {{e_{1}, j, k, e_{2}}}.

we need to verify that ind(⟨⟨et, j, k, e_{2}⟩⟩) ≥ ind({{e_{1}, j, k, e_{2}}}). However, this is done easily using Lemmas 4.10 and 4.7.

□

We illustrate the rewrite rules presented in this section by considering their use on the term ((λ ((λ (λ ((#1 #2) #3))) t_{2})) t_{3}), assuming that t_{2} and t_{3} are arbitrary de Bruijn terms. The following constitutes a ⊳_{rmβ_{s}}-reduction sequence for this term:

((λ ((λ (λ ((#1 #2) #3))) t_{2})) t_{3})
⊳_{β_{s}}[[((λ (λ ((#1 #2) #3))) t_{2}), 1, 0, (t_{3}, 0) :: nil]]
⊳_{β_{s}}[[[[(λ ((#1 #2) #3)), 1, 0, (t_{2}, 0) :: nil]], 1, 0, (t_{3}, 0) :: nil]]
⊳_{m}[[(λ ((#1 #2) #3)), 2, 0, {{(t_{2}, 0) :: nil, 0, 1, (t_{3}, 0) :: nil}}]]
⊳_{m}[[(λ ((#1 #2) #3)), 2, 0, ⟨⟨(t_{2}, 0), 0, 1, (t_{3}, 0) :: nil⟩⟩ :: {{nil, 0, 1, (t_{3}, 0) :: nil}}]]
⊳_{m}[[(λ ((#1 #2) #3)), 2, 0, ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: {{nil, 0, 1, (t_{3}, 0) :: nil}}]]
⊳_{m}[[(λ ((#1 #2) #3)), 2, 0, ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: (t_{3}, 0) :: nil]].

Notice that, in producing this term, the merging of suspensions has been realized through a sequence of genuinely atomic steps. The combined environment can now be moved inside the remaining abstraction by using a reading rule to yield the term

(λ [[((#1 #2) #3), 3, 1, @0 :: ([[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0) :: (t_{3}, 0) :: nil]]).

A repeated application of reading rules transforms the last term into

(λ ((#1 [[[[t_{2}, 1, 0, (t_{3}, 0) :: nil]], 0, 1, nil]]) [[t_{3}, 0, 1, nil]])).

The application of merging rules to this term yields

(λ ((#1 [[t_{2}, 1, 1, (t_{3}, 0) :: nil]]) [[t_{3}, 0, 1, nil]])).

Depending on the particular structures of t_{2} and t_{3}, the reading rules can be applied repeatedly to this term to finally produce a de Bruijn term that results from the original term by contracting the two outermost β-redexes.

4.4 Some properties of our notation

We observe some properties of ⊳_{rm} that relate our notation to the earlier informal discussion of it.

Lemma 4.13 Let e be a simple environment. Then

[[#i, ol, nl, e]] ⊳_{rm}^{∗} \{ \begin{matrix}#(i + (nl − ol)) & if i > ol \\ #(nl − m) & if i ≤ ol and e[i] = @m \\ [[t, 0, nl − m, nil]] & if i ≤ ol and e[i] = (t, m). \end{matrix}

Proof. By an induction on ol if i > ol and on i if i ≤ ol, using the rule schemata (r2)–(r5). □

Lemma 4.14 Let e be a simple environment. If (nl − l) ≥ ol, then ⟨⟨(t, l), nl, ol, e⟩⟩⊳_{rm}^{∗}(t, l). If (nl − l) < ol, then ⟨⟨(t, l), nl, ol, e⟩⟩ ⊳_{rm}-reduces to

([[t, ol − (nl − l), ind(e[nl − l + 1]), e{nl − l + 1}]], ind(e[nl − l + 1]) + (nl ^{.} ol)).

Proof. If (nl − l) < ol, we use an induction on (nl − l) and if (nl − l) ≥ ol, we use an induction on ol. Rule schemata (m10), (m9) and (m6) are used in this proof.

□

Lemma 4.15 Let e be a simple environment. Then

⟨⟨@l, nl, ol, e⟩⟩ ⊳_{rm}^{∗} \{ \begin{matrix}@l & if (nl − l) > ol \\ @(m + (nl ^{.} ol)) & if (nl − l) ≤ ol and e[nl − l] = @m \\ (t, m + (nl ^{.} ol)) & if (nl − l) ≤ ol and e[nl − l] = (t, m). \end{matrix}

Proof. Analogous to that of Lemma 4.14, using rule schemata (m6)–(m8) and (m10).

□

Lemma 4.16 Let e_{2} be a simple environment. Then {{nil, nl, ol, e_{2}}} ⊳_{rm}-reduces to nil if nl ≥ ol and to e_{2}{nl + 1} otherwise.

Proof. By an induction on ol if nl ≥ ol and on nl if nl < ol using rule schemata (m2)–(m4). □

Suppose that e_{1} and e_{2} are simple environments and, further, that e_{1} is et_{1} :: … et_{n} :: nil. By a repeated use of rule schema (m5), the term {{e_{1}, nl, ol, e_{2}}} can be reduced to

⟨⟨et_{1}, nl, ol, e_{2}⟩⟩ :: …:: ⟨⟨et_{n}, nl, ol, e_{2}⟩⟩ :: {{nil, nl, ol, e_{2}}}.

Lemmas 4.14–4.16 show the correspondence of this environment to the desired merged environment described in Section 4.1.

The above observations are relativized to simple expressions. They extend in a natural way to arbitrary expressions once the existence of ⊳_{rm}-normal forms has been demonstrated.

5 A well founded partial order on suspension expressions

We define in this section a well founded partial ordering relation on suspension expressions that will be used primarily in showing the finiteness of all ⊳_{rm}-reduction sequences. Not surprisingly, a determining factor in this relation is a measure of the work remaining in calculating a suspended substitution. To understand the construction of a possible measure, consider a term of the form [[t, ol, nl, e]]. The substitutions encoded in this term need to be propagated over the structure of t and so it is relevant to count the complexity of this structure. Further, terms from e are embedded in a suspension before they are substituted in — this is apparent from rule schema (r4) — and the complexity of their structure should also be counted. A complication in this basic pattern is that the propagation of substitutions may create multiple copies of an environment — this happens, for instance, when rule schema (r6) is used to rewrite [[(t_{1} t_{2}), ol, nl, e]] — and yet the resulting expression should have a lower complexity. A solution to this problem is to use the maximum ‘height’ in a term over which substitutions have to be propagated as opposed to the complexity of the structure of the term.

The ideas described above underlie the measure η that we now define. The auxiliary measure μ used in defining η counts, roughly, the heights of terms. The function max on pairs of integers picks the larger of its arguments.

Definition 5.1 The measures η on expressions and μ on terms are given as follows:

Category of exp  exp  η(exp)  μ(exp)
constant  0  1
#i  0  1
term  (t_{1} t_{2})  max(η(t_{1}), η(t_{2})) max(μ(t_{1}), μ(t_{2})) + 1
(λ t)  η(t)  μ(t) + 1
[[t, ol, nl, e]]  μ(t) + η(e)  μ(t) + η(e) + 1
nil  0  —
environment  et :: e  max(η(et), η(e))  —
{{e_{1}, nl, ol, e_{2}}} η(e_{1}) + η(e_{2}) + 1  —
@l  0  —
environment term  (t, l)  μ(t)  —
⟨⟨et, nl, ol, e⟩⟩ η(et) + η(e) + 1  —

The following properties of the measures η and μ are easily observed.

Lemma 5.2 For any expression x, η(x) ≥ 0. Further, for any term t, μ(t) > η(t).

Lemma 5.3 Let x_{1} and x_{2} be expressions of the same syntactic category and such that η(x_{1}) ≥ η(x_{2}) and, if x_{1} and x_{2} are terms, μ(x_{1}) ≥ μ(x_{2}). If x results from y by the replacement of subexpression x_{1} by x_{2}, then η(y) ≥ η(x) and, if x and y are terms, μ(y) ≥ μ(x).

The measure η does not yield by itself the ordering relation we desire. The reason for this is twofold. First, there are certain rewrite rules — in particular, those obtained from the schemata (r5), (m1), (m3), (m5) and (m10) — for which the lefthand and righthand sides have the same η value. Second, replacing a subexpression by one with a lower η value does not necessarily decrease the η value of the overall expression. We deal with these problems by extending the ordering on expressions imposed by η in a way that specifically overcomes them. This is the content of Definition 5.5.

Definition 5.4 Two expressions are said to have the same top-level structure if they are both constants, variable references, abstractions, applications, or suspensions or if they are both of the forms nil, et :: e, {{e_{1}, i, j, e_{2}}}, @l, (t, l), or ⟨⟨et, i, j, e⟩⟩. If two suspension expressions that have the same top-level structure have any immediate subexpressions, then there is an obvious correspondence between these subexpressions. This correspondence will be utilized below.

Definition 5.5 Given two expressions x_{1} and x_{2}, we say x_{1} ⊐ x_{2} if either η(x_{1}) > η(x_{2}) or η(x_{1}) = η(x_{2}) and one of the following conditions hold:

(1) x_{1} is #i and x_{2} is #j where i > j.

(2) x_{1} is [[t_{1}, ol_{1}, nl_{1}, e_{1}]], x_{2} is [[t_{2}, ol_{2}, nl_{2}, e_{2}]] and η(t_{1}) > η(t_{2}).

(3) x_{1} is {{e_{1}, nl, ol, e_{2}}}, x_{2} is et :: e and x_{1} ⊐ e.

(4) x_{1} and x_{2} have the same top-level structure and also have immediate subexpressions such that each immediate subexpression of x_{1} is identical to the corresponding immediate subexpression of x_{2} except for one pair of immediate subexpressions x′_{1} of x_{1} and x′_{2} of x_{2} for which x′_{1} ⊐ x′_{2}.

(5) x_{2} is an immediate subexpression of x_{1}.

We shall write x_{1} ⊒ x_{2} to signify that x_{1} = x_{2} or x_{1} ⊐ x_{2}.

Note that ⊐ is not transitive and hence it is not a partial ordering relation.^{5} However, its transitive closure provides a well founded partial ordering relation. The following lemma will be useful in showing that this is the case.

Lemma 5.6 There is no infinite sequences of expressions x_{1}, x_{2}, …, x_{n}, … such that

x_{1} ⊐ x_{2} ⊐ ⋯ ⊐ x_{n} ⊐ · · · .

Proof. Let us use the phrase “infinite descending sequence” to denote an infinite sequence of expressions x_{1}, x_{2}, …, x_{n}, … such that x_{1} ⊐ x_{2} ⊐ ⋯ ⊐ x_{n} ⊐ · · · . We prove the following by induction on η(x_{1}): (a) there is no infinite descending sequence of expressions x_{1}, x_{2}, …, x_{n}, … such that, for i, j ≥ 1, η(x_{i}) = η(x_{j}), and (b) there is no infinite descending sequence of expressions. Note that if x ⊐ y, then η(x) ≥ η(y). Thus, (b) is an consequence of (a) and the hypothesis. It is therefore only necessary to show (a). We do this by an induction on the structure of x. The argument proceeds by considering the various possibilities for this structure.

5A partial ordering relation has been described in the literature to be one that is irreflexive and transitive [27] as well as to be one that is reflexive, transitive and antisymmetric [16]. It is the former definition that we use here.

If x is a term: x is minimal with respect to ⊐ if it is a constant. If x is #k, the descending chain is of length at most (k − 1). Suppose x is the application (s_{1} t_{1}). Any infinite descending sequence of expressions starting at x and preserving η values must be of one of two forms:

(s_{1} t_{1}), (s_{2} t_{2}), …, (s_{n} t_{n}), …,

where, for i ≥ 1, either s_{i} = s_{i+1} and t_{i} ⊐ t_{i+1} or s_{i} ⊐ s_{i+1} and t_{i} = t_{i+1}, or

(s_{1} t_{1}), (s_{2} t_{2}), …, (s_{n} t_{n}), r_{n+1}, …,

where, for 1 ≤ i < n, either s_{i} = s_{i+1} and t_{i} ⊐ t_{i+1} or s_{i} ⊐ s_{i+1} and t_{i} = t_{i+1} and r_{n+1} is either s_{n} or t_{n}. In either case, there will be an infinite descending sequence starting at either s_{1} or t_{1}. This contradicts the hypothesis since η(s_{1}), η(t_{1}) ≤ η(x) and s_{1} and t_{1} are subexpressions of x.

An argument similar to that for an application can be provided when x is an abstraction. This leave only the case of a suspension. Let x = [[s_{1}, ol_{1}, nl_{1}, e_{1}]]. We use now an additional induction on η(s_{1}). By Lemma 5.2, η(x) > η(s_{1}) and η(x) > η(e_{1}). There are, therefore, no infinite descending sequences from s_{1} or e_{1}. From this, by an argument similar to that used in the case of an application, we see that a purportedly infinite descending sequence starting from t must have an initial segment of the form

[[s_{1}, ol_{1}, nl_{1}, e_{1}]], [[s_{2}, ol_{2}, nl_{2}, e_{2}]], …, [[s_{n}, ol_{n}, nl_{n}, e_{n}]], [[s_{n+1}, ol_{n+1}, nl_{n+1}, e_{n+1}]],

where, for 1 ≤ i < n, s_{i} ⊒ s_{i+1} and e_{i} ⊒ e_{i+1}, and η(s_{n}) > η(s_{n+1}). Clearly, η(s_{1}) > η(s_{n+1}). Thus, such an initial segment cannot exist if η(s_{1}) = 0. Furthermore, even if η(s_{1}) > 0, the segment cannot be extended into an infinite descending sequence: that would entail the existence of an infinite descending sequence from [[s_{n+1}, ol_{n+1}, nl_{n+1}, e_{n+1}]], in contradiction to the hypothesis. The claim must, therefore, be true in this case as well.

If x is an environment term: x is minimal with respect to ⊐ if it is of the form @l. If x is (t′, l), then there is an infinite descending sequence from it only if there is one from t′. However, η(x) > η(t′) by Lemma 5.2 and so this is impossible by hypothesis. Finally, suppose that x is ⟨⟨et, nl, ol, e⟩⟩. There can be an infinite descending sequence from x only if there is one from either et or e. This is, again, impossible because η(x) > η(et) and η(x) > η(e).

If x is an environment: x is minimal with respect to ⊐ if it is nil. Let x = et :: e. By an argument similar to that for an application, there is an infinite descending sequence starting at x only if there is also one starting at et or e. However, this is impossible by hypothesis, because η(x) ≥ η(et), η(x) ≥ η(e), and et and e are subexpressions of x.

The remaining case, where x is of the form {{e_{1}, nl, ol, e′_{1}}}, requires a non-constructive proof. Let us assume that there are infinite descending sequences starting at x. We pick from these a sequence x = y_{1}, y_{2}, y_{3}, … that is minimal in the following sense: for each i ≥ 1, there is no infinite descending sequence of the form y_{1}, y_{2}, …, y_{i}, y′_{i+1}, … where y′_{i+1} is a subexpression of y_{i+1}. We focus now on the sequence picked. Since η(x) > η(e_{1}) and η(x) > η(e′_{1}), there are, by hypothesis, no infinite descending sequences starting at either e_{1} or e′_{1}. From this, it is easily seen that our sequence must be of the form

{{e_{1}, nl, ol, e′_{1}}}, {{e_{2}, nl, ol, e′_{2}}}, …, {{e_{n}, nl, ol, e′_{n}}}, et_{n+1} :: e_{n+1}, …,

where, for 1 ≤ i < n, e_{i} ⊒ e_{i+1}, e′_{i} ⊒ e′_{i+1} and {{e_{n}, nl, ol, e′_{n}}} ⊐ e_{n+1}. Now, this infinite descending sequence entails that there is a similar sequence starting from et_{n+1} :: e_{n+1}. By a familiar argument, this can be the case only if there is an infinite descending sequence z_{1}, z_{2}, z_{3}, …, where z_{1} is either et_{n+1} or e_{n+1}. We note that η(et_{n+1}) ≤ η(x) and that et_{n+1} is an environment term. Thus, we have already shown that the former situation is impossible. In the latter case, we can construct the infinite descending sequence

{{e_{1}, nl, ol, e′_{1}}}, {{e_{2}, nl, ol, e′_{2}}}, …, {{e_{n}, nl, ol, e′_{n}}}, z_{1}, z_{2}, z_{3}, …,

contradicting our assumption of minimality for the sequence picked initially. We conclude, therefore, that no infinite sequence could have existed to begin with.

All the cases having been considered, our claim stands verified and so the lemma must be true.

□

We now deliver the promised ordering relation on expressions.

Definition 5.7 The relation ≻ on expressions is the transitive closure of the relation ⊐.

Theorem 5.8 The relation ≻ is a well founded partial ordering relation on expressions.

Proof. We need to show that ≻ is irreflexive and, assuming that it is a partial order, is also well founded. Both requirements follow from the observation that there can be no infinite descending chains relative to ≻, a fact that is an obvious consequence of Lemma 5.6.

□

We have provided a direct proof for the fact that ≻ is well founded so as to give specific insight into the nature of this relation. However, an alternative proof can be provided by invoking Kruskal’s tree theorem [14, 26], thereby exhibiting relationships between ≻ and the notions of simplification orderings [12] and Kamin and Lévy’s extended recursive path orderings (described, for example, in [22]). Towards this end, we note that expressions of the form [[t, ol, nl, e]], {{e_{1}, nl, ol, e_{2}}} and ⟨⟨et, nl, ol, e⟩⟩ can be thought of as functions of two arguments by incorporating nl and ol into the name of the function symbol; thus, the first expression may be rendered into the expression f_{ol,nl}(t, e), the second into g_{nl,ol}(e_{1}, e_{2}) and the third into h_{nl,ol}(et, e). In a similar fashion, an environment term of the form (t, l) could be rendered into the expression k_{l}(t), i.e., a function of one argument. Finally, expressions of the form (t_{1} t_{2}) and (λ t) can be translated into app(t_{1}, t_{2}) and lam(t), respectively, :: can be interpreted as a binary function symbol and expressions of the form #k, @l and nil can be thought of as constants. Given such a translation, ≻ can be seen to be a simplification ordering. This alone does not allow us to conclude that ≻ is well founded, since the alphabet over which our terms are constructed is infinite. However, let ≈ be the relation over this alphabet that includes the identity relation and is such that (i) f_{ol,nl} ≈ f_{ol′,nl′}, g_{nl,ol} ≈ g_{nl′,ol′} and h_{nl,ol} ≈ h_{nl′,ol′} for all ol, ol′, nl, nl′, (ii) k_{l} ≈ k_{l′} and @l ≈ @l′ for all l, l′, (iii) #i ≈ #j if i ≤ j, and (iv) c ≈ c′ for all constants c and c′ of the original vocabulary. It is easily seen that ≈ is a well quasi ordering relation on the alphabet. Now, let ⪯ be the homeomorphic embedding of ≈. By Kruskal’s theorem, ⪯ is a well quasi order on expressions. We observe at this point that if x ≻ y, then it cannot be the case that x ⪯ y. From this it follows that ≻ is well founded.

6 Correctness of the reading and merging rules

The reading and merging rules propagate substitutions embodied in suspension expressions. The correctness of these rules is dependent on their ability to eventually transform any given expression in our notation into ones that are ‘substitution-free’. Further, the expression that is so produced should be independent of the order of application of the rules. In the terminology of rewrite systems, these two requirements amount to the existence of a unique ⊳_{rm}-normal form for every expression. A final requirement is that the effect of using these rules should correspond to our informal understanding of the meaning of a suspension term. We show in this section that all these properties hold of the reading and merging rules.

6.1 Existence of Normal Forms

A stronger property than the existence of a normal form for every expression holds of the ⊳_{rm} relation: every ⊳_{rm}-reduction sequence terminates. The proof of this property uses the well founded partial ordering relation defined in Section 5 in an obvious fashion.

Lemma 6.1 If l → r is an instance of one of the rule schemata in Figures 2 or 3, then η(l) ≥ η(r) and, if l and r are terms, μ(l) ≥ μ(r).

Proof. By a routine inspection of the rules in question. We omit the details, but note that in all cases except when the rule is an instance of (r5), (m1), (m3), (m5) or (m10), η(l) > η(r).

□

Lemma 6.2 If x_{1} and x_{2} are expressions such that x_{1}⊳_{rm}x_{2}, then η(x_{1}) ≥ η(x_{2}).

Proof. This follows immediately from Lemmas 5.3 and 6.1.

□

Lemma 6.3 If l → r is an instance of one of the rule schemata in Figures 2 or 3, then l ≻ r.

Proof. Immediate from the fact noted in the proof of Lemma 6.1 in all cases except when the rule is an instance of (r5), (m1), (m3), (m5) or (m10). In the cases left, the lemma is easily shown to be true using Lemma 6.1 and inspecting Definitions 5.5 and 5.7. It is necessary only to note, for (m1), that η([[t, ol, nl, e]]) ≥ μ(t) and, by Lemma 5.2, μ(t) > η(t).

□

Lemma 6.4 If x_{1}⊳_{rm}x_{2}, then x_{1} ≻ x_{2}.

Proof. By induction on the structure of x_{1}. If x_{1} → x_{2} is an instance of one of the rule schemata in Figures 2 or 3, this follows from Lemma 6.3. Otherwise x_{1} and x_{2} have the same top-level structure and, by Lemma 6.2, η(x_{1}) ≥ η(x_{2}). If η(x_{1}) > η(x_{2}), the desired conclusion follows. If η(x_{1}) = η(x_{2}), by the definition of ⊳_{rm} and by the hypothesis, there is an immediate subexpression x′_{1} of x_{1} and a corresponding immediate subexpression x′_{2} of x_{2} such that x′_{1} ≻ x′_{2} and every other immediate subexpressions of x_{1} is identical to the corresponding immediate subexpression of x_{2}. Using the definition of ≻, it follows easily that x_{1} ≻ x_{2}.

□

Theorem 6.5 The relation ⊳_{rm} is noetherian.

Proof. An obvious consequence of Lemma 6.4 and Theorem 5.8.

□

Thus, a ⊳_{rm}-normal form exists for every expression. We note that our rules eventually transform suspension terms into de Bruijn terms and that they produce simple expressions in general.

Theorem 6.6 An expression x is in ⊳_{rm}-normal form if and only if one of the following holds:

(a) x is a de Bruijn term; (b) x is an environment term of the form @l or (t, l) where t is a term in ⊳_{rm}-normal form; or (c) x is an environment of the form nil or et :: e where et and e are, respectively, an environment term and an environment in ⊳_{rm}-normal form.

Proof. An inspection of Figures 2 and 3 shows that a well formed expression that has a subexpression of the form [[t, i, j, e]], {{e_{1}, i, j, e_{2}}} or ⟨⟨et, i, j, e⟩⟩ can be rewritten by using one of the rule schemata appearing in these figures. Such an expression can therefore not be in ⊳_{rm}-normal form.

□

6.2 An associativity property for environment merging

More than two environments might be merged in the production of a ⊳_{rm}-normal form. For example, given the term [[[[[[t, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]], ol_{3}, nl_{3}, e_{3}]], the three environments e_{1}, e_{2} and e_{3} might be merged before the substitutions they represent are propagated over the structure of t. Now, such a merging can be accomplished in two different ways: we may merge e_{1} and e_{2} first and then merge the result with e_{3}, or we may merge e_{1} with the outcome of merging e_{2} and e_{3}. The environments that are produced by these different processes are given by

{{{{e_{1}, nl_{1}, ol_{2}, e_{2}}}, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}}} and {{e_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}}},

respectively. A question that is pertinent to the uniqueness of ⊳_{rm}-normal forms is whether the same environment results from either merging process.

We answer this question affirmatively below. In particular, we show that the reading and merging rules can be used to rewrite the two displayed environment expressions to a common form. At a conceptual level, our argument utilizes a partitioning into two kinds of the elements of the environments corresponding to these expressions: those obtained from transforming the elements of e_{1} to account for the substitutions encoded in e_{2} and e_{3} and those obtained from merging (relevant segments of) e_{2} and e_{3}. For each kind of element, we show that the “calculations” encoded in the two different expressions can be made to converge. A detailed consideration of cases is involved of necessity in this process. The trusting reader may wish only to note the statement of Theorem 6.12.

The following observation is needed in arguing the identity of indices of environment terms.

Lemma 6.7 ((i + (j ^{.} k)) ^{.} l) = (i ^{.} l) + (j ^{.} (k + (l ^{.} i))).

Proof. ((i + (j ^{.} k)) ^{.} l) = (i ^{.} l) + ((j ^{.} k) ^{.} (l ^{.} i)) = (i ^{.} l) + (j ^{.} (k + (l ^{.} i))).

□

Certain reduction properties for environments and environment term will also be useful.

Lemma 6.8 Let et be an environment term such that ind(et) ≤ nl. Then, for j ≥ 1,

⟨⟨et, nl + j, ol + j, et_{1} :: …:: et_{j} :: e⟩⟩⊳_{rm}^{∗}⟨⟨et, nl, ol, e⟩⟩.

Proof. By an induction on j, using rule schema (m10).

□

Lemma 6.9 Let e_{1} be a simple environment. Further, let nl and ol be natural numbers such that (nl − ind(e_{1})) ≥ ol. Then {{e_{1}, nl, ol, e_{2}}}⊳_{rm}^{∗}e_{1}.

Proof. We assume that e_{2} is also a simple environment; if not, it can be ⊳_{rm}-reduced to one. We now use an induction on len(e_{1}). If this is 0, then e_{1} = nil. Since ind(nil) = 0, nl ≥ ol and so, by Lemma 4.16, {{e_{1}, nl, ol, e_{2}}}⊳_{rm}^{∗}nil. If len(e_{1}) > 0, e_{1} is of the form et_{1} :: e′_{1}. Using rule schema (m5), {{e_{1}, nl, ol, e_{2}}}⊳_{rm}^{∗}⟨⟨et_{1}, nl, ol, e_{2}⟩⟩ :: {{e′_{1}, nl, ol, e_{2}}}. We note that ind(et_{1}) = ind(e_{1}) and, by the definition of wellformedness, ind(e′_{1}) ≤ ind(e_{1}). The lemma then follows from Lemma 6.8, rule schema (m6) and the inductive hypothesis.

□

Lemma 6.10 If e_{1} is an environment such that ind(e_{1}) ≤ nl then, for j ≥ 1, the expressions

{{e_{1}, nl + j, ol + j, et_{1} :: …:: et_{j} :: e_{2}}} and {{e_{1}, nl, ol, e_{2}}}

⊳_{rm}-reduce to a common expression for any environment e_{2}.

Proof. We assume that e_{1} and e_{2} are simple expressions: if they are not, then they can be ⊳_{rm}- reduced to such expressions and, since, by Lemma 4.11, ind(e_{1}) is preserved by such a reduction, we can then invoke the argument provided here. We now use an induction on len(e_{1}). If this is 0, using Lemma 4.16 we see that both expressions ⊳_{rm}-reduce to nil if nl ≥ ol and to e_{2}{nl + 1} otherwise. If len(e_{1}) > 0, then e_{1} is of the form et′ :: e′_{1}. Using rule schema (m5),

{{e_{1}, nl + j, ol + j, et_{1} :: …:: et_{j} :: e_{2}}}⊳_{rm}

⟨⟨et′, nl + j, ol + j, et_{1} :: …:: et_{j} :: e_{2}⟩⟩ :: {{e′_{1}, nl + j, ol + j, et_{1} :: …:: et_{j} :: e_{2}}},

and, similarly, {{e_{1}, nl, ol, e_{2}}}⊳_{rm}⟨⟨et′, nl, ol, e_{2}⟩⟩ :: {{e′_{1}, nl, ol, e_{2}}}. Noting that ind(et′) = ind(e_{1}) and ind(e′_{1}) ≤ ind(e_{1}), Lemma 6.8 and the inductive hypothesis yield the desired conclusion.

□

Suppose that e_{1} is an environment of the form et_{1} :: e′_{1}. The first element of the merger of e_{1}, e_{2} and e_{3} can then be calculated in two ways: by accounting for the effect of e_{2} on et_{1} and, subsequently, for the effect of e_{3} on the result or by accounting for the effect on et_{1} of the merger of e_{2} and e_{3}. We show below that an identical value can be produced using either method of calculation.

Lemma 6.11 Let a and b be environment terms of the form

⟨⟨⟨⟨et_{1}, nl_{1}, ol_{2}, e_{2}⟩⟩, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}⟩⟩ and ⟨⟨et_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩,

respectively. Then there is an environment term r such that a⊳_{rm}^{∗}r and b⊳_{rm}^{∗}r.

Proof. We assume, without loss of generality, that et_{1}, e_{2} and e_{3} are simple expressions and we prove the lemma by an induction on len(e_{2}).

Base Case: len(e_{2}) = 0. In this case, a is ⟨⟨⟨⟨et_{1}, nl_{1}, 0, nil⟩⟩, nl_{2} + nl_{1}, ol_{3}, e_{3}⟩⟩ and, similarly, b is ⟨⟨et_{1}, nl_{1}, ol_{3} ^{.} nl_{2}, {{nil, nl_{2}, ol_{3}, e_{3}}}⟩⟩. Using rule schema (m6), a⊳_{rm}^{∗}⟨⟨et_{1}, nl_{2} + nl_{1}, ol_{3}, e_{3}⟩⟩.

Our analysis now splits into two subcases, depending on whether or not nl_{2} ≥ ol_{3}. Suppose that nl_{2} ≥ ol_{3}. Noting that ind(et_{1}) ≤ nl_{1}, by either Lemma 4.14 or Lemma 4.15, a⊳_{rm}^{∗}et_{1}.Using Lemma 4.16 and rule schema (m6) it is easily seen that b also ⊳_{rm}-reduces to et_{1}. Suppose instead that nl_{2} < ol_{3}. Using Lemmas 6.8 and 4.16 it can be seen that both a and b ⊳_{rm}-reduce to ⟨⟨et_{1}, nl_{1}, ol_{3} ^{.} nl_{2}, e_{3}{nl_{2} + 1}⟩⟩.

Inductive Step: len(e_{2}) > 0. Let e_{2} be of the form et_{2} :: e′_{2}. We now use a further induction on nl_{1} − ind(et_{1}).

Base Case for Second Induction: nl_{1} − ind(et_{1}) = 0. We consider the cases for the structure of et_{1}:

(a) et_{1} is of the form @l. We note first that l = nl_{1} − 1. Now, our analysis splits into two further subcases, depending on whether et_{2} is of the form @m or of the form (t, m).

Suppose et_{2} is of the form @m. Using Lemma 4.15 on the one hand and rule schema (m5) on the other, it can be seen that

a⊳_{rm}^{∗}⟨⟨@(m + (nl_{1} ^{.} ol_{2})), nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}⟩⟩ and
b⊳_{rm}^{∗}⟨⟨@l, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), ⟨⟨@m, nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{e′_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩.

Now, if (nl_{2} − m) > ol_{3}, by using Lemma 4.15 repeatedly and noting that (ol_{3} ^{.} nl_{2}) = 0, it can be seen that a and b both ⊳_{rm}-reduce to @(m + (nl_{1} ^{.} ol_{2})). If, on the other hand, (nl_{2} − m) ≤ ol_{3}, we need to consider the form of e_{3}[nl_{2} − m]. In the case that this is (t, p), then, using Lemmas 4.15 and 6.7, it can be seen that both a and b ⊳_{rm}-reduce to (t, p + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})). If e_{3}[nl_{2} − m] is @p, both a and b can be shown to ⊳_{rm}-reduce to @(p + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})) by a similar argument.

Suppose instead that et_{2} is of the form (t, m). Using Lemma 4.15 and rule schema (m5) again, we see that

a⊳_{rm}^{∗}⟨⟨(t, m + (nl_{1} ^{.} ol_{2})), nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}⟩⟩ and
b⊳_{rm}^{∗}⟨⟨@l, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), ⟨⟨(t, m), nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{e′_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩.

Now, if (nl_{2} − m) ≥ ol_{3}, it can be seen that both a and b ⊳_{rm}-reduce to (t, m + (nl_{1} ^{.} ol_{2})). On the other hand, if (nl_{2} − m) < ol_{3}, it follows from Lemmas 4.14, 4.15 and 6.7 that a and b both ⊳_{rm}-reduce to

([[t, ol_{3} − (nl_{2} − m), ind(e_{3}[nl_{2} − m + 1]), e_{3}{nl_{2} − m + 1}]],

ind(e_{3}[nl_{2} − m + 1]) + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})).

(b) et_{1} is of the form (t, l). Clearly, l = nl_{1}. Let ind(et_{2}) = m. Using Lemma 4.14,

a⊳_{rm}^{∗}⟨⟨([[t, ol_{2}, m, e_{2}]], m + (nl_{1} ^{.} ol_{2})), nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}⟩⟩ (1)

Our analysis again splits into two subcases, depending on whether or not (nl_{2} − m) ≥ ol_{3}. Suppose that (nl_{2} − m) ≥ ol_{3}. Using Lemma 4.14 and the observation that

(nl_{2} + (nl_{1} ^{.} ol_{2}) − (m + (nl_{1} ^{.} ol_{2}))) = (nl_{2} − m) ≥ ol_{3},

it follows from (1) that a⊳_{rm}^{∗}([[t, ol_{2}, m, e_{2}]], m + (nl_{1} ^{.} ol_{2})). Since (nl_{2} − m) ≥ ol_{3}, (ol_{3} ^{.} nl_{2}) = 0. Hence, using Lemma 6.9 and the fact that ind(e_{2}) = ind(et_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}⊳_{rm}^{∗}e_{2}. Invoking Lemma 4.14 we can now conclude that

b = ⟨⟨(t, nl_{1}), nl_{1}, ol_{2}, {{e_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩⊳_{rm}^{∗}([[t, ol_{2}, m, e_{2}]], m + (nl_{1} ^{.} ol_{2})).

Thus, a and b both ⊳_{rm}-reduce to the same expression in this case.

In the remaining subcase, (nl_{2} − m) < ol_{3}. Lemma 4.14 used in conjunction with (1) yields

a⊳_{rm}^{∗}([[[[t, ol_{2}, m, e_{2}]], ol_{3} − (nl_{2} − m), ind(e_{3}[nl_{2} − m + 1]), e_{3}{nl_{2} − m + 1}]],

ind(e_{3}[nl_{2} − m + 1]) + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})).

Using rule schema (m1), we get from this that

a⊳_{rm}^{∗}([[t, ol_{2} + ((ol_{3} − (nl_{2} − m)) ^{.} m),
ind(e_{3}[nl_{2} − m + 1]) + (m ^{.} (ol_{3} − (nl_{2} − m))),
{{e_{2}, m, ol_{3} − (nl_{2} − m), e_{3}{nl_{2} − m + 1}}}]],
ind(e_{3}[nl_{2} − m + 1]) + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})).

Now, since (nl_{2} − m) < ol_{3}, it must be the case that

((ol_{3} − (nl_{2} − m)) ^{.} m) = (ol_{3} ^{.} nl_{2}) and (m ^{.} (ol_{3} − (nl_{2} − m))) = (nl_{2} ^{.} ol_{3}).

These identities can be used to simplify the expression a is shown to ⊳_{rm}-reduce to. In particular,

a⊳_{rm}^{∗}([[t, ol_{2} + (ol_{3} ^{.} nl_{2}), ind(e_{3}[nl_{2} − m + 1]) + (nl_{2} ^{.} ol_{3}),
{{e_{2}, m, ol_{3} − (nl_{2} − m), e_{3}{nl_{2} − m + 1}}}]], (2)
ind(e_{3}[nl_{2} − m + 1]) + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3})).

With regard to b, using rule schema (m5) we first observe that it ⊳_{rm}-reduces to

⟨⟨(t, nl_{1}), nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), ⟨⟨et_{2}, nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{e′_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩.

Since ind(et_{2}) = m, it follows from either Lemma 4.14 or Lemma 4.15 that ⟨⟨et_{2}, nl_{2}, ol_{3}, e_{3}⟩⟩ ⊳_{rm}- reduces to an environment term whose index is ind(e_{3}[nl_{2} − m + 1]) + (nl_{2} ^{.} ol_{3}). By Lemma 4.11, indices are preserved under reduction. Hence, using Lemma 4.14,

b⊳_{rm}^{∗}([[t, ol_{2} + (ol_{3} ^{.} nl_{2}), ind(e_{3}[nl_{2} − m + 1]) + (nl_{2} ^{.} ol_{3}),
⟨⟨et_{2}, nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{e′_{2}, nl_{2}, ol_{3}, e_{3}}}]], (3)
ind(e_{3}[nl_{2} − m + 1]) + (nl_{2} ^{.} ol_{3}) + (nl_{1} ^{.} (ol_{2} + (ol_{3} ^{.} nl_{2})))).

Lemma 6.7 can be used to show that the indices of the environment terms in (2) and (3) are identical. Further inspecting these expressions, we see that they would ⊳_{rm}-reduce to a common expression if {{e_{2}, m, ol_{3} − (nl_{2} − m), e_{3}{nl_{2} − m + 1}}} and ⟨⟨et_{2}, nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{e′_{2}, nl_{2}, ol_{3}, e_{3}}} ⊳_{rm}-reduce to one. Using the rule schema (m5) and invoking Lemmas 6.8 and 6.10 after recalling that ind(e′_{2}) ≤ ind(et_{2}) = m and (nl_{2} − m) < ol_{3}, this can be seen to be the case.

Inductive Step for the Second Induction: nl_{1} − ind(et_{1}) > 0. In this case, by using rule schema (m10) on a and rule schemata (m5) and (m10) on b, we observe that

a⊳_{rm}^{∗}⟨⟨⟨⟨et_{1}, nl_{1} − 1, ol_{2} − 1, e′_{2}⟩⟩, nl_{2} + ((nl_{1} − 1) ^{.} (ol_{2} − 1)), ol_{3}, e_{3}⟩⟩, and

b⊳_{rm}^{∗}⟨⟨et_{1}, nl_{1} − 1, (ol_{2} − 1) + (ol_{3} ^{.} nl_{2}), {{e′_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩.

Obviously, len(e′_{2}) < len(e_{2}). The inductive hypothesis can now be invoked to conclude that a and b ⊳_{rm}-reduce to a common expression.

□

Theorem 6.12 Let a and b be environments of the form

{{{{e_{1}, nl_{1}, ol_{2}, e_{2}}}, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}}} and {{e_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}}},

respectively. Then there is an environment r such that a⊳_{rm}^{∗}r and b⊳_{rm}^{∗}r.

Proof. By induction on len(e_{1}), assuming that e_{1}, e_{2} and e_{3} are simple expressions. Base Case: len(e_{1}) = 0, i.e., e_{1} = nil. Our analysis splits into two subcases.

(a) nl_{1} < ol_{2}. Using Lemma 4.16 and noting that, in this subcase, (nl_{1} ^{.} ol_{2}) = 0, we see that

a⊳_{rm}^{∗}{{e_{2}{nl_{1} + 1}, nl_{2}, ol_{3}, e_{3}}}.

Using rule schema (m5) repeatedly, it follows that a ⊳_{rm}-reduces to

⟨⟨e_{2}[nl_{1} + 1], nl_{2}, ol_{3}, e_{3}⟩⟩ :: …:: ⟨⟨e_{2}[ol_{2}], nl_{2}, ol_{3}, e_{3}⟩⟩ :: {{nil, nl_{2}, ol_{3}, e_{3}}}. (4)

Now, if nl_{1} < ol_{2}, then nl_{1} < (ol_{2} + (ol_{3} ^{.} nl_{2})). Using this fact together with rule schema (m5) and Lemma 4.16, it can be seen that b also ⊳_{rm}-reduces to the expression shown in (4).

(b) nl_{1} ≥ ol_{2}. By adopting arguments similar to those in subcase (a), it can be seen that a and b both ⊳_{rm}-reduce to e_{3}{nl_{2} + (nl_{1} ^{.} ol_{2}) + 1} if ol_{3} > (nl_{2} + (nl_{1} ^{.} ol_{2})) and to nil if ol_{3} ≤ (nl_{2} + (nl_{1} ^{.} ol_{2})).

Inductive Step: len(e_{1}) > 0. Let e_{1} = et_{1} :: e′_{1}. Using rule schema (m5), we see that a and b ⊳_{rm}-reduce to

⟨⟨⟨⟨et_{1}, nl_{1}, ol_{2}, e_{2}⟩⟩, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}⟩⟩ :: {{{{e′_{1}, nl_{1}, ol_{2}, e_{2}}}, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}}}, and

⟨⟨et_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}⟩⟩ :: {{e′_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{1}, nl_{2}, ol_{3}, e_{3}}}}},

respectively. Lemma 6.11 and the hypothesis can be used to show that the latter two expressions ⊳_{rm}-reduce to a common expression.

□

6.3 Uniqueness of normal forms

We now show the uniqueness of ⊳_{rm}-normal forms. By virtue of Proposition 2.1, this property would hold if ⊳_{rm} is a confluent reduction relation. Further, in light of Proposition 2.2 and Theorem 6.5 it actually suffices to show that ⊳_{rm} is locally confluent.

Theorem 6.13 The relation ⊳_{rm} is locally confluent.

Proof. By Theorem 2.4, it is enough to show that, for each conflict pair ⟨r_{1}, r_{2}⟩ of the rule schemata in Figures 2 and 3, there is some expression s such that r_{1}⊳_{rm}^{∗}s and r_{2}⊳_{rm}^{∗}s. To do this, we need to consider the various nontrivial overlaps between the rule schemata in question. Examining these schemata, we see that such overlaps occur only between (m1) and each rule schema in Figure 2, (m1) and (m1) and (m2) and (m4). The last case is dealt with easily: the overlap occurs over the expression {{nil, 0, 0, nil}} and the two expressions in the corresponding conflict pair are identical, both being nil. We consider the conflict pairs relative to the remaining overlaps in turn below to complete our argument. In each case, we refer to the expression that constitutes the nontrivial overlap as t and to the terms in the conflict pair as r_{1} and r_{2} respectively. We will assume that subexpressions that are common to t, r_{1} and r_{2} are simple ones for, if not, they can always be reduced to such a form at the outset.

Overlap between (m1) and (r1). Let t be the term [[[[c, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]]. It is easily seen that r_{1} and r_{2} both ⊳_{rm}-reduce to c.

Overlap between (m1) and (r2). Let t be the term [[[[#i, 0, nl_{1}, nil]], ol_{2}, nl_{2}, e_{2}]]. Then r_{1} is the term [[#i, ol_{2} ^{.} nl_{1}, nl_{2} + (nl_{1} ^{.} ol_{2}), {{nil, nl_{1}, ol_{2}, e_{2}}}]] and r_{2} is the term [[#(i + nl_{1}), ol_{2}, nl_{2}, e_{2}]]. We distinguish three cases:

nl_{1} ≥ ol_{2}. From Lemmas 4.16 and 4.13 and noting that (nl_{1} ^{.} ol_{2}) = (nl_{1}−ol_{2}) and (ol_{2} ^{.} nl_{1}) = 0, we conclude that r_{1} and r_{2} both ⊳_{rm}-reduce to #(i + nl_{2} + (nl_{1} − ol_{2})).

nl_{1} < ol_{2} and i > (ol_{2} − nl_{1}). A similar argument to that above can be provided to show that r_{1} and r_{2} both ⊳_{rm}-reduce to #(i + nl_{2} − (ol_{2} − nl_{1})).

nl_{1} < ol_{2} and i ≤ (ol_{2} − nl_{1}). The common expression in this case depends on the form of e_{2}[i + nl_{1}]. If this is @m, then r_{1} and r_{2} are both ⊳_{rm}-reduce to #(nl_{2} − m) and if this is (t, m), then r_{1} and r_{2} both similarly reduce to [[t, 0, nl_{2} − m, nil]].

Overlap between (m1) and (r3). Let t be the term [[[[#1, ol_{1}, nl_{1}, @l :: e_{1}]], ol_{2}, nl_{2}, e_{2}]]. Then r_{1} and r_{2} are the terms

[[#1, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{@l :: e_{1}, nl_{1}, ol_{2}, e_{2}}}]] and [[#(nl_{1} − l), ol_{2}, nl_{2}, e_{2}]],

respectively. We distinguish two cases:

(nl_{1} − l) > ol_{2}. Note first that (nl_{1} ^{.} ol_{2}) = (nl_{1} − ol_{2}). Using rule schema (m5), Lemmas 4.13 and 4.15, it then follows that r_{1} and r_{2} both ⊳_{rm}-reduce to #(nl_{1} − l + nl_{2} − ol_{2}).

(nl_{1}−l) ≤ ol_{2}. A similar argument to that above shows that r_{1} and r_{2} ⊳_{rm}-reduce to #(nl_{2}−m) if e_{2}[nl_{1} − l] = @m and to [[t, 0, nl_{2} − m, nil]] if e_{2}[nl_{1} − l] = (t, m).

Overlap between (m1) and (r4). Let t be the term [[[[#1, ol_{1}, nl_{1}, (t, l) :: e_{1}]], ol_{2}, nl_{2}, e_{2}]]. Then r_{1} is the term

[[#1, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{(t, l) :: e_{1}, nl_{1}, ol_{2}, e_{2}}}]]

and r_{2} is the term [[[[t, 0, nl_{1} − l, nil]], ol_{2}, nl_{2}, e_{2}]]. Using rule schema (m1), r_{2} may be rewritten to

[[t, ol_{2} ^{.} (nl_{1} − l), nl_{2} + ((nl_{1} − l) ^{.} ol_{2}), {{nil, nl_{1} − l, ol_{2}, e_{2}}}]].

From this and from using Lemmas 4.13 and 4.16, it is easily seen that in the case that (nl_{1}−l) ≥ ol_{2}, r_{1} and r_{2} both ⊳_{rm}-reduce to [[t, 0, nl_{2} + (nl_{1} − l) − ol_{2}, nil]]. In the case that (nl_{1} − l) < ol_{2}, using Lemma 4.16 we see first that r_{2} ⊳_{rm}-reduces to [[t, ol_{2} − (nl_{1} − l), nl_{2}, e_{2}{nl_{1} − l + 1}]]. We wish to show that r_{1} also ⊳_{rm}-reduces to this term. Towards this end, letting ind(e_{2}{nl_{1} − l + 1}) = m and using rule schema (m5) and Lemma 4.14, we observe that

{{(t, l) :: e_{1}, nl_{1}, ol_{2}, e_{2}}}⊳_{rm}^{∗}
([[t, ol_{2} − (nl_{1} − l), m, e_{2}{nl_{1} − l + 1}]], m + (nl_{1} ^{.} ol_{2})) :: {{e_{1}, nl_{1}, ol_{2}, e_{2}}}.

But then, by rule schema (r4), r_{1}⊳_{rm}^{∗}[[[[t, ol_{2} − (nl_{1} − l), m, e_{2}{nl_{1} − l + 1}]], 0, nl_{2} − m, nil]]. Using rule schema (m1) and invoking Lemma 6.9, it follows from this that r_{1} ⊳_{rm}-reduces to the term [[t, ol_{2} − (nl_{1} − l), nl_{2}, e_{2}{nl_{1} − l + 1}]] as desired.

Overlap between (m1) and (r5). Let t be the term [[[[#k, ol_{1}, nl_{1}, et :: e_{1}]], ol_{2}, nl_{2}, e_{2}]] where k > 1. Then r_{1} is the term

[[#k, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{et :: e_{1}, nl_{1}, ol_{2}, e_{2}}}]]

and r_{2} is the term [[[[#(k − 1), ol_{1} − 1, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]]. It is easily seen that both r_{1} and r_{2} ⊳_{rm}-reduce to [[#(k − 1), ol_{1} + (ol_{2} ^{.} nl_{1}) − 1, nl_{2} + (nl_{1} ^{.} ol_{2}), {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]].

Overlap between (m1) and (r6). Let t be the term [[[[(t_{1} t_{2}), ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]]. Then r_{1} is the term [[(t_{1} t_{2}), ol′, nl′, {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]] where ol′ = (ol_{1}+(ol_{2} ^{.} nl_{1})) and nl′ = (nl_{2}+(nl_{1} ^{.} ol_{2})), and r_{2} is of the term [[([[t_{1}, ol_{1}, nl_{1}, e_{1}]] [[t_{2}, ol_{1}, nl_{1}, e_{1}]]), ol_{2}, nl_{2}, e_{2}]]. It is easily seen that r_{1} and r_{2} both ⊳_{rm}-reduce to ([[t_{1}, ol′, nl′, {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]] [[t_{2}, ol′, nl′, {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]]).

Overlap between (m1) and (r7). Let t be the term [[[[(λ t′), ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]]. Then r_{1} is the term [[(λ t′), ol′, nl′, {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]] where ol′ = (ol_{1} +(ol_{2} ^{.} nl_{1})) and nl′ = (nl_{2} +(nl_{1} ^{.} ol_{2})), and r_{2} is the term [[(λ [[t′, ol_{1} + 1, nl_{1} + 1, @nl_{1} :: e_{1}]]), ol_{2}, nl_{2}, e_{2}]]. Now, using rule schema (r7), we see that r_{1}⊳_{rm}^{∗}(λ [[t′, ol′ + 1, nl′ + 1, @nl′ :: {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]]). Similarly, using rule schemata (r7), (m1) and (m5) and invoking Lemma 4.15, we observe that

r_{2}⊳_{rm}^{∗}(λ [[t′, ol′ + 1, nl′ + 1, @nl′ :: {{e_{1}, nl_{1} + 1, ol_{2} + 1, @nl_{2} :: e_{2}}}]]).

Noting that ind(e_{1}) ≤ nl_{1} and using Lemma 6.10, we conclude that {{e_{1}, nl_{1} + 1, ol_{2} + 1, @nl_{2} :: e_{2}}} and {{e_{1}, nl_{1}, ol_{2}, e_{2}}} ⊳_{rm}-reduce to a common expression. But then so too do r_{1} and r_{2}.

Overlap between (m1) and (m1). Let t be the term [[[[[[t_{1}, ol_{1}, nl_{1}, e_{1}]], ol_{2}, nl_{2}, e_{2}]], ol_{3}, nl_{3}, e_{3}]]. Then r_{1} and r_{2} are the terms

[[[[t_{1}, ol_{1}, nl_{1}, e_{1}]], ol_{2} + (ol_{3} ^{.} nl_{2}), nl_{3} + (nl_{2} ^{.} ol_{3}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}]] and
[[[[t_{1}, ol_{1} + (ol_{2} ^{.} nl_{1}), nl_{2} + (nl_{1} ^{.} ol_{2}), {{e_{1}, nl_{1}, ol_{2}, e_{2}}}]], ol_{3}, nl_{3}, e_{3}]].

Using rule schema (m1), we see that

r_{1}⊳_{rm}^{∗}[[t_{1}, ol′, nl′, {{e_{1}, nl_{1}, ol_{2} + (ol_{3} ^{.} nl_{2}), {{e_{2}, nl_{2}, ol_{3}, e_{3}}}}}]] (5)

where ol′ = ol_{1} + ((ol_{2} + (ol_{3} ^{.} nl_{2})) ^{.} nl_{1}) and nl′ = nl_{3} + (nl_{2} ^{.} ol_{3}) + (nl_{1} ^{.} (ol_{2} + (ol_{3} ^{.} nl_{2}))). Similarly,

r_{2}⊳_{rm}^{∗}[[t_{1}, ol′′, nl′′, {{{{e_{1}, nl_{1}, ol_{2}, e_{2}}}, nl_{2} + (nl_{1} ^{.} ol_{2}), ol_{3}, e_{3}}}]] (6)

where ol′′ = ol_{1} + (ol_{2} ^{.} nl_{1}) + (ol_{3} ^{.} (nl_{2} + (nl_{1} ^{.} ol_{2}))) and nl′′ = nl_{3} + ((nl_{2} + (nl_{1} ^{.} ol_{2})) ^{.} ol_{3}). Using Theorem 6.12 in conjunction with (5) and (6), we see that r_{1} and r_{2} would ⊳_{rm}-reduce to a common expression if ol′ = ol′′ and nl′ = nl′′. But this can be seen to be the case using Lemma 6.7.

All the necessary cases having been considered, the proof of the theorem is complete.

□

As noted already, the following theorem is an immediate consequence:

Theorem 6.14 The reduction relation ⊳_{rm} is confluent.

By virtue of Theorem 6.5, Proposition 2.1 and Theorem 6.14, every suspension expression has a unique ⊳_{rm}-normal form. It will be convenient to have a special notation for such forms.

Definition 6.15 The ⊳_{rm}-normal form of an expression t is denoted by |t|.

6.4 Correspondence to de Bruijn terms

A suspension term is intended to encapsulate a de Bruijn term with a ‘pending’ substitution. We use ⊳_{rm}-normal forms and the meta-notation for substitution described in Section 3 to show that this encapsulation is as expected.

Theorem 6.16 Let t = [[t′, ol, nl, e]] be a term and let e′ = |e|. Then |t| = S(|t′|; s_{1}, s_{2}, s_{3}, …) where

s_{i} = \{ \begin{matrix}#(i − ol + nl) & if i > ol \\ #(nl − m) & if i ≤ ol and e′[i] = @m \\ |[[t_{i}, 0, nl − m, nil]]| & if i ≤ ol and e′[i] = (t_{i}, m). \end{matrix}

Proof. By induction on t with respect to the well founded ordering relation ≻. The argument is based on a consideration of the structure of the term t′.

If t′ is a constant: In this case |t| and S(|t′|; s_{1}, s_{2}, s_{3}, …) are both identical to t′.

If t′ is a variable reference: Noting the confluence of ⊳_{rm}, the desired conclusion in this case follows easily from Lemma 4.13.

If t′ is an application: Let t′ = (r_{1} r_{2}). Now t⊳_{rm}([[r_{1}, ol, nl, e]] [[r_{2}, ol, nl, e]]) by virtue of rule schema (r6) and, therefore, by the confluence of ⊳_{rm},

|t| = (|[[r_{1}, ol, nl, e]]| |[[r_{2}, ol, nl, e]]|). (7)

Additionally, using Lemma 6.4, t ≻ ([[r_{1}, ol, nl, e]] [[r_{2}, ol, nl, e]]). Now, for i = 1 and i = 2,

([[r_{1}, ol, nl, e]] [[r_{2}, ol, nl, e]]) ≻ [[r_{i}, ol, nl, e]]

and, by transitivity, t ≻ [[r_{i}, ol, nl, e]]. Invoking the hypothesis of the induction,

|[[r_{i}, ol, nl, e]]| = S(|r_{i}|; s_{1}, s_{2}, s_{3}, …).

From this fact used in conjunction with (7) and Definition 3.2, it follows that

|t| = S((|r_{1}| |r_{2}|); s_{1}, s_{2}, s_{3}, …).

Noting finally that |t′| = (|r_{1}| |r_{2}|), the theorem is seen to hold in this case.

If t′ is an abstraction: Let t′ = (λ r). Then |t| = (λ |[[r, ol + 1, nl + 1, @nl :: e]]|) by virtue of rule schema (r7) and the confluence of ⊳_{rm}. By an argument similar to that employed in the case when t′ is an application, we also see that t ≻ [[r, ol + 1, nl + 1, @nl :: e]]. Using the inductive hypothesis, |[[r, ol + 1, nl + 1, @nl :: e]]| = S(|r|; s′_{1}, s′_{2}, s′_{3}, …) where

s′_{i} = \{ \begin{matrix}#1 & if i = 1 \\ #(i − ol + nl) & if i > ol + 1 \\ #(nl + 1 − m) & if 1 < i ≤ (ol + 1) and e′[i − 1] = @m \\ |[[s, 0, nl + 1 − m, nil]]| & if 1 < i ≤ (ol + 1) and e′[i − 1] = (s, m) \end{matrix} (8)

Noting now that |t′| = (λ |r|) and using Definition 3.2, we see that

S(|t′|; s_{1}, s_{2}, s_{3}, …) = (λ S(|r|; #1, S(s_{1}; #2, #3, #4, …), S(s_{2}; #2, #3, #4, …), …)). (9)

From inspecting (8) and (9), it follows that the theorem would hold in this case if, for i ≥ 1, s′_{i+1} = S(s_{i}; #2, #3, #4, …). We show that this must be true by considering several subcases.

(a) i > ol. In this case both terms are #(i + 1 − ol + nl) and hence are identical.

(b) 1 < i ≤ ol and e′[i] is of the form @m. Now both terms are identical to #(nl + 1 − m).

(c) 1 < i ≤ ol and e′[i] is of the form (s, m). Here we need to show that

|[[s, 0, nl + 1 − m, nil]]| = S(|[[s, 0, nl − m, nil]]|; #2, #3, #4, …). (10)

By virtue of rule schemata (m1) and (m2), [[[[s, 0, nl − m, nil]], 0, 1, nil]]⊳_{rm}^{∗}[[s, 0, nl + 1 − m, nil]] and, thus,

|[[s, 0, nl + 1 − m, nil]]| = |[[[[s, 0, nl − m, nil]], 0, 1, nil]]|. (11)

Referring to Definition 5.1, we claim that η(t) > η([[[[s, 0, nl − m, nil]], 0, 1, nil]]). This is seen by noting the following: η([[[[s, 0, nl − m, nil]], 0, 1, nil]]) = μ(s) + 1, η(t) ≥ μ(s) + μ((λ r)), and μ((λ r)) ≥ 2. It thus follows that t ≻ [[[[s, 0, nl − m, nil]], 0, 1, nil]]. The inductive hypothesis can therefore be applied to the term on the right of (11). Doing so easily yields (10).

If t′ is a suspension: Using Lemma 6.4 and noting that t′ ≠ |t′|, t ≻ [[|t′|, ol, nl, e]]. Invoking the inductive hypothesis with respect to the latter term and noting that ||t′|| = |t′|, the theorem follows in this case.

□

7 Correspondence to beta reduction on de Bruijn terms

The β_{s}-contraction rule schema is intended to be a counterpart in the context of suspension terms of the β-contraction rule schema for de Bruijn terms. Towards stating the correspondence precisely, we note first that the reading and merging rules partition the collection of suspension terms into equivalence classes based on the notion of “having the same ⊳_{rm}-normal form.” The intention, then, is that the β_{s}-contraction rule schema have the same effect relative to the equivalence classes of suspension terms as does the β-contraction rule schema relative to de Bruijn terms.

We show in this section that the desired correspondence does, in fact, hold. In one direction, this amounts to a relative completeness result for the β_{s}-contraction rule schema.

Theorem 7.1 Let t be a de Bruijn term and let t⊳_{β}s. Then there is a suspension term r such that t⊳_{β_{s}}r and |r| = s.

Proof. By an induction on the structure of t.

Base Case: t is the β-redex rewritten by a β-contraction rule. Let t = ((λ t_{1}) t_{2}). By definition,

s = S(t_{1}; t_{2}, #1, #2, …). (1)

Now let r = [[t_{1}, 1, 0, (t_{2}, 0) :: nil]]. Obviously t⊳_{β_{s}}r and, using Theorem 6.16,

|r| = S(|t_{1}|; |[[t_{2}, 0, 0, nil]]|, #1, #2, …). (2)

Noting that t_{1} is a de Bruijn term, it follows that |t_{1}| = t_{1}. Using Theorem 6.16 and noting that t_{2} is a de Bruijn term, we similarly see that |[[t_{2}, 0, 0, nil]]| = t_{2}. Thus, the terms on the righthand sides of (1) and (2) are identical, i.e., |r| = s.

Inductive Step: t is an abstraction or an application. The argument in both cases is similar so we consider only the first case. Let t = (λ t_{1}). Then s = (λ s_{1}) where s_{1} is such that t_{1}⊳_{β}s_{1}. By hypothesis, there is a suspension term r_{1} such that t_{1}⊳_{β_{s}}r_{1} and |r_{1}| = s_{1}. Letting r = (λ r_{1}), we see that the requirements of the theorem are satisfied: |r| = (λ |r_{1}|) = (λ s_{1}) = s and obviously t⊳_{β_{s}}r.

□

In showing the correspondence in the converse direction, it will be necessary to consider the use of the β-contraction rule schema on suspension expressions.

Definition 7.2 The relation on suspension expressions generated by the β-contraction rule schema is denoted by ⊳_{β′}.

Note that the restriction of ⊳_{β′} to suspension terms in ⊳_{rm}-normal form is identical to ⊳_{β}. The following lemmas, whose proofs are obvious, ensure that ⊳_{β′} preserves the lengths of environments and the indices of environments and environment terms. Thus, ⊳_{β′} is well defined in that it relates only well formed suspension expressions.

Lemma 7.3 Let et_{1} be an environment term and let et_{2} be such that et_{1}⊳_{β′}^{∗}et_{2}. Then the following holds: if et_{1} is @m, then et_{2} is @m; if et_{1} is of the form (t_{1}, m), then et_{2} is of the form (t_{2}, m). Further, if et_{1} is in ⊳_{rm}-normal form, then, in the latter case, t_{1}⊳_{β}^{∗}t_{2}.

Lemma 7.4 Let e_{1} be an environment and let e_{2} be such that e_{1}⊳_{β′}^{∗}e_{2}. Then len(e_{1}) = len(e_{2}). Further, if len(e_{1}) > 0, then the following holds for 1 ≤ i ≤ len(e_{1}): if e_{1}[i] is @m, then e_{2}[i] is @m; if e_{1}[i] is of the form (t_{1}, m), then e_{2}[i] is of the form (t_{2}, m). Finally, if e_{1} is in ⊳_{rm}-normal form, then, in the latter case, t_{1}⊳_{β}^{∗}t_{2}.

A strengthened form of Theorem 7.1 can be obtained from it by an easy structural induction.

Lemma 7.5 Let x and y be suspension expressions such that x⊳_{β′}y. Then there is a suspension expression z such that x⊳_{β_{s}}z and |z| = |y|.

Theorem 7.1 shows that each application of the β-contraction rule schema on de Bruijn terms can be mimicked by a single use of the β_{s}-contraction rule schema and some reading and merging steps. Mimicking an application of the β_{s}-contraction rule schema may, on the other hand, require several or no uses of the β-contraction rule schema on the underlying de Bruijn term. This reflects the fact that the use of environments may foster a sharing of β-redexes or, alternatively, may result in temporarily maintaining β-redexes that would not appear in the term if the substitution were carried out completely. The important point to note, however, is that a β_{s}-contraction can be simulated by a sequence of β-contractions, i.e., the β_{s}-contraction schema is relatively sound. This follows from Theorem 7.9 whose proof uses the intervening lemmas.

Lemma 7.6 Let t_{1} be a term in ⊳_{rm}-normal form and let t_{2} be such that t_{1}⊳_{β′}^{∗}t_{2}. Further, let e_{1} be an environment in ⊳_{rm}-normal form and let e_{2} be such that e_{1}⊳_{β′}^{∗}e_{2}. Then

|[[t_{1}, ol, nl, e_{1}]]|⊳_{β}^{∗}|[[t_{2}, ol, nl, e_{2}]]|.

Proof. We note, using Theorem 6.16 and Corollary 3.6, that if s_{1} and s_{2} are de Bruijn terms such that s_{1}⊳_{β}^{∗}s_{2}, then |[[s_{1}, 0, n, nil]]|⊳_{β}^{∗}|[[s_{2}, 0, n, nil]]|. Using Theorem 6.16 and Lemma 7.4 in conjunction with the assumptions of the lemma, it follows easily that

|[[t_{1}, ol, nl, e_{1}]]| = S(u_{0}; u_{1}, u_{2}, u_{3}, …) and |[[t_{2}, ol, nl, e_{2}]]| = S(v_{0}; v_{1}, v_{2}, v_{3}, …),

where, for i ≥ 0, u_{i}⊳_{β}^{∗}v_{i}. But then, by Corollary 3.6, |[[t_{1}, ol, nl, e_{1}]]|⊳_{β}^{∗}|[[t_{2}, ol, nl, e_{2}]]|.

□

Lemma 7.7 Let et_{1} be an environment term in ⊳_{rm}-normal form and let et_{2} be an expression such that et_{1}⊳_{β′}^{∗}et_{2}. Further, let e_{1} be an environment in ⊳_{rm}-normal form and let e_{2} be such that e_{1}⊳_{β′}^{∗}e_{2}. Then |⟨⟨et_{1}, nl, ol, e_{1}⟩⟩|⊳_{β′}^{∗}|⟨⟨et_{2}, nl, ol, e_{2}⟩⟩|.

Proof. An easy consequence of Lemmas 7.3, 7.4, 4.14, 4.15 and 7.6.

□

Lemma 7.8 Let e_{1} and e_{2} be environments in ⊳_{rm}-normal form and let e′_{1} and e′_{2} be such that e_{1}⊳_{β′}^{∗}e′_{1} and e_{2}⊳_{β′}^{∗}e′_{2}. Then |{{e_{1}, nl, ol, e_{2}}}|⊳_{β′}^{∗}|{{e′_{1}, nl, ol, e′_{2}}}|.

Proof. By induction on len(e_{1}). If len(e_{1}) = 0, then e_{1} and e′_{1} are both nil. Then, by Lemma 4.16, either |{{e_{1}, nl, ol, e_{2}}}| and |{{e′_{1}, nl, ol, e′_{2}}}| are both nil, or, for some k, |{{e_{1}, nl, ol, e_{2}}}| = e_{2}{k} and |{{e′_{1}, nl, ol, e′_{2}}}| = e′_{2}{k}. The desired conclusion follows easily in either case. If len(e_{1}) > 0, let e_{1} = et_{1} :: t_{1}, noting that et_{1} and t_{1} must be in ⊳_{rm}-normal form. Then e′_{1} must be of the form et′_{1} :: t′_{1} where et_{1}⊳_{β′}^{∗}et′_{1} and t_{1}⊳_{β′}^{∗}t′_{1}. Using rule schema (m5),

|{{e_{1}, nl, ol, e_{2}}}| = |⟨⟨et_{1}, nl, ol, e_{2}⟩⟩| :: |{{t_{1}, nl, ol, e_{2}}}|, and
|{{e′_{1}, nl, ol, e′_{2}}}| = |⟨⟨et′_{1}, nl, ol, e′_{2}⟩⟩| :: |{{t′_{1}, nl, ol, e′_{2}}}|.

The lemma now follows from Lemma 7.7 and the inductive hypothesis.

□

Theorem 7.9 Let t and s be suspension expressions such that t⊳_{β_{s}}s. Then |t|⊳_{β′}^{∗}|s|.

Proof. By induction on t with respect to ≻. Note that t cannot be a constant, a variable reference, nil or of the form @m. The remaining cases for the structure of t are considered below.

If t is an application: There are two possibilities: t is the redex rewritten by a β_{s}-contraction rule or some proper subterm of t is rewritten. We analyze each possibility separately.

In the first subcase, t has the form ((λ t_{1}) t_{2}). We note first that |t| = ((λ |t_{1}|) |t_{2}|). Further,

s = [[t_{1}, 1, 0, (t_{2}, 0) :: nil]].

Using Theorem 6.16, it can be seen that |s| = S(|t_{1}|; |t_{2}|, #1, #2, …), i.e., that |t|⊳_{β′}|s|.

In the second subcase, t is of the form (t_{1} t_{2}). We assume, without loss of generality, that the redex rewritten is a subterm of t_{1}. Then s = (s_{1} t_{2}), where t_{1}⊳_{β_{s}}s_{1}. Since t_{1} is a proper subterm of t, t ≻ t_{1}. Thus, by hypothesis, |t_{1}|⊳_{β′}^{∗}|s_{1}|. The theorem now follows from noting that |t| = (|t_{1}| |t_{2}|) and |s| = (|s_{1}| |t_{2}|).

If t is an abstraction or has the form (t′, m) or et :: e: An inductive argument similar to that in the second subcase of an application can be used in each of these cases.

If t is a suspension: Let t = [[r, ol, nl, e]]. Then s = [[r′, ol, nl, e′]] where r⊳_{β_{s}}r′ and e = e′ or r = r′ and e⊳_{β_{s}}e′. In either case, using the fact that r and e are proper subexpressions of t and hence t ≻ r and t ≻ e, |r|⊳_{β′}^{∗}|r′| and |e|⊳_{β′}^{∗}|e′|. Now, by confluence of ⊳_{rm}^{∗},

|[[r, ol, nl, e]]| = |[[|r|, ol, nl, |e|]]| and |[[r′, ol, nl, e′]]| = |[[|r′|, ol, nl, |e′|]]|.

Using Lemma 7.6, it follows from this that |[[r, ol, nl, e]]|⊳_{β}^{∗}|[[r′, ol, nl, e′]]|. Recalling that ⊳_{β′} and ⊳_{β} are identical on de Bruijn terms, the theorem is seen to be true.

If t has the form ⟨⟨et, nl, ol, e⟩⟩: By an argument similar to that used for a suspension, s must be of the form ⟨⟨et′, ol, nl, e′⟩⟩ where |et|⊳_{β′}^{∗}|et′| and |e|⊳_{β′}^{∗}|e′|. Noting that

|⟨⟨et, nl, ol, e⟩⟩| = |⟨⟨|et|, nl, ol, |e|⟩⟩| and |⟨⟨et′, nl, ol, e′⟩⟩| = |⟨⟨|et′|, nl, ol, |e′|⟩⟩|,

and using Lemma 7.7, the theorem follows in this case.

If t is of the form {{e_{1}, nl, ol, e_{2}}}: Once again, s must be of the form {{e′_{1}, nl, ol, e′_{2}}} where, |e_{1}|⊳_{β′}^{∗}|e′_{1}| and |e_{2}|⊳_{β′}^{∗}|e′_{2}|. We note further that

|{{e_{1}, nl, ol, e_{2}}}| = |{{|e_{1}|, nl, ol, |e_{2}|}}| and |{{e′_{1}, nl, ol, e′_{2}}}| = |{{|e′_{1}|, nl, ol, |e′_{2}|}}|.

The theorem now follows from Lemma 7.8.

All possibilities for the structure of t having been considered, the proof of the theorem is complete.

□

The results of this section can be used to conclude that the rule schemata in Figures 1–3 correctly implement β-reduction. The following theorem is a generalization of this observation.

Theorem 7.10

(a) If x and y are suspension expressions such that x⊳_{rmβ_{s}}^{∗}y, then |x|⊳_{β′}^{∗}|y|.

(b) If x and y are suspension expressions in ⊳_{rm}-normal form such that x⊳_{β′}^{∗}y then x⊳_{rmβ_{s}}^{∗}y.

Proof. (a) By an induction on the length of the reduction sequence by which x⊳_{rmβ_{s}}^{∗}y. If the first rule used is an instance of the β_{s}-contraction rule schema, we use Theorem 7.9. Otherwise we use Theorem 6.14 to note that the ⊳_{rm}-normal form is preserved.

(b) An induction on the length of the reduction sequence by which x⊳_{β′}^{∗}y. It is only necessary to show that if x⊳_{β′}y, then x⊳_{rmβ_{s}}^{∗}y. This follows from Lemma 7.5 by noting that y must be in ⊳_{rm}-normal form and using the fact that ⊳_{rm} is confluent and noetherian.

□

8 Some reduction properties of the overall system

The results of the previous two sections can be used to observe some properties of reduction within our system of rewrite rules. The most important of these properties is that of confluence.

Theorem 8.1 The reduction relation ⊳_{rmβ_{s}} is confluent.

Proof. This is evident from the diagram below.

tr  s  u ⊳_{rmβ_{s}}^{∗} ⊳_{β′}^{∗} ⊳_{β′}^{∗} (1) (2)  (5) (4) ⊳{∗ \atop rmβ_{s}}  ⊳_{rmβ_{s}}^{∗} ⊳_{rm}^{∗}  ⊳_{rm}^{∗} (3) ⊳_{rm}^{∗} ⊳_{rmβ_{s}}^{∗}  ⊳_{β′}^{∗}  ⊳_{β′}^{∗} |t| |r|  |s|

In diagrams of this kind, dashed arrows signify the existence of reductions given by the labels on the arrows, depending on the reductions depicted by the solid arrows. The dashed arrows in the faces (1) and (2) are justified by Theorem 7.10, the remaining dashed arrows in face (3) are justified by a straightforward extension of Proposition 3.7 to ⊳_{β′}^{∗} and the last two dashed arrows in faces (4) and (5) are justified by Theorem 7.10.

□

Another observation concerns the redundancy in certain contexts of the merging rules. These rules have efficiency advantages in that they support the combination of substitution walks over terms. However, they are not essential to the implementation of β-reduction.

Lemma 8.2 Let t be a de Bruijn term and let t⊳_{β}s. Then t⊳_{rβ_{s}}^{∗}s.

Proof. By Theorem 7.1, t⊳_{β_{s}}r where |r| = s. We observe now that t, being a de Bruijn term, is a simple expression. From this it follows that r is also a simple expression. It is also easily seen that (a) a reading rule must be applicable to any simple expression that is not in ⊳_{rm}-normal form, and (b) applying such a rule produces another simple expression. Thus r⊳_{r}^{∗}|r|, i.e., r⊳_{r}^{∗}s. This implies that t⊳_{rβ_{s}}^{∗}s.

□

Theorem 8.3 Let t and s be de Bruijn terms such that t⊳_{β}^{∗}s. Then t⊳_{rβ_{s}}^{∗}s.

Proof. By induction on the length of the ⊳_{β}-reduction sequence, using Lemma 8.2.

□

It is not possible to eliminate uses of merging rules from all ⊳_{rmβ_{s}}-reduction sequences. However, when starting from a simple expression, merging rules are redundant if the objective is to produce an expression in the same ⊳_{rm}^{∗} equivalence class as the final expression that was originally produced.

Theorem 8.4 Let t be a simple expression and let s be such that t⊳_{rmβ_{s}}^{∗}s. Then there is an expression u such that t⊳_{rβ_{s}}^{∗}u and s⊳_{rm}^{∗}u.

Proof. Letting u be the expression |s|, the lemma is evident from the diagram below.

t  s |t|  |s| ⊳_{rmβ_{s}}^{∗} ⊳_{r}^{∗}  ⊳_{rm}^{∗} ⊳_{β′}^{∗} ⊳{∗ \atop rβ_{s}} (2) (1)

The dashed arrows in the face labelled (1) in this figure are justified by Theorem 7.10; the label ⊳_{r}^{∗} on the arrow from t to |t| is warranted by the observation (made in the proof of Lemma 8.2) that a simple expression can be reduced to its ⊳_{rm}-normal form by using only reading rules. The remaining dashed arrow in face (2) is justified by Theorem 8.3.

□

The arguments in this section use the ‘projection’ of suspension terms onto de Bruijn terms that follows from the results of Sections 6 and 7 in showing properties of our system. This method of argument is similar in spirit to the one referred to as the interpretation method in [17] and used in [17] and [39] in proving confluence properties of a combinator calculus. We use this method again in [29].

9 Conclusion

We have described in this paper a notation for the terms in a lambda calculus and a system for rewriting expressions in this notation. Our notation is based on the de Bruijn representation of lambda terms but embellishes this so as to allow for the representation of a term with a pending substitution. We have shown that the rewrite rules in our system can simulate the operation of β-reduction on terms in the usual representation and can, in a sense, be simulated by this operation. We have used this observation in establishing the confluence of our overall system. The notation developed here has several useful features. It is closely related to the usual representation of lambda terms and can in fact replace the latter notation even in contexts where intensions of terms have to be manipulated. The use of de Bruijn’s scheme for representing variables obviates α-conversion in comparing terms. Our rewrite system provides a fine-grained control over the substitution process involved in β-contraction, and thus can be used as the basis for a wide variety of reduction procedures. Furthermore, the ability our notation provides to suspend substitutions leads to efficiency advantages in the implementation of β-reduction: substitution and reduction walks over the structures of terms can be combined and substitutions can be delayed in some cases till such a point that it becomes unnecessary to perform them. Finally, our notation permits components of a β-contraction step to be intermingled with other operations such as those involved in unifying lambda terms. This ability is of practical relevance and is, in fact, being used to advantage in an implementation of the language λProlog.

While the specific notation presented here is new, the ideas embedded in it have received previous and parallel developments. A central idea in our notation is the use of environments in representing suspended substitutions. This idea is an old one within the implementation of βreduction to the extent that it is difficult to pinpoint a source for it. The category of terms that we have referred to as suspensions in this paper are what are usually called closures. However, most of these proposals have differed from that presented in this paper in two important respects. First, the idea of closures has been used largely as an implementation device and an attempt has not been made to reflect it into the notation or to describe a calculus that takes the resulting notation seriously. Second, in most cases the focus has been on generating weak head normal forms, i.e., the percolation of substitutions or the rewriting of β-redexes under abstractions is not considered. The latter assumption has the effect of greatly simplifying the kind of notation required, as the reader may well verify. Moreover, as discussed already, this is not an assumption that is valid in all contexts.

In our knowledge, the first serious consideration of a notation and a calculus that incorporate a fine-grained control over substitutions appears in the work of P-L. Curien [10, 11]. In this work, a categorical combinatory logic called CCL is described. The language underlying this logic is not the lambda calculus, but bears a close relationship to it: there is a translation from the (pure) lambda calculus augmented with the pairing function to CCL and vice versa that preserves the intended equality relation in the two calculi. Unfortunately, the rewrite rules that constitute CCL are not confluent [17]; this result might be anticipated from the fact that the lambda calculus with the pairing function is not confluent [24]. However, a subset of CCL terms can be exhibited on which the rewrite rules are confluent [17, 39]. Moreover, a subclass of this class of terms is isomorphic to the class of lambda calculus terms and this isomorphism can be extended to one between a subset of CCL rules and β-reduction [17]. An interesting characteristic of this subsystem is that it permits ‘β-contraction’ to be factored into the generation of a substitution and the subsequent percolation of this substitution in much the spirit of the system described in this paper.

While the CCL system has several desirable features, its relationship to the lambda calculus is a somewhat complex one. More recently, the general ideas embedded in CCL have been used in conjunction with notations that are more directly based on the lambda calculus in [1] and [13]. The resulting systems are very similar to the one described here and our work, in fact, represents a concurrent and independent development of these general ideas.^{6} At a level of detail, the notations in [1] and [13] are practically indistinguishable. However, they differ from our notation in two respects. The first of these is in the manner in which variables are represented. In our notation, these are represented directly by de Bruijn numbers. In contrast, in the other notations, variables are represented essentially as environment transforming operators that strip off parts of environments. The latter representation has the virtue of parsimony: a smaller vocabulary suffices and the rules that serve to combine environments can also be used to determine the bindings for variables. However, there are also advantages to our representation. As one example, the comparison of terms containing variables becomes somewhat easier. At a different level, there is a differentiation of rules in our system based on purpose, and this makes it easier to identify simpler, but yet complete, subsystems. Thus, as observed in Theorem 8.3, the rules for merging environments can be omitted from our system without losing the ability to simulate β-reduction. A similar observation cannot be made about the other systems being discussed.^{7}

The second respect in which our notation differs from the ones in [1] and [13] is the manner in which it encodes the adjustment that must be made to indices of terms in an environment. In our notation, this is not maintained explicitly but is obtained from the difference between the embedding level of the term that has to be substituted into and an embedding level recorded with the term in the environment. Thus, consider a suspension term of the form [[t_{1}, 1, nl, (t_{2}, nl′) :: nil]]. This represents a term that is to be obtained by substituting t_{2} for the first free variable in t_{1} (and modifying the indices for the other free variables). However, the indices for the free variables in t_{2} must be ‘bumped up’ by (nl − nl′) before this substitution is made. In the other systems, the needed increment to the indices of free variables is maintained explicitly with the term in the environment. Thus, the suspension term shown above would be represented, as it were, as [[t_{1}, 1, nl, (t_{2}, (nl − nl′)) :: nil]]; actually, the old and new embedding levels are needed in this term only for determining the adjustment to the free variables in t_{1} with indices greater than the old embedding level, and devices for representing environments encapsulating such an adjustment simplify the actual notation used. The representation used in [1] and [13] have the benefit of parsimony: no special syntax is required for environment terms and rules that are used for manipulating terms can also be used for manipulating terms in the environment. Notice, however, that the rule for moving substitutions under abstractions becomes more complex in that every term in the environment is now affected. Thus, from a term of the form [[(λ t_{1}), 1, nl, (t_{2}, (nl − nl′)) :: nil]], this rule must produce a term that looks something like (λ [[t_{1}, 2, nl + 1, @1 :: (t_{2}, nl − nl′ + 1) :: nil]]). In contrast, using our representation, this rule is required only to add a ‘dummy’ element to the environment and to make a local change to the embedding levels of the overall term. On a balance, the trade-offs in the two approaches appear to be even in the context of the overall rewriting systems. However, our representation seems to have an advantage if a simpler rewriting system, such as that obtained by eliminating the merging rules, is used.

6The ideas described here are an outgrowth of those contained in [32]. The present exposition of these ideas has, however, been influenced by [1].

7We note in this context that the remark in [1] to the effect that the rule for merging environments (labelled (Clos)) can be eliminated is incorrect. However, as pointed out to us by P.-L. Curien, restricted versions of this rule and of other environment manipulating rules suffice from the perspective of simulating β-reduction in the notation presented there.

In a different direction, the general idea of delaying substitutions appears to have been anticipated by de Bruijn in [3] and [4]. In the latter paper, de Bruijn actually presents a notation for lambda terms that includes mappings for transforming variable indices within terms. The specific notation presented in [4] is quite cumbersome and, in addition, does not include any mechanisms for encoding the substitution operation needed for β-contraction. However, a special form of the general substitution operation that suffices for β-contraction has been described in the literature, and using laziness in its implementation results in a notation close to the one presented here. In particular, β-contraction is described in [17] by means of a binary function σ_{n} and a unary function τ_{i}^{n} on terms. These functions perform the following tasks: σ_{n}(t_{1}, t_{2}) produces a term from t_{1} by decreasing the indices for the (n + 1)-st and later free variables by 1 and replacing the n-th free variable by t_{2} after the indices for the free variables in t_{2} have been ‘bumped up’ by n; τ_{i}^{n}(t) produces the term that results from t by raising the indices for the i-th and later free variables in it by n. A similar set of functions is described by Staples in [38]. Our notion of a suspension collapses these two functions into a common form and captures the effect of evaluating them in a delayed fashion. It is interesting to note that two indices ol and nl are needed in a term of the form [[t, ol, nl, e]] to achieve this objective; an attempt to use only one index was made in [33] but could not be carried out to completion. We also observe that our notation actually generalizes the mentioned functions by allowing for environments that represent multiple non-dummy substitutions that are to be performed simultaneously.

The notation studied in this paper is intended to have practical utility. Our particular desire is that this notation serve as a substrate upon which coarser-grained representations for lambda terms may be developed that are eventually used in actual implementations. We explore this issue in a companion paper [29]. One particular refinement we consider is that of eliminating the merging rules. These rules have a practical advantage in that it is only through them that substitution walks over the structure of a term can be combined. However, implementing these rules in their full generality can be cumbersome. Our approach to this is to capture some of their effects through auxiliary rules. The resulting rewrite system permits us to restrict our attention to only simple expressions. Another refinement consists of adding annotations to terms that determine whether or not they can be affected by substitutions generated by external β-contractions. We then use the refined notation to describe manipulations to lambda terms and to prove properties of such manipulations. It is this work that directly underlies the implementation that is being developed for λProlog [30].

Acknowledgements

We are grateful to P.-L. Curien for comments on an earlier version of this paper. Suggestions from reviewers have lead to significant improvements in presentation. John Hannan and an reviewer of an early presentation of the ideas here (in [32]) made us aware of related research. Stimulus was provided to the first author by Mike O’Donnell and his students by their participation in an exposition of these ideas in Spring 1991. Work on this paper has been supported by NSF grants CCR-89-05825 and CCR-92-08465.

References

[1] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

[2] L. Aiello and G. Prini. An efficient interpreter for the lambda-calculus. The Journal of Computer and System Sciences, 23:383–425, 1981.

[3] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5):381–392, 1972.

[4] N. de Bruijn. Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Math., 40:348–356, 1978.

[5] N. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 579–606. Academic Press, 1980.

[6] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[7] R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

[8] Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2/3):95–120, February/March 1988.

[9] G. Cousineau, P-L. Curien, and M. Mauny. The categorical abstract machine. The Science of Programming, 8(2):173–202, 1987.

[10] P-L. Curien. Categorical combinators. Information and Control, 69:188–254, 1986.

[11] P-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986.

[12] Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.

[13] John Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 1–15. ACM Press, January 1990.

[14] Jean H. Gallier. What’s so special about Kruskal’s theorem and the ordinal Γ_{0}? A survey of some results in proof theory. Annals of Pure and Applied Logic, 53:199–260, 1991.

[15] Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[16] Paul R. Halmos. Naive Set Theory. D. Van Nostrand Company, Inc., 1960.

[17] Thérèse Hardin. Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCL. Theoretical Computer Science, 65:291–342, 1989.

[18] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.

[19] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinatory Logic and Lambda Calculus. Cambridge University Press, 1986.

[20] Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

[21] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, October 1980.

[22] Gérard Huet. Formal structures for computation and deduction. Unpublished course notes, Carnegie Mellon University, 1986.

[23] Gérard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31–55, 1978.

[24] J.W. Klop. Combinatory Reduction Systems. Mathematisch Centrum, Amsterdam, 1980.

[25] Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.

[26] J.B. Kruskal. Well-quasi-ordering, the tree theorem and Vázsonyi’s conjecture. Trans. Amer. Math. Soc., 95:210–225, 1960.

[27] Azriel Levy. Basic Set Theory. Springer-Verlag, 1979.

[28] Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379–388, San Francisco, September 1987.

[29] Gopalan Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Technical Report TR-96-13, Department of Computer Science, University of Chicago, May 1996. To appear in Journal of Functional and Logic Programming.

[30] Gopalan Nadathur, Bharat Jayaraman, and Debra Sue Wilson. Implementation considerations for higher-order features in logic programming. Technical Report CS-1993-16, Department of Computer Science, Duke University, June 1993.

[31] Gopalan Nadathur and Dale Miller. An overview of λProlog. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810– 827, Seattle, Washington, August 1988. MIT Press.

[32] Gopalan Nadathur and Debra Sue Wilson. A representation of lambda terms suitable for operations on their intensions. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 341–348. ACM Press, 1990.

[33] Michael J. O’Donnell and Robert I. Strandh. Towards a fully parallel implementation of the lambda calculus. Technical Report JHU/EECS-84/13, Johns Hopkins University, 1984.

[34] Lawrence C. Paulson. The representation of logics in higher-order logic. Technical Report Number 113, University of Cambridge, Computer Laboratory, August 1987.

[35] Lawrence C. Paulson. The foundations of a generic theorem prover. Technical Report Number 130, University of Cambridge, Computer Laboratory, March 1988.

[36] Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, June 1989. IEEE Computer Society Press.

[37] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.

[38] John Staples. A new technique for analysing parameter passing, applied to the lambda calculus. Australian Computer Science Communications, 3(1):201–210, May 1981.

[39] Hirofumi Yokouchi. Church-Rosser Theorem for a rewriting system on categorical combinators. Theoretical Computer Science, 65:271–290, 1989.