TOBIAS NIPKOW AND CHRISTIAN PREHOFER

HIGHER-ORDER REWRITING AND EQUATIONAL REASONING

1. Introduction

In 1972, Knuth and Bendix published their seminal paper (Knuth and Bendix, 1970) which introduced the notion of a critical pair and showed that confluence of terminating term-rewriting systems is decidable. This was the birth of what is now known as term rewriting. Much effort has since gone into the study of term rewriting systems and as a result there is a large body of knowledge about their properties. The study of term rewriting proceeded in parallel and mostly independently of research in λ-calculus. A first attempt to bridge this gap is due to Klop (Klop, 1980), but it was not until the early nineties that a mixture of typed λ-calculus and term rewriting was proposed (Nipkow, 1991; Wolfram, 1993), called higher-order rewrite systems. They allow higher-order functions and their rules are pairs of simply typed λ-terms (as opposed to first-order terms).

As an example of higher-order rewriting consider symbolic differentiation. The function diff(F, X), defined by

diff(λy.F, X) → 0
diff(λy.y, X) → 1
diff(λy.sin(F (y)), X) → cos(F (X)) ∗ diff(λy.F (y), X)
diff(λy.ln(F (y)), X) → diff(λy.F (y), X)/F (X),

computes the differential of a function F at a point X. This set of rewrite rules is shown to be confluent and terminating in (Prehofer, 1995c). With these rules, we can for instance reduce a term as follows:

diff(λy.sin(sin(y)), X) →^{∗} cos(sin(X)) ∗ cos(X)

It is well-known that λ-abstraction is general enough to represent quantification in formulae, abstraction in functional programs, and many other variable-binding constructs (Pfenning and Elliott, 1988). Using this representation, many operations on formulae and programs can be expressed naturally as higher-order rewrite systems.

1

\begin{matrix}c \\ ◯ \end{matrix} 1998 Kluwer Academic Publishers. Printed in the Netherlands.

The objective of this chapter is to survey the results which have been generalized from first-order to higher-order rewrite systems. The aim of this generalization is to lift the rich theory developed around first-order rewrite systems and apply it to systems manipulating higherorder terms, such as program transformers, theorem provers and the like. We will consider the basic properties and techniques and focus on confluence results and equational reasoning.

The contents of the chapter is as follows. 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) and the induced reduction relation on terms, and show how the latter interacts 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 due to Knuth and Bendix is generalized to PRSs. This is extended to confluence modulo equality in Section 5. 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. Section 7 briefly surveys the literature on termination of HRSs, which is still in its infancy. In Section 8 we introduce a unification algorithm for a restricted class of λterms, called higher-order patterns, followed by an algorithm for the full higher-order case in Section 9. Then we focus in Section 10 on calculi for solving equational goals modulo a higher-order rewrite system and show some refinements in Section 11. This chapter combines and summarizes several earlier papers of the authors (Nipkow, 1991; Nipkow, 1993b; Nipkow, 1993a; Mayr and Nipkow, 1998; Prehofer, 1994b; Prehofer, 1995b), where all proofs can be found.

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 (Barendregt, 1992; Hindley and Seldin, 1986).

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.

HIGHER-ORDER REWRITING AND EQUATIONAL REASONING 3

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. 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. This means, for example, λx.(x y) =_{α} λz.(z y) but λx.(x y) ≠_{α} λy.(y y), (λx.x)t =_{β} t and λx.(y x) =_{η} y. 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 (Huet, 1980; Dershowitz and Jouannaud, 1990). 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. Note that there are slightly different approaches to positions in λ-terms, as discussed in (Prehofer, 1995c). As we do not give proofs, this issue is not elaborated here.

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_{n}}.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 ρ.

Two substitutions are equal on a set of variables W, written as θ =_{W} θ′, if θF = θ′F for all F ∈ W. A substitution θ is idempotent iff θ = θθ. We will in general assume that substitutions are idempotent. A substitution θ′ is more general than θ, written as θ′ ≤ θ, if θ = σθ′ for some substitution σ.

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.2).

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 a set of variables 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 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 (Huet, 1980).

3. Higher-Order Rewrite Systems

Higher-Order Rewrite Systems are generalizations of first-order rewrite systems (Baader and Nipkow, 1998; Dershowitz and Jouannaud, 1990) to terms with higher-order functions and bound variables. Since unifiability of λ-terms is undecidable in general (Goldfarb, 1981), 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 (higherorder) 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.

Some examples of higher-order patterns are λx.c(x), F, λx.F (λz.x(z)) and λx, y.F (y, x). 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 Miller (Miller, 1991a): it is decidable whether two patterns are unifiable; if they are unifiable, a most general unifier can be computed. This result is discussed in more detail in Section 8. Qian (Qian, 1996) shows that patterns can be unified in linear time.

DEFINITION 3.2. 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). An 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 Wolfram’s “higher-order term rewriting systems” (Wolfram, 1993).

A few remarks are in order:

− Recall that by convention l, r, s and t are in long βη-normal form. − Due to the restrictions placed on left-hand sides, they must always be of the form f(\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 (Kahrs, 1995b). 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 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 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 full HRSs the situation is different. Although unifiability is known to be undecidable even for second-order λ-terms (Goldfarb, 1981), it is not known whether higher-order matching is decidable. Padovani (Padovani, 1995) showed that 4th order matching is decidable, but the general case is still open.

EXAMPLE 3.3. The standard example of a PRS is pure lambdacalculus 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).

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

DEFINITION 3.4. 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}

all.tex; 26/06/1998; 10:06; p.7

where a is an atom of type \overline{τ_{m+1+n}} → τ.

Of course the two definitions of rewriting are equivalent.

LEMMA 3.5. If R is an HRS then →_{R} and ⇒_{R} coincide.

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 →.

A main theorem about →^{∗} is 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.3).

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

THEOREM 3.7. Let R be an HRS. If s →^{∗} s′ and θ →^{∗} θ′ then θs →^{∗} θ′s′.

This theorem has two obvious corollaries:

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

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

A different version of Theorem 3.7 is shown by Loría (Loría-Sáenz, 1993): he uses conditional rewrite rules whose left-hand sides are patterns.

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.8. 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.9. ((Nipkow, 1993a; Mayr and Nipkow, 1998)). If R is

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

Thus we know that undirected rewriting and equational logic coincide.

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

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

