Functional Unification of Higher-Order Patterns^{∗}

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

Abstract

The complete development of a unification algorithm for so-called higher-order patterns, a subclass of λterms, is presented. The starting point is a formulation of unification by transformation, the result a directly executable functional program. In a final development step the result is adapted to λ-terms in de Bruijn’s notation. The algorithms work for both simply typed and untyped terms.

1 Introduction

Unification of typed λ-terms (aka higher-order unification) is the basic inference mechanism for many theorem provers and programming languages based on typed λ-calculus [1, 15, 11, 16]. The implementations of most, if not all of these systems, rely on the unification algorithm invented by Gérard Huet [6]. Although the problem itself is undecidable and infinite sets of most general unifiers may exist, Huet’s algorithm performs surprisingly well in practice. This observation lead Dale Miller to the discovery of a subclass of λterms, so-called patterns, which behave almost like first-order terms w.r.t. unification: unification is decidable and unifiable terms have most general unifiers, which are easy to compute. In practice these patterns turn up very frequently, which explains why Huet’s algorithm is well-behaved most of the time. Miller [8] formulated a unification algorithm for patterns which can ultimately be seen as a specialized and improved version of Huet’s algorithm: imitation and projection coincide and flex-flex pairs can be solved. His results were taken up by Pfenning [17], who extended them to the Calculus of Constructions, and by Nipkow [12, 13], who reformulated and used them in the context of rewrite systems over simply typed λ-terms. Miller also showed that full higher-order unification can be regained by embedding pattern-unification in a search procedure [9], thus separating the treatment of variable binding from the search aspect.

The unification algorithm presented by Miller applies to quantified λ-terms (both untyped and simply typed) and is described informally (although rigorously); the algorithms by Pfenning and Nipkow are formulated at a fairly high level. The purpose of this paper is to present the development of a simple yet efficient implementation of unification of both untyped and simply typed patterns. The algorithm is written in a functional style and follows the structure of unification for first-order terms.

In the future Miller’s algorithm is bound to acquire a similar importance in the field of automatic term manipulations (including theorem proving, logic programming, term rewriting and programming languages) that first-order unification has had for a long time. In fact, ELF has already abandoned full higher-order unification in favour of patterns [7], some implementations of λProlog treat patterns specially (by solving flex-flex patterns, rather than suspending them [10]), and Isabelle^{1} [15] is about to follow suit. Hence it is vital that a simple and yet practical implementation of this algorithm is available.

After fixing the notation and the basic definitions (Section 2), a high-level description of unification using transformation rules (Section 3) is gradually refined to a directly executable functional algorithm (Sections 4–9). Initially we restrict our attention to simply typed terms, but at some point in the development the algorithm starts to work for both typed and untyped terms. An adaption of this algorithm to λ-terms in de Bruijn’s notation is presented in Section 10.

2 Notation

2.1 λ-Calculus

We use standard λ-calculus notation subject to the following conventions: s and t denote terms, F, G and H free variables, x, y and z bound variables, a and b atoms (i.e. bound variables or constants), and c constants. Binary application of λ-terms is written s.t in order to avoid confusion with application in the programming language used for expressing the algorithms. We follow the convention of keeping bound and free variables disjoint. Hence the language of λterms is defined by the following grammar:

∗Appeared in Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993.

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

‡Address: Institut für Informatik, Technische Universität München, Postfach 20 24 20, W-8000 München 2, Germany.

Email: Tobias.Nipkow@Informatik.TU-Muenchen.De

1Larry Paulson’s implementation of Huet’s algorithm already contains some of the ideas of pattern unification.

t = F | x | c | λx.t | (t_{1}.t_{2})

Although it is extremely convenient to distinguish bound and free variables on a syntactic level, it introduces so-called loose bound variables as in λx.y, where y is a bound variable without a corresponding enclosing binder. Such loose bound variables should essentially be treated like constants, except that renaming of bound variables has to take care not to capture such loose variables. The free variables in a term are denoted by FV(.).

Lists of variables and terms are written as \overline{x_{n}} and \overline{s_{n}}, where n is the length of the list. In particular λ\overline{x_{n}}.s is short for λx_{1} … λx_{n}.s and a(\overline{s_{n}}) is short for the iterated application ((⋯ (a.s_{1}) ⋯).s_{n}). Lists can be turned into sets by enclosing them in braces. Conversely, given a set \{\overline{x_{m}}\}, the x_{i} are all assumed to be distinct and the list \overline{x_{m}} denotes an arbitrary enumeration of the elements in \{\overline{x_{m}}\}.

Definition 2.1 A term t in β-normal form is 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 nonpatterns are F (c), λx.F (x, x) and λx.F (F (x)). In the sequel all terms are either implicitly assumed to be patterns or are patterns by construction.

