Termination of Rule-Based Calculi
for Uniform Semi-Unification
Takahito Aoto1 and Munehiro Iwami2
1

2

RIEC, Tohoku University, Japanaoto@nue.riec.tohoku.ac.jp

Dept. of Mathematics and Computer Science, Interdisciplinary Faculty of Scienceand Engineering, Shimane University, Japan
munehiro@cis.shimane-u.ac.jp

Abstract. Uniform semi-unification is a generalization of unification;
its efficient algorithms have been extensively studied in (Kapur et al.,1994) and (Oliart&Snyder, 2004). For (uniform) semi-unification, several variants of rule-based calculi are known. But, some of these calculi
in the literature lack the termination property, i.e. not all derivations are
terminating. We revisit symbolic semi-unification whose solvability coincides with that of uniform semi-unification. We give an abstract criterionof the strategy on which a general rule-based calculus for symbolic semiunification terminates. Based on this, we give an alternative and robust
correctness proof of a rule-based uniform semi-unification algorithm.
Keywords: Semi-Unification, Rule-Based Calculi, Termination

1

Introduction

Describing algorithms using rule-based calculi is often useful to present algorithms abstractly and to study the correctness of algorithms by separating theissue from those of the search strategy and/or efficiency. For many algorithms,
rule-based calculi have been widely adapted and commonly used to extend or
modify the algorithms; well-known such examples are the unification algorithm
and the Knuth-Bendix completion algorithm (see e.g. [1]).
Semi-unification is a generalization of unification. Its application includes
non-termination proving of term rewriting systems [3, 8, 16] and polymorphic
type inference problems of ML languages [7, 11]; it is also related to some problems in proof theory [17] and in computational linguistics [2]. Like unification,
if a semi-unifier exists, there exists a most general semi-unifier [7, 10, 17]. Unlike
unification, however, semi-unification is undecidable in general [10]. Hence, many
decidable classes of semi-unification have been studied: uniform semi-unification[4, 8, 15, 17–19], acyclic semi-unification [11, 14], left-linear semi-unification [6, 9],quasi-monadic semi-unification [13] and semi-unification in two variables [12].
Decidability of uniform semi-unification has been shown in various articles
almost at the same time [4, 5, 8, 12, 17]. Efficient algorithms for uniform semiunification have been extensively studied in [8, 15]. Like with unification, working

2

T. Aoto and M. Iwami

on graphs is mandatory in order to give efficient algorithms, and thus thesebest efficient algorithms are based on graphs. The basis of correctness of thesealgorithms, however, is given by a simple version of the algorithms given in[8] that can be almost adapted as a rule-based calculus (not on graphs but onterms). In [15], a variant of this calculus are adapted as a rule-based calculus
but no correctness proof is presented.
In contrast to similar rule-based calculi for the unification, some of suchcalculi in the literature lack the termination property, i.e. not all derivations
are terminating. It is mentioned in [8] that “it can be shown that Algorithm A1 will always terminate either reporting failure or semi-unifiability;...” without
a proof. But, actually, derivations in their rule-based calculus terminate only
if some suitable interpretation or derivation strategy is assumed. The calculus
given in [15] is more flexible than that of [8], and it is not terminating either.
It may be thought that giving a terminating variant of these calculi is easy.
However, it is, at least, difficult to adapt a termination proof similar to theone applied to calculi for unification for the following reasons: (1) equationsin “solved” form may later be changed to “unsolved”, and (2) the multiset ofthe (extended) variables in the equations may increase. In fact, as pointed out
in [13], it seems not easy to give a well-founded ordering that guarantees thetermination of such calculi.
In this paper, we revisit symbolic semi-unification, whose solvability coincides with that of uniform semi-unification. We present a new characterizationof symbolic semi-unification, which reinforces the correspondence between thesepresentations of uniform semi-unification. We give an abstract criterion of thestrategy on which a general rule-based calculus for symbolic semi-unification terminates. In this way, we give an alternative and robust proof for the correctnessof a rule-based uniform semi-unification algorithm.

2

Preliminaries

We denote sets of arity-fixed function symbols and variables by F and V, respectively. The set of terms is denote by T(F, V). The set of variables in an
object α, which may be a term, etc. is denoted by V(α). A context is a term inT(F ∪ {}, V) containing a single occurrence of , which is a special constantnot contained in F. A term obtained by replacing  in a context C with a term t
is denoted by C[t]. A term s is a subterm of a term t (written as s E t) if t = C[s]for some context C. A substitution σ is a mapping from V to T(F, V) with thefinite domain dom(σ) = {x | x 6= σ(x)}. Substitutions are homomorphicallyextended to mappings over T(F, V). We write σ(t) as tσ. A substitution σ withdom(σ) = {x1 , . . . , xn } and σ(xi ) = ti is denoted by {x1 := t1 , . . . , xn := tn }.
We denote an equation by s ≈ t which is indistinguished from t ≈ s and an
inequation by s 6 t. We also consider indexed inequations of the form s 6i t
where the index i ranges over 1, . . . , k. Let E = {si ◦i ti | 1 ≤ i ≤ n, ◦i ∈ {≈, 61, . . . , 6k }} be a set of equations and indexed inequations. Then E is said to besemi-unifiable if there exists a substitution τ, ρ1 , . . . , ρk such that τ (si ) = τ (ti )Termination of Rule-Based Calculi for Uniform Semi-Unification

