Higher-Order Rewrite Systems and their Confluence

Richard Mayr & Tobias Nipkow^{∗} TU München^{†}

Abstract

We study Higher-Order Rewrite Systems (HRSs) which extend term rewriting to λ-terms. HRSs can describe computations over terms with bound variables. We show that rewriting with HRSs is closely related to undirected equational reasoning. We define Pattern Rewrite Systems (PRSs) as a special case of HRSs and extend three confluence results from term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, confluence of rewriting modulo equations à la Huet, and confluence of orthogonal PRSs.

1 Introduction

Much effort has gone into the study of first-order rewrite systems and as a result there is a large body of knowledge about their properties. In 1972, Knuth and Bendix published their seminal paper [17] which shows that confluence of terminating term-rewriting systems is decidable: a simple test of confluence for the finite set of so called critical pairs suffices. Later Huet [10] gave the definitive formulation of this result and extended it in several directions, including confluence for term-rewriting modulo certain equational theories.

The objective of this paper is to generalize some of these results from first-order rewrite systems (usually referred to as term-rewriting systems), where all functions are first-order, to rewrite systems over simply typed λ-terms. The aim of this generalization is to lift the rich theory developed around first-order rewrite systems and apply it to systems manipulating higher-order terms, such as program transformers, theorem provers and the like. This paper can be seen as an investigation of the meta-theory of computer systems like λProlog [23] and Isabelle [32].

We study two kinds of rewrite systems: Pattern Rewrite Systems (PRSs) and the more general Higher-Order Rewrite Systems (HRSs). PRSs are similar to Klop’s Combinatory Reduction Systems (CRSs) [14, 16]. Both are generalizations of Term-Rewriting Systems (TRSs) [5] to terms with higher-order functions and bound variables. The main difference is that PRSs use the typed λ-calculus as a meta-language, whereas CRSs come with their own untyped abstraction and substitution mechanism. The precise relationship between the two formalisms is explored elsewhere [29]. In both approaches, the abstraction mechanism is general enough to represent quantification in formulae, abstraction in functional programs, and many other variable-binding constructs. Using this representation, many operations on formulae and programs can be naturally expressed as higher-order rewrite systems. In particular within theorem proving systems, capabilities for higher-order rewriting provide a useful tool for the manipulation of terms with bound variables.

In Section 2 we review the terminology and notation of the typed λ-calculus which is used to define object-level rewrite systems, and define some basic properties. In Section 3 we define Higher-Order Rewrite Systems (HRSs), Pattern Rewrite Systems (PRSs), the reduction relation they induce on terms and show how they interact with substitutions. Then we show how HRSs induce an equality on terms and how it relates to reduction. In Section 4 the Critical Pair Lemma from Knuth and Bendix is generalized to PRSs. In Section 5 a theorem due to Huet about confluence modulo equality is generalized to PRSs. In Section 6 we deal with Orthogonal Pattern Rewrite Systems (OPRSs). These are a special kind of PRSs that have no critical pairs and whose rewrite rules are all left linear. In this section we give two different proofs that OPRSs are confluent. The paper closes with a discussion of related work.

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

†Address: Institut für Informatik, Technische Universität München, D-80290 München, Germany. Email:

{mayrri,nipkow}@informatik.tu-muenchen.de

2 Preliminaries

What follows is a description of the meta-language of simply typed λ-calculus which is used to define object-level rewrite systems. The notation is roughly consistent with the standard literature [4, 9].

Starting with some fixed set of base types B the set of all types T is the closure of B under the function space constructor →. The letter τ is used to denote types. Function types associate to the right: τ_{1} → τ_{2} → τ_{3} means τ_{1} → (τ_{2} → τ_{3}). Instead of τ_{1} → … → τ_{n} → τ we also write \overline{τ_{n}} → τ, 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 τ ≠ τ′, by λ-abstraction and application. Arbitrary variables are denoted by x, y and z, free variables by upper case letters F, G and H, and constants by c, d, f and g. Atoms are constants or variables and are denoted by a and b. Terms are denoted by l, r, s, t and u. We write t : τ to indicate that a term t is of type τ. The inductive definition of simply typed λ-terms is as follows:

\frac{x ∈ V_{τ}}{x : τ} \frac{c ∈ C_{τ}}{c : τ} \frac{s : τ → τ′ t : τ}{(s t) : τ′}  \frac{x : τ s : τ′}{(λx.s) : τ → τ′}

In the sequel all our λ-terms are assumed to be simply typed.

Instead of λx_{1} … λx_{n}.s we also write λx_{1}, …, x_{n}.s or just λ\overline{x_{n}}.s, where the x_{i} are assumed to be distinct. Similarly instead of (… (t u_{1}) …)u_{n} we write t(u_{1}, …, u_{n}) or just t(\overline{u_{n}}). The notation t(\overline{u_{n}}) includes the possibility n = 0 if t is of base type. The free and bound variables occurring in a term s are denoted by fv(s) and bv(s), respectively. A term is called linear iff no free variable occurs in it more than once.

We assume the usual definition of α, β and η conversion between λ-terms. We write s =_{γ} t, where γ ∈ {α, β, η} if s and t are equivalent modulo γ-conversion. In the sequel α-equivalent terms are identified.

As the simply typed λ-calculus is confluent and terminating w.r.t. β-reduction (η-reduction) every term t has a β-normal form (η-normal form) which is denoted t↓_{β} (t↓_{η}). Let t be in βnormal form. Then t is of the form λ\overline{x_{k}}.a(\overline{u_{m}}), where a is called the head of t. 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 write t↕_{β}^{η}. A λ-term t is in long βη-normal form iff t = t↕_{β}^{η}.

Convention: Unless stated otherwise, the variables r, s, t, etc., range over λ-terms in long βη-normal form.

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 [10, 5]. 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. The letter i is reserved for natural numbers and i.p is the position obtained by appending i to the front of p. 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 & . \\ | & / \ \\ t & t_{1} t_{2} \end{matrix}

Formally this is defined as follows:

\begin{aligned}t/ϵ & = & t \\ (t_{1} t_{2})/(i.p) & = & t_{i}/p \\ (λx.t)/(1.p) & = & t/p \end{aligned}

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. For p_{1}, p_{2} ∈ P os(t) we define the partial ordering p_{1} ≤ p_{2} iff p_{1} is a prefix of p_{2}. We write p_{1} ∥ p_{2} iff neither p_{1} ≤ p_{2} nor p_{2} ≤ p_{1}. If p_{1} ≤ p_{2}, the position p_{2}/p_{1} ∈ P os(t/p_{1}) is defined as p_{2} without the prefix p_{1}.

Substitutions are finite mappings from variables to terms of the same type. Substitutions are denoted by θ, σ and δ. For θ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} we define Dom(θ) = {x_{1}, …, x_{n}} and Cod(θ) = {t_{1}, …, t_{n}}. The application of a substitution to a term is defined by θ(t) := (λ\overline{x_{k}}.t)(\overline{t_{n}})↕_{β}^{η}. We often drop the parentheses and simply write θt.

Let θ_{1} and θ_{2} be substitutions. Then θ_{1} + θ_{2} is a substitution with

Dom(θ_{1} + θ_{2}) := Dom(θ_{1}) ∪ Dom(θ_{2})

defined by

(θ_{1} + θ_{2})(F) := \{ \begin{matrix}θ_{2}(F) & if F ∈ Dom(θ_{2}) \\ θ_{1}(F) & otherwise \end{matrix}

A renaming ρ is an injective substitution with Cod(ρ) ⊂ V and Dom(ρ) ∩ Cod(ρ) = {}. Renamings are always denoted by ρ.

Note that we will always assume that the domain of a substitution does not contain any variable bound in a term the substitution is applied to. If necessary, the bound variables are renamed automatically.

Two terms s and t are called unifiable iff there is a substitution θ, such that θ(s) = θ(t). The term s matches the term t iff there is a substitution θ, such that θ(s) = t. The problem to decide if a term s matches a term t and to compute the substitution θ is called the matching problem, which is very important for rewriting (see the remarks after Definition 3.3).

Given p ∈ Pos(t), bv(t, p) is the list of all λ-abstracted variables on the path from the root of t to p:

bv(t, ε) = []
bv((t_{1} t_{2}), i.p) = bv(t_{i}, p)
bv(λx.t, 1.p) = x.bv(t, p)

It is frequently necessary to “lift” a term into a context of certain bound variables. 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 f(λy.g(F (y)), S) away from any W not containing G or T; the corresponding renaming is ρ = {F ↦ G, S ↦ T }.

Definition 2.1 We define the order of a type in the traditional way:

ord(τ) = 1  if τ is a base type
ord(τ_{0} → τ_{1}) = max{ord(τ_{0}) + 1, ord(τ_{1})}

The order of a substitution is the maximal order of the types of the variables in its domain:

ord(θ) = max{ord(τ) | V_{τ} ∩ Dom(θ) ≠ {}}

Note that ord({}), i.e. max{} is defined to be 0.

Given a relation →, →^{=} denotes the reflexive closure, ↔ the symmetric closure and →^{∗} the transitive and reflexive closure of →. We write s ↓ t iff there is a u, such that s →^{∗} u and t →^{∗} u. The relation → is (locally) confluent if r →^{∗} s (r → s) and r →^{∗} t (r → t) imply s ↓ t. The relation → is terminating if there is no infinite sequence s_{i} → s_{i+1} for all i ∈ IN. It is well known that terminating relations are confluent iff they are locally confluent [10].

3 Higher-Order Rewrite Systems

Higher-Order Rewrite Systems are generalizations of first-order rewrite systems [5] to terms with higher-order functions and bound variables. Since unifiability of λ-terms is undecidable in general [8], we often restrict to a certain subclass of λ-terms which behave very much like first-order terms w.r.t. unification.

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 η-equivalent to a list of distinct bound variables.

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

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

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

Nipkow [25] presents a simplified form of Miller’s unification algorithm and develops it towards a practical implementation. Qian [35] shows that patterns can be unified in linear time.

Definition 3.3 A rewrite rule is a pair l → r such that l is not a free variable, l and r are of the same base type, and fv(l) ⊇ fv(r). A pattern rewrite rule is a rewrite rule whose left-hand side is a pattern. A Higher-Order Rewrite System (HRS) is a set of rewrite rules. A Pattern Rewrite System (PRS) is a set of pattern rewrite rules. The letter R always denotes an HRS (which will often be a PRS). A HRS R induces a relation →_{R} on terms:

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

A rewrite rule is called left-linear iff its left-hand side is linear. A HRS is called left-linear iff all its rewrite rules are left-linear.

Our HRSs are exactly Wolfram’s “higher-order term rewriting systems” [39].

A few remarks are in order:

• Due to the restrictions placed on left-hand sides, they must always be of the form c(\overline{s_{n}}).

• For PRSs, the restriction fv(l) ⊇ fv(r) is preserved under substitution. Thus it has the same effect as for TRSs: rewriting cannot introduce new variables. This fails for general HRSs: although f(F (X)) → g(X) meets the restriction, replacing F by λx.Y yields f(Y) → g(X) which violates the restriction. This problem is investigated in more detail by Kahrs [13].

Since we derive only very basic results about HRSs, we do not need to impose anything like fv(l) ⊇ fv(r), whereas the latter is essential for the confluence results for PRSs.

• The restriction to rules of base type is is necessary because of the simple matching procedure inherent in the definition of →_{R}. Otherwise ↔^{∗}_{R} and =_{R} do not coincide (see section 3.1). Pulling rules down to base type by applying them to new variables is fine for HRSs but may fail for PRSs: λx.c(F (x)) is a pattern but ceases to be one when pulled down to base type: c(F (X)).

• →_{R} is defined only between terms in long βη-normal form. This simplifies technicalities. Alternatively we could work with a relation ⇝_{R} defined by s ⇝_{R} t :⇔ s↕_{β}^{η} →_{R} t↕_{β}^{η}.

• The relation →_{R} is decidable if the matching problem is decidable for the left-hand sides of the rules in R. As by Theorem 3.2 even unifiability is decidable for patterns, the relation →_{R} is decidable for any PRS R; full unification will come in handy in connection with critical pairs.

For general HRSs the situation is different. Although unifiability is known to be undecidable even for second order λ-terms [8], it is not known whether higher-order matching is decidable. Padovani [31] proved that 4th order matching is decidable, but the general case is still open.

Example 3.4 The standard example of a PRS is pure lambda-calculus itself. The syntax 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).