Substitutions, i.e. finite mappings from variables to terms, are denoted by θ; tθ is the application of θ to t (including renaming of bound variables in t), tθ↓_{β} the β-normal form of tθ. Individual substitutions are written as {v_{1} ↦ t_{1}, …, v_{n} ↦ t_{n}} where the v_{i} can be free or bound. Composition of substitutions is ∘: t(θ′ ∘ θ) = (tθ)θ′. The restriction of θ to a set of variables V is written θ|_{V}.

2.2 Algorithms

All algorithms are written in a mixture of simplified Standard ML and mathematics. In particular we rely on the following basic combinators:

\begin{aligned}x :: [y_{1}, …, y_{n}] & = & [x, y_{1}, …, y_{n}] \\ [x_{1}, …, x_{m}]@[y_{1}, …, y_{n}] & = & [x_{1}, …, x_{m}, y_{1}, …, y_{n}] \\ map f [x_{1}, …, x_{m}] & = & [f x_{1}, …, f x_{m}] \end{aligned}

\begin{aligned}foldl f a (x :: xs) & = & foldl f (f a x) xs \\ foldl f a [] & = & a \end{aligned}

\begin{aligned}zip (x :: xs) (y :: ys) & = & (x, y) :: zip xs ys \\ zip [] [] & = & [] \end{aligned}

assoc x ((y, z) :: ps) = if x = y then [z]
else assoc x ps
assoc x []  = []

Above, assoc is the lookup function for association lists. Returning either an empty or a singleton list avoids the introduction of a new data type with two constructors. Two-letter variable names ending in “s” stand for lists.

Lists can also be defined by comprehension [2]:

[e(i) | 1 ≤ i ≤ n ∧ P (i)]

is the list [e(i_{1}), …, e(i_{k})] where {i_{1}, …, i_{k}} = {i | 1 ≤ i ≤ n ∧ P (i)}.

3 Unification by transformation

The starting point of the development is an extremely transparent but very high-level description of unification using five simple rewrite rules shown in Fig. 1, adapted and simplified from [12].

We assume that

α : α-equivalent terms are identified, and

η : terms are simply typed and in η-expanded form, except for the arguments of free variables, which are in η-normal form, i.e. bound variables.

Both assumptions are later relaxed.

The transformation rules are of the form e → ⟨E′, θ′⟩ and should be read as follows: the unification problem e is reduced to the list of unification problems E′ under the new substitution θ′. Note that in rule (1) the binder λx can be removed because free and bound variables are from disjoint sets and can always be distinguished. In rule (3) the terms H_{i}(\overline{x_{m}}) may need to be η-expanded in case s_{i} is of function type. The free variable H is assumed to be a new variable in each instance.

λx.s =^{?} λx.t → ⟨[s =^{?} t], {}⟩  (1)
a(\overline{s_{n}}) =^{?} a(\overline{t_{n}}) → ⟨[s_{1} =^{?} t_{1}, …, s_{n} =^{?} t_{n}], \{\}⟩  (2)
F (\overline{x_{m}}) =^{?} a(\overline{s_{n}}) → ⟨[H_{1}(\overline{x_{m}}) =^{?} s_{1}, …, H_{n}(\overline{x_{m}}) =^{?} s_{n}], \{F ↦ λ\overline{x_{m}}.a(\overline{H_{n}(\overline{x_{m}})})\}⟩  (3)

where F ∉ FV(\overline{s_{n}}) and a is a constant or a ∈ \{\overline{x_{m}}\}

F (\overline{x_{n}}) =^{?} F (\overline{y_{n}}) → ⟨[], \{F ↦ λ\overline{x_{n}}.H(\overline{z_{p}})\}⟩  (4)

where \{\overline{z_{p}}\} = \{x_{i} | x_{i} = y_{i}\}

F (\overline{x_{m}}) =^{?} G(\overline{y_{n}}) → ⟨[], \{F ↦ λ\overline{x_{m}}.H(\overline{z_{p}}), G ↦ λ\overline{y_{n}}.H(\overline{z_{p}})\}⟩  (5)

where F ≠ G and \{\overline{z_{p}}\} = \{\overline{x_{m}}\} ∩ \{\overline{y_{n}}\}

Figure 1: Unification by transformation

The actual transformation relation is defined by

⟨e :: E, θ⟩ ⟶ ⟨E′@(Eθ′↓_{β}), θ′ ∘ θ⟩ if e → ⟨E′, θ′⟩.

Using lists rather than sets is intentional. Treating the unification problems as sets can result in divergence: try {F =^{?} c(G), G =^{?} c(F)}.

Theorem 3.1 A list of pattern unification problems E has a solution iff ⟨E, {}⟩ ⟶^{∗} ⟨[], θ⟩, in which case θ|_{FV(E)} is a most general unifier of E.

Proof sketch. Roughly speaking, correctness and completeness follow because e → ⟨E′, θ′⟩ implies that eθ′ and E′ have the same set of unifiers and because the five rules cover all solvable cases. To prove termination, first convert all higher-order patterns to firstorder terms by dropping all λs and all arguments of free variables. The resulting set of transformation rules is a variation on first-order unification as, for example, studied by Dershowitz and Jouannaud [5] and can be shown to terminate employing the same methods used there. □

