J. Symbolic Computation (1992) 11, 1–??

Unification Under a Mixed Prefix

DALE MILLER

Department of Computer Science

University of Pennsylvania

Philadelphia, PA 19107–6389 USA

(Received 8 July 1992)

Unification problems are identified with conjunctions of equations between simply typed λ-terms where free variables in the equations can be universally or existentially quantified. Two schemes for simplifying quantifier alternation, called Skolemization and raising (a dual of Skolemization), are presented. In this setting where variables of functional type can be quantified and not all types contain closed terms, the naive generalization of firstorder Skolemization has several technical problems that are addressed. The method of searching for pre-unifiers described by Huet is easily extended to the mixed prefix setting, although solving flexible-flexible unification problems is undecidable since types may be empty. Unification problems may have numerous incomparable unifiers. Occasionally, unifiers share common factors and several of these are presented. Various optimizations on the general unification search problem are as discussed.

1. Introduction

Most first-order unification algorithms are designed to solve existentially quantified sets of equations such as

∃x_{1} … ∃x_{n}[t_{1} = s_{1} ∧ … ∧ t_{m} = s_{m}].

That is, the free variables of the terms t_{1}, …, t_{m}, s_{1}, …, s_{m} are interpreted as being existentially quantified. Of course, if higher-order types are available, constants within the equations can be universally quantified giving a ∀∃ quantifier prefix. In this paper we consider the more general situation where equations must be solved under a mixed quantifier prefix. That is, we shall consider unification problems to be of the form

Q_{1}x_{1} … Q_{n}x_{n}[t_{1} = s_{1} ∧ … ∧ t_{m} = s_{m}],

where Q_{1}, …, Q_{n} are universal and existential quantifiers. Furthermore, we shall allow the terms t_{1}, …, t_{m}, s_{1}, …, s_{m} to be simply typed λ-terms and the variables x_{1}, …, x_{n} to be of primitive or functional type. Equality between closed λ-terms will be identified with βη-convertibility. Such quantified conjunctions of equations are called unification problems and solutions for them are certain restricted substitutions for the existentially quantified variables that yield closed equations valid in the βη theory of equality.

0747–7171/90/000000 + 00 $03.00/0 \begin{matrix}c \\ ◯ \end{matrix} 1992 Academic Press Limited \underline{2 D. Miller}

Below we list several reasons for studying βη-unification of simply typed λ-terms in this way.

Constants and variables are explicitly declared by a prefix. The quantifier prefix can be seen as a declarations of how its bound variables are to be interpreted within the equations. In particular, a universal quantifier declares that its bound variable is to be interpreted as a constant within its scope while an existential quantifier declares that its bound variable is to be interpreted as available for substitution. For example, the prefix ∀x∃y∀z∃u will be used to declare that x and z are constants while y and u are variables within a given unification problem. If the unification problem already contained constants, say c and d, these could be explicitly declared by adding ∀c∀d to the front of the prefix. In this way, it is generally possible to assume that the logic in which these unification problems are considered contains no nonlogical constants: constants are introduced explicitly by a prefix when they are needed.

Empty types can be studied and used. The explicit information of a prefix makes a convenient setting to study the effect of empty types on unification. For example, checking for the existence of unifiers in this case can be much more complex than in the usual case when all types are assumed to be nonempty.

Substitution terms can range over different signatures. The alternation of quantifiers in a prefix can make distinctions between existential variables that are not captured by type distinctions. Consider again a unification problem with prefix ∀c∀d∀x∃y∀z∃u. Any substitution term for y can contain c, d, and x, while a substitution term for u may contain these as well as z. Thus, different existentially quantified variables can receive substitution terms built from different signatures.

The intimate relation between λ-abstractions and universal quantifiers can be exploited. An equation between abstractions, say λxt = λxs, is provable if and only if the quantified equation ∀x.t = s is provable. Thus, the study of universal quantifiers in prefixes and the study of λ-abstractions in terms can be tied together closely. This connection will be exploited several times in this paper.

Skolemization does not provide a simple solution method. When variables of functional type can be existentially quantified, Skolemization does not provide a simple method of reducing the quantifier alternation in a prefix. There are basically two problems with Skolem functions. Types that were empty prior to introducing a Skolem function can become nonempty afterwards. Furthermore, if λ-abstractions are built without restriction from Skolem functions, solutions to a Skolemized unification problem may be difficult to relate back to solutions of the original problem. In order to deskolemize solutions and make Skolemization sound (without using a choice axiom), a restriction on the formation of λ-abstractions over Skolem functions must be made.

When higher types are available, Skolemization has a dual. Skolemization can be seen as taking a constant (a universally quantified variable) in a given unification problem and replacing it with a new constant, the Skolem function, at a higher type. In doing so, the alternation of quantifiers can be, in some sense, simplified. There is a dual operation to this, called raising, that takes an existentially quantified variable and replaces it with a new existential variable of higher type in such a way that quantifier alternation is again simplified.

Various computation systems generate unification problems with mixed prefixes. The unification problems considered in this paper are those that arise in the Isabelle theorem prover (Paulson, 1989), in the type inference programs described in (Pfenning, 1988), and in interpreters for the higher-order logic programming language λProlog (Nadathur & Miller, 1988). In fact many of the definitions and motivation for parts of this paper come directly from having implemented one such interpreter. For example, since many programs in λProlog rely only on second-order unification, the restrictions to secondorder used in Sections 11 and 12 have practical consequences. Also in λProlog, the socalled flexible-flexible unification problems may need to be presented as part of an answer substitution: as a result, it is important that the form of these unification problems be simple and intelligible. The material on improper factors in Section 11 can be used to simplify such unification problems.

This paper is organized as follows. In Section 2, unification problems are formalized as certain prenex normal formulas and solvable unification problems are defined as those that are provable in a simple proof system. An equivalent notion of solvability using substitutions for existentially bound variables is presented in Section 3. Some of the problems surrounding the use of Skolemization in this higher-order setting are presented and solved in Section 4. Raising is described and proved sound and complete in Section 5. Section 6 illustrates how Skolemization and raising can be used to process unification problems prior to submitting them to unification processes that do not address quantifier alternation. Huet’s pre-unification process for simply typed λ-terms (Huet, 1975) is modified to deal directly with mixed prefixes in Section 7. Pre-unification carries unification problems into a class of flexible-flexible problems and Section 8 addresses the solvability of these unification problems. Section 9 describes some unification problems that do not have solutions. A generalization to most general unifiers is presented in Section 10, and Sections 11 and 12 use that generalization on some classes of unification problems. We conclude by describing some related work in Section 13.

2. Unification Problems

Unification problems will be formalized in a logic that is essentially a small sublogic of Church’s Simple Theory of Types (Church, 1940). Type expressions in this logic are all the closed first-order terms defined using certain primitive types and one binary infix function symbol →. When reading type expressions, we associate the infix operator → to the right. We shall assume that there is at least one primitive type symbol meta that denotes the type of unification problems and as many other primitive types as we find useful. There are no type variables. The symbols τ and δ will be used as syntactic variables ranging over type expressions.

Definition 2.1. Let τ be the type τ_{1} → ⋯ → τ_{n} → τ_{0} where τ_{0} is primitive and n ≥ 0. (By convention, if n = 0 then τ is simply the type τ_{0}.) The types τ_{1}, …, τ_{n} are the argument types of τ while the type τ_{0} is the target type of τ. The order of τ is defined as follows: If τ is primitive then τ has order 0; otherwise, the order of τ is one greater than the maximum order of the argument types of τ.

We shall assume that there is a denumerably infinite list of variables. Constants are only the logical constants ⊤, ∧, =^{τ}, ∀_{τ}, and ∃_{τ}, where τ ranges over type expressions that do not contain the primitive type meta. The type annotations on =, ∀, and ∃ will occasionally be dropped when its actual value is not important or can be inferred from context. Untyped λ-terms can be built up from these variables and constants by using λ-abstraction and application. When reading λ-terms, we associate applications to the left. The notions of subterm and free and bound occurrences of variables are defined as

\underline{4 D. Miller}

usual. Two λ-terms are considered identical if they differ only in an alphabetic change of bound variables. The notation [N/x]M denotes the substitution of λ-term N for all free occurrences of x in M. Of course, bound variables of M must be systematically changed via α-conversion to avoid variable capture. A term is in β-normal form if it contains no occurrence of a β-redex, that is, a formula of the form (λxM)N. Every term t can be associated with a unique (up to α-conversion) β-normal term that is β-convertible to t. We shall assume that the reader is familiar with the basic definitions and properties of βη-conversion (see, for example, Chapters 1 – 7 and 13 of (Hindley & Seldin, 1986)).

In this paper we shall use several forms of equality. As mentioned above, λ-terms are equal if they are alphabetic variants. We shall use no special symbol to represent this equality relation, choosing instead to simply write phrases such as “t is equal to s”. When the unadorned symbol = is used, it is either the logical constant =^{τ} with its annotation dropped or the mathematical symbol relating objects such as sets or lists: exactly which relation is intended should always be clear from context.

Definition 2.2. A signature is a finite set Γ of pairs, written as x: τ, where x is a variable and τ is a type expression, and whenever x: τ ∈ Γ and x: δ ∈ Γ, τ and δ are the same type. Signatures are used to assign types to variables. The expression Γ + x: τ denotes the set Γ − {x: δ} ∪ {x: τ} if Γ assigns type δ to x, or the set Γ ∪ {x: τ} otherwise.

We now define a provability relation for this logic.

Definition 2.3. Let ⊢ be a provability relation between a signature on the left and either a term or pair t: τ where t is a term and τ is a type expression. The symbol ⊢^{∗} is an abbreviation: Γ ⊢^{∗} P means Γ ⊢ P: meta and Γ ⊢ P. Below are the axioms and inference rules for ⊢.

(τ_{0}) Γ ⊢ ⊤: meta, Γ ⊢ ∧: meta → meta → meta, Γ ⊢ =^{τ}: τ → τ → meta, Γ ⊢

∀_{τ}: (τ → meta) → meta, and Γ ⊢ ∃_{τ}: (τ → meta) → meta. (τ_{1}) If x: τ ∈ Γ then Γ ⊢ x: τ. (τ_{2}) If Γ ⊢ M: τ → δ and Γ ⊢ N: τ then Γ ⊢ MN: δ. (τ_{3}) If Γ + x: τ ⊢ M: δ then Γ ⊢ λx M: τ → δ. (⊤) Γ ⊢ ⊤. (=) If Γ ⊢ M: τ, Γ ⊢ N: τ, and M βη-converts to N then Γ ⊢ M =^{τ} N.

(ξ) If Γ + x: τ ⊢^{∗} N =^{δ} M then Γ ⊢ λx N =^{τ→δ} λx M.

(∧) If Γ ⊢^{∗} P and Γ ⊢^{∗} Q then Γ ⊢ P ∧ Q.

(∃) If Γ ⊢^{∗} [N/x]P and Γ ⊢ N: τ then Γ ⊢ ∃_{τ} x P.

(∀) If Γ + x: τ ⊢^{∗} P then Γ ⊢ ∀_{τ} x P.

A proof of P from Γ is a list of pairs ⟨Γ_{1}, P_{1}⟩, …, ⟨Γ_{n}, P_{n}⟩ where n ≥ 1 and (i) Γ_{n} is Γ and P is P_{n}, (ii) for all i = 1, …, n, Γ_{i} ⊢ P_{i} is either an axiom (an instance of (τ_{0}), (τ_{1}), or (⊤)) or results from previous pairs by an inference rule. If Γ is empty, we write ⊢ P instead of Γ ⊢ P.

The axioms and rules (τ_{0}), (τ_{1}), (τ_{2}), (τ_{3}) are those necessary to impose the simple type discipline on λ-terms. The axiom (=) is, of course, a powerful axiom, capturing all of βη-convertibility in one rule. This rule, however, is decidable for λ-terms that have simple types (Chapter 13, (Hindley & Seldin, 1986)).

Signatures only change in the inference rules (∀) and (ξ). In essence, a constant is discharged during these rules: this is best compared to the discharging of an assumption in the proof of an implication in natural deduction. Signatures are often called type assignments elsewhere. We shall prefer the former term since we think of variables occurring to the left of ⊢ as actually playing the role of constants with respect to unification.

It is immediate to see that the conclusion of the six rules (⊤), (=), (ξ), (∧), (∃), and (∀) could all be written with ⊢^{∗} substituted for ⊢. Hence, if Γ ⊢ P is provable, either P is of the form t: τ or it is ⊤, an equation, a conjunction, an existential, or a universal formula such that Γ ⊢ P: meta. In either case, the free variables of P are assigned some type by Γ.

The following two propositions are simple consequences of this definition of provability.

Proposition 2.4. Let Γ ⊢ t: τ and Γ ⊢ s: τ. Γ ⊢ t =^{τ} s if and only if t βη-converts to s.

Proof. In the reverse direction, this is simply the inference rule (=). The forward direction is not so immediate since there are two inference rules, namely (ξ) and (=), that can prove an equation. If Γ ⊢ t =^{τ} s then there is a proof of this fact that is built first of typing rules (τ_{0}) – (τ_{3}), a single instance of (=), and then some number n ≥ 0 of (ξ) rules. The conclusion of the (=) rule must be of the form

Γ + x_{1}: τ_{1} + … + x_{n}: τ_{n} ⊢ t′ =^{δ} s′

where τ is τ_{1} → … τ_{n} → δ and t and s are equal up to α-conversion to λx_{1} … λx_{n}.t′ and λx_{1} … λx_{n}.s′, respectively. Since t′ and s′ are βη-convertible, so are the terms λx_{1} … λx_{n}.t′ and λx_{1} … λx_{n}.s′. □

Adding the inference rule (ξ), therefore, does not enrich the equations that can be proved using βη-conversion. This rule is added so that the following proposition will hold.

Proposition 2.5. Assume that x is not in Γ and let Γ ⊢ N: τ → δ and Γ ⊢ M: τ → δ. Then, Γ ⊢ ∀_{τ} x.Nx =^{δ} Mx if and only if Γ ⊢ N =^{τ→δ} M.

Proof. Assume Γ ⊢ ∀_{τ} x.Nx =^{δ} Mx. Then this is proved from Γ + x: τ ⊢ Nx =^{δ} Mx, from which we can conclude by (ξ) that Γ ⊢ λxNx =^{τ→δ} λxMx. By Proposition 2.4 and ηconversion, we have Γ ⊢ N =^{τ→δ} M. If we assume Γ ⊢ N =^{τ→δ} M then Γ + x: τ ⊢ Nx =^{δ} Mx since βη-conversion is a congruence relation. Finally, by (∀), we have Γ ⊢ ∀_{τ} x.Nx =^{δ} Mx.

□

