Unification and Matching in Church’s Original Lambda Calculus

Ullrich Hustadt

MPI–I–92–219 June 1992 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

In current implementations of higher-order logics higher-order unification is used to lift the resolution principle from the first-order case to the higher-order case. Higher-order matching is the core of implementations of higher-order rewriting systems and some systems for program transformation.

In this paper I argue that Church’s original lambda calculus, called non-forgetful lambda calculus, is an appropriate basis for higher-order matching. I provide two correct and complete algorithms for unification in the non-forgetful lambda calculus. Finally, I show how these unification algorithms can be used for matching in the nonforgetful lambda calculus.

Keywords

Non-forgetful lambda-calculus, Permissive unification algorithm, Lawful unification algorithm, Higherorder matching

1 Introduction

In first-order term algebra we interpret a term M containing variables as the set of all ground instances σ(M) of M.

Example 1.1 Given the following signature Σ_{1}

sorts  T_{1}, T_{2}, T_{3}
constants a_{1}, a_{2} : T_{1}
constants b_{1}, b_{2} : T_{2}
constant  f : (T_{1} × T_{2} → T_{3})
variable  X : T_{1}
variable  Y : T_{2}

the term f(X, b_{1}) can be interpreted as the set {f(a_{1}, b_{1}), f(a_{2}, b_{1})}.

If we consider higher-order term algebras now, the interpretation of a term M to be the set of all ground instances of M, which we want to denote GI(M), gives surprising results.

Example 1.2 Suppose F is a variable of type (T_{1} × T_{2} → T_{3}) in signature Σ_{1}. Then F (X, Y) can be interpreted as the set of all terms of type T_{3}, i.e.

GI(F (X, Y)) = {f(a_{1}, b_{1}), f(a_{2}, b_{1}), f(a_{1}, b_{2}), f(a_{2}, b_{2})}.

On the other hand, F (X, b_{1}) has the same interpretation

GI(F (X, b_{1})) = {f(a_{1}, b_{1}), f(a_{2}, b_{1}), f(a_{1}, b_{2}), f(a_{2}, b_{2})}.

So there is no difference between GI(F (X, b_{1})) and GI(F (X, Y)), although intuitively F (X, b_{1}) is more specific than F (X, Y).

We want to interpret a term f(T_{1}, …, T_{m}) as the set of all ground instances σ(f(T_{1}, …, T_{m})), where the terms σ(T_{1}), …, σ(T_{m}) actually occur in σ(f(T_{1}, …, T_{m})). We will denote this set by RGI(M) for a term M. This results in a simple restriction to the allowed substitutions σ: If σ(X) = λ \overline{x_{n}: T_{n}}. N for some variable X, then all the variables in the binder must occur in the matrix N, i.e. x_{i} ∈ FV(N) for all i, 1 ≤ i ≤ n. So RGI(F (X, b_{1})) = {f(a_{1}, b_{1}), f(a_{2}, b_{1})}, for example.

This change of interpretation has impacts on our understanding of unification and matching substitutions. On the other hand, it is not possible to restrict the set of all substitutions to obey the restriction if we want to use some standard algorithm for unification and matching.

Example 1.3 Given the following signature

sort  T
constants a, b :
constant  f : (T → (T → T))
variable  F : (T → (T → T)),

we consider the unification problem U_{1} = {F (a, b) =^{?} f(a, g(a, b))}. Using the transformation system for higher-order unification given in Snyder and Gallier (1989), we have the following transformation sequences

\begin{matrix}\{F (a, b) =^{?} f(a, g(a, b))\} \\ \{f(H_{1}(a, b), H_{2}(a, b)) =^{?} f(a, g(a, b))\} \end{matrix}

Imitation rule using ρ_{1}={F/λ x_{1},x_{2}. f(H_{1}(x_{1},x_{2}),(H_{2}(x_{1},x_{2})))}

Decomposition rule

\begin{matrix}\{H_{1}(a, b) =^{?} a, H_{2}(a, b) =^{?} g(a, b)\} \\ \{a =^{?} a, H_{2}(a, b) =^{?} g(a, b)\} \\ \{H_{2}(a, b) =^{?} g(a, b)\} \\ \{g(K_{1}(a, b), K_{2}(a, b)) =^{?} g(a, b)\} \\ \{K_{1}(a, b) =^{?} a, K_{2}(a, b) =^{?} b\} \\ \{a =^{?} a, K_{2}(a, b) =^{?} b\} \\ \{K_{2}(a, b) =^{?} b\} \\ \{b =^{?} b\} \\ \{\} \end{matrix}

Imitation rule using σ_{1}={H_{1}/λ y_{1},y_{2}. a}

[figure]

Projection rule using σ_{2}={H_{1}/λ y_{1},y_{2}. y_{1}}

[figure]

Trivial removal

[figure]

Imitation rule using

τ_{1}={H_{2}/λ z_{1},z_{2}. g(K_{1}(z_{1},z_{2}),K_{2}(z_{1},z_{2}))}

[figure]

Decomposition rule

[figure]

Imitation rule using ϕ_{1}={K_{1}/λ y_{1},y_{2}. a}

[figure]

Projection rule using ϕ_{2}={K_{1}/λ y_{1},y_{2}. y_{1}}

[figure]

Trivial removal

[figure]

Imitation rule using ψ_{1}={K_{2}/λ y_{1},y_{2}. b}

[figure]

Projection rule using ψ_{2}={K_{2}/λ y_{1},y_{2}. y_{2}}

[figure]

Trivial removal

[figure] The set of all unifiers of U_{1} is

{ψ_{i} ∘ ϕ_{j} ∘ τ_{1} ∘ σ_{k} ∘ ρ_{1} | 1 ≤ i ≤ 2 ∧ 1 ≤ j ≤ 2 ∧ 1 ≤ k ≤ 2} =
{{F/λ x_{1}, x_{2}. f(x_{1}, g(x_{1}, x_{2}))}, {F/λ x_{1}, x_{2}. f(x_{1}, g(x_{1}, b))}, {F/λ x_{1}, x_{2}. f(x_{1}, g(a, x_{2}))},
{F/λ x_{1}, x_{2}. f(x_{1}, g(a, b))}, {F/λ x_{1}, x_{2}. f(a, g(x_{1}, x_{2}))}, {F/λ x_{1}, x_{2}. f(a, g(x_{1}, b))},
{F/λ x_{1}, x_{2}. f(a, g(a, x_{2}))}, {F/λ x_{1}, x_{2}. f(a, g(a, b))}}