The following lemma is a simple consequence of the fact that all rewrite rules must be of base type:

Lemma 3.5 If R is an HRS and λx.s →_{R} t then t = λx.u and s →_{R} u for some u.

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

Definition 3.6 Given an HRS R, let ⇒_{R} be the least relation on terms in long βη-normal form which is closed under the following rules:

{(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}} → τ.

Of course the two definitions of rewriting are equivalent.

Lemma 3.7 If R is an HRS then →_{R} and ⇒_{R} coincide. Proof The containment ⇒_{R} ⊆ →_{R} is shown by induction on the structure of ⇒_{R}, the reverse containment by induction on the length of p in the definition of →_{R}. □

In the sequel we will not distinguish →_{R} and ⇒_{R} and use whichever definition is most appropriate. In addition we usually drop the subscript _{R} and simply write →.

We will now prove an important theorem about →^{∗}, namely its stability under substitution. For TRSs this is simple and one obtains the stronger result that s → t implies θs → θt. For HRSs we have to replace → by →^{∗} because β-reductions during the application of a substitution can copy redexes. These copies need to be reduced sequentially; hence the use of →^{∗} instead of →. Later on we will see that a suitable notion of parallel reduction leads to a much nicer stability result (Lemma 6.4).

Definition 3.8 Let → be an arbitrary relation on terms. We define θ → θ′ to mean that θ(F) → θ′(F) holds for all F ∈ Dom(θ).

Theorem 3.9 Let R be an HRS. If s →^{∗} s′ and θ →^{∗} θ′ then θs →^{∗} θ′s′. Proof by induction on the order of θ (see Definition 2.1) with a nested induction on the length of the derivation s →^{∗} s′.

1. If s = s′, we prove θs →^{∗} θ′s by induction on the structure of s. The structure of normal forms dictates that s = λ\overline{x_{m}}.a(\overline{s_{n}}). The innermost induction hypothesis implies θs_{i} →^{∗} θ′s_{i}. Now we distinguish two cases.

(a) If a ∉ Dom(θ) (and hence a ∉ Dom(θ′) because the left-hand side of a rewrite rule cannot match a variable) then θs = λ\overline{x_{m}}.a(\overline{θs_{n}}) →^{∗} λ\overline{x_{m}}.a(\overline{θ′s_{n}}) = θ′s follows easily.

(b) If a ∈ Dom(θ) then θa = λ\overline{y_{n}}.t. By Lemma 3.5 it follows that θ′a = λ\overline{y_{n}}.t′ where t →^{∗} t′. Define the substitutions δ = \{\overline{y_{n} ↦ θs_{n}}\} and δ′ = \{\overline{y_{n} ↦ θ′s_{n}}\} and notice that we have δ →^{∗} δ′. If a is of type \overline{τ_{n}} → τ, the definition of ord implies ord(τ_{i}) < ord(\overline{τ_{n}} → τ) and hence ord(δ) < ord(θ) (note that this also holds in case n = 0). Thus the outermost induction hypothesis applies: δt →^{∗} δ′t′ because t →^{∗} t′. Thus we

obtain: θs = λ\overline{x_{m}}.(θa)(\overline{θs_{n}})↓_{β} = λ\overline{x_{m}}.(δt) →^{∗} λ\overline{x_{m}}.(δ′t′) = λ\overline{x_{m}}.(θ′a)(\overline{θ′s_{n}})↓_{β} = θ′s.

2. If s →^{∗} s′ → s′′, the inner induction hypothesis yields θs →^{∗} θ′s′. We show θ′s′ →^{∗} θ′s′′ by induction on the structure of the derivation s′ → s′′ as in Definition 3.6.

(a) If s′ = δl and s′′ = δr for some (l → r) ∈ R, θ′s′ = θ′δl = (θ′δ)l → (θ′δ)r = θ′δr = θ′s′′.

(b) If s′ = λx.t′ and s′′ = λx.t′′ such that t′ → t′′, the innermost induction hypothesis

yields θ′t′ → θ′t′′ and hence θ′s′ = λx.θ′t′ →^{∗} λx.θ′t′′ = θ′s′′.

(c) If s′ = a(\overline{s′_{n}}), s′′ = a(\overline{s′′_{n}}) such that s′_{k} → s′′_{k} for some k and s′_{i} = s′′_{i} for all i ≠ k, then the innermost induction hypothesis yields θ′s′_{k} →^{∗} θ′s′′_{k}. Because θ′s′_{i} →^{∗} θ′s′′_{i} holds trivially for all i ≠ k, we obtain θ′s′_{i} →^{∗} θ′s′′_{i} for all i. Now we distinguish two cases.

i. If a ∉ Dom(θ′) then θ′s′ = a(\overline{θ′s′_{n}}) →^{∗} a(\overline{θ′s′′_{n}}) = θ′s′′ follows easily.

ii. If a ∈ Dom(θ′) then θ′a = λ\overline{y_{n}}.t. Define the new substitutions δ′ = \{\overline{y_{n} ↦ θ′s′_{n}}\} and δ′′ = \{\overline{y_{n} ↦ θ′s′′_{n}}\} and notice that we have δ →^{∗} δ′. As above, we can show that ord(δ′) < ord(θ′); because → preserves types, we also have ord(θ′) = ord(θ). Thus the outermost induction hypothesis applies: δ′t →^{∗} δ′′t′ because t →^{∗} t. Thus

we obtain: θ′s′ = (θ′a)(\overline{θ′s′_{n}})↓_{β} = δ′t →^{∗} δ′′t = (θ′a)(\overline{θ′s′′_{n}})↓_{β} = θ′s′′. □

This theorem has two obvious corollaries:

• s →^{∗} s′ implies θs →^{∗} θs′ and

• θ →^{∗} θ′ implies θs →^{∗} θ′s.

However, the above proof fails if one reduces the statement of the theorem to one of the corollaries.

A slightly different version of Theorem 3.9 is also shown by Loría [18]: he uses conditional rewrite rules whose left-hand sides are patterns; his proof relies more on considerations about term positions.

Finally we lift Theorem 3.9 from →^{∗} to ↔^{∗}, at least for a special case:

Corollary 3.10 Let R be an HRS. If s ↔^{∗} s′ and t ↔^{∗} t′ then {x ↦ t}s ↔^{∗} {x ↦ t′}s′. Proof If s_{1} ↔ s_{2} ⋯ ↔ s_{m} and t_{1} ↔ t_{2} ⋯ ↔ t_{n}, let θ_{i} = {x ↦ t_{i}}. Now Theorem 3.9 implies

θ_{1}s_{1} ↔^{∗} θ_{2}s_{1} ↔^{∗} ⋯ ↔^{∗} θ_{n}s_{1} ↔^{∗} θ_{n}s_{2} ↔^{∗} ⋯ ↔^{∗} θ_{n}s_{m}. □

The general case, i.e. if θ ↔^{∗} θ′ and s ↔^{∗} s′ then θs ↔^{∗} θ′s′, is rather more tedious to derive and is left as an exercise.

3.1 Rewriting versus Equality

Originally, term rewriting was a means of analyzing equational theories, but it has long since taken on a life of its own. Returning to those roots we need to relate our notion of rewriting to a more “logical” notion of equality. In the sequel E will always denote a set of equations, i.e. a set of pairs s = t, where s and t are terms of the same type. In particular any rewrite rule l → r can also be viewed as an equation l = r.

Throughout this subsection we do not assume that terms or substitutions are in any normal form and θt denotes the non-normalizing application of θ to t.

Definition 3.11 A set of equations E induces a relation =_{E} defined by the following inference rules, which come in three groups:

• Basic conversion rules:

{(s = t) ∈ E \atop θs =_{E} θt} (E)  {s =_{β} t \atop s =_{E} t} (β)  {s =_{η} t \atop s =_{E} t} (η)

• Equality rules:

s =_{E} s (refl)  {s =_{E} t \atop t =_{E} s} (sym)  \begin{matrix}r =_{E} s & s =_{E} t \\ r =_{E} t \end{matrix} (trans)

• Congruence rules:

\begin{matrix}s_{1} =_{E} t_{1} & s_{2} =_{E} t_{2} \\ (s_{1} s_{2}) =_{E} (t_{1} t_{2}) \end{matrix} (app)  {s =_{E} t \atop λx.s =_{E} λx.t} (abs)

We call =_{E} the equational theory generated by E.

Note that θ in (E) is present only for convenience: substitution can be simulated by (abs), (app) and (β).

Modulo ↕_{β}^{η} we have the same relationship between →_{R} and =_{R} as in the first order case. This can be viewed as a justification of our definition of →_{R}.

Theorem 3.12 If R is an HRS then s =_{R} t ⇔ s↕_{β}^{η} ↔^{∗}_{R} t↕_{β}^{η}.

