A Complete Transformation System for Polymorphic Higher-Order Unification

Ullrich Hustadt

MPI–I–91–228 December 1991 Author’s Address

Ullrich Hustadt Max-Planck-Institut für Informatik Im Stadtwald W-6600 Saarbrücken Germany

E-mail: Ullrich.Hustadt@mpi-sb.mpg.de

Abstract

Polymorphic higher-order unification is a method for unifying terms in the polymorphically typed λ-calculus, that is, given a set of pairs of terms S_{0} = {s_{1} =^{?} t_{2}, …, s_{n} =^{?} t_{n}}, called a unification problem, finding a substitution σ such that σ(s_{i}) and σ(t_{i}) are equivalent under the conversion rules of the calculus for all i, 1 ≤ i ≤ n.

I present the method as a transformation system, i.e. as a set of schematic rules U ⟹ U′ such that any unification problem δ(U) can be transformed into δ(U′) where δ is an instantiation of the meta-level variables in U and U′. By successive use of transformation rules one possibly obtains a solved unification problem with obvious unifier. I show that the transformation system is correct and complete, i.e. if δ(U) ⟹ δ(U′) is an instance of a transformation rule, then the set of all unifiers of δ(U′) is a subset of the set of all unifiers of δ(U) and if U is the set of all unification problems that can be obtained from successive applications of transformation rules from an unification problem U, then the union of the set of all unifiers of all unification problems in U is the set of all unifiers of U.

The transformation rules presented here are essentially different from those in Snyder and Gallier (1989) or Nipkow (1990). The correctness and completeness proofs are in lines with those of Snyder and Gallier (1989).

Keywords

Higher-order unification, Polymorphic Lambda-Calculus

1 Introduction

Since the beginning of the 1970s a variety of higher-order theorem provers and higher-order programming languages have been invented. The languages used in these systems are based on the Simple Theory of Types defined in Church (1932). This theory is based on three sets of rules: The term formation rules define how to build expressions describing the application of a function to an object and the abstraction of a function from an expression describing an object. These rules are governed by the classification of objects into types. Types are either basic types or function types (A → B) where A and B are again types. The conversion rules define equivalence classes on terms. Turning the conversion rules into reduction rules gives an description of application evaluation. Deduction rules describe how formulas, which are simply terms of a designated type, can be proved.

In theorem proving most implementations lift the resolution principle well-known for first-order theorem proving to the higher-order case. For example Gordon (1985) and Paulson and Nipkow (1990) respectively describe the theorem provers HOL and Isabelle. Higher-order programming languages augment some PROLOG-like language with the term formation and reduction rules of the Simple Theory of Types. See for example Miller and Nadathur (1986) and Pfenning (1989) for descriptions of the programming languages λProlog and ELF, respectively.

The core of these systems is an implementation of unification of terms in the Simple Theory of Types, higher-order unification for short. All these implementations are based on the algorithmic description of the correct and complete higher-order unification algorithm given in Huet (1975). In Snyder and Gallier (1989) this algorithmic description is reformulated using the method of transformations on system of terms, which is based on Herbrand’s thesis and was adapted to first-order unification in Martelli and Montanari (1982). A unification problem is a set of pairs S_{0} = {s_{1} =^{?} t_{1}, …, s_{n} =^{?} t_{n}} of terms to be unified. By repeated application of various transformation rules one possibly obtains a solved system S_{n} whose unifier is obvious. The correctness of the transformation rules ensures that every unifier of a solved system S_{n} is also a unifier of S_{0}. A complete set of transformation rules allows to enumerate a complete set of unifiers by examing all possible transformation sequences.

Soon the limitations of the simple type theory for the formulation of axiom system and programs became apparent. Various extensions of the simple type theory were suggested. One of the most prominent extensions is the polymorphic λ-calculus. Beside the basic types it allows the usage of type variables in type formation, so it is possible to describe a family of types as instances of a single type.

To deal with these extensions the higher-order unification algorithm has to be modified. But none of the current implementations provides a complete algorithm. Nipkow (1990) presents a correct but incomplete transformation system for polymorphic higher-order unification. His transformation system is only able to enumerate a complete set of unifiers for sure if none of these unifiers instantiates a type variable with a function type. Dougherty (1991) presents a complete algorithm for unification in the polymorphic λcalculus. In his approach the problem of higher-order unification is translated to the problem of unification with respect to extensional equality in combinatory logic. Solving a unification problem in the λ-calculus involves translating it into a system of combinatory terms, computing unifiers using his transformation rules, and translating back the unifiers into unifiers in the λ-calculus. Although this approach allows for a very elegant presentation of the problem and its solution, it basically uses narrowing and some additional rules to transform the systems of combinatory terms and inherits all weaknesses of narrowing.

We will present a correct and complete transformation system HPT for polymorphic higher-order unification. The transformation rules are essentially different from the rules in Snyder and Gallier (1989) or Nipkow (1990). The correctness and completeness proofs are in line with those of Snyder and Gallier (1989). We define a verification system CPT , show that for every unifier for a given unification problem one can find a terminating sequence of transformations resulting in a solved system whose associated solution is this unifier. Then we show that every transformation in CPT corresponds to a sequence of transformations in HPT . This enables us to enumerate a complete set of unifiers by systematically applying all possible transformations in HPT to the unification problem.

2 Polymorphic Terms and Substitutions

Definition 2.1 (Types) Let T_{0} be a set of base types and V_{T} a set of type variables. The set of types T is inductively defined as the smallest set containing T_{0} and V_{T} such that if S, T ∈ T then (S → T) ∈ T . An element of either T_{0} or V_{T} is called a atomic type. △

Definition 2.2 (Terms) The set RL^{P oly} of raw terms is defined by the following abstract syntax

RL^{P oly} = V | (Σ: T ) | (V: T ) | (RL^{P oly} · RL^{P oly}) | λ V: T . RL^{P oly}

where V is a set of term variables and Σ a set of constants. We suppose V, Σ, and V_{T} to be pairwise disjoint. To define the set L^{P oly} ⊆ RL^{P oly} of well-typed terms, we use the following inference rules:

Bound variable:  \begin{aligned}& \frac{x:T ∈ Γ}{Γ ⊢ x:T} , \\ if & x ∈ V ∧ T ∈ T \end{aligned}

Free variable:  \begin{aligned}& \overline{Γ ⊢ (F: T):T} , \\ if & F ∈ V ∧ T ∈ T \end{aligned}

Constant:  \begin{aligned}& \overline{Γ ⊢ (c: T):T} , \\ if & c: T ∈ C ∧ T ∈ T \end{aligned}

Application:  \frac{Γ ⊢ M:(S → T) Γ ⊢ N:S}{Γ ⊢ (M · N):T}
Abstraction:  \frac{Γ ⊕ x:S ⊢ M:T}{Γλ x: S. N:(S → T)}

The set L^{P oly} is the set of all M ∈ RL^{P oly} such that ϵ ⊢ M:T for some T ∈ T . The set of all free variables is FV. The type variables have no special meaning for type inference. They act like nullary type constructors.

△

Definition 2.3 (type and range) We define the function range : T → T as follows:

range(T)  = T  if T ∈ T_{0}
range(T)  = T  if T ∈ V_{T}
range((S → T)) = range(T) otherwise

The functions type : L^{P oly} → T and range : L^{P oly} → T are defined by

type(M)  = T  iff ϵ ⊢ M:T
range(M)  = T  iff ϵ ⊢ M:S and range(S) = T
△

α-, β- and η-conversion on terms is defined in the usual way. We ignore α-conversion by working with α-equivalence classes of terms. The strong normalization property holds for β-reduction on polymorphically typed terms, so any term M has a unique β-normal form denoted M ↓. With any term M in β-normal form we can associate a unique η-expanded form η[M]. The set of all terms in η-expanded form is Lη^{P oly}. Any term M in β-normal form can be represented in general form λ x_{1}: S_{1}. . . . .λ x_{n}: S_{n}.(((a · P_{1}) ⋯) · P_{n}) which is also denoted λ x_{1}: S_{1} … x_{n}: S_{n}. a(P_{1}, …, P_{n}) or λ \overline{x_{n}: S_{n}}. a(\overline{P_{n}}). We call \overline{x_{n}: S_{n}} the binder of M, a the head, which is also denoted head(M), and a(\overline{P_{n}}) the matrix of M. If a is a constant or bound variable, e is called rigid, otherwise it is called flexible.

Definition 2.4 (Bound and free variables) A bound variable x is called bound in a term M_{1} if M_{1} contains a subterm of the form λ x: T. M_{2}. The subterm M_{2} is the scope of this binding occurrence of x: T. The set of all bound variables of a term M_{1} is denoted BV(M_{1}).

A free variable (F: T) ∈ FV is a free variable of M_{1} or is said to occur free in M_{1} if it is a subterm of M_{1}. The set of free variables of a term M_{1} is denoted FV^{Term}(M_{1}).

The set of all type variables occurring in some type decoration in a term M_{1} is denoted FV^{Type}(M_{1}). The set of all free term and type variables of a term M_{1} is denoted FV(M_{1}). △

Definition 2.5 (Size of types and terms) The term size of a raw term M, denoted |M|^{Term}, is the number of atomic subterms of M, defined by:

|x|^{Term}  = 1
|F: S|^{Term}  = 1
|c: S|^{Term}  = 1
|(M · N)|^{Term} = |M|^{Term} + |N|^{Term}
|λ x: S. M|^{Term} = |M|^{Term}