3

for all si ≈ ti ∈ E and ρj (τ (si )) = τ (ti ) for all si 6j ti ∈ E; the substitution τ
is called a semi-unifier of E and the substitutions ρ1 , . . . , ρk are called residual
substitutions of the semi-unifier τ . A semi-unification problem is a problem to ask
whether there is a semi-unifier for a given set of equations and (indexed) inequations. A semi-unification problem is said to be uniform if k = 1 (i.e. the index ofinequations is unique); when we think of a uniform semi-unification problem theindex of inequations will be omitted. Any (uniform) semi-unification problem E
can be reduced to a (uniform) semi-unification problem without equations byreplacing si ≈ ti ∈ E with zi 6 si , zi 6 ti using a fresh variable zi . Thus, one
can assume w.l.o.g. that any semi-unification problem deals with only the set of
inequations.
Example 1. Let E = {f(h(y), x) 6 f(x, h(h(y)))}. Take σ = {x := h(y ′ )} andρ1 = {y := y ′ , y ′ := h(y)}, where y ′ is a fresh variable. We have f(h(y), x)σρ1 =f(h(y), h(y ′ ))ρ1 = f(h(y ′ ), h(h(y))) = f(x, h(h(y)))σ. Thus E is semi-unifiable andσ is a semi-unifier. Note here that f(h(y), x) and f(x, h(h(y))) are not unifiable.

3

Symbolic Semi-Unification