The set of those unifiers obeying our restriction is

\begin{matrix}\{ψ_{2} ∘ ϕ_{2} ∘ τ_{1} ∘ σ_{2} ∘ ρ_{1}, ψ_{2} ∘ ϕ_{1} ∘ τ_{1} ∘ σ_{2} ∘ ρ_{1}, ψ_{2} ∘ ϕ_{2} ∘ τ_{1} ∘ σ_{1} ∘ ρ_{1},\} = \\ \{ & \{F/λ x_{1}, x_{2}. f(x_{1}, g(x_{1}, x_{2}))\}, \{F/λ x_{1}, x_{2}. f(x_{1}, g(a, x_{2}))\}, \{F/λ x_{1}, x_{2}. f(a, g(x_{1}, x_{2}))\}\} \end{matrix}

It is easy to see that neither σ_{1}, σ_{2}, ϕ_{1}, ϕ_{2}, ψ_{1} nor ψ_{2} obeys the restriction, only the appropriate compositions do.

In the following sections we will show that our restriction is necessary and sufficient to solve the problem. We will give a correct and complete transformation system for this context.

2 Non-forgetful Lambda-Calculus

Definition 2.1 (Non-forgetful Terms) Given a set T_{0} of base types we define the set of types T inductively as the smallest set containing T_{0} and if S, T ∈ T then (S → T) ∈ T .

The set RL^{→}(V, Σ) of raw terms is defined by the following abstract syntax

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

where V is a set of variables and Σ a set of constants. We suppose V, Σ, and T_{0} to be pairwise disjoint. The set L^{→}(V, Σ) ⊆ RL^{→}(V, Σ) of well-typed terms is defined using 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 ∈ Σ ∧ 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^{→}(V,Σ) is the set of all M ∈ RL^{→}(V, Σ) such that ϵ ⊢ M:T can be deduced for some T ∈ T . The function type : L^{→} → T is defined as type(M) = T ⟺ ϵ ⊢ M:T.

We simply write L^{→} if V and Σ are obvious from the context.

The set of all free variables is FV. With a set Z of free variables we associate the set symbols(Z) ⊆ V of all variables occurring in Z. The set of free variables of a term M with respect to V is FV_{V}(M). The set of bound variables of a term M with respect to V is BV_{V}(M). If the set of variables V is obvious from the context we write FV(M) or BV (M) for simplicity. △

Church (1941) defines a λ-term M to be well-formed iff • M is either a constant or a variable,

• M is an application of the form (M_{1} · M_{2}) and M_{1} and M_{2} are well-formed,

• M is an abstraction of the form λ x: T. M_{1} such that M_{1} is well-formed and contains at least an occurrence of x in the scope of this binder.

We will use the phrase non-forgetful for these terms instead. The set of all such terms is L\overrightarrow{nf}. The terms in L^{→} \ L\overrightarrow{nf} are called forgetful.

The set of all free variables of a term M is FV(M). The rules of lambda conversion are defined as usual. It is important to note that the set of non-forgetful λ-terms is closed under α-, β-, and η-conversion. The β-normal form of a term M is denoted M ↓, its η-expanded form is denoted η[M]. The set of all terms in η-expanded form is L\overrightarrow{η}.

Definition 2.2 (Substitution) A substitution σ in L^{→} is a mapping σ : V → L^{→} such that the domain of σ, defined DOM(σ) = {x ∈ V | σ(x) ≠ x}, is finite. The identity substitution is denoted ι. The set of all substitutions in L^{→} is denoted SUB(L^{→}^{V}).

The domain of a substitution σ is