It should be pointed out that Theorem 3.9 fails for rules of function type. The relation ↔^{∗} induced by the one-rule system

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

is strictly weaker than =_{R}: the equivalence 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 (Knuth and Bendix, 1970) showed that confluence of terminating term-rewriting systems is decidable: a simple test of confluence for the finite set of so called critical pairs suffices. This section generalizes the idea to PRSs (see Nipkow (Nipkow, 1991)) and prepares the ground for a further generalization to 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 left-hand 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.

Thus we come to the main result of this section. It looks exactly like its counterpart from the term rewriting literature, but its proof is considerably more complex (see (Mayr and Nipkow, 1998)).

LEMMA 4.2. (Critical Pair Lemma (Nipkow, 1993a)). 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.

It is now easy to prove

THEOREM 4.3. The relation → is locally confluent iff u_{1} ↓ u_{2} for all critical pairs ⟨u_{1}, u_{2}⟩ of the PRS R.

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

COROLLARY 4.4. Confluence of terminating PRSs is decidable.

EXAMPLE 4.5. 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

In the following, P and Q will be variables of type form whereas P′ and Q′ will be of type term → form. For readability we write ∀x.P′(x) instead of ∀(λx.P′(x)) (and similarly for ∃) and use ∧ and ∨ as infix symbols. Note that the rules of λ-calculus automatically guarantee that ∀x.P′(x) matches any universally quantified formulae, whereas ∀x.P matches only those where the bound variable does not occur in the body of the quatifier.

The negation normal form (Gallier, 1986), where ¬ is only applied to atomic formulae, can be defined via the following terminating 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}

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.6. Going back to Example 3.3, 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.

EXAMPLE 4.7. An interesting extension of beta+eta 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 more critical pairs: eta overlaps ⊥app yielding the pair ⟨⊥, 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.

The confluence proof for both of these examples requires stronger theorems. See the end of Section 6.

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.5 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.5.

This system terminates but is not confluent. The reason is that the term (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))⟩

and this critical pair has the 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 (Huet, 1980) introduced the notion of confluence modulo equality of first-order term rewriting systems. Below we present the generalizations of some of his results to PRSs as obtained by Mayr and Nipkow (Mayr and Nipkow, 1998).

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 (Huet, 1980)). 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 →∪∼ by a test of ∼-equivalence of →-normal forms. If →-normal forms are computable and ∼ is decidable, so is ≡.

In the sequel · denotes composition of relations:

→ · ∼ = {(x, z) | ∃y. x → y ∧ y ∼ z}

We will now concentrate on the application of confluence modulo to PRSs. To make things work we have to assume that the PRS modulo which we compute is symmetric, i.e. for every rule l → r it also contains the rule r → l. Although this is trivial to achieve by adding the converse of every rule, it means that, because the result must still be a PRS, both l and r must be patterns, neither l nor r are free variables and fv(l) = fv(r).

DEFINITION 5.4. 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. 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.5. An equational PRS ⟨R, E⟩ is called confluent iff the relation → defined by R is confluent modulo the equivalence relation ∼ defined by E.

DEFINITION 5.6. 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.7. The critical pairs of ⟨R, E⟩ are the union of the critical pairs of R and the critical pairs of E/R.

The following reformulation of Huet’s theorem yields as a sufficient condition for the confluence of an equational PRS and is due to (Mayr and Nipkow, 1998):

THEOREM 5.8. Let ⟨R, E⟩ be an equational PRS, such that R is leftlinear 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}.

EXAMPLE 5.9. 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.8 that ⟨R, E⟩ is a confluent equational PRS: modulo quantifiercommutativity, 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 (O’Donnell, 1977; Huet and Lévy, 1991; Klop, 1992). 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.

In the following, we sketch the confluence proof for OPRSs. The proof proceeds roughly like the one for the untyped λ-calculus due to Tait and Martin-Löf (Barendregt, 1984). For an alternative proof in the style of Takahashi (Takahashi, 1993) we refer to (Mayr and Nipkow, 1998).

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}.

Parallel reduction has a number of interesting properties.

LEMMA 6.1. s ⩾ s holds for all terms s in long βη-normal form.

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

LEMMA 6.2. → ⊆ ⩾ ⊆ →^{∗}

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

LEMMA 6.3. If s ⩾ s′ and θ ⩾ θ′ then θs ⩾ θ′s′.

As a consequence of some fairly technical lemma we obtain

LEMMA 6.4. 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 θ ⩾ θ′.

As a direct consequence this yields