The correctness of all further versions of pattern unification can be established by program transformation and data refinement techniques. The main correctness arguments in each step are sketched but details of the proofs have been left out.

Example 3.2 The following transformations show the unification of λx, y.F (x) and λx, y.c(G(y, x)):

⟨[λx, y.F (x) =^{?} λx, y.c(G(y, x))], {}⟩  ⟶
⟨[λy.F (x) =^{?} λy.c(G(y, x))], {}⟩  ⟶
⟨[F (x) =^{?} c(G(y, x))], {}⟩  ⟶
⟨[H(x) =^{?} G(y, x)], {F ↦ λx.c(H(x))}⟩ ⟶

\begin{matrix}⟨[], \{ & F ↦ λx.c(H′(x)), H ↦ λx.H′(x), \\ G ↦ λy, x.H′(x)\}⟩ \end{matrix}

4 Going functional

The first development step is a serialization of the above inference rules leading to the functional program displayed in Fig. 2. The free variable H is assumed to be a new variable in each instance. The condition m ≠ n prepares the ground for untyped terms; for simply typed terms, m = n is implied by F = G and by a = b.

The correctness of this algorithm can be shown by relating it back to the transformation rules. The functions rigidrigid, flexflex1 and flexflex2 correspond to rules (2), (4) and (5). Function proj, and hence flexrigid, corresponds to a sequence of transformations by rule (3), interleaved with rules (4) and (5). The precise relationship is:

Lemma 4.1 Let t = sθ↓_{β}. If proj \overline{x_{m}} θ s = δ ∘ θ and F ∉ FV(t) then ⟨(F (\overline{x_{m}}) =^{?} t) :: E, θ′⟩ ⟶^{∗} ⟨Eδ′, δ′ ∘ θ′⟩ such that δ′|_{FV(t)} = δ ∘ \{F ↦ λ\overline{x_{m}}.t\}.

Proof by structural induction on s. □

Intuitively, proj \overline{x_{m}} θ s tries to eliminate all loose bound variables from t which are not in \{\overline{x_{m}}\}. It does so by replacing free variables by projections onto that subset of their arguments contained in \{\overline{x_{m}}\}.

Example 4.2 The unification problem from Example 3.2 is first stripped down to F (x) =^{?} c(G(y, x)). Now flexrigid calls proj {x} θ (c(G(y, x))), where θ = {F ↦ λx.c(G(y, x))} (note the loose bound y!), which in turn composes {G ↦ λy, x.H(x)} with θ, thus eliminating y from G(y, x).

Note that the above algorithm, and all further ones, may fail for two reasons:

1. Exception fail is raised explicitly. This means that the input is not unifiable.

unif θ (s, t) = case (sθ↓_{β}, tθ↓_{β}) of ; \begin{matrix}(λx.s, λx.t) ⇒ & unif θ (s, t) \\ (s, t) ⇒ & cases θ (s, t) \end{matrix}

\begin{aligned}cases θ (F (\overline{x_{m}}), G(\overline{y_{n}})) & = & flexflex(F, \overline{x_{m}}, G, \overline{y_{n}}, θ) \\ cases θ (F (\overline{x_{m}}), t) & = & flexrigid(F, \overline{x_{m}}, t, θ) \\ cases θ (t, F (\overline{x_{m}})) & = & flexrigid(F, \overline{x_{m}}, t, θ) \\ cases θ (a(\overline{s_{m}}), b(\overline{t_{n}})) & = & rigidrigid(a, \overline{s_{m}}, b, \overline{t_{n}}, θ) \end{aligned}

flexflex(F, \overline{x_{m}}, G, \overline{y_{n}}, θ) = if F = G then flexflex1(F, \overline{x_{m}}, \overline{y_{n}}, θ) else flexflex2(F, \overline{x_{m}}, G, \overline{y_{n}}, θ)
flexflex1(F, \overline{x_{m}}, \overline{y_{n}}, θ) = if m ≠ n then fail else \{F ↦ λ\overline{x_{m}}.H([x_{i} | 1 ≤ i ≤ m ∧ x_{i} = y_{i}])\} ∘ θ
flexflex2(F, \overline{x_{m}}, G, \overline{y_{n}}, θ) = let \{\overline{z_{k}}\} = \{\overline{x_{m}}\} ∩ \{\overline{y_{n}}\} in \{F ↦ λ\overline{x_{m}}.H(\overline{z_{k}}), G ↦ λ\overline{y_{n}}.H(\overline{z_{k}})\} ∘ θ
flexrigid(F, \overline{x_{m}}, t, θ) = if F ∈ FV(t) then fail else proj \{\overline{x_{m}}\} (\{F ↦ λ\overline{x_{m}}.t\} ∘ θ) t
rigidrigid(a, \overline{s_{m}}, b, \overline{t_{n}}, θ) = if a ≠ b orelse m ≠ n then fail else foldl unif θ (zip \overline{s_{m}} \overline{t_{n}})
proj V θ s = case sθ↓_{β} of
λx.t ⇒ proj (V ∪ {x}) θ t
c(\overline{s_{m}}) ⇒ foldl (proj V) θ \overline{s_{m}}
x(\overline{s_{m}}) ⇒ if x ∈ V then foldl (proj V) θ \overline{s_{m}} else fail
F (\overline{y_{m}}) ⇒ let \{\overline{z_{n}}\} = \{\overline{y_{m}}\} ∩ V in \{F ↦ λ\overline{y_{m}}.H(\overline{z_{n}})\} ∘ θ