The next proposition follows immediately from the fact that it is decidable to determine if an untyped λ-terms has a simple typing and to determine βη-convertibility for simply typed λ-terms.

Proposition 2.6. Let Γ be a signature and let P be a λ-term that does not contain any occurrences of ∃. It is decidable whether or not Γ ⊢^{∗} P.

The following proposition lists several transformations of terms of type meta that are useful for several later manipulations. We shall think of such transformation rules as rewriting rules, and as we shall see, no significant property of unification problems are changed by using these rewriting rules.

\underline{6 D. Miller}

Proposition 2.7. Let Γ be a signature and let P be a λ-term such that Γ ⊢ P: meta. Let P′ be one of the following modifications of P.

(1) P′ is an alphabetic variant of P.

(2) P′ is the result of replacing a subterm of the form ∀_{τ} x.N =^{δ} M with one of the form λxN =^{τ→δ} λxM, or vice versa.

(3) P′ is the result of replacing a subterm of the form ∀_{τ} x.N with N, or vice versa, provided N does not contain x free and does not contain any existential quantifiers.

(4) P′ is the result of replacing a subterm of the form ∀_{τ} x.N ∧∀_{τ} x.M with ∀_{τ} x.(N ∧M), or vice versa.

(5) P′ is the result of replacing a subterm of the form M ∧ ⊤ or ⊤ ∧ M with M.

(6) P′ is the result of replacing a subterm of the form ∃_{τ} x∃_{δ}yM with ∃_{δ}y∃_{τ} xM or a subterm of the form ∀_{τ} x∀_{δ}yM with ∀_{δ}y∀_{τ} xM.

(7) P is the result of replacing a subterm of the form t = t with ⊤.

Then, Γ ⊢ P′: meta, and Γ ⊢ P if and only if Γ ⊢ P′.

Proof. Simple inductions on the length of proofs establish the correctness of all of these rewriting rules. □

Definition 2.8. A unification problem is a closed, β-normal λ-term P such that

(1) ⊢ P: meta,

(2) P is in prenex normal form; that is, no occurrence of an existential or universal quantifier is in the scope of a conjunction (given condition (1) and the restriction on the types of logical constants, no logical constant can occur in the scope of an equation),

(3) if P contains an occurrence of ∧, it contains no occurrences of ⊤ ( ⊤ denotes an empty conjunction), and

(4) equations in P are only between terms of primitive type.

Conditions (3) and (4) are not genuine restrictions; they are added only for convenience. Given Proposition 2.7, any prefix normal term of type meta can be rewritten into a terms satisfying these two conditions.

Example 2.9. Let i be a primitive type. Each of the following are provable:

∃_{i→i}X.X =^{i→i} X  ∀_{i}y∃_{i}X.X =^{i} X  ∀_{i}X.X =^{i} X.

The first term is proved by existentially generalizing over the equation λz z =^{i→i} λz z. This term is not a unification problem although it can be rewritten into the unification

problem ∃_{i→i}X∀_{i}y.Xy =^{i} Xy.

The unification problem ∃_{i}X.X =^{i} X is not provable from the empty signature. This shows that dropping vacuous universal quantifiers is not generally permitted. Similarly, anti-prenexing rules are not generally valid. For example, while ∀_{i}y∃_{i}X[y =^{i} y ∧ X =^{i} X] is provable, ∀_{i}y[y =^{i} y] ∧ ∃_{i}x[X =^{i} X] is not provable.

As this example shows, the nonprenex normal class of terms forms a class that is interesting on its own right. We shall, however, consider only prenex normal formulas in this paper since they will simplify parts of our presentation. While most of the structure of unification in simple types appears to be illustrated using only prenex normal formulas, the problem of mixing logical inference with unification cannot be addressed only with prenex normal formulas. See (Miller, 1991b) for an example of using nonprenex normal formulas to encode that state of a theorem prover that performs both unification and logical deductions.

Occasionally, we refer to a prefix as being of a form described by a sequence of ∀’s and ∃’s. For example, an important class of prefixes are of the form ∀∃∀. Such a prefix has zero or more universal quantifiers, followed by zero or more existential quantifiers, followed by zero or more universal quantifiers. Thus, a prefix that is of the form ∃∀ is also of the form ∀∃∀. A ∀-prefix is either empty or a sequence of just universal quantifiers.

Unification problems can easily be embedded into formulas of Church’s Simple Theory of Types (Church, 1940) in the following manner. Let P be a unification problem. While P is technically an untyped λ-term, given the fact that it is β-normal and inferred to have type meta, every subterm and bound variables of P can be given a unique type. Let P^{∗} be the simply typed λ-term where all those types are attached to all bound variables. Now let P be some particular unification problem and let τ_{1}, …, τ_{n} (n ≥ 1) be the primitive types used to build types in the prefix of P. Let T be the formulation of the simple theory of types over primitive types τ_{1}, …, τ_{n} and where meta is identified with Church’s type o. Let ⊢_{T} be provability as in (Church, 1940) except that the axioms of choice, description, and infinity are not assumed. The following theorem can be proved by using the cut-elimination theorem for T (see (Andrews, 1971), for example).

Theorem 2.10. If x_{1}, …, x_{n} are distinct variables, then x_{1}: τ_{1} …, x_{n}: τ_{n} ⊢ P if and only if ⊢_{T} P^{∗}.

The signature {x_{1}: τ_{1} …, x_{n}: τ_{n}} above is needed to assure that there exist terms of all types. Given the characterization of ⊢_{T} using general models (Henkin, 1950; Andrews, 1972), we can conclude from this theorem that ⊢ ∀_{τ_{1}}x_{1} … ∀_{τ_{n}}x_{n}P if and only if P^{∗} is true in all general models.

In the next section we present a characterization of provable unification problems using substitutions.

3. Prefix as Declaration

Besides declaring type information for constants and variables in a unification problem, a prefix also indicates, by the relative positions of variables in the prefix, which constants can appear in substitution terms for which variables. For example, the unification problem ∀_{i→i}f∃_{i}x∀_{i}w[(fw) = x], where i is a primitive type, has no solution: trying to instantiate x with (fw) will fail to yield a valid equality since the rules of substitution require that the bound variable w in the prefix be changed to some other variable to avoid variable capture. Thus, the resulting equation would be between (fw) and (fw′) where w would be a free variable and w′ would be a bound variable. Here, the prefix declares that any substitution term for x may contain f free but may not contain w free. The following definitions help to formalize this constraint on substitutions.

Definition 3.1. A quantifier prefix (prefix for short) is a finite list of distinct variables quantified using typed versions of either universal or existential quantifiers. Let Q be a

\underline{8 D. Miller}

prefix. The λ-term t is a Q-term if t contains no constants other than the logical constants and all the free variables of t are bound in Q. If t is a Q-term we will call the pair Qt a prefixed term. Such a prefixed term is of type δ if Γ ⊢ t: δ, where Γ is the set of pairs x: τ where x is bound by either ∀_{τ} or ∃_{τ} in Q. Finally, the prefix term Qt is β-normal if t is β-normal, and two prefixed terms Qt_{1} and Qt_{2} with the same prefix are β-convertible if t_{1} is β-convertible to t_{2}.

Given a prefix Q and an untyped λ-term t, it is decidable whether t is a Q-term of a given type. The type of t, however, is not uniquely determined, in general, from Q. For example, the untyped λ-term λw.w can be given the type τ → τ for any type τ with respect to any prefix Q. However, the type of all subexpressions and bound variables of a β-normal prefixed term are uniquely determined from a type given for the prefixed term. Finally, unification problems can be thought of as being prefixed terms: that is, if P is of the form QD where Q is a string of quantifiers and D is a (possibly empty) conjunction of equations, then QD is a β-normal prefixed term of type meta.

Definition 3.2. Let Q be the prefix Q_{1}QxQ_{2} for prefixes Q_{1} and Q_{2}. If y is bound in Q_{1} then y is to the left of x in Q. If y is bound in Q_{2} then y is to the right of x in Q. Often reference to the prefix Q is dropped when it is obvious which prefix is being considered.

Next we define what it means to substitute into a prefixed term.

Definition 3.3. Let Q be a prefix of the form Q_{1}∃_{τ} xQ_{2}. A term s is Q-closed for x if the free variables of s are universally bound in Q_{1} and Γ ⊢ s: τ where Γ is the signature that associates to universal variables in Q_{1} the type at which they are bound in Q_{1}.

A finite set θ of pairs is a Q-substitution if, whenever (x, s) ∈ θ, x is existentially quantified in Q and s is β-normal and Q-closed for x. Also, θ must be functional; that is, if (x, s_{1}) and (x, s_{2}) are members of θ, then s_{1} and s_{2} are equal terms. Finally, if (x, s) ∈ θ then x is in the domain of θ and s is in its range.

A Q-substitution θ can be considered as the following function on Q-terms. If θ is empty, then θ(Qt) := Qt. Otherwise, let (x, s) ∈ θ, let Q be Q_{1}∃xQ_{2}, and let θ′ := θ −{(x, s)}. Set θ(Qt) := θ′(Q_{1}Q_{2}[s/x]t). It is easy to show that since s does not contain any free occurrences of variables in the domain of θ, this definition is independent of the choice of (x, s) from θ. We shall generally write the substitution {(x_{1}, s_{1}), …, (x_{n}, s_{n})} with the more suggestive notation [x_{1} ↦ s_{1}, …, x_{n} ↦ s_{n}].

Two Q-substitutions are considered equal it they map the same existentially quantified variable to terms that are η-convertible.

There are prefixes Q for which no Q-substitution exists.

Definition 3.4. Let Q be a prefix of the form Q_{1}∃_{τ} xQ_{2}. If there is no Q-closed term for x then we say that this occurrence of ∃_{τ} in Q is empty.

Clearly, a Q-substitution exists if and only if all existential variables of Q are nonempty. Fortunately, determining whether or not there is a Q-substitution given Q is decidable since it is equivalent to proving formulas in intuitionistic propositional logic. In particular, a type, say τ, can be thought of as denoting a formula in propositional logic defined by considering all its primitive types as propositional symbols and by considering the type constructor → as implication.

Definition 3.5. Let Δ be a finite set of types and let τ be a type. The binary relation Δ ⊢_{I} τ defined by the three rules below determines intuitionistic provability for propositional implication logic.

(1) If τ ∈ Δ then Δ ⊢_{I} τ.

(2) If {τ_{1}} ∪ Δ ⊢_{I} τ_{2} then Δ ⊢_{I} τ_{1} → τ_{2}.

(3) If δ_{1} → δ_{2} ∈ Δ, Δ ⊢_{I} δ_{1}, and {δ_{2}} ∪ Δ ⊢_{I} τ then Δ ⊢_{I} τ.

This relation is shown to be polynomial-space complete in (Statman, 1979).

The following proposition follows immediately from well known results (Hindley & Seldin, 1986).

Proposition 3.6. Let Q be a prefix, let Δ be the set of types attributed to the bound variables in Q, and let τ be a type that does not contain the type symbol meta. Δ ⊢_{I} τ if and only if there is Q-term t of type τ.

Definition 3.7. Let P be a unification problem with prefix Q. A Q-substitution θ is a solution to P if its domain is the set of all existential variables of Q and ⊢ θP. Since θP contains no existential quantifiers, determining if θP is provable is decidable (Proposition 2.6).

Given these definitions, we can now use substitutions to characterize those unification problems that are provable.

Theorem 3.8. If P is a unification problem, then ⊢ P if and only if P has a solution.

Proof. The proof is a straightforward proof by induction on the length of the prefix of P. □

Thus, given a Q-substitution, it can be decided whether or not it is a solution to P. In general, however, it is undecidable whether or not P has a solution. This was first shown for third-order unification problems independently by Huet (1973a) and Lucchesi (1972) and then later for second-order unification problems by Goldfarb (1981). A variation on Goldfarb’s result is presented in Section 8.

One final observation concludes this section. Its proof is simple and omitted.

Proposition 3.9. The set of solutions to a unification problem does not change when using the rewriting rules in Proposition 2.7. In the case of the first rule using α-conversion, the names of the variables in the corresponding substitutions must be changed to account for the change of bound variables in the prefix.

The set of solutions for a given unification problem occasionally has a regular structure. For example, a first-order ∀∃-unification problem that has any solution can have all its solutions described as closed instances of a most general unifier (mgu). Recognizing the

\underline{10 D. Miller}

presence of mgu’s is valuable for numerous theoretical and practical considerations. As is well known, however, the unification problems we are considering here do not generally have mgu’s. The problem of finding a suitable replacement for mgu’s as a characterization of large sets of solutions is addressed in Section 10.

4. Skolemization

Consider the two propositions

∀_{τ} x∃_{δ}y P and ∃_{τ→δ}f∀_{τ} x [fx/y]P.  (1)

If we consider validity in general models, then it is valid that the second formula implies the first. A choice principle is needed to show that the first entails the second. If we dualize the quantifiers in (1), we get the two formulas

∃_{τ} x∀_{δ}y P and ∀_{τ→δ}f∃_{τ} x [fx/y]P.  (2).

In this case, the forward implication is valid while the reverse implication requires a choice principle. We shall show in Section 5 that when restricted to just the setting of unification problems, one of the formulas in (1) is provable if and only if the other formula in (1) is provable (choice is not needed). A similar relationship holds for the two formulas in (2) only if certain restrictions are made on unification problems. These restrictions are investigated in this section.

The process of replacing the first formula in (2) with the second formula will be called Skolemization. Notice that in the theorem proving literature, Skolemization is generally defined with respect to the first pair of formulas above since that literature is often involved with searching for refutations of the negation of proposed theorems. Since we shall be looking for direct proofs and not refutations, Skolemization is properly presented using the formulas in (2).

Skolemization can be described from the syntactic point of view as follows: the scoping of quantifiers in ∃_{τ} x∀_{δ}y P prohibits the variable y from appearing in the substitution term for x. Replacing the variable y in the first formula of (2) with the term fx will successfully encode this restriction: if t is the substitution term for x, then t cannot contain a subterm occurrence of ft.

For our purposes here, the usual presentation of Skolemization for first-order logic (see, for example, (Andrews, 1986)) is problematic on at least four accounts. First, a formal mechanism for forcing Skolem functions f to be new is generally achieved by enriching the logic with a denumerably infinite collection of constants that are not permitted in proposed theorems. These constants only enter the prover via Skolemization. As has already been described, we have a simpler and more elegant method for guaranteeing “newness” using prefixes: the Skolem function must be declared in the prefix of the unification problem and there, as all quantified variables, it must be different from any other variable declared for that problem. This way of writing Skolemization is also appealing since it can be viewed as a left rotation of a universal quantifier over an existential quantifier. This is particularly interesting since a dual operation, that is, a left rotation of an existential quantified variables over a universal quantifier, will also interest us (Section 5).