Proof The ⇐-direction is easy since =_{R} can mimic ↔^{∗} directly. If s↕_{β}^{η} ↔^{∗} t↕_{β}^{η} then s →^{∗}_{β} s_{β} ←^{∗}_{η} s_{η} ↔^{∗} t_{η} →^{∗}_{η} t_{β} ←^{∗}_{β} t. The reductions →_{β} and →_{η} are subsumed by (β) and (η); every ↔ is replaced by a single (E), possibly combined with (sym), embedded in a tree of congruence and reflexivity rules. Everything is held together with a finite amount of (trans).

For the ⇒-direction assume s =_{R} t. By induction on the structure of the derivation of s =_{R} t, considering each rule in turn, we prove s↕_{β}^{η} ↔^{∗} t↕_{β}^{η}.

(E): s = θl and t = θr for some (l → r) ∈ R. Thus l → r and hence s↕_{β}^{η} = (θl)↕_{β}^{η} →^{∗} (θr)↕_{β}^{η} = t↕_{β}^{η} by Theorem 3.9.

(β), (η), (refl): trivial because s↕_{β}^{η} = t↕_{β}^{η}.

(trans), (sym): by induction hypothesis because ↔^{∗} is transitive and symmetric.

(abs): by induction hypothesis because s′↕_{β}^{η} ↔^{∗} t′↕_{β}^{η} implies (λx.s′)↕_{β}^{η} ↔^{∗} (λx.t′)↕_{β}^{η}.

(app): s = (s_{1} s_{2}) and t = (t_{1} t_{2}). By induction hypothesis we have s_{i}↕_{β}^{η} ↔^{∗} t_{i}↕_{β}^{η}. Since s_{1} and t_{1} are of functional type, s_{1}↕_{β}^{η} must be of the form λx.s′_{1} and t_{1}↕_{β}^{η} of the form λx.t′_{1}. Thus Lemma 3.5 implies s′_{1} ↔^{∗} t′_{1}. Let θ = {x ↦ s_{2}↕_{β}^{η}} and θ′ = {x ↦ t_{2}↕_{β}^{η}}. Corollary 3.10

yields s↕_{β}^{η} = ((λx.s′_{1})s_{2})↕_{β}^{η} = (θs′_{1})↕_{β}^{η} ↔^{∗} (θ′t′_{1})↕_{β}^{η} = ((λx.t′_{1})t_{2})↕_{β}^{η} = t↕_{β}^{η}. □

Thus we know that undirected rewriting and equational logic coincide. Note that the proof sketch in [24] is considerably more involved because Theorem 3.9 is not available.

Now we can use the fact that for confluent reductions convertibility and existence of a common reduct coincide:

Corollary 3.13 If R is a confluent HRS then s =_{R} t ⇔ s↕_{β}^{η} ↓_{R} t↕_{β}^{η}.

Loría [18, Thm. 5.1.2] follows [24] to prove the same result for conditional PRSs. Wolfram [39, Thm. 4.11] claims the same result, but there is a gap in his proof: he fails to consider the (app)-rule, which requires something like Theorem 3.9, which is not at his disposal.

It should be pointed out that Theorem 3.12 fails for rules of function type. The one-rule system

R = {λx.c(x, F (x)) → λx.d(F (x), x)}

induces a relation ↔^{∗} which is strictly weaker than =_{R}: c(a, f(a)) =_{R} d(f(a), a) holds but c(a, f(a)) ↔^{∗} d(f(a), a) does not hold because the definition of → insists on rewriting β-normal forms only. Otherwise one could β-expand c(f(a), a) to (λx.c(x, f(x)))a before rewriting it to (λx.d(f(x), x))a.

4 The Critical Pair Lemma

In 1972, Knuth and Bendix [17] showed that confluence of terminating rewrite systems is decidable: a simple test of confluence for the finite set of so called critical pairs suffices. Later this result was generalized to PRSs by Nipkow [24], although no proof was given at the time. The purpose of this section is to supply the missing proof and at the same time prepare the ground for the related issue of confluence modulo equality which is treated in the following section.

Definition 4.1 Let there be two rewrite rules l_{i} → r_{i}, i = 1, 2, in a PRS and a position p ∈ P os(l_{1}) such that

• fv(l_{1}) ∩ bv(l_{1}) = {},

• the head of l_{1}/p is not a free variable in l_{1}, and

• the two patterns λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σl_{2}), where \{\overline{x_{k}}\} = bv(l_{1}, p) and σ is an \overline{x_{k}}-lifter of l_{2} away from fv(l_{1}), have a most general unifier θ.

Then the pattern l_{1} overlaps the pattern l_{2} at position p. The rewrite rules determine the critical pair ⟨θr_{1}, θ(l_{1}[σr_{2}]_{p})⟩. Note that because λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σl_{2}) unify, l_{1}/p must be of the form f(…).

Two redexes t/p_{1} and t/p_{2} in a term t are overlapping if there are rewrite rules l_{i} → r_{i}, i = 1, 2, such that p_{1} ≤ p_{2}, t/p_{1} = θ_{1}l_{1}, t/p_{2} = θ_{2}l_{2} and l_{1} overlaps l_{2} at position p_{2}/p_{1}.

The critical pairs of a PRS R are all the critical pairs arising from overlapping two lefthand sides of rules in R, except for a left-hand side of a rule overlapping itself at position ϵ. Note that it is possible that a left-hand side l of a rule l → r overlaps itself at positions p ≠ ϵ thus giving rise to a critical pair.

As this definition is difficult to handle, the following lemmas will be useful for dealing with critical pairs. Let us first show that critical pairs represent rewrite peaks:

Lemma 4.2 Let ⟨u_{1}, u_{2}⟩ be a critical pair. Then there exists a term s such that u_{1} ← s → u_{2}. Proof Let u_{1} = θr_{1} and u_{2} = θ(l_{1}[σr_{2}]_{p}) as in Definition 4.1 and define s := θl_{1}. Thus s → θr_{1} = u_{1} is trivial. We also have λ\overline{x_{k}}.θ(l_{1}/p) = θ(λ\overline{x_{k}}.(l_{1}/p)) = θ(λ\overline{x_{k}}.(σl_{2})) = λ\overline{x_{k}}.(θσl_{2}), because fv(l_{1}) ∩ bv(l_{1}) = {}. Therefore θ(l_{1}/p) = θσl_{2}. As l_{1} is a pattern and l_{1}/p is of the form f(…), we also have p ∈ Pos(θl_{1}) and (θl_{1})/p = θσl_{2}. So we get s = (θl_{1})[θσl_{2}]_{p} → (θl_{1})[θσr_{2}]_{p} = θ(l_{1}[σr_{2}]_{p}) = u_{2}. □

Lemma 4.3 Let there be two patterns l_{1}, l_{2}, a position p ∈ P os(l_{1}) where l_{1}/p is not of the form F (…), \{\overline{x_{k}}\} = bv(l_{1}, p) and an \overline{x_{k}}-lifter σ of l_{2} away from fv(l_{1}). Then the two patterns λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.σ(l_{2}) are unifiable iff there exist substitutions θ_{1} and θ_{2}, such that θ_{1}(l_{1}/p) = θ_{2}l_{2} and bv(l_{1}, p) ∩ Cod(θ_{1}) = {}. Proof

1. For the ⇐-direction assume w.l.o.g. Dom(θ_{1}) ⊆ fv(l_{1}). Let θ′_{2} := \{ρ(F) ↦ λ\overline{x_{k}}.θ_{2}(F) | F ∈ fv(l_{2})} and ρ be the renaming corresponding to σ. We now show that θ_{0} := θ_{1} ∪ θ′_{2} is a unifier of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σl_{2}). From θ′_{2}σ(F) = θ′_{2}((ρ(F))(\overline{x_{k}})) = θ_{2}(F) for all F ∈ fv(l_{2}) is follows that θ′_{2}(σl_{2}) = θ_{2}l_{2}. Therefore

θ_{0}(λ\overline{x_{k}}.(l_{1}/p)) = θ_{1}(λ\overline{x_{k}}.(l_{1}/p))  Dom(θ′_{2}) ∩ fv(l_{1}) = \{\}
= λ\overline{x_{k}}.θ_{1}(l_{1}/p)  bv(l_{1}, p) ∩ Cod(θ_{1}) = \{\}
= λ\overline{x_{k}}.θ_{2}(l_{2})
= λ\overline{x_{k}}.θ′_{2}(σ(l_{2})) = θ′_{2}(λ\overline{x_{k}}.σ(l_{2}))  Cod(θ′_{2}) ∩ \{\overline{x_{k}}\} = \{\}
= θ_{0}(λ\overline{x_{k}}.σ(l_{2}))  σ away from fv(l_{1}) ⊇ Dom(θ_{1})

2. For the ⇒-direction assume that θ is a unifier of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σl_{2}). Define θ_{1} := θ|_{fv(l_{1})} and θ_{2} := θσ. Then we have λ\overline{x_{k}}.θ_{1}(l_{1}/p) = θ(λ\overline{x_{k}}.(l_{1}/p)) = θ(λ\overline{x_{k}}.(σl_{2})) = λ\overline{x_{k}}.θ_{2}(l_{2}), because fv(l_{1}) ∩ bv(l_{1}) = \{\}. Therefore θ_{1}(l_{1}/p) = θ_{2}(l_{2}). As θ is a unifier of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σ(l_{2})) and \{\overline{x_{k}}\} = bv(l_{1}, p) ⊆ bv(λ\overline{x_{k}}.(l_{1}/p)) it follows that bv(l_{1}, p) ∩ Cod(θ_{1}) = {}. □

Lemma 4.4 Let there be two rules l_{i} → r_{i}, i = 1, 2, and a position p ∈ P os(l_{1}) where l_{1}/p is not of the form F (…), and substitutions θ_{1} and θ_{2} such that θ_{1}(l_{1}/p) = θ_{2}(l_{2}) and bv(l_{1}, p) ∩ Cod(θ_{1}) = {}. Then l_{1} overlaps l_{2} and there exist a critical pair ⟨s, t⟩ and a substitution δ with δs = θ_{1}r_{1} and δt = (θ_{1}l_{1})[θ_{2}r_{2}]_{p}. Proof Because fv(l_{i}) ⊇ fv(r_{i}) we can assume Dom(θ_{1}) ⊆ fv(l_{1}). Let \{\overline{x_{k}}\} = bv(l_{1}, p) and σ an \overline{x_{k}}-lifter of l_{2} away from fv(l_{1}). It follows from Lemma 4.3 that the two patterns λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.σ(l_{2}) are unifiable. Let θ_{0} be the unifier as defined in Lemma 4.3. By Lemma 3.2 there is a most general unifier θ of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.σ(l_{2}). Hence l_{1} overlaps l_{2} at position p and there is a critical pair ⟨s, t⟩, such that s = θr_{1} and t = θ(l_{1}[σr_{2}]_{p}). As θ is a most general unifier there exists a substitution δ with θ_{0} = δθ. Hence δs = θ_{0}r_{1} = θ_{1}r_{1} and δt = θ_{0}(l_{1}[σr_{2}]_{p}) = (θ_{0}l_{1})[θ_{0}(σr_{2})]_{p} = (θ_{1}l_{1})[θ′_{2}(σr_{2})]_{p} = (θ_{1}l_{1})[θ_{2}r_{2}]_{p} □

