<figure><img src="image_1.png" /></figure>

HAL
open science

# A unification algorithm for type theory

Gérard Huet

► To cite this version:

Gérard Huet. A unification algorithm for type theory. [Research Report] IRIA-RR-023, IRIA. 1973, pp.34. hal-04715932

HAL Id: hal-04715932

https://inria.hal.science/hal-04715932v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Isv: 01984

RR23

RIA
laboria

laboratoire de recherche
en informatique
et automatique

A unification algorithm
for type theory

G.P Huet

34P

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n° 23
juillet 1973
# 1 - INTRODUCTION

Given two well-formed formulas $e_1$ and $e_2$ of a logic $\mathcal{L}$, any substitution $\sigma$ for the free variables $^\dagger$ of $e_1$ and $e_2$ such that $\sigma o e_1 = \sigma o e_2$ is called a **unifier** of $e_1$ and $e_2$. The computation of unifiers is a very basic process in automatic demonstration or proof-checking since it gives us the basic pattern-matching capability by which we can recognize whether a rule of inference is applicable to one or several formulas. Moreover it has been discovered that in first-order logic, for any terms $e_1$ and $e_2$ which could be unified at all, there existed a most general unifier $\sigma$ of these terms, such that every unifier of $e_1$ and $e_2$ could be obtained from $\sigma$ by composition with some other substitution. A simple algorithm computing this m.g.u. (or reporting on the failure of unification) was first given by Guard (1964) under the name of matching. Then Robinson (1965) formulated a complete refutational system for first-order logic whose unique rule of inference, called resolution, can be described as a "cut modulo unification". Unification can thus be seen as an elegant way of getting rid of the substitution rule. Similarly, Robinson & Wos (1969) defined a rule of inference called paramodulation which uses unification to effect equality substitutions.

The situation is more complex in higher-order logic, since most general unifiers do not exist any more. The problem was first investigated by Guard (1964) and then by Gould (1966), who unfortunately restricted himself to the search for common instances of terms. Gould noted that in some cases one needs to consider infinite sets of unifiers. A few incomplete algorithms were given by Darlington (1971,1973) for second-order logic (f-matching) and Ernst (1971) for w-order logic. Then Pietrzykowski (1971) gave a complete enumeration algorithm for second-order logic, which was later extended to w-order logic by Pietrzykowski & Jensen (1972). In this last algorithm, unifiers are computed by composition of four elementary processes, called imitation, projection, elimination and iteration.

In this paper, we shall present an algorithm which searches for the existence of unifiers in w-order logic. Although this problem

<footnote>† If these free variables are supposed to be independent in $e_1$ and $e_2$ we assume that we have renamed them so that independent variables are distinct</footnote>
is undecidable as shown in Huet (1973 a) and Lucchesi (1972), which means that if two terms are not unifiable then our algorithm may never stop, we show here that this problem is much easier than the enumeration of most general unifiers. In particular, we need only to compose two elementary processes, similar to imitation and projection. The very prolific rule of iteration is not used, and our search seems to have good convergence properties.

Moreover, in a refutation-complete system generalizing resolution to order logic described in Huet (1972, 1973 b), we only need to know the possibility of unification, and not the actual computation of unifiers. Our algorithm can be used for this purpose, although it should be noted that in case of a possible unification we can effectively get an explicit unifier with this algorithm.

