Orthogonal Higher-Order Rewrite Systems are Confluent^{∗}

Tobias Nipkow^{†} TU München^{‡}

1 Introduction

Two important aspects of computation are reduction, hence the current infatuation with termrewriting systems (TRSs), and abstraction, hence the study of λ-calculus. In his groundbreaking thesis, Klop [10] combined both areas in the framework of combinatory reduction systems (CRSs) and lifted many results from the λ-calculus to the CRS-level. More recently [15], we proposed a different although related approach to rewriting with abstractions, higher-order rewrite systems (HRSs). HRSs use the simply-typed λ-calculus as a meta-language for the description of reductions of terms with bound variables. Furthermore we showed that the wellknown critical pairs can be extended to this setting, thus proving that confluence of terminating HRSs is decidable.

This paper is a second step towards a general theory of higher-order rewrite systems. It considers the complementary case, when there are no critical pairs and all rules are left-linear (no free variable appears twice on the left-hand side). Such systems are usually called orthogonal. The main result of this paper is that all orthogonal HRSs are confluent, irrespective of their termination. To a specialist in the field this will probably not come as a surprise because the same result holds for TRSs and CRSs, and the latter are close to HRSs. There are also many partial results in this direction [18, 1]. Hence the contribution of the paper is not so much the result itself but the combination of the following points:

• The demonstration that simply-typed λ-calculus is an ideal meta-language for rewriting terms with bound variables, because of its simple definition and because of the many powerful results available, especially w.r.t. reduction and unification.

• The simple proof, the idea of which goes back to Aczel [1] (in a more restrictive framework) and is similar to the classical confluence proof due to Tait and Martin-Löf.

• The meta-theorem itself.

This consolidates an emerging theory of higher-order rewrite systems based on simply-typed λ-calculus.

In the larger scheme of things it confirms the view that simply-typed λ-calculus is not a computational mechanism but a language for representing formulae. The above results apply directly to programming languages (like λProlog [14]) and theorem provers (like Isabelle [17]) whose meta-language is simply-typed λ-calculus. In fact, Amy Felty has implemented some aspects of HRSs in λProlog [6].

∗Appeared in Proceedings of Typed Lambda Calculi and Applications, 1993, Springer LNCS 664.

†Research supported by ESPRIT BRA 6453, Types, and WG 6028, CCL.

‡Address: Institut für Informatik, Technische Universität München, Postfach 20 24 20, W-8000 München 2, Germany. Email: Tobias.Nipkow@Informatik.TU-Muenchen.De

2 Preliminaries

The standard theory of the simply-typed λ-calculus is assumed (see [8, 15]). In particular we use the following terminology and notation.

T is the set of all types and the letter τ ranges over T . T is generated from a set of base types using the function space constructor →. Instead of τ_{1} → ⋯ → τ_{n} → τ we write \overline{τ_{n}} → τ. The latter form is used only if τ is a base type.

Terms are generated from a set of typed variables V = ⋃_{τ∈T} V_{τ} and a set of typed constants C = ⋃_{τ∈T} C_{τ}, where V_{τ} ∩ V_{τ′} = C_{τ} ∩ C_{τ′} = {} if τ ≠ τ′. Bound variables are denoted by x, y and z, free variables by upper-case letters (F, G, …), and constants by c. Atoms are constants or variables and are denoted by a. Terms are denoted by l, r, s, t, and u. In the sequel all λ-terms are assumed to be simply typed. We write t : τ if t is of type τ.

Instead of λx_{1} … λx_{n}.s we write λx_{1}, …, x_{n}.s or just λ\overline{x_{n}}.s, where the x_{i} are assumed to be distinct. Similarly we write t(u_{1}, …, u_{n}) or just t(\overline{u_{n}}) instead of (… (t u_{1}) …)u_{n}. The free variables occurring in a term s are denoted by fv(s).

The β-normal form of a term s is denoted by s↓_{β}. Let t be in β-normal form. Then t is of the form λ\overline{x_{n}}.a(\overline{u_{m}}), where a is called the head of t and the u_{i} are in β-normal form. The η-expanded form of t is defined by

t↑^{η} = λ\overline{x_{n+k}}.a(\overline{u_{m}}↑^{η}, x_{n+1}↑^{η}, …, x_{n+k}↑^{η})

where t : \overline{τ_{n+k}} → τ and x_{n+1}, …, x_{n+k} ∉ fv(\overline{u_{m}}). Instead of t↓_{β}↑^{η} we also write t↕_{β}^{η}. A term t is in long βη-normal form if t↕_{β}^{η} = t.

Most of the time, except at intermediate stages of a computation, we are working with long βη-normal forms. Hence their explicit inductive definition may be helpful:

\begin{matrix}a : \overline{τ_{n}} → τ & t_{1} : τ_{1} & … & t_{n} : τ_{n} \\ a(t_{1}, …, t_{n}) : τ \end{matrix}  \begin{matrix}x : τ & t : τ′ \\ λx.t : τ → τ′ \end{matrix}