Corollary 4.5 l_{1} overlaps l_{2} iff there exist p ∈ Pos(l_{1}), θ_{1} and θ_{2}, such that θ_{1}(l_{1}/p) = θ_{2}l_{2} and bv(l_{1}, p) ∩ Cod(θ_{1}) = {}. Proof The ⇐-direction follows directly from Lemma 4.4. For the ⇒-direction assume that l_{1} overlaps l_{2}. By Definition 4.1 there is a most general unifier of λ\overline{x_{k}}.(l_{1}/p) and λ\overline{x_{k}}.(σl_{2}), where \{\overline{x_{k}}\} = bv(l_{1}, p) and σ is an \overline{x_{k}}-lifter of l_{2} away from fv(l_{1}). Therefore the result follows from Lemma 4.3. □

Lemma 4.6 (Critical Pair Lemma) Let R be a PRS and → the corresponding reduction relation on terms. If s → s_{i}, i = 1, 2, then either s_{1} ↓ s_{2}, or there are a critical pair ⟨u_{1}, u_{2}⟩, a substitution δ and a position p ∈ P os(s), such that s_{i} = s[δu_{i}]_{p}, i = 1, 2. Proof By definition of s → s_{i} there are rules (l_{i} → r_{i}) ∈ R, positions p_{i} ∈ P os(s) and substitutions θ_{i}, such that s/p_{i} = θ_{i}l_{i} and s_{i} = s[θ_{i}r_{i}]_{p_{i}}. Depending on the relative positions of the redexes, there are two cases.

1. p_{1} ∥ p_{2}. It follows directly that s_{1} = s[θ_{1}r_{1}]_{p_{1}} → s[θ_{1}r_{1}]_{p_{1}}[θ_{2}r_{2}]_{p_{2}} ← s[θ_{2}r_{2}]_{p_{2}} = s_{2}.

2. W.l.o.g. p_{1} ≤ p_{2}. Let q := p_{2}/p_{1}. It follows that

s_{2}/p_{1} = (s[θ_{2}r_{2}]_{p_{2}})/p_{1} = (s/p_{1})[θ_{2}r_{2}]_{q} = (θ_{1}l_{1})[θ_{2}r_{2}]_{q}

and

(θ_{1}l_{1})/q = (s/p_{1})/q = s/p_{2} = θ_{2}l_{2}

There are two cases:

(a) The two redexes do not overlap, i.e. q = q_{1}q_{2}, such that q_{1} ∈ P os(l_{1}) and l_{1}/q_{1} = F (\overline{x_{k}}), with F ∈ fv(l_{1}) (remember that l_{1} is a pattern). Hence θ_{1}(F) is of the form λ\overline{x_{k}}.t and we define the substitution

θ′_{1} := θ_{1} + \{F ↦ λ\overline{x_{k}}.(t[θ_{2}r_{2}]_{q_{2}})\}

It follows that t/q_{2} = (θ_{1}(F (\overline{x_{k}})))/q_{2} = (θ_{1}(l_{1}/q_{1}))/q_{2} = ((θ_{1}l_{1})/q_{1})/q_{2} = (θ_{1}l_{1})/q = θ_{2}l_{2} and hence θ_{1} →^{=} θ′_{1} (Definition 3.8). By stability (Theorem 3.9) it follows that

θ_{1}r_{1} →^{∗} θ′_{1}r_{1}.

Let H be a new variable (i.e. unused so far in this context) and

\begin{aligned}θ_{0} & := & θ_{1} & ∪ & \{H ↦ θ′_{1}(F)\} \\ θ′_{0} & := & θ_{0} & + & \{F ↦ θ′_{1}(F)\} \end{aligned}

and l_{0} := l_{1}[H(\overline{x_{k}})]_{q_{1}}. From θ_{1} →^{=} θ′_{1} it follows that θ_{0} →^{=} θ′_{0}. Theorem 3.9 yields

(θ_{1}l_{1})[θ_{2}r_{2}]_{q} = (θ_{1}l_{1})[θ′_{1}(F (\overline{x_{k}}))]_{q_{1}} = θ_{0}l_{0} →^{∗} θ′_{0}l_{0} = θ′_{0}l_{1} = θ′_{1}l_{1} → θ′_{1}r_{1}. The step

θ_{0}l_{0} →^{∗} θ′_{0}l_{0} is necessary because F may occur more than once in l_{1}.

Combining all this we obtain s_{1}/p_{1} = θ_{1}r_{1} →^{∗} θ′_{1}r_{1} ←^{∗} (θ_{1}l_{1})[θ_{2}r_{2}]_{q} = s_{2}/p_{1}. Placing it in the context it follows that

s_{1} = s[θ_{1}r_{1}]_{p_{1}} →^{∗} s[θ′_{1}r_{1}]_{p_{1}} ←^{∗} s[(θ_{1}l_{1})[θ_{2}r_{2}]_{q}]_{p_{1}} = s[θ_{2}r_{2}]_{p_{2}} = s_{2}

and hence s_{1} ↓ s_{2}.

(b) The two redexes overlap, i.e. q ∈ P os(l_{1}) and l_{1}/q is not of the form F (…). W.l.o.g. let bv(l_{1}) ∩ Cod(θ_{1}) = {}. Thus it follows from Lemma 4.4 that there exist a critical pair ⟨u_{1}, u_{2}⟩ and a substitution δ with δu_{1} = θ_{1}r_{1} and δu_{2} = (θ_{1}l_{1})[θ_{2}r_{2}]_{q}. This implies s_{1} = s[θ_{1}r_{1}]_{p_{1}} = s[δu_{1}]_{p_{1}} and s_{2} = s[θ_{2}r_{2}]_{p_{2}} = s[θ_{1}(l_{1})[θ_{2}r_{2}]_{q}]_{p_{1}} = s[δu_{2}]_{p_{1}}. □

Theorem 4.7 The relation → is locally confluent iff u_{1} ↓ u_{2} for all critical pairs ⟨u_{1}, u_{2}⟩ of the PRS R. Proof The ⇒-direction is a trivial consequence of Lemma 4.2. For the ⇐-direction assume u_{1} ↓ u_{2} for all critical pairs ⟨u_{1}, u_{2}⟩ of R. Let s → s_{i}, i = 1, 2. Then the Critical Pair Lemma 4.6 can be applied. In the first of its two cases the result follows immediately. In the second case there is a critical pair ⟨u_{1}, u_{2}⟩, a substitution δ and a position p ∈ P os(s), such that s_{i} = s[δu_{i}]_{p}, i = 1, 2. By assumption there is a term w, such that u_{1} →^{∗} w ←^{∗} u_{2}. Theorem 3.9

yields δu_{1} →^{∗} δw ←^{∗} δu_{2} and hence s_{1} = s[δu_{1}]_{p} →^{∗} s[δw]_{p} ←^{∗} s[δu_{2}]_{p} = s_{2}. Thus s_{1} ↓ s_{2} and →

is locally confluent. □

As for terminating relations confluence and local confluence are equivalent, this yields a decision procedure for the confluence of a terminating PRS.

Corollary 4.8 Confluence of terminating PRSs is decidable.

Example 4.9 The syntax of classical predicate logic can be described by the two types term and form of terms and formulae and by the following constants:

¬ : form → form
∧, ∨ : form → form → form
∀, ∃ : (term → form) → form

For readability we write ∀x.P (x) instead of ∀(λx.P (x)) and use ∧ as an infix.

The negation normal form [7], where ¬ is only applied to atomic formulae, can be defined via the following terminating^{1} rewrite system:

\begin{aligned}¬¬ : & ¬¬P & → & P \\ ¬∧ : & ¬(P ∧ Q) & → & (¬P) ∨ (¬Q) \\ ¬∨ : & ¬(P ∨ Q) & → & (¬P) ∧ (¬Q) \\ ¬∀ : & ¬∀x.P′(x) & → & ∃x.¬P′(x) \\ ¬∃ : & ¬∃x.P′(x) & → & ∀x.¬P′(x) \end{aligned}

1Termination of this and of the other terminating systems in this paper can be proved with the techniques by van de Pol [33].

There are 5 critical pairs, all of which arise by unifying the left-hand side of some rule with the subterm ¬P of ¬¬P, and all of which are joinable. For example

\begin{aligned}& & ∃x.P′(x) \\ & ↗_{¬¬} \\ ¬¬∃x.P′(x) \\ & ↘_{¬∃} \\ & & ¬∀x.¬P′(x) \end{aligned}

is joinable because ¬∀x.¬P′(x) → ∃x.¬¬P′(x) → ∃x.P′(x). Hence the system is confluent, i.e. the negation normal form is uniquely determined.

Example 4.10 Going back to Example 3.4, the pure lambda-calculus, we find that both beta and eta have no critical pairs with themselves, and hence that beta and eta on their own are locally confluent. Since eta also terminates, this implies confluence. For the non-terminating beta we have to wait for the notion of orthogonality to deduce confluence. Combining beta and eta yields two critical pairs:

app(S, T)
↗_{β}
app(abs(λx.app(S, x)), T)
↘_{η}
app(S, T)
abs(λx.F (x))
↗_{β}
abs(λx.app(abs(λy.F (y)), x))
↘_{η}
abs(λy.F (y))

Both critical pairs are trivially joinable. Hence beta + eta is locally confluent. In Section 7 we quote a result which even permits to deduce confluence of beta + eta.

An interesting extension of this system can be obtained by adding a constant ⊥ : term representing the completely undefined term, and the two rules

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

This system has two critical pairs: eta overlaps ⊥app yielding ⟨⊥, abs(λx.⊥)⟩, and beta overlaps ⊥abs yielding ⟨⊥, app(⊥, S)⟩. This is a nice example of completion: if either of the two rules had been omitted, it would have followed from the other one as a critical pair. Hence the system is locally confluent. Unfortunately, we have no theorem which implies confluence.