The type size of a type T, denoted |T |^{Type}, is the number of atomic types of T, defined by

|A|^{Type}  = 1
|s|^{Type}  = 1
|(S → T)|^{Type} = |S|^{Type} + |T |^{Type}

The type size of a raw term M, denoted |M|^{Type}, is the number of atomic types occurring in M, defined by:

|x|^{Type}  = 0
|F: T |^{Type}  = |T |^{Type}
|c: T |^{Type}  = |T |^{Type}
|(M · N)|^{Type} = |M|^{Type} + |N|^{Type}
|λ x: S. M|^{Type} = |S|^{Type} + |M|^{Type}
△

Definition 2.6 (Substitutions) A polymorphic substitution is a pair σ = ⟨σ_{1}, σ_{2}⟩ consisting of a mapping σ_{1} from type variables to types and a mapping σ_{2} from free variables to terms defined in the usual way. σ̂_{1} denotes the unique extension of σ_{1} to a mapping from types to types and σ̂_{2} denotes the unique extension of σ_{2} to a mapping from λ-terms to λ-terms. We usually write σ or ⟨σ_{1}, σ_{2}⟩ instead of ⟨σ̂_{1}, σ̂_{2}⟩. We write σ_{1}(M) for the result of applying the type substitution σ_{1} to all type variables occurring in the term M.

The identity substition ι is the pair consisting of the identity substitution ι_{1} on types and the identity substitution ι_{2} on terms.

The union of two polymorphic substitutions σ = ⟨σ_{1}, σ_{2}⟩ and τ = ⟨τ_{1}, τ_{2}⟩ is the substitution σ ∪ τ = ⟨σ_{1} ∪ τ_{1}, σ_{2} ∪ τ_{2}⟩ where the union of the type substitutions and the union of the term substitutions are defined in the usual way. For a set Z of type and free variables, we say that two substitutions σ and τ are equal over Z with respect to some congruence relation =_{E} on terms, denoted σ =_{E} τ [Z], iff for all type variables A ∈ Z, σ_{1}(A) = τ_{1}(A), and for all free variables (F: T) ∈ Z, σ_{2}(F: T) =_{E} τ_{2}(F: T).

We say that σ is more general than τ over Z, denoted σ ≤_{E} τ [Z], iff there exists a substitution θ such that θ ∘ σ =_{E} τ [Z].

The domain of a substitution σ is

DOM(σ) = {A ∈ V_{T} | σ_{1}(A) ≠ A} ∪ {F ∈ FV | σ_{2}(F) ≠ F }.

The set of variables introduced by σ is

I(σ) = ⋃_{F ∈DOM(σ)} FV(σ(F)).

A substitution σ is normalized if σ(F) = σ(F)↓_{β} for all F ∈ DOM(σ) ∩ FV.

A substitution σ is a renaming substitution away from Z if σ(F)↓_{η} ∈ FV ∪ V_{T} for all F ∈ DOM(σ), I(σ) ∩ Z = ∅ and σ is injective. If σ is a renaming substitution and τ is some arbitrary substitution then σ ∘ τ is called a variant of τ.

The restriction of a substitution σ to a set of variables Z, denoted σ_{Z}, is the substitution

σ_{Z}(F) = \begin{cases}σ(F), & if F ∈ Z \\ F, & otherwise. \end{cases}

△

3 Polymorphic Unification Problems

Definition 3.1 (Unification problems in L^{P oly}) An equation in L^{P oly} is a multiset of terms M and N in Lη^{P oly} such that all free variables in {M, N} are uniquely annotated. For equations we will use the notation M =^{?} N. A system S in L^{P oly} is a multiset of equations in L^{P oly} such that that all free variables in the set of all terms in S are uniquely annotated. A unification problem in L^{P oly} is an ordered pair ⟨σ, S⟩ with σ a type substitution and S a system such that DOM(σ) ∩ FV^{Type}(S) = ∅. △

For a system

S = {M_{1} =^{?} N_{1}, …, M_{n} =^{?} N_{n}}

we write S↓ instead of {η[M_{1}↓] =^{?} η[N_{1}↓], …, η[M_{n}↓] =^{?} η[N_{n}↓]}. S↓ is unique up to renaming of bound variables.

There are at least two views of the meaning of σ in a unification problem ⟨σ, S⟩.

1. The type substitution σ is a representation of some equations on types that have to be solved like any equation on terms in S. That means any type variable has to occur only once in ⟨σ, S⟩. So if A ∈ DOM(σ) and A ∈ FV^{Type}(S) we have to eliminate A in S by applying σ_{{A}} to S.

2. The type substitution σ memorizes the type instantiation that has to be done to get a unifier for S. So typically we start with ⟨ι_{1}, S⟩ and transform it into ⟨σ_{1}, S′⟩. The solved system S′ represents a term substitution σ_{2} and σ_{1} a type substiution. Then ⟨σ_{1}, σ_{2}⟩ is a unifier of S.

In this paper I choose the second view. Then the restriction DOM(σ) ∩ FV^{Type}(S) = ∅ on a pair ⟨σ, S⟩ ensures that we can memorize type instantiations on S. Now I will give definitions for the notions of unifier and solved system that I already used in this explanation.

Definition 3.2 (Unifier in L^{P oly}) A normalized substitution θ is called a unifier in L^{P oly} of two terms M and N from Lη^{P oly} iff θ(M) ⟷^{∗}_{βη} θ(N) holds. θ is a unifier of a system S in L^{P oly} iff it is a unifier for every equation in S and it is called a unifier of a unification problem ⟨σ, S⟩ iff it is a unifier of the system S and an instance of ⟨σ, ι_{2}⟩.

The set of all unifiers of a unification problem U is denoted SU(U). △

Definition 3.3 (Complete set of unifiers) Let U be a unification problem and Z a finite set of variables, called the set of protected variables. A set CSU(U)[Z] of normalized substitutions is a complete set of unifiers for U separated on FV(U) away from Z iff (1) CSU(U)[Z] ⊆ SU(U)

(2) ∀ ϕ ∈ SU_{E}(Γ): ∃ θ ∈ CSU(U)[Z]: θ ≤_{β} ϕ [FV(U)]

(3) ∀ θ ∈ CSU(U)[Z]: DOM(θ) ⊆ FV(U) and I(θ) ∩ (Z ∪ DOM(θ)) = ∅.

If Z is not significant we drop the notation [Z]. If CSU(U) consists of a single substitution we call this substitution a most general unifier. △

For any set of equations between types there exists at most one unifier up to variable renaming. If this unifier exists for a set of equations E, it will be denoted mgu(E).

Definition 3.4 (Idempotent Substitution) A substitution σ is idempotent if σ ∘ σ = σ. △

It is easy to show that if I(σ) ∩ DOM(σ) = ∅ holds, σ is idempotent.

Lemma 3.5 If θ ∈ CSU(U) for some unification problem U then θ is idempotent.

Proof: Follows directly from the last condition in the definition of a complete set of unifiers CSU(U).

Definition 3.6 (Solved Form) An equation M =^{?} N is in solved form in a unification problem ⟨σ, S⟩ if it is in the form η[F: T] =^{?} N for some variable F: T which occurs exactly once in U, and F: T and N have the same type. A system S is solved if all of its pairs are solved. A unification problem ⟨σ, S⟩ is solved if S is solved.

With a system S = {F_{1}: T_{1} =^{?} N_{1}, …, F_{n}: T_{n} =^{?} N_{n}} in solved form we associate a term substitution ⌈S⌉^{SUB} = {F_{1}: T_{1}/N_{1}, …, F_{n}: T_{n}/N_{n}}. This substitution is unique up to variable renaming. With a unification problem ⟨σ, S⟩ in solved form we associate a substitution ⌈U⌉^{SUB} = ⟨σ, ⌈S⌉^{SUB}⟩. △

4 Problems with Unification in L^{P oly}

As stated in Nipkow (1990) type variables cause new problems through the possibility of type instantiation. Assume we use the transformation system HT defined in Snyder and Gallier (1989). HT is correct and complete for higher-order unification in the simply typed λ-calculus. In the following example we consider a system of polymorphically typed λ-terms with HT . We examine the effect of type variables on the applicability of the projection rule of HT which is Projection

\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ D

⇓

\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ \{F/P \}(D)↓,

where

• D is a system,

• F is a free variable and a an arbitrary atom,

• P is a variant of a ith projection binding for 1 ≤ i ≤ m, appropriate to the term λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}), that is, P = λ \overline{y_{m}: S_{m}}. y_{i}(\overline{λ \overline{z_{p_{q}}: R_{p_{q}}}. H_{q}(\overline{y_{m}}, \overline{z_{p_{q}}})}), and

• head(M_{i}) = a, if head(M_{i}) is a constant.

Example 4.1 Let A be a type variable and t some base type, such that type(F) = (A → t) and type(G) = A for free variables F and G. We consider the unification problem U

⟨ι_{1}, {F (G) =^{?} a}⟩.

If we want to instantiate F with a projection binding the only possibility is to use the first projection binding because there’s only one argument G. For the first projection binding to be appropriate for F we must have range(G) = range(F). A complete set of type substitutions for A satisfying this equation is

Θ = {{A/(A_{1}, …, A_{m} → t)} | A_{1}, …, A_{m} type variables, m ≥ 0}.