DOM(σ) = {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.

Any substitution σ can be uniquely extended to a mapping σ̂ : L^{→} → L^{→}. The composition of two substitutions σ and τ is written τ ∘ σ and defined τ ∘ σ(x) = τ̂(σ(x)) for all x ∈ V. The union of σ and τ, denoted σ ∪ τ, is defined by

σ ∪ τ(x) = \begin{cases}σ(x), & if x ∈ DOM(σ) \\ τ(x), & if x ∈ DOM(τ) \\ x, & otherwise \end{cases}

The set of non-forgetful substitutions SUB(L\overrightarrow{nf}^{V}) is the set of all substitutions σ : V → L\overrightarrow{nf}. This set is closed under composition and union of substitutions. The substitutions in SUB(L^{→}^{V}) \ SUB(L\overrightarrow{nf}^{V}) are called forgetful.

The restriction σ_{V} of a substitution σ and the equality σ = τ [V] of two substitutions σ and τ over a set of variables V is defined in the usual way. △

Lemma 2.3 Let σ be a forgetful substitution and τ some arbitrary substitution. Then the composition τ ∘ σ is again a forgetful substitution.

3 Unification Problems in Lambda-Calculus

We use the following representation of unification problems.

Definition 3.1 (Unification problems in L^{→}) An equation in L^{→} is a multiset of terms M and N in L\overrightarrow{η} of the same type. We will use the notation M =^{?} N for equations. A system D in L^{→} is a multiset of equations in L^{→}. A unification problem in L^{→} is an ordered pair ⟨D, V ⟩, written ⟨D | V ⟩, such that D is a system and V is a set of variables. △ For a system

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

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

Definition 3.2 (Unifier) Let SUB be a set of substitutions. A substitution θ in SUB is called unifier in SUB of two terms M and N from L\overrightarrow{η} iff θ(M) ⟷^{∗}_{βη} θ(N) holds.

A substitution θ in SUB is a unifier of a unification problem ⟨D | V ⟩ in SUB iff θ_{V} is a unifier for every equation in D.

If SUB is the set of all normalized substitutions in SUB(L^{→}^{V}) then the set of all unifiers of a unification problem U is denoted SU(U). If SUB is the set of all normalized substitutions in SUB(L\overrightarrow{nf}^{V}) then a unifier is called non-forgetful and the set of all non-forgetful unifier of U is written SU_{nf}(U). △

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

(1) CSU(U)[Z] ⊆ SU(U) ⊆ SUB

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

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

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

Again if SUB is the set of all normalized substitutions in SUB(L^{→}^{V}) then a complete set of all unifiers of a unification problem U is denoted CSU(U). If SUB is the set of all normalized substitutions in SUB(L\overrightarrow{nf}^{V}) then a complete set of all non-forgetful unifier of U is written CSU_{nf}(U). △

Definition 3.4 (Solved Form) An equation is in solved form in a unification problem U if it is in the form η[F] =^{?} N, for some variable F which occurs only once in U, and F and N have the same type. A system D is solved if each of its pairs is solved. A unification problem ⟨D | V ⟩ is solved if D is solved.

To a system S = {F_{1} =^{?} N_{1}, …, F_{n} =^{?} N_{n}} in solved form we associate a substitution

⌈S⌉^{SUB} = {F_{1}/N_{1}, …, F_{n}/N_{n}}.

This substitution is unique up to variable renaming. To a unification problem ⟨D | V ⟩ in solved form we associate a system

⟨D | V ⟩_{VAR} = {F =^{?} N | F =^{?} N ∈ D ∧ F ∈ V }.

Then we can associate to a unification problem U in solved form the substitution ⌈U⌉^{SUB} = ⌈U_{VAR}⌉^{SUB}. △

Lemma 3.5 If

U = ⟨{F_{1} =^{?} N_{1}, …, F_{n} =^{?} N_{n}} | V ⟩

is a unification problem in solved form and {F_{1}, …, F_{n}} ⊆ V, then {⌈U⌉^{SUB}} is a CSU_{nf}(U)[W] for any W

such that W ∩ FV(F_{1} =^{?} N_{1}, …, F_{n} =^{?} N_{n}) = ∅.

Proof: ⌈U⌉^{SUB} is obviously a unifier of U, so {⌈U⌉^{SUB}} ⊆ SU(U). If θ ∈ SU(U) then θ =_{β} θ ∘ ⌈U⌉^{SUB}, since θ(F_{i}) ⟷^{∗}_{β} θ(N_{i}) = θ(⌈U⌉^{SUB}(F_{i})) for 1 ≤ i ≤ n, and θ(x) = θ(⌈U⌉^{SUB}(x)) otherwise. So ⌈U⌉^{SUB} ≤_{β} θ and ⌈U⌉^{SUB} ≤_{β} θ [FV(U)]. Because DOM(⌈U⌉^{SUB}) = {F_{1}, …, F_{n}} ⊆ FV(U) and ⌈U⌉^{SUB} is idempotent the third condition is also fulfilled.

4 The Permissive Unification Algorithm

Snyder and Gallier (1989) give a correct and complete transformation system HU for unification in L^{→}. Our first approach to the problem of unification in L\overrightarrow{nf} will be a slight modification of their transformation system.

The central notion for both transformation systems is the partial binding.

Definition 4.1 (Partial binding) A partial binding of type (\overline{A_{n}} → A_{0}) is a term of the form

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

for some atom a of type (\overline{B_{m}} → A_{0}) and free variables H_{i} of type (\overline{A_{n}}, \overline{B_{p_{i}}} → B_{i}) for all i, 1 ≤ i ≤ m.

If a is a constant or a free variable, the partial binding is called an imitation binding. If a is a bound variable x_{i} for some i, 1 ≤ i ≤ n, then it is called an ith projection binding.

For a variable F, a partial binding M is appropriate to F if type(F) = type(M). △

The transformation system uses sequences of partial bindings to construct unifiers. Partial bindings allow to substitute a term for a free variable that is as much undetermined as possible and at least as determined as needed. We are using the fact that for any term M there exists a partial binding P and a substitution σ such that σ(P) ⟶^{∗}_{β} M. But this wouldn’t be true if σ has to be a non-forgetful substitution.

Example 4.2 Consider the term

M_{1} = λ x_{1}: A_{1}. f(a)

where f is a constant of type ((A_{1} → A_{1}) → A_{1}) and a is a constant of type (A_{1} → A_{1}). An appropriate partial binding is

P_{1} = λ x_{1}: A_{1}. f(λ z_{1}: A_{1}. H_{1}(x_{1}, z_{1}))

where H_{1} is a free variable of type (A_{1}, A_{1} → A_{1}). It is not possible to find a non-forgetful substitution σ such that σ(P_{1}) = M_{1}. This substitution has to satisfy σ(λ z_{1}: A_{1}. H_{1}(x_{1}, z_{1})) =_{βη} a, where . The reason is that the variable x_{1} has to occur in σ(λ z_{1}: A_{1}. H_{1}(x_{1}, z_{1})), but it doesn’t occur in a.

But the H_{i} are only auxiliary variables we are using to construct a instantiation for a free variable F in the original unification problem we consider. So it doesn’t matter that we instantiate H_{i} with a forgetful term as long as the instantiation for F is non-forgetful.

For this reason we augment the system of equation D we want to unify with the set of free variables in it. Now we can distinguish the variables which must be instantiated with non-forgetful terms from those which can be instantiated with arbitrary terms. In every step in the transformation sequence we will ensure that this restriction is obeyed. A unification problem ⟨D | V ⟩ such that the restriction of any unifier σ of ⟨D | V ⟩ to V is forgetful is called a forgetful unification problem. Otherwise it is called non-forgetful.

We define a predicate on unification problems which distinguishes non-forgetful unification problems from obviously forgetful ones.

Definition 4.3 ((Non-)Forgetful unification problems) An equation F =^{?} M is forgetful with respect to V if F is an element of the set of variables V, F does not occur in the free variables of M, and M is a forgetful term. Otherwise an equation is called possibly non-forgetful with respect to V. A unification problem ⟨D | V ⟩ is forgetful if some equation M =^{?} N in D is forgetful with respect to V. Otherwise it is possibly non-forgetful. A solved unification problem that is possibly non-forgetful is called non-forgetful. △

Lemma 4.4 If U_{1} is non-forgetful, i.e. it is solved and possibly non-forgetful, then ⌈U_{1}⌉^{SUB} is a non-forgetful substitution.

Proof: Because U_{1} is solved it has the form

⟨F_{1} =^{?} M_{1}, …, F_{m} =^{?} M_{m} | V ⟩,

for some free variables F_{1},…, F_{m} and some terms M_{1},…, M_{m}. Because U_{1} is possibly non-forgetful there is no equation F_{i} =^{?} M_{i}, 1 ≤ i ≤ m, such that M_{i} is a forgetful term. Without restriction of generality we can assume that V = {F_{1}, …, F_{n}} for some n, 0 ≤ n ≤ m. Then ⌈U_{n}⌉^{SUB} is

{F_{1}/M_{1}, …, F_{n}/M_{n}}

and this substitution is non-forgetful.

Definition 4.5 (Transformation system HU) The following rules form the transformation system on unification problems given by Snyder and Gallier (1989). Trivial removal

⟨{M =^{?} M} ∪ D | V ⟩ ⇒ ⟨D | V ⟩  HU_{1}

Decomposition

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{m}})\} ∪ D | V ⟩ \\ ⇓ \\ ⟨∪_{1≤i≤m}\{λ \overline{x_{k}: T_{k}}. M_{i} =^{?} λ \overline{x_{k}: T_{k}}. N_{i}\} ∪ D | V ⟩, \end{matrix}  HU_{2}