One of the main selling points of critical pairs has been the fact that they come with a so-called “completion algorithm”: a non-confluent rewrite system can be transformed into an equivalent (w.r.t. the equational theory) but confluent system by adding critical pairs as new reduction rules. As the last example indicates, this is also possible in our higher-order situation. However, higher-order critical pairs may no longer be pattern rewrite rules in case neither of the two components is a pattern. It is easy to see that this unfortunate state cannot arise if the original PRS we start with contains only rewrite rules where both the left and the right-hand sides are patterns, a rare situation in practice.

5 Confluence modulo Equality

The most important consequence of confluence is the uniqueness of normal forms. However, there are cases of non-confluent systems where the normal forms of any term are not unique, but somehow similar to each other.

Example 5.1 In Example 4.9 we showed how to express predicate logic formulae as λ-terms. The prenex normal form can be described by a rewrite system R consisting of the rules

\begin{aligned}Q∗ & : & (Qx.P′(x)) ∗ Q & → & Qx.(P′(x) ∗ Q) \\ ∗Q & : & P ∗ (Qx.Q′(x)) & → & Qx.(P ∗ Q′(x)) \end{aligned}

for all Q ∈ {∀, ∃} and ∗ ∈ {∧, ∨}, together with the rules ¬∀ and ¬∃ from Example 4.9.

This system terminates but is not confluent. This is because (Qx.P′(x)) ∗ (Qy.Q′(y)) gives rise to the critical pair ⟨r, s⟩ := ⟨Qx.(P′(x) ∗ (Qy.Q′(y))), Qy.((Qx.P′(x)) ∗ Q′(y))⟩ which has two distinct normal forms Qx.Qy.(P′(x) ∗ Q′(y)) and Qy.Qx.(P′(x) ∗ Q′(y)).

This example shows that commutativity of quantifiers needs to be taken into account as well. Huet [10] introduced the notion of confluence modulo equality of first-order term rewriting systems. In this section some of his results are lifted to PRSs.

Let us first look at abstract relations → and ∼.

Definition 5.2 A relation → is confluent modulo an equivalence relation ∼ iff

x ∼ y ∧ x →^{∗} x′ ∧ y →^{∗} y′ ⇒ ∃x′′, y′′. x′ →^{∗} x′′ ∧ y′ →^{∗} y′′ ∧ x′′ ∼ y′′

A relation → is called normalizing if for every x there is a y in →-normal form such that

x →^{∗} y.

Lemma 5.3 (Huet [10]) Let → be normalizing and let x↓ denote an arbitrary normal form of x. Then → is confluent modulo an equivalence relation ∼ iff

x ≡ y ⇒ x↓ ∼ y↓

where ≡ is (↔ ∪ ∼)^{∗}.

Thus we can replace the test for equivalence modulo the union of → and ∼ by a test of ∼- equivalence of →-normal forms. If →-normal forms are computable and ∼ is decidable, so is ≡.

Huet also proves a sufficient abstract condition for confluence modulo:

Lemma 5.4 (Huet [10]) Let ⊢⊣ be a symmetric relation, ∼ = ⊢⊣^{∗} and → a relation, such that → · ∼ is terminating. Then → is confluent modulo ∼ iff the conditions A and B are satisfied:

A : ∀x, y, z. x → y ∧ x → z ⇒ y ↓^{∼} z
B : ∀x, y, z. x ⊢⊣ y ∧ x → z ⇒ y ↓^{∼} z

where y ↓^{∼} z :⇔ ∃u, v. y →^{∗} u ∧ z →^{∗} v ∧ u ∼ v.

We will now concentrate on the application of confluence modulo to PRSs.

Definition 5.5 Let R be a PRS and E a symmetric PRS. Then ⟨R, E⟩ is called an equational PRS.

The PRS R defines a relation → on terms as usual. Because E is a symmetric PRS, for every rule (l → r) ∈ E the reverse rule (r → l) is in E as well. As E is a PRS it follows that both l and r are patterns, neither l nor r are free variables and fv(l) = fv(r). The symmetric reduction relation on terms defined by E is denoted by ⊢⊣_{E} or simply ⊢⊣. The transitive-reflexive closure ∼ := ⊢⊣^{∗} is an equivalence relation. It is called the equivalence relation defined by E.

Definition 5.6 An equational PRS ⟨R, E⟩ is called confluent iff the relation → defined by R is confluent modulo the equivalence relation ∼ defined by E.

Lemma 5.3 together with Theorem 3.12 implies that s =_{R∪E} t ⇔ s↕_{β}^{η}↓_{R} =_{E} t↕_{β}^{η}↓_{R} if R is terminating and ⟨R, E⟩ is confluent. Confluence of equational PRSs can be proved by also considering critical pairs between R and E.

Definition 5.7 Let ⟨R, E⟩ be an equational PRS. The critical pairs of E/R are defined as all critical pairs arising from overlapping (analogous to Definition 4.1) the left-hand sides of rules (l_{1} → r_{1}) and (l_{2} → r_{2}), where either (l_{1} → r_{1}) ∈ E and (l_{2} → r_{2}) ∈ R or (l_{1} → r_{1}) ∈ R and (l_{2} → r_{2}) ∈ E.

Definition 5.8 The critical pairs of ⟨R, E⟩ are the union of the critical pairs of R and the critical pairs of E/R.

Finally we can generalize Huet’s characterizations of conditions A and B to equational PRSs:

Lemma 5.9 ⟨R, E⟩ satisfies condition A iff u_{1} ↓^{∼} u_{2} for every critical pair ⟨u_{1}, u_{2}⟩ of R. Proof

1. Assume condition A and let ⟨u_{1}, u_{2}⟩ be a critical pair of R. By Lemma 4.2 there exists a term s such that u_{1} ← s → u_{2}. Hence u_{1} ↓^{∼} u_{2} by condition A.

2. Assume u_{1} ↓^{∼} u_{2} for every critical pair ⟨u_{1}, u_{2}⟩ of R and s → s_{i}, i = 1, 2. By the Critical Pair Lemma 4.6 there are two cases:

(a) s_{1} ↓ s_{2}. By the reflexivity of ∼ if follows that s_{1} ↓^{∼} s_{2}.

(b) There is a critical pair ⟨u_{1}, u_{2}⟩, a substitution δ and p ∈ P os(s), such that s_{i} = s[δu_{i}]_{p}, i = 1, 2. By assumption there are terms u′_{1}, u′_{2}, such that u_{1} →^{∗} u′_{1} ∼ u′_{2} ←^{∗} u_{2}. Theorem 3.9 yields δu_{i} →^{∗} δu′_{i}, i = 1, 2. As ∼ = ⊢⊣^{∗} and ⊢⊣ is defined by a symmetric

PRS, Theorem 3.9 also yields δ(u′_{1}) ∼ δ(u′_{2}). So we get

s_{1} = s[δu_{1}]_{p} →^{∗} s[δu′_{1}]_{p} ∼ s[δu′_{2}]_{p} ←^{∗} s[δu_{2}]_{p} = s_{2}

and hence s_{1} ↓^{∼} s_{2}.
□

Lemma 5.10 Let ⟨R, E⟩ be an equational PRS and R left-linear. Condition B is satisfied iff for every critical pair ⟨u_{1}, u_{2}⟩ of E/R we have u_{1} ↓^{∼} u_{2}. Proof

1. Assume condition B. Let ⟨u_{1}, u_{2}⟩ be a critical pair of E/R. There is a rule (l_{1} → r_{1}) ∈ R and a rule (l_{2} → r_{2}) ∈ E, such that w.l.o.g. l_{1} overlaps l_{2}. By Lemma 4.2 there is a term s, such that u_{1} ← s ⊢⊣ u_{2}. Hence condition B yields u_{1} ↓^{∼} u_{2}. The other case where l_{2} overlaps l_{1} is symmetric.

2. Assume u_{1} ↓^{∼} u_{2} for every critical pair ⟨u_{1}, u_{2}⟩ of E/R. Let s → s_{1} and s ⊢⊣ s_{2}. By definition of → and ⊢⊣ there are rules (l_{1} → r_{1}) ∈ R, (l_{2} → r_{2}) ∈ E, positions p_{1}, p_{2} ∈ P os(s) and substitutions θ_{1}, θ_{2}, such that s/p_{1} = θ_{1}l_{1}, s_{1} = s[θ_{1}r_{1}]_{p_{1}}, s/p_{2} = θ_{2}l_{2}, s_{2} = s[θ_{2}r_{2}]_{p_{2}}. There are three cases:

(a) p_{1} ∥ p_{2}. It is trivial that s_{1} = s[θ_{1}r_{1}]_{p_{1}} ⊢⊣ s[θ_{1}r_{1}]_{p_{1}}[θ_{2}r_{2}]_{p_{2}} ← s[θ_{2}r_{2}]_{p_{2}} = s_{2}. Hence s_{1} ↓^{∼} s_{2} and condition B is satisfied.

(b) p_{2} ≤ p_{1} and q := p_{1}/p_{2}. It follows that s_{1}/p_{2} = (s[θ_{1}r_{1}]_{p_{1}})/p_{2} = (s/p_{2})[θ_{1}r_{1}]_{q} =

(θ_{2}l_{2})[θ_{1}r_{1}]_{q} and (θ_{2}l_{2})/q = (s/p_{2})/q = s/p_{1} = θ_{1}l_{1}. There are two cases:

i. The two redexes do not overlap, i.e. q = q_{1}q_{2}, such that q_{1} ∈ P os(l_{2}) and l_{2}/q_{1} = F (\overline{x_{k}}), where F ∈ fv(l_{2}) (remember: l_{2} is a pattern). Hence θ_{2}(F) is of the form λ\overline{x_{k}}.t and we define the substitution

θ′_{2} := θ_{2} + \{F ↦ λ\overline{x_{k}}.(t[θ_{1}r_{1}]_{q_{2}})\}

Thus we have

t/q_{2} = (θ_{2}(F (\overline{x_{k}})))/q_{2} = (θ_{2}(l_{2}/q_{1}))/q_{2} = ((θ_{2}l_{2})/q_{1})/q_{2} = (θ_{2}l_{2})/q = θ_{1}l_{1}

and hence θ_{2} →^{=} θ′_{2}. Theorem 3.9 yields θ_{2}r_{2} →^{∗} θ′_{2}r_{2}. Let H be a new variable (unused so far in this context) and

\begin{aligned}θ_{0} & := & θ_{2} ∪ \{H ↦ θ′_{2}(F)\} \\ θ′_{0} & := & θ_{0} + \{F ↦ θ′_{2}(F)\} \end{aligned}