For every substitution θ_{1}^{m} in this set the projection rule is applicable using the projection binding

θ_{2}^{m} = λ y: (A_{1}, …, A_{m} → t). y(H_{1}(y), …, H_{m}(y)),

where type(H_{i}) = ((A_{1}, …, A_{m} → t) → A_{i}).

After applying θ_{2}^{m} to θ_{1}^{m}(F) we get the unification problem

S_{m} = ⟨θ_{1}^{m}, {G(H_{1}(G), …, H_{m}(G)) =^{?} a}⟩.

For the transformed unification problem S_{m} the substitution

ω_{2}^{m} = \{G/λ \overline{x_{m}: A_{m}}. a\}

is a unifier. Depending on m we get an infinitary set of non-subsuming unifiers for the unification problem U. So if the transformation system for higher-order unification in L^{P oly} contains a projection rule like HT does, it will be infinitary branching even for preunification or it will be incomplete, if it only considers a finitary subset of Θ.

5 An Analysis of Polymorphic Unifiers

We analyse the process of polymorphical higher-order unification as follows. Without loss of generality we assume that M and N are two lambda terms in Lη^{P oly} and that θ is an idempotent normalized unifier of M and N. In other words M has the form

M = λ \overline{x_{k}: A_{k}}. a(M_{1}, …, M_{m})

where M has type A = (A_{1}, …, A_{k} → A_{0}) and a has type B = (B_{1}, …, B_{m} → A_{0}). N has the form

N = λ \overline{x_{l}: C_{l}}. b(N_{1}, …, N_{n}),

where N has type C = (C_{1}, …, C_{l} → C_{0}) and b has type D = (D_{1}, …, D_{n} → C_{0}). And there exists some sequence of reductions to a β-normal form η[θ(M)] ⟶^{∗}_{β} P ⟵^{∗}_{β} η[θ(N)]. We analyse this sequence topdown. We have the following cases (which are intended to be mutually exclusive):

(A) M = N and no unification is necessary. We assume M and N to be distinct in the remaining cases.

(B) Suppose k < l. Then θ instantiates the type of M such that a sequence of η-expansions enlarges the binder of M. This is only possible if A_{0} is a type variable. Thus

θ(A_{0}) = (θ(C_{k+1}), …, θ(C_{l}) → θ(C_{0}))
= θ((C + 1, …, C_{l} → C_{0}))
= θ({A_{0}/(C_{k+1}, …, C_{l} → C_{0})}(A_{0}))

and θ is an instance of the most general unifier of A_{0} and (C_{k+1}, …, C_{l} → C_{0}).

(C) Suppose k = l but A_{i} ≠ C_{i} for some i, 0 ≤ i ≤ k. Then we have

θ(A_{i}) = θ(C_{i})

and θ must be an instance of the most general unifier of A_{i} and C_{i}. In the remaining cases we assume M and N have the same type. This implies that the binders of M and N are identical up to α-conversion.

(D) Suppose head(M) = a: (B_{1}, …, B_{m} → A_{0}) and head(N) = a: (D_{1}, …, D_{m} → A_{0}) are atoms with distinct types. Then we have B_{i} ≠ D_{i} for some i, 1 ≤ i ≤ m. Then θ possibly unifies B_{i} and D_{i}, i.e.

θ(B_{i}) = θ(D_{i}).

So θ is an instance of the most general unifier of B_{i} and D_{i}. Note that B and D necessarily have the same number of argument types.

(E) No substitution takes place in the head of either term. In this case, head(M) = head(N). Suppose

M = λ \overline{x_{k}: A_{k}}. a(M_{1}, …, M_{m})

and

N = λ \overline{x_{k}: A_{k}}. a(N_{1}, …, N_{m}),

where either a ∈ Σ or a = x_{i} for some i, 1 ≤ i ≤ k, or a is a free variable not in DOM(θ). Here we must have

η[θ(λ \overline{x_{k}: A_{k}}. M_{i})] ⟶^{∗}_{β} λ \overline{x_{k}: A_{k}}. P_{i} ⟵^{∗}_{β} η[θ(λ \overline{x_{k}: A_{k}}. N_{i})]

for 1 ≤ i ≤ m. That is, the subterms of M and N are pair-wise unifiable by θ.

(F) The two terms are

M = λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}})

and

N = λ \overline{x_{k}: A_{k}}. b(N_{1}, …, N_{m})

for some free variable F c.f. F ∉ FV(N). In this case, we must have

η[θ(λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}}))] ⟷^{∗}_{β} λ \overline{x_{k}: A_{k}}. b(N_{1}, …, N_{m})

and we know that σ = \{F/λ \overline{x_{k}: A_{k}}. b(N_{1}, …, N_{m})\} is a most general unifier of this equation.

(G) Some substitution takes place in the head of only one term. Assume that this term is M. Then b is either a function constant, a bound variable, or a free variable not in DOM(θ). Now in order for the two terms to unify, we must ensure that at some point in the sequence of β-reductions from θ(M) to P the head of M becomes b. There are two possibilities: either we imitate the head of N by substituting a term for F whose head is b or we substitute a term for F which projects up a subterm of M. We consider each of these possibilities in turn.

(Imitation) The substitution for F matches the head symbol of N by imitating the head symbol b where b ∈ Σ or b is a free variable not in DOM(θ). In contrast to the simply typed case we need to take the type substitution θ_{1} into account. Suppose N is a rigid term of the form

N = λ \overline{x_{k}: A_{k}}. b: D(\overline{N_{m}})

and the application of θ_{1} to D yields

θ_{1}(D) = θ_{1}((D_{1}, …, D_{m} → A_{0})) = D′ = (D′_{1}, …, D′_{m}, A′_{k+1}, …, A′_{k+p} → A′_{0}).

Then we get the following reduction sequence

θ(N) = θ_{2}(λ \overline{x_{k}: A′_{k}}. b: D′(\overline{N′_{m}}))
= λ \overline{x_{k}: A′_{k}}. b: D′(\overline{θ_{2}(N′_{m})})
⟶^{∗}_{β} λ \overline{x_{k}: A′_{k}}. b: D′(\overline{P_{m}})
⟵^{∗}_{η} λ \overline{x_{k+p}: A′_{k+p}}. b: D′(\overline{P_{m}}, x_{k+1}, …, x_{k+p})

where N′_{i} is the result of applying θ_{1} to N_{i} and P_{i} is the η-expanded normal form of θ_{2}(N′_{i}) for all i, 1 ≤ i ≤ m. We can assume that M has the form

M = λ \overline{x_{k}: A_{k}}. F: B(\overline{M_{m}})

and the result of applying θ_{1} to the type of M and the type of the head of M will be

θ_{1}(type(M)) = θ_{1}((A_{1}, …, A_{k} → A_{0})) = A′ = (A′_{1}, …, A′_{k}, A′_{k+1}, …, A′_{k+p} → A′_{0}),

and

θ_{1}(B) = θ_{1}((B_{1}, …, B_{m} → A_{0})) = B′ = (B′_{1}, …, B′_{m}, A′_{k+1}, …, A′_{k+p} → A′_{0}).

Note that B must have the same number of argument types as D. The η-expanded normal form of θ_{1}(M) will be

λ \overline{x_{k+p}: A′_{k+p}}. F: B′(\overline{M′_{m}}, x_{k+1}, …, x_{k+p})

where M′_{i} is the η-expanded normal form of θ_{1}(M_{i}) for all i, 1 ≤ i ≤ m. Thus θ must take the form

θ(F: B′) = λ \overline{z_{m}: B′_{m}}, z_{m+1}: A′_{k+1}, …, z_{m+p}: A′_{k+p}. b: D′(\overline{Q_{m}}, z_{m+1}, …, z_{m+p})

for some terms \overline{Q_{m}} of appropriate types. Note that none of the z_{m+1},…,z_{m+p} occurs in one of the Q_{i}, since none of them occurs in one of the P_{i} = η[θ_{1}(N_{i})] for some i, 1 ≤ i ≤ m. This leaves us with a reduction sequence of the form

θ(M) = θ_{1}(λ \overline{x_{k+p}: A′_{k+p}}. F: B′(\overline{M′_{m}}, \overline{x_{k+1...k+p}}))
⟶_{β} λ \overline{x_{k+p}: A′_{k+p}}. b: D′(\overline{P_{m}}, \overline{x_{k+1...k+p}})
⟶^{∗}_{η} λ \overline{x_{k}: A′_{k}}. b: D′(\overline{P_{m}})
⟵^{∗}_{β} θ(λ \overline{x_{k}: A_{k}}. b: D(\overline{N_{n}})).

Note that

λ \overline{z_{m}: B′_{m}}, z_{m+1}: A′_{k+1}, …, z_{m+p}: A′_{k+p}. b: D′(\overline{Q_{m}}, z_{m+1}, …, z_{m+p})

is an type-instance of

λ \overline{z_{m}: B_{m}}. b: D(\overline{Q_{m}}).

(Projection) The substitution for F projects up a subterm of M. When substituting a ith projection for the head of a flexible term M = λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) we constrain the type of M_{i} as follows:

range(type(θ(M_{i}))) = range(θ_{1}(B_{i}))
= range(type(θ(F)))
= range(θ_{1}((B_{1}, …, B_{m} → A_{0})))
= range(θ_{1}(A_{0})).