We shall first describe briefly the language we use (a slight modification of Church's typed λ-calculus). We shall then describe our algorithm, prove its correctness and discuss a few heuristic improvements. Finally we give a few examples of searches for unification.
## 2 - AN OVERVIEW OF TYPED λ-CALCULUS

We shall assume the reader familiar with the λ-calculus notation.

### 2.1/ Types

Every well formed expression (term) of the language possesses a unique *type*, which indicates its position in a functional hierarchy.

There exists a finite set $T_0$ of elementary types, and the set $T$ of types is generated by :

(1) $T_0 \subset T$

(2) $\alpha_1, \alpha_2, \dots, \alpha_n \in T \quad \& \quad \beta \in T_0 \supset (\alpha_1, \alpha_2, \dots, \alpha_n \to \beta) \in T \quad n > 0.$

We shall denote types by Greek letters $\alpha, \beta, \dots$

### 2.2/ Terms

Terms are composed of atoms, applications and abstractions.

#### 2.2.1) Atoms

We have a denumerable set of variables of each type, denoted by small case letters x,y,...,f,g,... and an arbitrary number of constants of any type, denoted by capitals A,B,...,F,G,.... Atoms are either variables or constants and they shall be denoted by $\mathcal{A}, \mathcal{A}', \dots$; the type of atom $\mathcal{A}$ is denoted by $\tau(\mathcal{A})$.

#### 2.2.2) Applications

If $e$ is a term of type $\tau(e) = (\alpha_1, \alpha_2, \dots, \alpha_n \to \beta) \quad n \ge 1$, and $e_1, e_2, \dots, e_m$ are terms of types $\tau(e_i) = \alpha_i \quad 1 \le i \le m \le n$, then we define the *application* $e' = e(e_1, e_2, \dots, e_m)$ as a term of type :

$$ \tau(e') = \begin{cases} (\alpha_{m+1}, \alpha_{m+2}, \dots, \alpha_n \to \beta) & \text{if } n > m \\ \beta & \text{if } n = m \end{cases} $$

In Church's λ-calculus such a term would be written as :

(... (( e( e₁) )( e₂) ) ...)( e_m) .
### 2.2.3) Abstractions

If e is a term and $u_1, u_2, \dots, u_n$ are distinct variables ($n \ge 1$), with $\tau(e) = \beta$ and $\tau(u_i) = \alpha_i$ ($i \le i \le n$), then we define the abstraction

$$e' = \lambda u_1 u_2 \dots u_n . e$$

as a term of type :

$$\tau(e') = \begin{cases} (\alpha_1, \alpha_2, \dots, \alpha_n \to \beta) & \text{if } \beta \in T_0 \\ (\alpha_1, \alpha_2, \dots, \alpha_n, \gamma_1, \gamma_2, \dots, \gamma_m \to \delta) & \text{if } \beta = (\gamma_1, \gamma_2, \dots, \gamma_m \to \delta) \end{cases}$$

In Church's $\lambda$-calculus such a term would be written as :

$$\lambda u_1 . (\lambda u_2 . (\dots (\lambda u_n . e) \dots)) .$$

The variables $u_1, u_2, \dots, u_n$ are said to be bound in $e'$.

### 2.2.4) $\lambda$-conversion

Two rules of $\lambda$-conversion are provided, corresponding to Church's $\alpha$ and $\beta$-reductions. $\alpha$-conversion is a renaming of the bound variables of an abstraction, $\beta$-conversion is the evaluation rule of $\lambda$-calculus which replaces formal arguments by actual ones in an application; more precisely, any subterm :

$$(\lambda u_1 u_2 \dots u_n . e) (e'_1, e'_2, \dots, e'_m) \quad n, m \ge 1$$

is replaced by :

$$-|e'_1/u_1| |e'_2/u_2| \dots |e'_n/u_n| e(e'_1, \dots, e'_m) \quad \text{if } m > n$$

$$-|e'_1/u_1| |e'_2/u_2| \dots |e'_n/u_n| e \quad \text{if } m = n$$

$$-|e'_1/u_1| |e'_2/u_2| \dots |e'_m/u_m| \lambda u_{m+1} \dots u_n . e \quad \text{if } m < n$$

where $|e'_1/u_1| e'_2$ denotes the term $e_2$, in which every occurrence of variable $u$ is replaced by an occurrence of term $e'_1$. Of course conflicts of variables are avoided by adequate applications of $\alpha$-conversion, in the usual way. Also we use the following simplification rules when applicable :
- $(e(e_1, e_2, \dots, e_n))(e_1', e_2', \dots, e_m') \quad n, m \ge 1$

is replaced by $e(e_1, e_2, \dots, e_n, e_1', e_2', \dots, e_m')$

- $\lambda u_1 u_2 \dots u_n (\lambda u_1' u_2' \dots u_m' . e) \quad n, m \ge 1$

is replaced by $\lambda u_1 u_2 \dots u_n u_1' \dots u_m' . e$.

### 2.2.5) Normal form

A term $\lambda u_1 u_2 \dots u_n . \mathcal{A}(e_1, e_2, \dots, e_p)$ is said to be in normal form if and only if:

```
  n \ge 0 ; if n=0      λ. is suppressed
  p \ge 0 ; if p=0     () is suppressed
  ω   is an atom
u_1 ... u_n are distinct variables which do not appear bound in
  e_i ; 1 \le i \le p.
e_i is a term in normal form 1 \le i \le p.
```

It is well known that every term can be transformed into a term in normal form (called its normal form) by a finite number of α-conversions. This normal form is unique, up to α-conversion. The proof uses a double induction on the type structure of the term. This fact contrasts with the non-existence of a normal form in full λ-calculus, and permits us from now on to consider all our terms in normal form. This has the great advantage of getting rid of explicit rules of λ-conversion, which are now used only implicitly for normalization. Therefore from now on two terms will be considered equal if their normal forms are identical, up to an α-conversion.

For instance :

$$ \lambda u.A(\lambda v.u, \lambda v.v) = \lambda v.A(\lambda w.v, \lambda t.v) $$

but : $\lambda u.A(v) \neq \lambda v.A(v)$

and : $f \neq \lambda x.f(x)$.
Let $e = \lambda u_1 u_2 \dots u_n \mathcal{A}(e_1, e_2, \dots, e_p)$ be a term in normal form. We shall call:

<figure><img src="image_3.png" /></figure>

If $\mathcal{A}$ is a constant or a variable belonging to its binder, $e$ is said to be *rigid*, otherwise it is *flexible*.

## 2.3/ Substitutions

A *substitution pair* $\langle x, e \rangle$ consists of a variable $x$ and of a term $e$ of the same type; it is said to *pertain to* variable $x$.

A *substitution* $\sigma = \{ \langle x_i, e_i \rangle \mid 1 \le i \le N \}$ is a finite set of substitution pairs pertaining to distinct variables. We ignore in $\sigma$ pairs such as $\langle x, x \rangle$.

The *application* of $\sigma$ to a term $e$, noted $\sigma \circ e$, is defined as the normal form of the term :

$$ (\lambda x_1 x_2 \dots x_N e) (e_1, e_2, \dots, e_N). $$

Note that possible conflicts of variables being taken care of automatically when we take the normal form, $\sigma \circ e$ does not depend on the order in which we take the $x_i$'s in $\sigma$. For instance, if

$$ \sigma = \{ \langle x, F(y) \rangle, \langle y, G(x) \rangle \}, $$

then

$$ \begin{aligned} \sigma \circ A(x,y) &= (\lambda x. A(x,y)) (F(y), G(x)) \\ &= (\lambda u.v. \Lambda(u,v)) (F(y),G(x)) = A(F(v),G(x)). \end{aligned} $$

If $V$ is any set of variables, we note :

$$ \sigma \setminus V = \{ \langle x_i, e_i \rangle \mid \langle x_i, e_i \rangle \notin \sigma \text{ & } x_i \notin V \} $$

and we define an equivalence $\cong_V$ between substitutions by :
$$ \sigma \bar{=} \sigma' \iff \sigma \setminus V = \sigma' \setminus V $$

Of course for any $\sigma$ and $V$: $\sigma \bar{=} \sigma \setminus V$, and for any term $e$:

$$ (*) \qquad \sigma \circ (\lambda u_1 \dots u_n . e) = \lambda u_1 \dots u_n . [(\sigma \setminus \{u_1, u_2, \dots, u_n\}) . e]. $$

As a corollary, any rigid term keeps its heading unchanged under any application of a substitution. Also, if $V$ does not contain any free variable of $e$, then $\sigma \circ e = (\sigma \setminus V) \circ e$.

The composition of substitutions $\sigma$ and $\rho$, noted $\rho \circ \sigma$, is defined as the substitution :

$$ \{ \langle u_i, \rho \circ e_i \rangle \mid \sigma \circ u_i = e_i \}. $$

Of course, we need to consider only the $u_i$'s to which either $\sigma$ or $\rho$ pertains, since we eliminate dummy pairs $\langle x, x \rangle$.

For instance, if $\sigma = \{ \langle x, f(A) \rangle, \langle y, C(x) \rangle \}$

and $\rho = \{ \langle f, \lambda u.x \rangle, \langle x, B \rangle \}$, then

$$ \rho \circ \sigma = \{ \langle f, \lambda u.x \rangle, \langle y, C(B) \rangle \} . $$

If $\sigma$ and $\rho$ are substitution pairs, $\rho \circ \sigma$ denotes $\{\rho\} \circ \{\sigma\}$.

We have the usual properties :

$$ \sigma_1 \circ (\sigma_2 \circ \sigma_3) = (\sigma_1 \circ \sigma_2) \circ \sigma_3 $$

$$ \text{and :} \qquad \sigma_1 \circ (\sigma_2 \circ e) = (\sigma_1 \circ \sigma_2) \circ e $$

which justifies dropping of parentheses in compositions of substitutions.

Finally, we note that conversion, and therefore applications of substitutions, preserve the types.
3 - THE UNIFICATION ALGORITHM

Let $e_o$ and $e'_o$ be any two terms of the same type. We call
unifier of $e_o$ and $e'_o$ any substitution $\sigma$ such that :

$\sigma \circ e_o = \sigma \circ e'_o$

We are interested in the existence of unifiers for $e_o$ and $e'_o$.
For this purpose we are going to construct a tree, called a matching
tree for $e_o$ and $e'_o$. A node in this tree will be a set of pairs
of terms, representing the current disagreement set :

$$
N = \{ \langle e_1^1, e_1^2 \rangle, \langle e_2^1, e_2^2 \rangle, \dots, \langle e_n^1, e_n^2 \rangle \}
$$

with
$$ \tau(e_i^1) = \tau(e_i^2) \quad 1 \le i \le n. $$

We denote by $\mathcal{F}(N)$ the set of all variables which appear free in some
$e_i^j$ $1 \le i \le n$ and $1 \le j \le 2$.

The nodes in the tree are linked by arcs labelled with substitu-
tion pairs. We also have nodes of a special kind, called TFNs (terminal
failure nodes) which do not have successors. The empty nodes Ø are
called TSNs (terminal success nodes) ; they indicate a successful
unification and do not have successors either.

We shall describe below two procedures :

- Simplify, which takes as argument a node and returns as value a
node, which is either terminal, or consists of a non-empty finite set
{<e<sub>1</sub><sup>1</sup>, e<sub>1</sub><sup>2</sup>> | 1 < i < n} such that :

$$
\begin{array}{l@{\quad}l@{\quad}l}
\forall i (1 \le i \le n) & e_i^1 & \text{is flexible} \\
\text{and} & e_i^2 & \text{is rigid.}
\end{array}
$$

- Match, which takes as arguments a flexible term $e_1$, a rigid term $e_2$ of the same type and a finite set of variables V. It returns a finite set of substitution pairs.
### 3.1/ Construction of a matching tree

The initial node in the tree is *Simplify* ({<e<sub>0</sub>, e'<sub>0</sub>}}). Let N be the current node. If N is a TSN or a TFN it has no successor. Otherwise, let <e<sub>1</sub>, e<sub>2</sub>> be a pair in N such that e<sub>2</sub> is rigid and let S = *Match* (e<sub>1</sub>, e<sub>2</sub>, F(N)). If S = Ø, replace N by TFN. Otherwise, for every σ in S, grow a link, labelled with σ, from N to

$$N' = \text{Simplify} ( \{ <\sigma_0 e_i^1, \sigma_0 e_i^2> \mid <e_i^1, e_i^2> \in N \} )$$

This construction is sound because of the properties of *Simplify* and *Match* given above. It is non-deterministic because of the arbitrary choice of the pair to *Match*. As we shall see, we do not need to impose any way of making this choice, and thus all matching trees constructed as above are complete. This permits us to use any heuristic considerations to pick up a pair in the current disagreement set.

A unification algorithm can then be described as any algorithm searching for a TSN in a matching tree (for instance using level saturation), and its completeness proved using our completeness theorem below and Koenig's lemma, the branchiness of any matching tree being finite. Again heuristic considerations can be used to direct the search in a matching tree.

Note that our construction applies as well to the simultaneous unification of any finite number of pairs of terms, by taking the set of these pairs as the initial node of the tree. It therefore applies also to the unification of a finite number of terms e<sub>1</sub>, e<sub>2</sub>, ..., e<sub>n</sub>. For instance, unify the set of pairs {<e<sub>1</sub>, e<sub>2</sub>>, ..., <e<sub>1</sub>, e<sub>n</sub>>}.

### 3.2/ Let us now describe the procedure Simplify

#### 3.2.1) Simplify (N);

**Step 1:** If there does not exist in N a pair <e<sub>1</sub>, e<sub>2</sub>> such that e<sub>1</sub> and e<sub>2</sub> are both rigid, then go to step 2, else let us write :

$$N = \{ <e_1, e_2> \} \cup \bar{N}$$
$$
\text{with :} \quad \begin{cases} e_1 = \lambda u_1 u_2 \dots u_{n_1} \cdot \mathcal{A}_1^1 (e_1^1, \dots, e_{p_1}^1) & n_1 \ge 0 \ p_1 \ge 0 \\ e_2 = \lambda v_1 v_2 \dots v_{n_2} \cdot \mathcal{A}_2^2 (e_2^2, \dots, e_{p_2}^2) & n_2 \ge 0 \ p_2 \ge 0 \ ; \end{cases}
$$

( ⋃ denotes the disjoint union).

If $n_1 \neq n_2$ then return (TFN) else let us write $n = n_1 = n_2$;

If $\mathcal{A}_1 \neq (\lambda v_1, v_2, \dots, v_n, \mathcal{A}_2)$ ($u_1, u_2, \dots, u_n$) then return (TFN) else let us
write $p = p_1 = p_2$ [true since $\tau(e_1) = \tau(e_2)$] ;

Do $N \leftarrow \{ \langle \tilde{e}_i^1, \tilde{e}_i^2 \mid 1 \le i \le p \} \cup \bar{N} $, where :

$$
\tilde{e}_i^1 = \lambda u_1 u_2 \dots u_n \cdot e_i^1 \quad (+)
$$

$$
\tilde{e}_i^2 = \lambda v_1 v_2 \dots v_n \cdot e_i^2 ; \text{ go to step 1 ;}
$$

Step 2 : Replace in N every pair <e<sub>1</sub>,e<sub>2</sub>> where e<sub>1</sub> is rigid and e<sub>2</sub>
is flexible, by the pair <e<sub>2</sub>,e<sub>1</sub>> ; go to step 3 ;

Step 3 : If there does not exist in N a pair <e<sub>1</sub>,e<sub>2</sub>> such that e<sub>2</sub>
is rigid then return (TSN) else return (N) ; end of Simplify ;

3.2.2) Examples of applications of Simplify

1) $N = \{ \langle A(\lambda u.B(x,u)),C),A(\lambda v.B(v,v)),f(C) \rangle \}$.

The different values assumed by N are, successively :

step 1 $N = \{ \langle \lambda u.B(x,u), \lambda v.B(v,v) \rangle, \langle C, f(C) \rangle \}$

step 1 $N = \{ \langle \lambda u.x, \lambda v.y \rangle, \langle \lambda u.u, \lambda v.v \rangle, \langle C, f(C) \rangle \}$

step 1 $N = \{ \langle \lambda u.x, \lambda v.y \rangle, \langle C, f(C) \rangle \}$

step 2 $N = \{ \langle \lambda u.x, \lambda v.y \rangle, \langle f(C), C \rangle \}$ which is returned.

2) $N = \{ \langle A(\lambda u.B(x,u)), A(\lambda v.B(v,v)) \rangle \}$.

After first three steps as above, we get

$N = \{ \langle \lambda u.x, \lambda v.v \rangle \}, \text{ and after step 3 we return TSN.}$

+ If $e_i^1 = \lambda v_1 \dots v_m \cdot \mathcal{A}^1(\dots)$ then $\tilde{e}_i = \lambda u_1 \dots u_n w_1 \dots w_m \cdot \mathcal{A}^1(\dots)$ and by
our definition of normal form, if $e_i$ is in normal form then every
$\tilde{e}_i^1$ will be too : no precaution is needed for conflicts of variables.
3) $N = \{ <\lambda uv.A(u, \lambda vw.v), \lambda vw.A(v, \lambda u.v)> \}.$

step 1 $N = \{ <\lambda uv.u, \lambda vw.v> , <\lambda uvw.v, \lambda vwu.v> \}$

step 1 $N = \{ <\lambda uvw.v, \lambda vwu.v> \}$

step 1 we return TFN.

It is obvious that for every N, Simplify will stop after a finite number of steps. We shall now prove its correctness.

### 3.2.3) Proof of correctness of Simplify.

First we introduce the definition : a substitution $\sigma$ is said to unify a node N if and only if it simultaneously unifies every pair in N.

Let N be any node. We mean by correctness of *Simplify* the following three lemmas :

**Lemma 1** Simplify (N) = TFN $\Rightarrow \exists \sigma : \sigma$ unifies N.

**Lemma 2** Simplify (N) = N' $\Rightarrow \forall \sigma : (\sigma$ unifies N $\Longleftrightarrow$ $\sigma$ unifies N')$ where N' is not a terminal node.

**Lemma 3** Simplify (N) = TSN $\Rightarrow \exists \sigma : \sigma$ unifies N.

We prove the first two of these lemmata by induction on the number of applications of step 1. Let $N_k$ be the current set at the beginning of step 1, $<e_1, e_2>$ the pair selected in $N_k$. As we saw, rigid terms keep their heading under substitution. Therefore, since $e_1$ and $e_2$ are both rigid, they must have the same heading (up to $\alpha$-conversion) in order to be unifiable. If they do not have the same heading, TFN is returned, proving lemma 1. Otherwise, let $\sigma$ be any substitution.

Let us write :
$$e_1 = \lambda u_1 \dots u_n \cdot \underline{a_1} (e_1^1, \dots, e_p^1)$$

$e_2 = \lambda v_1 \dots v_n \cdot \underline{a_2} (e_1^2, \dots, e_p^2),$

and let :
$$\sigma_1 = \sigma \setminus \{u_i \mid 1 \le i \le n\}, \quad \sigma_2 = \sigma \setminus \{v_i \mid 1 \le i \le n\}.$$

Then, according to (*) above :

$\sigma \circ e_1 = \lambda u_1 \dots u_n \cdot \underline{a_1} (\sigma_1 \circ e_1^1, \dots, \sigma_1 \circ e_p^1)$

and
$$\sigma \circ e_2 = \lambda v_1 \dots v_n \cdot \underline{a_2} (\sigma_2 \circ e_1^2, \dots, \sigma_2 \circ e_p^2).$$
Now $\sigma \circ e_1 = \sigma \circ e_2$ if and only if all their arguments are pairwise identical, up to renaming of $u_i$ by $v_i$ ($1 \le i \le n$), i.e. if and only if: $\lambda u_1 \dots u_n \cdot (\sigma_1 \circ e_1) = \lambda v_1 \dots v_n \cdot (\sigma_2 \circ e_1^2)$, $1 \le i \le p$ i.e., using (*) again in the other direction, if and only if:

$$ \sigma \circ e_i^1 = \sigma \circ e_i^2 \quad (\text{using the notations of the algorithm}). $$

This proves that, for any $\sigma$, $\sigma$ unifies $N_k \Leftrightarrow \sigma$ unifies $N_{k+1}$ where $N_{k+1}$ is the set at the next application of step 1. Therefore, by induction on the number of applications of step 1, $N'$ being the set at the beginning of step 2: $\forall \sigma: (\sigma$ unifies $N \Leftrightarrow \sigma$ unifies $N'$).

Step 2 is obviously sound since unifiable is a symmetric relation and so if in $N'$ there exists a rigid term lemma 2 is proved. Else, let $N$ be the set at the beginning of step 3. To prove lemma 3, we need only prove that if $N = \{ \langle e_i^1, e_i^2 \rangle \mid 1 \le i \le n \}$, where $e_i^1$ is flexible ($1 \le i \le n$, $1 \le j \le 2$), then there exists a unifier for $N$.

Let $f_1, f_2, \dots, f_p$ be all the variables that appear as head of $e_i^1$ or $e_i^2$, $1 \le i \le n$; let us write $\tau(f_i) = (\alpha_1^i, \alpha_2^i, \dots, \alpha_{q_i}^i, \beta_i)$ if $\tau(f_i)$ is a composite type, $\tau(f_i) = \beta_i$ if it is elementary. We define at most $|T_0|$ equivalence classes of these variables by the relation $f_i \equiv f_j \Leftrightarrow \beta_i = \beta_j$ and for each class $[\beta]$ we introduce a new variable $h_\beta$ of type $\beta$. Now we define:

$$ \sigma = \{ \langle f_i, \lambda v_1 \dots w_{q_i} \cdot h_{\beta_i} \rangle \mid 1 \le i \le p \} $$

where the $w_{j}$'s are new variables of type respectively $\alpha_j^i$; if $\tau(f_i) = \beta_i$, then we omit the binder. We claim that $\sigma$ unifies $N$.

**Proof:** Suppose $e_i^1 = \lambda u_1 \dots u_{m_1} \cdot f_j (E_1^1, E_2^1, \dots, E_r^1)$ and $e_i^2 = \lambda v_1 \dots v_{m_2} \cdot f_k (E_1^2, E_2^2, \dots, E_s^2)$.

$$ \begin{align*} \text{Then } \sigma \circ e_i^1 &= \lambda u_1 \dots u_{m_1} w_{r+1} \dots w_{q_j} \cdot h_{\beta_j} \\ \sigma \circ e_i^2 &= \lambda v_1 \dots v_{m_2} w_{s+1} \dots w_{q_k} \cdot h_{\beta_k} \end{align*} $$

Since $\tau(e_i^1) = \tau(e_i^2)$, we must have:
$$ egin{cases} m_1 + q_j - r = m_2 + q_k - s \\ \tau(u_1) = \tau(v_1), \dots, \tau(w_q) = \tau(w_q) \\ \beta_j = \tau(h_{\beta_j}) = \tau(h_{\beta_k}) = \beta_k \text{ and therefore } h_{\beta_j} = h_{\beta_k} \end{cases} $$

which proves $\sigma \circ e_i^1 = \sigma \circ e_i^2$. QED

This concludes the proof of correctness of *Simplify*. Note that we are able to give explicitly a unifier for any TSN; however this TSN will represent in general a whole set of unifiers. We shall come back to this remark later.

### 3.3/ Let us now describe the procedure *Match*.

We shall present it in a loose algorithmic fashion, with many comments to explain and justify its actions.

#### 3.3.1) *Match* ($e_1, e_2, V$);

$e_1$ is a flexible term and $e_2$ a rigid term of the same type. $V$ is a finite set of variables. Let us write :

$$ e_1 = \lambda u_1 \dots u_{n_1} . f(e_1^1, e_2^1, \dots, e_{p_1}^1) \qquad n_1 \ge 0 \quad p_1 \ge 0 $$

$$ e_2 = \lambda v_1 \dots v_{n_2} . \mathcal{A}(e_1^2, e_2^2, \dots, e_{p_2}^2) \qquad n_2 \ge 0 \quad p_2 \ge 0 $$

$$ \text{and} \quad \tau(f) = (\alpha_1, \alpha_2, \dots, \alpha_{p_1}, \alpha_{p_1+1}, \dots, \alpha_{q_1} \to \beta) \qquad q_1 \ge p_1 $$

Since $e_2$ is rigid, its heading cannot be changed by substitution, whereas the heading of $e_1$ can be adjusted to that of $e_2$ under certain conditions. First, in order to adjust its binder, we need to have $n_1 \le n_2$. Therefore, if $n_1 > n_2$ we return $S = \emptyset$; else let $n = n_2 - n_1 \ge 0$.

We shall need $p_1$ variables, that we shall denote by $w_i$ with $\tau(w_i) = \alpha_i$ ($1 \le i \le p_1$). In order to avoid conflicts, we impose $w_i \notin \{v_{n_1+1}, \dots, v_{n_2}\}$.

In order to adjust the binder of $e_1$, we shall consider substitutions for $f$ of term $\lambda z_1 \dots z_2 \mathcal{A}'(\dots)$. The head $\mathcal{A}'$ will be :

- either $\mathcal{A}'$, and the most general such substitution will be given by the rule of imitation (†) below.

<footnote>† This term is due to T. Pietrzykowski.</footnote>
- or $z_k 1 \le k \le r$, which corresponds to the rule of projection below.

As we shall see it is sufficient to consider these two cases. The
result S will be the union of the results given by the two rules.

3.3.1.1) Imitation rule

We want to "imitate" $e_2$ by $e_1$, substituting a term with head $\mathcal{D}$ for
$f$. This will not be possible if $\mathcal{D}$ is some $v_i$ with $1 \le i \le n_1$ because the
corresponding $u_i$ is protected from substitution by $f$ by the binder of $e_1$.
This rule is therefore applicable only if $\mathcal{D}$ is a constant or some $v_i$ with
$n_1 < i \le n_2$. We shall have two (exclusive) subcases.

3.3.1.1.1) n >= 0