Figure 2: Functional unification

2. A function is called with an argument which is not covered by any of the clauses defining the function. This means that the algorithm was applied to arguments outside its domain, namely non-patterns.

In a real implementation it may be advantageous to test for non-patterns during unification, possibly branching to a full higher-order unification algorithm. To make sure that our algorithms reject all nonpatterns, one has to impose the restriction that \overline{x_{m}} only matches a list of distinct variables. Unsurprisingly, the solution computed in the repeated variable case is not a most general unifier: try λx.F (x, x) =^{?} λx.x.

5 On-the-fly α-conversion

Let us now drop assumption α and take α-conversion (almost) seriously.

unif θ (s, t) = case (sθ↓_{β}, tθ↓_{β}) of ; \begin{matrix}(λx.s, λy.t) ⇒ & unif θ (s, t\{y ↦ x\}) \\ (s, t) ⇒ & cases θ (s, t) \end{matrix}

We have simply converted λy.t to λx.t{y ↦ x}. However, in case t contains a loose bound x introduced by removing some corresponding λx, this x is now captured. Hence we have to assume that in a term λx.s, s does not contain a subterm λx.t, i.e. nested abstractions bind distinct variables. If necessary, this assumption can be enforced by preprocessing. In addition we have to ensure that renaming, for example during β-reduction, cannot introduce bound variables that have already been used. The obvious solution is to generate a completely new bound variable in each renaming step. With the introduction of de Bruijn’s indices in Section 10 all such complications disappear.

6 Implementing substitutions

Now we implement substitutions as association lists of variables and terms. Consequently we replace substitutions of the form {F ↦ t} ∘ θ by (F, t) :: θ. The expression sθ↓_{β} now becomes devar θ s, where devar is a “lazy” form of substitution application: only if s is of the form F (…) is F replaced by F θ; otherwise s

cases θ (s, t) = case (strip s, strip t) of ; \begin{matrix}((F, ys), (G, zs)) ⇒ & flexflex(F, ys, G, zs, θ) \\ ((F, ys), ) ⇒ & flexrigid(F, ys, t, θ) \\ ( , (F, ys)) ⇒ & flexrigid(F, ys, s, θ) \\ ((a, ss), (b, ts)) ⇒ & rigidrigid(a, ss, b, ts, θ) \end{matrix}

proj V θ s = case strip(devar θ s) of
(λx.t, []) ⇒ proj (V ∪ {x}) θ t
(c, ss) ⇒ foldl (proj V) θ ss
(x, ss) ⇒ if x ∈ V then foldl (proj V) θ ss else fail
(F, \overline{y_{m}}) ⇒ let \{\overline{z_{n}}\} = \{\overline{y_{m}}\} ∩ V in (F, λ\overline{y_{m}}.H(\overline{z_{n}})) :: θ

Figure 3: Pattern-matching

is returned unchanged:

devar θ (F (\overline{x_{n}})) = case assoc F θ of

\begin{matrix}[λ\overline{y_{n}}.t] ⇒ & devar θ (t\{\overline{y_{n} ↦ x_{n}}\}) \\ [] ⇒ & F (\overline{x_{n}}) \end{matrix}

devar θ s  = s

This is justified because the case-expressions in unif and proj examine only the outermost layer of a term. However, the test F ∈ FV(t) in flexrigid may examine all of t and is therefore replaced by occ F θ t where

occ F θ G  = (F = G) orelse

case assoc G θ of ; \begin{matrix}[s] ⇒ & occ F θ s \\ [] ⇒ & false \end{matrix}

occ F θ (s.t) = occ F θ s orelse occ F θ t
occ F θ (λx.s) = occ F θ s
occ F θ  = false

7 On-the-fly η-expansion

The following modifications remove the need to work with η-expanded simply typed terms. This is not just relevant for applications to untyped terms. It also paves the way for terms containing type variables which may get instantiated during unification (as in λProlog and Isabelle): such instantiations may require further η-expansions. It is not difficult to see that the η-expansions below are correct for typed terms as well. Hence the resulting algorithm, and all further refinements, apply to both typed and untyped terms alike.