COROLLARY 6.5. (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.

Coherence is best explained in terms of the following diagram:

a(s_{1},…,s_{n}) = θl → θr
∨^{/}  ∨^{/}  ∨^{/}
a(t_{1},…,t_{n}) = θ′l → θ′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.6. (Nipkow, 1993b; Mayr and Nipkow, 1998) If R is an OPRS then ⩾ has the diamond property.

The proof is by induction on the definition of ⩾. As a corollary we obtain

COROLLARY 6.7. Every OPRS is confluent.

Going back to Example 3.3, we find that beta and eta on their own each form an OPRS. Thus the above corollary yields confluence of beta and eta reduction for untyped λ-calculus. However, as shown in Example 4.6, both rules together give rise to critical pairs and thus do not form an OPRS.

A more complex analysis of reductions shows that all weakly orthogonal PRSs are confluent (Oostrom and Raamsdonk, 1994; Raamsdonk, 1996). Although these papers define weak orthogonality directly rather than in terms of critical pairs, it can be translated as follows:

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

Looking at the critical pairs in Example 4.6 once more, we find that they are both of the form ⟨u, u⟩. Hence the combination of beta and eta reduction is a weakly orthogonal PRS and therefore confluent as well.

Van Oostrom (Oostrom, 1997) has gone one step further and proved an analogue of Huet’s parallel closure condition (Huet, 1980) for PRSs. He calls a PRS R development-closed if s{∘ \atop →_{R}} r for every critical pair ⟨r, s⟩ of R, where s\underrightarrow{∘}_{R} r means that a “complete development” (in the sense of λ-calculus) of all R-redexes of s yields r. He shows that every left-linear development-closed PRS is confluent. It is easy to verify that the four rule system in Example 4.7 is development-closed.

7. Termination

Termination of rewriting is undecidable, but there exist many results for terminating classes of rewrite systems or semi-decision procedures (see for example (Dershowitz and Jouannaud, 1990)). Termination of some HRS R can be proved by exhibiting a terminating ordering > such that →_{R} ⊆ >. The latter property can be proved by showing that R ⊆ > and that this extends to →_{R}. For the first-order case, there exist large classes of orderings that are known to extend to →_{R}. In the higher-order case, such orderings are more difficult, as > must be preserved by higher-order substitutions.

One current approach (Kahrs, 1995a; Pol, 1994) aims at finding appropriate semantic domains in order to interpret higher-order rewriting. In particular, strictly monotonic interpretations of terms in monotonic domains are used in (Pol, 1994). That is, (higher-order) symbols are interpreted by monotonic functions. It is shown that an HRS terminates if the interpretation of the right hand-side is smaller than the lefthand side for each rule. Alternatives which extend syntactic orderings on first-order terms (Dershowitz and Jouannaud, 1990) to higher-order terms are pursued in (Loría-Sáenz, 1993; Avenhaus and Loría-Sáenz, 1994; Lysne and Piris, 1995; Jouannaud and Rubio, 1996). These papers use first-order interpretations on (often restricted) λ-terms. A main problem is that basic first-order properties of orderings, e.g. stability under substitutions is more involved in λ-calculus.

A confluent and terminating HRS R is called convergent. It follows from Corollary 3.10 for convergent R that s =_{R} t can be decided by comparing s↓_{R} and t↓_{R}.

8. Unification of Higher-Order Patterns

Unification of higher-order patterns is a special case of higher-order unification that proceeds similarly to first-order unification. The important result is that most general unifiers exist for patterns. In addition to the first-order case, bound variables must be treated correctly: the unification problem

λx.sin(F (x)) =^{?} λx.sin(cos(x))

has solution {F ↦ λy.cos(y)}, whereas

λx.F =^{?} λx.sin(cos(x))

is unsolvable, as the left-hand side does not depend on x.

The following set of rules for unification of higher-order patterns is due to Nipkow (Nipkow, 1993a). The transformations in Figure 1 work on lists (in Prolog’s [ | ] notation), as the order of application is important for termination (Nipkow, 1993a). The problem is that the algorithm introduces new variables on the way and repeating this eagerly may lead to non-termination. For instance, consider {c(X) = Y, Y =^{?} X} ⇒_{P U} {X =^{?} Y_{1}, c(Y_{1}) =^{?} X}. Here the occurs check applies only after an elimination whereas repeated imitation diverges.

The algorithm coincides with standard first-order unification algorithms, e.g. (Jouannaud and Kirchner, 1991), for first-order terms. Notice that in the Flex-Flex rules any permutation of the bound variables \overline{z_{p}} is sufficient for computing a most general unifier.

It can be shown that PU terminates (Grobauer, 1997). More importantly, it computes most general unifiers in the following sense:

THEOREM 8.1. ((Miller, 1991b; Nipkow, 1993a)). Let S_{0} be a list of unification problems s =^{?} t, where both s and t are patterns.

1.If S_{0} has a unifier, then S_{0} has exactly one PU-normal form, namely [ ], and for every reduction sequence S_{0} ⇒^{θ_{1}} S_{1} … ⇒^{θ_{n}} [ ] the composition θ_{n} ⋯ θ_{1} is a most general unifier.

2.If S_{0} has no unifier, every PU-normal form of S_{0} is distinct from [ ].

Deletion

[t =^{?} t | S] ⇒ S

Decomposition

[λ\overline{x_{k}}.f(\overline{t_{n}}) =^{?} λ\overline{x_{k}}.f(\overline{t′_{n}}) | S] ⇒ [\overline{λ\overline{x_{k}}.t_{n} =^{?} λ\overline{x_{k}}.t′_{n}} | S]

Elimination

[F =^{?} t | S] ⇒^{θ} θS if F ∉ fv(t) and

where θ = {F ↦ t}

Imitation/Projection

[λ\overline{x_{k}}.F (\overline{y_{n}}) =^{?} λ\overline{x_{k}}.v(\overline{t′_{m}}) | S] ⇒^{θ} [\overline{λ\overline{x_{k}}.H_{m}(\overline{y_{n}}) =^{?} λ\overline{x_{k}}.θt′_{m}} | θS]

where θ = \{F ↦ λ\overline{y_{n}}.v(\overline{H_{m}(\overline{y_{n}})})\}, v is a constant or v ∈ \{\overline{y_{n}}\}, \overline{H_{m}} are fresh variables, and F ∉ fv(λ\overline{x_{k}}.v(\overline{t′_{m}}))

Flex-Flex Same

[λ\overline{x_{k}}.F (\overline{y_{n}}) =^{?} λ\overline{x_{k}}.F (\overline{y′_{n}}) | S] ⇒^{θ} θS

where θ = \{F ↦ λ\overline{x_{n}}.F′(\overline{z_{p}})\} F′ is a fresh variable, and \{\overline{z_{p}}\} = \{y_{i} | y_{i} = y′_{i}\}, i = 1, …, n

Flex-Flex Diff

[λ\overline{x_{k}}.F (\overline{y_{n}}) =^{?} λ\overline{x_{k}}.F′(\overline{y′_{m}}) | S] ⇒^{θ} θS if F ≠ F′ and where

\begin{aligned}θ & = & \{F ↦ λ\overline{y_{n}}.H(\overline{z_{p}}), \\ & & F′ ↦ λ\overline{y′_{m}}.H(\overline{z_{p}})\}, \end{aligned}

H is a fresh variable, and \{\overline{z_{p}}\} = \{\overline{y_{n}}\} ∩ \{\overline{y′_{m}}\}

Figure 1. System PU for Pattern Unification

9. Higher-Order Unification by Transformations

We present in the following a version of the transformation system PT for higher-order unification of Snyder and Gallier (Snyder and Gallier, 1989).

Full higher-order unification is substantially more difficult than pattern unification. First, the former is undecidable and second, there may not be a single most general unifier. We even have to resort to a weaker form of unification, called pre-unification, as there may not even be a minimal complete set of unifiers (MCSU (Prehofer, 1997)). Pre-unification differs from unification by the handling of so-called flexflex pairs. These are equations of the form λ\overline{x_{k}}.P (…) =^{?} λ\overline{x_{k}}.P′(…). Huet (Huet, 1976) showed that such pairs of order three may not have a MCSU: there may exist an infinite chain of unifiers, one more general than the other, without any most general one. The important idea to remedy this situation is that flex-flex pairs are guaranteed to have at least one unifier, e.g. \{P ↦ λ\overline{x_{m}}.a, P′ ↦ λ\overline{x_{n}}.a\}. The idea of preunification is to handle flex-flex pairs as constraints and not to attempt to solve them explicitly.

Consider solving an equation λ\overline{x_{k}}.F (\overline{t_{n}}) =^{?} λ\overline{x_{k}}.v(\overline{t′_{m}}) where v is not a free variable. Such equations are called flex-rigid. Clearly, for any solution θ to F the term θF (\overline{t_{n}}) must have (after β-reduction) the symbol v as its head. There are two possibilities:

− In the first case, v already occurs in (the solution to) some t_{i}. For instance, consider the equation F (a) =^{?} a, where {F ↦ λx.x} is a solution based on a projection. In general, a projection binding for F is of the from \{F ↦ λ\overline{x_{n}}.x_{i}(…)\}. As some argument, here a, is carried to the head of the term, such a binding is called projection. This name was introduced in (Jensen and Pietrzykowski, 1976). − The second case is that the head of the solution to F is just the desired symbol v. For instance, in the last example, an alternative solution is {F ↦ λx.a}. This is called imitation. Notice that imitation is not possible if v is a bound variable.

To solve a flex-rigid pair, the strategy is to guess an appropriate imitation or projection binding only for one rigid symbol, here a, and thus approximate the solution to F. Unification proceeds by iterating this process which focuses only on the outermost symbol. Roughly speaking, the rest of the solution for F is left open by introducing new variables. Formally, this is defined as follows.

Assume an equation λ\overline{x_{k}}.F (\overline{t_{n}}) =^{?} λ\overline{x_{k}}.v(\overline{t′_{m}}), where all terms are in long βη-normal form. An imitation binding for F is of the form

F ↦ λ\overline{x_{n}}.f(\overline{H_{m}(\overline{x_{n}})})

where \overline{H_{m}} are new variables of appropriate type. A projection binding for F is of the form

F ↦ λ\overline{x_{n}}.x_{i}(\overline{H_{p}(\overline{x_{n}})})

where \overline{H_{p}} are new variables with \overline{H_{p} : τ_{p}} and x_{i} : \overline{τ_{p}} → τ. A partial binding is an imitation or a projection binding. Notice that in the above definition, the bindings are not written in long βη-normal form. The long βη-normal form of an imitation or projection binding can be written as

F ↦ λ\overline{x_{n}}.v(\overline{λ\overline{z_{j_{p}}}.H_{p}(\overline{x_{n}}, \overline{z_{j_{p}}})}).

A full exhibition of the types involved can be found in (Snyder and Gallier, 1989).

The transformation rules PT for higher-order unification in Figure 2 consist of the basic rules for unification, such as Deletion, Elimination and Decomposition plus the two rules explained above: Imitation and Projection. The rules work on pairs of terms to be unified, written as {u =^{?} v, …}, and return a set of new pairs. We extend the transformation rules on goals to sets of goals in the canonical way: \{s =^{?} t\} ∪ S ⇒^{θ} \{\overline{s_{n} =^{?} t_{n}}\} ∪ θS if s =^{?} t ⇒^{θ} \{\overline{s_{n} =^{?} t_{n}}\}. We abbreviate a sequence of transformations

G_{0} ⇒_{P T}^{δ_{1}} G_{1} ⇒_{P T}^{δ_{2}} … ⇒_{P T}^{δ_{n−1}} G_{n−1} ⇒_{P T}^{δ_{n}} G_{n}

by ⇒^{∗} _{P T}^{δ}, where δ = δ_{n} … δ_{1}.

A substitution θ is a pre-unifier of s and t if the equation θs =^{?} θt can be simplified by Deletion, Decomposition and Elimination to a set of Flex-Flex pairs. In other words, θs =^{?} θt only differ at subterms that have variable heads.

The following soundness lemma is easy to show:

THEOREM 9.1. System PT is a sound transformation system for higher-order pre-unification.

THEOREM 9.2. (Completeness of PT). If s =^{?} t has solution θ, i.e. θs = θt, then {s =^{?} t} ⇒^{∗} _{P T}^{δ} F such that δ is more general than θ and F is a set of flex-flex goals.

Deletion

t =^{?} t ⇒ ∅

Decomposition

λ\overline{x_{k}}.v(\overline{t_{n}}) =^{?} λ\overline{x_{k}}.v(\overline{t′_{n}}) ⇒ \{\overline{λ\overline{x_{k}}.t_{n} =^{?} λ\overline{x_{k}}.t′_{n}}\}

Elimination

F =^{?} t ⇒^{θ} ∅ if F ∉ fv(t) and
where θ = {F ↦ t}

Imitation

λ\overline{x_{k}}.F (\overline{t_{n}}) =^{?} λ\overline{x_{k}}.f(\overline{t′_{m}}) ⇒^{θ} \{\overline{λ\overline{x_{k}}.H_{m}(\overline{θt_{n}}) =^{?} λ\overline{x_{k}}.θt′_{m}}\},

where θ = \{F ↦ λ\overline{x_{n}}.f(\overline{H_{m}(\overline{x_{n}})})\} is an appropriate imitation binding

Projection

λ\overline{x_{k}}.F (\overline{t_{n}}) =^{?} λ\overline{x_{k}}.v(\overline{t′_{m}}) ⇒^{θ} \{λ\overline{x_{k}}.θt_{i}(\overline{H_{j}(\overline{t_{n}})}) =^{?} λ\overline{x_{k}}.v(\overline{θt′_{m}})\},

where θ = \{F ↦ λ\overline{x_{n}}.x_{i}(\overline{H_{j}(\overline{x_{n}})})\} is an appropriate projection binding

Figure 2. System PT for Higher-Order Unification

The above result does not show a practically important property of PT: it only computes incomparable solutions, if used properly. For this, we have to examine the application of rules more carefully. When applying the rules of system PT to a set of equations, there are two sources of non-determinism:

1. Which rule to apply

2. to which equation.

It was shown in the early work by Huet (Huet, 1976) that completeness does not depend on how the equations are selected. This is implicit in the proof in (Snyder and Gallier, 1989), and is also explained at the end of this section. Furthermore, the only branching occurs when both Imitation and Projection apply to some equation. In other words, application of the first three rules is deterministic (Snyder and Gallier, 1989). When examining the substitutions computed for the Imitation and the Projection rules, it can be seen that only incomparable solutions are computed.

Since higher-order unification is undecidable in general, we are interested in classes where higher-order unification is decidable. In many works concerning higher-order unification (Wolfram, 1993; Baader and Siekmann, 1994; Nadathur, 1987; Paulson, 1994), it is observed that non-termination of higher-order (pre-)unification occurs very rarely in practice. A large part of these observations are due to higher-order patterns, which cover most practical cases.

There are a few other results. It is shown in (Prehofer, 1994a) that the unification of a linear higher-order pattern s with an arbitrary second-order term that shares no variables with s is decidable. In particular, we do not have to resort to pre-unification, flex-flex pairs can be finitely solved in this case. The main application of this result is the unification of linear left-hand sides of rewrite rules with second-order terms, as employed in higher-order narrowing, which is the topic of the next section.

10. Lazy Narrowing

In this section, we introduce the narrowing calculus which is used for solving equational goals with free (or logic) variables modulo an equational theory. This is also called equational or E-unification.

In our setting we consider directed goals of the form s →^{?} t for ground terms t, where a substitution θ is a solution if θs →^{∗}_{R} t. Note that we have to generalize this to θs →^{∗}_{R} θt in most theorems. To solve undirected equations of the form s =_{R}^{?} t wrt confluent rewrite rules, we can just add a rule (X =^{?} X) → true and solve (s =^{?} t) →^{?} true and hence treat =^{?} as a new function symbol. The focus on directed goals simplifies many technicalities and is essential for programming applications as shown later.

For the narrowing rules we need some notation. Let s ↔^{?} t stand for one of s →^{?} t and t →^{?} s. For goals of the form s ↔^{?} t, the rules are intended to preserve the orientation of ↔^{?}. We extend the transformation rules on goals to sets of goals in the canonical way: \{\overline{s →^{?} t}\} ∪ S ⇒^{θ} \{\overline{s_{n} →^{?} t_{n}}\} ∪ θS if s →^{?} t ⇒^{θ} \{\overline{s_{n} →^{?} t_{n}}\}. For a sequence ⇒^{θ_{1}} … ⇒^{θ_{n}} of LN steps, we write ⇒^{∗}^{θ}, where θ = θ_{n} … θ_{1}.

System LN for lazy higher-order narrowing essentially consists of the rules for higher-order unification of the last section plus the Lazy Narrowing rules in Figure 3. Note that the rules for higher-order unification apply, which are presented with undirected goals apply in both directions to directed goals. For a first impression of lazy narrowing, we start with a few examples. Assuming the rules

\begin{aligned}map(F, [X|Y]) & → & [F (X)|map(F, Y)] \\ map(F, []) & → & [] \\ father(mary) & → & john \\ father(john) & → & art \end{aligned}

we solve the goal R(mary) →^{?} art by

R(mary) →^{?} art  ⇒_{LN} Narrowing at Variable,
R ↦ λx.father(R_{1}(x))
R_{1}(mary) →^{?} john, art →^{?} art  ⇒_{LN} Deletion or Decomposition
R_{1}(mary) →^{?} john  ⇒_{LN} Narrowing at Variable,
R_{1} ↦ λx.father(R_{2}(x))
R_{2}(mary) →^{?} mary, john →^{?} john ⇒_{LN} Projection
mary →^{?} mary, john →^{?} john  ⇒^{∗}_{LN} Solved by Deletion

Thus we get the solution R ↦ λx.father(father(x)) by composing the partial bindings. Notice that the trivial solution R ↦ λx.art is also possible here, but it is easy to avoid by further constraints as e.g. in the following example.

Another, slightly more involved example is the following. We use functional evaluation in this example for brevity.

map(F, [mary, john]) →^{?} [john, art] ⇒^{∗}_{LN} Evaluation,

Decomposition

F (mary) →^{?} john, F (john) →^{?} art ⇒^{∗}_{LN} Narrowing at Variable,

F ↦ λx.father(H(x))

H(mary) →^{?} mary, john →^{?} john,

father(H(john)) →^{?} art  ⇒_{LN} P rojection, H ↦ λx.x

mary →^{?} mary, john →^{?} john, father(john) →^{?} art

The last goals are easily solved by evaluation and Deletion. This yields the solution F ↦ λx.father(x). Observe how in the last examples Lazy Narrowing at Variable is used to compute solutions for functional Lazy Narrowing with Decomposition

λ\overline{x_{k}}.f(\overline{t_{n}}) →^{?} λ\overline{x_{k}}.t ⇒ \{\overline{λ\overline{x_{k}}.t_{n} →^{?} λ\overline{x_{k}}.l_{n}}, λ\overline{x_{k}}.r →^{?} λ\overline{x_{k}}.t\}
where f(\overline{l_{n}}) → r is an \overline{x_{k}}-lifted rule

Lazy Narrowing at Variable

λ\overline{x_{k}}.H(\overline{t_{n}}) →^{?} λ\overline{x_{k}}.t ⇒^{θ} \{\overline{λ\overline{x_{k}}.H_{m}(\overline{θt_{n}}) →^{?} λ\overline{x_{k}}.l_{m}},
λ\overline{x_{k}}.r →^{?} λ\overline{x_{k}}.θt\}

where f(\overline{l_{m}}) → r is an \overline{x_{k}}-lifted rule,

and θ = \{H ↦ λ\overline{x_{n}}.f(\overline{H_{m}(\overline{x_{n}})})\}
with fresh variables \overline{H_{m}}

Figure 3. Narrowing Rules of System LN

variables. Although this rule is very powerful, it also has a high degree of non-determinism and will be restricted in later refinements.

There are two sources of non-determinism for such systems of transformations: which rules to apply and how to select the equations. Completeness fortunately does not depend on the goal selection, as each subgoal is independently solvable.

DEFINITION 10.1. A (higher-order) narrowing calculus N is complete for some HRS R if the following holds: If s →^{?} t has solution θ, i.e. θs →^{∗}_{R} θt, then {s →^{?} t} ⇒^{∗} _{N}^{δ} F such that δ is more general, modulo the newly added variables, than θ. Moreover, F is a set of flex-flex goals.

THEOREM 10.2. System LN is complete.

The above result has been stated for PRS in (Prehofer, 1994b) and proved for HRS in (Prehofer, 1995c). It should be noted that other approaches to narrowing and superposition found in the literature, see e.g. (Bachmair, 1991), are not suitable in the higher-order case. The difference is that many superposition calculi model rewrite steps at inner positions in terms, whereas lazy narrowing strictly works outsidein. As the term structur of λ-terms is much more involved, these calculi are not suitable in the higher-order case, as examined in (Prehofer, 1994b; Prehofer, 1995c)

11. Refinements for Convergent Rewrite Rules

This section develops several refinements which exploit the determinism of convergent systems. For convergent systems it is sufficient to consider normalized solutions and particular reductions in the proofs, which allows to remove redundancies in the solutions. The following results have been proved for PRS in (Prehofer, 1995b; Prehofer, 1995c) and are are generalized to HRS in (Prehofer, 1997).

There exist several other refinements (Prehofer, 1994b; Prehofer, 1995a; Prehofer, 1995c) if linearity of the left-hand sides of rewrite rules is assumed, which is common in programming applications, e.g. functional programs. For a class of even further restricted orthogonal rewrite rules, called inductively-sequential, an optimal calculus was presented in (Hanus and Prehofer, 1996). It is optimal in the sense that it produces only incomparable substitutions.

11.1. Avoiding Lazy Narrowing at Variables

An essential refinement is to avoid narrowing at a variable occurring in a term of the form X(\overline{x_{n}}) for a R-normalized substitution θ with an HRS R. For a pattern X(\overline{x_{n}}), reducibility of a term θX(\overline{x_{n}}) implies that θ is not R-normalized, hence violating the assumption on θ. This result generalizes the first-order case, as for first-order terms narrowing at variable position is not needed. It is an important optimization, as narrowing at variable positions is highly unrestricted and thus creates large search spaces. We strongly conjecture that in practice, as in higher-order logic programming (Michaylov and Pfenning, 1992), most terms are patterns and hence narrowing at variables is not needed very often.

To establish this result we need innermost reductions which evaluate terms at inner redices first. For any solution there exists an innermost reduction, if R is convergent.

DEFINITION 11.1. System LNN is defined as the restriction of system LN where Lazy Narrowing at Variable is not applied to goals of the form λ\overline{x_{n}}.X(\overline{y_{m}}) →^{?} t if λ\overline{x_{n}}.X(\overline{y_{m}}) is a higher-order pattern.

THEOREM 11.2. System LNN is complete for a convergent HRS R wrt R-normalized solutions.

11.2. Simplification via Normalization

Simplification by normalization of goals is one of the earliest and one of the most important optimizations (Hanus, 1992). Its motivation is to prefer deterministic reduction over search within narrowing.

Observe that normalization coincides with deterministic evaluation as in functional languages. Also, as shown below, deterministic operations are possible as soon as the left-hand side of a goal has been simplified to a term with a constructor at its root. For instance, with the rule f(1) → 1, we can simplify a goal f(1) →^{?} g(Y) by {f(1) →^{?} g(Y), …} ⇒ {1 →^{?} g(Y), …} and deterministically detect a failure.

For oriented goals, normalization is only complete for goals s →^{?} t, where θt is in R-normal form for a solution θ. For instance, it suffices if t is a ground term in R-normal form. For most applications, this is no real restriction and corresponds to the intuitive understanding of directed goals.

DEFINITION 11.3. Normalizing Lazy Narrowing is defined as the rules of LNN plus arbitrary simplification steps on the left-hand sides of goals.

THEOREM 11.4. Normalizing Lazy Narrowing is complete for convergent R wrt R-normalized solutions.

11.3. Deterministic Eager Variable Elimination

Eager variable elimination is a particular strategy which has been examined for general equational unification. The idea is to apply the Elimination rule as a deterministic operation whenever possible. That is, when elimination applies to a goal, all other rule applications are not considered.

Eager variable elimination is of great practical value. Consider for instance the following example using the rules of Section 1:

{λx.diff(λy.1 ∗ ln(F (y)), x) →^{?} λx.cos(x)/sin(x)} ⇒^{∗} Eval.
{λx.diff(λy.F (y), x)/F (x) →^{?} λx.cos(x)/sin(x)} ⇒^{∗} Decomp.

{λx.diff(λy.F (y), x) →^{?} λx.cos(x),

λx.F (x) →^{?} λx.sin(x)}  ⇒^{∗} Elim.

At this point, we have to chose which goal to solve first. Since on the second Elimination applies, we prefer this and consider no further rules.

It remains the goal

{λx.diff(λy.sin(y), x) →^{?} λx.cos(x)}

Unfortunately, it is an open problem of general (first-order) equational unification if eager variable elimination is still complete (Snyder, 1991). In our case, with oriented goals, we obtain more precise results by differentiating the orientation of the goal to be eliminated. As we consider oriented equations, we can distinguish two cases of variable elimination. For goals X →^{?} t, elimination is deterministic as we can show that for a solution θ, θt is in R-normal form.

THEOREM 11.5. Lazy Narrowing with eager variable elimination on goals X →^{?} t where X ∉ fv(t) is complete for convergent HRS R

12. Examples of Equational Reasoning

In the following, we present examples of reasoning in higher-order logic; more example can be found in (Prehofer, 1995c). We first come back to the introductory example in Section 1 and then consider an example of program transformation.

Assume the rules for differentiation of Section 1, plus the simplification rule x ∗ 1 → x. With these rules, we can solve the following goal with System LN:

{λx.diff(λy.ln(F (y)), x) →^{?} λx.cos(x)/sin(x)} ⇒^{∗} Evaluation for diff
{λx.diff(λy.F (y), x)/F (x) →^{?} λx.cos(x)/sin(x)} ⇒^{∗} Decomposition

{λx.diff(λy.F (y), x) →^{?} λx.cos(x),

λx.F (x) →^{?} λx.sin(x)}  ⇒^{∗} Elimination
{λx.diff(λy.sin(y), x) →^{?} λx.cos(x)}  ⇒^{∗} Evaluation
{λx.cos(x) ∗ diff(λy.y, x) →^{?} λx.cos(x)}  ⇒^{∗} Evaluation
{λx.cos(x) →^{?} λx.cos(x)}  ⇒^{∗} Decomposition

∅

With a more refined narowing strategy (Prehofer, 1995c), it can be shown that there is no search necessary to find the solution F ↦ λx.sin(x).

The utility of higher-order unification for program transformations has been shown nicely by Huet and Lang (Huet and Lang, 1978) and has been developed further in (Pfenning and Elliott, 1988; Hannan and Miller, 1988). The following example, taken from (Field and Harrison, 1988), applies unfold/fold program transformation and requires full instead of strict equality. We assume the following standard rules for lists

\begin{aligned}map(F, [X|R]) & → & [F (X)|map(F, R)] \\ foldl(G, [X|R]) & → & G(X, foldl(G, R)) \end{aligned}

Now assume writing a function g(F, L) by

g(F, L) → foldl(λx, y.plus(x, y), map(F, L))

that first maps F onto a list and then adds the elements via the function plus. This simple implementation for g is inefficient, since the list must be traversed twice. The goal is now to find an equivalent function definition that is more efficient. We can specify this with higher-order terms in a syntactic fashion by one simple equation:

∀f, x, l.g(f, [x|l]) = B(f(x), g(f, l))

The variable B represents the body of the function to be computed and the first argument of B allows to use f(x) in the body. The scheme on the right only allows recursing on l for g.

To solve this equation, we add a rule X = X → true and then apply narrowing. This yields the solution θ = {B ↦ λfx, rec.plus(fx, rec)}, where fx and rec are bound variables. The solution can be illustrated as follows:

g(f, [x|l]) = θB(f(x), g(f, l)) = plus(f(x), g(f, l)).

This shows the more efficient definition of g. In this example, simplification can reduce the search space for narrowing drastically: it suffices to simplify the goal to

\begin{matrix}λf, x, l.plus(f(x), foldl(plus, map(f, l))) & =^{?} \\ λf, x, l.B(f(x), foldl(plus, map(f, l))), \end{matrix}

where narrowing with the newly added rule X = X → true yields the two goals

\begin{aligned}λf, x, l.plus(f(x), foldl(plus, map(f, l))) & →^{?} & λf, x, l.X(f, x, l), \\ λf, x, l.B(f(x), foldl(plus, map(f, l))) & →^{?} & λf, x, l.X(f, x, l). \end{aligned}

These can be solved by pure higher-order unification.

References

Avenhaus, J. and C. Loría-Sáenz: 1994, ‘Higher-Order Conditional Rewriting and Narrowing’. In: J.-P. Jouannaud (ed.): Constraints in Computational Logics, Vol. 845 of Lect. Notes in Comp. Sci. pp. 269–284.

Baader, F. and T. Nipkow: 1998, Term Rewriting and All That. Cambridge

University Press. To appear. Baader, F. and J. H. Siekmann: 1994, ‘Unification Theory’. In: D. Gabbay, C.

Hogger, and J. Robinson (eds.): Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press.

Bachmair, L.: 1991, Canonical Equational Proofs, Progress in Theoretical

Computer Science. Birkhäuser. Barendregt, H. P.: 1984, The Lambda Calculus, its Syntax and Semantics.

North-Holland, 2nd edition. Barendregt, H. P.: 1992, ‘Lambda Calculi with Types’. In: S. Abramsky, D.

Gabbay, and T. Maibaum (eds.): Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, pp. 118–309.

Dershowitz, N. and J.-P. Jouannaud: 1990, ‘Rewrite Systems’. In: J. van Leeuwen (ed.): Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B. Elsevier—MIT Press, pp. 243–320.

Field, A. J. and P. G. Harrison: 1988, Functional Programming. Addison-

Wesley. Gallier, J. H.: 1986, Logic for Computer Science. Harper & Row. Goldfarb, W. D.: 1981, ‘The Undecidability of the second-order unification

problem’. Theoretical Computer Science 13, 225–230. Grobauer, B.: 1997, ‘A verified Unification Algorithm for Higher-Order Pat-

ters’. Master’s thesis, Institut für Informatik, TU München. Hannan, J. and D. Miller: 1988, ‘Uses of higher-order unification for imple-

menting program transformers’. In: Fifth International Logic Programming Conference. pp. 942–959.

Hanus, M.: 1992, ‘Improving Control of Logic Programs by Using Functional Logic Languages’. In: Programming Language Implementation and Logic Programming, Vol. 631 of Lect. Notes in Comp. Sci. pp. 1–23.

Hanus, M. and C. Prehofer: 1996, ‘Higher-Order Narrowing with Definitional Trees’. In: H. Ganzinger (ed.): Rewriting Techniques and Applications, Vol. 1103 of Lect. Notes in Comp. Sci. pp. 138–152.

Hindley, J. R. and J. P. Seldin: 1986, Introduction to Combinators and λ-

Calculus. Cambridge University Press. Huet, G.: 1976, ‘Résolution d’équations dans les langages d’ordre 1, 2, ..., ω’.

Thèse d’Etat, Université Paris VII.

Huet, G.: 1980, ‘Confluent Reductions: Abstract Properties and Applications

to Term Rewriting Systems’. J. ACM 27, 797–821. Huet, G. and B. Lang: 1978, ‘Proving and Applying Program Transformations

Expressed with Second-Order Patterns’. Acta Informatica 11, 31–55. Huet, G. and J.-J. Lévy: 1991, ‘Computations in Orthogonal Rewriting Sys-

tems’. In: J.-L. Lassez and G. Plotkin (eds.): Computational Logic: Essays in Honor of Alan Robinson. MIT Press, pp. 395–443.

Jensen, D. and T. Pietrzykowski: 1976, ‘Mechanizing ω-order type theory

through unification’. Theoretical Computer Science 3, 123–171. Jouannaud, J.-P. and C. Kirchner: 1991, ‘Solving Equations in Abstract Alge-

bras: A Rule-Based Survey of Unification’. In: J.-L. Lassez and G. Plotkin (eds.): Computational Logic: Essays in Honor of Alan Robinson. MIT Press, pp. 257–321.

Jouannaud, J.-P. and A. Rubio: 1996, ‘A recursive path ordering for higherorder terms in η-long β-normal form’. In: H. Ganzinger (ed.): Rewriting Techniques and Applications, Vol. 1103 of Lect. Notes in Comp. Sci. pp. 108–122.

Kahrs, S.: 1995a, ‘Towards a Domain Theory for Termination Proofs’. In: J. Hsiang (ed.): Rewriting Techniques and Applications, Vol. 914 of Lect. Notes in Comp. Sci. pp. 241–255.

Kahrs, S.: 1995b, ‘The Variable Containment Problem. Extended Abstract’.

In: Workshop on Higher-Order Algebra, Logic and Term Rewriting. Klop, J. W.: 1980, Combinatory Reduction Systems, Mathematical Centre

Tracts 127. Mathematisch Centrum, Amsterdam. Klop, J. W.: 1992, ‘Term Rewriting Systems’. In: S. Abramsky, D. Gabbay,

and T. Maibaum (eds.): Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, pp. 2–116.

Knuth, D. E. and P. Bendix: 1970, ‘Simple Word Problems in Universal Algebra’. In: J. Leech (ed.): Computational Problems in Abstract Algebra. Pergamon Press, pp. 263–297.

Loría-Sáenz, C. A.: 1993, ‘A Theoretical Framework for Reasoning about Program Construction Based on Extensions of Rewrite Systems’. Ph.D. thesis, Universität Kaiserslautern.

Lysne, O. and J. Piris: 1995, ‘A Termination Ordering for Higher-Order Rewrite Systems’. In: J. Hsiang (ed.): Rewriting Techniques and Applications, Vol. 914 of Lect. Notes in Comp. Sci. pp. 26–40.

Mayr, R. and T. Nipkow: 1998, ‘Higher-Order Rewrite Systems and their

Confluence’. Theoretical Computer Science 192, 3–29. Michaylov, S. and F. Pfenning: 1992, ‘An Empirical Study of the Runtime Be-

haviour of Higher-Order Logic Programs’. In: D. Miller (ed.): Proc. Workshop on λProlog. University of Pennsylvania, pp. 257–271. Available as Tech. Rep. MS-CIS-92-86.

Miller, D.: 1991a, ‘A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification’. Journal of Logic and Computation 1(4), 497–536.

Miller, D.: 1991b, ‘A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification’. In: P. Schroeder-Heister (ed.): Extensions of Logic Programming. pp. 253–281.

Nadathur, G.: 1987, ‘A Higher-Order Logic as the Basis for Logic Program-

ming’. Ph.D. thesis, University of Pennsylvania, Philadelphia. Nipkow, T.: 1991, ‘Higher-Order Critical Pairs’. In: 6th IEEE Symp. Logic in

Computer Science. pp. 342–349. Nipkow, T.: 1993a, ‘Functional Unification of Higher-Order Patterns’. In: 8th

IEEE Symp. Logic in Computer Science. pp. 64–74. Nipkow, T.: 1993b, ‘Orthogonal Higher-Order Rewrite Systems are Confluent’.

In: M. Bezem and J. Groote (eds.): Proc. Int. Conf. Typed Lambda Calculi and Applications, Vol. 664 of Lect. Notes in Comp. Sci. pp. 306–317.

O’Donnell, M. J.: 1977, Computing in Systems Described by Equations, Vol. 58

of Lect. Notes in Comp. Sci. Springer-Verlag. Oostrom, V. v.: 1997, ‘Developing Developments’. Theoretical Computer Sci-

ence 175, 159–181. Oostrom, V. v. and F. v. Raamsdonk: 1994, ‘Weak Orthogonality Implies Con-

fluence: The Higher-Order Case’. In: A. Nerode (ed.): Logical Foundations of Computer Science, Vol. 813 of Lect. Notes in Comp. Sci. pp. 379–392.

Padovani, V.: 1995, ‘On Equivalence Classes of Interpolation Equations’. In: M. Dezani-Ciancaglini and G. Plotkin (eds.): Typed Lambda Calculi and Applications, Vol. 902 of Lect. Notes in Comp. Sci. pp. 335–349.

Paulson, L. C.: 1994, Isabelle: A Generic Theorem Prover, Vol. 828 of Lect.

Notes in Comp. Sci. Springer-Verlag. Pfenning, F. and C. Elliott: 1988, ‘Higher-Order Abstract Syntax’. In: Proc.

SIGPLAN ’88 Symp. Programming Language Design and Implementation. pp. 199–208.

Pol, J. v. d.: 1994, ‘Termination Proofs for Higher-Order Rewrite Systems’. In: J. Heering, K. Meinke, B. Möller, and T. Nipkow (eds.): Higher-Order Algebra, Logic and Term Rewriting, Vol. 816 of Lect. Notes in Comp. Sci. pp. 305–325.

Prehofer, C.: 1994a, ‘Decidable Higher-order Unification Problems’. In: A. Bundy (ed.): Automated Deduction — CADE-12, Vol. 814 of Lect. Notes in Comp. Sci.

Prehofer, C.: 1994b, ‘Higher-order Narrowing’. In: 9th IEEE Symp. Logic in

Computer Science. pp. 507–516. Prehofer, C.: 1995a, ‘A Call-by-Need Strategy for Higher-Order Functional-

Logic Programming’. In: J. Lloyd (ed.): Logic Programming. pp. 147–161. Prehofer, C.: 1995b, ‘Higher-Order Narrowing with Convergent Systems’. In:

4th Int. Conf. Algebraic Methodology and Software Technology, Vol. 936 of Lect. Notes in Comp. Sci.

Prehofer, C.: 1995c, ‘Solving Higher-Order Equations: From Logic to Programming’. Technical Report I9508, Technische Universität, München. PhD Thesis.

Prehofer, C.: 1997, Solving Higher-order Equations: From Logic to Program-

ming. Birkhäuser PCTS Series. Qian, Z.: 1996, ‘Unification of Higher-Order Patterns in Linear Time and

Space’. Journal of Logic and Computation 6, 315–341. Raamsdonk, F. v.: 1996, ‘Confluence and Normalization for Higher-Order

Rewriting’. Ph.D. thesis, Vrije Universiteit, Amsterdam. Snyder, W.: 1991, A Proof Theory for General Unification. Birkäuser. Snyder, W. and J. Gallier: 1989, ‘Higher-Order Unification Revisited: Com-

plete Sets of Transformations’. J. Symbolic Computation 8, 101–140. Takahashi, M.: 1993, ‘λ-Calculi with Conditional Rules’. In: M. Bezem and

J. Groote (eds.): Typed Lambda Calculi and Applications, Vol. 664 of Lect. Notes in Comp. Sci. pp. 406–417.

Wolfram, D. A.: 1993, The Clausal Theory of Types, Cambridge Tracts in Theoretical Computer Science 21. Cambridge University Press.