and l_{0} := l_{2}[H(\overline{x_{k}})]_{q_{1}}. From θ_{2} →^{=} θ′_{2} is follows that θ_{0} →^{=} θ′_{0}. Applying Theo-

rem 3.9 we get (θ_{2}l_{2})[θ_{1}r_{1}]_{q} = (θ_{2}l_{2})[θ′_{2}(F (\overline{x_{k}}))]_{q_{1}} = θ_{0}l_{0} →^{∗} θ′_{0}l_{0} = θ′_{0}l_{2} = θ′_{2}l_{2} =

θ′_{2}l_{2} ⊢⊣ θ′_{2}r_{2} and therefore

s_{2}/p_{2} = θ_{2}r_{2} →^{∗} θ′_{2}r_{2} ⊢⊣ θ′_{2}l_{2} ←^{∗} (θ_{2}l_{2})[θ_{1}r_{1}]_{q} = s_{1}/p_{2}

Placing it in the context it follows that

s_{2} = s[θ_{2}r_{2}]_{p_{2}}  s[(θ_{2}l_{2})[θ_{1}r_{1}]_{q}]_{p_{2}} = s[θ_{1}r_{1}]_{p_{1}} = s_{1}
↓_{∗}  ↓_{∗}
s[θ′_{2}r_{2}]_{p_{2}} ⊢⊣ s[θ′_{2}l_{2}]_{p_{2}}

and hence s_{1} ↓^{∼} s_{2}. ii. The two redexes overlap, i.e. q ∈ P os(l_{2}) and l_{2}/q is not of the form F (…).

W.l.o.g. assume that bv(l_{2}) ∩ Cod(θ_{2}) = {}. Thus it follows from Lemma 4.4 that there exist a critical pair ⟨u_{1}, u_{2}⟩ and a substitution δ, such that δu_{1} = θ_{2}r_{2} and δu_{2} = θ_{2}(l_{2})[θ_{1}r_{1}]_{q}. By Definition 5.7 ⟨u_{1}, u_{2}⟩ is a critical pair of E/R. By assumption there exist terms u′_{1}, u′_{2}, such that u_{1} →^{∗} u′_{1} ∼ u′_{2} ←^{∗} u_{2}. From Theorem 3.9 it follows that δu_{i} →^{∗} δu′_{i}, i = 1, 2. As ∼ is defined by a symmetric PRS, Theorem 3.9 also yields δu′_{1} ∼ δu′_{2}. So we have s_{2} = s[δu_{1}]_{p_{2}} →^{∗} s[δu′_{1}]_{p_{2}} ∼

s[δu′_{2}]_{p_{2}} ←^{∗} s[δu_{2}]_{p_{2}} = s_{1} and hence s_{1} ↓^{∼} s_{2}.

(c) The last case is p_{1} ≤ p_{2} with q := p_{2}/p_{1}. This case is similar to case 2b, except that

we have to make use of the condition that R is left linear. There are two cases: i. If the two redexes do not overlap, we again have θ_{1}(F) = λ\overline{x_{k}}.t and define

θ′_{1} := θ_{1} + \{F ↦ λ\overline{x_{k}}.(t[θ_{2}r_{2}]_{q_{2}})\}

So we get θ_{1} ⊢⊣^{=} θ′_{1} and Theorem 3.9 yields θ_{1}r_{1} ⊢⊣^{∗} θ′_{1}r_{1}. As the PRS R is assumed to be left-linear, the free variable F occurs only once in l_{1}. Therefore

(θ_{1}l_{1})[θ_{2}r_{2}]_{q} = (θ_{1}l_{1})[θ′_{1}(F (\overline{x_{k}}))]_{q_{1}} = θ′_{1}l_{1} → θ′_{1}r_{1}

It follows that

s_{1} = s[θ_{1}r_{1}]_{p_{1}}  s[(θ_{1}l_{1})[θ_{2}r_{2}]_{q}]_{p_{1}} = s[θ_{2}r_{2}]_{p_{2}} = s_{2}
↓_{∗}  ↓
s[θ_{1}r_{1}]_{p_{1}} ∼ s[θ′_{1}r_{1}]_{p_{1}}

and hence s_{1} ↓^{∼} s_{2}. ii. The case where the two redexes overlap, i.e. q ∈ P os(l_{1}) and l_{1}/q is not of the

form F (…) is completely analogous to case 2(b)ii.

□

Huet gives a simple example which shows that left-linearity of R is essential.

With the help of these lemmas it is now possible to formulate a sufficient criterion for the confluence of an equational PRS.

Theorem 5.11 Let ⟨R, E⟩ be an equational PRS, such that R is left-linear and (→ · ∼) terminates. Then the equational PRS ⟨R, E⟩ is confluent iff u_{1}↓ ∼ u_{2}↓ for all critical pairs ⟨u_{1}, u_{2}⟩ of ⟨R, E⟩, where u_{i}↓ is an arbitrary →-normal form of u_{i}. Proof First note that since → · ∼ terminates, so does → because ∼ is reflexive. Hence the notation t↓ is always defined. The theorem follows almost directly from 5.4, 5.9 and 5.10 because u_{1} ↓^{∼} u_{2} ⇔ u_{1}↓ ∼ u_{2}↓: the ⇐-direction is trivial; for the other direction note that if u_{1} →^{∗} u′_{1} ∼ u′_{2} ←^{∗} u_{2} then confluence implies u_{1}↓ ∼ u_{2}↓ using Lemma 5.3. □

Example 5.12 Now we can prove that the PRS R from Example 5.1 is confluent modulo the symmetric PRS

E := {Qx.Qy.H(x, y) ↔ Qy.Qx.H(x, y) | Q ∈ {∀, ∃}}

As usual, ∼ denotes the equivalence relation defined by E. It is easily checked that all critical pairs of R arise by overlapping Q∗ with ∗Q, and that their two normal forms are ⟨r↓, s↓⟩ = ⟨Qx.Qy.(P′(x) ∗ Q′(y)), Qy.Qx.(P′(x) ∗ Q′(y))⟩. Thus we have r↓ ∼ s↓.

In addition we can overlap the rules Q∗ and ∗Q with the rules in E which gives rise to the critical pairs of E/R, whose normal forms are ⟨Qx.Qy.(H(x, y) ∗ Q), Qy.Qx.(H(x, y) ∗ Q)⟩ and ⟨Qx.Qy.(Q ∗ H(x, y)), Qy.Qx.(Q ∗ H(x, y))⟩, both of which are contained in ∼.

As R is left-linear and (→ · ∼) terminates, it follows from Theorem 5.11 that ⟨R, E⟩ is a confluent equational PRS: modulo quantifier-commutativity, R computes a unique prenex normal form. As =_{E} is decidable the relation =_{R∪E} is decidable by Lemma 5.3.

It is interesting to note that confluence is destroyed by a frequently employed optimization in computing prenex forms:

\begin{aligned}(∀x.P′(x)) ∧ (∀y.Q′(y)) & → & ∀x.(P′(x) ∧ Q′(x)) \\ (∃x.P′(x)) ∨ (∃y.Q′(y)) & → & ∃x.(P′(x) ∨ Q′(x)) \end{aligned}

These new rules give rise to non-trivial critical pairs with R, requiring, for example, the further rule ∀x.∀y.(P′(x) ∧ Q′(y)) → ∀x.(P′(x) ∧ Q′(x)). It seems unlikely that confluence can be regained by some form of completion.

6 Orthogonal Pattern Rewrite Systems

We now turn our attention to a subclass of PRSs, the so called orthogonal ones. An Orthogonal Pattern Rewrite System (OPRS) is a PRS that is left linear and has no critical pairs. This means that there are no rules whose left-hand sides overlap (see Definition 4.1).

Orthogonal term-rewriting systems have a long history [27, 11, 15]. They have been studied very closely because of their similarity to functional programs with pattern matching. The key property of orthogonal systems is their confluence, regardless of whether they terminate or not. We show that this holds for OPRSs as well. The main idea is to define a relation ⩾ on terms such that → ⊆ ⩾ ⊆ →^{∗}, which implies ⩾ = →^{∗}. It is well known that in this case → is confluent if ⩾ has the diamond property: r ⩾ s ∧ r ⩾ t ⇒ ∃u. s ⩾ u ∧ t ⩾ u.

6.1 The Classical Proof

In this section we generalize Aczel’s [1] confluence proof from his “consistent sets of contraction schemes” to arbitrary OPRSs. Note that the former are a proper subset of the latter. The proof proceeds roughly like the one for the untyped λ-calculus due to Tait and Martin-Löf [3]. Although we want to prove the confluence of OPRSs, the first steps towards the standard proof work just as well for HRSs.

Given a fixed HRS R, parallel 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)

\begin{aligned}s_{i} ⩾ t_{i} & (i = 1, …, n) & c(\overline{t_{n}}) = θl & (l → r) ∈ R \\ & c(\overline{s_{n}}) ⩾ θr \end{aligned} (R)

where a is an atom of type \overline{τ_{n}} → τ and s_{i} : τ_{i}. Our relation ⩾ is essentially Aczel’s >. It is instructive to look at a few variations on this theme:

• For orthogonal TRSs, (L) is 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 ⩾ {x ↦ t′}(s′), and we need to add a ⩾ a. The latter is a special case of the above formulation of (A).

• For OPRSs, Nipkow [26] uses an apparently weaker version of (R) which does not allow overlapping reductions: (∀F ∈ fv(l). θ(F) ⩾ θ′(F)) ⇒ θl ⩾ θ′r. Note that for OPRSs the two versions of (R) coincide because left-hand sides do not overlap. Nevertheless it seems that by using the stronger form above, the confluence proof is simplified.

Further variations of this technique appear in the literature [37, 6].

Parallel reduction has a number of interesting properties.

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

Because all rules are of base type we again have

Lemma 6.2 If λx.s ⩾ t′ then t′ = λx.t and s ⩾ t for some t.

More importantly we find that → and ⩾ are strongly related:

Lemma 6.3 → ⊆ ⩾ ⊆ →^{∗}

Proof using the inductive definition of → (Definition 3.6).

• s → t ⇒ s ⩾ t is proved by induction on the structure of s → t. If θl → θr then l = c(\overline{l_{n}}) and Lemma 6.1 implies θl_{i} ⩾ θl_{i} and thus (R) yields θl ⩾ θr. If a(\overline{s_{n}}) → a(\overline{t_{n}}), where s_{k} → t_{k} and s_{i} = t_{i} for all i ≠ k, then s_{i} ⩾ t_{i} for all i by induction hypothesis together with Lemma 6.1. Hence a(\overline{s_{n}}) ⩾ a(\overline{t_{n}}) follows by rule (A). The remaining case is trivial.