However, we still retain the assumption that all arguments to free variables must be bound variables. This merely simplifies the notation and can be relaxed, for example, by a preprocessing phase that η-normalizes the arguments of free variables.

unif θ (s, t) = case (devar θ s, devar θ t) of ; \begin{matrix}(λx.s, λy.t) ⇒ & unif θ (s, t\{y ↦ x\}) \\ (λx.s, t) ⇒ & unif θ (s, t.x) \\ (s, λx.t) ⇒ & unif θ (s.x, t) \\ (s, t) ⇒ & cases θ (s, t) \end{matrix}

devar θ s = case strip s of

(F, ys) ⇒ case assoc F θ of ; \begin{matrix}[t] ⇒ & devar θ (red(t, ys)) \\ [] ⇒ & s \end{matrix}

⇒ s

\begin{aligned}red(λx.s, y :: ys) & = & red(s\{x ↦ y\}, ys) \\ red(s, y :: ys) & = & red(s.y, ys) \\ red(s, []) & = & s \end{aligned}

strip t = \begin{matrix}let & \begin{matrix}strip (f.t, ts) = strip (f, t :: ts) \\ strip (t, ts) = (t, ts) \end{matrix} \\ in strip (t, []) \end{matrix}

Calling red(s, ys) applies s to the list of variables ys, performing as many β-reductions as possible. Since terms are no longer η-expanded, the number of λs at the front of s and the length of ys may differ.

8 Pattern-matching

As a final step towards an executable algorithm we remove all occurrences of (programming language) patterns of the form a(\overline{s_{m}}) in favour of the destructor strip. This has already occurred in the last version of devar. The necessary changes to cases and proj are shown in Fig. 3.

The point is that we have chosen the traditional binary application representation of λ-terms (s.t) but

flexflex1(F, \overline{x_{m}}, \overline{y_{m}}, θ) = if \overline{x_{m}} = \overline{y_{m}} then θ else (F, λ\overline{x_{m}}.H([x_{i} | 1 ≤ i ≤ m ∧ x_{i} = y_{i}])) :: θ

flexflex2(F, \overline{x_{m}}, G, \overline{y_{n}}, θ) = if \{\overline{x_{m}}\} ⊆ \{\overline{y_{n}}\} then (G, λ\overline{y_{n}}.F (\overline{x_{m}})) :: θ else if \{\overline{x_{m}}\} ⊇ \{\overline{y_{n}}\} then (F, λ\overline{x_{m}}.G(\overline{y_{n}})) :: θ else let \{\overline{z_{k}}\} = \{\overline{x_{m}}\} ∩ \{\overline{y_{n}}\} in (F, λ\overline{x_{m}}.H(\overline{z_{k}})) :: (G, λ\overline{y_{n}}.H(\overline{z_{k}})) :: θ

Figure 4: Minimizing new variables

that we often want to view the terms in their functorarguments form (a(\overline{s_{m}})). The functions red and strip realize the isomorphisms between both representations: red(strip t) = t, if t is in β-normal form, and strip(red(a, ss)) = (a, ss).

Making binary application primitive and deriving the functor-arguments form from it is not necessarily optimal. Measurements by Michaylov and Pfenning [7] indicate that in an environment where unification is the bottleneck it may be advantageous to make the functor-arguments form primitive. In our algorithm this would certainly pay off since translations back to binary application form would not be required.

9 Minimizing new variables

Careful handling of flex-flex cases can often avoid the introduction of new variables, as shown in Fig. 4. The last line of proj can be improved similarly:

(F, \overline{x_{m}}) ⇒ if \{\overline{x_{m}}\} ⊆ V then θ

else \begin{matrix}let \{\overline{y_{n}}\} = \{\overline{x_{m}}\} ∩ V \\ in (F, λ\overline{x_{m}}.H(\overline{y_{n}})) :: θ \end{matrix}

10 De Bruijn’s notation

Recall that λ-terms in de Bruijn’s notation [4] are generated by the following grammar

e = F | i | c | (e_{0}.e_{1}) | λe

where i ranges over natural numbers. A natural number i represents a variable bound by the (i + 1)^{st} λ above i. For example λx.λy.(x.y) is represented by λλ(1.0). The abbreviation λ_{k} denotes k nested abstractions.

The main advantage of de Bruijn’s notation is the fact that α-equivalent terms are really identical, which has made this representation popular with implementors. Unfortunately this is also a bit of a problem because the previous unification algorithm made essential use of the ability to rename bound variables. For example the solution to the flex-flex pair F (x, y) =^{?} G(y, z) is the substitution {F ↦ λx, y.H(y), G ↦ λy, z.H(y)}, where the bodies are the same (H(y)) and the binders differ. In de Bruijn’s notation it is just the other way around: {F ↦ λ_{2}H(0), G ↦ λ_{2}H(1)}. The problem becomes worse in the flex-rigid case: F (\overline{x_{m}}) =^{?} t has the solution θ ∘ \{F ↦ λ\overline{x_{m}}.t\}, where θ contains the necessary projections. The point is that t can be copied from the problem to the solution. With de Bruijn’s indices we cannot force new binders on t but we have to adjust the loose bound variables inside t.