Terms can also be viewed as trees. Subterms can be numbered by so-called positions which are the paths from the root to the subterm in Dewey decimal notation. Details can be found in [9, 4]. We just briefly review the notation. The positions in a term t are denoted by Pos(t) ⊆ IN^{∗}. The letters p and q stand for positions. The root position is ε, the empty sequence. Two positions p and q are appended by juxtaposing them: pq. Given p ∈ Pos(t), t/p is the subterm of t at position p; t[u]_{p} is t with t/p replaced by u.

Abstractions and applications yield the following trees:

\begin{matrix}λx & . \\ | & / \ \\ s & s t \end{matrix}

Hence positions in λ-terms are sequences over {1, 2}. Note that the bound variable in an abstraction is not a separate subterm and can therefore not be accessed by the s/p notation.

In order to simplify the treatment of λ-terms we use Barendregt’s [2, p.26] variable conventions: α-equivalent terms are identified and free and bound variables in terms are kept disjoint. We cannot enforce this convention completely. For example in the congruence rule s = t ⇒ λx.s = λx.t the variable x occurs both free and bound. Similarly the names of bound variables matter if the notation t/p is used.

Substitutions are finite mappings from variables to terms of the same type. Substitutions are denoted by θ and σ. If θ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} we define Dom(θ) = {x_{1}, …, x_{n}} and Cod(θ) = {t_{1}, …, t_{n}}. A renaming ρ is an injective substitution with Cod(ρ) ⊂ V and Dom(ρ) ∩ Cod(ρ) = {}. Renamings are always denoted by ρ.

Using the above convention about free and bound variables, tθ, the application of a substitution to a term, can be defined naïvely:

cθ = c
F θ = θF
(s t)θ = (sθ tθ)
(λx.s)θ = λx.(sθ)

Composition of substitutions is juxtaposition: t(θ_{1}θ_{2}) = (tθ_{1})θ_{2}. Application and normalization are postfix operators which associate to the left: sθ_{1}θ_{2}↓_{β} = ((sθ_{1})θ_{2})↓_{β}. In particular sθ↓_{β} is the β-normal form of sθ.

We say that two terms s and t unify if there is a substitution θ such that sθ and tθ are βη-equivalent. It is well-known that this holds iff sθ↕_{β}^{η} = tθ↕_{β}^{η}.

A relation → has the diamond property if y_{0} ← x → y_{1} implies that there is a z such that y_{0} → z ← y_{1}; → is confluent if →^{∗} has the diamond property. The following lemma is folklore:

Lemma 2.1 If → ⊆ > ⊆ →^{∗} and > has the diamond property, then → is confluent.

3 Orthogonal Higher-Order Rewrite Systems

Higher-Order Rewrite Systems (HRSs) were introduced in [15]. Let us briefly review their definition and some basic results.

Definition 3.1 A term t in β-normal form is called a (higher-order) pattern if every free occurrence of a variable F is in a subterm F (\overline{u_{n}}) of t such that \overline{u_{n}}↓_{η} is a list of distinct bound variables.

Examples of higher-order patterns are λx.c(x), X, λx.F (λz.x(z)), and λx, y.F (y, x), examples of non-patterns are F (c), λx.F (x, x) and λx.F (F (x)).

The following crucial result about unification of patterns is due to Dale Miller [12]:

Theorem 3.2 It is decidable whether two patterns are unifiable; if they are unifiable, a most general unifier can be computed.

This result ensures both the computability of the rewrite relation defined by an HRS and of critical pairs. Nipkow [15] presented a simplified form of Miller’s unification algorithm which is further developed towards a practical implementation in [16].

Definition 3.3 A rewrite rule is a pair l → r such that l is a pattern but not η-equivalent to a free variable, l and r are long βη-normal forms of the same base type, and fv(l) ⊇ fv(r). A Higher-Order Rewrite System (for short: HRS) is a set of rewrite rules. The letter R always denotes an HRS. An HRS R induces a relation →_{R} on terms in long βη-normal form:

s →_{R} t ⇔ ∃(l → r) ∈ R, p ∈ Pos(s), θ. s/p = lθ↓_{β} ∧ t = s[rθ↓_{β}]_{p}.

A few explanatory remarks are in order, especially since this definition differs from the one in [15]:

• In contrast to [15] we have defined →_{R} only on long βη-normal forms and require the rules to be in that form as well. This is no restriction — every term has a unique long βη-normal form — and simplifies some technicalities.

• The term t = s[rθ↓_{β}]_{p} is again in long βη-normal form provided s, r and the elements of Cod(θ) are: t is in β-normal form because rθ↓_{β} is of base type; t is in η-expanded form because rθ↓_{β} is.

• The rewriting mechanism works just as well for rules not of base type. However, rewriting and equality fail to coincide in that case (see Theorem 3.5 below) and both the proof of the critical pair lemma [15] and of confluence of orthogonal HRSs rely on this restriction. Hence it is easier to build it into the framework.

• Because all rules in R are of base type and left-hand sides must not be η-equivalent to free variables, each left-hand side is of the form c(\overline{l_{n}}).

• The subterm s/p may contain free variables which used to be bound in s but whose binding λs are above p. Felty [6] uses a slightly different but equivalent definition of →_{R} which makes this fact explicit.

Example 3.4 The syntax of the pure lambda-calculus involves just the type term of terms and two constants for abstraction and application:

abs : (term → term) → term
app : term → term → term

The rewrite rules are:

\begin{aligned}beta : & app(abs(λx.F (x)), S) & → & F (S) \\ eta : & abs(λx.app(S, x)) & → & S \end{aligned}

Note how the use of meta-level application and abstraction removes the need for a substitution operator (in the beta-rule) and side conditions (in the eta-rule).

In the sequel it will be convenient to have an inference-rule based formulation of rewriting:

{(l → r) ∈ R \atop lθ↓_{β} →_{R} rθ↓_{β}}  {s →_{R} t \atop a(\overline{s_{m}}, s, \overline{u_{n}}) →_{R} a(\overline{s_{m}}, t, \overline{u_{n}})}  {s →_{R} t \atop λx.s →_{R} λx.t}

where a is an atom of type \overline{τ_{m+1+n}} → τ. The two definitions of →_{R} are equivalent.

Every HRS R also induces an equality =_{R} obtained by combining all instances of the rules in R with reflexivity, symmetry, transitivity, the two congruence rules for application and abstraction, and β and η-conversion. Because →_{R} acts only on long βη-normal forms, Theorem 3.4 of [15] becomes

Theorem 3.5 s =_{R} t ⇔ s↕_{β}^{η} ↔_{R}^{∗} t↕_{β}^{η}

This equivalence between =_{R} and ↔_{R}^{∗} only holds because of the restriction to rules of base type (which is built into the above definition of an HRS). Given the rule

λx.c(x, F (x)) → λx.d(F (x), x),

the relation ↔_{R}^{∗} is strictly weaker than =_{R}: c(a, f(a)) =_{R} d(f(a), a) holds but c(a, f(a)) ↔_{R}^{∗} d(f(a), a) does not hold. The reason is that rewriting acts only on terms in β-normal form. Consequently we do not consider it a problem that the main result of this paper also relies on the restriction to rules of base type.

Confluence of rewrite systems always depends on an analysis of critical pairs. Critical pairs involve the unification of one left-hand side with the subterm of another left-hand side. But taking the subterm of a λ-term may turn a bound into a free variable. For example x in the subterm abs(S, x) of the left-hand side of eta used to be bound. To cope with this phenomenon, the lost binders have to be reintroduced, thus leading to λx.abs(S, x). In the example this happens to be a subterm itself, which is coincidental. In order to unify λx.abs(S, x) with the left-hand side of beta, the latter needs to be lifted:

Definition 3.6 If p ∈ Pos(s) let bv(t, s) be the set of all λ-abstracted variables on the path from the root of s to p.

An \overline{x_{k}}-lifter of a term t away from W is a substitution σ = \{F ↦ (ρF)(\overline{x_{k}}) | F ∈ fv(t)\} where ρ is a renaming such that Dom(ρ) = fv(t), Cod(ρ) ∩ W = {} and ρF : τ_{1} → ⋯ → τ_{k} → τ if x_{1} : τ_{1}, …, x_{k} : τ_{k} and F : τ.

For example {F ↦ G(x), S ↦ T (x)} is an x-lifter of app(abs(λy.F (y), S)) away from any W not containing G or T.

Now we can give the (w.r.t. [15] slightly corrected) definition of critical pairs for HRSs.

Definition 3.7 Two rules l_{i} → r_{i}, i = 1, 2, a position p ∈ Pos(l_{1}), and a most general unifier θ of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(l_{2}σ) such that

• the free and bound variables in l_{1} are disjoint and the head of l_{1}/p is not free in l_{1}, and

• \{\overline{x_{k}}\} = bv(l_{1}, p) and σ is an \overline{x_{k}}-lifter of l_{2} away from fv(l_{1})

determine a critical pair ⟨r_{1}θ↓_{β}, (l_{1}[r_{2}σ]_{p})θ↓_{β}⟩.

The critical pairs of an HRS are the critical pairs between any two of its rules, with the exception of those pairs arising from overlapping a rule with itself at position ε.