This determines completely the heading of the term we must substi-
tute for f. The rest of the term is filled in the most general way, by
introducing new variables. Precisely, we return as unique solution of
this subcase :

$$
\sigma = \langle f, \lambda w_1 \dots w_{p_1} v_{n_1+1} \dots v_{n_2} \dots a(E_1, E_2, \dots, E_{p_2}) \rangle
$$

$$
\text{where} \quad E_i = h_i(w_1, \dots, w_{p_1}, v_{n_1+1}, \dots, v_{n_2}) \quad 1 \le i \le p_2,
$$

the $h_i$'s being distinct variables of the appropriate type not in V.

(Note : no conflict will arise, even if $v_k$, $n_l < k \le n_2$ appears free in $e_l$ ; also there is no risk of conflict of a $h_i$ with a $w_j$ or a $v_k$ because they have different types).

3.3.1.1.2) n = 0

Considering the remark above, in this subcase $\mathcal{D}$ must be a constant.
The heading of the term substituted for $f$ is going to be some $\lambda w_1 \dots w_k \mathcal{D}$,
with $0 \le k \le p_1$. However, any such $k$ will not do, because we have a
type condition on the remaining arguments of $e_1$. More precisely, we must
be able to complete the term with a number of arguments = $p_2 - (p_1 - k) \ge 0$
which gives the first condition :