where a is an arbitrary atom. Variable elimination

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ D | V ⟩ \\ ⇓ \\ ⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ θ(D)↓ | V ⟩, \end{matrix}  HU_{3}

where

• F is a variable, and

• F ∉ FV(λ \overline{x_{k}: T_{k}}. N) and F ∈ FV(D)m

• θ = \{F/λ \overline{x_{k}: T_{k}}. N\}.

Imitation

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ D | V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ \{F/P \}(D)↓ | V ⟩, \end{matrix}  HU_{4a}

where

• F is a free variable and a is either a constant or a free variable not equal to F, and

• P is a variant of a imitation binding appropriate to F e.g. P = λ \overline{y_{m}: S_{m}}. a(\overline{λ \overline{z_{p_{n}}: R_{p_{n}}}. H_{n}(\overline{y_{m}}, \overline{z_{p_{n}}})}).

Projection

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ D | V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ \{F/P \}(D)↓ | V ⟩, \end{matrix}  HU_{4b}

where

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

• P is a variant of a ith projection binding for 1 ≤ i ≤ m, appropriate to the free variable F, 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.

Explosion

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. G(\overline{N_{n}})\} ∪ D | V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. G(\overline{N_{n}})\} ∪ \{F/P \}(D)↓ | V ⟩, \end{matrix}  HU_{4c}

where

• F and G are free variables and

• P = λ \overline{y_{m}: S_{m}}. a(\overline{λ \overline{z_{p_{n}}: R_{p_{n}}}. H_{n}(\overline{y_{m}}, \overline{z_{p_{n}}})}) is a variant of some arbitrary partial binding appropriate to the term λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) such that a ≠ F and a ≠ G.

△

Definition 4.6 (Transformation system PU) We obtain the transformation system PU by adding the restriction that U_{1} ⟹_{PU} U_{2} iff U_{1} ⟹_{HU} U_{2} and U_{2} is possibly non-forgetful. △

4.1 Correctness and Completeness of PU

Theorem 4.7 (Correctness) If U = ⟨D | FV(D)⟩ ⟹^{∗}_{PU} U′, with U′ in solved form and possibly nonforgetful, then the substitution ⌈U′⌉^{SUB} is a non-forgetful unifier of U.

Proof: Snyder and Gallier (1989) have shown that HU is correct, i.e. if U′ = ⟨D′ | V ⟩, where V = FV(D), and U ⟹^{∗}_{HU} U′ then ⌈D⌉^{SUB} ∈ SU(D). Because for any transformation step U_{1} ⟹_{PU} U_{2} there exists a transformation step U_{1} ⟹_{HU} U_{2} we can conclude that ⌈U′⌉^{SUB} ∈ SU(U).

Now if ⟨D′ | V ⟩ is solved and possibly non-forgetful then any equation in D′ has the form F =^{?} M, where F is a variable, F does not occur anywhere else in D′, and M is a non-forgetful term if F is in V. So ⌈U′⌉^{SUB} is non-forgetful.

Lemma 4.8 If M = λ \overline{x_{n}: T_{n}}. N is a forgetful term then exists no substitution σ such that σ(M)↓ is a non-forgetful term.

Proof: Because M is forgetful some bound variable, let’s assume it is x_{i}, for some i, 1 ≤ i ≤ n, does not occur in N. The substitution σ instantiates free variables with some λ-terms but applied to M it could never happen that the instantiation results in a new occurrence of the bound variable x_{i}. So x_{i} does not occur free in the matrix of σ(M) or its normal form.

Lemma 4.9 If U_{1} is a forgetful unification problem then there exists no transformation U_{1} ⟹_{HU} U_{2} such that U_{2} is possibly non-forgetful.

Proof: We consider each transformation rule in turn:

Trivial removal Trivial equations are non-forgetful, so the removal of a trivial equation doesn’t change

forgetfulness. Decomposition If either term in the decomposed equation is forgetful, it’s decomposition will be forgetful

too. Variable elemination If the equation F =^{?} λ \overline{x_{k}: T_{k}}. N is forgetful, the resulting unification problem is

forgetful because this equation is preserved. If some equation in D is forgetful then θ(D)↓ will be forgetful because of lemma 4.8.

Imitation If the equation λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}}) is forgetful then the resulting unification problem is forgetful because this equation is preserved. If some equation in D is forgetful then θ(D)↓ will be forgetful because of lemma 4.8.

Projection The same argumentation as for the imitation rule holds. Explosion If the equation λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. G(\overline{N_{n}}) is forgetful then the resulting unification

problem is forgetful because this equation is preserved. If some equation in D is forgetful then θ(D)↓ will be forgetful because of lemma 4.8.

Lemma 4.10 If U_{1} is a unification problem then in any transformation sequence

U_{1} ⟹_{HU} U_{2} ⟹_{HU} ⋯ ⟹_{HU} U_{n}

such that U_{n} is in solved form and ⌈U_{n}⌉^{SUB} is a non-forgetful substitution each U_{i} is possibly non-forgetful for 1 ≤ i ≤ n.