Assume θ_{1}((B_{1}, …, B_{m} → A_{0})) = B′ = (B′_{1}, …, B′_{m}, B′_{m+1}, …, B′_{p} → E_{0}) for some types B′_{0}, …, B′_{p} and m ≤ p. The substitution for F takes the form \{F: B′/λ \overline{y_{p}: B′_{p}}. y_{i}(\overline{L_{q}})\} for some terms \overline{L_{q}} and some i in \{1, …, m\} such that type(y_{i}) = type(θ(M_{i})) = (E_{1}, …, E_{q} → E_{0}). We have a reduction sequence of the form

θ_{2}(η[θ_{1}(M)]) = θ_{2}(λ \overline{x′_{k+p−m}}. F: B′(M′_{1}, …, M′_{m}, x′_{k+1}, …, x′_{k+p−m}))
= λ \overline{x′_{k+p−m}}. λ \overline{y_{p}}. y_{i}(\overline{L_{q}})(s′_{1}, …, M′_{m}, x′_{k+1}, …, x′_{k+p−m})
⟶_{β} λ \overline{x′_{k+p−m}}. M′_{i}(\overline{L_{q}})
⟶^{∗}_{β} λ \overline{x′_{k+p−m}}. a′(\overline{P_{r}})
⟷^{∗}_{β} θ(N).

In this case, the head b of N may be a function constant, a free variable or a bound variable. Note that i ≤ m because b can not be equal to any of the x′_{k+1}, …, x′_{k+p−m}.

(H) Substitutions take place at the head of both terms. Then let M = λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) and N = λ \overline{x_{k}: A_{k}}. G(\overline{N_{n}}) for both F and G in DOM(θ). Here we must eventually match the heads of the two terms, but we can do it in a large number of ways. In order to simplify our analysis if possible, we reduce it to the previous case. Let us (without loss of generality) focus on the binding for the variable F. There are two subcases.

(1) θ substitutes a non-projection term for F, e.g., θ(F) = λ \overline{y_{p}}. a(\overline{r_{q}}), where a ≠ G is not a bound variable. By idempotency a is not a variable in DOM(θ). The substitution (possibly) causes a β-reduction, after which we can analyse the result using (G).

(2) θ substitutes a projection term for F (which obeys the typing constraints discussed above), e.g., θ(F) = λ \overline{y_{p}}. y_{j}(\overline{L_{q}}). For further analysis we use (G) if the head symbol is either a function constant, a bound variable, or a variable not in DOM(θ). We use (H) if the head is a variable in DOM(θ).

It is straightforward to formulate transformation rules for cases (A), (C), (D), (E), and (F). To formulate the transformation analysed in case (B), we need the notion of a binder expanding substitution:

Definition 5.1 (Binder expanding substitution) A type substition {A_{0}/(A_{1} → A_{2})} with type variables A_{0}, A_{1}, and A_{2} is called a binder expanding substitution for a term of type (B_{1}, …, B_{m} → A_{0}), where B_{1}, …, B_{m} are arbitrary types. △

The substitution {A_{0}/(C_{k+1}, …, C_{l} → C_{0})} in case (B) is an instance of the composition of l − (k + 1) binder expanding substitutions.

The transformations associated with cases (G) and (H) can be formulated using partial binding substitutions. I use the definition due to Snyder and Gallier (1989).

Definition 5.2 (Partial binding) A partial binding of type (A_{1}, …, A_{n} → B) (for B atomic) is the η-expanded form of a term of the form

λ \overline{y_{n}: A_{n}}. a(H_{1}(\overline{y_{n}}), …, H_{m}(\overline{y_{n}}))

for some atom a of type (C_{1}, …, C_{m} → B), where C_{i} = (D_{1}^{i}, …, D_{p_{i}}^{i} → C′_{i}) for 1 ≤ i ≤ m. The H_{i} have type (A_{1}, …, A_{n}, D_{1}^{i}, …, D_{p_{i}}^{i} → C′_{i}) for 1 ≤ i ≤ m. C′_{1}, …, C′_{m} are atomic types. The arguments of a partial binding will be called general flexible terms. △

We will now show that every partial binding can be constructed using matrix expanders and selectors.

Definition 5.3 (Matrix expander) A matrix expander of type (A_{1}, …, A_{m+n} → A) (where A is a base type) is a term of the form

λ \overline{y_{m+n}: A_{m+n}}. F (\overline{y_{m+n}}, G(\overline{y_{m}}))

with free variables F and G such that • type(F) = (A_{1}, …, A_{m+n}, B → A) and

• type(G) = (A_{1}, …, A_{m} → B). A substitution {H: D/M} with M a matrix expander of type D is called a matrix expanding substitution. △ Definition 5.4 (Selector) A selector appropriate to type (A_{1}, …, A_{m}, B_{1}, …, B_{n} → C) is a term of the form

λ \overline{y_{m}: A_{m}}, \overline{z_{n}: B_{n}}. a(\overline{z_{n}})

where a is some arbitrary atom of type (B_{1}, …, B_{n} → C). A substitution {H: D/M} with M a selector of type D is called a selector substitution. △ Lemma 5.5 For any partial binding substitution

τ = \{F/λ \overline{y_{m}: A_{m}}. a(λ \overline{z_{p_{1}}^{1}: B_{p_{1}}^{1}}. H_{1}(\overline{y_{m}}, \overline{z_{p_{1}}^{1}}), …, λ \overline{z_{p_{n}}^{n}: B_{p_{n}}^{n}}. H_{n}(\overline{y_{m}}, \overline{z_{p_{n}}^{n}}))\}

such that • F is free variable of type (A_{1}, …, A_{m} → A),

• a is some arbitrary atom of type (C_{1}, …, C_{n} → A) with C_{i} = (B_{1}^{i}, …, B_{p_{i}}^{i} → B^{i}) for 1 ≤ i ≤ n and B^{i} ∈ T_{0}, and

• type(H_{i}) = (A_{1}, …, A_{m}, B_{1}^{i}, …, B_{p_{i}}^{i} → B^{i}) for 1 ≤ i ≤ n, there exist matrix expanding substitutions τ_{1}, …, τ_{n} and a selector substitution τ_{0}, such that

τ = τ_{0} ∘ τ_{n} ∘ ⋯ ∘ τ_{1}.

Proof: Let

τ_{1} = \{F/λ \overline{y_{m}: A_{m}}. F_{1}(\overline{y_{m}}, λ \overline{z_{p_{1}}^{1}: B_{p_{1}}^{1}}. H_{1}(\overline{y_{m}}, \overline{z_{p_{1}}^{1}}))\}
type(F_{1}) = (A_{1}, …, A_{m}, (B_{1}^{1}, …, B_{p_{1}}^{1} → B^{1}) → A)
= (A_{1}, …, A_{m}, C_{1} → A)
type(H_{1}) = (A_{1}, …, A_{m}, B_{1}^{1}, …, B_{p_{1}}^{1} → B^{1})
τ_{2} = \{F_{1}/λ \overline{y_{m}: A_{m}}, x_{1}: C_{1}. F_{2}(\overline{y_{m}}, x_{1}, λ \overline{z_{p_{2}}^{2}: B_{p_{2}}^{2}}. H_{2}(\overline{y_{m}}, \overline{z^{2}}_{p_{2}}))\}
type(F_{2}) = (A_{1}, …, A_{m}, C_{1}, (B_{1}^{2}, …, B_{p_{2}}^{2} → B^{2}) → A)
= (A_{1}, …, A_{m}, C_{1}, C_{2} → A)
type(H_{2}) = (A_{1}, …, A_{m}, B_{1}^{2}, …, B_{p_{2}}^{2} → B^{2})
⋮
τ_{n} = \{F_{n−1}/λ \overline{y_{m}: A_{m}}, \overline{x_{n−1}: C_{n−1}}. F_{n}(\overline{y_{m}}, \overline{x_{n−1}}, λ \overline{z_{p_{n}}^{n}: B_{p_{n}}^{n}}. H_{n}(\overline{y_{m}}, \overline{z_{p_{n}}^{n}}))\}
type(F_{n−1}) = (A_{1}, …, A_{m}, C_{1}, …, C_{n−1} → A)
type(F_{n}) = (A_{1}, …, A_{m}, C_{1}, …, C_{n−1}, (B_{1}^{n}, …, B_{p_{n}}^{n} → B^{n}) → A)
type(H_{n}) = (A_{1}, …, A_{m}, B_{1}^{n}, …, B_{p_{n}}^{n} → B^{n})
τ_{0} = \{F_{n}/λ \overline{y_{m}: A_{m}}, \overline{x_{n}: C_{n}}. a(\overline{x_{n}})\}
type(a) = (A_{1}, …, A_{m} → A)

We have

τ_{0} ∘ τ_{n} ∘ ⋯ ∘ τ_{1} = \{F/λ \overline{y_{m}: A_{m}}. a(λ \overline{z_{p_{1}}^{1}: B_{p_{1}}^{1}}. H_{1}(\overline{y_{m}}, \overline{z_{p_{1}}^{1}}), …, λ \overline{z_{p_{n}}^{n}: B_{p_{n}}^{n}}. H_{n}(\overline{y_{m}}, \overline{z_{p_{n}}^{n}}))\}
= τ

6 The Transformation System HPT

We define the following transformation system on unification problems using the notions of binder expanding, matrix expanding and selector substitutions. Definition 6.1 (Transformation system HPT ) The rules for the transformation system HPT for unification problems in L^{P oly} are: Trivial removal