• s ⩾ t ⇒ s →^{∗} t is proved by induction on the structure of s ⩾ t. If c(\overline{s_{n}}) ⩾ θr by rule (R), then s_{i} →^{∗} t_{i} follows by induction hypothesis and hence c(\overline{s_{n}}) →^{∗} c(\overline{t_{n}}) = θl → θr. If a(\overline{s_{n}}) ⩾ a(\overline{t_{n}}) by rule (A), s_{i} →^{∗} t_{i} follows by induction hypothesis and hence a(\overline{s_{n}}) →^{∗} a(\overline{t_{n}}). The remaining case is trivial. □

Next we show that ⩾ interacts very nicely with substitutions. The proof is similar to the one of Theorem 3.9 but considerably simpler.

Lemma 6.4 If s ⩾ s′ and θ ⩾ θ′ then θs ⩾ θ′s′. Proof by induction on the order of θ (see Definition 2.1) with a nested induction on the structure of s ⩾ s′.

(A) If s = a(\overline{s_{n}}) ⩾ a(\overline{s′_{n}}) = s′, then by the inner induction hypothesis θs_{i} ⩾ θ′s′_{i}. We distinguish two cases.

1. If a ∉ Dom(θ) (and hence a ∉ Dom(θ′)) then θs = a(\overline{θs_{n}}) ⩾ a(\overline{θ′s′_{n}}) = θ′s′ follows by rule (A).

2. If a ∈ Dom(θ) then θa = λ\overline{y_{n}}.t. By Lemma 6.2 it follows that θ′a = λ\overline{y_{n}}.t′ where t ⩾ t′. Define the substitutions δ = \{\overline{y_{n} ↦ θs_{n}}\} and δ′ = \{\overline{y_{n} ↦ θ′s′_{n}}\} and notice that we have δ ⩾ δ′. If a is of type \overline{τ_{n}} → τ, the definition of ord implies ord(τ_{i}) < ord(\overline{τ_{n}} → τ) and hence ord(δ) < ord(δ′) (note that this also holds in case n = 0). Thus the outer induction hypothesis applies: δt ⩾ δ′t′ because t ⩾ t′. Thus we obtain: θs = (θa)(\overline{θs_{n}}) = δt ⩾ δ′t′ = (θ′a)(\overline{θ′s′_{n}}) = θ′s′.

(L) If s = λx.t, s′ = λx.t′ and t ⩾ t′ then the inner induction hypothesis yields θs = λx.(θt) ⩾ λx.(θ′t′) = θ′s′ using rule (L).

(R) If s = c(\overline{s_{n}}), s_{i} ⩾ s′_{i}, c(\overline{s′_{n}}) = δl and s′ = δr then the inner induction hypothesis implies θs_{i} ⩾ θ′s′_{i}. Since c(\overline{θ′s′_{n}}) = θ′δl rule (R) directly yields θs = c(\overline{θs_{n}}) ⩾ θ′δr = θ′s′. □

The following lemma expresses a simple idea: in a reduction step θl ⩾ s, where l is a linear pattern and does not overlap with any rule, the l-part cannot change, i.e. all reductions must take place inside the terms introduced via θ.

Lemma 6.5 Let R be an OPRS and let l_{0} = λ\overline{x_{n}}.l be a linear pattern that does not overlap any left-hand side of R. If θl ⩾ s and Cod(θ) ∩ \{\overline{x_{n}}\} = \{\} (Dom(θ) ∩ \{\overline{x_{n}}\} = \{\} by convention!) then there exists a substitution θ′ such that θ′l = s, θ|_{fv(l_{0})} ⩾ θ′ and Dom(θ′) = fv(l_{0}). 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) or (R). In either case there are t_{i} such that θl_{i} ⩾ t_{i}. Each λ\overline{x_{n}}.l_{i} is again a linear pattern. Since l_{0} does not overlap any left-hand side of R, it follows easily from Corollary 4.5 that neither do the λ\overline{x_{n}}.l_{i}. Now the induction hypothesis yields substitutions θ_{i} such that θ_{i}l_{i} = t_{i}, θ|_{fv(λ\overline{x_{n}}.l_{i})} ⩾ θ_{i} and Dom(θ_{i}) = fv(λ\overline{x_{n}}.l_{i}). Now let θ′ := ⋃_{i=1}^{m} θ_{i}, which is a well-defined substitution because the Dom(θ_{i}) are disjoint, thanks to linearity. In particular we have θ′l = c(\overline{t_{m}}), θ|_{fv(l_{0})} ⩾ θ′ and Dom(θ′) = fv(l_{0}). If rule (A) was used, θ′l = s as required. Rule (R) cannot have been used because it would mean that c(\overline{t_{m}}) = δl′, where l′ is the left-hand side of a rule in R. Because θ′l = δl′, Corollary 4.5 implies that l_{0} overlaps l′, a contradiction.

2. If l = F (\overline{s_{m}}) then l↓_{η} = F (\overline{y_{m}}) because l is a pattern. Wlog θF = λ\overline{y_{m}}.r. Hence θl = (λ\overline{y_{m}}.r)(\overline{y_{m}})↕_{β}^{η} = r and thus r ⩾ s. Let θ′ = \{F ↦ λ\overline{y_{m}}.s\}. Obviously θ′ has the desired properties.

3. If l = λx.l′ then the claim follows easily from the induction hypothesis. (At this point it becomes important not simply to drop the λx because the remaining l′ might no longer be a pattern.) □

Lemma 6.6 Let R be an OPRS and let l be the left-hand side of a rule in R. If θl = a(\overline{s_{n}}) and s_{i} ⩾ t_{i} then there exists a θ′ such that θ′l = a(\overline{t_{n}}) and θ ⩾ θ′. Proof l must be of the form a(\overline{l_{n}}) and a must be a constant. Since R is orthogonal, none of the l_{i}, all of which are patterns, can overlap with any left-hand side of R. By Lemma 6.5 we obtain substitutions θ_{i} such that θ_{i}l_{i} = t_{i}, Dom(θ_{i}) = fv(l_{i}) and θ|_{fv(l_{i})} ⩾ θ_{i}. Because l is linear, the θ_{i} have disjoint domains and θ′′ := ⋃_{i=1}^{n} θ_{i} is well-defined, θ′′l = a(\overline{t_{n}}) and θ|_{fv(l)} ⩾ θ′′. Using Lemma 6.1 it is trivial to extend θ′′ to θ′ with the desired properties. □

As a corollary we easily obtain

Corollary 6.7 (Coherence) Let R be an OPRS. If (l → r) ∈ R, θl = a(\overline{s_{n}}) and s_{i} ⩾ t_{i}, i = 1, …, n, then there exists a θ′ such that θ′l = a(\overline{t_{n}}) and θr ⩾ θ′r.

We can finally show that ⩾ has the diamond property, i.e. if s ⩾ t_{i}, i = 0, 1, then there exists a u such that t_{i} ⩾ u, i = 0, 1.

Theorem 6.8 If R is an OPRS then ⩾ has the diamond property. Proof We assume that s ⩾ s_{i}, i = 0, 1, and show by induction on the structure of s ⩾ s_{0} that there is a t such that s_{i} ⩾ t, i = 0, 1.

(L) If s = λx.u ⩾ λx.u_{0} = s_{0} and u ⩾ u_{0}, then Lemma 6.2 implies s_{1} = λx.u_{1} and u ⩾ u_{1}. By induction hypothesis there exists a u such that u_{i} ⩾ u and hence s_{i} ⩾ λx.u =: t by (L).

(A) If s = a(\overline{u_{n}}), u_{j} ⩾ u_{0j}, and a(\overline{u_{0n}}) = s_{0}, then s ⩾ s_{1} can only be a consequence of (A) or (R). In either case u_{j} ⩾ u_{1j} and hence by induction hypothesis there are t_{j} such that u_{ij} ⩾ t_{j}. If s ⩾ s_{1} by (A) then s_{1} = a(\overline{u_{1n}}) and thus t := a(\overline{t_{n}}) closes the diamond.

If s ⩾ s_{1} by (R) then a(\overline{u_{1n}}) = θl → θr = s_{1} for suitable θ and (l → r) ∈ R. Coherence yields θ′ such that a(\overline{t_{n}}) = θ′l and s_{1} = θr ⩾ θ′r =: t. By rule (R) we also have s_{0} = a(\overline{u_{1n}}) ⩾ t, thus closing the diamond.

(R) If s = a(\overline{u_{n}}), u_{j} ⩾ u_{0j} and a(\overline{u_{0n}}) = θl → θr = s_{0} then s ⩾ s_{1} can only be a consequence of (A) or (R). In either case u_{j} ⩾ u_{1j} and hence by induction hypothesis there are t_{j} such that u_{ij} ⩾ t_{j}. Coherence yields θ′ such that a(\overline{t_{n}}) = θ′l and s_{0} = θr ⩾ θ′r =: t. By rule (R) we also have a(\overline{u_{1n}}) ⩾ t. If s ⩾ s_{1} by (A) then s_{1} = a(\overline{u_{1n}}), thus closing the diamond.

If s ⩾ s_{1} by (R) then a(\overline{u_{1n}}) = θ_{1}l_{1} → θ_{1}r_{1} = s_{1} for suitable θ_{1} and (l_{1} → r_{1}) ∈ R. Coherence yields θ′_{1} such that a(\overline{t_{n}}) = θ′_{1}l_{1} and θ_{1}r_{1} ⩾ θ′_{1}r_{1}. Therefore θ′l = θ′_{1}l_{1}, i.e. l and l_{1} overlap at ε. Because R is orthogonal this means (l → r) = (l_{1} → r_{1}), θ′ = θ′_{1} and hence s_{1} ⩾ θ′_{1}r_{1} = θ′r = t. □

6.2 Confluence by Complete Superdevelopments

This proof is inspired by Takahashi’s proof of the confluence of semi-orthogonal CLC (conditional lambda calculus) [38] (see also Section 7). Takahashi uses developments, i.e. chains of reductions where no newly created redexes are contracted, to transform terms t into “normal forms” t^{∗} where all redexes in t have been contracted. Her key idea is to show that if t ≥ t′ then t′ ≥ t^{∗}, where ≥ is the standard notion of parallel reduction instead of Aczel’s ⩾.