$$
(1) \quad \max(0, p_1 - p_2) \le k \le p_1
$$

Also, the unchanged arguments of $e_1$ must be type-compatible with the
ones of $e_2$ :

$$
(2) \quad \alpha_j = \tau(e_{p_2-p_1+j}^2) \quad \text{Vj} \quad k < j \le p_1
$$
Conversely, these conditions are sufficient for the substitution below to be legitimate. Therefore, for every k satisfying (1) and (2), we take as solution in S :

$$ \sigma = \langle f, \lambda w_1 \dots w_k \cdot \mathcal{A}(E_1, E_2, \dots, E_{p_2-p_1+k}) \rangle $$

where $E_i = h_i(w_1, \dots, w_k)$, $1 \le i \le p_2-p_1+k$, the $h_i$'s being distinct variables of the appropriate type not in V. In this subcase, we have therefore at most $\min(p_1, p_2) + 1$ solutions. Note that conditions (1) and (2) are always satisfied with $k = p_1$, which guarantees at least one solution. But we cannot restrict ourselves to this case unless we admit the n-reduction rule :

$$ \lambda u \cdot e(u) = e \text{ where } u \text{ does not appear free in } e. $$

For instance, consider $e_1 = f(B(A))$ and $e_2 = A(B(f))$, with $\tau(f) = \tau(A) = (\alpha \to \alpha)$, $\tau(B) = ((\alpha \to \alpha) \to \alpha)$, which admit as unique unifier $<f, A>$, corresponding to $p_1 = p_2 = 1$, $k = 0$.