⟨σ, {M =^{?} M} ∪ S⟩ ⇒ ⟨σ, S⟩  HPT_{1}

Type unification

\begin{matrix}⟨σ, \{M =^{?} N\} ∪ S⟩ \\ ⇓ \\ ⟨θ ∘ σ, θ(\{M =^{?} N\} ∪ S)⟩ \end{matrix}  HPT_{2}

where • M is a term of type A and N is term of type C,

• A ≠ C, and

• θ = mgu({A =^{?} C}).

Head type unification

\begin{matrix}⟨σ, \{λ \overline{x_{k}: A_{k}}. a: B(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a: D(\overline{N_{m}})\} ∪ S⟩ \\ ⇓ \\ ⟨θ ∘ σ, θ(\{λ \overline{x_{k}: A_{k}}. a: B(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a: D(\overline{N_{m}})\} ∪ S)⟩ \end{matrix}  HPT_{3}

where • B ≠ D,

• θ = mgu({B =^{?} D}).

Decomposition

\begin{matrix}⟨σ, \{λ \overline{x_{k}: A_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a(\overline{N_{m}})\} ∪ S⟩ \\ ⇓ \\ ⟨σ, ⋃_{1≤i≤m} \{λ \overline{x_{k}: A_{k}}. M_{i} =^{?} λ \overline{x_{k}: A_{k}}. N_{i}\} ∪ S⟩ \end{matrix}  HPT_{4}

where a is some arbitrary atom. Variable elimination

\begin{matrix}⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}}) =^{?} N\} ∪ S⟩ \\ ⇓ \\ ⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}}) =^{?} N\} ∪ \{F/N\}(S)⟩ \end{matrix}  HPT_{5}

where • F is a free variable,

• F ∈ FV(S) and F ∉ FV(N), and

• type(F) = type(N). Binder-Expansion

\begin{matrix}⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. b(\overline{N_{n}})\} ∪ S⟩ \\ ⇓ \\ ⟨θ ∘ σ, η[θ(\{λ \overline{x_{k}: M_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: M_{k}}. b(\overline{N_{n}}) ∪ S\})]⟩, \end{matrix}  HPT_{6a}

where • F is a free variable of type (B_{1}, …, B_{m} → A_{0}),

• A_{0} is a type variable, and

• θ = {A_{0}/(C_{1} → C_{2})} for type variables C_{1} and C_{2}. Matrix-Expansion

\begin{matrix}⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. b(\overline{N_{n}})\} ∪ S⟩ \\ ⇓ \\ ⟨σ, \{F =^{?} Q\} ∪ \{F/Q\}(\{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. b(\overline{N_{n}})\} ∪ S)↓⟩, \end{matrix}  HPT_{6b}

where • F is a free variable of type (B_{1}, …, B_{m} → A_{0});

• b is an arbitrary atom of type type(a) = (D_{1}, …, D_{n} → A_{0});

• Q is a variant of a matrix expander of type (B_{1}, …, B_{m} → A_{0}), i.e. M = λ \overline{y_{m}: B_{m}}. G(\overline{y_{m}}, H(\overline{y_{l}})) with

l ≤ m. Selection

\begin{matrix}⟨σ, \{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. b(\overline{N_{n}})\} ∪ S⟩ \\ ⇓ \\ ⟨θ ∘ σ, \{θ(F) =^{?} Q\} ∪ \{θ(F)/Q\}(θ(\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. b(\overline{N_{n}})\} ∪ S))↓⟩, \end{matrix}  HPT_{7}

where • F is a free variable of type (\overline{B_{m}} → A_{0});

• b is some arbitrary atom of type (\overline{D_{n}} → D_{0});

• a is some arbitrary atom of type (E_{1}, …, E_{k} → E_{0}), for some k and some l, k ≤ m − l, 0 ≤ l ≤ m, such that (B_{l+1}, …, B_{m} → A_{0}) and type(a) have a most general unifier θ;

• Q is a variant of a selector appropriate for type θ((B_{1}, …, B_{m} → A_{0})), i.e.

Q = η[θ(λ \overline{y_{m}: B_{m}}. a(y_{l+1}, …, y_{m}))],

such that l ≤ m.

△

7 Correctness and Completeness of HPT

7.1 Correctness of HPT

Lemma 7.1 Let τ be an idempotent type substitution and M, N two terms. If θ is an instance of τ then θ is a unifier of τ(M) =^{?} τ(N) iff θ is a unifier of M =^{?} N.

Proof: Because θ is an instance of τ there exists a substitution ρ such that θ = ρ ∘ τ. So we have

θ(τ(M)) = θ(τ(N))

iff ρ(τ(τ(M))) = ρ(τ(τ(N)))
iff ρ(τ(M)) = ρ(τ(N))
iff θ(M) = θ(N).

Lemma 7.2 If U ⟹_{HPT} U′ using one of the transformation rules HPT_{1}, HPT_{2}, or HPT_{5}, then U(U) = U(U′).

Proof: We consider each of the transformation rules in turn:

HPT_{1} If θ is a unifier for a unification problem ⟨σ, S⟩ then θ is also a unifier of ⟨σ, M =^{?} M ∪ S⟩. The

converse holds because θ(M) = θ(M) holds for any substitution θ. HPT_{2} Suppose τ is a unifier of ⟨σ, M =^{?} N ∪ S⟩. Then τ_{1} unifies the types of M and N and because there

exists a most general unifier θ of type(M) and type(N), τ_{1} must be an instance of θ. So a variant of τ is also a unifier of ⟨θ ∘ σ, θ(M =^{?} N ∪ S)⟩. Suppose on the other hand τ is a unifier of ⟨θ ∘ σ, θ(M =^{?} N ∪ S)⟩. Then τ must be an instance of θ and therefore a variant of τ is a unifier of ⟨σ, M =^{?} N ∪ S⟩.

HPT_{5} Let ρ be the substitution {F/N}. For any substitution τ if τ(F) ⟷^{∗}_{βη} τ(N) then τ =_{βη} τ ∘ ρ, since τ ∘ ρ differs from τ only at F but τ(F) ⟷^{∗}_{βη} τ(N) = τ ∘ ρ(F). We have τ ∈ U(U) iff τ ∘ ρ ∈ U(U). Furthermore, since for any term P we have τ ∘ ρ(P) = τ(ρ(u)) ⟶^{∗}_{β} τ(ρ(P)↓), it can easily be shown that τ ∘ ρ ∈ U(U) iff τ ∈ U(ρ(U)↓). Thus

τ ∈ U({F =^{?} N} ∪ S)

iff τ(F) ⟷^{∗}_{βη} τ(N) and τ ∈ U(N)
iff τ(F) ⟷^{∗}_{βη} τ(N) and τ ∘ ρ ∈ U(U)
iff τ(F) ⟷^{∗}_{βη} τ(N) and τ ∈ U(ρ(U)↓)
iff τ ∈ U({F =^{?} N} ∪ ρ(U)↓).

Lemma 7.3 Let U ⟹_{HPT_{3}} U′ where the transformed equation in U is