A second and more serious problem is that Skolem functions should not be used in abstractions as if they are genuine functions. Unrestricted uses of Skolem functions in substitutions can only be justified if choice principles are permitted, but such are not available in the proof system presented in Section 2. Consider the following example. In this section, we shall assume that a and b are two primitive types.

Example 4.1. The unification problem ∀_{(a→b)→a}z∃_{a}X∀_{b}y ⊤ has no solution: since there is no intuitionistic proof of a from (a → b) → a, there is no λ-term of type a whose only free variables are of type (a → b) → a. If we Skolemize this formula by moving the bound variable y to the left, we get ∀_{(a→b)→a}z∀_{a→b}f∃_{a}X ⊤, which does have the solution X ↦ z(λw(fw)) (which is equal to the substitution X ↦ zf).

Here, the Skolem function f is used as a first class function and not as the simple syntactic device motivated above. If Skolem terms are used only as such a device, then whenever f has type τ → δ and there are no Q-terms of type τ, then there should be no Q∀_{τ→δ}f-terms containing the function f. A restriction on Skolem functions will be presented later in this section by the introduction of “ranked” universal quantifiers. The aspect of unsoundness demonstrated by this example will be fixed by ranks.

A third problem with Skolemization arises when the solutions to unifications problems before and after Skolemizing are compared. It is most desirable to have a bijection between solutions of a problem and its Skolemized form. Unfortunately, there appears to be no such bijection. A “deskolemizing” mapping can be defined but it will not generally convert all solutions to a Skolemized problem back to solutions of the original problem. Furthermore, when deskolemizing can be used, it may be many-to-one, a fact that is illustrated in the next example.

Example 4.2. The unification problem ∀_{a}z∃_{a}X∀_{a}y ⊤ has exactly one solution, namely X ↦ z. The Skolemized form of this problem, namely ∀_{a}z∀_{a→a}f∃_{a}X ⊤, has an infinite number of different solutions, namely X ↦ z, X ↦ fz, X ↦ f(fz), etc. The deskolemization process described later will be able to collapse all of these solutions into the solution above by identifying f with the constant-valued z function.

There seems no easy way to improve Skolemization in order to solve this many-to-one correspondence of solutions. Skolemization adds redundancy to a unification problem.

Our final problem with the use of Skolem functions is the most serious and illustrates an aspect of empty types that is not illustrated by Example 4.1.

Example 4.3. The unification problem ∀_{a}z∀_{b→a}g∃_{a}X∀_{b}y ⊤ has exactly one solution, namely X ↦ z. Its Skolemized form, that is, ∀_{a}z∀_{b→a}g∀_{a→b}f∃_{a}X ⊤ has an infinite number of solutions; X ↦ z, X ↦ g(fz), X ↦ g(f(g(fz))), etc. No simple interpretation of the Skolem function f would seem to identify all of these substitution terms since there is no ∀_{a}z∀_{b→a}g-term of type b.

In this example, the prefix to the left of the existential variable X in the original unification problem does not provide enough variables to build a term of type b. After Skolemization, however, the prefix to the left of X can be used to build a term of type b and that term can be use to build new terms of type a. There seems to be no way to identify the new term of intermediate type b built using f with any term in the original problem.

As we shall see in Theorem 4.11, if the type of the variable that gets Skolemized is nonempty (with respect to the prefix to the left of the existential variable), then all

\underline{12 D. Miller}

solutions to the Skolemized problem can be deskolemized to solutions of the original unification problem.

As was mentioned above, part of the approach to making Skolem functions sound in this setting is to restrict their occurrences within substitution terms. The notion of rank must first be introduced.

Definition 4.4. The constants ∀_{τ}^{r}, where r ≥ 0 and τ is any type with r or more argument types, are called ranked universal quantifiers. A variable bound by ∀_{τ}^{r} is said to have rank r. The quantifier ∀_{τ}^{0} is identified with ∀_{τ}. The logical constant ∀_{τ}^{r} has the same type as the logical constant ∀_{τ}.

Ranked universal quantifiers will now be permitted in the prefixes of unification problems. Let ∀_{τ}^{r} quantify the variable x and let τ be of the form τ_{1} → ⋯ → τ_{n} → τ_{0} with τ_{0} a primitive type and r ≤ n. Then, n is the maximum number of arguments that occurrences of x can have, while as we define below, r is the number of arguments that occurrences x must have. Several of our definitions regarding prefixes must now be extended. The most fundamental extension is in the following definition: other extensions are more immediate. The motivation for the following definition, however, has already been presented: variables that have a positive rank play the role of Skolem functions: they cannot be permitted to act as genuine functions.

Definition 4.5. Let Q be a prefix containing possibly positively ranked universal quantifiers. The λ-term t is a Q-term if (i) t contains no nonlogical constants and all the free variables of t are bound in Q, (ii) if t contains a free occurrence of r-ranked universally bound variable then that occurrence must have at least r arguments, called its necessary arguments, and (iii) if any variable has a free occurrence in any necessary argument then that free occurrence is also free in t.

The aggregation of a ranked variable with its necessary arguments is intended to be the name of a single, new object. The condition on free variable occurrences in necessary arguments makes certain that an abstraction is not made into that name.

Example 4.6. Let Q be the prefix ∀_{a→a}^{1}f∀_{a→a}^{1}g∃_{a→a→a}A∀_{a}x. Then (fx), (f(gx)), and λw(Aw(gx)) are all Q-terms. On the other hand, f, λw(fw), and λw(A(gx)(fw)) are not Q-terms.

Notice that the complications mentioned in Examples 4.2 and 4.3 are not solved if we add ranks to the Skolem functions in them and reinterpreted Q-terms using ranked quantifiers. The proofs of Propositions 4.7 and 4.9 below can be found in (Miller, 1987).

Proposition 4.7. Let Q be a prefix and let t be a Q-term of type τ. If t is η-convertible to t′ then t′ is a Q-term of type τ. If t β-reduces to t′ then t′ is a Q-term of type τ. In particular, if Q = Q_{1}∃_{δ}xQ_{2} and s is a Q_{1}-term of type δ, then [s/x]t is a Q-term of type τ.

The converse of the statement regarding β-reduction is not true: if t′ reduces to the Q-term t then t′ is not necessarily a Q-term. For example, if Q is ∀_{a}y∀_{a→a}^{1}u, then the term y is a Q-term while (λw y)u is not.

Definition 4.8. Let f be a variable, and let s, t, and A be λ-terms. The deskolemizing operation D_{s}^{ft} is defined as follows: D_{s}^{ft}A is the result of replacing all subterms of A that are βη-convertible to ft by s. Of course, it may be necessary to change bound variable names in A to avoid capturing free variables of s.

Given that we equate two terms if they are alphabetic variants of each other, the operation D_{s}^{ft} is technically not well defined. For example, if D_{y}^{fx} is applied to the two equal terms λx.a(fx) and λz.a(fz), two different answers result, namely λx.ay and λz.a(fz). Fortunately, this cannot happen if f is declared to have a positive rank. For example, we have the following result.

Proposition 4.9. Let Q be the prefix Q_{1}∀_{τ→δ}^{p+1}f∃_{τ} xQ_{2}, let t be a Q_{1}-term of type τ, and let A and B be Q-terms. Then all the following are true.

(1) Any occurrence of y in D_{y}^{ft}A will have at least p arguments and any free variables in that occurrence’s first p arguments are free in D_{y}^{ft}A.

(2) If A is β-reducible to B then D_{y}^{ft}A is β-reducible to D_{y}^{ft}B.

(3) If A is the β-normal form of B, then D_{y}^{ft}A is the β-normal form of D_{y}^{ft}B.

(4) If A is η-convertible to B then D_{y}^{ft}A is η-convertible to D_{y}^{ft}B.

The term D_{y}^{ft}A may not be a Q_{1}∃x∀^{p}yQ_{2}-term since it may contain occurrences of f. We can, however, prove the following.

Lemma 4.10. Let Q be the prefix Q_{1}∀_{τ→δ}^{p+1}f∃_{τ} xQ_{2}, let t be a Q-term of type τ, and let A be a Q-term. Also assume that there exist Q_{1}-terms of type δ. Then A can be completely “deskolemized” with respect to f in the following fashion. Let {t, u_{1}, …, u_{m}} (m ≥ 0) be a set of terms that contains all terms u such that fu is a subterm of A. Let d_{1}, …, d_{m} be a list of (not necessarily distinct) Q_{1}-terms of type δ. The term

A′ := D_{d_{1}}^{fu_{1}}(… (D_{d_{m}}^{fu_{m}}(D_{y}^{ft}A)) …)

is a Q_{1}∃x∀^{p}yQ_{2}-term.

Proof. Clearly, A′ contains no occurrences of f. Consider an occurrence of the p-ranked variable y in A′. Such an occurrence of y arises from removing an occurrence of ft, which has at least p arguments. Hence, all the occurrences of y in A′ have at least p arguments. Finally, applications of the D operator cannot introduce any new bound variable dependencies. Therefore, A′ is a Q_{1}∃x∀^{p}yQ_{2}-term. □

The following theorem establishes the completeness for Skolemization. Soundness is only established in the case that the type of the variable being Skolemized is nonempty.

Theorem 4.11. Let D be a conjunction of equations such that

Q_{1}∃_{τ} x∀_{δ}^{p}yQ_{2}D  (∗)

is a unification problem. If this problem has a solution, the unification problem

Q_{1}∀_{τ→δ}^{p+1}f∃_{τ} xQ_{2}[fx/y]D  (∗∗)

has a solution. If there exists a Q_{1}-term of the type δ, the converse is true.

\underline{14 D. Miller}

Proof. Let θ be a solution for (∗) and let t be θx. Let

θ′ := {(z, [ft/y]s) | (z, s) ∈ θ}.

It is easy to verify that this substitution is a Q_{1}∀^{p+1}f∃xQ_{2}-substitution. Furthermore, if u and v are two terms such that θu and θv are βη-convertible, then [ft/y]θu and [ft/y]θv are βη-convertible. These last two terms, however, are simply equal to θ′([fx/y]u) and θ′([fx/y]v). Hence, θ′ is a solution to (∗∗).

Let θ be a Q_{1}∀^{p+1}f∃xQ_{2}-substitution that is a solution to (∗∗) and let t be θx. Let {t, u_{1}, …, u_{m}} (m ≥ 0) be a set of terms that contains all terms u such that fu is a subterm of some term in the range of θ. Let d_{1}, …, d_{m} be a list of (not necessarily distinct) β-normal Q_{1}-terms. Finally, let E be the operation Es := D_{d_{1}}^{fu_{1}}(… (D_{d_{m}}^{fu_{m}}(D_{y}^{ft}s)) …), and let θ′ := {(z, Es) | (z, s) ∈ θ}. We now show that θ′ is a solution to (∗).

Let (z, s) ∈ θ′. If z is in the prefix Q_{2} then s will contain no occurrences of f but may contain occurrences of y. If z is x, then s is Et, which cannot contain any occurrences of y since ft is not a subterm of t. If z is in the prefix Q_{1} then Es is the same as s since s contains no occurrences of f. Thus, using Lemma 4.10, θ′ is a Q_{1}∃x∀^{p}yQ_{2}- substitution. Furthermore, let u and v be two terms such that θ([fx/y]u) and θ([fx/y]v) are βη-convertible. These two terms are also equal to [ft/y]θu and [ft/y]θv, respectively. By repeated use of Proposition 4.9, the two terms E([ft/y]θu) and E([ft/y]θv) are βηconvertible. But these terms are equal to E(θu) and E(θv), which are the terms θ′u and θ′v. Hence, θ′ is a solution to (∗). □

Definition 4.12. If P is the unification problem (∗) and P′ is the unification problem (∗∗) above, we say that P′ is the result of Skolemizing P at ∀_{δ}^{p}y.

Example 4.13. The unification problem

∀_{a→a}f∀_{a→a}g∀_{a}u∃_{a}X∀_{a}y∃Z[(fX(gy)) =^{a} (fuZ)]

can be Skolemized to the unification problem

∀_{a→a}f∀_{a→a}g∀_{a}u∀_{a→a}^{1}k∃_{a}X∃_{a}Z[fX(g(kX)) =^{a} fuZ].

This problem has the solution {(X, u), (Z, g(ku))} and it can be deskolemized to {(X, u), (Z, gy)}.

For another example, consider the unification problem

∀_{a→a→a}g∀_{a}x∃_{a→a}F ∀_{a}y∃_{a}Z[F y =^{a} gyx ∧ Z =^{a} F y].

This can be Skolemized to the unification problem

∀_{a→a→a}g∀_{a}x∀_{(a→a)→a}^{1}k∃_{a→a}F ∃_{a}Z[F (kF) =^{a} g(kF)x ∧ Z =^{a} F (kF)].

Here, gx is a ∀_{a→a→a}g∀_{a}x-term of type a → a. There is exactly one solution for this unification problem, namely,

{(F, λw(gwx)), (Z, g(k(λw(gwx)))x)}.

If this solution is deskolemized, we get a solution for the original unification problem, namely, {(F, λw(gwx)), (Z, gyx)}.

Example 4.14. If we return to Example 4.3 and make certain that the type of the Skolemized variable is nonempty, we notice that deskolemizing will work correctly. Consider the modified unification problem ∀_{b}w∀_{a}z∀_{b→a}g∃_{a}X∀_{b}y ⊤ and its Skolemized form

∀_{b}w∀_{a}z∀_{b→a}g∀_{a→b}^{1}f∃_{a}X ⊤.

This latter unification problem now has solutions X ↦ z, x ↦ (gw), X ↦ g(fz), X ↦ g(f(g(fz))), etc. We can now deskolemize any of these solutions by replacing the subterms fz, f(g(fz)) etc. with w. All these solutions collapse down to just the two solutions for the original problem, namely X ↦ z and X ↦ (gw).

The more general case of Skolemization for nonprenex normal formulas of a higherorder logic is studied in (Miller, 1987). In the next section, we present the dual to Skolemization mentioned earlier.

5. Raising

The dual operation of rotating an existential quantifiers to the left over a universal quantifier will be called raising. In comparison to Skolemization, the metatheory of this rewriting process is particularly simple. It requires no new declarations, such as ranked quantifiers. Solutions before and after raising can be placed in one-to-one correspondence. The following theorem is the main result of this section.

Theorem 5.1. Let D be a conjunction of equations so that

Q_{1}∀_{τ} y∃_{δ}xQ_{2}D  (∗)

is a unification problem. This problem has a solution if and only if the unification problem

Q_{1}∃_{τ→δ}h∀_{τ} yQ_{2}[hy/x]D  (∗∗)

has a solution. Furthermore, a solution for either problem can be transformed in a oneto-one fashion to a solution of the other problem.