Proof: We will first show that U_{n} is possibly non-forgetful: Assume that U_{n} is forgetful. Then U_{n} has the form U_{n} = ⟨{F_{1} =^{?} M_{1}, …, F_{m} =^{?} M_{m}} | V ⟩ and there is an equation F_{i} =^{?} M_{i} for some i, 1 ≤ i ≤ m, such that F_{i} ∈ V and M_{i} is a forgetful term. But then ⌈U_{n}⌉^{SUB}(F_{i}) = M_{i} implies that ⌈U_{n}⌉^{SUB} is a forgetful substitution in contradiction to our assumption. So U_{n} must be non-forgetful.

If U_{i+1} is possibly non-forgetful then U_{i} must be possibly non-forgetful for all i, 1 ≤ i ≤ n − 1. Assume again the contrary, i.e. that U_{i} is forgetful. Then following lemma 4.9 there could be no transformation U_{i} ⟹_{HU} U_{i+1} such that U_{i+1} is non-forgetful.

So we can conclude that each U_{i} in the transformation sequence is possibly non-forgetful.

Theorem 4.11 (Completeness of PU) Let U = ⟨D | FV(D)⟩ be a unification problem. If θ ∈ SU_{nf}(U), then there exists a sequence of transformations

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

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

Proof: From the completeness HU we know that for θ ∈ SU_{nf}(U), there exists a sequence of transformations

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

where U_{n} is in solved form and ⌈U_{n}⌉^{SUB} ≤_{β} θ [FV(U)],i.e. there exists a substitution σ such that σ ∘ ⌈U_{n}⌉^{SUB} =_{β} θ [FV(U)]. Because θ is non-forgetful and following lemma 2.3 ⌈U_{n}⌉^{SUB} must be non-forgetful too. From lemma 4.10 we know that each U_{i}, 1 ≤ i ≤ n, must be possibly non-forgetful. So there exists a transformation sequence

U = U_{0} ⟹_{PU} U_{1} ⟹_{PU} U_{2} ⟹_{PU} ⋯ ⟹_{PU} U_{n}.

5 The Lawful Unification Algorithm

If we want to use non-forgetful substitutions only, we have to modify the notion of partial bindings. Consider again the general form of a partial binding, i.e.

P_{1} = λ \overline{x_{n}: A_{n}}. a(\overline{λ \overline{y_{p_{m}}: B_{p_{m}}}. H_{m}(\overline{x_{n}}, \overline{y_{p_{m}}})}).

Let’s assume that this partial binding is used in a transformation sequence resulting in a unifier σ. Let σ(λ \overline{y_{p_{j}}: B_{p_{j}}}. H_{j}(\overline{x_{n}}, \overline{y_{p_{j}}})) = M_{j} and let \{x_{k_{1,j}}, …, x_{k_{q_{j} ,j}}\}, 1 ≤ k_{1,j} < j_{2,j} < ⋯ < j_{q_{j},j} ≤ n, be the set of all x_{i} appearing in M_{j} for all j, 1 ≤ j ≤ m. Then a binding of the form

P_{2} = λ \overline{x_{n}: A_{n}}. a(\overline{λ \overline{y_{p_{m}}: B_{p_{m}}}. H_{m}(\overline{x_{k_{qm,m}}}, \overline{y_{p_{m}}})}).

could be used instead of P_{1} in a transformation sequence resulting in the unifier σ. We will prove this conjecture after we defined the notion of selective partial bindings and the presentation of the lawful transformation system.

Definition 5.1 (Selective Partial Bindings) A selective partial binding of type (\overline{A_{n}} → A_{0}) is a term of the form

λ \overline{x_{n}: A_{n}}. a(\overline{λ \overline{y_{p_{m}}: B_{p_{m}}}. H_{m}(\overline{x_{k_{qm,m}}}, \overline{y_{p_{m}}})})

for some atom a of type (\overline{B_{m}} → A_{0}) and free variables H_{j} of type (\overline{A_{j_{q_{j}}}} , \overline{B_{p_{j}}} → B_{j}) where 1 ≤ k_{1,j} < k_{2,j} < ⋯ < k_{q_{j},j} ≤ n for all j, 1 ≤ j ≤ m.

If a is a constant or a free variable, the selective partial binding is called an selective imitation binding; if a is a bound variable x_{i} for some i, 1 ≤ i ≤ n, then it is called a selective ith projection binding.

For a variable F, a selective partial binding M is appropriate to F if type(F) = type(M). △

Definition 5.2 (Transformation system LU) The following rules form the lawful unification algorithm for unification in the non-forgetful lambda-calculus Trivial removal

⟨{M =^{?} M} ∪ D, V ⟩ ⇒ ⟨D, V ⟩  LU_{1}

Decomposition

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{m}})\} ∪ D, V ⟩ \\ ⇓ \\ ⟨∪_{1≤i≤m}\{λ \overline{x_{k}: T_{k}}. M_{i} =^{?} λ \overline{x_{k}: T_{k}}. N_{i}\} ∪ D, V ⟩, \end{matrix}  LU_{2}

where a is an arbitrary atom. Variable elimination

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ D, V ⟩ \\ ⇓ \\ ⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ θ(D)↓, V ⟩, \end{matrix}  LU_{3}

where

• F is a variable,

• F ∉ FV(λ \overline{x_{k}: T_{k}}. N) and F ∈ FV(D), and

• θ = \{F/λ \overline{x_{k}: T_{k}}. N\}.

Imitation

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ D, V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ \{F/P \}(D)↓, V ⟩, \end{matrix}  LU_{4a}

where

• F is a free variable and a is either a constant or a free variable not equal to F, and

• P is a variant of a selective imitation binding appropriate to F, e.g.

P = λ \overline{y_{m}: S_{m}}. a(\overline{λ \overline{z_{p_{n}}: R_{p_{n}}}. H_{n}(\overline{y_{k_{qm,m}}}, \overline{z_{p_{n}}})}).

Projection

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ D, V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}})\} ∪ \{F/P \}(D)↓, V ⟩, \end{matrix}  LU_{4b}

falls

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

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

\begin{matrix}⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. G(\overline{N_{n}})\} ∪ D, V ⟩ \\ ⇓ \\ ⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. G(\overline{N_{n}})\} ∪ \{F/P \}(D)↓, V ⟩, \end{matrix}  LU_{4c}

where

• F and G are free variables and