In the sequel we recast her work in the context of OPRSs using ⩾. Thus the transformation from t to t^{∗} is not a development, but is more like a superdevelopment defined by van Raamsdonk [36] for λ-calculus. We call the transformation t ⩾ t^{∗} a complete superdevelopment. Although the classical proof and Takahashi’s version share the basic lemmas, we find that her auxiliary notion t^{∗} leads to a shorter and more appealing proof of her main lemma (Lemma 6.10) compared to the direct proof of Theorem 6.8. Both proofs are shown to allow the reader a direct comparison.

Definition 6.9 Let R be an OPRS. For every λ-term t in long βη-normal form the term t^{∗} is defined recursively as follows.

1. (λx.t)^{∗} = λx.(t^{∗})

2. a(\overline{t_{n}})^{∗} = a(\overline{t_{n}^{∗}}), if a(\overline{t_{n}^{∗}}) is not a redex.

3. a(\overline{t_{n}})^{∗} = θ(r), if there is a rule (l → r) ∈ R and a substitution θ, such that θ(l) = a(\overline{t_{n}^{∗}}).

where a is an atom of type \overline{τ_{n}} → τ and t_{i} : τ_{i}. The term t^{∗} is well defined, because for OPRSs the rule (l → r) and the substitution θ are uniquely determined by the redex a(\overline{t_{n}^{∗}}).

Lemma 6.10 Let R be an OPRS, ⩾ the corresponding parallel reduction and t a λ-term in long βη-normal form. Then we have t ⩾ t′ ⇒ t′ ⩾ t^{∗} Proof by induction on the size of t. There are three cases:

(L) t = λx.s ⩾ λx.s′ = t′ with s ⩾ s′. By induction hypothesis s′ ⩾ s^{∗} and hence t′ = λx.s′ ⩾ λx.s^{∗} = t^{∗}.

(A) t = a(\overline{t_{n}}) ⩾ a(\overline{t′_{n}}) = t′ with t_{i} ⩾ t′_{i} (i = 1, …, n). By induction hypothesis we have t′_{i} ⩾ t_{i}^{∗} (i = 1, …, n). Now there are two cases:

1. If a(\overline{t_{n}^{∗}}) is no redex, i.e. there are no (l → r) ∈ R and θ such that θl = a(\overline{t_{n}^{∗}}), then

t′ = a(\overline{t′_{n}}) ⩾ a(\overline{t_{n}^{∗}}) = t^{∗}.

2. If a(\overline{t_{n}^{∗}}) is a redex, i.e. there are (l → r) ∈ R and θ such that θ(l) = a(\overline{t_{n}^{∗}}), then

t′ = a(\overline{t′_{n}}) ⩾ θ(r) = t^{∗}.

(R) t = a(\overline{t_{n}}) ⩾ θ(r) for some substitution θ and (l → r) ∈ R such that t_{i} ⩾ t′_{i} (i = 1, …, n) and θ(l) = a(\overline{t′_{n}}). By induction hypothesis we have t′_{i} ⩾ t_{i}^{∗}. It follows from Lemma 6.6 that there is a substitution θ′, such that θ′(l) = a(\overline{t_{n}^{∗}}) and θ ⩾ θ′. Lemma 6.4 yields t′ = θ(r) ⩾ θ′(r) = t^{∗}. □

Theorem 6.11 OPRSs are confluent. Proof It follows from Lemma 6.10 that for any OPRS R the relation ⩾ has the diamond property. Hence → is confluent, because of Lemma 6.3. □

7 Related Work

As already indicated in the introduction, PRSs are closely related to CRSs [14, 16]. Confluence of CRSs has been investigated for orthogonal systems. HRSs are the same as Wolfram’s higher-order term rewriting systems. This abundance of slightly different frameworks has lead to a notion of higher-order rewriting system (HORS) which is parameterized by a “substitution calculus” [30, 28] and generalizes all of the aforementioned frameworks. In the case of HRSs/PRSs the substitution calculus is the simply-typed λ-calculus. It has been shown that all weakly orthogonal HORSs are confluent [30, 28]. Although no notion of critical pair has been defined for HORSs, weak orthogonality for PRSs can be translated as follows:

Definition 7.1 A PRS R is called weakly orthogonal iff it is left-linear and all of its critical pairs are of the form ⟨u, u⟩.

By the above result it follows that all weakly orthogonal PRSs are confluent. This generalizes one of the results obtained in our paper, but at a considerable increase in complexity. Hence we believe that the simplified proofs of confluence for OPRSs which we provide have their own merit. On the other hand, van Oostrom’s techniques yield further dividends, for example that the weakly-orthogonal combination of left-linear and confluent PRSs is again confluent [28, Thm 3.5.13], generalizing a theorem by Nipkow [26, Thm. 6.1].

This result about weakly-orthogonal systems has some interesting consequences. For example, it implies that lambda-calculus with both beta and eta (Example 4.10) is confluent: both rules are left-linear and all critical pairs are of the from ⟨u, u⟩.

Takahashi [38] has investigated a condition called semi-orthogonality which lies in between orthogonality and weak orthogonality: it is strictly weaker than orthogonality but might coincide with weak orthogonality. Takahashi proves confluence of semi-orthogonal “conditional lambda-calculi” (CLC), her own brand of higher-order rewrite systems. As CLC are very close to PRSs, semi-orthogonality can be defined for PRSs in the same way, and her confluence result carries over [20]. It turns out that one of her requirements, namely that the left-hand sides of two different rules do not overlap at position ϵ, is superfluous.

Finally there is a large body of research that is concerned with the combination of λ-calculi and rewrite systems (see, for example, [2]). Although superficially similar to our approach, it is in fact quite different: whereas we consider rewriting modulo the conversions of the λ-calculus, i.e. λ-calculus is a meta-language for describing rewrite systems, they combine β-reduction with other restricted forms of rewrite rules on the same level. This yields relatively strong modularity results for special combinations, e.g. adding β-reduction to a left-linear confluent TRS preserves confluence [22], whereas HRSs aim for a general theory of arbitrary higher-order rules.

Finally it should be mentioned that methods for proving termination of HRSs/PRSs are only just emerging [33, 34, 19, 12]. More work is needed in this area.

Acknowledgment This paper has benefitted enormously from the amazing scrutiny of Ralf Matthes who was volunteered to present very preliminary fragments of it in a seminar.

References

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

[2] Franco Barbanera, Maribel Fernández, and Herman Geuvers. Modularity of strong normalization and confluence in the algebraic λ-cube. In Proc. 9th IEEE Symp. Logic in Computer Science, pages 406–415, 1994.

[3] Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, 2nd edition, 1984.

[4] Hendrik Pieter Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118–309. Oxford University Press, 1992.

[5] Nachum Dershowitz and Jean-Pierre 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.

[6] Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda-calculus. In Ronald V. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, volume 488 of Lect. Notes in Comp. Sci., pages 37–48. Springer-Verlag, 1991.

[7] Jean H. Gallier. Logic for Computer Science. Harper & Row, 1986.

[8] W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.

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

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

[11] Gérard Huet and Jean-Jacques Lévy. Computations in orthogonal rewriting systems. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 395–443. MIT Press, 1991.

[12] Stefan Kahrs. Towards a domain theory for termination proofs. In Jieh Hsiang, editor, Rewriting Techniques and Applications, volume 914 of Lect. Notes in Comp. Sci., pages 241–255. Springer-Verlag, 1995.

[13] Stefan Kahrs. The variable containment problem. Extended abstract. In Workshop on Higher-Order Algebra, Logic and Term Rewriting, September 1995.

[14] Jan Willem Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980.

[15] Jan Willem Klop. Term rewriting systems. In Samson Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 2–116. Oxford University Press, 1992.

[16] Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk. Combinatory reduction systems, introduction and survey. Theoretical Computer Science, 121:279–308, 1993.

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

[18] Carlos Alberto Loría-Sáenz. A Theoretical Framework for Reasoning about Program Construction Based on Extensions of Rewrite Systems. PhD thesis, Universität Kaiserslautern, 1993.

[19] Olav Lysne and Javier Piris. A termination ordering for higher-order rewrite systems. In Jieh Hsiang, editor, Rewriting Techniques and Applications, volume 914 of Lect. Notes in Comp. Sci., pages 26–40. Springer-Verlag, 1995.

[20] Richard Mayr. Konfluenz bei Termersetzungssystemen auf λ-Termen. Master’s thesis, Institut für Informatik, Technische Universität München, 1994.

[21] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

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

[23] Gopalan Nadathur and Dale Miller. An overview of λProlog. In Robert A. Kowalski and Kenneth A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, pages 810–827. MIT Press, 1988.

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

[25] Tobias Nipkow. Functional unification of higher-order patterns. In Proc. 8th IEEE Symp. Logic in Computer Science, pages 64–74, 1993.

[26] Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In M. Bezem and J.F. Groote, editors, Proc. Int. Conf. Typed Lambda Calculi and Applications, volume 664 of Lect. Notes in Comp. Sci., pages 306–317. Springer-Verlag, 1993.

[27] Michael J. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lect. Notes in Comp. Sci. Springer-Verlag, 1977.

[28] Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.

[29] Vincent van Oostrom and Femke van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, Higher-Order Algebra, Logic and Term Rewriting, volume 816 of Lect. Notes in Comp. Sci., pages 276–304. Springer-Verlag, 1994.

[30] Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In A. Nerode, editor, Logical Foundations of Computer Science, volume 813 of Lect. Notes in Comp. Sci., pages 379–392. Springer-Verlag, 1994.

[31] Vincent Padovani. On equivalence classes of interpolation equations. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lect. Notes in Comp. Sci., pages 335–349. Springer-Verlag, 1995.

[32] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.

[33] Jaco van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Möller, and T. Nipkow, editors, Higher-Order Algebra, Logic and Term Rewriting, volume 816 of Lect. Notes in Comp. Sci., pages 305–325. Springer-Verlag, 1994.

[34] Jaco van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lect. Notes in Comp. Sci., pages 350–364. Springer-Verlag, 1995.

[35] Zhenyu Qian. Linear unification of higher-order patterns. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proc. Coll. Trees in Algebra and Programming, volume 668 of Lect. Notes in Comp. Sci., pages 391–405. Springer-Verlag, 1993.

[36] Femke van Raamsdonk. Confluence and superdevelopments. In Claude Kirchner, editor, Proc. 5th Int. Conf. Rewriting Techniques and Applications, volume 690 of Lect. Notes in Comp. Sci., pages 168–182. Springer-Verlag, 1993.

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

[38] Masako Takahashi. λ-calculi with conditional rules. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lect. Notes in Comp. Sci., pages 406–417. Springer-Verlag, 1993.

[39] David A. Wolfram. The Clausal Theory of Types. Cambridge Tracts in Theoretical Computer Science 21. Cambridge University Press, 1993.