Proof. Let θ be a solution to (∗) and let t be θx. Set θ′ := θ − {(x, t)} and θ′′ := θ′ ∪ {(h, λyt)}. Clearly, θ′′ is a Q_{1}∃h∀yQ_{2}-substitution. Also, θ′′([hy/x]D) is equal to [(λyt)y/x](θ′D) which is nothing more than θD. Hence, θ′′ is a solution for (∗∗).

For the converse, let θ be a solution for (∗∗). Let t be the value of θh, and set θ′ := θ−{(h, t)} and θ′′ := θ∪{(x, ty)}. Clearly, θ′′ is a Q_{1}∀y∃xQ_{2}-substitution. Now, θ[hy/x]D is equal to [ty/x]θ′D which is the same as θ′′D. Hence, θ′′ is a solution to (∗).

The translations of solutions given in this proof put the solutions for (∗) in one-to-one correspondence with the solutions for (∗∗). □

Definition 5.2. If P is the unification problem (∗) and P′ is the unification problem (∗∗) above, we say that P′ is the result of raising P at ∃_{δ}x.

Example 5.3. Let a be a primitive type. The unification problem

∀_{a→a→a}f∀_{a}y∃_{a→a}X∀_{a}z[Xz =^{a} fzy]

can be raised twice to

∃_{(a→a→a)→a→a→a}H∀_{a→a→a}f∀_{a}y∀_{a}z[Hfyz =^{a} fzy].

\underline{16 D. Miller}

Using Proposition 2.7, this is solvable if and only if

∃_{(a→a→a)→a→a→a}H[λfλyλz.Hfyz = λfλyλz.fzy]

is provable. Here the type on this last equation is (a → a → a) → a → a → a. Since the left-hand side of the equation is η-convertible to H, the only solution to this unification problem is {(H, λfλyλz.fzy)}. By the proof Theorem 5.1, we know that the original unification problem has exactly one solution, namely {(X, λz.fzy)}.

Raising is closely related to a translation used in (Statman, 1981) where several simplifications in the presentation of unification problems are made. First, a unification problem with a ∃∀-prefix of the form

∃x_{1} … ∃x_{n}∀y_{1} … ∀y_{p}[t_{1} = s_{1} ∧ … ∧ t_{m} = s_{m}]  (∗)

is encoded by the two λ-terms

M_{1} := λx_{1} … λx_{n}λy_{1} … λy_{p}λz(zt_{1} … t_{m}) and
M_{2} := λx_{1} … λx_{n}λy_{1} … λy_{p}λz(zs_{1} … s_{m}).

The unification problem in (∗) has a solution if and only if there is a list of λ-terms, N_{1}, …, N_{n} such that for all i = 1, …, n, N_{i} can be given the same type as x_{i} is given in the prefix and such that

M_{1}N_{1} … N_{n} βη-converts to M_{2}N_{1} … N_{n}.  (∗∗)

A second simplification in (Statman, 1981) is that constants are not allowed in the terms M_{1} and M_{2}. Assume that the constants c_{1}, …, c_{q} (q ≥ 0) occurred in (∗) and hence in the terms M_{1} and M_{2}. Let z_{1}, …, z_{q} be variables that have no occurrences in (∗) and let φ be the mapping that when applied to a λ-term, replaces the constant c_{i} with z_{i} for all i = 1, …, q. Instead of using M_{1} and M_{2} to denote the unification problem (∗), Statman uses the following two constant-free terms:

M_{1}^{∗} := λw_{1} … λw_{n}λz_{1} … λz_{q}((φM_{1})(w_{1}z_{1} … z_{q}) … (w_{n}z_{1} … z_{q})) and
M_{2}^{∗} := λw_{1} … λw_{n}λz_{1} … λz_{q}((φM_{2})(w_{1}z_{1} … z_{q}) … (w_{n}z_{1} … z_{q})).

It is easy to show (∗∗) is satisfied if and only if

M_{1}^{∗}N_{1}^{∗} … N_{n}^{∗} βη-converts to M_{2}^{∗}N_{1}^{∗} … N_{n}^{∗},

where, for i = 1, …, n, N_{i}^{∗} is equal to λz_{1} … λz_{q}φN_{i}. In this sense, it is always possible to replace constants appearing in unification problems with abstracted variables.

The relationship of this translation of unification problems to raising is immediate. If the unification problem (∗) contained the constants c_{1}, …, c_{q}, we would have chosen to declare them explicitly in the prefix of (∗); that is, we would have written the unification problem as

∀z_{1} … ∀z_{q}∃x_{1} … ∃x_{n}∀y_{1} … ∀y_{p}[φt_{1} = φs_{1} ∧ … ∧ φt_{m} = φs_{m}].

By repeatedly raising its existential variables, this problem could be written into the form

∃w_{1} … ∃w_{n}∀z_{1} … ∀z_{q}∀y_{1} … ∀y_{p}[ρt_{1} = ρs_{1} ∧ … ∧ ρt_{m} = ρs_{m}],

where, for i = 1, …, n, w_{i} is the result of raising x_{i} by moving it left over ∀z_{1} … ∀z_{q}, and ρ is the substitution that results in applying φ and then replacing x_{i} with (w_{i}z_{1} … z_{q}) for i = 1, …, n. This latter unification problem is represented by the pair of λ-terms M_{1}^{∗} and M_{2}^{∗}.

The operation of ∀-lifting in (Paulson, 1989) is also related to raising in the sense that it can be presented as the backchaining inference rule followed by a sequence of raising steps (see (Miller, 1991b)).

6. Simplifying the Prefix of a Unification Problem

Skolemization can be used to rewrite a unification problem into a problem with a ∀∃- prefix: repeatedly move universal quantifiers left over existential quantifiers increasing their rank and their type as they move. Once a ∀∃-prefix is constructed, all the universal quantifiers can be replaced by “ranked” constants. The resulting unification problem is purely existential and as such can be dealt with by conventional unification processes, modified if necessary to handle such ranked constants. Since λ-abstractions are not available in the first-order setting, first-order unification does not need to be so modified. We show in the next section how the unification of λ-terms must be modified to deal correctly with ranked constants. Once a solution for the simplified unification problem is found, it can be converted to a solution of the original problem by repeatedly deskolemizing the solution, provided that all the types of Skolemized quantifiers are not empty.

In a similar manner, any prefix without positive ranked universal quantifiers can be rewritten using raising until it is an ∃∀-prefix. The resulting unification problem can further be simplified by taking the universally quantified variables in the prefix and λ-abstracting them over the terms in all the equations of the problem. The resulting unification problem again has only an existential prefix, with terms containing possibly long binders and high orders. For each universal quantifier an existential quantifier is moved over, the type of the variable being quantified is raised by giving it an additional argument. Thus, a unification problem that is first-order, that is, in which the existentially quantified variables are all of primitive type, would be converted to a unification problem with functional variables. This may seem undesirable given that several useful properties of first-order unification do not hold for unification involving functional variables. As shown in Section 12, the complexity introduced by raising is particularly simple. A raised first-order unification problem has a decidable unification problem and most general unifiers.

The two rewriting processes, Skolemization and raising, can be used together in the same prefix. Once a universal quantifier is moved left by Skolemization, no existential variable can be move left past it since raising can only involve universal quantifiers of rank zero. Prefixes of the form ∀∃∀ represents a natural reduction class for unification problems: the outermost universal quantified variables denote the constants of the problem while the inner most universal quantified variables denote the top-level λ-abstractions.

Of course, it is should be possible to take existing unification algorithms and modify them so that they can deal directly with general unification problems. This is the topic of the next section.

7. Reducing Unification Problems

This section is an adaptation of part of (Huet, 1975) to our mixed prefix setting. Several rewriting methods are presented that convert unification problems to, hopefully, more solvable problems.

\underline{18 D. Miller}

Following standard convention, equations occurring within unification problems will also be called disagreement pairs. The following classification of prefixed terms and disagreement pairs is central to the unification process describe below.

Definition 7.1. Any β-normal prefixed term Qt can be written uniquely as

Qλx_{1} … λx_{n}(yt_{1} … t_{m})

where n ≥ 0, m ≥ 0, and y is a variable. The binder of this term is the list x_{1}, …, x_{n}, its head is the variable y, and its arguments are the terms t_{1}, …, t_{m}.

If y is existentially quantified in Q, then Qt is flexible. Otherwise, y is either universally bound in Q or a member of the binder of t: in either case Qt is rigid.

Let P be a unification problem with prefix Q and let t =^{τ} s be an equation of P. (Of course, τ is a primitive type.) This equation is rigid-rigid if both Qt and Qs are rigid, is flexible-flexible if both Qt and Qs are flexible, and is flexible-rigid otherwise.

This classification is important because it captures the one invariance about substitution and β-normalization that we will use repeatedly: if Qt is rigid, then any Qsubstitution instance of Qt is rigid and has the same head as Qt. This invariance justifies the following simplification of rigid-rigid disagreement pairs. Let ht_{1} … t_{p} = ks_{1} … s_{q} be a rigid-rigid disagreement pair in a unification problem with prefix Q. If these two terms are to have instances that are λ-convertible under some substitution, their heads must be the same, p and q must be equal, and for i = 1, …, p, t_{i} and s_{i} must be simultaneously unifiable under the prefix Q.

Example 7.2. Using these observations, we can rewrite the unification problem

∀_{((i→i)→i)→i→i}f∀_{i}a∃_{i}V ∃_{i→i}W ∀_{i}b[f(λx(xa))V =^{i} f(λy(yV))(W b)]

into the term

∀f∀a∃V ∃W ∀b[λx(xa) =^{(i→i)→i} λy(yV) ∧ V =^{i} W b].

This is not a proper unification problem. Using Proposition 2.7, this term has the same solutions as the unification problem

∀f∀a∃V ∃W ∀b∀_{i→i}x[xa =^{i} xV ∧ V =^{i} W b].

This problem contains a rigid-rigid pair and can be rewritten as

∀f∀a∃V ∃W ∀b∀x[a =^{i} V ∧ V =^{i} W b].

This final unification problem contains no rigid-rigid disagreement pairs and cannot be simplified in this manner any further. The first pair is flexible-rigid while the second is flexible-flexible.

Definition 7.3. Let P be a unification problem that contains an equation of the form kt_{1} … t_{n} = ks_{1} … s_{n} (n ≥ 0). The process of rewriting P by replacing this equation with the conjunction t_{1} = s_{1} ∧ … ∧ t_{n} = s_{n} and then using Proposition 2.7 repeatedly to make the resulting term a unification problem is called the simplification rewriting step. If n = 0 then ⊤ replaces the equation k = k. A unification problem that contains no rigid-rigid pairs with the same head is a simplified unification problem.

The following proposition follows immediately.

Proposition 7.4. Using simplification and the rewriting rules (1), (2), (4), and (5) of Proposition 2.7, a unification problem P can be rewritten to a unification problem, say P′, in which there are either no rigid-rigid disagreement pairs or where some rigid-rigid disagreement pair is composed of terms with different heads. In either case, the solutions to P′ are exactly the same as the solutions to P. Furthermore, P′ is unique modulo α-conversion and the ordering of the rightmost universal variables of the prefix.

Further analysis of disagreement pairs will require the use of substitutions for existentially quantified variables. These substitutions will not, in general, be Q-substitutions (where Q is the prefix of the unification problem in question) since such substitutions replace existential variables with essentially closed or completed terms. We shall need the flexibility in building solutions incrementally by using substitution terms that are open, that is, that contain subterms that must be determined later. To this end, we introduce the following definitions.

Definition 7.5. Let Qt be a prefixed term where Q is of the form Q_{1}∃_{τ} fQ_{2}. A prefixed term Q_{1}∃H_{1} … ∃H_{n}s (n ≥ 0) is Q-free for f if it is of type τ. Here, we may assume that the variables H_{1}, …, H_{n} are not bound in Q. The result of substituting s for f in Qt, written as [f ↦ s]Qt, is the prefixed term

Q_{1}∃H_{1} … ∃H_{n}Q_{2}([s/f]t).

Similarly, if P is a unification problem, it can also be thought of as a prefixed term. Thus, the term [f ↦ s]P can be made into a unification problem by using β-reduction and the rewrites in Proposition 2.7.

If Q is of the form Q_{1}∃_{τ} fQ_{2} and if Q_{1}∃H_{1} … ∃H_{n}s is Q-free for f, the substitution [f ↦ s] is not generally a Q-substitution because s may contain existential variables of Q_{1} or it may contain new existential variables (namely, H_{1}, …, H_{n}). We shall make use of these kinds of substitutions, however, to build solutions for unification problems. The substitutions of the form [f ↦ s] used in this section will all be such that free variables of s are either universal variables of Q_{1} or are new existential variables. It will not be until Section 10 that such substitution terms will contain existential variables of Q_{1}.

Definition 7.6. Let σ be a Q_{1}∃H_{1} … ∃H_{n}Q_{2}-substitution and let Q_{1}∃H_{1} … ∃H_{n}s be a prefixed term that is Q_{1}∃_{τ} fQ_{2}-free for f. The composition of [f ↦ s] with σ, written [f ↦ s] ∘ σ, is the Q_{1}∃fQ_{2}-substitution given by

{(f, s′)} ∪ {(v, σv) | v ∈ dom(σ) and v ∉ {H_{1}, …, H_{n}}},

where s′ is the term part of the prefixed term σQ_{1}∃H_{1} … ∃H_{n}s. Composition associates to the right and satisfies the equation (f ∘ g)x = g(f(x)).

We shall occasionally suppress stating the prefix of Q_{1}∃H_{1} … ∃H_{n}s since it can be constructed from Q by taking the free variables of s not bound to the left of f as the variables H_{1}, …, H_{n} and then determining an appropriate type for those variables. The following proposition shows that when s is Q-free for f, [f ↦ s] can represent a component of a final complete solution.

\underline{20 D. Miller}

Proposition 7.7. Let P be a unification problem with prefix Q = Q_{1}∃_{τ} fQ_{2}. Let s be Q-free for f. Then [f ↦ s]P has solution σ if and only if P has solution [f ↦ s] ∘ σ.

Proof. Let Q_{1}∃_{τ} fQ_{2}t be a prefixed term and let Q_{1}∃H_{1} … ∃H_{n}s be Q-free for f. Let σ be a Q_{1}∃H_{1} … ∃H_{n}Q_{2}-substitution. The β-normal form of the formulas σ([f ↦ s]Q_{1}∃_{τ} fQ_{2}t) and ([f ↦ s] ∘ σ)Q_{1}∃_{τ} fQ_{2}t are the same. Let P be a unification problem with prefix Q_{1}∃_{τ} fQ_{2}. Since σ([f ↦ s]Q_{1}∃_{τ} fQ_{2}t) and ([f ↦ s] ∘ σ)Q_{1}∃_{τ} fQ_{2}t are the same, [f ↦ s]P has solution σ if and only if P has solution [f ↦ s] ∘ σ. □