• P = λ \overline{y_{m}: S_{m}}. a(\overline{λ \overline{z_{p_{n}}: R_{p_{n}}}. H_{n}(\overline{y_{k_{qm,m}}}, \overline{z_{p_{n}}})}) is a variant of some arbitrary selective partial binding appropriate to F such that a ≠ F and a ≠ G

△

5.1 Correctness and Completeness of LU

Lemma 5.3 If U ⟹ U′ using transformation rules LU_{1} or LU_{3} then SU_{nf}(U) = SU_{nf}(U′).

Proof: Snyder and Gallier (1989) show in lemma 4.12 that if D ⟹_{HU} D′ using transformations HU_{1} and HU_{3}, then SU(D) = SU(D′). Now LU_{1} and LU_{3} are exactly the same rules as HU_{1} and HU_{3}, so we conclude SU(⟨D | V ⟩) = SU(⟨D′ | V ⟩). This implies SU_{nf}(⟨D | V ⟩) = SU_{nf}(⟨D′ | V ⟩).

Theorem 5.4 (Correctness) If U = ⟨D | FV(D)⟩ is a unification problem in L^{→} and U ⟹^{∗}_{LU} U′, with U′ in solved form and non-forgetful, then the substitution ⌈U′⌉^{SUB} is a non-forgetful unifier of U.

Proof: The proof is exactly the same as for the correctness of PU.

Lemma 5.5 If M = λ \overline{x_{n}: T_{n}}. a(\overline{M_{m}}) is a non-forgetful term then there exists a variant of a selective partial binding P and a non-forgetful substitution τ such that τ(P) ⟶^{∗}_{β} M.

Proof: We distinguish the following cases:

m = 0: Then M itself is a selective partial binding. We let P = M and τ = ι. m > 0: Suppose X_{i} = BV (M_{i}) ∩ {x_{1}, …, x_{n}} = {x_{k_{1,i}}, …, x_{k_{q_{i},i}}} with 1 ≤ k_{1,i} < k_{2,i} < ⋯ < k_{q_{i},i} ≤

n. Let P_{i} = η[H_{i}(x_{k_{1,i}}, …, x_{k_{q_{i},i}})], where type(P_{i}) = type(M_{i}) and H_{i} is a free variable of appropriate type, for all i, 1 ≤ i ≤ m. Because M is a non-forgetful term, we must have ⋃_{1≤i≤m} X_{i} ∪ \{a\} = \{x_{1}, …, x_{n}\}. Therefore P = λ \overline{x_{n}: T_{n}}. a(\overline{P_{m}}) is a selective partial binding.

Let τ = \{H_{1}/λ \overline{x_{k_{q_{1},1}}}. M_{1}, …, H_{m}/λ \overline{x_{k_{qm,m}}}. M_{m}\}. τ is obviously non-forgetful and τ(P_{i}) ⟶^{∗}_{β} M_{i},

for each i, 1 ≤ i ≤ m. Thus τ(P) ⟶^{∗}_{β} M.

Lemma 5.6 If θ = {F/M}∪θ′ is a non-forgetful substitution then there exists a variant of a selective partial binding P appropriate to F and a non-forgetful substitution τ such that

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

If θ is idempotent then θ′′ = {F/M} ∪ τ ∪ θ′ is an idempotent, non-forgetful unifier of the equation F =^{?} P.

Proof: Because θ is non-forgetful, the term M must be non-forgetful and we can define P and τ as in lemma 5.5. Because P is a variant, we have DOM(τ) ∩ DOM(θ) = ∅. Therefore the first equation holds. We have already shown τ(P) ⟶^{∗}_{β} M, so

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

If θ is idempotent and DOM(τ) ∩ I(θ) = ∅ then DOM(θ′′) ∩ I(θ′′) = ∅. Finally θ′′(P) = τ(P) ⟶^{∗}_{β} θ′′(F) shows that θ′′ is a unifier of F =^{?} P.

Definition 5.7 (Transformation system LV) We define the transformation system LV on pairs of unification problems and substitutions in the following way Trivial removal

⟨⟨{M =^{?} M} ∪ D | V ⟩, θ⟩ ⇒ ⟨⟨D | V ⟩, θ⟩  LV_{1}

Decomposition

\begin{matrix}⟨⟨\{λ \overline{x_{k}: T_{k}}. a(\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{m}})\} ∪ D | V ⟩, θ⟩ \\ ⇓ \\ ⟨⟨∪_{1≤i≤m}\{λ \overline{x_{k}: T_{k}}. M_{i} =^{?} λ \overline{x_{k}: T_{k}}. N_{i}\} ∪ D | V ⟩, θ⟩, \end{matrix}  LV_{2}

where a is not a free variable in DOM(θ). Variable elimination

\begin{matrix}⟨⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ D | V ⟩, θ⟩ \\ ⇓ \\ ⟨⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{x_{k}}) =^{?} λ \overline{x_{k}: T_{k}}. N\} ∪ σ(D)↓ | V ⟩, θ⟩, \end{matrix}  LV_{3}

where • F is a variable,

• F ∉ FV(λ \overline{x_{k}: T_{k}}. N) and F ∈ FV(D), and

• σ = \{F/λ \overline{x_{k}: T_{k}}. N\}. Selective partial binding

\begin{matrix}⟨⟨\{λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. b(\overline{N_{n}})\} ∪ D | V ⟩, \{F/Q\} ∪ θ⟩ \\ ⇓ \\ ⟨⟨\{F =^{?} P , λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. b(\overline{N_{n}})\} ∪ \{F/P \}(D)↓ | V ⟩, \{F/Q\} ∪ τ ∪ θ⟩, \end{matrix}  LV_{4}

where • F is a free variable and the equation λ \overline{x_{k}: T_{k}}. F (\overline{M_{m}}) =^{?} λ \overline{x_{k}: T_{k}}. a(\overline{N_{n}}) is not solved,

• Q = λ \overline{y_{m}: S_{m}}. a(\overline{Q_{n}}),

• P is a variant of a selective partial binding appropriate to F, e.g.

P = λ \overline{y_{m}: S_{m}}. a(\overline{λ \overline{z_{p_{n}}: R_{p_{n}}}. H_{n}(\overline{y_{n_{qn}}} , \overline{z_{p_{n}}})}),

and

• τ = \{H_{1}/λ \overline{y_{m}: S_{m}}. Q_{1}, …, H_{n}/λ \overline{y_{m}: S_{m}}. Q_{n}\}.