The following algorithm is a translation of the version in Section 8, i.e. without minimizing new variables, into de Bruijn’s notation. The main unification functions are displayed in Fig. 5, auxiliary ones in Fig. 6. Functions which are syntactically identical to their alphabetic counterpart, e.g. flexflex and occ, have been omitted. Although the structure of the two algorithms is very close, computations with de Bruijn indices are notoriously subtle and deserve special attention.

The two flex-flex cases involve some index arithmetic but are straightforward translations. As motivated above, the main difference to the version with alphabetic bound variables is found in flexrigid where mapbnd adjusts the loose bound variables inside the rigid term t. In general, calling mapbnd f t applies f to all loose bound variables in t, taking the depth, i.e. the number of enclosing λs, into account. The function idx \overline{ı_{n}} performs two tasks: it adjusts those loose bound variables which appear in \overline{ı_{n}} and replaces the ones not in \overline{ı_{n}} by −∞. On a second pass through t, proj eliminates all occurrences of −∞ with appropriate projections. Since the index arithmetic involved is quite subtle, an example may help.

Example 10.1 Consider again the unification problem from Example 3.2. In de Bruijn’s notation it becomes λλF (1) =^{?} λλc(G(0, 1)). Applying mapbnd (idx [1]) to c(G(0, 1)) yields u = c(G(−∞, 0)). Calling proj θ u, where θ = {F ↦ λu}, eliminates −∞ by composition of {G ↦ λλH(0)} with θ.

Note that −∞ was chosen to indicate “dead” variables because mapbnd may add an offset to bound variables. But since −∞ + d = −∞ for any natural number d, this adjustment leaves dead variables dead.

unif θ (s, t) = case (devar θ s, devar θ t) of ; \begin{matrix}(λs, λt) ⇒ & unif θ (s, t) \\ (λs, t) ⇒ & unif θ (s, (incr t).0) \\ (s, λt) ⇒ & unif θ ((incr s).0, t) \\ (s, t) ⇒ & cases θ (s, t) \end{matrix}

cases θ (s, t) = case (strip s, strip t) of ; \begin{matrix}((F, \overline{ı_{m}}), (G, \overline{ȷ_{n}})) ⇒ & flexflex(F, \overline{ı_{m}}, G, \overline{ȷ_{n}}, θ) \\ ((F, \overline{ı_{m}}), ) ⇒ & flexrigid(F, \overline{ı_{m}}, t, θ) \\ ( , (F, \overline{ı_{m}})) ⇒ & flexrigid(F, \overline{ı_{m}}, s, θ) \\ ((a, \overline{s_{m}}), (b, \overline{t_{n}})) ⇒ & rigidrigid(a, \overline{s_{m}}, b, \overline{t_{n}}, θ) \end{matrix}

flexflex1(F, \overline{ı_{m}}, \overline{ȷ_{n}}, θ) = if m ≠ n then fail else (F, λ_{m}H([m − k | 1 ≤ k ≤ m ∧ i_{k} = j_{k}])) :: θ
flexflex2(F, \overline{ı_{m}}, G, \overline{ȷ_{n}}, θ) = let \{\overline{k_{l}}\} = \{\overline{ı_{m}}\} ∩ \{\overline{ȷ_{n}}\} in (F, lam(\overline{ı_{m}}, H, \overline{k_{l}})) :: (G, lam(\overline{ȷ_{n}}, H, \overline{k_{l}})) :: θ
lam(\overline{ı_{m}}, G, \overline{ȷ_{n}}) = λ_{m}G(map (idx \overline{ı_{m}}) \overline{ȷ_{n}})
flexrigid(F, \overline{ı_{n}}, t, θ) = if occ F θ t then fail else let u = mapbnd (idx \overline{ı_{n}}) t in proj ((F, λ_{n}u) :: θ) u
proj θ s = case strip(devar θ s) of
(λt, []) ⇒ proj θ t
(c, ss) ⇒ foldl proj θ ss
(i, ss) ⇒ if i < 0 then fail else foldl proj θ ss
(F, \overline{ı_{n}}) ⇒ (F, λ_{n}H([n − j | 1 ≤ j ≤ n ∧ i_{j} ≥ 0])) :: θ

Figure 5: Unification in de Bruijn’s notation

Nevertheless −∞ smells of a hack. The main reason for doing it this way is one of presentation. A more efficient way of solving the flex-rigid case is to traverse t only once, adjusting its loose bound variables and at the same time computing the necessary projections. Unfortunately this leads to a more complex function because both a term and a substitution are computed. Nevertheless it is preferable, not just for efficiency reasons: the introduction of −∞ destroys the link to the corresponding binder which may hold information such as the type or (for printing) the external name of the bound variable.