We can now return to the construction of solutions to unification problems. Consider the case where only one term of a disagreement pair is rigid; the other one being flexible. For example, let ft_{1} … t_{p} = ks_{1} … s_{q} be a disagreement pair and assume that f is existentially quantified while k is a universally quantified. For these to be unifiable, f must be instantiated with a term that, after β-normalization, puts k at the head of the flexible term. There are two general ways to place k at the head since there are two processes that are used to make these terms equal, namely, substitution and λ-reduction.

Straightforward substitution can make the flexible term look like the rigid one if the substitution term for f has head k. That is, the substitution term imitates the head of the rigid term. However, λ-reduction can also be performed on disagreement pairs after a substitution. Thus the term substituted for f could be used to migrate subterms of the flexible term that might contain k into the head position of the flexible term. This method of placing k at the head of a the flexible term is indirect and, hence, will often produce several possible substitution terms. Immediate subterms in the flexible term can be accessed by a sequence of projections. For example, to place the i^{th} argument t_{i} of the flexible term in the head position, a substitution term for f would be an abstraction of the variables λw_{1} … λw_{p} over a term with w_{i} as its head. The result of substituting such a term for f and then normalizing will leave a term whose head is equal to the head of t_{i}. If the head of t_{i} is k then we have succeeded in our goal. If the head is a universally quantified variable different than k, we have failed and need to backtrack to other choices. If the head of t_{i} is an existentially quantified variable, we could use such a projection term again to access subterms of t_{i}, or try to use imitation on the flexible head of t_{i}.

Let us now be more precise about both the imitation and projection schemes for getting a flexible head to match a rigid head. Assume that we are given the flexiblerigid disagreement pair ft_{1} … t_{p} = ks_{1} … s_{q} where f is existentially quantified and k is universally quantified.

If k is quantified to the right of f, the imitation scheme cannot be used since the substitution term for f cannot contain k. If k is quantified to the left of where f is quantified, then it is possible to make the head of the flexible term become k directly. Let r be the rank of k. If r = 0 then the imitation term for f is a λ-term of the form

λw_{1} … λw_{p} (k(H_{1}w_{1} … w_{p}) … (H_{q}w_{1} … w_{p})),

which has the same type as f. This term takes each of the p arguments of the flexible term and constructs a new term with k as the head and whose arguments depend functionally on the arguments of the flexible term. Notice that this functional dependency is left unspecified; H_{1}, …, H_{q} are unspecified higher-order variables. Examining just the surface structure of the rigid term does not provide any information on how these new variables should be instantiated. Their determination is attempted later after simplification removes more of the surface structure.

Notice that if the rank r is positive then the substitution term suggested above is not a valid Q-term. This is easily corrected, however, by restricting the first r arguments of this substitution term to not be functionally dependent on the abstracted variables. In particular, the correct substitution term would be

λw_{1} … λw_{p} (kH_{1} … H_{r}(H_{r+1}w_{1} … w_{p}) … (H_{q}w_{1} … w_{p})).

Since we have assumed that the terms in unification problems are Q-terms themselves, r ≤ q and this term is sensible.

In either case, the displayed term is called the imitation term for the given disagreement pair. We shall require that the free variables H_{1}, …, H_{q} do not appear in the given unification problem’s prefix. Notice that an imitation term is unique up to the choice of these free variables and the bound variables w_{1}, …, w_{p}.

Finally, we need to consider the projection scheme for matching a flexible head to a rigid head. In this case, we only try to rearrange the flexible term so that one of its arguments is moved into the head position. In particular, consider all the terms of the same type as f that are of the form

λw_{1} … λw_{p} (w_{i}(H_{1}w_{1} … w_{p}) … (H_{m}w_{1} … w_{p})),

where m ≥ 0, 1 ≤ i ≤ p, and H_{1}, …, H_{m} are variables that do not occur in the prefix of the given unification problem. All such terms are Q-terms and are never of primitive type. There are, of course, p or fewer such terms, if we do not count differences in the names of their free and bound variables. Such a term instructs the flexible term to project its i^{th} argument to its head and to give it any additional arguments (the m arguments in the term above) it might need for the entire term to be the same type of function as f. A projection term for the given flexible-rigid disagreement pair is any of these terms.

Notice that all of the substitution terms above are designed to be functionally dependent on all p arguments of the flexible term. Such terms need not be functional on all such arguments, but if η-conversion is available, then we only need to consider the terms built here. If η-conversion is not available, as in the first part of (Huet, 1975), then more imitation and projection terms need to be considered.

Definition 7.8. Let P be a unification problem with prefix Q = Q_{1}∃_{τ} fQ_{2} and with a flexible-rigid disagreement pair ft_{1} … t_{p} = ks_{1} … s_{q}. We shall write imit(f, τ, k, Q) to be either the empty set if k is bound to the right of f or the set {Q_{1}∃H_{1} … ∃H_{q}t} where t is the imitation term described above. Similarly, we write proj(f, τ, Q) to be the set of all projection terms generated above for type τ with the appropriate prefix added. Finally, we define match(f, τ, k, Q) = imit(f, τ, k, Q) ∪ proj(f, τ, Q). Any term in this set is a match term for the disagreement pair ft_{1} … t_{p} = ks_{1} … s_{q}. The values of imit, proj, and match are unique up to alphabetic changes of bound variables. The argument Q is used during building the imitation term to determine the rank of k and whether or not k is to the right or left of f. It is also used to constrain the picking of the variables H_{1}, …, H_{n} since these cannot appear in Q.

Example 7.9. Let i and a be primitive types. Let Q be ∀k∀^{1}l∃F ∀j where the variables k, j all have type i → i and l has the type i → i → i → i. The following are some values of imit. (The prefixes for the various match terms presented below are suppressed: they are

\underline{22 D. Miller}

all of the form ∀k∀^{1}l∃H_{1} … ∃H_{i} where i ≥ 0 is the number of new existential variables free in the term.)

\begin{matrix}imit(F, i, k, Q) = & \{kH_{1}\} \\ imit(F, i → i, k, Q) = & \{λw(k(H_{1}w))\} \\ imit(F, i → a, k, Q) = & \{\} \\ imit(F, i → i, j, Q) = & \{\} \\ imit(F, (i → i) → i → i, l, Q) = & \{λw_{1}λw_{2}(lH_{1}(H_{2}w_{1}w_{2})(H_{3}w_{1}w_{2}))\} \end{matrix}

In this last imitation term, the types of w_{1} and w_{2} are i → i and i, while the types of H_{1}, H_{2}, and H_{3} are i, (i → i) → i → i and (i → i) → i → i, respectively. Below are some values of proj.

\begin{matrix}proj(F, i → i → a, Q) = & \{\} \\ proj(F, i → i, Q) = & \{λw w\} \\ proj(F, i → i → i, Q) = & \{λw_{1}λw_{2} w_{1}, λw_{1}λw_{2} w_{2}\} \\ proj(F, (i → i) → i → i, Q) = & \{λw_{1}λw_{2} (w_{1}(H_{1}w_{1}w_{2})), λw_{1}λw_{2} w_{2}\} \end{matrix}

In order to facilitate a completeness proof for this unification rewriting process, we define the following complexity measures on terms and substitutions.

Definition 7.10. Let t be a β-normal term. Let |t| denote the number of occurrences of applications in t. That is,

|λx_{1} … λx_{n}(ht_{1} … t_{m})| = m + ∑_{i=1}^{m} |t_{i}| (n, m ≥ 0).

Let σ be the substitution {(w_{1}, t_{1}), …, (w_{n}, t_{n})} where n ≥ 0. Then |σ| is defined as

|σ| = n + ∑_{i=1}^{n} |t_{i}|.

The following proposition is critical for establishing a completeness theorem later.

Proposition 7.11. Let P be a simplified unification problem that has solution σ. Also assume that the prefix Q of P is of the form Q_{1}∃_{τ} F Q_{2} and that P contains a flexiblerigid disagreement pair with F as the flexible head and k as the rigid head. Then there exists a unique prefixed term Q_{1}∃H_{1} … ∃H_{n}s in match(F, τ, k, Q) (n ≥ 0) and a unique Q_{1}∃H_{1} … ∃H_{n}-substitution ρ with domain {H_{1}, …, H_{n}} such that

(1) σF β-converts to ρs.

Furthermore, let σ′ be the substitution ρ ∪ (σ − {(F, σF)}). Then

(2) σ = [F ↦ s] ∘ σ′,

(3) σ′ is a solution to the unification problem [F ↦ s]P, and

(4) |σ′| < |σ|.

Proof. Let t be the β-normal form of σF. Then t is of the form λw_{1} … λw_{n}(ct_{1} … t_{m}) for some variables c, w_{1}, …, w_{n} and terms t_{1}, …, t_{m} (n, m ≥ 0). Since t is Q-closed for F, the variable c must be either universally bound in Q or a member of the list w_{1}, …, w_{m}. In the first case, the head of the flexible term will become c. Since the unification problem P has a solution, c must be k. Let s be the imitation term for this flexible-rigid pair. If c is a member of the list w_{1}, …, w_{m}, then by the construction of match terms, there is a unique term, say s ∈ match(F, τ, k, Q), which projects the same member of the binder to its head. In either case, let H_{1}, …, H_{p} be the new free variables of s, listed in the left-to-right order they appear in s (p ≥ 0). If we define ρ = {(H_{i}, λw_{1} … λw_{m}t_{i}) | i = 1, … p}, we see that t is β-convertible to ρs (hence, showing (1) above). Notice also that |t| = m + ∑_{i=1}^{m} |t_{i}|. Let σ′ be as defined in the theorem. Then (2) obviously holds. Since ([f ↦ s] ∘ σ′)P is equal to the prefixed term σP, σ′ is a solution to [x ↦ s]P (showing (3)). Finally,

|σ′| = |σ| − |t| + ∑_{i=1}^{m} |t_{i}| − 1 + m

which simplifies to |σ′| = |σ| − 1 (conclusion (4) above). □

Definition 7.12. A unification problem containing either no equations or only flexibleflexible equations is called a flexible-flexible unification problem.

In Section 8, we consider the general problem of determining when flexible-flexible problems have solutions. Consider the following example of a flexible-flexible unification problem that does not have a solution.

Example 7.13. Let a, b, and c be primitive types. Consider the following flexible-flexible unification problem:

∀_{a→b}y∃_{a→b}F ∀_{c→b}z∃_{c→b}G∀_{a}u∀_{c}v [F u =^{b} Gv].

Although all existentials in this prefix are nonempty, this unification problem has no solution.

We can now organize the two rewriting rules of simplification and substitution with matching terms into a search process for flexible-flexible unification problems. Such a search is often referred to as pre-unification.

Definition 7.14. Let P and P′ be unification problems. We shall write P →_{s}^{F} P′ if all the following conditions are true.

(1) P is in simplified form,

(2) F is an existentially quantified in P,

(3) there is a flexible-rigid pair in P in which the flexible term has F as its head,

(4) s is a matching term for this pair, and finally,

(5) P′ is the simplified form of [F ↦ s]P.

These rewriting rules can be used to nondeterministically decompose unification problems with solutions to flexible-flexible unification problems with solutions.

\underline{24 D. Miller}

Proposition 7.15. Let P be a simplified unification problem. P has a solution σ if and only if there exists a sequence of rewrite steps

P →_{s_{1}}^{F_{1}} … →_{s_{n}}^{F_{n}} P′ (n ≥ 0)

where P′ is a flexible-flexible problem with solution ρ and σ = [F_{1} ↦ s_{1}]∘⋯∘[F_{n} ↦ s_{n}]∘ρ.

Proof. Let P be a simplified unification problem. If a sequence of unification problems as above carries P to a flexible-flexible problem with solution ρ, then by induction and Propositions 7.4 and 7.7, P has the solution σ, defined in the theorem. Assume the converse, however, that P has a solution, say σ. Then a sequence of such rewriting steps must exist and its length is bounded by |σ|. The following simple nondeterministic procedure will construct such a sequence. Let σ_{1} be σ, let P_{1} be P, and pick any flexiblerigid pair in P. Let F_{1} be the head of the flexible term. By Proposition 7.11, this pair determines a nonempty set of matching terms that contains a unique term s_{1} such that [F_{1} ↦ s_{1}]P has a solution σ_{2} where |σ_{2}| < |σ| and σ = [F_{1} ↦ s_{1}] ∘ σ_{2}. Let P_{2} be a simplified form of [F_{1} ↦ s_{1}]P. If P_{2} is a flexible-flexible problem, then we are finished. Otherwise, we repeat this selection of a flexible-rigid pair and a match term again on this new unification problem. This process must terminate since each subsequent call to the unification process will reduce the complexity of a solution the unification problem. □

N.B. In the rest of this paper, we shall assume that unification problems will not contain universal quantifiers of positive rank. This assumption is taken to simplify the presentation of various different technical definitions in the following sections. While most of these definitions can be generalized to handle positively ranked universal quantifiers, doing so complicates those definitions without adding to their content.

8. Solving Flexible-Flexible Problems

Flexible-flexible unification problems are considered “reduced” in the sense that the principal invariant used in Section 7, that rigid terms preserve their heads under substitution, is not useful when examining flexible-flexible unification problems. We now show that deciding whether or not a flexible-flexible unification problem has a solution is undecidable. For the next three lemmas and one theorem, let i be a primitive type. Proofs for the lemmas are straightforward and not given.

Lemma 8.1. Let t be a closed β-normal term of type (i → i) → i → i. Then t is ηconvertible to a term of the form λfλx.f^{n}x for some n ≥ 0.

Closed λ-terms of type (i → i) → i → i are called Church numerals. For n ≥ 0, we write n̂ to denote the n^{th} Church numeral, that is, the term λfλx.f^{n}x. For example, ˆ0 = λfλx.x, ˆ1 = λfλx.fx, and ˆ2 = λfλx.f(fx).

Lemma 8.2. The flexible-flexible unification problem

∃_{(i→i)→i→i}N∀_{i→i}f∀_{i}x[Nf(Nfx) =^{i} (Nf(fx))]

has the unique solution {(N, ˆ1)}.

Lemma 8.3. Let the existential quantifiers below associate type (i → i) → i → i to their bound variables. The flexible-flexible unification problem

∃M∃N∃P ∀_{i→i}f∀_{i}x[(Nf)(Mf)x =^{i} P fx]

has solution {(N, r), (M, s), (P, t)} if and only if for some n, m ≥ 0, r is n̂, s is m̂, and t is n̂ + m. The flexible-flexible unification problem

∃M∃N∃P ∀_{i→i}f∀_{i}x[N(Mf)x =^{i} P fx]