△

Lemma 5.8 If θ ∈ SU_{nf}(U) for some unification problem U not in solved form and W is a set of variables, then there exists some transformation ⟨U, θ⟩ ⟹_{LV} ⟨U′, θ′⟩ such that

1. θ = θ′ [W];

2. If θ is idempotent then θ′ is an idempotent non-forgetful unifier of U′ and

3. U ⟹_{LU} U′.

Proof: Because U is not in solved form there exists an equation M =^{?} N, that is not solved in U. We distinguish the following three cases:

1. If M = N then we can use the transformation rule LV_{1}. If head(M) is not a free variable in DOM(θ), we can use LV_{2} too.

2. If head(M) = head(N)∉DOM(θ) then we can use LV_{2}.

3. Otherwise M ≠ N and we have one of the following two cases:

(a) head(M) ≠ head(N): Because there exists a unifier for U one of M or N must be flexible. We assume that M is a flexible term.

(b) head(M) = head(N) ∈ DOM(θ): In this case M is flexible too.

Let M = λ \overline{x_{k}: T_{k}}. F (M_{m}) and N = λ \overline{x_{k}: T_{k}}. N′. Then LV_{4} is applicable or if M ⟶^{∗}_{η} F and F ∉FV(N) the rule LV_{3} is applicable too.

Therefore there exists a transformation

⟨U, θ⟩ ⟹_{LV} ⟨U′, θ′⟩

If one of the rules LV_{1}, LV_{2} or LV_{3} is applied, the requirements for θ′ are fulfilled 1. Because θ = θ′;

2. Because of the correctness of LU;

3. Because of the definition of LV. If the transformation rule LV_{4} is applied, we can assume, that θ = {F/Q} ∪ ϕ. Following lemma 5.6 there exists a selective partial binding P and a non-forgetful substitution τ such that

DOM(τ) ∩ W = ∅,
θ′ = {F/Q} ∪ τ ∪ ϕ =_{β} τ ∘ {F/P } ∪ ϕ, and

U′ = {F/P }(U) ∪ {F =^{?} P }.

The requirements for θ′ are fulfilled 1. Because of the construction of θ′;

2. We suppose DOM(θ) ∩ I(θ) = ∅, so following lemma 5.6

DOM(θ′) ∩ I(θ′) = ∅,

and

θ′(P) = τ(P) ⟶^{∗}_{β} Q = θ′(F).

3. Because U is unifiable, we can deduce from the applicability of LV_{4} the applicability of at least one of

LU_{4a}, LU_{4b}, or LU_{4c}:

• If head(N) is not a variable in DOM(θ) and – if head(Q) = head(N) then U ⟹_{LU_{4a}} U′ or – if head(Q) ≠ head(N) then U ⟹_{LU_{4b}} U′.

• If head(N) is a variable then U ⟹_{LU_{4c}} U′.

Lemma 5.9 If θ ∈ SU_{nf}(U) and no transformation applies to ⟨U, θ⟩ then U is in solved form.

Theorem 5.10 (Completeness of LU) For any unification problem U = ⟨D | FV(D)⟩, if θ ∈ SU_{nf}(U) then there exists a transformation sequence

U = U_{0} ⟹_{LU} U_{1} ⟹_{LU} ⋯ ⟹_{LU} U_{n}

such that U_{n} is in solved form and ⌈U_{n}⌉^{SUB} ≤_{β} θ [FV(D)].

Proof: It is easy to show that any sequence of LV-transformations terminates. Therefore we have for any unification problem U and unifier θ of U a finite sequence

⟨U, θ⟩ = ⟨U_{0}, θ_{0}⟩ ⟹^{∗}_{LV} ⟨U_{l}, θ_{l}⟩

such that no further transformation is applicable. By induction over l using lemma 5.8 with W = FV(U) we have θ = θ_{l} [W] and θ_{l} ∈ SU_{nf}(U_{l}). Furthermore there exists a corresponding transformation sequence

U = U_{0} ⟹^{∗}_{LU} U_{l}.

Using the previous lemma, U_{l} is in solved form. So we have ⌈U_{l}⌉^{SUB} ≤_{β} θ_{l} = θ [W].

6 Matching

To avoid the decision which definition of ‘matching’ we want to deal with, we consider the problem of restricted unification instead. A V-restricted unification problem is just a unification problem in the sense of definition 3.1. But the definition of a unifier changes in the following way:

Definition 6.1 (Unifier of a V-restricted unification problem) Let SUB be a set of substitutions. A substitution θ in SUB is a unifier of a V-restricted unification problem ⟨D | V ⟩ in SUB iff DOM(θ) ∩ (FV(D) \ V) = ∅ and θ_{V} is is a unifier for every equation in D.

If SUB is the set of all normalized substitutions in SUB(L^{→}^{V}) then the set of all unifiers of a V-restricted unification problem U is denoted SU^{V} (U). If SUB is the set of all normalized substitutions in SUB(L\overrightarrow{nf}^{V}) then a unifier is called non-forgetful and the set of all non-forgetful unifier of a U is written SU_{nf}^{V}(U). △

Obviously we have yet considered the problem of FV(D)-restricted unification or unrestricted unification. For D = {M_{1} =^{?} N_{1}, …, M_{n} =^{?} N_{n}} the problem of FV(M_{1}, …, M_{n})\FV(N_{1}, …, N_{n})-restricted unification will be called the problem of matching M_{1},…, M_{n} to N_{1},…, N_{n}.

Restricted unification can be reduced to unrestricted unification by an enrichment of the set of constants Σ and a reduction of the set of variables V generating the set of λ-terms. For a V-restricted unification problem ⟨D | V ⟩ let V′ = V \ symbols(((FV_{V}(D) \ V) ∪ (V \ FV_{V}(D)))) and Σ′ = Σ ∪ symbols((FV(D) \ V)). The free variables in FV_{V}(D) \ V occur in D but are not allowed to be instantiated by a V-restricted unifier. So they are added to the set of constants. Beside that the symbols of variables in V \ FV_{V}(D) are neither included in V′ nor in Σ′. This is necessary if we want to use LU as a complete transformation system for V-restricted unification as one can see in the proof of theorem 6.3.