In this section, we introduce a notion of symbolic1 semi-unification. The notion
is based on the idea of syntactically representing the substitution ρ of the identity ρ(τ (s)) = τ (t) expressing semi-unifiability. This idea goes back to [8]. Ourpresentation mostly follows a nicer formulation given in [13]. In the literature,various symbols are used as the “place holder” for ρ; we here use ∇ as it isclearly distinguished from substitutions denoted by ρ, τ, σ, etc.
Definition 2 (symbol ∇, ∇-variables, ∇-terms, operator ∇).
1. We use a unary special function symbol ∇ which is supposed to be notcontained in F.
2. We define ∇-terms as follows: (i) ∇i (x) where x ∈ V and i ≥ 0 are ∇-terms
i-timesz }| {
where ∇ (x) abbreviates ∇(· · · ∇(x) · · · ); (ii) if t1 , . . . , tn are ∇-terms thenf (t1 , . . . , tn ) is a ∇-term for any f ∈ F of arity n. Equations of ∇-terms
are said to be ∇-equations.
3. ∇-terms of the form ∇i (x) (i ≥ 0) are called ∇-variables. We denote ∇i (x)by xi . Hence x0 = x, ∇(xi ) = xi+1 , and xj E xi for all j ≤ i. The sets of∇-variables and ∇-terms are denoted by V ∗ and T(F, V ∗ ), respectively. The
set of ∇-variables in an object α is denoted by V ∗ (α).
4. We define a unary operation ∇ on ∇-terms recursively as follows: ∇(xi ) =xi+1 ; ∇(f (t1 , . . . , tn )) = f (∇(t1 ), . . . , ∇(tn )).
i

Example 3. A ∇-term t = f(x, g(∇(∇(y)))) may be also written as f(x, g(∇2 (y)))
or f(x, g(y 2 )). The set of ∇-variables in t is V ∗ (t) = {x, y, ∇(y), ∇(∇(y))} ={x, y, y 1 , y 2 }. We have ∇(t) = ∇(f(x, g(∇2 (y)))) = f(∇(x), ∇(g(∇2 (y)))) =f(∇(x), g(∇3 (y))) = f(x1 , g(y 3 )) and ∇2 (t) = ∇(∇(t)) = f(x2 , g(y 4 )).
1

The name “symbolic” is from [19].

4

T. Aoto and M. Iwami

Contexts over ∇-terms and the subterm relation on ∇-terms are definedsimilarly to the usual contexts and subterms. We define ∇-substitutions below.
Definition 4 (∇-substitution).
1. A ∇-substitution is a partial mapping σ from V ∗ to T(F, V ∗ ) such that (i)the domain dom(σ) of σ is finite; (ii) for each x ∈ V there exists at mostone i such that xi ∈ dom(σ); (iii) for each xi , y j ∈ dom(σ), y j 6E σ(xi ).
2. The application σ(t) of a ∇-substitution σ to a ∇-term t is recursively defined
as follows: σ(y j ) = y j if y i ∈/ dom(σ) for any i ≤ j; σ(y j ) = ∇j−i (σ(y i )) ifiy ∈ dom(σ) for some i ≤ j; σ(f (t1 , . . . , tn )) = f (σ(t1 ), . . . , σ(tn )).
3. The many-time application σ ∗ (t) of a ∇-substitution σ to a ∇-term t isdefined as follows: σ ∗ (t) = t if xi 6E t for any xi ∈ dom(σ); σ ∗ (t) = σ ∗ (σ(t))
otherwise.
We write σ(t) as tσ and σ ∗ (t) as tσ ∗ ; in particular, we write σ ∗ (∇(t)) as∇(t)σ ∗ . The notion of many-time application of a ∇-substitution to a ∇-term isused to give an invariance of derivation for symbolic semi-unification.
Example 5. The partial mapping σ = {x := a, x1 := b} is not a ∇-substitution,
as the σ does not satisfy the condition (ii). Neither is the partial mapping σ ={x1 := f(y 1 ), y 1 := b}, as the σ does not satisfy the condition (iii). The partial
mapping σ = {x1 := y, y 1 := f(z 2 )} is a ∇-substitution, and we have σ(y 3 ) =∇2 (σ(y 1 )) = ∇2 (f(z 2 )) = f(z 4 ) and σ ∗ (x2 ) = σ ∗ (∇(y)) = σ ∗ (y 1 ) = f(z 2 ).
It may be not so obvious from the definition that tσ ∗ is always well-defined;
however, this can be derived from our definition of ∇-substitutions.
Lemma 6. For any ∇-substitution σ and ∇-term t, tσ ∗ is well-defined.
Proof. Define, for each ∇-variable xj , w(xj ) = max{j − i + 1, 0} if xi ∈ dom(σ)
for some i, and w(xj ) = 0 otherwise. Let W(t) be the multiset of weight of∇-variables in a ∇-term t. Then if t 6= tσ then W(t) ≫ W(tσ), where ≫ is themultiset extension (e.g. [1]) of the natural order > on the set of natural numbers.
The claim follows from the well-foundedness of ≫.
⊓⊔Lemma 7. For any ∇-term t and ∇-substitution σ, ∇(t)σ ∗ = ∇(tσ ∗ )σ ∗ .
Proof. Let R = {ug → vg | u := v ∈ σ} be a TRS (see e.g. [1]), where ()g replaces
each variable with a distinct constant. The claim follows from completeness of
the TRS R ∪ {∇(f (x1 , . . . , xn )) → f (∇(x1 ), . . . , ∇(xn )) | f ∈ F}.
⊓⊔
We now introduce a notion of symbolic semi-unification.
Definition 8 (symbolic semi-unification). For a set E of ∇-equations, asemi-unifier of E is a ∇-substitution σ such that sσ ∗ = tσ ∗ for all s ≈ t ∈ E; if
E has a semi-unifier, E is said to be semi-unifiable. A symbolic semi-unification
problem asks whether there exists a semi-unifier for a given set of ∇-equations.
The next lemma is shown using Lemma 7.

Termination of Rule-Based Calculi for Uniform Semi-Unification

5

Lemma 9 (semi-unifiability is closed under ∇). Let σ be a ∇-substitution
and s, t be ∇-terms. If sσ ∗ = tσ ∗ then ∇(s)σ ∗ = ∇(t)σ ∗ .
Remark 10. In contrast to Lemma 9, sσ = tσ does not necessary imply ∇(s)σ =∇(t)σ: Let σ = {x2 := f(x)}, s = x3 and t = f(x1 ). Then sσ = f(x1 ) = tσ, but∇(s)σ = x4 σ = f(x2 ) 6= f(f(x)) = f(x2 )σ = ∇(t)σ.
The notions of ∇-equality and inconsistency were introduced in [8].
Definition 11 (∇-equality). For a set E of ∇-equations, the ∇-equality generated by E, denoted by ≈E , is the smallest equivalence relation such that (i)s ≈E t for any s ≈ t ∈ E, (ii) s ≈E t implies ∇(s) ≈E ∇(t), and (iii) for any
f ∈ F, f (s1 , . . . , sn ) ≈E f (t1 , . . . , tn ) iff, for any i = 1, . . . , n, si ≈E ti holds.
Definition 12 (inconsistency). A set E of ∇-equations is inconsistent if either (i) xi ≈E s with xi E s ∈/ V ∗ , or (ii) f (s1 , . . . , sm ) ≈E g(t1 , . . . , tn ) with
f 6= g for some f, g ∈ F. Furthermore, E is consistent if it is not inconsistent.
The next lemma will be used heavily in our proof.
Lemma 13. Let E be a set of ∇-equations. Suppose E is semi-unifiable and let
σ be a semi-unifier of E. Then for any ∇-terms u, v, u ≈E v implies uσ ∗ = vσ ∗ .
Proof. By induction on the derivation of u ≈E v using Lemma 9.

4⊓⊔

Symbolic Semi-Unification and Semi-Unification

In this section, we show the equivalence between the consistency and the symbolic semi-unifiability of ∇-equations and the semi-unifiability of the corresponding inequations. Thus, we extend and give a rigorous proof of a result of [8]. A
part of the proof will be postponed until Section 6.
We first introduce interpretations of ∇-terms, a key notion of our proof.
Definition 14 (interpretation). Let τ, ρ be substitutions. An interpretation[[t]]τρ ∈ T(F, V) of t ∈ T(F, V ∗ ) is given by [[xi ]]τρ = ρi (τ (x)); [[f (s1 , . . . , sn )]]τρ =f ([[s1 ]]τρ , . . . , [[sn ]]τρ ).
Lemma 15. Let τ, ρ be substitutions. (1) For t ∈ T(F, V ∗ ), [[∇(t)]]τρ = ρ([[t]]τρ ).
(2) For t ∈ T(F, V), [[t]]τρ = τ (t).
Proof. By induction on t.

⊓⊔

A solution σu , σm of a uniform semi-unification problem can be obtained froma solution σ of symbolic semi-unification problem as follows.
Definition 16 ([8]). Let σ be a ∇-substitution. Then we define its unification
part σu and matching part σm as below.
1. Let X0S= {x ∈ V | x ∈ dom(σ)}, X1 = {xi | xi ∈ dom(σ), i > 0}, andX2 = ( {V ∗ (xi ≈ σ(xi )) | xi ∈ dom(σ)}) \ (V ∪ X1 ).

6

T. Aoto and M. Iwami

2. Prepare fresh distinct variables for each xi ∈ X2 and let ϕ be a mapping thatassigns to each xi ∈ X2 the corresponding fresh variable; let ϕ be recursively
extended as ϕ(y) = y; ϕ(f (t1 , . . . , tn )) = f (ϕ(t1 ), . . . , ϕ(tn )).
3. For each xi ∈ X1 , put σm (xi−1 ) = ϕ(σ(xi )) if i = 1, and σm (ϕ(xi−1 )) =ϕ(σ(xi )) otherwise. For each xi ∈ X2 , put σm (xi−1 ) = ϕ(xi ) if i = 1, andσm (ϕ(xi−1 )) = ϕ(xi ) otherwise.
4. For each x ∈ X0 , put σu (x) = ϕ(σ(x)).
Example 17. Let σ = {x := f(y, z 1 ), y 1 := f(y, z), z 3 := f(z 1 , w2 )}. Then X0 ={x}, X1 = {y 1 , z 3 } and X2 = {z 1 , z 2 , w1 , w2 }. Put ϕ = {z 1 := z ′ , z 2 := z ′′ , w1 :=w′ , w2 := w′′ }. Then we have σm = {y := f(y, z), z ′′ := f(z ′ , w′′ ), z := z ′ , z ′ :=z ′′ , w := w′ , w′ := w′′ } and σu = {x := f(y, z ′ )}.
Lemma 18. For any ∇-substitution σ, σu and σm are well-defined substitutions.
ii(x) = ϕ(σ(xi )) for xi ∈ X1 .
(x) = ϕ(xi ) for xi ∈ X2 . (2) σm
Lemma 19. (1) σm

Lemma 20. Let t ∈ T(F, V ∗ ) such that V(t) ∩ X0 = ∅ and V ∗ (t) \ V ⊆ X2 .
Then [[t]]σσum = ϕ(t). In particular, for any xi ∈ X1 , [[σ(xi )]]σσum = ϕ(σ(xi )).
The next two key lemmas are used to prove the theorem below.
Lemma 21. For any t ∈ T(F, V ∗ ) and any ∇-substitution σ, [[σ ∗ (t)]]σσum = [[t]]σσum .
Proof. First prove [[σ(t)]]σσum = [[t]]σσum using Lemmas 15, 19 and 20.

⊓⊔

Lemma 22. Let s, t ∈ T(F, V ∗ ), and ρ, τ be substitutions. Suppose that [[l]]τρ =[[r]]τρ for any l ≈ r ∈ E. Then if u ≈E v then [[u]]τρ = [[v]]τρ .
Proof. By induction on the derivation of u ≈E v, using Lemma 15.

⊓⊔

Theorem 23 (consistency and semi-unifiability). For any terms s, t ∈T(F, V), the following are equivalent: (i) {∇(s) ≈ t} is semi-unifiable, (ii){s 6 t} is semi-unifiable, and (iii) {∇(s) ≈ t} is consistent.
Proof. (iii) ⇒ (i) will be shown later (Corollary 45). To show (i) ⇒ (ii), use
Lemmas 15 and 21. To show (ii) ⇒ (iii), use Lemmas 15 and 22.
⊓⊔(ii) ⇔ (iii) was obtained in [8]; we incorporate an equivalence with (i).

5

Partial Correctness of Symbolic Semi-Unification

In this section, we give a rule-based symbolic semi-unification procedure andshow its partial correctness. Our calculus is a variant of the one given in [8]. Essentially the same calculi are given in [12, 13, 15, 19]. Before giving the procedure,
we need a preparation.
Definition 24 (relation ⋗). We fix an arbitrary (strict) total order ⋗ on V ∗satisfying (i) i > j implies xi ⋗ xj and (ii) xi ⋗ y j implies xi+1 ⋗ y j+1 . The
order ⋗ is extended by xi ⋗ t for any t ∈/ V ∗ and xi 6E t.

Termination of Rule-Based Calculi for Uniform Semi-Unification
Decompose

Reduce7{f (s1 , . . . , sn ) ≈ f (t1 , . . . , tn )} ⊎ E
f ∈F{s1 ≈ t1 , . . . , sn ≈ tn } ∪ E{xi ≈ t, C[xi ] ≈ u} ⊎ E{xi ≈ t, C[t] ≈ u} ∪ E

xi ⋗ tDelete{xi ≈ xi } ⊎ E
E

Clash

{f (s1 , . . . , sm ) ≈ g(t1 , . . . , tn )} ⊎ E
f 6= g, f, g ∈ F
⊥

Check

{xi ≈ t} ⊎ Et∈/ V ∗ , xi E t⊥
Fig. 1. Inference rules for symbolic semi-unification

It readily follows from our condition that (i) i > j iff xi ⋗ xj and (ii) xi ⋗ y j
iff xi+1 ⋗ y j+1 . One way to give ⋗ is to fix some total order > on V and definexi ⋗ y j iff either x > y or (x = y and i > j) as in [8, 15, 19]. But our proof reveals
that the abstract condition above is sufficient.
Definition 25 (symbolic semi-unification procedure). One step derivation using any of inference rules listed in Figure 1 is denoted by ❀. Here, theinference rules act on a finite set of ∇-equations and ⊎ denotes the disjoint
union. For an input of a finite set E0 of ∇-equations and the relation ⋗, asymbolic semi-unification procedure non-deterministically constructs a derivation E0 ❀ E1 ❀ · · · (possibly following some fixed derivation strategy). The
derivation may be finite or infinite, and it is maximal if it does not end with
Ek for which a further application of an inference rule is possible. A symbolic
semi-unification procedure (following a fixed derivation strategy) terminates if
any derivation (following that derivation strategy) is finite.
∗

The reflexive transitive closure of ❀ is denoted by ❀.
Example 26. Let the total order ⋗ be given by wi ⋗ xj ⋗ y k ⋗ z l for any i, j, k, l.
Consider E = {y 3 ≈ z, w3 ≈ x, x2 ≈ f 2 (y), x1 ≈ f(w2 )}. Then we have{y 3 ≈ z, w3 ≈ x, x2 ≈ f 2 (y), x1 ≈ f(w2 )}❀ {y 3 ≈ z, w3 ≈ x, f(w3 ) ≈ f 2 (y), x1 ≈ f(w2 )}❀ {y 3 ≈ z, w3 ≈ x, w3 ≈ f(y), x1 ≈ f(w2 )}❀ {y 3 ≈ z, f(y) ≈ x, w3 ≈ f(y), x1 ≈ f(w2 )}❀ {y 3 ≈ z, x ≈ f(y), w3 ≈ f(y), f(y 1 ) ≈ f(w2 )}❀ {y 3 ≈ z, x ≈ f(y), w3 ≈ f(y), w2 ≈ y 1 }❀ {y 3 ≈ z, x ≈ f(y), y 2 ≈ f(y), w2 ≈ y 1 }❀ {z ≈ f(y 1 ), x ≈ f(y), y 2 ≈ f(y), w2 ≈ y 1 }.
Here, modified parts are underlined.

8

T. Aoto and M. Iwami

Remark 27. In [8], the following (almost) rule-based procedure is given: (1) Apply Decompose as many times as possible; Apply Clash or Check if possible. (2)Fix a total order > on variables. Consider a ground TRS R = {l → r | l ≈r ∈ E, l > r}. Then: “For each rule, reduce each side (if reducible) by a single
step of rewriting by other rules. If no rule can be rewritten any further, report
SUCCESS. Otherwise replace the rule by the new equation thus obtained and
go to Step (1).”
It is claimed in [8] that this procedure is terminating. The description “Foreach rule, ...” is difficult to interpret: for example,{h(g(y 1 ), g(z 1 ), g(x1 )) ≈ h(x, y, z)} ❀ {x ≈ g(y 1 ), y ≈ g(z 1 ), z ≈ g(x1 )}❀ {x ≈ g2 (z 2 ), y ≈ g2 (x2 ), z ≈ g2 (y 2 )}❀ {x ≈ g4 (y 4 ), y ≈ g4 (z 4 )), z ≈ g4 (x4 )}❀ ···should not be the case, as they claim that their procedure terminates.
Remark 28. Recall the following inference rules of the unification procedure corresponding to Reduce and Check:
Reduce′Check′
h{x ≈ t} ⊎ E, σih{x ≈ s} ⊎ E, σix∈/ V(t)x ✂ s, s ∈/Vh{x := t}(E), {x := t} ◦ σi⊥