has solution {(N, r), (M, s), (P, t)} if and only if for some n, m ≥ 0, r is n̂, s is m̂, and t is n̂ × m.

The outline of the following proof is suggested by the main proof in (Goldfarb, 1981).

Theorem 8.4. The problem of determining if a given flexible-flexible unification problem has a solution is recursively undecidable.

Proof. Using the preceding three lemmas, it is simple to encode any finite set of equation of the form x = 1, x+y = z, and x×y = z into a flexible-flexible unification problem such that the unification problem has a solution if and only if the set of equations has an interpretation of its variables over nonnegative integers such that all the equations are true. In this encoding, each variable in an equation would correspond to an existential variable of type (i → i) → i → i, and each equation would correspond to a flexible-flexible disagreement pair. Since the problem of determining if such a set of equations can be solved over the nonnegative integers is recursively unsolvable (Hilbert’s Tenth Problem), the problem of determining if flexible-flexible unification problems have solutions is recursively unsolvable. Notice that the unification problems needed for this encoding are only second-order; that is, the highest order of any variables in these prefixes is 2. □

There are many flexible-flexible unification problems for which it is easy to compute a solution. The following proposition describes such a collection of flexible-flexible unification problems.

Proposition 8.5. Let P be a flexible-flexible unification problem with prefix Q. Let E be the set of existential variables of Q, and let ≈^{0} be the relation on E such that x ≈^{0} y if and only if x and y are the heads of a common disagreement pair of P. Let ≈ be the equivalence closure of ≈^{0}. Let E be some ≈-equivalence class, let τ be the common target type of the variables in E, and let Q′ be the prefix to the left of the leftmost variable in E. Call the set E solvable if there is a Q′-term of type τ. Finally, if all equivalence classes of E are solvable, then P has a solution.

Proof. The following proof is a simple extension of a proof given in (Huet, 1975). Let E be an equivalence class of existential variables of the prefix Q, let τ be their common target type, let Q′ be the prefix to the left of the leftmost variable in E, and let t be a Q′-term of type τ. For each variable x in E substitute the λ-term λw_{1} … λw_{n}.t, where n is the unique nonnegative integer needed to make this term the same type as x and the variables w_{1}, …, w_{n} are not free in t. In this way, a substitution for all the existential variables of Q can be built. It is immediate that this substitution is a solution for P. □

\underline{26 D. Miller}

In the event that a unification problem has a ∀∃-prefix, then the above proposition reduces to simply checking if each of the primitive types labeling equations in the unification problem are nonempty with respect to the purely universal part of the prefix.

When flexible-flexible unification problems have solutions, computing all solution can be difficult. Although Proposition 8.5 can be used occasionally to produce some solutions to some flexible-flexible unification problems, it provides no information on the nature of other solutions available. Such unification problems may have an infinite number of incomparable solutions and no nonredundant enumeration of a complete set of solutions for general flexible-flexible unification problem is possible (Huet, 1975).

9. Some Unsolvable Unification Problems

We now identify some classes of unification problems that have no solutions.

Definition 9.1. A simple failure problem is a simplified unification problem containing a disagreement pair that is either (i) rigid-rigid (thus, its terms have different heads), or (ii) flexible-rigid and the set of matching terms for this pair is empty.

Theorem 9.2. If P is a simple failure node then it has no solutions.

Proof. Let P be a simple failure unification problem. There are two cases to consider. If P contains a rigid-rigid disagreement pair with different heads, then no substitution into these terms can make them equal and P can have no solution. From Proposition 7.11 it follows that if P has a solution, every flexible-rigid disagreement pair in P must have a nonempty set of match terms. Thus, if P contains a flexible-rigid pair that has an empty set of match terms, P could not have a solution. □

The analysis required to recognize simple failure unification problems is inexpensive: only the surface structure of the terms involved need to be examined. The remaining failure cases presented in this section are more costly to determine. The following two definitions generally require the examination of much of a term’s structure.

Definition 9.3. Let Qt be a prefixed formula. The binary relation → →^{0} on prefixed terms is defined by the following two rules. First, Qλxt → →^{0} Q∀xt, provided x is not a member of the prefix Q (otherwise change the name of x before moving it to the prefix). Second, Q(ht_{1} … t_{n}) → →^{0} Qt_{i} provided h is a universally quantified variable in Q and 1 ≤ i ≤ n. Let → → be the transitive closure of → →^{0}. A variable w of Q is said to have a permanent occurrence in Qt if Qt → → Q′(wt_{1} … t_{n}) for some prefix Q′, n ≥ 0, and some terms t_{1}, …, t_{n}.

The proof of the following proposition is done by a simple induction on the structure of terms: the proof is omitted.

Proposition 9.4. Let t be a β-normal Q-term and let y be a universally quantified variable of Q that has a permanent occurrence in Qt. If σ is a Q-substitution, then y has a permanent occurrence in σQt. If s is Q-free for f in Q, then y has a permanent occurrence in [f ↦ s]Qt.

Definition 9.5. Let t be a β-normal Q-term. A universally bound variable y of Q possibly occurs in Qt if y occurs free in t or y is to the left of some existential variable of Q that occurs free in t.

The following proposition justifies this use of terminology.

Proposition 9.6. Let P be a unification problem with prefix Q and a disagreement pair t = u. If there exists a universally quantified variable y in Q that does not have a possible occurrence in t but does have a permanent occurrence in u, then P has no solution.

Proof. Assume that σ is a solution for P. By Proposition 9.4, y has an occurrence in σu. Since y does not occur in t and since the existential variables free in t are on the left of y, σt does not contain an occurrence of y. Hence, σt and σu are not equal and this contradicts the assumption that σ is a solution to P. □

Example 9.7. The unification problem

∀_{i→i}y∃_{(i→i)→i}H∀_{i→i}x[x(Hx) =^{i} Hy]

has no solution since x has a permanent occurrence in x(Hx) while it has no possible occurrence in Hy.

Below we present a different class of unsolvable unification problems. They can be recognized as such by noticing how a simple strategy of applying matching terms would produce a cyclic pattern in the search for a solution.

Definition 9.8. Let prefix Q be of the form Q_{1}∃xQ_{2}. Consider an equation of the form xs_{1} … s_{n} = t where n ≥ 0 and for every i = 1, …, n, Qs_{i} has a head that is bound universally in Q_{2}. Let Y be the set of heads of the terms s_{1}, …, s_{n}. Finally, assume that x has a permanent occurrence in t witnessed by the sequence of prefixed terms

Qt = Q_{1}t_{1} → →^{0} … → →^{0} Q_{m}t_{m} = Q′(xe_{1} … e_{n}) (m ≥ 2),

where for all i = 1, …, m − 1, the head of t_{i} is not in the set Y. Such an equation is a simple divergent equation.

The following is a generalization of the occurrence-check found with in first-order unification.

Proposition 9.9. If P is a unification problem with a simple divergent disagreement pair, P has no solution.

Proof. We shall show that if P is a unification problem with a simple divergent disagreement pair and with a solution, say σ, then there is another unification problem P′ with a simple divergent disagreement pair and a solution σ′ where |σ′| < |σ|. From this, a contradiction quickly follows: if n = |σ|, use the above argument n + 1 times to reach the conclusion that there is some unification problem whose solution has negative size.

Thus, let P contain a simple divergent disagreement pair xs_{1} … s_{n} = t, and let Y be as defined in Definition 9.8. Let t be kt_{1} … t_{p} where p ≥ 1 and let j ∈ {1, …, n} be such that x has a permanent occurrence in the term t_{j} satisfying the same condition

\underline{28 D. Miller}

regarding the set Y. By assumption, k ∉ Y. Since P has a solution, there is a match term s for this equation such that P →_{s}^{x} P′ where P′ has a solution σ′ with |σ′| < |σ| and σ = [x ↦ s] ∘ σ′. If s is a projection term, then P′ contains a rigid-rigid disagreement pair whose heads are k and the head of s_{i} for some i = 1, …, m. Such a P′ is a simple failure problem since these heads are different: if k is in Q_{1} then k cannot equal the head of s_{i} by assumption on s_{i}, and if k is in Q_{2}, then k cannot be equal to the head of s_{i} since it is a member of Y.

Thus s must be the imitation term and k is bound in Q_{1}. Let the imitation term, s, be written as

λy_{1} … λy_{n}(k(H_{1}y_{1} … y_{n}) … (H_{p}y_{1} … y_{n})).

Thus, P′ contains the β-normal form of the equation H_{j}s_{1} … s_{n} = [s/x]t_{j}. Since t_{j} contained a permanent occurrence of x and the head of s is a universal variable not in Y, this pair is then a simple divergent disagreement pair. This completes the proof. □

Example 9.10. Consider the unification problem

∀_{i→i}a∃_{i→i}X∀_{i}u[Xu =^{i} a(Xu)].

Since X occurs permanently in a(Xu) and that occurrence is not under u, this unification problem has no solution. Another way to see this is to notice that the imitation term for the disagreement pair in this unification problem is λw .a(Hw) for a new variable H of the same type as X. Substituting this into the unification problem yields the problem ∀a∃H∀u[Hu =^{i} a(Hu)], which is simply an alphabetic variant of the original problem. Since this problem cannot be rewritten into a flexible-flexible problem, Proposition 9.1 implies that this problem has no solution.

On the other hand, consider the following unification problem taken from (Huet, 1975):

∀_{i}a∃_{(i→i)→i}X∀_{i→i}u[Xu =^{i} (u(X(λv v)))].