λ \overline{x_{k}: A_{k}}. a: B(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a: D(\overline{N_{m}}).

Let θ be any substitution. Then

(1) θ ∈ U(U′) iff θ ∈ U(U) if a is either a constant or a free variable not in DOM(θ).

(2) θ ∈ U(U′) implies θ ∈ U(U) if a ∈ DOM(θ).

Proof: Let U′ = ⟨τ ∘ σ, D′⟩ and U = ⟨σ, D⟩. Let θ be a unifier of U′. Then θ is an instance of τ ∘ σ where τ is an idempotent substitution. So following lemma 7.1 θ is a unifier of every equation in D. And because DOM(σ) ∩ DOM(τ) = ∅ the substitution θ is an instance of σ. So θ is a unifier of the unification problem U.

Now let θ be a unifier of U. Suppose a is either a constant or a free variable not in DOM(θ). Then θ(a: B) = a: θ_{1}(B) = a: θ_{1}(D) = θ(a: D). So θ is an instance of the most general unifier τ of B and D. Using lemma 7.1 we can conclude that θ must be a unifier of U′.

Lemma 7.4 Let U ⟹_{HPT_{4}} U′ where the transformed equation in U is λ \overline{x_{k}: A_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a(\overline{N_{m}}). Let θ be any substitution. Then

(1) θ ∈ U(U′) iff θ ∈ U(U) if a is either a constant or a bound variable or a free variable not in DOM(θ).

(2) θ ∈ U(U′) implies θ ∈ U(U) if a ∈ DOM(θ).

Proof: If ρ(λ \overline{x_{k}: A_{k}}. M_{i}) ⟷^{∗}_{β} ρ(λ \overline{x_{k}: A_{k}}. N_{i}) for 1 ≤ i ≤ m, then clearly we have ρ(λ \overline{x_{k}}. a(\overline{M_{m}})) = ρ(λ \overline{x_{k}}. a(\overline{N_{m}})). So for any atom a we have ρ ∈ U(U) whenever ρ ∈ U(U′). If a is either a function constant, a bound variable or a variable not in DOM(ρ), then ρ(a) = a. It is easy to see that the converse direction holds as well.

Lemma 7.5 If U ⟹_{HPT} U′ using one of the transformation rules HPT_{3} or HPT_{4} then U(U′) ⊆ U(U).

Proof: This is a consequence of lemma 7.3 and 7.4.

Lemma 7.6 If U ⟹_{HPT} U′ using transformation rule HPT_{6a} then U(U′) ⊆ U(U).

Proof: In this case U′ = θ(U) where θ is an idempotent type substitution. So we can use lemma 7.1 to prove U(U′) ⊆ U(U).

Lemma 7.7 If U ⟹_{HPT} U′ using transformations HPT_{6b} or HPT_{7} then U(U′) ⊆ U(U).

Proof: These transformations add a pair {F =^{?} Q} to the system S of the unification problem U = ⟨σ, S⟩ and then apply the substitution {F/Q} to S. Since S ⊆ {F =^{?} Q} ∪ S we have U({F =^{?} Q} ∪ S) ⊆ U(S). The application of the substitution can be seen as an application of HPT_{5} which has been shown to be sound in lemma 7.2.

Theorem 7.8 (Soundness) If U ⟹^{∗}_{HPT} U′, with U′ in solved form, then the substitution ⌈U′⌉^{SUB}_{FV_{(U)}} ∈ U(U).

Proof: By induction on the length of transformation sequences, and using the previous lemmas in the induction step, we can show that ⌈U′⌉^{SUB} ∈ U(U). Since the restriction to the free variables of U does not change the effect of the substitution on the terms in U, we see that ⌈U′⌉^{SUB}_{FV_{(U)}} ∈ U(U).

7.2 Completeness of HPT

In this section we will give a completeness proof for the transformation system HPT .

Lemma 7.9 Let U be any unification problem, ϕ any substitution, and Z any set of protected variables. Then, provided ϕ ∈ SU(U), there exists some normalized substitution θ such that

(1) θ ∈ SU(U);

(2) θ ≤_{βη} ϕ [FV(U)] and ϕ ≤_{βη} θ [FV(U)];

(3) DOM(θ) ⊆ FV(U) and I(θ) ∩ (Z ∪ DOM(θ)) = ∅.

Proof: Suppose ϕ_{FV_{(U)}} is normalized and satisfies condition (3). Then θ = ϕ_{FV_{(U)}} is the substitution we are looking for.

Otherwise, we assume that I(ϕ) ∩ FV = {F_{1}, …, F_{n}} holds. We can choose a set of free variables {G_{1}, …, G_{n}} such that type(G_{i}) = type(F_{i}) for all i, 1 ≤ i ≤ n, holds and the intersection with Z ∪ I(ϕ) ∪ FV(U) is empty. Also we can assume that I(ϕ) ∩ V_{T} = {A_{1}, …, A_{m}} holds. We can choose a set of type variables {B_{1}, …, B_{m}} such that the intersection with Z ∪ I(ϕ) ∪ FV(U) is empty. Let

ζ_{1} = {A_{1}/B_{1}, …, A_{m}/B_{m}}
ρ_{1} = ⟨ζ_{1}, {ζ_{1}(F_{1})/η[ζ_{1}(G_{1})], …, ζ_{1}(F_{n})/η[ζ_{1}(G_{n})]}⟩
ζ_{2} = {B_{1}/A_{1}, …, B_{m}/A_{m}}
ρ_{2} = ⟨ζ_{2}, {G_{1}/η[F_{1}], …, G_{n}/η[F_{n}]}⟩
θ′ = (ρ_{1} ∘ ϕ)_{FV (S)}
θ = θ′↓_{βη}

We will show now that the substitution θ satisfies conditions (1)-(3).

(1): For every M =^{?} N ∈ S we have ϕ(M)↓ = ϕ(N)↓ and for every term P we have θ′(P) ⟷^{∗}_{βη} θ(P).

Therefore

θ(M) ⟷^{∗}_{βη} θ′(M)
= ρ_{1}(ϕ(M))
⟶^{∗}_{βη} ρ_{1}(ϕ(M)↓) = ρ_{1}(ϕ(N)↓)
⟵^{∗}_{βη} ρ_{1}(ϕ(N))
= θ′(N)
⟷^{∗}_{βη} θ(N)

Thus θ is an element of SU(U).

(2): Because

θ =_{βη} ρ_{1} ∘ ϕ [FV(U)]

we must have

ϕ ≤_{βη} θ [FV(U)].

Since ρ_{2} ∘ ρ_{1} =_{βη} ι [FV(S) ∪ I(ϕ)] holds, we have

ϕ =_{βη} ρ_{2} ∘ ρ_{1} ∘ ϕ [FV(U) ∪ I(ϕ)].

Using θ =_{βη} ρ_{1} ∘ ϕ [FV(U)] we get

ϕ =_{βη} ρ_{2} ∘ θ [FV(U)], and

therefore

θ ≤_{βη} ϕ [FV(U)].

(3): is implied by the construction of θ.

Lemma 7.10 Let U = ⟨σ, {F_{1} =^{?} M_{1}, …, F_{n} =^{?} M_{n}}⟩ be a unification problem in solved form. Then the set {⌈U⌉^{SUB}} is a CSU(U)[Z] for any finite set Z such that Z ∩ FV(U) = ∅.

Proof: We have to show that {⌈S⌉^{SUB}} satisfies (1)-(3) of definition 3.3.

(1): Trivially, {⌈U⌉^{SUB}} ⊆ SU(U). (2): We must prove that for every normalized substitution θ ∈ SU(U) there exists a substitution in σ ∈

{⌈U⌉^{SUB}} such that σ ≤_{β} θ [FV(U)] holds.

If θ ∈ SU(U) then θ =_{β} θ ∘ ⌈U⌉^{SUB} because

θ(F_{i}) ⟷^{∗}_{β} θ(M_{i}) = θ(⌈U⌉^{SUB}(F_{i}))

for every i, 1 ≤ i ≤ n, and

θ(F_{i}) = θ(⌈U⌉^{SUB}(F_{i})),

otherwise. For any type variable A we have

θ(A) = ρ(σ(A))

for some type substitution ρ because θ is an instance of σ. Therefore ⌈U⌉^{SUB} ≤_{β} θ and ⌈U⌉^{SUB} ≤_{β} θ [FV(U)].

(3): We have to show that DOM(ϕ) ⊆ FV(U), and I(ϕ) ∩ (Z ∪ DOM(ϕ)) = ∅ for all ϕ ∈ {⌈U⌉^{SUB}}. This is satisfied because DOM(⌈U⌉^{SUB}) = FV(U) and ⌈U⌉^{SUB} is idempotent.

Lemma 7.11 If M = λ \overline{x_{n}: A_{n}}. a(\overline{s_{m}}) is any term of type (\overline{A_{n}} → A_{0}) then there exists a variant of a partial binding P and a substitution ρ such that ρ(P) ⟶^{∗}_{β} M.

Proof: We distinguish the two cases m = 0 and m > 0.

m = 0: M has the form λ \overline{x_{n}: A_{n}}. a. According to the definition of partial bindings M is itself one. So choose

P = M and ρ = ι. m > 0: Let

P = η[λ \overline{x_{n}: A_{n}}. a(\overline{H_{m}(\overline{x_{n}})})]

be a partial binding appropriate for type (A_{1}, …, A_{n} → A_{0}). ρ is the substitution

⟨ι_{1}, \{H_{1}/λ \overline{x_{n}: A_{n}}. M_{1}, …, H_{m}/λ \overline{x_{n}: A_{n}}. M_{m}\}⟩.

Then

ρ(P) = λ \overline{x_{n}: A_{n}}. a(\overline{(λ \overline{x_{n}: A_{n}}. M_{m})(\overline{x_{n}})}) ⟶^{+}_{β} λ \overline{x_{n}: A_{n}}. a(M_{1}, …, M_{m})

as required.

So the term P and the substitution ρ have the desired properties.

Lemma 7.12 If θ = {F/M} ∪ θ′ then there exists a variant of a partial binding P appropriate to F and a substitution ρ such that

θ = {F/M} ∪ ρ ∪ θ′ [DOM(θ)]
=_{β} ρ ∘ {F/P } ∪ θ′ [DOM(θ)].

Furthermore, if DOM(θ) ∩ I(θ) = ∅ then θ′′ = {F/M} ∪ ρ ∪ θ′ is a unifier of the equation F =^{?} P and DOM(θ′′) ∩ I(θ′′) = ∅.

Proof: Define P and ρ according to lemma 7.11. Therefore DOM(ρ) ∩ DOM(θ) = ∅ and ρ(P) ⟶^{∗}_{β} M. Thus

{F/M} = {F/M} ∪ ρ =_{β} ρ ∘ {F/P } [DOM(θ)].

Assume DOM(θ) ∩ I(θ) = ∅. Because P is a variant we also have DOM(ρ) ∩ I(θ) = ∅ which implies (DOM(θ) ∪ DOM(ρ)) ∩ I(θ) = ∅.

Because DOM(θ) ∪ DOM(ρ) = DOM(θ′′) and I(θ) = I(θ′′) we have DOM(θ′′) ∩ I(θ′′) = ∅.

Finally, we show that θ′′ is a unifier of F and P:

θ′′(P) = ({F/M} ∪ ρ ∪ θ′)(P) = ρ(P) ⟶^{∗}_{β} M = ({F/M} ∪ ρ ∪ θ′)(F) = θ′′(F).

Note that a can be a variable. If DOM(θ) ∩ I(θ) ≠ ∅ then θ = {F/M, a/N} ∪ θ′ is possible. But in this case we have θ′′(t) = ({F/M} ∪ ρ ∪ {a/N} ∪ θ′)(P) ≠ ρ(P). Therefore the condition DOM(θ) ∩ I(θ) = ∅ is necessary.

These lemmas show that using partial bindings we can build arbitrary terms in an incremental way.

We define a transformation system CPT in which the applications of the transformation rules is controlled by a substitution θ. It is the goal of the transformations to get from the original unification problem U to a unification problem U′ in solved form such that ⌈U′⌉^{SUB} ≤_{β} θ holds.

Definition 7.13 (Transformation system CPT ) With the following rules we define a transformation system on ordered pairs of normalized substitutions and unification problems. Trivial removal

⟨Θ, ⟨σ, {M =^{?} M} ∪ S⟩⟩ ⟹ ⟨Θ, ⟨σ, S⟩⟩  CPT_{1}

Term type unification

\begin{matrix}⟨Θ, ⟨σ, \{M =^{?} N\} ∪ S⟩⟩ \\ ⇓ \\ ⟨Θ, ⟨θ ∘ σ, θ(\{M =^{?} N\} ∪ S)⟩⟩ \end{matrix}  CPT_{2}

where

• M is a term of type B and N is term of type D,

• B ≠ D, and

• θ = mgu({B =^{?} D}).

Head type unification

\begin{matrix}⟨Θ, ⟨σ, \{λ \overline{x_{k}: A_{k}}. a: B(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a: D(\overline{N_{m}})\} ∪ S⟩⟩ \\ ⇓ \\ ⟨Θ, ⟨θ ∘ σ, θ(\{λ \overline{x_{k}: A_{k}}. a: B(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a: D(\overline{N_{m}})\} ∪ S)⟩⟩ \end{matrix}  CPT_{3}

where • B ≠ D,

• Θ_{1}(B) = Θ_{1}(D), and

• θ = mgu({B =^{?} D}).

Decomposition

\begin{matrix}⟨Θ, ⟨σ, \{λ \overline{x_{k}: A_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. a(\overline{N_{m}})\} ∪ S⟩⟩ \\ ⇓ \\ ⟨Θ, ⟨σ, ∪_{1≤i≤m}\{λ \overline{x_{k}: A_{k}}. M_{i} =^{?} λ \overline{x_{k}: A_{k}}. N_{i}\} ∪ S⟩⟩, \end{matrix}  CPT_{4}

where a is some arbitrary atom. Variable elimination

\begin{matrix}⟨Θ, ⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}}) =^{?} N\} ∪ S⟩⟩ \\ ⇓ \\ ⟨Θ, ⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{x_{k}}) =^{?} N\} ∪ \{F/N\}(S)↓⟩⟩, \end{matrix}  CPT_{5}