Two differences can be observed:• the equations part and the substitution part are separated, and• Reduce′ uses the substitution (replacing all occurrences of x), while Reduce
uses the replacement (replacing a single occurrence of xi ).
In the unification procedure, the substitution part can be naturally separated
from the equations part, as the substitution {x := t} is not needed again in theequation part. But in the case of semi-unification, this is not the case:{x1 ≈ f(x, y 2 ), y 1 ≈ g(x), y 3 ≈ g(z)}❀ {x1 ≈ f(x, y 2 ), y 1 ≈ g(x), g(x2 ) ≈ g(z)}❀ {x1 ≈ f(x, y 2 ), y 1 ≈ g(x), x2 ≈ z}
❀ {x1 ≈ f(x, y 2 ), y 1 ≈ g(x), f(x1 , y 3 ) ≈ z}
❀ ···{x1 , x, y 2 , y 1 , x, y 3 , z}{x1 , x, y 2 , y 1 , x, x2 , z}{x1 , x, y 2 , y 1 , x, x2 , z}{x1 , x, y 2 , y 1 , x, x1 , y 3 , z}

At the first line, x1 := f(x, y 2 ) can not be applied to other equations, while it
can be applied to the equation x2 ≈ z at the third line. Thus, a solved equationneeds to be kept in the system for the future simplifications or for the case theequation itself is simplified in the future. Hence, it is not possible to split off thesolved equations as the substitution part. Furthermore, since the substitution
does not eliminate the future need of the application of the same substitution,
it seems natural to use the replacement in Reduce instead of the substitution.
It is also observed that the derivation from the first line to the fourth line
strictly increases the multiset of ∇-variables in the equation, which is listed at
the right. Hence it is difficult to adapt a termination proof similar to the one
applied to calculi for unification (see e.g. [1]).