Although X occurs rigidly in u(X(λv v)), this theorem does not apply to this problem since X occurs under u. This unification problem actually does give rise to a flexibleflexible problem since substituting the projection term λw(w(Hw)) for X and simplifying yields ∀a∃H∀u[Hu = H(λv v)]. This has the solution, {(H, λz a)}, and the original problem has the solution {(X, λw(wa)}.

To see why Proposition 9.9 provides a generalization of the occurrence-check in firstorder unification, assume that the equation x = s is first-order, x is different than s, and that x occurs in s. Thus, x has a permanent occurrence in s and the restriction on the permanent occurrence is vacuously true. As the proposition concludes, there is no unifier for any unification problem containing this equation.

10. Factors of Unification Problems

In this section, we will capitalize on the fact that occasionally there are unification problems whose solutions all share certain features. Recognizing such cases and features permits a search strategy to commit to a particular approach to constructing an initial portion of a solution without needing to consider backtracking. The common structure of solutions, when they exist, will be called factors.

Definition 10.1. Let P be a unification problem with prefix Q. Let P_{0} be P and Q_{0} be Q. A list of quadruples

(f_{1}, s_{1}, Q_{1}, P_{1}), …, (f_{n}, s_{n}, Q_{n}, P_{n}) (n ≥ 1)

is called a cascading substitution for P if for i = 1, …, n, the term s_{i} is Q_{i−1}-free for the variable f_{i} and P_{i} is the simplified unification problem [f_{i} ↦ s_{i}]P_{i−1} and Q_{i} is the prefix of P_{i}. We shall denote by [f_{1} ↦ s_{1}] ∘ ⋯ ∘ [f_{n} ↦ s_{n}] the function that carries Q_{n}- substitutions σ to the Q-substitution [f_{1} ↦ s_{1}] ∘ ⋯ ∘ [f_{n} ↦ s_{n}] ∘ σ. We shall frequently refer to just the expression [f_{1} ↦ s_{1}] ∘ ⋯ ∘ [f_{n} ↦ s_{n}] as a cascading substitution. The syntactic variable ψ will be used to denote cascading substitutions. If ψ′ denotes the above cascading substitution and if ψ′′ denotes a cascading substitution for P_{n}, then their composition, written as ψ′ ∘ ψ′′, is the concatenation of their list of quadruples. The interpretation of ψ′ ∘ψ′′ as a mapping on substitutions is given by composing the meaning of the interpretation of both ψ′ and ψ′′.

Definition 10.2. Let P be a unification problem. We say that a cascading substitution [f_{1} ↦ s_{1}] ∘ ⋯ ∘ [f_{n} ↦ s_{n}] for P is a factor of P if for every solution σ of P there is a solution σ′ for [f_{n} ↦ s_{n}](⋯ ([f_{1} ↦ s_{1}]P) ⋯) such that σ = [f_{1} ↦ s_{1}]∘⋯∘[f_{n} ↦ s_{n}]∘σ′. This factor is a proper factor if whenever σ and σ′ exist as above, |σ′| < |σ|. Otherwise, it is improper.

Notice that if P is an unsolvable unification problem, then every cascading substitution for P is a factor for P.

Example 10.3. It is possible for an improper factor ψ to increase the size of a substitution; that is, for σ = ψ ∘ σ′ and |σ′| > |σ| to hold. The unification problem ∀_{a}c∃_{a}F.F =^{a} c has the single solution {(F, c)}. It also has the factor [F ↦ (H_{1}H_{2})] where

∀_{a}c∃_{a→a}H_{1}∃_{a}H_{2} (H_{1}H_{2})

is ∀_{a}c∃_{a}F -free for F. Now

{(F, c)} = [F ↦ (H_{1}H_{2})] ∘ {(H_{1}, λw.w), (H_{2}, c)}

but |{(H_{1}, λw.w), (H_{2}, c)}| = 2 and |{(F, c)}| = 1.

Without exception, we shall be interested only in improper factors that keep the size of solutions constant. Such improper factors always exist for unification problems containing existential quantifiers in their prefix. For example, let x be existentially bound with type τ_{1} → … → τ_{n} → τ_{0} where n ≥ 0. If π is a permutation of {1, …, n}, the substitution [x ↦ λw_{1} … λw_{n}.Hw_{π1} … w_{πn}] is an improper factor. This is a kind of renaming operation: x is renamed to H with the possibilities that its arguments are permuted. We shall find improper factor useful since it is possible that applying such a factor to a unification problem yields a problem that is syntactically simplier although its solutions are not “smaller”.

Proposition 10.4. Let ψ′ be a factor of P and let ψ′′ be a factor of ψ′P. Then ψ′ ∘ ψ′′ is a factor of P. Furthermore, if both ψ′ and ψ′′ are proper factors then so is ψ′ ∘ ψ′′.

Proof. Let σ be a solution to P. Then there is a σ′ such that σ′ solves ψ′P and σ = ψ′ ∘ σ′. Since ψ′′ is a factor of ψ′P, then there exists a solution σ′′ of ψ′′(ψ′P) such

\underline{30 D. Miller}

that σ′ = ψ′′ ∘ σ′′. Thus, σ = (ψ′ ∘ ψ′′) ∘ σ′′ and σ′′ solves (ψ′ ∘ ψ′′)P. Hence, (ψ′ ∘ ψ′′) is a factor. If ψ′ and ψ′′ are proper, then |σ′| < |σ| and |σ′′| < |σ′|, so |σ′′| < |σ| and ψ′ ∘ ψ′′ is proper. □

The following proposition shows that factors identified for a subset of the equations in a unification problem are factors for the full unification problem.

Proposition 10.5. Let P and P′ be two unification problems with the same prefixes and be such that the disagreement pairs of P are all contained in P′. It follows that any factor of P must be a factor of P′.

Proof. Let ψ be a factor of P and let σ be a solution of P′. Thus, σ is a solution of P and σ = ψ ∘ σ′ for some σ′ where σ′ is a solution to ψP. Thus, σ′ is also a solution to ψP′. □

We shall now present four different classes of factors: the first two classes are proper and are presented in Propositions 10.6 and 10.8. The third and fourth classes, presented in the next section, are improper factors that can be used to prune existential variables of functional types; that is, such variables are replaced with existential variables of fewer arguments. The first class of proper factors is provided as an immediate corollary of Proposition 7.11.

Proposition 10.6. Let P be a unification problem that contains a flexible-rigid pair with x as the flexible head. If the set of match terms for this disagreement pair is a singleton set, say {s}, then [x ↦ s] is a proper factor of P.

The second class of proper factors arises by generalizing on the usual definition of variable-term disagreement pairs found in first-order unification.

Definition 10.7. Let P be a unification problem with prefix Q. A variable defining disagreement pair is a pair of the form xy_{1} … y_{n} = t where n ≥ 0, x is an existentially quantified in Q and does not occur free in t, the variables y_{1}, …, y_{n} are distinct and universally quantified to the right of x, and λy_{1} … λy_{n}t is Q-free for x.

Notice that a variable defining disagreement pair could be flexible-rigid as well as flexible-flexible.

Proposition 10.8. Let P be unification problem with the variable defining disagreement pair xy_{1} … y_{n} = t. The substitution [x ↦ λy_{1} … λy_{n}t] is a proper factor of P.

Proof. Let σ be a solution for P. Let s be σx and let σ′ := σ/{(x, s)}. Using β and η-conversion, we can assume that s is of the form λy_{1} … λy_{n}s′, where s′ is βη-convertible to σt which is also equal to σ′t since x is not free in t. Hence, [x ↦ λy_{1} … λy_{n}t] ∘ σ′ = {(x, λy_{1} … λy_{n}σ′t)}∪σ′ = σ. Thus, [x ↦ λy_{1} … λy_{n}t] is a factor that is also proper since |σ′| = |σ| − 1 − |s|. □

Example 10.9. Consider the equation

λy_{1} … λy_{n}.Xy_{π1} … y_{πn} = t

where π is a permutation of {1, …, n}, none of the variables X, y_{1}, …, y_{n} are free in t, and the prefix to this equation is of the form ∀∃. Then the substitution

[X ↦ λy_{π1} … λy_{πn}.ty_{1} … y_{n}]

is a factor.

The substitution provided in the above proposition is the first instance of a substitution that replaces an existential variable with a term that may contain another existential variable in the current unification problem. In all other substitutions so far, substitution terms contained either universal variables or new existential variables.

11. Pruning Unification Problems

We now consider two classes of improper factors we collectively call pruning factors. In each case, an existential variable, say x, of functional type is replaced by a new existential variable, say h, of one fewer arguments. This is done using the substitution

ψ = [x ↦ λw_{1} … λw_{n}(hw_{1} … w_{i−1}w_{i+1} … w_{n})]

where n ≥ 0 and 1 ≥ i ≥ n. If ψ is a factor, then it must be an improper factor: let σ and σ′ be substitutions such that σ = ψ ∘ σ′. There must be some term u and some substitution σ′′ that contains neither x nor h in its domain and is such that σ is {(x, λw_{1} … λw_{n} u)} ∪ σ′′ and σ′ is {(h, λw_{1} … λw_{i−1}λw_{i+1} … λw_{n} u)} ∪ σ′′. Since the only difference in these substitutions is in the number of abstractions in substitution terms, and since these are not counted by | |, |σ| = |σ′|.

Proposition 11.1. Let P be a unification problem with a disagreement pair xt_{1} … t_{n} = s, where x is existentially bound with type τ_{1} → ⋯ → τ_{n} → τ_{0} and where τ_{0}, …, τ_{n} are primitive types. If there is a universal variable y that has a permanent occurrence in t_{i}, for some i = 1, …, n, and that does not have a possible occurrence in s, then

ψ = [x ↦ λw_{1} … λw_{n}(hw_{1} … w_{i−1}w_{i+1} … w_{n})]

is an improper factor for P.

Proof. Let xt_{1} … t_{n} = s be as in the theorem, with the universal variable y occurring permanently in t_{i} but not having a possible occurrence in s. Let σ be a solution for P. Since σs cannot contain y free, y cannot be free in σ(xt_{1} … t_{n}). Since y occurs permanently in t_{i}, it also occurs permanently in σt_{i}. Now σx is η-convertible to a λ-term of the form λw_{1} … λw_{n} u where the abstracted variables are of primitive type. If w_{i} is free in u then σ(xt_{1} … t_{n}) would contain σt_{i} as a subterm and y would be free in σ(xt_{1} … t_{n}), which is not possible. Thus, σ = ψ ∘ σ′ where σ′ is

{(h, λw_{1} … λw_{i−1}λw_{i+1} … λw_{n} u)} ∪ {(v, σ(v)) | v ∈ dom(σ) and v ≠ x}.

Hence, ψ is a factor. By the discussion above, it must be an improper factor. □

Example 11.2. The unification problem

∃_{i→i}F ∃_{i→i}G∀_{i}x∀_{i}y[F x =^{i} Gy]

has [F ↦ λw H_{1}] as a pruning substitution. A pruned form of this unification problem is therefore ∃H_{1}∃G∀x∀y[H_{1} = Gy]. This has [G ↦ λw H_{2}] as a pruning substitution.

\underline{32 D. Miller}

A pruned form of this problem is then ∃H_{1}∃H_{2}∀x∀y[H_{1} = H_{2}]. Thus, the compound substitution, [F ↦ λw H_{1}] ∘ [G ↦ λw H_{2}] is a factor of the original unification problem.

For another example, consider the unification problem

∀_{i→i→i}c∃_{i→i→i}∃_{i→i→i}G∀_{i}x∀_{i}y[G(cxy)(cyy) =^{i} F yy].

This problem has a pruning substitution, namely [G ↦ λw_{1}λw_{2}(Hw_{2})]. The resulting unification problem is the simpler ∀c∃F ∃H∀x∀y[H(cyy) = F yy].

The restriction on the type of the variable being prune is necessary as the unification problem

∀_{i}a∃_{(i→i)→i→i}X∀_{i}y[X(λz.a)y =^{i} a]

shows. Here, y has a permanent occurrence in the second argument of X while it does not have a possible occurrence in the term a. It is not the case, however, that the substitution [X ↦ λw_{1}λw_{2}(Hw_{1})] is a factor for this unification. In particular, the solution [X ↦ λz_{1}λz_{2}(z_{1}z_{2})] is not in the image of that substitution.

The type information in a prefix can be used to suggest pruning substitutions. For example, consider the prefix Q_{1}∃_{δ→τ} fQ_{2}. A solution for a unification problem with this prefix must provide f with a term of type δ → τ whose free variables are all universally quantified in Q_{1}. As describe in Section 3, it is possible to use the type information in Q_{1} to determine if there is a term of type δ → τ. This same type information can be used to determine more about the possible substitution terms for f. For example, it is possible to determine whether there is a term, say λx.t, of type δ → τ in which x is free in t. If such a term does not exist, then the pruning substitution [f ↦ λw.h] is a factor.

In order to determine this structural property given the type information in a prefix, we modify the proof system in Definition 3.5 to enforce that a particular hypothesis is used in a proof.

Definition 11.3. Let Δ be a finite set of types including the type δ. The relation Δ ⊢_{I}^{δ} τ, for type τ, is defined by the following clauses.

(1) Δ ⊢_{I}^{δ} δ.

(2) Δ ⊢_{I}^{δ} τ_{1} → τ_{2} if {τ_{1}} ∪ Δ ⊢_{I}^{δ} τ_{2}.

(3) Δ ⊢_{I}^{δ} τ if δ is δ_{1} → ⋯ → δ_{n} → τ and Δ ⊢_{I} δ_{1}, …, Δ ⊢_{I} δ_{n} (n ≥ 0).

(4) Δ ⊢_{I}^{δ} τ if δ_{1} → ⋯ → δ_{n} → τ ∈ Δ and Δ ⊢_{I} δ_{1}, …, Δ ⊢_{I} δ_{n} and for some i = 1, …, n, Δ ⊢_{I}^{δ} δ_{i} (n ≥ 1).

Proposition 11.4. The relationship Δ ⊢_{I}^{δ} τ is decidable.

Proof. Provability of Δ ⊢_{I}^{δ} τ can only depend on the provability of statements of the form Δ′ ⊢_{I}^{δ} τ′ or Δ′ ⊢_{I} τ′ where τ′ is a subexpression of some type in {τ, δ} ∪ Δ and Δ′ is some finite set of similar types. In particular, there are only a finite number of such values for Δ′ and τ′, so the length of any proof for Δ ⊢_{I}^{δ} τ can be bounded prior to looking for a proof. □

Proposition 11.5. Let Δ be the set of types for quantified variables in the prefix Q. There is a β-normal Q-term λx.t of type δ → τ such that x is free in t if and only if Δ ⊢_{I}^{δ} τ.

Proof. Assume that Δ ⊢_{I}^{δ} τ. We show by induction on the length of a proof of this fact that if Q∀_{δ}x is a prefix whose quantifiers are typed by types in Δ, then there is a Q∀_{δ}x-term of type τ that contains x free. If δ is τ then the required term is simply x. Assume that τ is τ_{1} → τ_{2} and that {τ_{1}} ∪ Δ ⊢_{I}^{δ} τ_{2}. By the inductive hypothesis, there is a Q∀_{τ_{1}}y∀_{δ}x-term t′ of type τ_{2} such that x is free in t′. Thus, λy.t′ is the required Q∀_{δ}x-term of type τ which contains x free. Assume that δ is δ_{1} → ⋯ → δ_{n} → τ and that Δ ⊢_{I} δ_{1}, …, Δ ⊢_{I} δ_{n} (n ≥ 0). By Proposition 3.6, there are Q∀_{δ}x-terms, t_{i}, of type δ_{i} for i = 1, …, n. Thus, (xt_{1} … t_{n}) is the required Q∀_{δ}x-term of type τ which contains x free. Finally, assume that δ_{1} → ⋯ → δ_{n} → τ ∈ Δ and Δ ⊢_{I} δ_{1}, …, Δ ⊢_{I} δ_{n} and for some i = 1, …, n, Δ ⊢_{I}^{δ} δ_{i} (n ≥ 0). Again, there are Q∀_{δ}x-terms, t_{i}, of type δ_{i} for i = 1, …, n, one of which contains x free. Thus, if c is bound in Q∀_{δ}x at type δ_{1} → ⋯ → δ_{n} → τ then (ct_{1} … t_{n}) is the required Q∀_{δ}x-term of type τ which contains x free.

Let λx.t be a β-normal Q-term of type δ → τ such that x is free in t. We show by induction on the structure of t that if Δ is the set of types in Q, then Δ ⊢_{I}^{δ} τ. If t is a variable, then t is x, and we have Δ ⊢_{I}^{δ} δ by rule (1). If t is λy.t′, then y is different from x and τ is τ_{1} → τ_{2}. Thus λx.t′ is a β-normal Q∀_{τ_{1}}y-term of type δ → τ_{2}. The inductive hypothesis, {τ_{1}} ∪ Δ ⊢_{I}^{δ} τ_{2}, and rule (2) completes this case. Finally, assume that t is of the form (ct_{1} … t_{n}) for c a variable and for some n > 0. We now have two cases: either c is x or x appears free in t_{i} for some i = 1, …, n. In the first case, δ is of the form δ_{1} → ⋯ → δ_{n} → τ where t_{i} is a Q-term of type δ_{i}. By Proposition 3.6 and rule (3), the conclusion follows. Finally, assume that c is not x. Thus x is free in t_{i} for some i = 1, …, n and c is quantified in Q with type δ_{1} → ⋯ → δ_{n} → τ, and the type of t_{i} is δ_{i}. This case is completed by the inductive hypothesis, Proposition 3.6, and rule (4) above. □

The following Proposition is now an immediate consequence.

Proposition 11.6. Let P be a unification problem with prefix Q_{1}∃_{δ→τ} fQ_{2} and let Δ be the set of types that include δ and all the types of quantified variables in Q_{1}. If Δ ⊢_{I}^{δ} τ is not provable then [f ↦ λw.H] is a factor for P, where H is a variable not in Q.

Example 11.7. Let list, int, bool, and bt be four primitive types. Let Q be the prefix that contains universal quantifiers for the following pairs of variables and types:

\begin{matrix}true, & bool & false, & bool \\ zero, & int & succ, & int → int \\ node, & int → bt → bt → bt & leaf, & int → bt \\ sign, & int → bool & nil, & list \\ bcons, & bool → list → list & icons, & int → list → list \end{matrix}

Notice that all primitive types and all types built using these primitive types are nonempty. Let Δ be the set of types displayed above. The chart below describes when the relation Δ ⊢_{I}^{δ} τ holds given that τ and δ range over the primitive types above. There is a “Y ” in the row δ and column τ if Δ ⊢_{I}^{δ} τ can be proved; otherwise there is an “N”.

list int bool bt
list Y N N N
int Y Y Y  Y
bool Y N Y  N
bt N N N Y

\underline{34 D. Miller}

Thus, if a unification problem has the prefix Q∃fQ′ where the type for f is list → int → bool → bt, this chart can be used to infer that [f ↦ λw_{1}λw_{2}λw_{3}.hw_{2}] is a factor.

12. A Subcase of Unification

As an illustration of using some of the technical devices defined in the previous sections, we investigate a class of unification problems in which the search for a pre-unifier give rise to no important choices. That is, if such unification problems have solutions, they have factors that rewrite them into flexible-flexible unification problems. This class contains all first-order unification problems: factors of such problems correspond to most general unifiers. It also contains the class of raised first-order unification problems described in Section 6.

In this section we shall assume that prefixes are restricted to have low orders. In particular, prefixes are restricted so that the type of existentially quantified variables are of order 1 or 0 and universally quantified variables to the right of some existential variable are of primitive type.

Definition 12.1. A β-normal prefixed term Qt of type τ is an argument-restricted term if the order of τ is 0 or 1 and every subterm of t of the form xt_{1} … t_{n} (n ≥ 0) where x is existentially quantified in Q is such that the terms t_{1}, …, t_{n} have as heads distinct variables that are either universally quantified in Q to the right of x or are internally λ-abstracted variables. A unification problem is argument-restricted if it is argumentrestricted as a prefixed term.

Notice that any unification problem comprised of only first-order terms is trivially an argument-restricted unification problem. This set of unification problems also has useful closure properties.

Proposition 12.2. Let P be an argument-restricted unification problem. Let P′ be the result of Skolemizing, raising, simplifying, pruning, or applying match terms to P. Then P′ is argument-restricted.

Proof. If P′ results from Skolemizing P, P′ is argument-restricted since Skolemization only introduces new occurrences of existentially quantified variable occurrences which are not applied to any arguments. Since simplifying does not introduce any occurrences of existentially quantified variables, the result of simplifying an argument restricted prefixed term is also argument restricted.

If P′ results from raising P, then various subterms of P of the form xt_{1} … t_{n} are replaced with subterms of the form hyt_{1} … t_{n} where y, which is to the left of x in P and is not at the head of any term in t_{1}, …, t_{n}, is to the right of h in P′. The heads of the terms y, t_{1}, …, t_{n} are thus all distinct. Also since y is of primitive type, the type of h is of order 1.

Since pruning has the effect of tossing out arguments to existentially quantified variables, if P′ results from pruning P, then P′ is clearly argument-restricted.

The case of verifying the application of match terms is slightly more involved. Let Qt be an argument-restricted prefixed term where the prefix is of the form Q_{1}∃zQ_{2} and let s be a match term for z. We show by induction on |t| that the β-normal form of [z ↦ s]Qt is a variable-restricted prefixed term. Let H_{1}, …, H_{m} be the free variables of s that are not bound in Q and let Q′ be the prefix Q_{1}∃H_{1} … ∃H_{m}Q_{2}. Thus [z ↦ s]Qt is equal to Q′[s/z]t. If |t| = 0 then t is a variable and [z ↦ s]Qt is either Q′t or Q′s. In either case, the result is argument-restricted.

Now assume that |t| > 0. Thus, t is of the form λu_{1} … λu_{p}(ae_{1} … e_{n}) where p ≥ 0, n > 0, a is a variable, and the variables u_{1}, …, u_{p} are not free in s. Let a′, e′_{1}, …, e′_{n} be the β-normal forms of [z ↦ s]a, [z ↦ s]e_{1}, …, [z ↦ s]e_{n}, respectively. By the inductive hypothesis, these terms are argument-restricted. If a is a variable other than z, then the β-normal form of [z ↦ s]Qt is Q′λu_{1} … λu_{p}(ae′_{1} … e′_{n}), which is argument-restricted. If a is the variable z then e′_{1}, …, e′_{n} all have distinct variable heads that are either universally quantified in Q to the right of z, are in the set {u_{1}, …, u_{p}}, or are bound internally. If s is the imitation term, which is of the form λw_{1} … λw_{n} k(H_{1}w_{1} … w_{n}) … (H_{m}w_{1} … w_{n}), then the β-normal form of [z ↦ s]Qt is

Q′λu_{1} … λu_{p}k(H_{1}e′_{1} … e′_{n}) … (H_{m}e′_{1} … e′_{n}).

Since the terms e′_{1} … e′_{n} all have the necessary distinct heads, the term [z ↦ s]Qt must also be argument-restricted. If s is a projection term then it must have the form λw_{1} … λw_{n} w_{i} for some i = 1, …, n since the type of z is at most order 1. Thus, [z ↦ s]Qt reduces to Q′λu_{1} … λu_{p}.e′_{i}, which is argument-restricted. □

Example 12.3. The restrictions on the order of types in the definition of argumentrestricted are necessary to achieve closure under the substitution of projection terms. For example, consider the prefixed term

Q∃Y ∃X∀a∀f.Y (λw(f(Xaw)))a,

where Q is some prefix and the types declared for Y, X, a, and f are (i → i) → i → i, i → i → i, i, and i → i, respectively. This prefixed term is not argument-restriction only because the type of Y is of order 2. Applying the projection term λw_{1}λw_{2}.w_{1}(Hw_{1}w_{2}) for Y yields the prefixed term

Q∃H∃X∀a∀f.f(Xa(H(λw(f(Xaw)))a))),