### 3.3.1.2) Projection rule

We want to project f on one of its arguments. The possible headings for the term we want to substitute for f are :

- either (a) $\lambda w_1 \dots w_k \cdot w_i$ with $1 \le i \le k \le p_1$

- or (b) $\lambda w_1 \dots w_{p_1} \cdot v_{n_1+1} \dots v_{n_1+k} \cdot w_i$ with $1 \le k \le n \le p_1$

- or (c) $\lambda w_1 \dots w_{p_1} \cdot v_{n_1+1} \dots v_{n_1+k} \cdot v_{n_1+i}$ with $1 \le i \le k \le n$.

However in case (c), after substitution of the term for f, we would have to unify

$$ \sigma \cdot e_1 = \lambda u_1 \dots u_{n_1} \cdot v'_{n_1+1} \dots v'_{n_1+k} \cdot v'_{n_1+i} \dots $$

with $\sigma \cdot e_2 = \lambda v_1 \dots v_{n_1} \cdot v_{n_1+1} \dots v_{n_2} \cdot \mathcal{A} \dots$ (...), and this

will be rejected by Simplify unless $k = n$ and $\mathcal{A} = v_{n_1+i}$, which case we have already considered in 3.3.1.1 and so we can limit ourselves to cases (a) and (b). These cases are not exclusive, and we shall return as result the union of their solutions.
### 3.3.1.2.1) Heading $\lambda w_1 \dots w_k \cdot w_i$

$$ (1) \qquad 1 \le i \le k \le p_1 $$

Here we have a supplementary condition on the type of $w_i$. Precisely, there must exist $m \ge 0$ such that:

$$ (2) \qquad \alpha_i = (\gamma_1, \gamma_2, \dots, \gamma_m, \alpha_{k+1}, \dots, \alpha_{q_1} \to \beta) \\ \text{for some } \gamma_1, \dots, \gamma_m \in \mathcal{T}. $$

For each $i$ and $k$ satisfying (1) and (2), we take as solution in $S$:

$$ \sigma = \langle f, \lambda w_1 \dots w_k \cdot w_i (E_1, E_2, \dots, E_m) \rangle $$

where $E_j = h_j(w_1, \dots, w_k)$, $1 \le j \le m$, the $h_j$'s being distinct variables of the appropriate type not in $V$.

Note that, given $i$ and $k$, $m$ is completely determined from (2). This gives us a maximum of $p_1(p_1+1)/2$ solutions.

### 3.3.1.2.2) Heading $\lambda w_1 \dots w_p \cdot w_{n_1+1} \dots w_{n_k} \cdot w_i$

This case is very similar to the previous one, changes are just notational.

$$ (1) \quad 1 \le k \le n \quad \text{and similarly:} $$

$$ (2) \qquad \alpha_i = (\gamma_1, \gamma_2, \dots, \gamma_m, \alpha_{p_1+k+1}, \dots, \alpha_{q_1} \to \beta) \\ \text{(As above, this condition is satisfied if } p_1+k=q_1, \text{ } m=0 \text{ and } \alpha_i = \beta \text{).} $$

The solutions in this case are all the:

$$ \sigma = \langle f, \lambda w_1 \dots w_p \cdot w_{n_1+1} \dots w_{n_k} \cdot w_i (E_1, E_2, \dots, E_m) \rangle $$

where $E_j = h_j(w_1, \dots, w_p, v_{n_1+1}, \dots, v_{n_k} \cdot k)$, $1 \le j \le m$, the $h_j$'s being distinct variables of the appropriate type not in $V$. Here we have a maximum of $n \times p_1$ solutions.

This completes our analysis of the projection rule. Note that we have at most $p_1(p_1 + 2n + 1)/2$ solutions. In practice of course we shall get fewer solutions because of the conditions (2).
end of *Match* ;

3.3.2) Example of application of *Match*

Let $e_1 = f(x, B)$ and $e_2 = A(B)$, with

$$
\alpha_1 = \tau(x) = (\gamma, \gamma \to \gamma), \alpha_2 = \tau(B) = \gamma, \beta = \gamma, \tau(A) = (\gamma \to \gamma).
$$

Here : $n_1 = n_2 = 0, p_1 = q_1 = 2, p_2 = 1$.

We call *Match* ($e_1, e_2, \{x,f\}$).

3.3.2.1) *Imitation*

$n = n_3 - n_1 = 0$ and so we are in case 3.3.1.1.2

$p_1 - p_2 = 1 \le k \le p_1 = 2$, so we have two choices :

. k = 1 for which condition (2) : α₂ = τ(B) = γ holds, and we take
σ₁ = <f, λw₁.A >; note that x will be eliminated here.

. k = 2 for which condition (2) is vacuous, and we take

$$
\sigma_2 = \langle f, \lambda w_1, w_2 \cdot A(h_1(w_1, w_2)) \rangle
$$

with

$$
\tau(h_1) = ((\gamma, \gamma \to \gamma), \gamma \to \gamma).
$$

3.3.2.2) *Projection*

As $n = 0$ we consider only case 3.3.1.2.1 : $1 \le k \le 2$.

With $k = 1$, condition (1) forces $i = 1$, and condition (2) is satisfied
for $m = 1$, which gives the solution :

$$
\sigma_3 = \langle f, \lambda w_1 \cdot w_1(h_1(w_1)) \rangle, \text{ with } \tau(h_1) = ((\gamma, \gamma \to \gamma), \gamma \to \gamma).
$$

The $h_1$ here is of course distinct from the one in $\sigma_2$, since they
have a different type. But the only constraint we impose on the "new
variables" $h_i$ is that they should not appear free in the node of the
matching tree from which we call *Match*, and so we could use the same
"new" variables for distinct successors of a node.
With $k = 2$, we have two choices for $i$ :

i = 1 ; then m = 2 and we take :

$$
\sigma_4 = \langle f, \lambda w_1 w_2 \cdot w_1 (h_1 (w_1, w_2), h_2 (w_1, w_2)) \rangle,
$$
with $\tau(h_1) = \tau(h_2) = \tau(f)$.

. i = 2 ; then m = 0 and we take :

$$
\sigma_5 = \langle f, \lambda w_1 w_2 \cdot w_2 \rangle.
$$

The reader will check that $\sigma_1 - \sigma_5$ are independent substitutions.
If the node from which we called *Match* was $N = \{\langle e_1, e_2 \rangle\}$, then its
corresponding successors are

$$
N_1 = \text{TSN}
$$

$$
N_2 = \{ \langle h_1(x, B), B \rangle \}
$$

$$
N_3 = \{ \langle x(h_1(x), B), A(B) \rangle \}
$$

$$
N_4 = \{ \langle x(h_1(x, B), h_2(x, B)), A(B) \rangle \}
$$

$$
N_5 = \text{TFN.}
$$

3.3.3) Proof of correctness of Match

Let us first introduce a complexity measure for substitutions.

Definition.

Let $\xi = \{<u_i, e_i> \mid 1 \le i \le r\}$ be any substitution. We define :

$$
\mathrm{comp}(\xi) = \sum_{i=1}^{r} c(e_i), \quad \text{with}
$$

$$
c(\lambda u_1 \dots u_n \circled{\bf (E}}_1, \dots, \underline{\mathbf{E}}_p \underline{\mathbf{) }} ) = 1 + \sum_{i=1}^{p} c(E_i).
$$

We mean by correctness of *Match* the following lemma :

Lemma 4.