11 Efficiency

The algorithms presented above may take exponential time. This is not hard to see since their restriction to first-order terms is essentially Robinson’s algorithm, where substitutions are represented as graphs rather than trees. This leads to linear space consumption but is still exponential in time [3]. However, the amazing success of Prolog, many of whose implementations are both unsound (no occurs-check) and exponential, has shown that in practice this is not a problem.

Asymptotically efficient first-order unification algorithms, for example Paterson and Wegman’s [14], rely on pointer structures for their efficiency. For firstorder terms this works well, because the unification of a variable with a term can be implemented by updating a pointer. In the higher-order case this is less straightforward because the variable may be applied to some arguments. Yet Qian [18] has presented a linear (imperative) unification algorithm for patterns. Not surprisingly, the functional algorithm in this paper is far simpler. Whether it is also faster for small terms can only be assessed by comparing two implementations. However, no implementation of Qian’s algorithm is available to the author.

12 Variations

There are two variations of the unification problem that are important in practice: matching, and unification of terms whose types may contain type variables (as in ML, LCF, HOL, Isabelle, …).

Matching is significantly easier than unification. There are no flex-flex cases and the flex-rigid case F (\overline{x_{m}}) =^{?} t can be solved in one step: either all loose

devar θ s = case strip s of

\begin{matrix}(F, is) ⇒ & case assoc F θ of ; \begin{matrix}[t] ⇒ & devar θ (red t is []) \\ [] ⇒ & s \end{matrix} \\ ⇒ & s \end{matrix}

\begin{aligned}red (λs) (i :: is) js & = & red s is (i :: js) \\ red s is \overline{ȷ_{n}} & = & app (mapbnd (fn k ⇒ j_{k+1}) s) is \end{aligned}

\begin{aligned}app s (i :: is) & = & app (s.i) is \\ app s [] & = & s \end{aligned}

mapbnd f = let mpb d i  = if i < d then i else f(i − d) + d mpb d (λt) = λ(mpb (d + 1) t) mpb d (t_{1}.t_{2}) = (mpb d t_{1}).(mpb d t_{2}) mpb d t  = t

in mpb 0

incr = mapbnd (fn i ⇒ i + 1)
idx (i :: is) j = if i = j then |is| else idx is j
idx [] j  = −∞

Figure 6: Auxiliary functions for de Bruijn’s notation

bound variables in t are contained in \{\overline{x_{m}}\}, in which case the solution is F ↦ λ\overline{x_{m}}.t, or there is no solution.

Type variables can be dealt with by maintaining the invariant that the two terms to be unified have the same type. The invariant can only be destroyed in the rigid-rigid case. If the heads of the rigid terms are bound variables, they must be identical and hence of the same type^{2}. If they are constants, they can have different instances of the same polymorphic type. These instances must be unified, thus establishing the invariant for the equations between the arguments of the constants.

Acknowledgement Many thanks are due to Larry Paulson, Christian Prehofer, Konrad Slind and Oskar Slotosch for their careful reading and their comments.

References

[1] P. B. Andrews, S. Issar, D. Nesmith, and F. Pfenning. The TPS theorem proving system. In M. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, pages 641–642. LNCS 449, 1990.

[2] R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall, 1988.

[3] J. Corbin and M. Bidoit. A rehabilitation of Robinson’s unification algorithm. In R. Pavon, editor, Proc. 1983 IFIP Congress, pages 909–914. North-Holland, 1983.

[4] N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381–392, 1972.

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

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

[7] S. Michaylov and F. Pfenning. An empirical study of the runtime behaviour of higher-order logic programs. In D. Miller, editor, Proc. Workshop on λProlog, pages 257–271, 1992.

2λ-bound variables are monomorphic.

fun foldl f (a,x::xs) = foldl f (f(a,x),xs)
| foldl f (a,[]) = a;
fun foldr f (x::xs,a) = f(x,foldr f (xs,a))
| foldr f ([],a) = a;
datatype 'a option = Some of 'a | None;
fun assoc x ((y,t)::ps) = if x=y then Some(t) else assoc x ps
| assoc x [] = None;
infix mem;
fun (x mem (y::ys)) = x=y orelse x mem ys
| (x mem []) = false;
infix /\;
fun ((x::xs) /\ ys) = if x mem ys then x::(xs /\ ys) else xs /\ ys
| ([] /\ _) = [];
fun map f (x::xs) = f x :: map f xs
| map f [] = [];

Figure 7: Basic library

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

[9] D. Miller. Unification of simply typed lambdaterms as logic programming. In P. Furukawa, editor, Proc. 1991 Joint Int. Conf. Logic Programming, pages 253–281. MIT Press, 1991.

[10] D. Miller. Private communication, November 1992.

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

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