where • F is a free variable,

• F ∉ FV(N) and F ∈ FV(S),

• type(F) = type(N), and

• F and head(N) are not in DOM(Θ). Partial binding

\begin{matrix}⟨\{F/Q\} ∪ Φ, ⟨σ, \{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. N\} ∪ S⟩⟩ \\ ⇓ \\ ⟨\{F/Q\} ∪ ρ ∪ Φ, ⟨τ ∘ σ, \{F =^{?} P , η[\{F/P \}(τ(λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. N) ∪ S)]\}⟩⟩ \end{matrix}  CPT_{6}

where • F is a free variable of type (\overline{B_{m}} → B_{0}) which is not solved in \{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. N\} ∪ S,

• Q = λ \overline{y_{l}: B′_{l}}. a: D(\overline{Q_{p}}) with some terms Q_{1}, …, Q_{p} and Φ(\overline{B_{m}} → B_{0}) = (\overline{B′_{l}} → B′_{0}) where a is some atom of type D = (\overline{D_{p}} → B′_{0}),

• τ = mgu({B_{0} =^{?} (B_{m+1}, …, B_{l} → C_{0})}) for some type variables B_{m+1}, …, B_{l}, and C_{0},

• P = η[τ(λ \overline{y_{l}: B_{l}}. a: C(\overline{H_{p}: (\overline{B_{l}} → C_{i})(\overline{y_{l}})}))] is a partial binding appropriate for F with the same head a as Q of type C = (\overline{C_{p}} → C_{0}) and free variables H_{i}: (\overline{B_{l}} → C_{i}) for all i, 1 ≤ i ≤ p, and

• ρ = ⟨mgu(⋃_{1≤i≤p} \{τ(\overline{B_{l}} → C_{i}) =^{?} D_{i}\}), \{H_{1}: D_{1}/λ \overline{y_{l}: B′_{l}}. Q_{1}, …, H_{p}: D_{p}/λ \overline{y_{l}: B′_{l}}. Q_{p}\}⟩.

△

Lemma 7.14 If Θ_{1} ∈ SU(U_{1}) for some unification problem ⟨σ_{1}, S_{1}⟩ and

⟨Θ_{1}, ⟨σ_{1}, S_{1}⟩⟩ ⟹_{CPT} ⟨Θ_{2}, ⟨σ_{2}, S_{2}⟩⟩

then there exists a corresponding sequence of HPT -transformations

⟨σ_{1}, S_{1}⟩ ⟹^{+}_{HPT} ⟨σ_{2}, S_{2}⟩.

Proof: The only problematic transformation rule is CPT_{6}. Suppose F is a free variable of type (\overline{B_{m}} → B_{0}) and the partial binding substitution is ⟨τ, {τ(F)/P }⟩ with

τ = mgu({B_{0} =^{?} (B_{m+1}, …, B_{l} → C_{0})})

and

P = η[τ(λ \overline{y_{l}: B_{l}}. a: C(\overline{H_{p}(\overline{y_{l}})}))].

We define the substitutions θ_{1}, …, θ_{l−m}, γ_{1}, …, γ_{p} and δ in the following way:

θ_{1} = {B_{0}/(B_{m+1} → F_{1})}
θ_{2} = {F_{1}/(B_{m+2} → F_{2})}
⋮
θ_{l−m} = {F_{l−(m+1)}/(B_{l} → C_{0})}
γ_{1} = \{θ_{l−m} ∘ … ∘ θ_{1}(F)/λ \overline{y_{l}: B_{l}}. G_{1}(\overline{y_{l}}, H_{1}(\overline{y_{l}}))\}
γ_{2} = \{G_{1}/λ \overline{y_{l}: B′_{l}}, z_{1}: C_{1}. G_{2}(\overline{y_{l}}, z_{1}, H_{2}(\overline{y_{l}}))\}
⋮
γ_{p} = \{G_{p−1}/λ \overline{y_{l}: B_{l}}, \overline{z_{p}: C_{p}}. G_{p}(\overline{y_{l}}, H_{p}(\overline{y_{l}}))\}
δ = \{G_{p}/λ \overline{y_{l}: B_{l}}, \overline{z_{p}: C_{p}}. a: C(\overline{z_{p}})\}.

It is easy to see that θ_{l−m}∘⋯∘θ_{1} = τ [FV^{Type}({B_{0}, B_{m+1}, …, B_{l}, C_{0}})] and δ∘γ_{m}∘⋯∘γ_{1} = {τ(F)/P } [{F }]. Now define the systems S_{1}, …, S_{l−m+p+3} as follows:

S_{1} = \{λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: A_{k}}. N\} ∪ S
S_{2} = η[θ_{1}(S_{1})]
S_{3} = η[θ_{2}(S_{2})]
⋮
S_{l−m+1} = η[θ_{l−m}(S_{l−m})]
S_{l−m+2} = {η[F] =^{?} γ_{1}(η[F])} ∪ γ_{1}(S_{m−l+1})↓
S_{l−m+3} = {G_{1} =^{?} γ_{2}(G_{1})} ∪ γ_{2}(S_{m−l+2})↓
⋮
S_{l−m+p+2} = {G_{p−1} =^{?} γ_{p}(G_{p−1})} ∪ γ_{p}(S_{l−m+p+1})↓
S_{l−m+p+3} = {G_{p} =^{?} δ(G_{p})} ∪ δ(S_{l−m+p+2})↓.

Then we get following transformation sequence:

⟨σ_{1}, S_{1}⟩ ⟹_{HPT_{6a}} ⟨θ_{1} ∘ σ_{1}, S_{2}⟩
⟹_{HPT_{6a}} ⟨θ_{2} ∘ θ_{1} ∘ σ_{1}, S_{3}⟩
⋮
⟹_{HPT_{6a}} ⟨θ_{l−m−1} ∘ ⋯ ∘ θ_{1} ∘ σ_{1}, S_{l−m}⟩
⟹_{HPT_{6a}} ⟨τ ∘ σ_{1}, S_{l−m+1}⟩
⟹_{HPT_{6b}} ⟨τ ∘ σ_{1}, S_{l−m+2}⟩
⟹_{HPT_{6b}} ⟨τ ∘ σ_{1}, S_{l−m+3}⟩
⋮
⟹_{HPT_{6b}} ⟨τ ∘ σ_{1}, S_{l−m+p+1}⟩
⟹_{HPT_{6b}} ⟨τ ∘ σ_{1}, S_{l−m+p+2}⟩
⟹_{HPT_{7}} ⟨τ ∘ σ_{1}, S_{l−m+p+3}⟩

and ⟨τ ∘ σ_{1}, S_{l−m+p+3}⟩ = ⟨σ_{2}, S_{2}⟩ holds. Lemma 7.15 If Θ ∈ SU(⟨σ, S⟩) for some unification problem U = ⟨σ, S⟩ not in solved form then there exists a transformation