Termination of Rule-Based Calculi for Uniform Semi-Unification

9

Example 29. In fact, our calculus is not terminating—this is witnessed by thefollowing derivation.
{x ≈ z, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(y) ≈ z, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(y) ≈ g(x), x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {y ≈ x, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(z) ≈ x, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(z) ≈ g(y), x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {z ≈ y, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(x) ≈ y, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {g(x) ≈ g(z), x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ {x ≈ z, x ≈ g(y), y ≈ g(z), z ≈ g(x)}❀ ···We note that because of some postponed applications of Reduce, Check is notapplicable in the derivation. This infinite derivation is also valid in the calculus given in [15]. In Section 6, we will give a sufficient criterion on derivation
strategies under which any derivation terminates.
Remark 30. The infinite derivation above is not possible, if one adopts a variantof Reduce using substitution (instead of the replacement):
Reduce′′{xi ≈ t} ⊎ E{xi ≈ t} ∪ {xi := t}(E)xi ⋗ tRule-based semi-unification calculi in [8, 15] use the replacement, and those in[12, 13, 19] use the substitution. We note that any substitution can be simulated
by repeated applications of replacement. We refer Lemma 43 for the terminationof the calculus obtained by replacing the Reduce by Reduce′′ —termination ofsuch calculus under a particular derivation strategy is also obtained in [12].
Remark 31. Another difference of the rule-based semi-unification calculi in theliterature is whether the transformation ∇(f (t1 , . . . , tn )) = f (∇(t1 ), . . . , ∇(tn ))is admitted in the course of derivations. The calculi in [15, 19] admit such flexibility. Adding such flexibility, however, causes another non-terminating derivation2 .
We now give several properties of finite derivations.
∗Lemma 32. Suppose E ❀ E ′ with E ′ 6= ⊥. Then ≈E = ≈E ′ .
Using Lemma 13, we have∗

Corollary 33. If E ❀ E ′ 6= ⊥, then E is semi-unifiable iff E ′ is semi-unifiable.
Using Lemma 13 and Corollary 33, partial correctness of our symbolic semiunification procedure is obtained.
Theorem 34 (partial correctness). Let E be a finite set of ∇-equations. (1)∗∗If E ❀ ⊥ then E is not semi-unifiable. (2) If E ❀ E ′ 6= ⊥ and no inference′
rules are applicable to E , then E is semi-unifiable.
2

The authors learned this observation from an anonymous reviewer.

10

6

T. Aoto and M. Iwami

Termination of Symbolic Semi-Unification Procedure

In this section, we show termination of our rule-based symbolic semi-unification
procedure under an assumption on the derivation strategy employed.
For the proof, we introduce a new relation.
Definition 35 (variable relation). A relation >v on ∇-variables, called thevariable relation consistent with a set of ∇-equations E and the order ⋗, is thesmallest transitive relation satisfying the following conditions: (i) if xi ≈E y jwith xi ⋗ y j then xi >v y j , (ii) if xi ≈E C[y j ] with C[y j ] ∈/ V ∗ for some strictijcontext C then x >v y . Here, a context C is strict if C is not of the form
C ′ [∇()] for some context C ′ . The reflexive closure of >v is denoted by ≥v .
Lemma 36. Let >v be a variable relation consistent with E and ⋗. If xi >v y jthen xi ≈E C[y j ] for some context C; furthermore, if C =  then xi ⋗ y j .
Lemma 37. Let X be a finite set of variables. Let a0 , a1 , . . . be an infinite sequence of ∇-variables from X ∗ = {xi | x ∈ X, i ≥ 0}. Then there exist indexesi, j with i < j such that aj = ∇k (ai ) for some k ≥ 0.
Definition 38 (M(t), M(E)). The multiset M(t) of ∇-variables that occur
maximallyin a ∇-term t is defined like this: M(xi ) = {xi }; M(fU (t1 , . . . , tn )) =
U
M(t
).
For
a
finiteset
Eof∇-equations,
we
put
M(E)
=
{M(s) ⊎ M(t) |iis ≈ t ∈ E}. Here, ⊎ denotes the multiset union.
The next property is well-known (see e.g. [1]).
Proposition 39. Let ≫v be the multiset extension of >v and ≥≥v its reflexive
closure. Let M0 ≥≥v M1 ≥≥v · · · be an infinite sequence of finite multisets suchthat Mi ≫v Mi+1 for infinitely many indexes i. Then there is an infinite sequencea0 ≥v a1 ≥v · · · with ai ∈ Mi such that ai >v ai+1 for infinitely many indexes i.
Lemma 40. Let E0 be a finite set of ∇-equations, >v the variable relation con∗sistent with E0 and ⋗. If E0 ❀ E ❀ E ′ 6= ⊥ then M(E) ≥≥v M(E ′ ). In′
particular, if E ❀ E is by Reduce, then M(E) ≫v M(E ′ ).
Proof. Distinguish the cases by the inference rule used in E ❀ E ′ .

⊓⊔Theorem 41 (termination of symbolic semi-unification procedure). Every derivation starting from a consistent finite set of ∇-equations is finite.
Proof. Suppose E0 ❀ E1 ❀ · · · be an infinite derivation and E0 is consistent.
Then, Clash and Check can not be used in this derivation. Decompose andDelete do not increase M(Ei ) but reduce the number of symbols. Hence there
does not exists an index j such that the Decompose and Delete are used for all
Ei ❀ Ei+1 with i > j. Thus there are infinitely many i such that Reduce is usedon Ei ❀ Ei+1 . Hence M(E0 ) ≥≥v M(E1 ) ≥≥v · · · and there are infinitely many isuch that M(Ei ) ≫v M(Ei+1 ) by Lemma 40. Then, by Proposition 39, we havean infinite sequence xi00 >v x1i1 >v · · · . Thus by Lemma 37 there exists indexesTermination of Rule-Based Calculi for Uniform Semi-Unification

11

k, l (k < l) such that ik ≤ il and xk = xl = x. Since >v is transitive relation,
xikk >v xil l . Hence by Lemma 36, xik ≈E C[xil ] for some context C such thatC =  implies xik ⋗ xil . C 6=  contradicts with the consistency of E. If C = then xik ⋗ xil contradicts ik ≤ il . Thus there exists no infinite derivation.
⊓⊔
The above theorem motivates the following definition.
Definition 42 (refutational completeness). A derivation strategy is said tobe refutationally complete if any maximal derivation starting from an inconsistent set of ∇-equations and following that strategy is finite and ends with ⊥.
The next lemma gives a concrete example of refutationally complete derivation strategy. Note that the rule Reduce′′ is given in Remark 30.
Lemma 43. A derivation strategy subject to using Reduce′′ in place of Reduceand applying Check whenever possible is refutationally complete.
Proof. Suppose E0 ❀ E1 ❀ · · · be a maximal derivation and E0 is inconsistent. If Clash or Check is used then we are done. Otherwise, from the proof
ik+1
of Theorem 41, we have a sequence of ∇-variables xik = xikk >v xk+1
>v
ik+1
] ∈
· · · >v xil l = xil with ik ≤ il . This means that there exist xik ≈ Ck [xk+1
il−1
Eik , . . . , xl−1
≈ Cl [xil ] ∈ Eil−1 . Since Reduce′′ is simulated in our derivation,
ij+2
ij+1
ij+1
] for j = k + 1, . . . , l − 1. Hence] is replaced by Cj+1 [xj+2every xj+1 in Cj [xj+1ik+1] ∈ Eik has the descendant xik ≈ C[xil ] ∈ Eil such that C = 
xik ≈ Ck [xk+1ik
implies x ⋗ xil . If C 6=  then Check can be applied, which contradicts ourassumption. If C =  then xik ⋗ xil contradicts ik ≤ il .
⊓⊔The next theorem immediately follows from Theorems 34 and 41.
Theorem 44 (total correctness). The symbolic semi-unification procedureterminates if it follows a refutationally complete derivation strategy; either the
input E is semi-unifiable and any maximal derivation ends with a set of ∇equations or E is not semi-unifiable and any maximal derivation ends with ⊥.
We now obtain Theorem 4.1 of [8], on which their correctness proof is based,
as a corollary.
Corollary 45 (consistency and semi-unifiability [8]). Let E be a finite setof ∇-equations. Then E is consistent iff E is semi-unifiable.
Proof. (⇒) Use Theorem 44 and Lemma 32. (⇐) Use Lemma 13.

7⊓⊔

Conclusion

We have revisited rule-based calculi for uniform semi-unification, on which efficient uniform semi-unification procedures [8, 15] are based. We have given a
new characterization of symbolic semi-unification and extended the correspondence between symbolic semi-unifiability and uniform semi-unifiability. For arule-based calculus of symbolic semi-unification, which is given in a general form
essentially including those of [8, 12, 15, 19], we have shown its termination andcorrectness under refutationally complete derivation strategy.

12

T. Aoto and M. Iwami

Acknowledgment
Thanks are due to anonymous referees for many valuable comments. The authors
are grateful for Yoshihito Toyama for helpful comments. This work was partially
supported by a grant from JSPS No. 23500002.

References
1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press(1998)
2. Dörre, J., Rounds, W.C.: On subsumption and semiunification in feature algebras.
In: Proc. of LICS 1990. pp. 300–310. IEEE (1990)
3. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving terminationof higher-order functions. In: Proc. of FroCoS 2005. LNAI, vol. 3717, pp. 216–231.
Springer-Verlag (2005)
4. Henglein, F.: Algebraic properties of semi-unification. In: Proc. of LFP 1988. ACM
Press (1988)
5. Henglein, F.: Polymorphic Type Inference and Semi-Unification. Ph.D. thesis, Rutgers University (1989)
6. Henglein, F.: Fast left-linear semi-unification. In: Proc. of ICCI 1990. LNCS, vol.
468, pp. 82–91. Springer-Verlag (1990)
7. Henglein, F.: Type inference with polymorphic recursion. TOPLAS 15(2), 253–289(1993)
8. Kapur, D., Musser, D., Narendran, P., Stillman, J.: Semi-unification. TCS 81(2),169–187 (1991)
9. Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Computational consequences and partial
solutions of a generalized unification problem. In: Proc. of LICS 1989. pp. 98–104.
IEEE (1989)
10. Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: The undecidability of the semi-unification
problem. IC 102(1), 83–101 (1993)
11. Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: An analysis of ML typability. JACM 41(2),368–398 (1994)
12. Leiß, H.: Polymorphic recursion and semi-unification. In: Proc. of CSL 1989. LNCS,
vol. 440, pp. 211–224. Springer-Verlag (1990)
13. Leiß, H., Henglein, F.: A decidable case of the semi-unification problem. In: Proc.
of MFCS 1991. LNCS, vol. 520, pp. 318–327. Springer-Verlag (1991)
14. Lushman, B., Cormack, G.V.: A larger decidable semiunification problem. In: Proc.
of PPDP 2007. pp. 143–152. ACM Press (2007)
15. Oliart, A., Snyder, W.: Fast algorithms for uniform semi-unification. JSC 37(4),455–484 (2004)
16. Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. TCS
403(2–3), 307–327 (2008)
17. Pudlák, P.: On a unification problem related to Kreisel’s conjecture. Commentationes Mathematicae Universitatis Carolinae 29(3), 551–556 (1988)
18. Purdom Jr., P.W.: Detecting looping simplifications. In: Proc. of RTA 1987. LNCS,
vol. 256, pp. 54–61. Springer-Verlag (1987)
19. Ružička, P.: An efficient decision algorithm for the uniform semi-unification problem. In: Proc. of MFCS 1991. LNCS, vol. 520, pp. 415–425. Springer-Verlag (1991)