[13] T. Nipkow. Orthogonal higher-order rewrite systems are confluent. In M. Bezem and J. F. Groote, editors, Proc. Int. Conf. Typed Lambda Calculi and Applications. LNCS 664, 1993.

[14] M. Paterson and M. Wegman. Linear unification. J. Computer and System Sciences, 16:158–167, [15] L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

[16] F. Pfenning. Logic programming in the LF Logical Framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 66–78. Cambridge University Press, 1991.

[17] F. Pfenning. Unification and anti-unification in the calculus of constructions. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 74–85, 1991.

[18] Z. Qian. Linear unification of higher-order patterns. In J.-P. Jouannaud, editor, Proc. 1993 Coll. Trees in Algebra and Programming. LNCS, 1993. To appear.

A The complete ML code

Figures 7 through 10 present the translation of the algorithm from Section 8 into Standard ML. This implementation, together with one for de Bruijn’s notation, is also available by email/ftp from the author.

(*** Generation of new names --- non functional!     ***)
(*** Assumption: names in input terms are not primed ***)
val Fname = ref("F");
val Bname = ref("x");
fun newname(r) = (r := !r ^"'"; !r);
fun newB() = newname Bname;
infix 9 $;
infixr \;
datatype term = V of string            (* free var  *)
              | B of string            (* bound var *)
              | C of string            (* constant  *)
              | op $ of term * term    (* application *)
              | op \ of string * term; (* abstraction *)
fun newV() = V(newname Fname);
fun B1(B s) = s;
fun strip t = let fun strip(s$t,ts) = strip(s,t::ts)
                    | strip p = p
              in strip(t,[]) end;
fun abs(xs,t) = foldr op \ (map B1 xs,t);
fun hnf(xs,F,ss) = abs(xs, foldl op $ (F,ss));

Figure 8: Terms

fun occ F S (V G) = (F=G) orelse (case assoc G S of Some(s) => occ F S s | None => false)
  | occ F S (s$t) = occ F S s orelse occ F S t
  | occ F S (_\s) = occ F S s
  | occ F S (_)   = false;
fun subst y x = let fun sub(b as B z) = if z=x then B y else b
                      | sub(s1$s2) = (sub s1) $ (sub s2)
                      | sub(t as z\s) = if z=x then t else
                                        if z<>y then z \ sub s else
                                        let val z' = newB() in z' \ sub(subst z' z s) end
                      | sub(s) = s
                in sub end;
fun red (x\s) (y::ys) = red (subst (B1 y) x s) ys
  | red s     (y::ys) = red (s$y) ys
  | red s     []      = s;
fun devar S t = case strip t of
                  (V F,ys) => (case assoc F S of Some(t) => devar S (red t ys) | None => t)
                | _=> t;

Figure 9: Substitutions

exception Unif;
fun proj W (S,s) = case strip(devar S s) of
      (x\t,_)  => proj (x::W) (S,t)
    | (C _,ss) => foldl (proj W) (S,ss)
    | (B x,ss) => if x mem W then foldl (proj W) (S,ss) else raise Unif
    | (V F,ss) => (F, hnf(ss, newV(), ss /\ (map B W))) :: S;
fun eqs (x::xs) (y::ys) = if x=y then x::eqs xs ys else eqs xs ys
  | eqs [] [] = []
  | eqs __= raise Unif;
fun flexflex1(F,ym,zn,S) = (F, hnf(ym, newV(), eqs ym zn)) :: S;
fun flexflex2(F,ym,G,zn,S) =
    let val xk  = ym /\ zn and H = newV()
    in (F, hnf(ym,H,xk)) :: (G, hnf(zn,H,xk)) :: S end;
fun flexflex(F,ym,G,zn,S) = if F=G then flexflex1(F,ym,zn,S) else flexflex2(F,ym,G,zn,S);
fun flexrigid(F,ym,t,S) = if occ F S t then raise Unif
                          else proj (map B1 ym) (((F,abs(ym,t))::S),t);
fun zip (x::xs) (y::ys) = (x,y) :: zip xs ys
  | zip [] [] = []
  | zip __= raise Unif;
fun unif (S,(s,t)) = case (devar S s,devar S t) of
        (x\s,y\t) => unif (S,(s,if x=y then t else subst x y t))
      | (x\s,t)   => unif (S,(s,t$(B x)))
      | (s,x\t)   => unif (S,(s$(B x),t))
      | (s,t)     => cases S (s,t)
and cases S (s,t) = case (strip s,strip t) of
                      ((V F,ym),(V G,zn)) => flexflex(F,ym,G,zn,S)
                    | ((V F,ym),_)        => flexrigid(F,ym,t,S)
                    | (_,(V F,ym))        => flexrigid(F,ym,s,S)
                    | ((a,sm),(b,tn))     => rigidrigid(a,sm,b,tn,S)
and rigidrigid(a,ss,b,ts,S) = if a <> b then raise Unif else foldl unif (S,zip ss ts);

Figure 10: Unification