⟨Θ, ⟨σ, S⟩⟩ ⟹_{CPT} ⟨Θ′, ⟨σ′, S′⟩⟩,

such that

(1) Θ = Θ′ [W] with W a set of variables,

(2) If DOM(Θ) ∩ I(Θ) = ∅, then Θ′ ∈ SU(S′) and DOM(Θ′) ∩ I(Θ′) = ∅, and

(3) ⟨σ, S⟩ ⟹^{+}_{HPT} ⟨σ′, S′⟩.

Proof: Because U is not in solved form there is a pair M =^{?} N which is not solved in U. We distinguish the following cases:

1. M = N. Then we may apply the transformation rules CPT_{1} or CPT_{4}.

2. type(M) ≠ type(N). Then we can apply CPT_{2}. In the remaining cases we may assume type(M) = type(N).

3. head(M) = a: B and head(N) = a: D for some arbitrary atoms a: B and a: D such that B ≠ D. We can apply CPT_{3}.

4. head(M) = head(N) ∉ DOM(Θ). Then we can apply CPT_{4}.

5. M ≠ N, head(M) = a: B, head(N) = b: D, and one of the following two cases applies.

(a) Θ_{1}(head(M)) ≠ Θ_{1}(head(N)): Because there exists a unifier of S, not both M and N can be rigid. We can assume that M is a flexible term.

(b) Θ_{1}(head(M)) = Θ_{1}(head(N)) ∈ DOM(Θ): One of the terms is flexible too. Let’s assume that M is flexible.

Therefore

M = λ \overline{x_{k}: A_{k}}. F (\overline{M_{m}})

and

N = λ \overline{x_{k}: A_{k}}. N′.

Then we can apply CPT_{6} or if M ⟶^{∗}_{η} F CPT_{5} is applicable too if it’s application constraints are fulfilled.

Thus there exists a transformation

⟨Θ, ⟨σ, S⟩⟩ ⟹^{+}_{CPT} ⟨Θ′, ⟨σ′, S′⟩⟩.

If we apply one of the transformation rules CPT_{1}, …, CPT_{5}, the conditions hold because

(1) Θ = Θ′,

(2) of the correctness lemma.

(3) of the definition of CPT . If we apply the transformation rule CPT_{6}, we can assume that

Θ = {F/Q} ∪ Φ

and

Θ′ = {F/Q} ∪ ρ ∪ Φ =_{β} ρ ∘ {F/P } ∪ Φ
S′ = {F =^{?} P } ∪ {F/P }(τ(S))
σ′ = τ ∘ σ

holds for partial binding P and substitutions ρ and τ, as given in the definition of CPT_{6}.

Therefore the conditions are satisfied

(1) because of the construction of Θ′ and lemma 7.12.

(2) If we assume DOM(θ′) ∩ I(θ′) = ∅ then following lemma 7.12

DOM(Θ′) ∩ I(Θ′) = ∅

and

Θ′(P) = ρ(q) ⟶^{∗}_{β} Q = Θ′(F)

holds.

(3) because of lemma 7.14.

Corollary 7.16 If θ ∈ SU(U) and no transformation rule in CPT is applicable to ⟨θ, U⟩, then U is in solved form.

Theorem 7.17 (Completeness of HPT ) Let U be a unification problem. If Θ ∈ SU(U), then there exists a sequence of transformations

U = U_{0} ⟹_{HPT} U_{1} ⟹_{HPT} U_{2} ⟹_{HPT} ⋯ ⟹_{HPT} U_{n},

where U_{n} is in solved form and ⌈U_{n}⌉^{SUB} ≤_{β} Θ [FV(U)].

Proof: DOM(Θ) ∩ I(Θ) = ∅ because of lemma 7.9. We define a complexity measure μ(⟨⟨Θ_{1}, Θ_{2}⟩, ⟨σ, S⟩⟩) = ⟨l, m, n⟩ by

l = ∑_{x∈DOM(Θ_{2})\Solved(S)} |Θ_{2}(x)|^{Term}
m = ∑_{(M=^{?}N)∈S} |M|^{Term} + |N|^{Term}
n = ∑_{x∈DOM(Θ_{1})} |Θ_{1}(x)|^{Type} − |σ(x)|^{Type}.

Using lexicographic combination of the <-ordering on natural number on every component we get a notherian ordering < on this measure. For every CPT -transformation U ⟹_{CPT} U′ we get μ(U′) < μ(U): CPT_{1} reduces m without changing l. CPT_{2} reduces n without changing l and m. Since θ ≠ ι and |σ(x)|^{Type} ≤ |θ ∘ σ(x)|^{Type} ≤ |Θ_{1}(x)|^{Type} for all

x ∈ DOM(Θ_{1}). CPT_{3} reduces n without changing l and m for the same reason as for CPT_{2}. CPT_{4} reduces m without changing l. CPT_{5} reduces l, because a variable out of DOM(Θ) \ Solved(U) is erased. CPT_{6} reduces l: The binding

\{F/λ \overline{y_{l}: B′_{l}}. a: D(\overline{Q_{p}})\}

does not increase l because F is solved in U′, Rather

⟨mgu( ⋃_{1≤i≤p} \{τ(\overline{B_{l}} → C_{i}) =^{?} D_{i}\}), \{H_{1}: D_{1}/λ \overline{y_{l}: B′_{l}}. Q_{1}, …, H_{p}: D_{p}/λ \overline{y_{l}: B′_{l}}. Q_{p}\}⟩.

is inserted and a is removed. In all l has decreased. Hence every sequence of CPT -transformations is finite. Therefore there exists a sequence

⟨Θ, U⟩ = ⟨Θ_{0}, U_{0}⟩ ⟹^{+}_{CPT} ⟨Θ_{k}, U_{k}⟩,

such that no further transformations are applicable, and by induction over k using lemma 7.15 with W = FV(S) we get Θ = Θ_{k} [W] and Θ_{k} ∈ SU(U_{k}). Due to lemma 7.14 there exists a corresponding sequence of HPT -transformations

U = U_{0} ⟹^{+}_{HPT} U_{p},

where as in Corollary 7.16 U_{p} is in solved form. Applying lemma 7.10 we get

⌈U_{p}⌉^{SUB} ≤_{β} Θ_{k} = Θ [FV(U)].

Theorem 7.18 For every unification problem U there exists a set

G = {⌈U′⌉^{SUB}_{FV_{(U)}} | U ⟹^{+}_{HPT} U′ and U′ is in solved form}

which is a CSU(U). Using some renaming substitution away from W this set is a CSU(U)[W] for arbitrary W.

Proof: We have to check the conditions of Definition 3.3:

(1) G ⊆ SU(S) follows from the correctness of HPT .

(2) The fact that for any normalized substitution θ ∈ SU(U) there is substitution σ ∈ G, such that σ ≤_{β} θ [FV(U)], follows from the completeness of HPT .

(3) The condition DOM(σ) ⊆ FV(U) follows from the construction of the substitutions in G. The condition I(σ) ∩ (Z ∪ DOM(σ)) = ∅ can be satisfied by appropriate renaming.

8 Future Work

The transformation system HPT introduced in this paper is based on the transformation system UT of Dougherty (1991) for unification in the polymorphically typed combinatory logic. In a forthcoming paper I present a detailed investigation of the relationship between HPT and UT.

It is not difficult to see that the search space of HPT is finitely branching. The search space of HT , in contrast, is infinitely branching. However, although we have transformed the infinitely branching search space into a finitely branching one, (unfortunately) we have not reduced the search space. To this end the idea in Nipkow (1990) of introducing product types should be investigated. This amounts to developing a correct and complete unification algorithm for the λ-calculus with product types.

References

Alonzo Church, 1932. A Set of Postulates for the Foundation of Logic. Annals of Mathematics, Vol. 33, pp. 346–366.

Daniel J. Dougherty, 1991. Higher-Order Unificaiton via Combinators. Preprint.

M. Gordon, 1985. HOL: A Machine Oriented Formulation of Higher Order Logic. Technical Report 68, Computer Laboratory, University of Cambridge, Cambridge, England.

G.P. Huet, 1975. A Unification Algorithm for typed λ-Calculus. Theoretical Computer Science, Vol. 1, pp. 27–57.

S. Kaplan and M. Okada, editors, 1990. Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, LNCS, vol. 516, Montreal, Canada. Springer-Verlag.

A. Martelli and U. Montanari, 1982. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, Vol. 4, No. 2, pp. 258–292.

D. Miller and G. Nadathur, 1986. Higher-Order Logic Programming. In Shapiro (1986), pp. 448–462. Tobias Nipkow, 1990. Higher-Order Unification, Polymorphism and Subsorts. In Kaplan and Okada (1990), pp. 229–237. L. C. Paulson and T. Nipkow, 1990. Isabelle Tutorial and User’s manual. Technical Report 189, Computer Laboratory, University of Cambridge, Cambridge, England. Frank Pfenning, 1989. Elf: A language for logic definition and verifieed meta-programming. In Fourth Annual Sumposium on Logic in Computer Science, pp. 313–322. IEEE. E. Shapiro, editor, 1986. Proceedings of the Third International Logic Programming Conference, LNCS, vol. 225, London. Springer-Verlag. W. Snyder and J. Gallier, 1989. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation, Vol. 8, pp. 101–140.