This induces a bijection f between L^{→}(V,Σ) and L^{→}(V’,Σ’): f renames bound variables x: T such that x ∈ symbols((FV(D) \ V) ∪ (V \ FV(D))) to some y: T with y ∈ V′. So f(M) is only a α-variant of M. Because we have considered α-equivalence classes of terms all the time we will never use f explicitly in the following.

Of course, f can be lifted to a bijection from substitutions in SUB(L^{→}(V, Σ)^{V})_{V\(FV (D)\V)} into substitutions in SUB(L^{→}(V′, Σ′)^{V′}) and between systems in L^{→}(V, Σ) and systems in L^{→}(V′, Σ′).

Theorem 6.2 (Correctness) If U = ⟨D | V ⟩ is a V-restricted unification problem in L^{→}(V, Σ) and there exists a transformation sequence

⟨D | FV_{V}′(D)⟩ = U_{0} ⟹_{LU} U_{1} ⟹_{LU} ⋯ ⟹_{LU} U_{n}

in L^{→}(V′, Σ′) such that U_{n} is in solved form and possibly non-forgetful, then ⌈U_{n}⌉^{SUB} is a V-restricted unifier of U.

Proof: The correctness of LU implies that ⌈U_{n}⌉^{SUB} is a unifier of U. We have to show that it is V-restricted. Because all variables in FV_{V}(D) \ V are considered as constants in D the free variables of D are a subset of V. Because V′ and FV_{V}′(D) \ V are disjoint no free variable in U_{n} will be in FV_{V}′(D) \ V. So the domain of ⌈U_{n}⌉^{SUB} will be a subset of V. So ⌈U_{n}⌉^{SUB} is a V-restricted unifier of U.

Theorem 6.3 (Completeness) If U = ⟨D | V ⟩ is a V-restricted unification problem in L^{→}(V, Σ) and θ is a non-forgetful unifier of U then there exists a transformation sequence

⟨D | V ⟩ = U_{0} ⟹_{LU} U_{1} ⟹_{LU} ⋯ ⟹_{LU} U_{n}

in L^{→}(V′, Σ′) such that U_{n} is in solved form and possibly non-forgetful and

⌈U_{n}⌉^{SUB} ≤ θ [V].

Proof: Because θ is a unifier of the V-restricted unification problem ⟨D | V ⟩ it is also a unifier of the unification problem ⟨D | FV_{V}′(D)⟩. Because of the completeness of LU there exists a transformation sequence

⟨D | FV_{V}′(D)⟩ = U′_{0} ⟹^{∗}_{LU} ⟨D_{n} | FV_{V}′(D)⟩ = U′_{n}

in L^{→}(V′, Σ′) such that U′_{n} is in solved form and possibly non-forgetful. Because LU ignores the set of variables associated with the unification problem there is also a transformation sequence

⟨D | V ⟩ = U_{0} ⟹^{∗}_{LU} ⟨D_{n} | V ⟩ = U_{n}

We have ⌈U′_{n}⌉^{SUB} ≤ θ [FV_{V}′(D)].

Now we have FV_{V}′(D) ⊆ V. So we have to explain why we expect ⌈U_{n}⌉^{SUB} ≤ θ [V] to hold. Of course, this is true if (DOM(⌈U_{n}⌉^{SUB}) ∪ COD(⌈U_{n}⌉^{SUB})) ∩ (V \ FV_{V}′(D)) = ∅.

Let us carefully reconsider the completeness proof for the transformation system LU using the system LV. We can see that in neither step

⟨⟨D_{i} | V ⟩, θ_{i}⟩ ⟹_{LV} ⟨⟨D_{i+1} | V ⟩, θ_{i+1}⟩

a variable not in DOM(θ_{i}) is instantiated. Furthermore DOM(θ_{i+1}) \ DOM(θ_{i}) ⊆ V′. Because variables in V \FV_{V}(D) are not in FV′ and V \FV_{V}(D) = V \FV_{V}′(D), no variable in V \FV_{V}′(D) will be instantiated by ⌈U_{n}⌉^{SUB}. So we have at least ⌈U_{n}⌉^{SUB} = ⌈U′_{n}⌉^{SUB} [V].

For the same reason, no variable x ∈ (V \ FV_{V}′(D)) is an element of COD(⌈U_{n}⌉^{SUB}): Because they are neither in V′ nor in Σ′, they will not be introduced in some transformation step

⟨⟨D_{i} | V ⟩, θ_{i}⟩ ⟹_{LV} ⟨⟨D_{i+1} | V ⟩, θ_{i+1}⟩.

So they will not occur in U_{n} and we have ⌈U_{n}⌉^{SUB} ≤ θ [V].

7 Future Work

The question wether or not higher-order matching is decidable in the simply typed lambda calculus is open. It is obvious that neither the matching algorithm based on PU nor the algorithm based on LU provides a decision procedure for matching in the non-forgetful lambda calculus.

Example 7.1 Given the signature

sort  T_{1}
constants a : T_{1}
variable  F : ((T_{1} → T_{1}) → T_{1})

we consider the second-order matching problem

M_{0} = ⟨{F: T_{1}(λ x: T_{1}. x) =^{?} a: T_{1}} | F ⟩

In LU as well as in PU it is possible to use the project rule. We apply the substitution

σ = {F: T_{1}/λ y: (T_{1} → T_{1}). y(H_{1}: ((T_{1} → T_{1}) → T_{1})(y))}

to M_{0} resulting in the matching problem

M_{1} = ⟨{H_{1}: T_{1}(λ x: T_{1}. x) =^{?} a: T_{1}} | F ⟩.

M_{1} is identical to M_{0} up to renaming of the free variable. So the projection rule can be applied again and again resulting in an infinite branch in the search space.

Nevertheless, the use of the non-forgetful lambda calculus puts a strong restriction on the unifiers of a V - restricted unification problem. In the above example it is easy to see that there exists no matching substition for M_{0}. So it could be possible that it is easier to provide a decision procedure for matching in the nonforgetful lambda calculus than to provide such a procedure for the simply typed lambda calculus (if either of them exists).

References

Alonzo Church, 1941. The Calculi of Lambda-Conversion. Number 6 in Annals of Mathematics Studies. Princeton University Press, Princeton, USA.

W. Snyder and J. Gallier, 1989. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation, Vol. 8, pp. 101–140.