which is not argument-restricted for the additional reason that the variable X has an argument that has the existentially quantified variable H as its head.

Our main theorem about this class of unification problems follows from this lemma.

Lemma 12.4. Let P be a simplified, argument-restricted unification problem. If P is neither a simple failure problem nor a flexible-flexible problem then there exists a proper factor ψ such that ψP is an argument-restricted unification problem.

Proof. Since P is neither a simple failure problem nor a flexible-flexible problem, it must contain a flexible-rigid pair, say xt_{1} … t_{n} = ks_{1} … s_{m}, with x being the existentially quantified variable. Since P is not a simple failure, the set of match terms for this equation is nonempty. Although this set may not be a singleton, at most one substitution term in this set can lead to a solution. To see this, consider the variable k. If k is universally bound to the left of x in Q, then the imitation term is the only match term that can lead to a solution. If k is universally bound to the right of x in Q, then the only possible match terms leading to a solution are the projection terms. Such projection terms would move one of the arguments, say t_{i}, into the head position. In this case, the head of t_{i}

\underline{36 D. Miller}

must be the same as k. By assumption, however, there is exactly one such term t_{i} since all the terms t_{1}, …, t_{n} have distinct rigid heads. Thus, the projection term that maps the i^{th} argument of x to the head position must be a factor. In either case, let s be this distinguished match term. The substitutions [x ↦ s] is the desired factor. □

Theorem 12.5. Let P be an argument-restricted unification problem that is not flexibleflexible. If a solution to P exists, there exists a proper factor ψ of P such that ψP is a flexible-flexible unification problem.

Proof. Let P be a simplified, argument-restricted unification problem with solution σ. Also assume that P is not flexible-flexible. Hence, P is not a simple failure problem. We proceed by induction on |σ|. By Lemma 12.4, P has a proper factor, say ψ, and ψP is an argument-restricted unification problem. If ψP is a flexible-flexible unification problem then we are finished. Otherwise, ψP has a solution σ′ such that σ = ψ ∘ σ′ and |σ′| < |σ|. By the inductive hypothesis, ψP has a factor ψ′ such that ψ′(ψP) is a flexible-flexible unification problem. The desired proper factor is ψ ∘ ψ′. □

The subset of argument-restricted unification problems in which existentially quantified variables are applied to terms that are distinct variables bound either internally or to the right of the existential variable is an interesting class of problems. This subset is called L_{λ}-unification in (Miller, 1991b) and appears to be the weakest extension to first-order unification that treats bound variables via the equations of βη-conversion. Unification in L_{λ} is decidable and most general unifiers exist when unifiers exist. Unlike above where unification needed to be restricted to essentially second-order, L_{λ} is ω-ordered.

13. Related Work

For a summary of the early work done on the unification of simply typed λ-terms, see (Huet, 1975). Section 7 is largely a modification of the part of (Huet, 1975) that deals with unification modulo βη-conversion. Snyder & Gallier (1989) present the material of (Huet, 1975) in terms of transformations on sets of equations and provide new completeness proofs. Several abstract properties of unification problems are developed in (Statman, 1981). A declarative specification of simply typed λ-term unification is given in (Miller, 1991a) using a logic programming language as the vehicle for specifying search and λ-term syntax.

The earliest applications of βη-unification were in automating some aspects of deduction in higher-order logic. Theorem proving procedures that incorporated such unification are described in (Andrews et al., 1984; Huet, 1973b; Jensen & Pietrzykowski, 1976; Pietrzykowski, 1971; Pietrzykowski & Jensen, 1976). Also, certain problems regarding the length of proofs can be formulated as unification problems (Farmer, 1984).

A higher-order extension to Horn clauses incorporating βη-unification of simply typed λ-terms is described in (Nadathur, 1987; Nadathur & Miller, 1990) and used as the foundations for an extension of Prolog, called λProlog (Nadathur & Miller, 1988). The Elf logic programming language (Pfenning, 1991) employs βη-unification of dependenttyped λ-terms (Elliott, 1989; Pym, 1990).

The unification of simply typed λ-terms has occasionally been adopted as a component of programs that must manipulate logical expressions or other programs. Huet and Lang (1978) demonstrated that second-order matching, a decidable subset of λ-term unification, could be used to analysis and transform programs in a natural fashion. Their ideas were enriched by moving their analysis into λProlog (Hannan & Miller, 1988; Hannan & Miller, 1989; Miller & Nadathur, 1987). In the domain of the manipulation of logical expressions, λ-term unification has been used to implement inference rules in the Isabelle theorem prover (Paulson, 1986; 1989) and in theorem provers written in λProlog (Felty & Miller, 1988; Felty, 1989). Elliott and Pfenning (1988) further extended this notion and refer to the use of λ-terms and unification to analyze logical expressions and programs as higher-order abstract syntax. Acknowledgements. I am grateful to Peter Andrews, Masami Hagiya, Sunil Issar, Gopalan Nadathur, Larry Paulson, Frank Pfenning, David Wolfram, and the anonymous referees for useful comments on an earlier drafts of this paper. This work was supported in part by the grants ONR N00014-88-K-0633, NSF CCR-87-05596, and DARPA N00014-85-K-0018, and by a British Science and Engineering Research Council visiting fellowship research grant.

References

Andrews, P. (1971). Resolution in Type Theory. Journal of Symbolic Logic 36, 414 – 432. Andrews, P. (1972). General Models and Extensionality. Journal of Symbolic Logic 37, 395 – 397. Andrews, P., Cohn, E., Miller, D., Pfenning, F. (1984). Automating higher order logic. In Automated

Theorem Proving: After 25 Years, eds. W. Bledsoe and D. Loveland, American Mathematical Society, Providence, RI, 169 – 192.

Andrews, P. (1986). An Introduction to Mathematical Logic and Type Theory. Academic Press, 1986. Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56 – 68. Elliott, C., Pfenning, F. (1988). Higher-Order Abstract Syntax. Proceedings of the ACM-SIGPLAN

Conference on Programming Language Design and Implementation, 199 – 208, ACM Press. Elliott, C. (1989). Higher-Order Unification with Dependent Types. Rewriting Techniques and Applica-

tions, Springer-Verlag LNCS 355, 121 – 136. Farmer. W. (1984). Length of Proofs and Unification Theory. PhD. dissertation, University of Wisconsin,

Madison. Felty, A., Miller, D. (1988). Specifying Theorem Provers in a Higher-Order Logic Programming Language.

Proceedings of the Ninth International Conference on Automated Deduction, Argonne, IL, eds. E. Lusk and R. Overbeek, Springer-Verlag LNCS 310, 61 – 80.

Felty, A. (1989). Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming

Language. PhD dissertation, University of Pennsylvania. Goldfarb, W. (1981). The Undecidability of the Second-Order Unification Problem. Theoretical Computer

Science 13, 225 – 230. Hannan, J., Miller, D. (1988). Uses of Higher-Order Unification for Implementing Program Transform-

ers. Fifth International Conference and Symposium on Logic Programming, ed. K. Bowen and R. Kowalski, MIT Press, 942 – 959.

Hannan, J., Miller, D. (1989). A Meta Language for Functional Programs. Meta-Programming in Logic

Programming, eds. H. Rogers and H. Abramson, MIT Press. Henkin, L. (1950). Completeness in the theory of types. Journal of Symbolic Logic 15, 81 – 91. Hindley, J., Seldin, J. (1986). Introduction to Combinators and λ-calculus. Cambridge University Press. Huet, G. (1973a). The Undecidability of Unification in Third Order Logic. Information and Control 22,

257 – 267. Huet, G. (1973b). A Mechanization of Type Theory. Proceedings of the Third International Joint Con-

ference on Artificial Intelligence, 139 – 146. Huet, G. (1975). A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1, 27 –

57. Huet, G., Lang, B. (1978). Proving and Applying Program Transformations Expressed with Second-

Order Patterns. Acta Informatica 11, 31 – 55. Jensen, D., Pietrzykowski, T. (1976). Mechanizing ω-Order Type Theory Through Unification. Theoret-

ical Computer Science 3, 123 – 171. Lucchesi, C. (1972). The Undecidability of the Unification Problem for Third Order Languages. Report

CSRR 2059, Dept. of Applied Analysis and Computer Science, University of Waterloo. Miller, D. (1987). A Compact Representation of Proofs. Studia Logica 46/4, 345 – 368.

\underline{38 D. Miller}

Miller, D. (1991a). Unification of Simply Typed Lambda-Terms as Logic Programming. Eight Interna-

tional Logic Programming Conference, Paris, ed. K. Furukawa, MIT Press, 255 – 269. Miller, D. (1991b). A Logic Programming Language with Lambda-Abstraction, Function Variables, and

Simple Unification. Journal of Logic and Computation 2/4, 497 – 536. Miller, D., Nadathur, G. (1987). A Logic Programming Approach to Manipulating Formulas and Pro-

grams. Symposium on Logic Programming, San Franciso, ed. S. Haridi, IEEE Press, 379 – 388. Nadathur, G. (1987). A Higher-Order Logic as the Basis for Logic Programming. PhD dissertation,

University of Pennsylvania. Nadathur, G., Miller, D. (1988). An Overview of λProlog. Fifth International Conference on Logic

Programming, MIT Press, 810 – 827. Nadathur, G., Miller, D. (1990). Higher-order Horn Clauses. Journal of the ACM, 37/4, 777 – 814. Paulson, L. (1986). Natural Deduction as Higher-Order Resolution. Journal of Logic Programming 3/3,

237 – 258. Paulson, L. (1989). The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning, 5,

363 – 397. Pfenning, F. (1988). Partial Polymorphic Type Inference and Higher-Order Unification. Proceedings of

the 1988 ACM Conference on Lisp and Functional Programming. Pfenning, F. (1991). Logic Programming in the LF Logical Framework. In Logical Frameworks, eds. G.

Huet and G. Plotkin, Cambridge University Press, 149 – 181. Pietrzykowski, T. (1971). A Complete Mechanization of Second-Order Logic. Journal of the ACM 20/2,

333 – 364. Pietrzykowski, T., Jensen, D. (1976). Mechanizing ω-Order Type Theory Through Unification. Theoret-

ical Computer Science 3, 123 – 171. Pym, D. (1990). Proofs, Search and Computation in General Logic. PhD dissertation, University of

Edinburgh. Snyder, W., Gallier, J. (1989). Higher Order Unification Revisited: Complete Sets of Transformations.

Journal of Symbolic Computation, 8/1 – 2, 101 – 140. Statman, R. (1979). Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoretical Com-

puter Science 9, 67 – 72. Statman, R. (1981). On the Existence of Closed Terms in the Typed λ-Calculus II: Transformations of

Unification Problems. Theoretical Computer Science 15, 329 – 338.