In Example 3.4 we have two critical pairs, one of which arises by taking l_{1} = abs(λx.app(S, x)) and l_{1}/p = app(S, x). Then bv(l_{1}, p) = {x} and σ = {F ↦ G(x), S ↦ T (x)} is an x-lifter of l_{2} = app(abs(λy.F (y)), S) away from fv(l_{1}). Because θ = {S ↦ abs(λy.H(y)), T ↦ λx.x, G ↦ λx, y.H(y)} is a most general unifier of λx.app(S, x) and λx.app(abs(λy.G(x, y)), T (x)), the actual critical pair is ⟨abs(λy.H(y)), abs(λx.H(x)⟩.

Since our main concern is not the critical pairs themselves but their absence, we can work with a more concise definition:

Definition 3.8 l_{1} at p overlaps with l_{2} if the head of l_{1}/p is not a variable free in l_{1} and λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(l_{2}σ) unify, where \{\overline{x_{k}}\} = bv(l_{1}, p), and σ is an \overline{x_{k}}-lifter of l_{2} away from fv(l_{1}). Two terms l_{1} and l_{2} overlap if, for some p ∈ Pos(l_{1}), l_{1} at p overlaps with l_{2}.

It follows easily that

Lemma 3.9 An HRS has no critical pairs iff each left-hand side overlaps only with itself at ε.

Finally we can define our object of interest:

Definition 3.10 An HRS is orthogonal (OHRS) if it is left-linear (no free variable appears twice on the left-hand side of a rule) and has no critical pairs.

It is not difficult to see that the pure lambda-calculus (Example 3.4) with only beta or eta is an OHRS. However, combining beta and eta leads to two (trivial) critical pairs [15], one of which is shown above.

For technical reasons we need the following lemma:

Lemma 3.11 If l_{0} = λ\overline{x_{k}}.l, the head of l_{0} is not a free variable and lθ↓_{β} = l′θ′↓_{β}, then l_{0} and l′ overlap. Proof We claim that l_{0} at p = 1^{k}, the sequence of k 1s, overlaps with l′. Let σ be an \overline{x_{k}}-lifter of l′ away from fv(l_{0}). By definition l_{0} at p and l′ overlap if λ\overline{x_{k}}.(l_{0}/p) = l_{0} and λ\overline{x_{k}}.(l′σ) unify. We show that θ′′ = θ ∪ θ_{1}, where θ_{1} = \{ρF ↦ λ\overline{x_{k}}.(θ′F) | F ∈ fv(l′)\}, is such a unifier.

For any substitution θ let θ↓_{β} := {F ↦ (θF)↓_{β} | F ∈ Dom(θ)}. Using this definition we get (σθ_{1})↓_{β} = (\{F ↦ (λ\overline{x_{k}}.(θ′F))(\overline{x_{k}}) | F ∈ fv(l′)\} ∪ θ_{1})↓_{β} = \{F ↦ (θ′F)↓_{β} | F ∈ fv(l′)} ∪ θ_{1}↓_{β} = θ′↓_{β} ∪ θ_{1}↓_{β}. Now the required unifiability follows easily: l_{0}θ′′↓_{β} = l_{0}θ↓_{β} = λ\overline{x_{k}}.(lθ↓_{β}) = λ\overline{x_{k}}.(l′θ′↓_{β}) = λ\overline{x_{k}}.(l′(θ′↓_{β})↓_{β}) = λ\overline{x_{k}}.(l′(θ′↓_{β} ∪ θ_{1}↓_{β})↓_{β}) = λ\overline{x_{k}}.(l′((σθ_{1})↓_{β})↓_{β}) = (λ\overline{x_{k}}.(l′σ))θ_{1}↓_{β} = (λ\overline{x_{k}}.(l′σ))θ′′↓_{β}. □

Note that this lemma is only true because by our conventions the free variables in the domain and codomain of θ are disjoint from the bound variables in l_{0}.

4 Confluence of OHRSs

Having set the stage, we can now proceed to prove the main result of this paper. The proof is based on the combination of two classical techniques for showing confluence of orthogonal reduction systems. In the sequel let R be an OHRS. Parallel bottom-up reduction w.r.t. R is the smallest relation > on terms which is closed under the following inference rules:

\begin{matrix}s_{i} > t_{i} & (i = 1, …, n) \\ a(\overline{s_{n}}) > a(\overline{t_{n}}) \end{matrix} (A)  {s > t \atop λx.s > λx.t} (L)  {θ >^{fv(l)} θ′ \atop lθ↓_{β} > rθ′↓_{β}} (R)

where a is an atom of type \overline{τ_{n}} → τ and s_{i} : τ_{i}, (l → r) ∈ R, and θ >^{W} θ′ is short for ∀F ∈ W. θF > θ′F.

This definition is essentially a combination of proof techniques for orthogonal TRSs and λcalculus. It is interesting to compare it with the corresponding definitions for these two classical cases:

• for orthogonal TRSs, (A) remains unchanged, (L) must be dropped, and (R) becomes lθ > rθ;

• for pure λ-calculus, (A) becomes s_{0} > t_{0} ∧ s_{1} > t_{1} ⇒ (s_{0} s_{1}) > (t_{0} t_{1}), (R) becomes s > s′ ∧ t > t′ ⇒ (λx.s)t > s′{x ↦ t′}, and we need to add s > s. The latter is implicit in the above formulation of (A).

Various further combinations of these two techniques appear in the literature [18, 5]. In contrast to the above versions of >, the definition given by Aczel is slightly more general:

\begin{aligned}s_{1} > t_{1} & … & s_{n} > t_{n} & a(\overline{t_{n}}) = lθ↓_{β} \\ & a(\overline{s_{n}}) > rθ↓_{β} \end{aligned}

This rule allows the reduction of a(\overline{s_{n}}) even if the latter became a redex only through the reduction of some of its immediate subterms s_{i}. In orthogonal systems the two versions of (R) coincide because left-hand sides do not overlap. In weakly orthogonal systems, however, a certain amount of overlapping is permitted. This generalization is studied by Femke van Raamsdonk [19] who uses Aczel’s version of > in her confluence proof.

For inductive purposes we also define |s > t| as the size of the proof of s > t. Although there may be many proofs of s > t, the one in question can usually be inferred from the context.

|a(\overline{s_{n}}) > a(\overline{t_{n}})| = 1 + ∑_{i=1}^{n} |s_{i} > t_{i}|

|λx.s > λx.t| = 1 + |s > t|
|lθ↓_{β} > rθ′↓_{β}| = 1 + |θ >^{fv(l)} θ′|

where |θ >^{W} θ′| = ∑_{F ∈W} |s_{F} > s′_{F} | if for all F ∈ W: θF = λ\overline{x_{k_{F}}} .s_{F}, θ′F = λ\overline{x_{k_{F}}} .s′_{F} and s_{F} and s′_{F} are not abstractions.

4.1 Lemmas

Before we can embark on the proof of the diamond property of >, we need a number of supporting lemmas. The first few are obvious enough.

Lemma 4.1 s > s holds for all terms s in long βη-normal form. Proof by induction on the structure of s. □

Lemma 4.2 If s > t then both s and t are in long βη-normal form. Proof by induction on the structure of s > t. All three inferences (A), (L) and (R) preserve long βη-normal forms. For (A) this is because a : \overline{τ_{n}} → τ and τ is atomic. For (R) it follows because sθ↓_{β} is not only in β-normal form but also in long βη-normal form if both s and the terms in the codomain of θ are. □

Lemma 4.3 →_{R} ⊆ > ⊆ →_{R}^{∗} Proof using the inference rule based definition of →_{R}.

• s →_{R} t ⇒ s > t is proved by induction on the structure of s →_{R} t. The only non-trivial case is a(\overline{s_{n}}) →_{R} a(s_{1}, …, s_{k−1}, t_{k}, s_{k+1}, …, s_{n}) and s_{k} →_{R} t_{k}. Then s_{k} > t_{k} by induction hypothesis and s_{i} > t_{i} := s_{i} by Lemma 4.1 for i ≠ k. Hence a(\overline{s_{n}}) > a(\overline{t_{n}}) follows by rule (A).

• s > t ⇒ s →_{R}^{∗} t is proved by induction on the structure of s > t. The only non-trivial case is a(\overline{s_{n}}) > a(\overline{t_{n}}) and s_{i} > t_{i} for i = 1, …, n. By induction hypothesis s_{i} →_{R}^{∗} t_{i} and hence a(\overline{s_{n}}) →^{∗} a(t_{1}, s_{2}, …, s_{n}) →^{∗} ⋯ →^{∗} a(t_{1}, …, t_{n−1}, s_{n}) →^{∗} a(\overline{t_{n}}).

□

Lemma 4.4 If λx.s > t′ then t′ = λx.t and s > t for some t. Proof Derivation (A) is syntactically inapplicable and R cannot apply because all its rules are of base type. □

The first non-trivial lemma is the following. It relies crucially on the presence of a type structure which serves as a well-founded set for inductive purposes.

Lemma 4.5 If s > t and θ >^{fv(s)} θ′ then sθ↓_{β} > tθ′↓_{β}. Proof by induction on the order of θ

ord(τ) = 0  if τ is a base type
ord(τ_{0} → τ_{1}) = max{ord(τ_{0}) + 1, ord(τ_{1})}
ord(θ) = max{ord(τ) | V_{τ} ∩ Dom(θ) ≠ {}}

immediately followed by an induction on the structure of s > t.

1. If s = a(\overline{s_{n}}), t = a(\overline{t_{n}}) and s_{i} > t_{i} for i = 1, …, n, then by the inner induction hypothesis s_{i}θ↓_{β} > t_{i}θ↓_{β} holds.

If a is a constant or not in the domain of θ (and hence θ′), then sθ↓_{β} = a(\overline{s_{n}θ↓_{β}}) > a(\overline{t_{n}θ↓_{β}}) = tθ′↓_{β} follows immediately.

Otherwise a ∈ Dom(θ). From Lemmas 4.2 and 4.4 it follows that θa = λ\overline{x_{n}}.u, θ′a = λ\overline{x_{n}}.u′ and u > u′. Thus we have sθ↓_{β} = (θa)(\overline{s_{n}θ↓_{β}})↓_{β} = uθ_{1}↓_{β} and tθ′↓_{β} = (θ′a)(\overline{t_{n}θ′↓_{β}})↓_{β} = u′θ′_{1}↓_{β} where θ_{1} = \{\overline{x_{n} ↦ s_{n}θ↓_{β}}\} and θ′_{1} = \{\overline{x_{n} ↦ t_{n}θ′↓_{β}}\}. If a is of type \overline{τ_{n}} → τ, the definition of ord implies ord(τ_{i}) < ord(\overline{τ_{n}} → τ) and hence ord(θ_{1}) < ord(θ), i.e. the outer induction hypothesis applies. Hence uθ_{1}↓_{β} > u′θ′_{1}↓_{β} follows, which completes the proof of sθ↓_{β} > tθ′↓_{β}.

2. If s = λx.u, t = λx.u′ and u > u′ then the inner induction hypothesis yields sθ↓_{β} = (λx.u)θ↓_{β} = λx.(uθ↓_{β}) > λx.(u′θ′↓_{β}) = (λx.u′)θ′↓_{β} = tθ′↓_{β}.

3. If s = lθ_{1}↓_{β}, t = rθ′_{1}↓_{β} and θ_{1} >^{fv(l)} θ′_{1} then the inner induction hypothesis yields F θ_{1}θ↓_{β} > F θ′_{1}θ′↓_{β} for all F ∈ fv(l). Let θ_{2} = {F ↦ F θ_{1}θ↓_{β} | F ∈ fv(l)} and θ′_{2} = {F ↦ F θ′_{1}θ′↓_{β} | F ∈ fv(l)}. Thus we have sθ↓_{β} = lθ_{1}↓_{β}θ↓_{β} = lθ_{1}θ↓_{β} = lθ_{2}↓_{β} > rθ′_{2}↓_{β} = rθ′_{1}θ′↓_{β} = rθ′_{1}↓_{β}θ′↓_{β} = tθ′↓_{β}.

□

Corollary 4.6 If s is in long βη-normal form and θ >^{fv(s)} θ′ then sθ↓_{β} > sθ′↓_{β}. Proof by combining Lemmas 4.1 and 4.5. □

The following lemma looks very technical but expresses a simple idea: in a reduction step lθ↓_{β} > s, where l is linear and does not overlap with any rule, the l-part cannot change, i.e. all reductions must have taken place inside the terms introduced via θ. Thus there is a θ′ such that θ >^{fv(l)} θ′ and lθ′↓_{β} = s.

Lemma 4.7 Let l_{0} = λ\overline{x_{n}}.l be a linear pattern that does not overlap with any left-hand side of R and let W = fv(l_{0}). If the elements of Cod(θ) are in long βη-normal form and lθ↓_{β} > s then there exists a substitution θ′ such that θ >^{W} θ′, |θ >^{W} θ′| ≤ |lθ↓_{β} > s| and lθ′↓_{β} = s. Proof by induction on the structure of l.

1. If l = c(\overline{l_{m}}), then the last inference in lθ↓_{β} > s must be (A): it cannot be (L) and Lemma 3.11 implies that it cannot be (R) either, otherwise l_{0} would overlap with the lefthand side of a rule in R. Therefore s = c(\overline{s_{m}}) and l_{i}θ↓_{β} > s_{i}. Because each λ\overline{x_{n}}.l_{i} is also a linear pattern that does not overlap with any left-hand side of R, the induction hypothesis yields substitutions θ_{i} such that θ >^{W_{i}} θ_{i}, |θ >^{W_{i}} θ_{i}| ≤ |l_{i}θ↓_{β} > s_{i}| and l_{i}θ_{i}↓_{β} = s_{i}, where W_{i} = fv(λ\overline{x_{n}}.l_{i}). Now let θ′ := ⋃_{i=1}^{m} θ_{i}, which is a well-defined substitution because the W_{i}, and hence the domains of the θ_{i}, are disjoint, thanks to linearity. Obviously θ >^{W} θ′ and lθ′↓_{β} = c(\overline{l_{m}θ_{m}↓_{β}}) = s and |θ >^{W} θ′| = ∑_{i=1}^{m} |θ >^{W_{i}} θ_{i}| ≤ ∑_{i=1}^{m} |l_{i}θ↓_{β} > s_{i}| < 1 + ∑_{i=1}^{m} |l_{i}θ↓_{β} > s_{i}| = |lθ↓_{β} > s|.

2. If l = F (\overline{s_{m}}) then l↓_{η} = F (\overline{y_{m}}) because l_{0} is a pattern. Wlog θF = λ\overline{y_{m}}.r. Hence lθ↓_{β} = l↓_{η}θ↕_{β}^{η} = (λ\overline{y_{m}}.r)(\overline{y_{m}})↕_{β}^{η} = r and thus r > s. Let θ′ = \{F ↦ λ\overline{y_{m}}.s\}. Obviously θ >^{\{F \}} θ′, |θ >^{\{F \}} θ′| = |r > s| = |lθ↓_{β} > s| and lθ′↓_{β} = l↓_{η}θ′↕_{β}^{η} = (λ\overline{y_{m}}.s)(\overline{y_{m}})↕_{β}^{η} = s.

3. If l = λx_{n+1}.l′ then the claim follows easily from the induction hypothesis.

□

4.2 The Proof

Theorem 4.8 If R is orthogonal then > has the diamond property. Proof We assume that s > s^{i}, i = 0, 1, and show by induction on |s > s^{0}| + |s > s^{1}| that there is a t such that s^{i} > t, i = 0, 1.

If s = λx.s′, Lemma 4.4 implies s^{i} = λx.t^{i} and s′ > t^{i}, for i = 0, 1. By induction hypothesis there exists a t′ such that t^{i} > t′ and hence s^{i} > λx.t′ =: t.

If s = a(\overline{s_{n}}), there are three possible combinations of (A) and (R) inferences.

1. If both s > s^{0} and s > s^{1} via (A) then s = a(\overline{s_{n}}) and s^{i} = a(\overline{s_{n}^{i}}) and s_{j} > s_{j}^{i}. By induction hypothesis there exist t_{j} such that s_{j}^{i} > t_{j} and hence s^{i} > a(\overline{t_{n}}) =: t.

2. If both s > s^{0} and s > s^{1} via (R) then s = l_{i}θ_{i}↓_{β} > r_{i}θ′_{i}↓_{β} = s^{i} for some (l_{i} → r_{i}) ∈ R, i = 0, 1. Since R is orthogonal, the two rules must be the same (otherwise they would give rise to an overlap at ε) and hence (l_{0} → r_{0}) = (l_{1} → r_{1}) =: (l → r) and θ_{0} = θ_{1} =: θ. Because |s > s^{i}| = 1 + |θ >^{fv(l)} θ′_{i}|, the induction hypothesis applies and there is a θ′ such that θ′_{i} >^{fv(l)} θ′. Since fv(r) ⊆ fv(l), Lemma 4.5 yields the desired s^{i} = rθ′_{i}↓_{β} > rθ′↓_{β} =: t.

3. If s > s^{0} via (R) and s > s^{1} via (A) then s = lθ↓_{β} = a(\overline{s_{n}}), s^{0} = rθ′↓_{β}, θ >^{fv(l)} θ′, (l → r) ∈ R, s^{1} = a(\overline{s_{n}^{1}}), and s_{i} > s_{i}^{1}. By an observation above l must be of the form c(\overline{l_{n}}) and hence a = c and l_{i}θ↓_{β} = s_{i}. Because l is a linear pattern that can only overlap with itself at ε, the l_{i} are linear patterns which do not overlap with any left-hand side of R. Thus Lemma 4.7 yields the existence of substitutions θ_{i} such that θ >^{fv(l_{i})} θ_{i}, |θ >^{fv(l_{i})} θ_{i}| ≤ |s_{i} > s_{i}^{1}| and l_{i}θ_{i}↓_{β} = s_{i}^{1}. Since l is linear, the free variables in the l_{i} are disjoint and hence θ′′ := ⋃_{i=1}^{n} θ_{i} is a well-defined substitution with θ >^{fv(l)} θ′′. Now the induction hypothesis yields a substitution σ such that θ′ >^{fv(l)} σ and θ′′ >^{fv(l)} σ. Hence s^{1} = c(\overline{s_{n}^{1}}) = c(\overline{l_{n}θ_{n}↓_{β}}) = c(\overline{l_{n}θ′′↓_{β}}) = lθ′′↓_{β} > rσ↓_{β} =: t. Corollary 4.6 yields s^{0} = rθ′↓_{β} > rσ↓_{β} = t, thus closing the diamond.

□

Combining Lemmas 2.1 and 4.3 with the above theorem immediately yields the main result of this paper:

Corollary 4.9 Every OHRS is confluent.

5 Applications

The standard application of our result is to various lambda-calculi, in particular pure lambdacalculus itself (Example 3.4). It was already mentioned that beta and eta on their own form orthogonal systems. Thus we can conclude that beta and eta reductions are confluent. The combination of the two is treated in the next section. Since previous work on rewriting lambdaterms [1, 10, 18] has already treated many reduction systems arising in proof theory, we refrain from adding more examples to this list. However, we would like to point out that our result should help to eliminate sentences like “A proof can be given by adapting the method of Tait and Martin-Löf using a form of parallel reduction (see also Stenlund)” [7, pp. 9 and 29] in favour of a direct application of our meta-theorem.

A second application area concerns the combination of term rewriting systems with betareduction as studied by Breazu-Tannen [3]. Breazu-Tannen combines a fixed higher-order reduction, namely beta, with an arbitrary set of first-order reductions R and is able to show that confluence of R is preserved by adding simply-typed beta. This result was generalized significantly by Dougherty [5] who showed that it is not the type system (simple, polymorphic, etc.) but the strong normalization property which makes the result hold.

We can also obtain some results in this area by combining our object-level beta-rule with other reductions. The first-order term f(s_{1}, …, s_{n}) translates to app(...(app(f, t_{1}), ...), t_{n}), where t_{i} is the translation of s_{i}. It is easy to see that the left-hand side of beta does not overlap with the left-hand side of the translation of a first-order reduction. In fact, we have the more general lemma:

Lemma 5.1 Let R be an OHRS such that no left-hand side has abs as a head constant or a subterm of the form app(F, t), where F is free and t is arbitrary. Then R ∪ {beta} is orthogonal and hence confluent.

Comparing this with the result by Dougherty, we find that the above lemma admits more general rules (not just first-order reductions) and needs no (object-level) types or strong normalization property, but requires orthogonality of R. In fact, our lemma is much closer to a recent result by Fritz Müller [13] who proves that R ∪ {beta} is confluent if R is a confluent left-linear “applicative term rewriting system” (ATRS). Again, his and our result are incomparable: his ATRSs are less general than the rules in the above lemma in that the left-hand sides may not contain abs at all, but he allows overlapping rules.

6 Extensions

Although our main result yields the confluence of beta and eta in isolation, it does not extend to the combination of beta and eta because the two rules overlap. However, their two critical pairs are trivial, i.e. of the form ⟨t, t⟩ [15]. Left linear TRSs with only trivial critical pairs are sometimes called weakly orthogonal and are confluent [11]. In fact, Huet [9, p. 815] proved confluence for the even larger class of left-linear “parallel closed” TRSs. Very recently, Femke van Raamsdonk [19] has shown that weakly orthogonal CRSs are confluent. Hence it is tempting to assume that weakly orthogonal HRSs are confluent as well. Analyzing van Raamsdonk’s proof, it becomes clear why we failed to prove her result for HRSs: our definition of > is too weak and Aczel’s definition should be used (see Section 4).

In order to prove confluence for the combination of beta and eta we had to resort to a proof technique that is usually employed in classical confluence proofs [2]: the two reductions are separately shown to be confluent and their combined confluence follows by a certain kind of commutation. Abstracting from the particulars of the eta-rule we call a term in β-normal form non-duplicating if it is fully linear (no free or bound variable occurs twice) and has no subterm of the form F (… G …), where F and G are free. A rule is called non-duplicating if its right-hand side is. The definition ensures that non-duplicating rules cannot duplicate subterms.

Theorem 6.1 If R_{0} and R_{1} are left-linear and confluent, all critical pairs between rules in R_{0} and R_{1} are trivial, i.e. of the form ⟨t, t⟩, and R_{1} is non-duplicating, then R := R_{0} ∪ R_{1} is confluent. Proof sketch. According to the lemma of Hindley/Rosen it suffices to show that →_{R_{0}}^{∗} and →_{R_{1}}^{∗} commute, which in turn is implied if for every fork s →_{R_{i}} s_{i}, i = 0, 1, there is a term t such that s_{0} →_{R_{1}}^{∗} t and s_{1} →_{R_{0}}^{=} t, i.e. either s_{1} →_{R_{0}} t or s_{1} = t [2, p. 65].

If the two redexes overlap, they are instances of a critical pair and hence s_{0} = s_{1} =: t. If the R_{0}-redex is above the R_{1}-redex, it is easy to find a t such that s_{0} →_{R_{1}}^{∗} t and s_{1} →_{R_{0}} t. If the R_{0}-redex r_{0} is below the R_{1}-redex, there is at most one descendant of r_{0} in s_{1} (R_{1} is non-duplicating!) and we can find a t such that s_{0} →_{R_{1}} t and s_{1} →_{R_{0}}^{=} t. □

Since beta and eta on their own are left-linear and confluent, the two critical pairs between beta and eta are trivial, and eta is non-duplicating, beta+eta is again confluent. The same argument applies to some other well-known weakly-orthogonal systems, for example parallel-or:

Por = \{ \begin{matrix}or(X, true) → & true & or(true, X) → & true \\ or(X, false) → & X & or(false, X) → & X \end{matrix} \}

Por is locally confluent (all critical pairs are trivial), terminating and hence confluent. Adding beta preserves confluence because there are no critical pairs between Por and beta, and Por is non-duplicating. This confluence result also follows from the work of Müller. Note that in the absence of termination, the violation of left-linearity is again fatal: adding the rules or(X, X) → X and or(not(X), X) → true leads to non-confluence just as in Breazu-Tannen’s example [3].

7 Conclusion

The results about higher-order critical pairs and the confluence of OHRSs provide a firm foundation for the further study of higher-order rewrite systems. It should now be interesting to lift more results and techniques both from term-rewriting and λ-calculus to the level of HRSs. For example termination proof techniques are much studied for TRSs and are urgently needed for HRSs; similarly the extension of our result to weakly orthogonal HRSs or even to Huet’s “parallel closed” systems is highly desirable. Conversely, a large body of λ-calculus reduction theory has been lifted to CRSs [10] already and should be easy to carry over to HRSs.

Finally there is the need to extend the notion of an HRS to more general left-hand sides. For example the eta-rule for the case-construct on disjoint unions [15]

case(U, λx.F (inl(x)), λy.G(inr(y))) → F (U)

is outside our framework, whichever way it is oriented.

Acknowledgement I would like to thank Jan Willem Klop, Christian Prehofer and Femke van Raamsdonk for their careful reading and for the corrections and improvements they suggested.

References

[1] P. Aczel. A general Church-Rosser theorem. Technical report, University of Manchester, 1978.

[2] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, 2nd edition, 1984.

[3] V. Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, pages 82–90, 1988.

[4] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B, pages 243–320. Elsevier - The MIT Press, 1990.

[5] D. J. Dougherty. Adding algebraic rewriting to the untyped lambda-calculus. In R. V. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, pages 37–48. LNCS 488, 1991.

[6] A. Felty. A logic-programming approach to implementing higher-order term rewriting. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Extensions of Logic Programming, Proc. 2nd Int. Workshop, pages 135–158. LNCS 596, 1992.

[7] J. Gallier. Constructive Logics. Part I. Technical Report 8, DEC Paris Research Laboratory, 1991.

[8] J. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.

[9] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27:797–821, 1980.

[10] J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980.

[11] J. W. Klop. Term rewriting systems. Technical Report CS-R9073, CWI, Amsterdam, 1990.

[12] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming, pages 253–281. LNCS 475, 1991.

[13] F. Müller. Confluence of the lambda-calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293–299, 1992.

[14] G. Nadathur and D. Miller. An overview of λProlog. In R. A. Kowalski and K. A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, pages 810–827. MIT Press, 1988.

[15] T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342–349, 1991.

[16] T. Nipkow. Functional unification of higher-order patterns. Technical report, TU München, Institut für Informatik, 1992.

[17] L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

[18] S. Stenlund. Combinators, λ-Terms, and Proof Theory. D. Reidel, 1972.

[19] F. van Raamsdonk. A simple proof of confluence for weakly orthogonal combinatory reduction systems. Technical Report CS-R9234, CWI, Amsterdam, 1992.