For any terms $e_1$ and $e_2$ of the same type, where $e_1$ is flexible
and $e_2$ rigid, and for any finite set $V$ of variables, if there exists
a unifier $\rho$ of $e_1$ and $e_2$, then *Match*($e_1$, $e_2$, $V$) returns a non-empty set
in which there is a substitution pair $\sigma$ more general than $\rho$, in the
sense that there exists a substitution $\eta$ such that :
$$
\begin{cases}
\text{comp}(\eta) < \text{comp}(\rho) \\
\rho = \bar{\rho}, \eta \circ \sigma \text{ for some finite set } V' \text{ such that } V' \cap V = \emptyset
\end{cases}
$$

Proof.

Let $f$ be the head of $e_1$, $\mathcal{A}$ that of $e_2$. If $\rho$ unifies $e_1$ and $e_2$, there must exist in $\rho$ a pair pertaining to $f$.

Let us write :

$\rho = \{<f, \lambda z_1 z_2 \dots z_k . \mathcal{A}'(E_1', \dots, E_\ell') >| \cup \bar{\rho} \cup \bar{\bar{\rho}} , \text{ where } \bar{\rho} \text{ contains all pairs of } \rho \text{ which pertain to variables in } V \setminus \{f\}.$

1st case.

$\mathcal{A}'$ is $\mathcal{A}$, or some $z_i$, $1 \le i \le k$. We saw that we considered in
Match all possible cases of such headings, which means that there
exists in the result $S = \text{Match}(e_1, e_2, V)$ some :

$$
\sigma = \langle f, \lambda w_1 w_2 \dots w_k . \mathcal{A}''(E_1, \dots, E_\ell) \rangle, \text{ where :}
$$

$$
\left\{
\begin{array}{l}
\tau(w_i) = \tau(z_i) \qquad 1 \le i \le k \\
\\
\mathcal{A}'' = (\lambda z_1 z_2 \dots z_k . \mathcal{A}') (w_1, w_2, \dots, w_k) \\
\\
E_j = h_j(w_1, w_2, \dots, w_k) \qquad 1 \le j \le l \qquad h_j \notin V.
\end{array}
\right.
$$

Now let $\eta = \{ \langle h_j, \lambda z_1 \dots z_k . E_j' \rangle \mid 1 \le j \le l \} \cup \bar{\rho}$; $\eta$ is a legitimate substitution, since every pair in $\bar{\rho}$ pertains to some variable in $V$.

Taking $V' = \{ \langle h_j | 1 \le j \le l \rangle \cup \{g | \exists \langle g, e_g \rangle \in \bar{\rho} \} \}$, we check that :

$\rho = \bar{\rho}, \eta \circ \sigma \text{ with } V' \cap V = \emptyset.$

$$
\text{Finally :}
\begin{align*}
\text{comp}(\eta) &= \text{comp}(\bar{\rho}) + \sum_{j=1}^{\ell} c(\lambda z_1 \dots z_k . E_j') \\
&= \text{comp}(\bar{\rho}) + \sum_{j=1}^{\ell} c(E_j') = \text{comp}(\rho) - 1 - \text{comp}(\bar{\bar{\rho}}) . \text{NED}
\end{align*}
$$
2nd case.

ω' is neither ω nor some zᵢ. Then ρ∘e₁ will be :

$$ - \text{if } k \le p_1 : \lambda u_1 \dots u_{n_1} \cdot \omega''(\dots) $$

$$ - \text{if } k > p_1 : \lambda u_1 \dots u_{n_1} z'_{p_1+1} \dots z'_k \cdot \omega''(\dots) $$

where ω'' is an atom distinct from ω, uⱼ, 1 ≤ j ≤ n₁ and z'ᵢ, pᵢ < i ≤ k.

This contradicts the fact that it must be equal to ρ∘e₂ = λv₁...vₙ₂ ∙ ω(...)

and so we shall never have to consider this case. This shows that the two rules of imitation and projection are sufficient for our purpose.

This concludes the proof of lemma 4.

In the case of interest to us, V = F(N), where <e₁, e₂> ∈ N and therefore we can conclude that η∘σ unifies e₁ and e₂.

Actually, the minimal V would be F(N) \ {f}, but in practical implementations the simpler is to have *Match* generate totally new variables for the hᵢ's.

## 4 - CORRECTNESS OF THE UNIFICATION PROCESS

We shall now prove that our unification process is correct. First we prove a soundness theorem, stating that if any matching tree for e₀ and e'₀ possesses a TSN then e₀ and e'₀ are unifiable. Then we prove a completeness theorem, stating that if e₀ and e'₀ are unifiable, then every matching tree for e₀ and e'₀ possesses a TSN at a finite level.

### 4.1/ Soundness

Let us suppose that we have constructed a matching tree for e₀ and e'₀ which possesses a TSN on some branch :

$$ N_0 \xrightarrow{\sigma_1} N_1 \xrightarrow{\sigma_2} \dots \xrightarrow{\sigma_p} N_p = \text{TSN} \qquad p \ge 0 $$

Let $\xi_p$ be defined as a substitution which unifies $N_p$, as constructed in the proof of lemma 3 above.
Now, we define :

$$ \xi_i = \xi_{i+1} \circ \sigma_{i+1} \qquad p > i \ge 0. $$

We prove by (descending) induction on i that $\xi_i$ unifies $N_i$. The base step has been done in lemma 3, for the induction step we assume that $\xi_{i+1}$ unifies $N_{i+1}$.

Let $\overline{N}_{i+1} = \{ \langle \sigma_{i+1} \circ e_j^1, \sigma_{i+1} \circ e_j^2 \rangle \mid \langle e_j^1, e_j^2 \rangle \in N_i \}$.

By induction hypothesis and lemma 2, since $N_{i+1} = \text{Simplify}(\overline{N}_{i+1})$, $\xi_{i+1}$ unifies $\overline{N}_{i+1}$; that is, for every $\langle e_j^1, e_j^2 \rangle \in N_i$, $\xi_{i+1} \circ \sigma_{i+1} \circ e_j^1 = \xi_{i+1} \circ \sigma_{i+1} \circ e_j^2$ i.e. $\xi_i$ unifies $N_i$, which concludes the induction step.

As a particular case, we get that $\xi_o$ unifies $N_o = \text{Simplify}(\langle e_o, e_o' \rangle)$ and therefore by lemma 2, $\xi_o = \xi_p \circ \sigma_p \circ \sigma_{p-1} \circ \dots \circ \sigma_1$ unifies $e_o$ and $e_o'$. QED

## 4.2/ Completeness

Let us assume that terms $e_o$ and $e_o'$ are unifiable by substitution $\rho$. Let us consider an arbitrary matching tree for $e_o$ and $e_o'$. We shall construct a branch

$$ N_o \xrightarrow{\sigma_1} N_1 \xrightarrow{\sigma_2} \dots \xrightarrow{\sigma_i} N_i $$

of this tree, together with a sequence of substitutions $\xi_o, \xi_1, \dots, \xi_i$ such that $\forall i \ge 0 \ \xi_i$ unifies $N_i$, and of complexities strictly decreasing.

We prove this by (ascending) induction on i. The base step is obvious, taking $\xi_o = \rho$, since $\rho$ unifies $N_o = \text{Simplify}(e_o, e_o')$ by lemma 2. For the induction step, we assume the assertion true for i. Now either $N_i$ is a TSN, in which case we stop the construction, or in $N_i$ we are considering a pair $\langle e_1, e_2 \rangle$ such that $e_2$ is rigid. $N_i$ cannot be a TFN by lemma 1, since by hypothesis $\xi_i$ unifies $N_i$. Using lemma 4, we know that $\text{Match}(e_1, e_2, \mathcal{F}(N_i))$ returns some $\sigma$ such that there exists $\eta$ with $\xi_i \bar{\eta}, \eta \circ \sigma$, and therefore there exists a branch $N_i \xrightarrow{\sigma} N'$ in the tree.

Let us choose : $\xi_{i+1} = \eta, \sigma_{i+1} = \sigma$ and $N_{i+1} = N'$.

By construction,

$$ N_{i+1} = \text{Simplify}(\overline{N}_{i+1}), $$
where $\bar{N}_{i+1} = \{ < \sigma_{i+1} \circ e_j^1, \sigma_{i+1} \circ e_j^2 | <e_j^1, e_j^2> \in N_i \}$.

For every $<e_j^1, e_j^2>$ in $N_i$: $\xi_{i+1} \circ e_j^1 = \xi_{i+1} \circ e_j^2$ by hypothesis, and therefore $\xi_{i+1} \circ \sigma_{i+1} \circ e_j^1 = \xi_{i+1} \circ \sigma_{i+1} \circ e_j^2$, since $V'$ does not contain free variables of $e_j^1$ or $e_j^2$. This shows that $\xi_{i+1}$ unifies $\bar{N}_{i+1}$ and thus unifies $N_{i+1}$ by lemma 2, unless $N_{i+1}$ is a TSN. By lemma 4 finally, we have $\text{comp}(\xi_{i+1}) <\text{comp}(\sigma_i)$, which concludes the induction step. This last relation shows that our construction will stop on a TSN in at most $\text{comp}(\rho)$ steps. Therefore our matching tree will have a TSN at a level $< \text{comp}(\rho)$.

This proves our completeness theorem. Of course if $e_0$ and $e'_0$ are not unifiable then we may construct an infinite tree. This may happen even for first-order pairs such as $<x, A(x)>$, which we could easily recognize as TFNs. We shall discuss in the next section a few heuristics for such special cases.

# 5 - HEURISTIC IMPROVEMENTS AND REMARKS

## 5.1/ Let us first look at the special case of unification of a variable $x$ with a term $e$ of the same type.

This case is specially important since it occurs often in practice.

### Lemma 5.

If $x$ does not appear free in $e$, then $\sigma = \{<x, \emptyset>\}$ is a most general unifier of $x$ and $e$.

### Proof

Let $\rho$ be any unifier of $x$ and $e$; we shall give a substitution $\eta$ such that $\rho = \eta \circ \sigma$.

## Case 1.

There exists in $\rho$ a pair pertaining to $x$; let us write :
$\rho = \{<x, E>\} \cup \bar{\rho}$.

$\rho \circ x = E = \rho \circ e$ by hypothesis.

$\rho \circ e = (\rho \setminus \{x\}) \circ e = \bar{\rho} \circ e$ since x does not appear free in e.

Therefore $\bar{\rho} \circ \sigma = \{<x, E>\} \cup \bar{\rho} = \rho$ and so $\bar{\rho}$ is a legitimate $\eta$.

**Case 2.**

There is no pair in $\rho$ pertaining to $x$. Then

$\rho \circ x = x = \rho \circ e$, and :

$\rho \circ \sigma = \rho \cup \{<x, x>\} = \rho$ and $\rho$ is a legitimate $\eta$. QED

This lemma, which is a generalization to $\omega$-order logic of a well-known property of first-order unification, could be used by *Match*($x,e,V$), which would then return the unit set $\{<x,e>\}$ and by *Simplify* for those pairs $<x,e>$ such that $e$ is flexible.

However, its converse is not true any more; i.e., $x$ may appear free in $e$ and still be unifiable with it. For example, if $e = f(x)$, by substitution $\{<f,\lambda u.u>\}$ or $\{<f,\lambda u.u>\}$.

This may happen even if there is no free variable such as $f$ above to eliminate $x$. For instance, take

$e = \lambda u.u(x(\lambda v.v))$ with $\tau(v) = \gamma, \tau(u) = (\gamma \rightarrow \gamma)$,
$\tau(x) = ((\gamma \rightarrow \gamma) \rightarrow \gamma)$;

$\sigma = \{<x, \lambda u.u(y)>\}$ unifies $e$ and $x$, with $\tau(y) = \gamma$.

A still more striking example is the following one :

$e = \lambda u.u(\lambda v.w, x(\lambda u'v'w'.A(u'(v'),w'))), x(f))$

with $\tau(u) = \tau(f) = ((\gamma \rightarrow \gamma), \gamma, \gamma \rightarrow \gamma)$, $\tau(x) = (((\gamma \rightarrow \gamma), \gamma, \gamma \rightarrow \gamma) \rightarrow \gamma)$,

$\tau(u') = (\gamma \rightarrow \gamma), \tau(v) = \tau(w) = \tau(v') = \tau(w') = \gamma, \tau(A) = (\gamma, \gamma \rightarrow \gamma)),$

taking $\sigma = \{<x, \lambda u.u(\lambda v.w, A(w,y),y)>,<f, \lambda u.v'w'.y>\}$ with $\tau(y) = \gamma$.
Let us call rigid path for x in e a sequence of terms :

$$e = e_1, e_2, \dots, e_n, e_{n+1} \quad n \ge 0 \quad \text{such that :}$$

$$ \left\{ \begin{array}{l} - e_{i+1} \text{ is an argument of } e_i, \quad 1 \le i \le n \\ - \text{the head of } e_i \text{ is a constant or a variable in the binder of} \\ \quad \text{some } e_j, \quad 1 \le j \le i \le n. \\ - \text{the head of } e_{n+1} \text{ is a free occurrence of } x. \end{array} \right. $$

We are able to generalize lemma 5 into :

### Lemma 6.

If there exists no rigid path for x in e, then e and x are unifiable.

Its converse is false, as shown by the previous examples. We can conclude partially in two special cases, given by the next two lemmas, which are easy to establish.

### Lemma 7.

If e has a null binder and there exists a rigid path for x in e, then e and x are not unifiable.

### Lemma 8.

If there exists a rigid path for x in e : $e_1, e_2, \dots, e_{n+1}$ such that $e_{n+1}$ has no arguments, then e and x are not unifiable.

Lemmas 7 and 8 can be used to recognize TFNs. Lemma 6 is not of much use, unless we are in a node with a single pair $<x,e>$, and in this case we would get a TSN at a finite distance anyway.

Remark that this problem is the problem of finding a fixpoint to some instance of $\lambda x.e$.
5.2/ We have not assumed so far the η-rule of λ-calculus : λx.e(x) = e where e does not contain free occurrences of x.

To imbed this rule in our algorithm, we would have to make the
following changes.

1. η-normal form. The η-normal form of a term is obtained from its normal form by replacing every subterm

$$
\lambda u_1 \dots u_n . \dot{\alpha}(e_1, \dots, e_p)
$$

where $\tau(\dot{\alpha}) = (\alpha_1, \alpha_2, \dots, \alpha_n, \dots, \alpha_m \to \beta)$ $m \ge n$

by a term : $\lambda u_1 \dots u_n w_1 \dots w_{m-n} \cdot \dot{\alpha}(e_1, \dots, e_p, w_1, \dots, w_{m-n})$

where the wᵢ's are new variables of the appropriate type.

2. Change <u>Match</u> as follows.

- in 3.3.1.1.2 consider only k = p₁

- suppress 3.3.1.2.1

- in 3.3.1.2.2 consider only k = n.

The justification 's obvious : the suppressed solutions have
η-normal forms which are instances of the ones of the solutions kept.
This allows us to consider only 1 case of imitation and p₁ cases of
projections, as opposed to the previous p₁ (p₁ + 2n+1)/2 cases.

5.3/

It is interesting to wonder whether our algorithm could be used to
generate a complete set of unifiers of e₀ and e'₀, by searching all
TSNs in a matching tree. First, we need to make a supplementary res-
triction to the "new variables" hᵢ of <u>Match</u>. The third argument given
to <u>Match</u> should be the set of all variables free not only in the current
node, but also in all nodes on the path from the initial node to the
current node. This is to avoid constructions of branches such as :

$$
\langle f(x, y), A(B) \rangle \stackrel{\langle f, \lambda uv.u \rangle}{\longrightarrow} \{ \langle x, A(B) \rangle \} \stackrel{\langle x, A(y) \rangle}{\longrightarrow} \{ \langle y, B \rangle \} \stackrel{\langle y, B \rangle}{\longrightarrow} \text{TSN}.
$$

With this convention, we can prove a stronger statement for the
completeness : if e₀ and e'₀ are unifiable by substitution ρ, then in
any matching tree for e₀ and e'₀ there exists a finite branch
<figure><img src="image_4.png" /></figure>

such that $N_p$ is a TSN and $\rho = \xi_p \circ \sigma_p \circ \dots \circ \sigma_1$, where V does not contain any variable free in $e_o$ or $e'_o$.

Still, this does not give us in the general case a way of computing all $\xi_p$'s unifying a given TSN. Actually these TSNs represent the most difficult cases to treat for general unification, and we would need here supplementary rules similar to Pietrzykowski's elimination and iteration. This fact is rather satisfying, since it shows that our algorithm is taking great advantage of the fact that we are looking only for the existence of unifiers.

### 5.4/

A very useful heuristic to incorporate in the unification process would be to suppress branches which lead to infinite repeating cycles. That is, if a branch $N_o \to N_1 \to \dots \to N_p$ is such that for some $n < p$ $N_n$ is identical to $N_p$ up to a 1-1 renaming of their free variables, then $N_p$ can be safely replaced by a TFN.

For instance, consider the following matching tree, with

$$ \tau(A) = \gamma, \quad \tau(f) = \tau(F) = (\gamma \to \gamma): $$

<figure><img src="image_5.png" /></figure>

We can recognize the starred node as being identical with the initial one, up to renaming of $f$ by $g$. We can replace it by a TFN, and we get a finite (failure) tree.

Note that replacing $N_p$ by a TFN does not mean here that $N_p$ is not unifable; but merely that if it possesses a TSN descendant, then $N_n$ possesses one too at a lower level on some other branch.

This heuristic will not avoid other kinds of sterile infinite branches. Consider for instance $e_o = f(f(A)), e'_o = F(f(f(A)))$;
actually one cannot hope to be able to recognize all cases, since unification is undecidable in logic of order 3 or more. If we restrict our language to order 2 the result is not known. Let us just indicate that in the monadic case the problem reduces to finding a solution to a system of equations in a free monoid, which problem we conjecture to be solvable.

## 6 - EXAMPLES

Let us now give a few examples of matching trees.

### 6.1 / Ex. 1

$$e_o = f(f(x))$$

$$e'_o = A(A(B))$$

with $τ(x) = τ(B) = γ$ , $τ(f) = τ(A) = (γ → γ)$ .

Notation for terms : implicit association to the right.

<figure><img src="image_6.png" /></figure>
In this case there is a unique matching tree (only one pair in each node) and it is finite. Compare this example with its analogue in Pietrzykowski (1971).

## 6.2/ Ex. 2

$$e_0 = A(y, x(B))$$

$$e'_0 = A(x(\lambda u.y), B(y))$$

with $\tau(y) = \tau(u) = \gamma$, $\tau(B) = (\gamma \to \gamma)$, $\tau(x) = ((\gamma \to \gamma) \to \gamma)$, $\tau(A) = (\gamma, \gamma \to \gamma)$.

Here we have a unique infinite matching tree, which possesses a unique TSN at level 1 :

<figure><img src="image_7.png" /></figure>

Note that the TSN is obtained from *Simplify* applied to {$<h(B), y>$}.

Note also that, in the nodes with two pairs, only one of these pairs is flexible-rigid, but which pair it is keeps alternating from one node to the next.

Here lemma 7 could be used to transform the starred node into a TFN.
6.3/ Ex. 3

Let us show how we can find a unifier for the example considered
in 5.1 :

$e_o = x$

$$
e'_{o} = \lambda u.u(\lambda v.w, x(e), x(f))
$$

with e = λu' v' w'.A(u'(v'),w'), types as given above. We shall just
give the successful branch of a matching tree.

<figure><img src="image_8.png" /></figure>

which is a TSN ! (actually, <u, v, w> would return Ø at this step).

Using the method of lemma 3 to get a unifier, we obtain :

$$
\sigma = \{ \langle x, \lambda u.u(\lambda v.z, A(z,z), z) \rangle, \langle f, \lambda u.v'w'.z \rangle, \langle w, z \rangle \}
$$

and $\sigma_o e = \sigma_o x = \lambda u.u(\lambda v.z, A(z,z), z)$.

This example exhibits a very good convergence. It demonstrates
that the new variables introduced by <u, v, w> (the h_i's) do not complicate
the unification process, since they are never considered in "don't care"
situations.
CONCLUSION

We have presented in this paper an algorithm which searches for the existence of unifiers of sets of formulas in w-order typed λ-calculus.

This algorithm demonstrates very good convergence properties. This is due to the fact that we perform only substitutions which are absolutely mandatory, when we match two terms one of which is rigid.

This condition gives us a good directionality, since the heading of the rigid term is used as a handle on the unification process. We never search in "don't care" situations because our algorithm, in contrast with existing ones, does not examine the formulas in a left to right fashion. Finally situations which can be described as "don't care in all positions" are recognized as successes (TSNs). This permits us to ignore the most complicated cases of unification (the flexible-flexible pairs) and to get rid of the rules of elimination and iteration; this last rule is very prolific, since it is not directional.

This work represents a first step towards reasonably efficient proof procedures for higher-order logic. Such a system, using our unification algorithm, is currently being implemented at IRIA, for experimental purposes.
B I B L I O G R A P H Y

[ 1 ]
Andrews P.B. (1971)
Resolution in type theory.
Journal of Symbolic Logic 36,3 pp. 414-432.

[ 2 ]
Church A. (1940)
A formulation of the simple theory of types.
Journal of Symbolic Logic 5,1 pp. 56-68

[ 3 ]
Darlington J.L. (1971)
A partial mechanization of second-order logic.
Machine Intelligence 6, pp. 91-100
American Elsevier, New York.

[ 4 ]
Darlington J.L. (1973)
Automatic program synthesis in second-order logic.
Proceedings of 3rd 1 J C A I, Stanford August 73.

[ 5 ]
Ernst G.W. (1971)
A matching procedure for type theory.
Computing & Information Sciences Dept.,
Case Western Reserve University.

[ 6 ]
Gould W.E. (1966)
A matching procedure for w-order logic.
Scientific Report n°4, A F C R L 66-781
Contact AF 19 (628) - 3250
AD 646 560

[ 7 ]
Guard J.R. (1964)
Automated logic for semi-automated mathematics.
Scientific Report n°1, A F C R L 64-411
Contract AF 19 (628) - 3250
AD 602 710
[8] Huet G.P. (1972)
Constrained resolution : a complete method for type theory.
Jennings Computing Center report 1117,
Case Western Reserve University.

[9] Huet G.P. (1973 a)
The undecidability of unification in third order logic.
Information and Control 22,3 pp. 257-267.

[10] Huet G.P. (1973 b)
A mechanization of type theory.
Rapport de recherche n° 9,
I R I A - Laboria.
Also Proceedings of 3rd I J C A I, Stanford August 73.

[11] Lucchesi C.L. (1972)
The undecidability of the unification problem for third order
languages.
Report C S R R 2059, Dept of Applied Analysis and Computer
Science, University of Waterloo.

[12] Pietrzykowski T. (1971)
A complete mechanization of second order logic.
Report C S R R 2038, Dept of Applied Analysis and Computer
Science,
University of Waterloo.
Also Journal of Assoc. for Comp. Mach. 20,2 pp. 333-364.

[13] Pietrzykowski T. and Jensen D. (1972)
A complete mechanization of ω-order type theory.
Association for Computing Machinery National Conference
1972, vol. 1, pp. 82-92.

[14] Robinson G.A. and Wos L.T. (1969)
Paramodulation and theorem proving in first-order theories
with equality.
Machine Intelligence 4, pp. 135-150.
American Elsevier, New York.

[15] Robinson J.A. (1965)
A machine-oriented logic based on the resolution principle.
Journal of Assoc. for Comp. Mach. 12,1 pp. 23-41.