Recurrence Domains: Their Unification and Application to Logic Programming ^{∗}

Hong Chen, Jieh Hsiang Department of Computer Science State University of New York at Stony Brook Stony Brook, NY 11794

July 25, 1991

Abstract

In this paper we present a formalism for finitely representing infinite sets of terms. This formalism, called ρ-terms, enables us to reason finitely about certain recursive types. We present an extension of Horn logic programs, called ρ-Prolog, which allows a finite schematization of infinitely many clauses via predicates with ρ-terms as arguments. We show that for every ρ-Prolog program there is an equivalent Horn logic program. That is, incorporating ρ-terms into first order logic programming does not change its denotational semantics. Computationally, however, ρ-Prolog has the advantages of (1) representing infinitely many answers finitely, (2) avoiding repetition in computation and thus achieving better efficiency, (3) allowing infinite queries, and (4) avoiding certain non-termination of Prolog programs. The ρ-terms play a similar role as regular-trees [MR85] and sort-expressions [Com90] in explicitly defining abstract data types. It differs from the others in that it allows us to define certain non-regular-tree sets such as {(a^{n}, b^{n}, c^{n}) : n ∈ N }. We present a finite and complete algorithm for unification between ρ-terms, with which we can also compute the intersection of the sets defined by ρ-terms.

1 Introduction

In first order logic a term either represents an individual object or, if it contains a variable, an infinite set of objects by ranging its variables over a flat domain, the Herbrand universe. Structured domains, such as the set of tuples {(a^{n}, b^{n}, c^{n}) : n ∈ N }, must be defined explicitly. If the computation requires retrieving a specific value in a structured domain, it is usually obtained through unification, and only one of the values can be dealt with at a time. If infinitely many such values are needed, then non-terminating computation often occurs.

Example 1.1 [CI89] The following program specifies that Toto and Tintin meet their teacher on alternate days.

meets(T + 1, Y) : −meets(T, X), next(X, Y).

∗This work was partially supported by NSF grants INT-8715231, CCR-8805734, and CCR-8901322. A short version of this paper appears in the 18th International Colloquium on Automata, Languages, and Programming.

meets(0, toto).
next(toto, tintin).
next(tintin, toto).

Then the answers to the query Q = {Days : meets(Days, toto)} an infinite set, namely, the set of all even numbers.

This example can be handled by the constraint logic programming language CLP(N) [JL87], where N is the structure of natural numbers. That is, the four clauses can be represented as:

\begin{aligned}meet(X, toto) & : − & X = 2 × Y. \\ meet(X, tintin) & : − & X = 2 × Y + 1. \end{aligned}

where Y is a variable ranging over N. Thus the answers to the query are simply Q = {Days = 2 × Y }.

The example can also be dealt with finitely in Horn logic programming languages with sorts. For instance, if we specify X_{even} and X_{odd} to be sort variables ranging over the sorts of even numbers and odd numbers respectively, the four clauses become:

\begin{matrix}meet(X_{even}, toto). \\ meet(X_{odd}, tintin). \end{matrix}

The answer to the query is then Q = {Days ← X_{even}}.

Several approaches are used to define sorts. They include regular-trees [MR85], sort-expressions [Com90], function declaration [GM84] and term declaration [GM85, Sch89]. Sorted logics based on the first three have decidable term unification, while those based on term declarations do not. For this reason, the existing sorted Horn logic programming languages are based on the function declaration approach. However, as pointed out by Comon [Com89], sorts defined by the first three approaches are regular-tree languages, i.e, the languages accepted by regular-tree automata. Thus when a structured domain is a not a regular-tree language, such as the following example illustrates, it can not be specified by the function declaration mechanism.

Example 1.2 Let a^{n} denote the concatenation of n a’s and • denote the concatenation operator. The following are three programs which differ from each other only on their last facts. Each program is associated with a query.

(1) p(x) : −r(x, y, z), q(z).
(2) r(a, b, c).
(3) r(a • x, b • y, c • z) : −r(x, y, z).
(4) q(c^{20}).  (4’) q(d).  (4”) q(x).
(G) : −p(x).  (G’) : −p(x).  (G”) : −setof(p(x), p(x), S).

In the first example the query p(x) requires 20 backtracking steps through clause (2) in order to get p(a^{20}). In the second example the query p(x) does not terminate due to the infinite backtracking through r(x, y, z), and since none of the bindings for z of r(x, y, z) satisfies q(d). The third example computes the fixpoint of p(x). It does not terminate since there are infinitely many bindings x ← a, x ← a^{2}, x ← a^{3}, ⋯ such that p(x) is true.

As we can see, many of these structured domains are recursive data types whose terms share certain repetitive patterns. For instance, the pattern of tuples {(a^{n}, b^{n}, c^{n}) : n ∈ N } is (a • ⋄_{a}, b • ⋄_{b}, c•⋄_{c}) in the sense that for every tuple (a^{n}, b^{n}, c^{n}) in the domain, (a•a^{n}, b•b^{n}, c•c^{n}) is also in the domain. In this paper we utilize this recurrence relation and represent the above set of tuples as a single expression (Φ(a•⋄, N, a), Φ(b•⋄, N, b), Φ(c•⋄, N, c)) where the first argument of Φ represents the pattern, the third argument represents the base term, and the second serves as a counter. By allowing expressions as such to be part of the language, we are able to schematize certain infinite set of first order terms finitely. We call this extension a ρ-term. (We emphasize that a ρ-term is an abstraction of an infinite set of finite terms. It should not be confused with infinite terms such as used in Prolog II [Col82].)

By allowing the arguments of a predicate to be ρ-terms, we can represent infinitely many Horn clauses finitely. We call this extension ρ-Prolog. ρ-Prolog can be considered as an instance of constraint logic programming CLP(X) [JL87] where X in our case is the first order term algebra with ρ-terms. The constraint solving part is unification between ρ-terms.

We define ρ-terms in section 2. We then give a finite and complete ρ-unification algorithm in section 3. The soundness and correctness of the ρ-unification algorithm is presented in the Appendix. Our algorithm finds a complete set of instantiations of ρ-terms R and L under which the two sets represented by the respective ρ-terms have the largest intersection. The most general unifiers of two ρ-terms are not unique. We also give some complexity for the case of unifying two ground ρ-terms in the Appendix.

Unification of ρ-terms is interesting in its own right. Unification is performed on sets of terms instead of on terms. The ρ-terms are closed under unification. By representing the unifiers of ρ-terms as ρ-terms, a complete set of most general unifiers of two ρ-terms can be obtained finitely. As a special case, the unification algorithm computes the intersection of sets of ground first order terms schematizable by ρ-terms.

In section 4, we give an extension of Horn logic programming to incorporate ρ-terms, and show that logic programming with ρ-terms is equivalent to first order logic programming by giving a transformation which yields a finite set of Horn clauses for each Horn clause with ρ-terms. When SLD-resolution is used as the execution strategy, our formalism becomes ρ-Prolog. ρ-Prolog is discussed in section 5. Although equivalent in denotational semantics, operationally ρ-Prolog has certain advantages over Prolog: Due to the compact representation of recursive types (which in Prolog are represented as part of the program), some backtracking can be eliminated and better efficiency can be achieved. When a query has infinitely many answers, they can be represented finitely in our framework which cannot be done in Prolog. Suppose the least fixpoint of a predicate is infinite, such as is often the case when setof is part of the query, Prolog falls into an infinite loop since it cannot return an infinite answer. In ρ-Prolog, on the other hand, the query may succeed since infinitely many terms can be represented compactly. Examples demonstrating these features are also given in the paper. In the last section we discuss related work.

2 Definitions

Let V denote a countable set of variables and F denote a finite set of function symbols. T (F,V) is the set of terms freely generated from F and V. A substitution is a function mapping δ : V → T (F,V) with δ(x) ≠ x for only a finite subset (denoted by Dom(δ)) of V, and Dom(δ) ∩ V({δ(x) : x ∈ Dom(δ)}) = ∅. The result of applying δ to a term t, denoted by tδ, is the result of replacing every variable x of t by δ(x). Without loss of generality, we denote a substitution δ by a finite set {x←δ(x) : x ∈ Dom(δ)}. A substitution δ is a ground substitution if for all x ∈ Dom(δ), δ(x) is ground. A substitution δ is an empty substitution if Dom(δ) = ∅. Throughout the paper, we reserve ϕ as the empty substitution. The composition σ ∘ δ of two substitutions σ and δ is defined as δ(σ(x)) for each variable x.

A term t has a set of positions P (t) defined as:

1. λ ∈ P (t) where λ denotes the root position.

2. i.u_{i} ∈ P (t) if t = f(t_{1}, ..., t_{i}, ..., t_{n}) and u_{i} ∈ P (t_{i}), where . is concatenation. The length of a position u is defined as |u| = 1 + |u′| if u = i.u′, as 0 if u = λ. The height of a term t is 1 + max({|u| : u ∈ P (t)}). We use t/u to denote the subterm at position u of t and t[u ← s] to denote the term after replacing t/u by s.

2.1 Syntax of ρ-Terms

Definition 2.1 Let F be a finite set of function symbols, V be a countable set of first order variables, Φ be a special function symbol of arity 3, and V_{Φ} be a countable set of variables over natural numbers, which we call degree variables. The set of ρ-terms is defined as the inductive closure of the following:

1. Every variable in V is a ρ-term.

2. If f ∈ F has arity n, and t_{1}, ..., t_{n} are ρ-terms, then f(t_{1}, ..., t_{n}) is a ρ-term.

3. If h[u ← l] is a ground first order term where u is a non-root position of h, and N is a degree variable then Φ(h[u ← ⋄], N, l) is a ρ-term, where ⋄ is a special symbol serving as a place holder.^{1}

Normally we use lowercase letters to denote first order symbols, uppercase letters N, M, Q to denote degree variables and H, L, R to denote ρ-terms . For convenience, we still refer to the first order terms in T (F, V) as terms. We call Φ(h[u ← ⋄], N, l) a generator, or an N-generator when N is emphasized. A ρ-term is ground if it does not contain any first order variables. For instance, f(a, Φ(g(⋄), N, a)) is a ground ρ-term while f(x, Φ(g(⋄), N, a)) is not.

For convenience of discussion, we treat the place holder ⋄ as a special constant. Thus we consider, for instance, f(a, ⋄) as a ground first order term. A ground ρ-term s[u←Φ(h[v←⋄], N, l)] is a ground N-term if s[u←⋄] is a ground first order term. In the following discussion, we often write Φ(h[v←⋄], N, l) as Φ_{N}(h[v←⋄], l).

2.2 Semantics of ρ-Terms

A ρ-term either represents a first order term or an infinite set of first order terms when it contains degree variables. We call a ρ-term with uninstantiated degree variables a proper ρ-term. We use H[N_{1} ← n_{1}..., N_{m} ← n_{m}] to denote the ρ-term obtained from another ρ-term H by instantiating the degree variables N_{1}, ..., N_{m} to natural numbers n_{1}, ..., n_{m} respectively, and then evaluating the instantiated generators Φ(h[u ← ⋄], n, l) to h^{n}[u^{n} ← l] where h^{n}[u^{n} ← l] is an abbreviation of \underbrace{h[u ← h[u ← ...h[u}_{n} ← l]...]. Particularly, h^{0}[u^{0} ← l] = l. Formally, the unfolding is defined as

1In fact we also allow the second argument of Φ to be q ∗N +k, where q and k are natural numbers. The extension is straightforward.

follows:

\begin{matrix}Φ(h[u ← ⋄], n + 1, l) & =^{def} & h[u ← Φ(h[p ← ⋄], n, l)] \\ Φ(h[u ← ⋄], 0, l) & =^{def} & l. \end{matrix}

Example 2.1 f(x, Φ_{N}(g(⋄), a), Φ_{M}(g(⋄), b))[N ← 2, M ← 1] = f(x, g(g(a)), g(b)).

Let V(H) and V_{Φ}(H) denote the set of first order variables and the set of degree variables appearing in a ρ-term H respectively. The set Ω(H) of terms represented by a ρ-term H is

Ω(H) =^{def} {H[N_{1} ← n_{1}, ..., N_{m} ← n_{m}] : n_{1}, ..., n_{m} ∈ N , and {N_{1}, ..., N_{m}} = V_{Φ}(H)}.

Definition 2.2 The elements of Ω(H) are called the constituents of H. The relationship between H and Ω(H) is represented as H ≃ Ω(H).

Example 2.2

f(x, Φ_{N}(g(⋄), a), Φ_{M}(g(⋄), b)) ≃ { f(x, a, b),
f(x, g(a), b), f(x, a, g(b)), f(x, g(a), g(b)),
f(x, g(g(a)), b), f(x, a, g(g(b))), f(x, g(g(a)), g(b)), ...}.

We call Ω(H) a recurrence-domain where H is a ρ-term.

Definition 2.3 Two ρ-terms L and R are strongly equivalent, denoted as L =_{st} R, if and only if L[N_{1} ← n_{1}, ..., N_{m} ← n_{m}] = R[N_{1} ← n_{1}, ..., N_{m} ← n_{m}] for all n_{1}, ..., n_{m} ∈ N where {N_{1}, ..., N_{m}} = V_{Φ}(L) ∪ V_{Φ}(R). Two ground ρ-terms L and R are weakly equivalent, denoted as L =_{wk} R, if and only if Ω(L) = Ω(R).

Example 2.3

f(Φ_{N}(f(⋄), a))  =_{st} Φ_{N}(f(⋄), f(a)),
f(Φ_{N}(f(⋄), a))  ≠_{st} Φ_{M}(f(⋄), f(a)),
g(x, Φ(f(⋄), N, a)) ≠_{st} g(y, Φ(f(⋄), N, a)),
f(Φ_{N}(f(⋄), a))  =_{wk} Φ_{M}(f(⋄), f(a)).

Note that the weakly equivalent relation is only defined on ground ρ-terms. The ρ-terms constitute a subset of recurrence-terms [CHK90] by requiring that no generators are nested in another generator and that generators are ground with respect to the first order variables.

3 A Unification Algorithm for ρ-terms

Unification between two ρ-terms is called ρ-unification. The ρ-unification differs from unification of first order terms in that unifications are performed on sets of terms instead of on terms. It may be the case that one term in a set unifies with several or infinitely many terms in another set, or there are infinitely many terms in one set that unify with infinitely many terms in another set. Not only do we have to answer the question whether there exists a term in one set which unifies with a term in another set, but we also need to have the ability to compute all the terms which are unifiable cross the sets and return those (possibly infinitely many) unified instances finitely. Thus, some of the infinitary unification problems are collapsed into finitary unification problems under our current notion, and much more computational power is achieved.

In this section, we present a set of inference rules which constitutes a ρ-unification algorithm for ρ-terms and show that the set of inference rules is sound, complete and terminating.

3.1 The ρ-unifiers

As we mentioned before, ρ-unification differs from unification of first order terms in that unification is performed among sets of terms instead of terms. Thus, we need a notion to remember which terms in a set unify with terms in another set.

Definition 3.1 Let q and k be integers, N and Q be degree variables, ∗ be the arithmetic multiplication and + be the arithmetic addition in the expression N ← q ∗ Q + k. We call a finite set {N_{1} ← q_{1} ∗ Q_{1} + k_{1}, ..., N_{m} ← q_{m} ∗ Q_{m} + k_{m}} an unfolding substitution if N_{i} ≠ N_{j} for all i ≠ j, and N_{i} ≠ Q_{j} for all i ≠ j. An empty unfolding substitution is denoted as id.

Applying N ← q ∗ Q + k to a ρ-term H is defined as:

Definition 3.2

H[N ← q ∗ Q + k] ≡ \{ \begin{matrix}x & : & H = x, \\ f(s_{1}[N ← q ∗ Q + k], ...s_{n}[N ← q ∗ Q + k]) & : & H = f(s_{1}, ..., s_{n}), \\ Φ_{M} & : & H = Φ_{M}, where M ≠ N, \\ h^{k}[u^{k} ← Φ_{Q}(h^{q}[u^{q} ← ⋄], l)] & : & H = Φ_{N}(h[u ← ⋄], l). \end{matrix}

As a special case, Φ_{Q}(h^{0}[u^{0} ← ⋄], l) = l. Unfolding substitutions serve to select a subset of constituents of a ρ-term.

Example 3.1 Suppose

Φ_{N}(h[u ← ⋄], l) ≃ {s_{i} : s_{i} = h^{i}[u^{i} ← l]}.

\begin{aligned}Φ_{N}(h[u ← ⋄], l)[N ← k] & = & s_{k} & ≃ & \{s_{k}\} \\ Φ_{N}(h[u ← ⋄], l)[N ← q ∗ Q] & = & Φ_{Q}(h^{q}[u^{q} ← ⋄], l) & ≃ & \{s_{0}, s_{q}, s_{2q}, s_{3q}, ...\} \\ Φ_{N}(h[u ← ⋄], l)[N ← q ∗ Q + k] & = & h^{k}[u^{k} ← Φ_{Q}(h^{q}[u^{q} ← ⋄], l)] & ≃ & \{s_{k}, s_{q+k}, s_{2q+k}, s_{3q+k}, ...\}. \end{aligned}

Let us denote the application of an unfolding substitution es to a ρ-term H as H ∘ es.

Definition 3.3

\begin{matrix}H ∘ (\{N ← q ∗ Q + k\} ∪ es) & =^{def} & (H[N ← q ∗ Q + k]) ∘ es, \\ H ∘ id & =^{def} & H. \end{matrix}

Example 3.2 The intersection of Ω(Φ_{N}(f^{2}(⋄), a)) and Ω(Φ_{M}(f^{3}(⋄), a)) is

{a, f^{6}(a), f^{12}(a), f^{18}(a), ...}

where

\begin{aligned}Ω(Φ_{N}(f^{2}(⋄), a)) & = & \{a, f^{2}(a), f^{4}(a), f^{6}(a), ...\}, \\ Ω(Φ_{M}(f^{3}(⋄), a)) & = & \{a, f^{3}(a), f^{6}(a), f^{9}(a), ...\}. \end{aligned}

Applying an unfolding substitution es = {N ← 3 ∗ Q, M ← 2 ∗ Q} to Φ_{M} and Φ_{N}, we obtain

Φ_{N}(f^{2}(⋄), a) ∘ es = Φ_{M}(f^{3}(⋄), a) ∘ es
= Φ_{Q}(f^{6}(⋄), a)
≃ {a, f^{6}(a), f^{12}(a), f^{18}(a), ...}.

Definition 3.4 Let σ be a variable substitution from first order variables to ρ-terms, and es be an unfolding substitution. The pair (σ, es) is called a ρ-substitution.

Applying a ρ-substutution (σ, es) to a ρ-term H, denoted as H ∘ (σ, es), is defined as es(σ(H)), namely to apply σ to H first and then apply es to σ(H).

We normally use Θ, Υ, Γ, etc, to denote ρ-substitutions. For simplicity, we often write σ(H) as H ∘ σ or Hσ, es(H) as H ∘ es, H ∘ Θ as HΘ.

By the definition of a ρ-substitution Θ = (α, es), the intersection of Range_{Φ}(α) and Dom_{Φ}(es) may not be empty. Hence, the equality between (Hα)∘es and (H ∘es)α may not hold as exemplified by the following:

Example 3.3 Let Θ = (α, es) = ({x ← Φ_{N}(s(⋄), 0)}, {N ← 2 ∗ Q}).

(f(x, Φ_{N}(s(⋄), 0))α) ∘ es = f(Φ_{Q}(s^{2}(⋄), 0), Φ_{Q}(s^{2}(⋄), 0)),
(f(x, Φ_{N}(s(⋄), 0)) ∘ es)α = f(Φ_{N}(s(⋄), 0), Φ_{Q}(s^{2}(⋄), 0)).

Clearly, the two resulting ρ-terms represent different sets of terms, since the latter does not reflect the relationship between N and Q. However, there always exists an equivalent ρ-substitution (β, es′) to (α, es) such that Range_{Φ}(β) ∩ Dom_{Φ}(es) = ∅.

Lemma 3.1 Given any ρ-substitution Θ = (α, es). If β = {x ← t ∘ es : x ← t ∈ α}, then for any ρ-term H,

H ∘ (α, es) = (Hβ) ∘ es = (H ∘ es)β.

Proof: Let α = {x_{1}←t_{1}, ..., x_{n}←t_{n}}, and H = H′[u_{11}←x_{1}, ..., u_{1m_{1}}←x_{1}, ⋯, u_{n1}←x_{n}, ..., u_{nm_{n}}←x_{n}] where H′ is the maximal prefix of H which does not contain variables x_{1}, ..., x_{n}.

Now Hα = H′[u_{11}←t_{1}, ..., u_{1m_{1}}←t_{1}, ⋯, u_{n1}←t_{n}, ..., u_{nm_{n}}←t_{n}]. Applying es to Hα, we have

(Hα) ∘ es = H′ ∘ es[u_{11}←t_{1} ∘ es, ..., u_{1m_{1}}←t_{1} ∘ es, ⋯, u_{n1}←t_{n} ∘ es, ..., u_{nm_{n}}←t_{n} ∘ es]
= (H′ ∘ es)[u_{11}←x_{1}β, ..., u_{1m_{1}}←x_{1}β, ⋯, u_{n1}←x_{n}β, ..., u_{nm_{n}}←x_{n}β]
= (H ∘ es)β
= (Hβ) ∘ es : since Range_{Φ}(β) ∩ Dom_{Φ}(es) = ∅.

□

We use es(N) to denote q ∗ Q + k if N←q ∗ Q + k ∈ es, and to denote N otherwise. If

Q←p ∗ M + r ∈ es′ then es′(q ∗ Q + k) =^{def} q ∗ (p ∗ M + r) + k = q ∗ p ∗ M + q ∗ r + k. To separate

degree variables from first order variables, we use Dom_{Φ} and Range_{Φ} to denote the sets of degree variables appearing in the domain and range of a ρ-substitution.

Definition 3.5 The composition es ∘ es′ of two unfolding substitutions is defined as

es ∘ es′(N) =^{def} es′(es(N)) for each degree variable N.

Definition 3.6 The composition of two ρ-substitutions (σ, es) and (δ, es′) is a ρ-substitution (γ̃, ẽs) such that

\begin{aligned}γ̃ & = & \{x←t ∘ ẽs : x←t ∈ γ\} \\ ẽs & = & es ∘ es′ \end{aligned}

where γ = σ ∘ δ.

Example 3.4 The composition of two ρ-substitutions ({x←a, y←Φ_{N}(f(a, ⋄), b)}, id) and ({ϕ, {N←0}) is ({x←a, y←b}, {N←0}).

Lemma 3.2 Variable substitutions, unfolding substitutions and ρ-substitutions are idempotent, namely, α ∘ α = α, es ∘ es = es and Θ ∘ Θ = Θ.

Proof: Let Θ = (α, es) be a ρ-substitution. The lemma follows directly from the definition of variable substitutions and unfolding substitutions where Dom(α) ∩ Range(α) = ∅ and Dom_{Φ}(es) ∩ Range_{Φ}(es) = ∅. □

Definition 3.7 A ρ-substitution (θ, es) is called a ρ-unifier of two ρ-terms L and R if and only if

L ∘ (θ, es) =_{st} R ∘ (θ, es).

The es of a ρ-unifier (θ, es) of L and R is an unfolding-unifier of L and R.

Example 3.5 The ρ-substitution ({x ← g(a)}, {N ← 1}) is a ρ-unifier of f(g(a), Φ_{N}(g(⋄), a)) and f(x, g(a)).

Definition 3.8 A ρ-substitution Θ is more general than another ρ-substitution Υ, denoted as Θ ≤ Υ, if there exists a ρ-substitution Γ such that Υ = Θ ∘ Γ. Θ is strictly more general than Υ, denoted as Θ < Υ, if Θ ≤ Υ but not Υ ≤ Θ.

Example 3.6 The ρ-substitution Θ = ({x←f(y)}, {N←M+1}) is more general than Υ = ({x←f(g(z))}, {N←2Q + 1}) since there is a ρ-substitution Γ = ({y←g(z)}, {M←2Q}) such that Θ = Υ ∘ Γ.

Definition 3.9 A ρ-substitution Θ is a most general ρ-unifier (ρ-mgu) of ρ-terms L and R if no ρ-unifier of L and R is strictly more general than Θ. A set U_{c} of ρ-unifiers of L and R is a complete set of most general ρ-unifiers of L and R if (i) each element of U_{c} is a ρ-unifier of L and R; (ii) for any ρ-unifier Θ, there is a ρ-unifier in U_{c} which is more general than Θ; (iii) no element in U_{c} is more general than any other element in U_{c}. We call the set of unfolding-unifiers {es : (θ, es) ∈ U_{c}} a complete set of most general unfolding-unifiers of L and R.

Example 3.7 Let L = f(x, y) and R = Φ_{N}(f(a, ⋄), f(a, b)) be two ρ-terms. The ρ-substitution Θ = ({x←a, y←Φ_{N}(f(a, ⋄), b)}, id) is a most general ρ-unifier of L and R. Furthermore, {Θ} is a complete set of most general ρ-unifiers of L and R. {id} is the complete set of most general unfolding-unifiers of L and R.

Definition 3.10 A set C of ρ-unifiers of L and R is a complete set of ρ-unifiers of L and R if

1. for any ρ-substitution Ψ = (σ, ẽs) satisfying that L ∘ ẽs = R ∘ ẽs is a constituent of L = R and σ is the most general unifier of L ∘ ẽs and R ∘ ẽs, there exists a Θ ∈ C such that Θ ≤ Ψ;

2. no element in C is more general than another element in C.

A ρ-unifier in C is most general with respect to the first order variables. However, it may not be most general with respect to the degree variables. Nevertheless, according to Definition 4.10, a complete set of ρ-unifiers of L and R covers the set of most general unifiers of the constituents

s =^{?} t in L =^{?} R.

Example 3.8 (Example 4.7 Cont’) The ρ-substitutions Θ_{1} = ({x←a, y←b}, {N←0}) and Θ_{2} = ({x←a,y←Φ_{M}(f(a, ⋄),f(a, b))}, {N←M + 1}) are ρ-unifiers of L and R. However, they are not the most general ones since there exist ρ-substitutions Γ_{1} = ({ϕ, {N←0}) and Γ_{2} = (ϕ, {N←M + 1}) such that Θ_{1} = Θ ∘ Γ_{1}, and Θ_{2} = Θ ∘ Γ_{2}. Nevertheless, {Θ_{1}, Θ_{2}} is complete in the sense that Θ_{1} and Θ_{2} combined together cover all the most general unifiers of the constituents f(x, y) =^{?} f(a, b),

f(x, y) =^{?} f(a, f(a, b)), f(x, y) =^{?} f(a, f(a, f(a, b))), ⋯, of L =^{?} R.

Clearly, a complete set of most general ρ-unifiers of two ρ-terms L and R is also a complete set of ρ-unifiers. As a special case, when both L and R are first-order terms, L and R has a unique complete set of ρ-unifiers, namely the complete set of most general ρ-unifiers.

Two ω-terms may have more than one complete set of ρ-unifiers. For instance, both

{({x←a, y←Φ_{N}(f(a, ⋄), b)}, id)}

and

{({x←a, y←b}, {N←0}), ({x←a, y←Φ_{M}(f(a, ⋄), f(a, b))}, {N←M + 1})}

are complete sets of ρ-unifiers of f(x, y) and Φ_{N}(f(a, ⋄), f(a, b)). According to our definition, the infinite set

{ ({x←a, y←b}, {N←0}),
({x←a, y←f(a, b)}, {N←1}),
({x←a, y←f(a, f(a, b))}, {N←2}),
⋮
}

is also a complete set of ρ-unifiers of f(x, y) and Φ_{N}(f(a, ⋄), f(a, b)).

In this paper, we will give an algorithm which computes a finite and complete set of ρ-unifiers of ρ-terms.

Lemma 3.3 Let L be a ρ-term, Θ and Ψ be two ρ-substitutions, then

(L ∘ Θ) ∘ Ψ = L ∘ (Θ ∘ Ψ).

Proof: Follows directly from the definitions of composition and application of ρ-substitutions. □

3.2 Two Special Cases of ρ-unification

Before we give the general algorithm we consider two special cases of ρ-unification for which a complete set of most general unifiers can be obtained. They are unifying between two ground Nterms L and R, and unifying between a ground N-term L and an M-generator R where N and M are different degree variables. The first case is equivalent to checking for which i, L[N ← i] = R[N ← i]. The latter is equivalent to computing the intersection of Ω(L) and Ω(R).

3.2.1 The ρ-unification of Ground N-terms

In this section, we study the ρ-unification of two ground N-terms. Let L = s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] and R = Φ_{N}(h_{2}[u_{2}←⋄], l_{2}) be two ground N-terms. Let CUU(L, R) denote a complete set of most general unfolding-unifiers of L and R. Let the set of terms represented by L and R be

\begin{aligned}L & ≃ & \{s_{i} : s_{i} = L[N←i]\}, \\ R & ≃ & \{t_{i} : t_{i} = R[N←i]\}. \end{aligned}

The following algorithm computes CUU(L, R). The correctness of the algorithm is given in Appendix A.

if |u_{1}| > |u_{2}|: CUU(L, R) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}} where

p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{2}|, |u_{1}| − |u_{2}|)⌉.

if |u_{1}| = |u_{2}|: Let p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{1}|, |u_{2}|)⌉.

(1) If s_{p} = t_{p}, then CUU(L, R) = {id}.
(2) If s_{p} ≠ t_{p}, then CUU(L, R) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}}.

if |u_{1}| < |u_{2}|: Let r be the minimal integer such that L′ = L[N←Q + r] and R′ = R[N←Q + r] satisfy: either (1) the prefixes of L′ and R′ do not match; or (2) L′ = s′[u′←Φ_{Q}(h_{1}[u_{1}←⋄], l_{1})],

R′ = s′[u′←s′′[u′′←Φ_{Q}(h_{2}[u_{2}←⋄], l_{2})]].
if (1) CUU(L, R) = {{N←i} : 0 ≤ i < r, s_{i} = t_{i}}.
if (2) CUU(L, R) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}} where
p = ⌈max(height(s_{r+1}), height(t_{r+1}))/min(|u_{1}|, |u_{2}| − |u_{1}|)⌉.

Example 3.9 Let

\begin{matrix}L = g(Φ_{N}(g^{2}(⋄), a)) \\ R = Φ_{N}(g(⋄), g^{2}(a)). \end{matrix}

It falls into the case |u_{1}| = 2 > |u_{2}| = 1. We see that s_{1} = g^{3}(a), t_{1} = g^{3}(a), height(s_{1}) = height(t_{1}) = 4, and p = 4. The CUU(L, R) = {{N←1}}.

Example 3.10 Let

\begin{matrix}L = g(Φ_{N}(g(⋄), a)) \\ R = Φ_{N}(g(⋄), a). \end{matrix}

It falls into the case where |u_{1}| = |u_{2}| = 1. We see that s_{1} = g^{2}(a), t_{1} = g(a), height(s_{1}) = 3, height(t_{1}) = 2, and p = 3. It falls into the case where s_{p} ≠ t_{p}. The CUU(L, R) = ∅.

Example 3.11 Let

\begin{matrix}L = g(Φ_{N}(f(g(⋄)), a)) \\ R = Φ_{N}(g(f(⋄)), g(a)). \end{matrix}

It falls into the case where |u_{1}| = |u_{2}| = 2. We see that s_{1} = g(f(g(a))), t_{1} = g(f(g(a))), height(s_{1}) = 4, height(t_{1}) = 4, and p = 2. It falls into the case where s_{p} = t_{p}. The CUU(L, R) = {id}, which implies that for every i, s_{i} = t_{i}.

Example 3.12 Let

\begin{matrix}L = f(Φ_{N}(f(a, ⋄), a), a) \\ R = Φ_{N}(g^{2}(⋄), f(a, a)). \end{matrix}

It falls into the case where |u_{1}| = 1 < |u_{2}| = 2. Note that there is a mismatch at the prefixes of L[N←Q + 1] and R[N←Q + 1]:

\begin{matrix}L[N←Q + 1] = f(f(a, Φ_{Q}(f(a, ⋄), a)), a) \\ R[N←Q + 1] = g^{2}(Φ_{Q}(g^{2}(⋄), f(a, a))). \end{matrix}

It then falls into the subcase (1). The r is 1 and CUU(L, R) = {{N←0}}.

Example 3.13 Let

\begin{matrix}L = g(Φ_{N}(g(⋄), a)) \\ R = Φ_{N}(g^{2}(⋄), a). \end{matrix}

It falls into the case where |u_{1}| = 1 < |u_{2}| = 2. From

\begin{matrix}L[N←Q + 1] = g^{2}(Φ_{Q}(g(⋄), a)) \\ R[N←Q + 1] = g^{2}(Φ_{Q}(g^{2}(⋄), a)). \end{matrix}

we see that r = 1, s_{r+1} = g^{3}(a), t_{r+1} = g^{4}(a), height(s_{r+1}) = 4, height(t_{r+1}) = 5, and p = 5. It falls into the subcase (2). The CUU(L, R) = {{N←1}}.

Proposition 3.1 If there are infinitely many i′s such that s_{i} = t_{i}, then for every i, s_{i} = t_{i}, and L and R has a unique most general unfolding-unifier id.

Sketch of the proof: If there are infinitely many i’s such that s_{i} = t_{i}, then it has to be the case where |u_{1}| = |u_{2}|. We then show that s_{p} = t_{p} follows where p is given in the above algorithm. It then follows that the CUU(L, R) is id, which is clearly unique.

The proof is similar to the proof of Lemma 8.2. □

Although we have shown that two ground N-terms have a unique unfolding-unifier if they have infinitely many unified instances, the following example shows that this is not true in the finite case.

Example 3.14 Let L = f(Φ_{N}(f(a, ⋄), a), a) and R = Φ_{N}(f(⋄, a), f(a, a)). It can be shown that {{N←0}, {N←1}} is a complete set of most general unfolding-unifiers of L and R.

Lemma 3.4 The time complexity of computing the complete set CUU(L, R) of most general unfoldingunifiers of two ground N-terms L and R is bounded by O(n^{3}) where n is the number of occurrences of symbols in s_{1} and t_{1}. The size of CUU(L, R) is bounded by 3m where m is the maximal height of s_{1} and t_{1}.

Proof: See Appendix A. □

Although we have shown that there may be several most general unfolding-unifiers between two ground N-terms, we are only able to construct examples with at most two most general unfoldingunifiers. We conjecture that two is actually the maximal number of most general unfolding-unifiers for two ground N-terms. When s_{0} ≠ t_{0}, the most general unfolding-unifier is conjectured to be unique.

3.2.2 The ρ-unification of a ground N-term and a M-generator

In this section, we assume that N and M are distinct degree variables. For convenience, in this section we denote Φ_{N}(h_{1}[u_{1}←⋄], l_{1}) and Φ_{M}(h_{2}[u_{2}←⋄], l_{2}) as Φ_{N} and Φ_{M} respectively.

Let

\begin{aligned}s[u←Φ_{N}] & ≃ & \{s_{i} : s_{i} = s[u←Φ_{N}[N←i]]\} \\ Φ_{M} & ≃ & \{t_{j} : t_{j} = Φ_{M}[M←j]\}. \end{aligned}

Again, we use CUU(L, R) to denote the complete set of most general unfolding-unifiers of two ρ-terms L and R.

The unification between a ground N-term and a ground M-term is more complicated than that between two ground N-terms because the N-generator and the M-generator can be unfolded independently.

Since it is easy to check whether a ground term is a constituent of a ρ-term, a naive algorithm for checking whether L and R are unifiable is to solve the following unification problems:

s_{0} =^{?} R, L =^{?} t_{0}, s_{1} =^{?} R, L =^{?} t_{1}, ⋯

If L and R are unifiable, then at least one of s_{i} =^{?} R or L =^{?} t_{i} must be unifiable. We can represent such an algorithm as a set of inference rules where each rule has the form

\frac{S, es}{S′, es′} or \frac{S, es}{□}

where S is a set of equations L =^{?} R of ρ-terms to be solved, and es is an unfolding substitution. Note that we assume that S contains at most one N-generator and one M-generator.

Naive Inference Rules

(Decompose):

\frac{\{f(s_{1}, ..., s_{n}) =^{?} f(t_{1}, ..., t_{n})\} ∪ S, es}{\{s_{1} =^{?} t_{1}, ..., s_{n} =^{?} t_{n}\} ∪ S, es}

(Fail):

\frac{\{f(s_{1}, ..., s_{n}) =^{?} g(t_{1}, ..., t_{m})\} ∪ S, es}{□}

(Initiate):

\frac{\{Φ_{N}(h[u ← ⋄], l) =^{?} R\} ∪ S, es}{\{l =^{?} R\} ∪ S, es ∘ \{N ← 0\}}

(Unfold):

\frac{\{Φ_{N}(h[u ← ⋄], l) =^{?} R\} ∪ S, es}{\{h[u←Φ_{Q}(h[u ← ⋄], l)] =^{?} R\} ∪ S, es ∘ \{N ← Q + 1\}}

To unify L and R, we start with ({L =^{?} R}, id).

Example 3.15

s(Φ_{N}(s^{2}(⋄), s(0))) =^{?} Φ_{M}(s^{2}(⋄), 0)

⇒^{Unfold} s(Φ_{N}(s^{2}(⋄), s(0))) =^{?} s^{2}(Φ_{M}(s^{2}(⋄), 0)) : M←M_{1} + 1
⇒^{Decompose} Φ_{N}(s^{2}(⋄), s(0)) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), 0))  :
⇒^{Initiate} s(0) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), 0))  : N←0
⇒^{Decompose} 0 =^{?} Φ_{M_{1}}(s^{2}(⋄), 0)
⇒^{Initiate} 0 =^{?} 0  : M_{1}←0
⇒^{Decompose} succeed

An unfolding-unifier {N←0, M←1} is obtained.

However, this naive algorithm may return infinitely many unfolding-unifiers when the intersection of Ω(L) and Ω(R) is an infinite set, and it may not terminate even if L and R do not unify.

Example 3.16 The most general unfolding-unifier of s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)) is {M←Q, N←Q}. However, if we apply unfolding and decomposition alternatively, an infinite derivation occurs:

s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0))

⇒^{Unfold} s(Φ_{N}(s^{2}(⋄), 0)) =^{?} s^{2}(Φ_{M}(s^{2}(⋄), s(0))) : M←M_{1} + 1
⇒^{Decompose} Φ_{N}(s^{2}(⋄), 0) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), s(0)))
⇒^{Unfold} s^{2}(Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), s(0))) : N←N_{1} + 1
⇒^{Decompose} s(Φ_{N_{1}}(s^{2}(⋄), 0)) =^{?} Φ_{M_{1}}(s^{2}(⋄), s(0))
⇒^{Unfold} ...

Notice that up to the renaming of degree variables, the initial equation we try to solve occurs again after p and q steps of unfolding N and M. If we can show that for some i < p, s_{i} = t_{j} for some j or for some j < q, s_{i} = t_{j} for some i, then we can infer that the intersection of Ω(s[u←Φ_{N}]) and Ω(Φ_{M}) is infinite. Furthermore, {N←p∗Q+i, M←q ∗Q+j} is an unfolding-unifier of s[u←Φ_{N}] and Φ_{M}. In this example, both p and q are 1, and s_{0} = t_{0}. It follows that {N←1 ∗ Q + 0, M←1 ∗ Q + 0}, namely, {N←Q, M←Q} is an unfolding-unifier of s(Φ_{N}(s^{2}(⋄), 0)) and Φ_{M}(s^{2}(⋄), s(0)).

Example 3.17 s(Φ_{N}(s^{2}(⋄), 0)) and Φ_{M}(s^{2}(⋄), a) do not unify. However, if we apply unfolding and decomposition alternatively, an infinite derivation occurs:

s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), a)

⇒^{Unfold} s(Φ_{N}(s^{2}(⋄), 0)) =^{?} s^{2}(Φ_{M}(s^{2}(⋄), a)) : M←M_{1} + 1
⇒^{Decompose} Φ_{N}(s^{2}(⋄), 0) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), a))
⇒^{Unfold} s^{2}(Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), a)) : N←N_{1} + 1
⇒^{Decompose} s(Φ_{N_{1}}(s^{2}(⋄), 0)) =^{?} Φ_{M_{1}}(s^{2}(⋄), a)
⇒^{Unfold} ...

More generally, it may not be the initial equation which occurs twice in a possible infinite derivation. Rather it is some intermediate equation which occurs twice. Using the pigeonhole principle, it can be shown that after some finite number of unfolding and decomposition, a loop does occur if the intersection of Ω(s[u←Φ_{N}]) and Ω(Φ_{M}) is infinite. The following picture shows the derivation: (decomposition is performed and does not show up in the following diagram.)

s[u←Φ_{N}]  =^{?} Φ_{M}
⇓ k_{N} unfoldings  ⇓ k_{M} unfoldings
s′[u′←Φ_{N′}] =^{?} s′′[u′′←Φ_{M′}]
⇓ p unfoldings  ⇓ q unfoldings
s′[u′←Φ_{N′′}]  =^{?} s′′[u′′←Φ_{M′′}]

where at least one of u′ and u′′ is λ. Let p and q be the smallest numbers with above property, and no Φ_{N} =^{?} Φ_{M} is generated intermediately. If for some r_{N} < p and r_{M} < q, s′[u′←Φ_{N}][N←r_{N}] = s′′[u′′←Φ_{M}][M←r_{M}], clearly, {N←p ∗ Q + k_{N} + r_{N}, M←q ∗ Q + k_{M} + r_{M}} is an unfolding-unifier of s[u←Φ_{N}] and Φ_{M}.

Without loss of generality, let us assume that u′′ = λ. Let s′_{i} denote s′[u′←Φ_{N}][N←i] and t′_{i} denote Φ_{M}[M←i]. Together with the set of unfolding-unifiers {{N←i, M←j} : i < k_{N} or j < k_{M}}, we obtain a complete set of unfolding-unifiers for s[u←Φ_{N}] and Φ_{M}.

From these examples, we observe that what this naive algorithm lacks is the consideration of the recurring patterns and structural properties of L and R.

Definition 3.11 A history set A of ρ-unification is a set of equations s[u←Φ_{N}] =^{?} Φ_{M} or Φ_{N} =^{?} s[u←Φ_{M}] where u can be an empty position λ.

Definition 3.12 Let A be a history set. We denote

A ⊢ (s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] =^{?} Φ_{M}(h_{2}[u_{2}←⋄], l_{2}), p, q)

if

1. there is a renaming unfolding substitution es = {N←N′, M←M′} such that

s[u←Φ_{N′}(h_{1}[u_{1}←⋄], l_{1})] ∘ es =^{?} Φ_{M′}(h_{2}[u_{2}←⋄] ∘ es, l_{2}) ∈ A,

and

2. p and q are the minimal number of unfoldings with respect to N′ and M′ between the occur-

rences of s[u←Φ_{N′}(h_{1}[u_{1}←⋄], l_{1})]∘=^{?} Φ_{M′}(h_{2}[u_{2}←⋄], l_{2}) and s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})]=^{?} Φ_{M}(h_{2}[u_{2}←⋄], l_{2}).

More precisely, N′ = N + p and M′ = M + q.

The integers p and q are used to remember the minimal number of unfoldings of s[u←Φ_{N}] and Φ_{M} between two possible occurrences of s[u←Φ_{N}] =^{?} Φ_{M}. For instance, both p and q are 1 in Example 4.16.

The inference rules for a ground N-term and a ground M-term has the form

\frac{A, S, es}{S′, es′} or \frac{A, S, es}{□}

where A is a history set, S is a set of equations L =^{?} R of ρ-terms to be solved, and es is an unfolding substitution. Note that S contains at most two degree variables, one of them is N and the other is M.

Inference Rules for a Ground N-term and a Ground M-term

(Decompose):

\frac{A, \{f(s_{1}, ..., s_{n}) =^{?} f(t_{1}, ..., t_{n})\} ∪ S, es}{A, \{s_{1} =^{?} t_{1}, ..., s_{n} =^{?} t_{n}\} ∪ S, es}

(Fail):

\frac{A, \{f(s_{1}, ..., s_{n}) =^{?} g(t_{1}, ..., t_{m})\} ∪ S, es}{□}

(Initiate):

\frac{A, \{L =^{?} Φ_{M}(h[u ← ⋄], l)\} ∪ S, es}{A, \{L =^{?} l\} ∪ S, es ∘ \{M ← 0\}}

(Unfold):

\frac{A, \{L =^{?} Φ_{M}(h[u ← ⋄], l)\} ∪ S, es}{A′, \{L =^{?} h[u←Φ_{Q}(h[u ← ⋄], l)]\} ∪ S, es ∘ \{M ← Q + 1\}}

where

• A ⊬ (L =^{?} Φ_{M}(h[u ← ⋄], l), p, q)
• if L is a ground N-term, then

A′ = A ∪ {L =^{?} Φ_{M}(h[u ← ⋄], l)}

else A′ = A

(Succeed):

\frac{A, \{s[u←Φ_{N}(h_{1}[u_{1} ← ⋄], l_{1})] =^{?} Φ_{M}(h_{2}[u_{2} ← ⋄], l_{2})\} ∪ S, es}{A, S, es ∘ \{N ← p ∗ Q + k, M←q ∗ Q + r\}}

where

• A ⊢ (s[u←Φ_{N}(h[u ← ⋄], l)] =^{?} Φ_{M}(h_{2}[u_{2} ← ⋄], l_{2}), p, q)
•

either (i) ∃k < p such that s_{k} = t_{r} for some r
or (ii) ∃r < q such that s_{k} = t_{r} for some k

To unify s[u←Φ_{N}] and Φ_{M}, we start with (∅, {s[u←Φ_{N}] =^{?} Φ_{M}}, id).

Example 3.18 (Example 4.16 Cont’)

A = ∅

S = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0))}

es = id

⇓ Unfold

A = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0))}

S = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} s^{2}(Φ_{M}(s^{2}(⋄), s(0)))}

es = {M←M_{1} + 1}

⇓ Decompose

A = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0))}

S = {Φ_{N}(s^{2}(⋄), 0) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), s(0)))

es = {M←M_{1} + 1}

⇓ Unfold

A = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)), Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M}(s^{2}(⋄), s(0)))}

S = {s^{2}(Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M_{1}}(s^{2}(⋄), s(0)))}

es = {M←M_{1} + 1, N←N_{1} + 1}

⇓ Decompose

A = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)), Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M}(s^{2}(⋄), s(0)))}

S = {s(Φ_{N_{1}}(s^{2}(⋄), 0)) =^{?} Φ_{M_{1}}(s^{2}(⋄), s(0))}

es = {M←M_{1} + 1, N←N_{1} + 1}

⇓ Succeed

A = {s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)), Φ_{N}(s^{2}(⋄), 0)) =^{?} s(Φ_{M}(s^{2}(⋄), s(0)))}

S = ∅

es = {M←Q + 1, N←Q + 1}

When the Succeed rule is applied, we have a = b = 1, s_{0} = t_{0}, namely k = r = 0. It then follows that M_{1} = b ∗ Q + r = Q and N_{1} = a ∗ Q + k = Q. The composition {M←M_{1} + 1, N←N_{1} + 1} ∘ {M_{1}←Q, N←Q} is {M←Q + 1, N←Q + 1}. Another unfolding-unifier of s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)) computed by applying Initiate Rule is {M←0, N←0}. In this example, our inference algorithm does not yield a complete set of most general unfolding-unifiers. Nevertheless, it computes a complete set of unfolding-unifiers {{N←0, M←0}, {N←Q + 1, M←Q + 1}}.

A complete set C of unfolding-unifiers of s[u←Φ_{N}] and Φ_{M} can be transformed into a complete set of most general unfolding-unifiers of s[u←Φ_{N}] and Φ_{M}.

If each of the unfolding-unifier in C has the form {N←i, M←j}, then clearly C is a set of most general unfolding-unifiers. Now let us assume that es = {N←p ∗ Q + k, M←q ∗ Q} is in C. Let

\begin{aligned}k & = & n ∗ p + k′ & : & 0 ≤ k′ < p, \\ r & = & m ∗ q + r′ & : & 0 ≤ r′ < q. \end{aligned}

We know that s_{k} = t_{r}. Thus, if one of n and m is 0, then clearly C is a most general set. Otherwise, we will check whether s_{k′′} = t_{r′′} where k′′ = (n − 1) ∗ p + k′ and r′′ = (m − 1) ∗ q + r′. If it is true, then C′ = C ∪{{N←p∗Q+k′′, M←q ∗Q+r′′}} - {{N←p∗Q+k, M←q ∗Q+r}} As we can see, this process deletes {N←p∗Q+p+k′′, M←q∗Q+q+r′′} from C and adds {N←p∗Q+k′′, M←q∗Q+r′′}, which is more general than the one being deleted. We then delete those {N←i, M←j} that are less general than {N←p ∗ Q + k′′, M←q ∗ Q + r′′}. Clearly, this process terminates and results in a complete set of most general unfolding-unifiers of s[u←Φ_{N}] and Φ_{M}.

Example 3.19 As we have seen, C = {{N←0, M←0}, {N←Q + 1, M←Q + 1}} is a complete set of unfolding-unifiers of s(Φ_{N}(s^{2}(⋄), 0)) =^{?} Φ_{M}(s^{2}(⋄), s(0)). In {N←Q + 1, M←Q + 1}, p = q = 1, k = r = 1 and k′ = r′ = 0. Now k′′ = r′′ = 0. Since s_{0} = t_{0}, according to the algorithm we just described above, we delelete {N←Q + 1, M←Q + 1} from C and add {N←Q, M←Q} to C. Since {N←0, M←0} is less general than {N←Q, M←Q}, we delete {N←0, M←0} from C. The algorithm terminates and returns {{N←Q, M←Q}} which is the complete set of most general set.

The correctness of the above inference rules for unifying s[u←Φ_{N}] and Φ_{M} is shown in Appendix A.

Lemma 3.5 Ω(s[u←Φ_{N}]) ∩ Ω(Φ_{M}) is infinite, s[u←Φ_{N}] and Φ_{M} have a unique most general unfolding-unifier.

Proof: Follows from Lemma 8.6 when u is the root position λ, and Lemma 8.9 in the general case. □

When Ω(s[u←Φ_{N}]) ∩ Ω(Φ_{M}) is finite, the most general ρ-unifiers of s[u←Φ_{N}] and Φ_{M} may not be unique.

Example 3.20 Let L = f(Φ_{N}(f(a, ⋄), a), a) and R = Φ_{M}(f(⋄, a), f(a, a)). It can be shown that {{N←0, M←0}, {N←1, M←1}} is a complete set of most general unfolding-unifiers of L and R.

Lemma 3.6 The time complexity of computing CUU(Φ_{N}, Φ_{M}) is bounded by O(n^{3}) where n is the number of occurrences of symbols in s_{1} and t_{1}. The size of CUU(Φ_{N}, Φ_{M}) is bounded by m where m is the maximal height of s_{1} and t_{1}.

Proof: See Appendix A. □

We can informally summarize the lemmas in the previous two sections as the following corollary.

Corollary 3.1 The ρ-unification of two ground N-terms L and R is decidable. If they are ρunifiable then they have a computable finite, complete set of most general unfolding-unifiers. The same is true for the ρ-unification of two ρ-terms s[u←Φ_{N}] and Φ_{M}.

3.3 Inference Rules of ρ-Unification

We now define a ρ-unification algorithm via a set of inference rules. Each rule will be of the form

\frac{S, es}{S′, es′} or \frac{S, es}{□}

where S is a set of equations L =^{?} R of ρ-terms to be solved, and es is an unfolding substitution which also controls the application of inference rules. We call the tuple (S, es) a configuration. For instance, inference rule U1 can only be applied when the second component of the configuration is empty. The symbol □ denotes failure, and S′, and es′ are the results after applying an inference rule.

We call one step of application of inference rules as one step of a ρ-unification derivation and denote it by ⊢. We use ⊢^{∗} to denote zero or more steps of ρ-unification derivations. For simplicity, we intentionally leave out the collection of variable substitutions and unfolding substitutions in a derivation. In the following, we do not distinguish between L =^{?} R and R =^{?} L.

U1 (Replace):

\frac{\{L =^{?} x\} ∪ S, ∅}{S[x ← L], ∅} if x is not a proper subterm of L

U2 (Delete):

\frac{\{L =^{?} L\} ∪ S, ∅}{S, ∅}

U3 (Decompose):

\frac{\{f(s_{1}, ..., s_{n}) =^{?} f(t_{1}, ..., t_{n})\} ∪ S, ∅}{\{s_{1} =^{?} t_{1}, ..., s_{n} =^{?} t_{n}\} ∪ S, ∅}

U4 (Occurs-check):

\frac{\{s[x] =^{?} x\} ∪ S, ∅}{□}

U5 (Fail):

\frac{\{f(s_{1}, ..., s_{n}) =^{?} g(t_{1}, ..., t_{m})\} ∪ S, ∅}{□}

\frac{\{f(s_{1}, ..., s_{n}) =^{?} Φ_{N}(h[u ← ⋄], l)\} ∪ S, ∅}{\{f(s_{1}, ..., s_{n}) =^{?} l\} ∪ S, \{N ← 0\}}

\frac{\{f(s_{1}, ..., s_{n}) =^{?} Φ_{N}(h[u ← ⋄], l)\} ∪ S, ∅}{\{f(s_{1}, ..., s_{n}) =^{?} Φ_{N}(h[u ← ⋄], l)\} ∪ S, \{N ← Q + 1\}}

U6 (Initiate): If f(s_{1}, ..., s_{n}) is neither a ground N-term nor a ground M-term, U7 (Unfold): If f(s_{1}, ..., s_{n}) is neither a ground N-term nor a ground M-term, U8 (MN-succeed): If a ground N-term s[u←Φ_{N}(h_{N}[u_{N}←⋄], l_{N})] and Φ_{M}(h_{M}[u_{M}←⋄], l_{M})

have a non-empty complete set CUU of most general unfolding-unifiers

(N and M may be the same degree variable),

\frac{\{s[u←Φ_{N}(h_{N}[u_{N}←⋄], l_{N})] =^{?} Φ_{M}(h_{M}[u_{M}←⋄], l_{M})\} ∪ S, ∅}{S, U} where U ∈ CUU

U9 (MN-fail): A ground N-term s[u←Φ_{N}(h_{N}[u_{N}←⋄], l_{N})] and Φ_{M}(h_{M}[u_{M}←⋄], l_{M})

are not ρ-unifiable (N and M may be the same degree variable),

\frac{\{s[u←Φ_{N}(h_{N}[u_{N}←⋄], l_{N})] =^{?} Φ_{M}(h_{M}[u_{M}←⋄], l_{M})\} ∪ S, ∅}{□}

U10 (Transform) :

\frac{S, \{N ← q ∗ Q + k\} ∪ U}{S[N ← q ∗ Q + k], U}

Definition 3.13 We call a derivation of the form (S, ∅) ⊢^{∗} (∅, ∅) a successful ρ-unification derivation of S, and (S, ∅) ⊢^{∗} □ a failed ρ-unification derivation. The ρ-substitution (θ, es) is called a ρ-unifier associated with D_{S} if θ and es are compositions θ = {x_{1} ← t_{1}} ∘ ... ∘ {x_{n} ← t_{n}} and es = U_{1} ∘ ... ∘ U_{m} of variable substitutions and unfolding-substitutions collected in a successful ρ-unification derivation D_{S} of S.

Example 3.21

{f(x, Φ_{N}(s^{2}(⋄), 0)) =^{?} f(Φ_{M}(s(⋄), s(0)), Φ_{M}(s(⋄), 0))}

⇒^{U3} : {x←Φ_{M}(s(⋄), s(0)), Φ_{N}(s^{2}(⋄), 0) =^{?} Φ_{M}(s(⋄), 0)}
⇒^{U1} {Φ_{N}(s^{2}(⋄), 0) =^{?} Φ_{M}(s(⋄), 0)}  : θ_{0} = {x←Φ_{M}(s(⋄), s(0))}
⇒^{U8} ∅  : es_{0} = {N←Q, M←2Q}

The ρ-substitution associated with above derivation is ({x←Φ_{M}(s(⋄), s(0))}, {N←Q, M←2Q}), which is equal to ({x←Φ_{Q}(s^{2}(⋄), s(0))}, {N←Q, M←2Q}). It is not difficult to see that {({x←Φ_{Q}(s^{2}(⋄), s(0))}, {N←Q, M←2Q})} is a complete set of most general ρ-unifiers of f(x, Φ_{N}(s^{2}(⋄), 0)) and f(Φ_{M}(s(⋄), s(0)), Φ_{M}(s(⋄), 0))

To prove the termination of the algorithm, we need to define a well-founded ordering and show that the complexity measure decreases when the inference rules are applied. We first define a well-founded ordering. Let MP_{V}(s) denote the multiset of the lengths of positions at which first order variables occur in a ρ-term s. For instance, MP_{V}(f(x, g(x, y, Φ_{N}(g(⋄), b)))) = {1, 2, 2}. Let MP_{Φ}(s) denote the multiset of the lengths of shared maximal path between any two generators. For instance,

MP_{Φ}(g(Φ_{N}, Φ_{M}))  = {0},
MP_{Φ}(f(Φ_{N}, g(Φ_{M}, Φ_{N}))) = {0, 0, 1},
MP_{Φ}(f(a, g(Φ_{N}, h(Φ_{M}))) = {1}.

In the case where s contains at most one generator, MP_{Φ}(s) is the empty set ∅.

For a ρ-term s, the sets MP_{V}(s) and MP_{Φ}(s) are invariant in the sense:

Proposition 3.2 For every ρ-term L, and an unfolding-substitution {N←q ∗ Q + k},

\begin{aligned}MP_{V}(L) & = & MP_{V}(L[N←q ∗ Q + k]) \\ MP_{Φ}(L) & = & MP_{Φ}(L[N←q ∗ Q + k]) \end{aligned}

Proof: Trivial. □

We associate with each configuration (S, U) a complexity measure (A, B, C, D, E, F) where

• A is the number of distinct unsolved first order variables appearing in S,

• B is the number of generators appearing in S,

• C is the size of U,

• D = ⋃_{L=^{?}R∈S}(MP_{V}(L) ∪ MP_{V}(R)),

• E = ⋃_{L=^{?}R∈S}(MP_{Φ}(L) ∪ MP_{Φ}(R)),

• F = {L̄, R̄ : L =^{?} R ∈ S and L̄ and R̄ are the results of replacing every generator term of L and R by a special constant c}.

We order the measure (A, B, C, D, E, F) by the well-founded lexicographic ordering whose first, second, and third arguments are ordered by the ordering >_{N} on natural numbers, fourth and fifth arguments are ordered by the multiset ordering ≫_{N} on integers, and sixth argument is ordered by the multiset ordering ≫_{sub} of the subterm ordering. The ordering can be rewritten as (>_{N} , >_{N} , >_{N} , ≫_{N} , ≫_{N} , ≫_{sub}).

Theorem 3.1 (Termination) The ρ-unification derivation ⊢ is well-founded. In other words, any derivation starting from ({L =^{?} R}, ∅) must terminate.

Proof: We assume that the complexity measure associated with the current configuration ({L =^{?} R} ∪ S_{0}, ∅) is (A, B, C, D, E, F).

The following table shows that the application of every rule strictly decreases the complexity measure of the current configuration (S, U). For instance, the table says after U10 is applied, the arguments A and B either decrease or unchange according to the corresponding ordering associated with A and B. The argument C decreases. The entry X denotes don’t care, since the entry is irrelevant with respect to the ordering. In the following, the rule U3 is discussed in three different cases where

U3^{a} : L =^{?} R contains first order variables. U3^{b} : U3^{a} is not true and L or R contains more than one generators. U3^{c} : Neither U3^{a} nor U3^{b} is true, namely L and R are ground and each has at most one generator.

A B C  D  E F
U4, U5, U9  failure
U1 > X X  X  X X
U2 ≥ ≥ =  ≥  ≥ >
U6, U8 ≥ > X  X  X X
U10 ≥ ≥ >  X  X X
U3^{a} ≥ ≥ =  >  X X
U3^{b} ≥ ≥ =  ≥  > X
U3^{c} ≥ ≥ =  ≥  ≥ >

If U4, U5 and U9 can be applied, then it means that the ρ-unification fails. Clearly the algorithm terminates. While it is easy to check that any application of the rest of rules decreases the measure, the rule U7 needs further discussions. By the nature of the inference rules, U10 must be applied after U7. Then either U3^{a} or U3^{b} must be applied. Let the complexity measure be (A, B, C, D, E, F) before U7 is applied. After U7 is applied, the measure is (A, B, C_{1}, D, E, F). Note that C_{1} >_{N} C and other arguments remain the same. By Proposition 4.2, after U10 is applied, the C_{1} is decreased into C again, and the measure is (A_{1}, B_{1}, C, D, E, F). Note that A_{1} ≤_{N} A and B_{1} ≤_{N} B. In the case of U3^{a}, we have D decreased and in the case of U3^{b} we have E decreased. The above arguments can be picturized by the following table:

A B C D E F
U7 ⇒ U10 ⇒ U3^{a} ≥ ≥ = > X X
U7 ⇒ U10 ⇒ U3^{b} ≥ ≥ = ≥ > X
□

Theorem 3.2 (Soundness) If {L =^{?} R} has a successful ρ-unification derivation with an associated ρ-unifier Θ then Θ is a ρ-unifier of L and R.

Proof: Follows directly from Lemma 9.1 when the initial configuration is ({L =^{?} R}, ∅). For the proof of Lemma 9.1, consult Appendix B. □

Theorem 3.3 (Completeness) The set of ρ-unifiers of two ρ-terms L and R computed by the ρ-unification algorithm constitutes a complete set of ρ-unifiers of L and R.

Proof: The first condition in the definition of a complete set of ρ-unifiers is clearly satisfied. This follows directly from lemma 9.2 when the initial configuration is ({L =^{?} R}, ∅). For the proof of lemma 9.2, consult Appendix B.

To show that the second condition in the definition of a complete set of ρ-unifiers is satisfied, we argue that if our algorithm generates two distinct ρ-unifiers Θ_{1} and Θ_{2}, then none of which is more general than another.

Let U_{i_{1}}, ⋯, U_{i_{m}} be the sequence of rules being applied in a successful derivation which generates Θ_{1}, and U_{j_{1}}, ⋯, U_{j_{n}} be the sequence of rules being applied in a successful derivation which generates Θ_{2}. Clearly, if Θ_{1} and Θ_{2} are distinct, then it has to be one of the following: either (1) at least there is some k such that for all r < k, U_{i_{r}} and U_{j_{r}} are the same, and U_{i_{k}} and U_{j_{k}} are different rules; (2) U8 is applied and different most general unfolding-unifiers are chosen for Θ_{1} and Θ_{2}.

If case (1) is true, it implies that we have two choices, either we can perform U_{i_{k}} or we can perform U_{j_{k}}. By the nature of ρ-unification rules, our inference rules are deterministic expect that non-determination may occur at the pair (U_{2}, U_{3}) and (U_{6}, U_{7}). Namely, (U_{i_{k}}, U_{j_{k}}) can only be either (U2, U3) or (U6, U7). In the case of (U_{2}, U_{3}), since neither variable substitutions nor unfoldingsubstitutions are generated, this non-determination does not contribute to the difference between Θ_{1} and Θ_{2}. Thus, if Θ_{1} and Θ_{2} are distinct, it has to be the case that the non-determination is caused by choosing either U_{6} or U_{7}. If we choose U_{6} in Θ_{1}, a degree variable, say N, is instantiated to 0 and N←0 is in Θ_{1}. If we choose U_{7} in Θ_{2}, then N = M + 1 for some M and N←M + 1 is in Θ_{2}. Clearly, Θ_{1} is not more general than Θ_{2} since {N←0} is not more general than {N←M + 1}. Similarly, Θ_{2} is not more general than Θ_{1} since {N←M + 1} is not more general than {N←0}.

If case (2) is true, it implies that U8 succeeds and a ground N-term s[u←Φ_{N}] and an Mgenerator Φ_{M} have more than one most general unfolding-unifiers, where N and M can be the same degree variable. We have shown that whenever s[u←Φ_{N}] and Φ_{M} has more than one most general unfolding-unifiers, CUU(s[u←Φ_{N}], Φ_{M}) has to be a finite set and each element of CUU(s[u←Φ_{N}], Φ_{M}) is of the form {N←i, M←j} (or {N←i} if N and M are the same degree variable).

If a most general unfolding-unifier es_{1} = {N←i_{1}, M←j_{1}} is chosen for Θ_{1} and another distinct one es_{2} = {N←i_{2}, M←j_{2}} is chosen for Θ_{2}, then it follows that none of Θ_{1} and Θ_{2} is more general than the other because the degree variable N and M are instantiated into distinct numbers in Θ_{1} and Θ_{2}, respectively. □

Our algorithm cannot generate all the most general ρ-unifiers. Nevertheless, our algorithm can generate a finite and complete set of ρ-unifiers, which cover every term expressed by most general ρ-unifiers.

Example 3.22 The most general ρ-unifier of f(x, y) and Φ_{N}(f(a, ⋄), f(a, b)) is

({x←a, y←Φ_{N}(f(a, ⋄), b)}, id).

Our algorithm generates two ρ-unifiers:

({x←a, y←b}, {N←0})

and

({x←a, y←Φ_{M}(f(a, ⋄), f(a, b))}, {N←M + 1})

which constitute a complete set of ρ-unifiers of f(x, y) and Φ_{N}(f(a, ⋄), f(a, b)).

Theorem 3.4 (Finiteness) The ρ-unification inference rules compute a finite, complete set of ρ-unifiers for ρ-terms L and R.

Proof: For every configuration in a ρ-unification derivation, there are only finitely many branches. By the termination theorem and the completeness theorem, we are done. □

Although the given set of ρ-unification inference rules may not always compute a complete set of most general ρ-unifiers, it does compute a finite, complete set of ρ-unifiers. In most cases, however, a complete set of most general ρ-unifiers can obtained. In particular, a complete set of most general ρ-unifiers can always be found between two ground ρ-terms.

One of the most desirable properties of ρ-unification is the closure property i.e., ρ-unification of ρ-terms still yields ρ-terms.

Theorem 3.5 (Closure) If {L =^{?} R} has a successful ρ-unification derivation with an associated ρ-unifier Θ, then both LΘ and RΘ are ρ-terms.

Proof: ρ-terms satisfy the conditions that every generator is ground and no generator is nested in another generator. Since a ρ-unifier always substitutes ρ-terms for first order variables, and substitutes a ground term or another generator for an generator, by the fact that first order variables always occur outside of the generators, applying a ρ-unifier or a ρ-substitution to a ρ-term still obtains a ρ-term. □

4 Logic Programming with ρ-terms

4.1 The ρ-logic Programs

Definition 4.1 We call p(s_{1}, ..., s_{n}) a ρ-atom if p is an n-ary predicate and s_{1} through s_{n} are ρterms. A ρ-literal is either a ρ-atom or the negation of a ρ-atom. A ρ-Horn-clause is a disjunction of ρ-literals with at most one positive literal. A set of ρ-Horn-clauses {C_{1}, ..., C_{m}} is a conjunction of ρ-clauses C_{1} ∧ ..., ∧C_{m}. A ρ-clause with only negative literals is called a goal and a ρ-clause with no literals is called an empty ρ-clause, denoted as □, which denotes the truth value false. A Horn ρ-logic program consists of a set of ρ-Horn-clauses. All the first order variables and degree variables in a ρ-clause are universally quantified. A goal ¬B_{1} ∨ ... ∨ ¬B_{n} can be represented as

: −B_{1}, ..., B_{n}.

A definite ρ-clause H ∨ ¬B_{1} ∨ ... ∨ ¬B_{n} can be represented as

H : −B_{1}, ..., B_{n}.

and we call H as the head and B_{1}, ..., B_{n} the body of the ρ-clause.

4.2 Equivalence of ρ-logic Programs and Logic Programs

Incorporating ρ-terms into Horn logic programming does not change its denotational semantics. This is not difficult to perceive since ρ-terms are simply a formalism to explicitly and algebraically represent some recursive data types. These data types can usually be expressed directly as Horn clauses. The advantage of using ρ-terms, however, is seen from an operational aspect. By using a compact representation of these data types and the incorporation of special unification to deal with them, greater efficiency as well as the elimination of certain non-termination can be achieved.

In this subsection, we show the semantical equivalence of ρ-Horn logic and Horn logic programs by presenting a transformation from the former to the latter.

A ρ-clause with degree variables schematizes infinitely many Horn clauses. Let us start with an example.

Example 4.1 A ρ-clause C

p(f(x, Φ_{N}(g(⋄), a))) : −q(b).

represents the following infinitely many ρ-clauses:

p(f(x, a)) : −q(b).
p(f(x, g(a))) : −q(b).
p(f(x, g(g(a)))) : −q(b).
⋮

By introducing a new predicate symbol q′ to capture the domain {a, g(a), g(g(a)), ...}, the above can be transformed into a logic program:

p(f(x, y)) : −q(b), q′(y).
q′(g(y)) : −q′(y).
q′(a).

Both programs compute the same fixpoint for predicate p, This process of conservatively transforming recurrence-terms into Horn clauses is similar to relativization which transforms many-sorted logics into unsorted ones [Obe62], [Wal83].

We use p⃗(t⃗[h_{1}[N], ..., h_{n}[N]]) to denote a conjunction of ρ-atoms with n occurrences of Ngenerators Φ_{N}(h_{1}[u_{1}←⋄], l_{1}), ..., Φ_{N}(h_{n}[u_{n}←⋄], l_{n}). The conjunction p⃗(t⃗[h_{1}[N], ..., h_{n}[N]]) may contain degree variables other than N.

In general, a ρ-clause C

p(t⃗[h_{1}[N], ..., h_{n}[N]]) : −q⃗[s⃗[h′_{1}[N], ..., h′_{m}[N]]

represents the following infinitely many ρ-clauses, each of which in turn may represent infinitely many ρ-clauses,

p(t⃗[l_{1}, ..., l_{n}]) : −q⃗[s⃗[l′_{1}, ..., l′_{m}]]
p(t⃗[h_{1}[l_{1}], ..., h_{n}[l_{n}]]) : −q⃗[s⃗[h′_{1}[l′_{1}], ..., h′_{m}[l′_{m}]]]
p(t⃗[h_{1}^{2}[l_{1}], ..., h_{n}^{2}[l_{n}]]) : −q⃗[s⃗[h_{1}^{′2}[l′_{1}], ..., h_{m}^{′2}[l′_{m}]]]
⋮

We introduce a new predicate symbol p′ and define it in such a way that the fixpoint of p′ is

{ p′(l_{1}, ..., l_{n}, l′_{1}, ..., l′_{m}),
p′(h_{1}[u_{1}←l_{1}], ..., h_{n}[u_{n}←l_{n}], h′_{1}[u′_{1}←l′_{1}], ..., h′_{m}[u′_{m}←l′_{m}]),
p′(h_{1}^{2}[u_{1}^{2}←l_{1}], ..., h_{n}^{2}[u_{n}^{2}←l_{n}], h_{1}^{′2}[u_{1}^{′2}←l′_{1}], ..., h_{m}^{′2}[u_{m}^{′2}←l′_{m}]), ...}

Thus, the ρ-clause

p(t⃗[y_{1}, ..., y_{n}]) : −q⃗(s⃗[z_{1}, ..., z_{m}]), p′(y_{1}, ..., y_{n}, z_{1}, ..., z_{m}).

schematizes the same set of Horn clauses as the ρ-clause C does.

Definition 4.2 The ρ-transformation transforms every ρ-clause

p(t⃗[h_{1}[N], ..., h_{n}[N]]) : −q⃗[s⃗[h′_{1}[N], ..., h′_{m}[N]]

into the following ρ-clauses:

p(t⃗[y_{1}, ..., y_{n}]) : −q⃗(s⃗[z_{1}, ..., z_{m}]), p′(y_{1}, ..., y_{n}, z_{1}, ..., z_{m}).
p′(h_{1}(y_{1}), ..., h_{n}(y_{n}), h′_{1}(z_{1}), ..., h′_{m}(z_{m})) : −p′(y_{1}, ..., y_{n}, z_{1}, ..., z_{m}).
p′(l_{1}, ..., l_{n}, l′_{1}, ..., l′_{m}).

where p′ is a new predicate symbol, and y_{1}, ..., y_{n}, z_{1}, ..., z_{n} are new variables which appear nowhere else in the clause p(t⃗[h_{1}[N], ..., h_{n}[N]]) : −q⃗[s⃗[h′_{1}[N], ..., h′_{m}[N]].

Example 4.2 Given a ρ-program ρ-P

p(h(x, Φ_{N}(f(⋄), a), Φ_{M}(g(⋄), b))) : −q_{1}(Φ_{N}(g(⋄), a)), q_{2}(h(x, y, b)).

By applying the transformation to N, we obtain a ρ-logic program

p(h(x, y_{1}, Φ_{M}(g(⋄), b))) : −q_{1}(z_{1}), q_{2}(x, y, b), q′(y_{1}, z_{1}).
q′(f(y_{1}), g(z_{1})) : −q′(y_{1}, z_{1}).
q′(a, a).

After the second round, we obtain a logic program P

p(h(x, y_{1}, y_{3})) : −q_{1}(z_{1}), q_{2}(x, y, b), q′(y_{1}, z_{1}), q′′(y_{3}).
q′(f(y_{1}), g(z_{1})) : −q′(y_{1}, z_{1}).
q′(a, a).
q′′(g(y_{3})) : −q′′(y_{3}).
q′′(b).

It is not difficult to see that P and ρ-P have the same fixpoint for predicate p.

Theorem 4.1 Any ρ-logic program ρ-P can be transformed into an equivalent logic program P.

Proof: Since each step of ρ-transformation strictly decreases the number of distinct degree variables in a ρ-clause, the ρ-transformation always terminates with a resulting logic program P.□

From the semantics of ρ-clauses given above, we can see that the meanings of a ρ-clause and the obtained ρ-clauses after the ρ-transformation are the same. Thus, we can prove by induction on the number of distinct degree variables in the ρ-logic programs, and conclude that

Theorem 4.2 (Correctness) The ρ-transformation is correct with respect to the fixpoints of predicates in the original ρ-logic program.

5 The ρ-Prolog

5.1 Goal Derivation

Operationally, SLD-resolution can be extended to ρ-clauses in a natural way. Prolog with ρ-terms is called ρ-Prolog. To be more precise, ρ-Prolog is ρ-Horn logic programming with SLD-derivation as its evaluation strategy.

Definition 5.1 Given a set A of ρ-clauses and a ρ-goal : −G_{1}, ..., G_{n}. If H : −D_{1}, ..., D_{m} ∈ A and U_{ρ} is a complete set of ρ-unifiers of H and G_{1}, then

: −D_{1}Θ, ..., D_{m}Θ, G_{2}Θ, ..., G_{n}Θ.

is a resolving ρ-goal, where Θ ∈ U_{ρ}.

Similar to Prolog, the ρ-substitutions collected while resolving away all the goals form a ρ-answer subsitution for the ρ-goal.

Definition 5.2 A ρ-answer substitution for A∪{G} is a ρ-unifier Θ = (σ, es) such that σ is a substitution for variables of G and es is an unfolding sequence for degree variables of G. We say a conjunction of ρ-atoms G_{1} ∧ ... ∧ G_{n} is a logical consequence of A if every constituent of it is a logical consequence of A. Let G be : −G_{1}, ..., G_{n}. We say that Θ is a correct ρ-answer substitution for A ∪ {G} if G_{1}Θ ∧ ... ∧ G_{n}Θ is a logical consequence of A.

Example 5.1 Given a ρ-logic program p(f(Φ_{N}(g(⋄), a), Φ_{M}(h(h(⋄)), b))), and a ρ-goal : −p(f(x, Φ_{Q}(h(⋄), b))), the pair ({x ← Φ_{N}(g(⋄), a)}, {Q ← 2 ∗ Q′, M←Q′}) is a correct ρ-answer substitution.

This example reveals an important feature of ρ-Prolog, that it is possible to ask infinitely many queries simultaneously by permitting ρ-terms in the query. The correct ρ-answer substitutions will filter out those queries which are not consequences of the program. (In this particular example, the goal is unsatisfiable when Q is instantiated to an odd integer.)

Theorem 5.1 Let P be a program, G be a goal : −G_{1} ∧ ... ∧ G_{k}, and Θ_{1}, ..., Θ_{n} be a sequence of ρ-unifiers produced in a successful SLD-refutation of P ∪ {G}, then Θ_{1} ∘ ⋯ ∘ Θ_{n} is a correct ρ-answer substitution.

Proof: The theorem is proved by induction on the length of the refutation, which is n. Suppose n = 1, it follows that G is of the form : −G_{1}, and P contains a unit ρ-clause A : −. such that Θ is a ρ-unifier of A and G_{1}, and AΘ = G_{1}Θ. Since G_{1}Θ represents a subset of instances of A, it follows that G_{1}Θ is a logic consequence of P.

Suppose the theorem holds for refutations of length n − 1, and let A : −B_{1}, ..., B_{m} be the first ρ-clause in the refutation, and G_{q} be the selected atom of G. By induction hypothesis,

(G_{1} ∧ ... ∧ G_{q−1} ∧ B_{1} ∧ ... ∧ B_{m} ∧ G_{q+1} ∧ ... ∧ G_{k})Θ_{1} ∘ ... ∘ Θ_{n}

is a logic consequence of P. Thus, if m > 0, (B_{1} ∧ ... ∧ B_{m})Θ_{1} ∘ ... ∘ Θ_{n}is a logic consequence of P. Consequently,

G_{q}Θ_{1} ∘ ... ∘ Θ_{n} = AΘ_{1} ∘ ... ∘ Θ_{n}

is a logic consequence of P. Therefore (G_{1} ∧ ... ∧ G_{k})Θ_{1} ∘ ... ∘ Θ_{n} is a logic consequence of P. □

Although denotationally ρ-logic programs are no more powerful than logic programs, operationally ρ-Prolog behaves quite differently from Prolog. In addition to allowing infinitely many queries and providing infinitely many answers in a finite form, it can also optimize search by avoiding repetitious computation and backtracking. Certain non-termination which are typical in Prolog can also be eliminated:

Example 1.1 Continued: In ρ-Prolog, the same program can be formulated as

meets(toto, Φ_{N}(2 + ⋄, 0)).
meets(tintin, Φ_{N}(2 + ⋄, 1)).

Then the answer for the query Q = {Days : meets(Days, toto)} is {Φ_{N}(2 + ⋄, 0)}, which can be expressed easily in our framework.

Example 1.2 Continuned:

In ρ-Prolog, the programs become

(1) p(x) : −r(x, y, z), q(z).
(2’) r(Φ_{N}(a • ⋄, a), Φ_{N}(b • ⋄, b), Φ_{N}(c • ⋄, c)).
(4) q(c^{20}).  (4’) q(d).  (4”) q(x).
(G) : −p(x).  (G’) : −p(x).  (G”) : −setof(p(x), p(x), S).

That is, the definition of r is condensed into one single ρ-fact. Then in the first example, the query p(x) yields a correct ρ-answer substitution

Θ = ({x ← a^{20}}, {N ← 20})

which is directly obtained through ρ-unification with no backtracking. Thus, some computational efficiency is achieved.

In the second example the query p(x) stops finitely due to the failed unification of Φ_{N}(a • ⋄, a) and d, as depicted by the following derivation:

: −p(x)
: −\underline{r(x, y, z)}, q(z)
: −r(Φ_{N}(a • ⋄, a), Φ_{N}(b • ⋄, b), Φ_{N}(c • ⋄, c)), \underline{q(Φ_{N}(c • ⋄, c))}
: −fail.

In the third example the query setof(p(x), p(x), S) is the same as p(x) , which stops and returns a correct ρ-answer substitution

Θ = ({x ← Φ_{N}(a • ⋄, a)}, id).

We can see that Ω(p(x)Θ) = {p(a), p(a^{2}), p(a^{3}), ...}, which is the fixpoint of p.

6 Related Work and Conclusion

Other work concerning finite representation of structured domains in Prolog include [CI89] and [HJ90].

Chomicki and Imielinski [CI89] observed that the “function free” DATALOG [CH85] is not sufficient to handle flow of time and recursive data structures since they use function symbols. On the other hand, incorporating function symbols into DATALOG may result in infinite query answers, which is normally considered as “unsafe”. They noticed that if function symbols are only allowed to occur at some fixed positions of predicates, then the least fixpoints of the function rules have some repetitive patterns which can be compactly represented via congruence closure. Thus, infinitely many answers, which are often the fixpoints, can be obtained by using the congruence closure procedure [NO80].

Heintze and Jaffar [HJ90] used cartesian closure [BJ88] to define finite approximations of the least models of logic programs. For a class of programs whose head atoms are linear and every body atom has at most one distinct variable appearing elsewhere in the rule, the fixpoints of such programs can be accurately approximated and represented by cyclic term graphs.

These methods can be used to infer a finite representation for infinitely many query answers by a type inference like procedure. Their applications are often hindered by the difficulties of learning a finite representation of an infinite set of terms unless the syntax of the programs on which the learning processes are performed is restricted.

The ρ-Prolog takes a different approach by encoding infinite domains or fixpoints explicitly. Thus, we do not need to impose any restriction on the syntax of Prolog programs. As for the expressive power, ρ-terms can express some fixpoints which can not be represented by congruence closure and cyclic term graph. The reverse is also true.

Another way to look at ρ-Prolog is through the constraint logic programming scheme CLP(X), introduced by Jaffar and Lassez [JL87]. CLP treats a Horn clause as A : −c, |, B_{1}, ..., B_{n}, where A, B_{1}, ..., B_{n} are uninterpreted atoms and c is a constraint – a conjunction of atoms – interpreted by a particular structure X. It is also assumed that there is a decision procedure for solving the constraints. Thus, executing a CLP program consists of SLD-resolution of the uninterpreted atoms as well as employing semantic means for solving the constraints. Greater efficiency and less possibility of loops can be achieved with such a framework. Well-known instances of CLP include CLP(R), Prolog II and CHIP.

The ρ-Prolog can also be considered as an instance of the general CLP(X) framework. A ρclause A : −B_{1}, ..., B_{n} can be transformed into a constraint clause A′ : − x_{1} = G_{1}, ⋯, x_{m} = G_{m} | B1^{′}, ..., B′_{n} by replacing each distinct generator term G_{i} in A : −B_{1}, ..., B_{n} by a new variable x_{i}, and considering x_{i} = G_{i} as part of the constraint. The domain X in our context is then the term algebra of the ρ-terms and the constraint solving part is ρ-unification of the ρ-terms. To our knowledge, our work is the first to incorporate syntactically structured domains into the CLP framework.

Although our intention is to use ρ-term to represent an infinite set of first order terms, we think that ρ-term can be straightforwardly extended to denote fixpoints of certain circular data structures.

Acknowledgements

We are grateful to Enno Ohlebusch and anonymous referees for their careful comments on the paper.

References

[BJ88] M. Bruynooghe and G. Janssens. An Instance of Abstract Interpretation Integrating Type and Mode Inference. In Proc. 5^{th} Int. Conf. on Logic Programming, pages 669–683, K.A. Bowen and R.A. Kowalski(eds), MIT Press, Aug. 1988.

[CH85] A. Chandra and D. Harel. Horn Clause Queries and Generalizations. J. Logic Programming, 2(1):1–16, April 1985.

[CHK90] Hong Chen, Jieh Hsiang, and H.C. Kong. On Finite Representations of Infinite Sequences of Terms. In Proc. of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 37–44, Montreal, June 1990. To appear in LNCS, Springer-Verlag.

[CI89] J. Chomicki and T. Imielinski. Relational Specification of Infinite Query Answers. In Proc. of the 1989 ACM SIGMOD Int. Conf. on the Management of Data, pages 174–183, Portland, Oregon, June 1989. Vol. 18, No. 2.

[Col82] A. Colmerauer. Prolog and Infinite Trees. In Logic Programming, Academic Press, 1982.

[Com89] Hubert Comon. Inductive Proofs by Specifications Transformation. In Proc. Rewriting Techniques and Applications, pages 76–91, Springer Verlag, Chapel Hill, 4 1989. LNCS 355.

[Com90] Hubert Comon. Equational Formulas in Order-Sorted Algebras. In ICALP 90, pages 674– 688, July 1990.

[GM84] J.A. Goguen and J. Meseguer. Equalities, Types Modules and Generics for Logic Programming. Journal of Logic Programming, 1, 1984.

[GM85] J.A. Goguen and J. Meseguer. Order-Sorted Algebra I, Partial and Overloaded Operators, Error and Inheritance. Technical Report 000, SRI, 1985.

[HJ90] N. Heintze and J. Jaffar. A Finite Presentation Theorem for Approximating Logic Programs. In POPL-90, pages 197–209, Feb. 1990.

[JL87] J. Jaffar and J.L. Lassez. Constraint Logic Programming. In Proceedings of 14th ACM Symposium on Principles of Programming languages, pages 111–119, 1987.

[MR85] P. Mishra and U. Reddy. Declaration-Free Type Checking. In ACM Sym. on Principles of Programming Languages, pages 7–21, ACM, 1985.

[NO80] C. G. Nelson and D.C. Oppen. Fast Decision Algorithms based on Congruence Closure. Journal of the ACM, 27(2), 1980.

[Obe62] Oberschelp. Untersuchungen Zur mehrsortigen Quantorenlogik. Mathematische Annalen, 145:297–333, 1962.

[Sch89] M. Schmidt-Schaub. Computational Aspects of an Order-Sorted Logic with Term Declarations. Springer-Verlag, 1989. Lecture Notes in Artificial Intelligence, 395.

[Wal83] C. Walther. Unification in Many-Sorted Theories. In Proc. of 6th ECAI, pages 383–392, R. O’Shea(ed), North-Holland, Pisa, 1983.

7 Appendix A

7.1 The ρ-unification of Ground N-terms

In this section, we study the ρ-unification of two ground N-terms. Let L = s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] and R = Φ_{N}(h_{2}[u_{2}←⋄], l_{2}) be two ground N-terms. Let CUU(L, R) denote a complete set of most general unfolding-unifiers of L and R. Let the set of terms represented by L and R be

\begin{aligned}L & ≃ & \{s_{i} : s_{i} = L[N←i]\}, \\ R & ≃ & \{t_{i} : t_{i} = R[N←i]\}. \end{aligned}

Proposition 7.1 Given two ground first order terms s and t, if there is a position u in s but not in t, then s and t are not equal.

Lemma 7.1 Let |u_{1}| > |u_{2}| and p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{2}|, |u_{1}| − |u_{2}|)⌉, then ∀ i ≥ p, s_{i} ≠ t_{i}, and CUU(L, R) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}}.

Proof: The idea is to show that for all i ≥ p, the position u.u_{1}^{i} of s_{i} is not a position of t_{i}. Thus, by Proposition 8.1, for all i ≥ p, s_{i} ≠ t_{i}. Suppose the longest positions of s[u←⋄], h_{1}[u_{1}←⋄], l_{1}, h_{2}[u_{2}←⋄] and l_{2} are u_{s}, w_{1}, v_{1}, w_{2}, and v_{2} respectively. Thus, for all i ≥ 1, the longest positions u_{s_{i}} and u_{t_{i}} of s_{i} and t_{i} will be

u_{s_{i}} = longest(u_{s}, u.u_{1}^{i−1}.w_{1}, u.u_{1}^{i}.v_{1})
u_{t_{i}} = longest(u_{2}^{i−1}.w_{2}, u_{2}^{i}.v_{2})

Since we define the height of a term is the longest position of a term plus 1, then

p ≥ ⌈longest(u_{s}, u.w_{1}, u.u_{1}.v_{1}, w_{2}, u_{2}.v_{2})/min(|u_{2}|, |u_{1}| − |u_{2}|)⌉

It is easy to see that |u.u_{1}^{p}| > u_{s}, and p ≥ 1, thus for all i ≥ p,

|u_{s_{i}}| = |longest(u.u_{1}^{i−1}.w_{1}, u.u_{1}^{i}.v_{1})|
= |u| + (i − 1) ∗ |u_{1}| + max(|w_{1}|, |u_{1}| + |v_{1}|)
= |u| + i ∗ |u_{1}| + max(|w_{1}| − |u_{1}|, |v_{1}|)
|u_{t_{i}}| = |longest(u_{2}^{i−1}.w_{2}, u_{2}^{i}.v_{2})|
= (i − 1) ∗ |u_{2}| + max(|w_{2}|, |u_{2}| + |v_{2}|)

If |u_{2}| + |v_{2}| ≥ |w_{2}|, then for all i ≥ p, u_{t_{i}} = i ∗ |u_{2}| + |v_{2}|, thus

|u_{s_{i}} − u_{t_{i}}| = |u| + i ∗ |u_{1}| + max(|w_{1}| − |u_{1}|, |v_{1}|) − i ∗ |u_{2}| − |v_{2}|
≥ |u| + i ∗ (|u_{1}| − |u_{2}|) − |v_{2}|
≥ |u| + p ∗ (|u_{1}| − |u_{2}|) − |v_{2}|
≥ |u| + max(|u_{s}|, |u| + |w_{1}|, |u| + |u_{1}| + |v_{1}|, |w_{2}|, |u_{2}| + |v_{2}|) − |v_{2}|
> 0

Similarly, we can show the lemma is true when |u_{2}| + |v_{2}| < |w_{2}|.

Since for all i ≥ p, s_{i} ≠ t_{i}, CUU(L, R) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}}. □

Lemma 7.2 If |u_{1}| = |u_{2}|, then for p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{1}|, |u_{2}|)⌉,

a . s_{p} = t_{p} implies that ∀ i ≥ 0, s_{i} = t_{i}, CUU(L, R) = {id}.

b . s_{p} ≠ t_{p} implies that ∀ i > p, s_{i} ≠ t_{i}, CUU(L, P) = {{N←i} : 0 ≤ i < p, s_{i} = t_{i}}.

Proof of a:

u = λ : First, we want to show that u_{1} = u_{2}. We prove it by contradiction. Suppose u_{1} ≠ u_{2}. By premise |u_{1}| = |u_{2}|, it follows that neither u_{1} ≤ u_{2} nor u_{2} ≤ u_{1}. If u_{1} is not a position in h_{2}[u_{2}←⋄] then for any i ≥ 1, u_{1}^{i} can not be a position of h_{2}[u_{2}←⋄]. Thus, s_{p} ≠ t_{p}, a contradiction. If u_{1} is a position in h_{2}[u_{2}←⋄], then the choice of p implies that u_{1}^{p} can not be a position of h_{2}[u_{2}←⋄]. This again implies that s_{p} ≠ t_{p}, which contradicts the premise s_{p} = t_{p}.

The conditions u_{1} = u_{2} and s_{p} = t_{p} imply that h_{1}[u_{1}←⋄] = h_{2}[u_{2}←⋄] and l_{1} = l_{2}. Therefore, for all i ∈ N, h_{1}^{i}[u_{1}^{i}←l_{1}] = h_{2}^{i}[u_{2}^{i}←l_{2}], i.e., s_{i} = t_{i} for all i.

u ≠ λ : From the premises that |u_{1}| = |u_{2}| and s_{p} = t_{p}, it follows that for some integer k < p and positions v and w such that u = u_{2}^{k}.v, v.w = u_{2} and w.v = u_{1} (see Figure 1) since otherwise, u_{2}^{p} will not be a position in s_{p}, which consequently contradicts the premise s_{p} = t_{p}. Furthermore, it follows that

h_{1}[u_{1}←⋄] = h_{2}/v[w←h_{2}[v←⋄]].  (1)

From the Figure 1 and Fact 1, it follows that for any i ∈ N,

h_{1}^{i+1}[u_{1}^{i+1}←⋄] = h_{2}/v[w←h_{2}^{i}[u_{2}^{i}←h_{2}[v←⋄]]  (2)

We first prove that s_{p} = t_{p} implies ∀i > p, s_{i} = t_{i}. The equality s_{p} = t_{p} can be written as

s[u←h_{1}^{k+1}[u_{1}^{k+1}←h_{1}^{j}[u_{1}^{j}←l_{1}]]] = h_{2}^{k}[u_{2}^{k}←h_{2}[v←h_{2}/v[w←h_{2}^{j}[u_{2}^{j}←h_{2}[v←h_{2}/v[w←l_{2}]]]]]] (3)

where

p = k + j + 1,
s[u←⋄] = h_{2}^{k}[u_{2}^{k}←h_{2}[v←⋄]],
h_{1}^{k}[u_{1}^{k}←l_{1}] = h_{2}/v[w←l_{2}]

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; s[u←⋄] =; h_{2}[u_{1}←⋄]=; k h_{2}’s; h_{2}; u_{2}; w; v; v; w; h_{1}[u_{1}←⋄] =]

Figure 1: u = u_{2}^{k}.v, v.w = u_{2}, and w.v = u_{1}

By fact 2 , we can replace the j in the fact 3 by any integer such that fact 3 holds. Thus, we conclude that

∀i ≥ k + 1, s_{i} = t_{i}.

Now we prove that s_{p} = t_{p} implies that s_{i} = t_{i} ∀i < p. Actually, we have proved a stronger result, namely, ∀i ≥ k + 1, s_{i} = t_{i}. Now we only need to prove for all i ≤ k, s_{i} = t_{i}.

The fact that s_{k+1} = t_{k+1} implies that

\begin{aligned}s[u←⋄] & = & h_{2}^{k}[u_{2}^{k}←h_{2}[v←⋄]] \\ h_{1}[u_{1}←⋄] & = & h_{2}/v[w←h_{2}[v←⋄]] \\ h_{1}^{k}[u_{1}^{k}←l_{1}] & = & h_{2}/w[v←l_{2}] \end{aligned}

which again implies that s[u←l_{1}] = l_{2}, namely, s_{0} = t_{0}.

Similarly, we can show s[u←h_{1}[u_{1}←l_{1}]] = h_{2}[u_{2}←l_{2}], etc. Thus, L =_{st} R and id is the unique most general unfolding-unifier of L and R. □.

Proof of b: Suppose there exists a k > p such that s_{k} = t_{k}. By the same techniques we used in the proof of part a, we can show that for all i, s_{i} = t_{i}. Thus, it contradicts the premise that s_{p} ≠ t_{p}. □

Lemma 7.3 Let s[u←L] and s[u←R] be two ground N-terms. Then

s[u←L][N←i] = s[u←R][N←i] if and only if L[N←i] = R[N←i].

Proof: Follows from the definition of ρ-terms. □

Lemma 7.4 If |u_{1}| < |u_{2}|, and r is the minimal integer such that L′ = L[N←Q + r] and R′ = R[N←Q + r] satisfy:

either (a) the prefixes of L′ and R′ do not match,

or (b)

\begin{matrix}L′ = s′[u′←Φ(h_{1}[u_{1}←⋄], l_{1})] \\ R′ = s′[u′←s′′[u′′←Φ(h_{2}[u_{2}←⋄], l_{2})]], \end{matrix}

then

in case (a): CUU(L, R) = {{N←i} : 0 ≤ i < r, s_{i} = t_{i}}

in case (b): CUU(L, R) = {{N←i} : 0 ≤ i < k, s_{i} = t_{i}} where

k = ⌈max(height(s_{r+1}), height(t_{r+1}))/min(|u_{1}|, |u_{2}| − |u_{1}|)⌉.

Proof: Lemma 8.1 can not be applied immediately since |u_{1}| < |u_{2}|. The intuitive idea is that we can always unfold L and R finitely many times (say r times) till one of the following holds: (i) a position mismatch occurs between the two prefixes which do not cover positions in l_{1} and l_{2} (which implies that for all i ≥ r, s_{i} ≠ t_{i}); (ii) s[u←h_{1}^{r}[u_{1}^{r}←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})]] and h_{2}^{r}[u_{2}^{r}←Φ_{N}(h_{2}[u_{2}←⋄], l_{2})]] can be written as s′[u′←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] and s′[u′←s′′[u′′←Φ_{N}(h_{2}[u_{2}←⋄], l_{2})]] respectively. In case (a), it is obvious that for all i > r, s_{i} ≠ t_{i}. In case (b), by Lemma 8.3, the unification problem is transformed into

s′′[u′′←Φ_{N}(h_{2}[u_{2}←⋄], l_{2})] =^{?} Φ_{N}(h_{1}[u_{1}←⋄], l_{1}).

By Lemma 8.1, for all i > p, s_{i} ≠ t_{i} where

p = ⌈max(height(s′′[u′′←h_{2}[u_{2}←l_{2}]]), height(h_{1}[u_{1}←l_{1}]))/min(|u_{1}|, |u_{2}| − |u_{1}|)⌉.

Therefore, for all i > r + p, s_{i} ≠ t_{i}. Since k ≥ r + p, thus for all i > k, s_{i} ≠ t_{i}. □

7.2 The ρ-unification of a ground N-term and a M-generator

In this section, we assume that N and M are distinct degree variables. For convenience, in this section we denote Φ_{N}(h_{N}[u_{N}←⋄], l_{N}) and Φ_{M}(h_{M}[u_{M}←⋄], l_{M}) as Φ_{N} and Φ_{M} respectively.

Let

\begin{aligned}s[u←Φ_{N}] & ≃ & \{s_{i} : s_{i} = s[u←Φ_{N}[N←i]]\} \\ Φ_{M} & ≃ & \{t_{j} : t_{j} = Φ_{M}[M←j]\}. \end{aligned}

Again, we use CUU(L, R) to denote the complete set of most general unfolding-unifiers of two ρ-terms L and R. First we concentrate on the special case in which u is empty.

7.2.1 The ρ-unification of generators Φ_{N} and Φ_{M}

Lemma 7.5 Let p and q be two integers satisfying |u_{N}| ∗ p = |u_{M}| ∗ q = lcm(|u_{N}|, |u_{M}|), where lcm stands for the least common multipler. Then Ω(Φ_{N}) ∩ Ω(Φ_{M}) is infinite if and only if

h_{N}^{p}[u_{N}^{p}←⋄] = h_{M}^{q}[u_{M}^{q}←⋄] and \begin{matrix}∃i 0 ≤ i < p, ∃j, s_{i} = t_{j}, or \\ ∃j, 0 ≤ j < q, ∃i, s_{i} = t_{j}. \end{matrix}

Proof: ⟹: All the s_{i} and t_{j}, where i ≥ p and j ≥ q, can be written as

s_{i} = h_{N}^{p}[u_{N}^{p}←h_{N}^{k}[u_{N}^{k}←l_{N}]]
t_{j} = h_{M}^{q}[u_{M}^{q}←h_{M}^{k′}[u_{M}^{k′}←l_{M}]]

For each s_{i} at most one t_{j} equals to s_{i}. Therefore, s_{0}, ..., s_{p−1} can only have finitely many t_{j}’s equivalent to them. Similarly, t_{0}, ..., t_{q−1} can only have finitely many s_{i}’s equivalent to them. In order to ensure the intersection of Ω(Φ_{N}) and Ω(Φ_{M}) to be infinite, for some i ≥ p and j ≥ q, s_{i} = t_{j} has to be true. Consequently, u_{N}^{p} = u_{M}^{q} has to be true, since otherwise, there will be some m such that u_{N}^{m∗p} ∉ P (t_{j}) for any j, and for all i > m ∗ p, no t_{j} equals to s_{i}, which contradicts the assumption that the intersection of Ω(Φ_{N}) and Ω(Φ_{M}) is infinite. Thus,

h_{N}^{p}[u_{N}^{p}←⋄] = h_{M}^{q}[u_{M}^{q}←⋄]

If s_{i} and t_{j} are equal, they can be rewritten as either

\{ \begin{matrix}s_{i} & = & h_{N}^{m∗p}[u_{N}^{m∗p}←h_{N}^{k}[u_{N}^{k}←l_{N}]] for some 0 ≤ k < p \\ t_{j} & = & h_{M}^{m∗q}[u_{M}^{m∗q}←h_{M}^{k′}[u_{M}^{k′}←l_{M}]] for some k′ \end{matrix}

or

\{ \begin{matrix}s_{i} & = & h_{N}^{m∗p}[u_{N}^{m∗p}←h_{N}^{k}[u_{N}^{k}←l_{N}]] for some k \\ t_{j} & = & h_{M}^{m∗q}[u_{M}^{m∗q}←h_{M}^{k′}[u_{M}^{k′}←l_{M}]] for some 0 ≤ k′ < q \end{matrix}

In both cases, we can see that s_{i} and t_{j} are equal if and only if s_{k} = t_{k′}.

⟸: Obvious. □

Lemma 7.6 If Ω(Φ_{M})∩Ω(Φ_{N}) is infinite, then there exists a unique pair of index (n, m) satisfying

(0 ≤ n < p and s_{n} = t_{m}) or (0 ≤ m < q and s_{n} = t_{m}).

Proof: According to Lemma 8.5,

h_{N}^{p}[u_{N}^{p}←⋄] = h_{M}^{q}[u_{M}^{q}←⋄] and \begin{matrix}∃i 0 ≤ i < p, ∃j, s_{i} = t_{j}, or \\ ∃j, 0 ≤ j < q, ∃i, s_{i} = t_{j}. \end{matrix}

We prove the lemma by studying the cases p = 1 and p > 1. The discussion for q is symmetric to that of p. p = 1 : It must be s_{0} = t_{m} for some m. If m ≥ q, then there is no m′ < q such that t_{m′} = s_{n′} for

any n′ since the size of the sequence increases monotonically. Thus, the pair (n, m) is unique. When m < q, suppose there is a pair (n′, m′) such that s_{n′} = t_{m′} and m < m′ < q. We rewrite s_{n′} and t_{m′} as h_{N}^{n′∗p}[u_{N}^{n′∗p}←s_{0}] and h_{M}^{m′−m}[u_{N}^{m′−m}←t_{m}] respectively. However, u_{N}^{n′∗p} > u_{N}^{m′−m}. Thus, s_{0} = t_{m} and s_{n′} = t_{m′} imply that s_{0} is equal to a proper super-term of it, which is impossible.

p > 1 : Using the same techniques as for the case of p = 1, we can show that the Lemma is true. The only difference is that we have to take more case analysis into account when p > 1. For instance, we have to consider s_{n} = t_{m} and s_{n′} = t_{m′} where 0 ≤ n < n′ < p. □.

Corollary 7.1 If Ω(Φ_{M}) ∩ Ω(Φ_{N}) is infinite, then {N = p ∗ Q + n, M = q ∗ Q + m}, where n and m are given by Lemma 8.6, is the unique most general unfolding-unifier of Φ_{N} and Φ_{M}.

Lemma 7.7 If Ω(Φ_{M}) ∩ Ω(Φ_{N}) is finite, then for some integers k and r,

CUU(Φ_{N}, Φ_{M}) = {{N←i, M←j} : (0 ≤ i ≤ k and s_{i} = t_{j}) or (0 ≤ j ≤ r and s_{i} = t_{j})}.

Proof: We prove the Lemma by analyzing the two cases: u_{N}^{p} = u_{M}^{q} and u_{N}^{p} ≠ u_{M}^{q}.

u_{N}^{p} = u_{M}^{q} : If h_{N}^{p}[u_{N}^{p}←⋄] = h_{M}^{q}[u_{M}^{q}←⋄], then by Lemma 8.5, Ω(Φ_{M}) ∩ Ω(Φ_{N}) must be empty. Consequently, the set CUU(Φ_{N}, Φ_{M}) is empty. If h_{N}^{p}[u_{N}^{p}←⋄] ≠ h_{M}^{q}[u_{M}^{q}←⋄], then for all i ≥ p, j ≥ q, s_{i} ≠ t_{j} since h_{N}^{p}[u_{N}^{p}←⋄] and h_{M}^{q}[u_{M}^{q}←⋄] are the prefixes of s_{i} and t_{j} respectively. We can choose k and r to be p and q. Thus, the Lemma follows.

u_{N}^{p} ≠ u_{M}^{q} : For some p′ < p, q′ < q, u_{N}^{p′} is not a prefix of u_{M}^{q} and u_{M}^{q′} is not a prefix of u_{N}^{p}, as illustrated by Figure 2. Thus, for all j ≥ q′′ where q′′ = ⌈height(h_{N}[u_{N}←⋄])/|u_{M}|⌉, u_{M}^{q′+q′′} is not a position of s_{i} for any i. Similarly, for all i ≥ p′′ where p′′ = ⌈height(h_{M}[u_{M}←⋄])/|u_{N}|⌉, u_{N}^{p′+p′′} is not a position of t_{j} for any j. Therefore, for all i ≥ p′ + p′′ and j ≥ q′ + q′′, s_{i} ≠ t_{j}. We then choose k = p′ + p′′, r = q′ + q′′ and the Lemma follows. □

7.2.2 The General Case

Let L = s[u←Φ_{N}] and R = Φ_{M}. If |u| ≥ |u_{M}|, and there is no r and v such that u_{M}^{r}.v = u, then for all i > |u|/|u_{M}|, the position u_{M}^{i} of h_{M}^{i}[u_{M}^{i}←Φ_{M}] will be in s[u←⋄]. However, since term s[u←⋄] has fixed size, there is at most one j such that s[u←⋄]/u^{j} = l_{M}. In other words, for all i > j, no constituent of s[u←Φ_{N}] equals to t_{i}. Based on the same argument we repeatedly used before, this i is bounded by the maximal height m of s_{1} and t_{1}, and consequently, the size of CUU(s[u←Φ_{N}], Φ_{M}) is bounded by m.

Suppose |u| ≥ |u_{M}|, and there are r and v such that |v| < |u_{M}| and u_{M}^{r}.v = u. If h_{M}^{r} is not a prefix of s, then for all j > r, no constituent of s[u←Φ_{N}] equals to t_{j} since every constituent of s[u←Φ_{N}] has s as its prefix. Thus, {{N←i, M←j} : j < r, s_{i} = t_{j}} is a complete set of most general unfolding-unifiers of s[u←Φ_{N}] and Φ_{M}, and clearly its size is bounded by the maximal height of s_{1} and t_{1}. If h_{M}^{r} is a prefix of s, then the complete set of unfolding-unifiers of s[u←Φ_{N}] and Φ_{M} is {{N←i, M←j} : j ≤ r, s_{i} = t_{j}} ∪CUU(s′[v←Φ_{N}], Φ_{M}) where s′[v←⋄] is s[u←⋄]/n_{M}^{r}.

\begin{matrix}. & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & [figure] & [figure] & [figure] & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & [figure] & [figure] & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & h_{M}^{q}[u_{M}^{q}←⋄] = & h_{N}^{p}[u_{N}^{p}←⋄]= & u_{N}^{p′} & u_{M} & h_{M} & u_{M}^{q′} & u_{N} & h_{N} \\ Figure 2: u_{N}^{p} ≠ u_{M}^{q} \end{matrix}

37

Now we need to compute the complete set of (most general) unfolding-unifiers of s′[v←Φ_{N}] and Φ_{M} where |v| < |u_{M}|.

Without loss of generality, let us assume that we discuss the ρ-unification of s[u←Φ_{N}] and Φ_{M} where 0 < |u| < |u_{M}|. The case under which |u| = 0 has been discussed previously.

We first start with an example.

Example 7.1 The most general unfolding-unifier of s(Φ(s(s(⋄)), N, 0)) =^{?} Φ(s(s(⋄)), M, s(0)) is {M←Q, N←Q}. However, if we apply unfolding and decomposition interchangeblely, an infinite derivation occurs:

s(Φ(s(s(⋄)), N, 0)) =^{?} Φ(s(s(⋄)), M, s(0))
⇒ s(Φ(s(s(⋄)), N, 0)) =^{?} s(s(Φ(s(s(⋄)), M, s(0)))) : M←M_{1} + 1
⇒ Φ(s(s(⋄)), N, 0) =^{?} s(Φ(s(s(⋄)), M_{1}, s(0)))
⇒ s(s(Φ(s(s(⋄)), N, 0))) =^{?} s(Φ(s(s(⋄)), M_{1}, s(0))) : N←N_{1} + 1
⇒ s(Φ(s(s(⋄)), N_{1}, 0)) =^{?} Φ(s(s(⋄)), M_{1}, s(0))
⇒ ...

Up to the renaming for degree variables, the initial equation we try to solve occurs again after p and q steps of unfolding N and M. If we can show that for some i < p, s_{i} = t_{j} for some j or for some j < q, s_{i} = t_{j} for some i, then we can infer that the intersection of Ω(s[u←Φ_{N}]) and Ω(Φ_{M}) is infinite. Furthermore, {N←p ∗ Q + i, M←q ∗ Q + j} is an unfolding-unifier of s[u←Φ_{N}] and Φ_{M}. In this example, both p and q are 1, and s_{0} = t_{0}. It follows that {N←1 ∗ Q + 0, M←1 ∗ Q + 0}, namely, {N←Q, M←Q} is an unfolding-unifier of s(Φ(s(s(⋄)), N, 0)) and Φ(s(s(⋄)), M, s(0)).

More generally, it may not be the initial equation which occurs twice in a possible infinite derivation. Rather it is some intermediate equation which occurs twice. Using the pigeonhole principle, it can be shown that after some finite number of unfolding and decomposition, a loop does occur if the intersection of Ω(s[u←Φ_{N}]) and Ω(Φ_{M}) is infinite. The following picture shows the derivation: (decomposition is performed and does not show up in the following diagram.)

s[u←Φ_{N}]  =^{?} Φ_{M}
⇓ k_{N} unfoldings  ⇓ k_{M} unfoldings
s′[u′←Φ_{N′}] =^{?} s′′[u′′←Φ_{M′}]
⇓ p unfoldings  ⇓ q unfoldings
s′[u′←Φ_{N′′}]  =^{?} s′′[u′′←Φ_{M′′}]

where at least one of u′ and u′′ is λ. Let p and q be the smallest numbers with above property, and no Φ_{N} =^{?} Φ_{M} is generated intermediately. If for some r_{N} < p and r_{M} < q, s′[u′←Φ_{N}][N←r_{N}] = s′′[u′′←Φ_{M}][M←r_{M}], clearly, {N←p ∗ Q + k_{N} + r_{N}, M←q ∗ Q + k_{M} + r_{M}} is an unfolding-unifier of s[u←Φ_{N}] and Φ_{M}.

Without loss of generality, let us assume that u′′ = λ. Let s′_{i} denote s′[u′←Φ_{N}][N←i] and t′_{i} denote Φ_{M}[M←i]. Together with the set of unfolding-unifiers {{N←i, M←j} : i < k_{N} or j < k_{M}}, we obtain a complete set of unfolding unifiers for s[u←Φ_{N}] and Φ_{M}.

Definition 7.1 The ρ-equation s[u←Φ_{N}] =^{?} Φ_{M} is called a loop pair if for some minimal integers p and q,

\begin{aligned}s[u←Φ_{N}][N←N′ + p] & = & s′[u′←s[u←Φ_{N′}]] \\ Φ_{M}[M←M′ + q] & = & s′[u′←Φ_{M′}] \end{aligned}

The pair (p, q) is called the loop factor of s[u←Φ_{N}] =^{?} Φ_{M}.

Definition 7.2 A loop pair s[u←Φ_{N}] =^{?} Φ_{M} with loop factor (p, q) is called minimal if satisfies:

Proper: There does not exist integers p′ ≤ p and q′ ≤ q′ such that (a′, b′) is different from (a, b)

and

\begin{aligned}s[u←Φ_{N}][N←N′ + p′] & = & s′[u′←Φ_{N′}] \\ Φ_{M}[M←M′ + q′] & = & s′[u′←Φ_{M′}]. \end{aligned}

Minimal: there does not exist p′ < p′′ < p and q′ < q′′ < q such that either

(s[u←Φ_{N}] =^{?} Φ_{M}) ∘ {N←N′ + p′, M←M′ + q′} = s′[u′←c[u_{c}←Φ_{N′}]] =^{?} s′[u′←Φ_{M′}]
(s[u←Φ_{N}] =^{?} Φ_{M}) ∘ {N←N′′ + p′′, M←M′′ + q′′} = s′′[u′′←c[u_{c}←Φ_{N′′}]] =^{?} s′′[u′′←Φ_{M′′}]

or

(s[u←Φ_{N}] =^{?} Φ_{M}) ∘ {N←N′ + p′, M←M′ + q′} = s′[u′←Φ_{N′}] =^{?} s′[u′←c[u_{c}←Φ_{M′}]]
(s[u←Φ_{N}] =^{?} Φ_{M}) ∘ {N←N′′ + p′′, M←M′′ + q′′} = s′′[u′′←Φ_{N′′}] =^{?} s′′[u′′←c[u_{c}←Φ_{M′′}]]

The Proper condition ensures that during the derivation in which a loop pair occurs twice, the trivial ρ-equation Φ_{N} =^{?} Φ_{M}, whose unification algorithm is discussed in the previous section, will not be introduced. Enforcing Proper condition just simplifies the ensuing proofs. The Minimal condition ensures that no other loop pairs occur twice during the derivation in which a loop pair occurs twice. From a minimal loop pair, we are able to construct most general unfolding-unifiers.

Example 7.2 The ρ-equation s(Φ(s(s(⋄)), N, 0)) =^{?} Φ(s(s(⋄)), M, s(0)) is a loop pair and (1, 1) is a minimal loop factor. However, the ρ-equation s(Φ(s(⋄), N, 0)) =^{?} Φ(s(⋄), M, s(0)) is not a loop pair since Φ(s(⋄), N, 0) =^{?} Φ(s(⋄), M, s(0)) violates the Proper condition.

Lemma 7.8 Let s[u←Φ_{N}] =^{?} Φ_{M} be a minimal loop pair with loop factor (p, q), then Ω(s[u←Φ_{N}])∩ Ω(Φ_{M}) is infinite if and only if

either (i) ∃k < p such that s_{k} = t_{r} for some r
or (ii) ∃r < q such that s_{k} = t_{r} for some k

Proof: ⟹: We proceed by the technique of proof by contradiction. Suppose neither condition (i) nor condition (ii) is true, then we show that Ω(s[u←Φ_{N}]) ∩ Ω(Φ_{N}) is empty. Should Ω(s[u←Φ_{N}]) ∩ Ω(Φ_{N}) be not empty, it can only be that s_{i} = t_{j} for some i ≥ p and j ≥ q. However, for every such i and j,

\begin{aligned}s_{i} & = & s′[u′←s_{i−p}] \\ t_{j} & = & s′[u′←t_{j−q}] \end{aligned}

where s′ and u′ are from the context

\begin{aligned}s[u←Φ_{N}][N←N′ + p] & = & s′[u′←s[u←Φ_{N′}]] \\ Φ_{M}[M←M′ + q] & = & s′[u′←Φ_{M′}]. \end{aligned}

Clearly, s_{i} = t_{j} if and only if s_{i−p} = t_{j−q}. After finite steps of such peeling, either condition (i) or condition (ii) has to be satisfied, which contradicts our assumption.

⟸: Obvious since for any i = m ∗ p + k and j = m ∗ q + r where m ≥ 0, s_{i} = t_{j}. □

Lemma 7.9 Let s[u←Φ_{N}] =^{?} Φ_{M} be a minimal loop pair with loop factor (p, q), and {N←p ∗ Q + k, M←q ∗ Q + r} be an unfolding-unifier of s[u←Φ_{N}] and Φ_{M} where k < p or r < q, and s_{k} = t_{r} is true, then {N←p ∗ Q + k, M←q ∗ Q + r} is a unique unfolding-unifier of s[u←Φ_{N}] and Φ_{M}.

Proof: We prove by contradiction. Note that for any i ≥ p and j ≥ q, s_{i} = t_{j} implies that s_{i−p} = t_{j−q}. Thus, we assume that there is a pair (k′, r′) distinct from (k, r) such that k′ < p or r′ < q, and s_{k′} = t_{r′} is true. Let k < k′. Note that k and k′ can not be equal since this will implies that r = r′. There are only five possibilities under which s_{k} = t_{r} and s_{k′} = t_{r′}:

• k < k′ < p and r < r′ < q,

• k < k′ < p and r < q ≤ r′,

• k < k′ < p and q ≤ r < r′,

• k < p ≤ k′ and r < r′ < q,

• p ≤ k < k′ and r < r′ < q.

We show that none of these cases can be true. Without loss of generality, let us only consider the first case, namely, k < k′ < p and r < r′ < q. The proof techniques can be generalized to other cases in a straightforward way. Note that s_{k}, t_{r}, s_{k′} and t_{r′} can be represented as follows:

\begin{aligned}s_{k} & = & s[u←h_{N}^{k}[u_{N}^{k}←l_{N}]] \\ t_{r} & = & h_{M}^{r}[u_{M}^{r}←l_{M}] \\ s_{k′} & = & s[u←h_{N}^{k}[u_{N}^{k}←h_{N}^{k′−k}[u_{N}^{k′−k}←l_{N}]]] \\ t_{r′} & = & h_{M}^{r}[u_{M}^{r}←h_{M}^{r′−r}[u_{M}^{r′−r}←l_{M}]]. \end{aligned}

Now there are three possibilities for the root positions of l_{N} and l_{M} in s_{k} and t_{r}:

• u.u_{N}^{k} = u_{M}^{r}, or

• u.u_{N}^{k}.v = u_{M}^{r} for some v, or

• u.u_{N}^{k} = u_{M}^{r}.w for some w.

The positions u_{N}^{k} and u_{M}^{r} can not be disjoint since both of them are prefixes of u′ where s′[u′←s[u←Φ_{N′}]] = s[u←Φ_{N}[N←N′ + p]]. The first can not be true since it implies that Φ_{N} =^{?} Φ_{M} is an intermediate equation, which clearly violates the Proper condition for the minimal loop pair s[u←Φ_{N}] =^{?} Φ_{M}. The second cannot be true since if s_{k} = t_{r}, namely,

\begin{aligned}s_{k} & = & s′′[u.u_{N}^{k}←l_{N}] \\ t_{r} & = & s′′[u.u_{N}^{k}←s′′′[v←l_{M}]]. \end{aligned}

then l_{N} = s′′′[v←l_{M}]. By the fact that s_{k′} = t_{r′}, we have

\begin{aligned}s_{k′} & = & t′[v′←l_{N}] \\ t_{r′} & = & t′[v′←s′′′[v←l_{M}]]. \end{aligned}

Thus, we see that Φ_{N} =^{?} s′′′[v←Φ_{M}] is a loop pair with loop factor (k′ − k, r′ − r), k′ − k < p, and r′ − r < q, which violates the Minimal condition of the s[u←Φ_{N}] =^{?} Φ_{M}.

Similarly, we can show that the possibility u.u_{N}^{k} = u_{M}^{r}.w cannot be true either. □

Lemma 7.10 If during the ρ-unification of s[u←Φ_{N}] =^{?} Φ_{M}, no loop pair can be derived, then for all i, j > m, s_{i} ≠ t_{j} where m is the maximal height of s_{1} and t_{1}.

Proof: The proof is rather tedious and the techniques used are similar to the ones in proving Lemma 8.1. □

Now let us go back to the unification s[u←Φ_{N}] =^{?} Φ_{M}. If s[u←Φ_{N}] =^{?} Φ_{M} is not a minimal loop pair, then we unfold Φ_{M}, and then decompose. Either (i) the unification terminates, or (ii) after k_{N} steps of unfolding Φ_{N} and k_{M} steps of unfolding Φ_{M}, we obtain a minimal loop pair s′[u′←Φ_{N}] =^{?} Φ_{M} with loop factor (p, q) and s_{k} = t_{r} for k < p or r < q (note that the case where the minimal loop

pair is Φ_{N} =^{?} s′′[u′′←Φ_{M}] is symmetric). The set S = {{N←i, M←j} : i < k_{N} or j < k_{M}}

∪{{N←p ∗ Q + k_{N} + k, M←q ∗ Q + k_{M} + r}} is a complete set of unfolding-unifiers of s[u←Φ_{N}] and Φ_{M}.

7.3 The Complexity of Two Special Cases of ρ-Unification

In this section, we analyze the time complexity of (i) unifying an N-term s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] and an N-generator Φ_{N}(h_{2}[u_{2}←⋄], l_{2}), and (ii) unifying an M-generator Φ_{M}(h_{M}[u_{M}←⋄], l_{M}) and an N-generator Φ_{N}(h_{N}[u_{N}←⋄], l_{N}). In the later case we often abbreviate the M-generator as Φ_{M} and the N-generator as Φ_{N}.

We start with the first case. Let the set of terms represented by L and R be

\begin{aligned}L & ≃ & \{s_{i} : s_{i} = s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})][N←i]\}, \\ R & ≃ & \{t_{i} : t_{i} = Φ_{N}(h_{2}[u_{2}←⋄], l_{2})[N←i]\}. \end{aligned}

Lemma 4.4 The time complexity of computing the complete set CUU(L, R) of most general unfolding-unifiers of two ground N-terms L and R is bounded by O(n^{3}) where n is the number of occurrences of symbols in s_{1} and t_{1}. The size of CUU(L, R) is bounded by 3m where m is the maximal height of s_{1} and t_{1}.

Proof: We analyze by the following cases:

|u_{1}| > |u_{2}| : Let p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{2}|, |u_{1}| − |u_{2}|)⌉. Clearly, p ≤ m ≤ n, By Lemma 8.1, for all i ≥ p, s_{i} ≠ t_{i}. Since the sizes of s_{n} and t_{n} are less than n^{2}, thus to check for each i < p, whether s_{i} = t_{i} is bounded by O(n^{2}). Thus it takes O(n^{3}) to check for all 0 ≤ i ≤ n, whether s_{i} = t_{i}. The size of CUU(L, R) is clearly bounded by p, which is also bounded by m.

|u_{1}| = |u_{2}| : Let p = ⌈max(height(s_{1}), height(t_{1}))/min(|u_{1}|, |u_{2}|)⌉. It is obvious that p ≤ m ≤ n. It then follows that the sizes of s_{p} and t_{p} are bounded by n^{2}, and s_{p} = t_{p} can be checked in O(n^{2}). By Lemma 8.2, if s_{p} = t_{p}, then s_{i} = t_{i} for all i. The CUU(L, R) is {id}.

If s_{p} ≠ t_{p}, then by Lemma 8.2, for all i ≥ p, s_{i} ≠ t_{i}. Since for each i < p, whether s_{i} = t_{i} can be checked in O(n^{2}), O(p ∗ n^{2}) is sufficient to computer for all i < p, whether s_{i} = t_{i}. We know that p ≤ m ≤ n. Thus the time complexity of computing CUU(L, R) is O(n^{3}), and the size of CUU(L, R) is bounded by m.

|u_{1}| < |u_{2}| : In this case our algorithm unfolds L and R in hope of deriving a pair L′ = L[N←N′ + r] = s′[u′←L′′] and R′ = R[N←N′ + r] = s′[u′←R′′] where L′′ = Φ_{N′}(h_{1}[u_{1}←⋄], l_{1}) and R′′ = s′′[u′′←Φ_{N′}(h_{1}[u_{2}←⋄], l_{2})].

If such a minimal r exists, then r satisfies the condition |u|+r ∗|u_{1}| ≤ r ∗|u_{2}|. By solving this condition, we obtain |u|/(|u_{2}| − |u_{1}|) ≤ r. Since |u|/(|u_{2}| − |u_{1}|) ≤ m and r is chosen to be minimal, r ≤ m ≤ n , and |u′′| < |u_{2}| holds. It follows that the sizes and maximal heights of L′′[N′←1] and R′′[N′←1] are less than 2n and 2m respectively. Since whether the prefixes of L′ and R′ have the form s′[u′←⋄] or not can be computed in O(n^{2}) and according to the case |u_{1}| > |u_{2}|, the complexity of computing CUU(R′′, L′′) is bounded by O(n^{3}), and the size of CUU(R′′, L′′) is bounded by 2m. It then follows that the time complexity of computing CUU(L, R) is bounded by O(n^{3}), and the size of CUU(L, R) is bounded by 2m plus r, which is bounded by 3m.

If there is no such minimal r such that unfolding L and R r times obtains L′ and R′ as above, then there must exist a minimal r such that a mismatch between L[N←r] and R[N←r] occurs, and for all i > r, L[N←i] ≠ R[N←i]. This r can be easily obtained since there are only two cases where a mismatch can happen: (i) the prefixes of L[N←r] and R[N←r] mismatch and these prefixes do not cover the positions in l_{1} and l_{2}; (ii) the positions where Φ_{N}(h_{1}[u_{1}←⋄], l_{1}) and Φ_{N}(h_{2}[u_{2}←⋄], l_{2}) occur are disjoint, and mismatch is due to that no constituent of a generator matches a ground term. In both cases, r is bounded by m, and it follows that the time complexity of computing CUU(L, R) is bounded by O(n^{3}) and the number of unfolding unifiers of L and R is bounded by m, which is less than 3m.

□

Let Φ_{N} ≃ {s_{i} : s_{i} = Φ_{N}[N←i} and Φ_{M} ≃ {t_{j} : t_{j} = Φ_{M}[M←j}.

Lemma 4.6 The time complexity of computing CUU(Φ_{N}, Φ_{M}) is bounded by O(n^{3}) where n is the number of occurrences of symbols in s_{1} and t_{1}. The size of CUU(Φ_{N}, Φ_{M}) is bounded by m where m is the maximal height of s_{1} and t_{1}.

Proof: Let p and q be the minimal integers such that |u_{N}| ∗ p = |u_{M}| ∗ q. Since |u_{N}| < n and |u_{M}| < n, then p < n and q < n. Thus the sizes of h_{N}^{p}[u_{N}←⋄] and h_{M}^{q}[u_{M}←⋄] are smaller than n^{2}. The time complexity of checking for each i < p, whether there exists a j such that s_{i} = t_{j} is bounded by O(n^{2}). Symmetrically, for each j < q, whether there exists an i such that s_{i} = t_{j} is also bounded by O(n^{2}). Since the size of s_{p} is bounded by n^{2}, the set of all i and j satisfying (0 ≤ i < p) or (0 ≤ j < q) and s_{i} = t_{j} can be computed in O(n^{3}).

If h_{N}^{p}[u_{N}←⋄] = h_{m}^{q}[u_{M}←⋄] and there exists a i ≤ p and j such that s_{i} = t_{j}, both of which can be checked in O(n^{3}), then by Lemma 8.6, the unfolding-unifier is unique and CUU(Φ_{N}, Φ_{M}) can be computed in O(n^{3}).

If h_{N}^{p}[u_{N}←⋄] = h_{m}^{q}[u_{M}←⋄], but no i ≤ p and j such that s_{i} = t_{j}, then by Lemma 8.6, the CUU(Φ_{N}, Φ_{M}) is empty. Clearly, CUU(Φ_{N}, Φ_{M}) can be computed in O(n^{3}).

If h_{N}^{p}[u_{N}←⋄] ≠ h_{m}^{q}[u_{M}←⋄], then by Lemma 8.7, there is no i > p, j > q such that s_{i} = t_{j}. Since both p and q are less than n, CUU(Φ_{N}, Φ_{M}) can be computed in O(n^{3}).

In all above cases, the size of CUU(Φ_{N}, Φ_{M}) is bounded by m. □

8 Appendix B: The Correctness of ρ-unification

The functionality of rule U10(Transform) is to perform the unfolding substitutions derived by U6(Initiate), U7(Unfold) and U8(MN-succeed). Its applications are always triggered by U6, U7 and U8. We separated it from its triggers merely to enhance the clarity of the ρ-unification algorithm. Without loss of generality, in the following proofs, we consider the application of one of U6, U7 or U8 followed by several applications of U10 as one step of ρ-unification derivation. That is to say, we designate U10 to be invisible. The consequence of this is that all the derivations will have the form (S, ∅) ⊢ (S′, ∅) where the second component is always empty. However, we frequently need to consider the ρ-substitutions associated with the derivations. In the following, we slightly change the notion of derivations and denote the new derivation as (S, Θ_{0}) ⊢ (S′, Θ_{0} ∘Θ_{1}) where Θ_{0} denotes the ρ-substitutions already collected up to the configuration (S, Θ_{0}) and Θ_{1} is the ρ-substitution associated with this particular step of derivation.

Lemma 8.1 If (S, Θ_{0}) ⊢^{∗} (∅, Θ_{0} ∘ Θ), then for each (L_{i}, R_{i}) ∈ S, L_{i}Θ =_{st} R_{i}Θ.

Proof: We proceed by induction on the number of steps of a ρ-unification derivation. Let us use ⊢^{k} to denote k steps of a ρ-unification derivation.

Base case: k = 1. The set S must contain only one equation L =^{?} R. It follows that one of U1, U2, U3 and U8 is applied. If U1 is applied, then at least one of L and R must be a variable, say R is a variable x. Θ must be ({x←L}, id), therefore LΘ = xΘ. If U2 is applied, then L = R and Θ = (ϕ, id). It then follows that LΘ = RΘ. If U3 is applied, then Θ = (ϕ, id) and L = R = a where a is a constant. It then follows that LΘ = RΘ. If U8 is applied, by corollary 4.1, Θ belongs to a complete set of unfolding-unifiers of L and R, which then implies that LΘ =_{st} RΘ. Induction Hypothesis: For all i ≤ k, the lemma follows.

Induction: Suppose for some rule Uj, ({L =^{?} R} ∪ S_{0}, Θ_{0}) ⊢_{Uj} (S′, Θ_{0} ∘ Θ_{1}) ⊢^{k} (∅, Θ_{0} ∘ Θ_{1} ∘ Θ′). Let Θ denote Θ_{1} ∘ Θ′. We show that the lemma is true w.r.t. each Uj. We do not consider U4, U5 and U9 since they do not lead to a successful derivation.

U1: Suppose R is a variable x. Now S′ = S_{0}[x←L] and Θ_{1} = ({x←L}, id). By induction hypothesis,

for each L′_{i} =^{?} R′_{i} ∈ S′, L′_{i}Θ′ = R′_{i}Θ′. But L′_{i} = L_{i}Θ_{1} and R′_{i} = R_{i}Θ_{1}. (L_{i}Θ_{1})Θ′ = (R_{i}Θ_{1})Θ′.

Therefore, by Lemma 4.3, L_{i}Θ =_{st} R_{i}Θ.

U2 & U3: Obvious since Θ_{1} = (ϕ, id), and by induction hypothesis, the lemma follows.

U6 : Θ_{1} = (ϕ, {N←0}). By induction hypothesis, for each L′_{i} =^{?} R′_{i} ∈ S′, L′_{i}Θ′ =_{st} R′_{i}Θ′. Thus L′_{i} = L_{i}[N←0] and R′_{i} = R_{i}[N←0]. It then follows that (L_{i}Θ_{1})Θ′ =_{st} (R_{i}Θ_{1})Θ′. By lemma 4.3,

L_{i}Θ =_{st} R_{i}Θ.

U7 : Similar to the proof of U6.

U8: Follows directly from corollary 4.1 and the induction hypothesis. □

The following lemma is to show the completeness of ρ-unification.

Lemma 8.2 Given a configuration (S, Θ_{0}), if Ψ = (α, ẽs) is a ρ-unifier of L_{i} and R_{i} satisfying that for every L_{i} =^{?} R_{i} ∈ S such that (i) L_{i}∘ẽs and R_{i}∘ẽs are constituents of L_{i} and R_{i} respectively, and (ii) α is the most general unifiers of L_{i} ∘ẽs and R_{i} ∘ẽs, then there exists a successful derivation

(S, Θ_{0}) ⊢^{∗} (∅, Θ_{0} ∘ Θ)

such that

L_{i}Θ =_{st} R_{i}Θ, and L_{i}Ψ = R_{i}Ψ is in Ω(L_{i}Θ = R_{i}Θ)

Proof: We prove the lemma by induction on the lexicographic ordering of the complexity measure (A, B, D, E) of the configuration (S, Θ_{0}) which was defined right before the termination theorem Theorem 4.1, namely A and B are the numbers of distinct first order variables and occurrences of degree variables in S respectively, D is the multiset of the lengths of the positions at which the first order variables occur in ρ-terms of S, and E is the multiset of the lengths of maximally and pairwisely shared paths of generators in ρ-terms of S. Without loss of generality (cf Lemma 4.1), let us assume Θ = (θ, es) such that Ψ is in normalized form in the sense that Range_{Φ}(α) ∩ Dom_{Φ}(ẽs) = ∅.

Base Case : (A, B, D, E) = (0, 0, ∅, ∅). Trivially true.

Induction Hypothesis: For all (A′, B′, D′, E′) <_{lex} (A, B, D, E), the lemma is true.

Induction Step: We proceed by studying the structure of the first equation in S. Let S = {L_{1} =^{?} R_{1}} ∪ S_{0}.

Case 1: (Either L_{1} or R_{1} is a variable). Let us assume that R_{1} = x and x ∉ V (L_{1}) if L_{1} is not a variable. Since xΨ is a first order term and Ψ is in normalized form, it follows that x←t ∈ α for some first order term t. Thus, xΨ = L_{1}Ψ = t. Thus, Ψ can be written as Ψ = ({x←L_{1}}, ∅) ∘ (α′, ẽs) where α′ is obtained from α by deleting x←t of α. Let Ψ′ denote (α′, ẽs). Clearly, L_{1}Ψ = L_{1}Ψ′ = t. For every L′_{i} =^{?} R′_{i} ∈ S_{0}[x←L_{1}] where L′_{i} = L_{i}[x←L_{1}] and R′_{i} = R_{i}[x←L_{1}], we have L′_{i}Ψ′ = R′_{i}Ψ′. Now the complexity measure of S_{0}[x←L_{1}] is less than (A, B, D, E), by induction hypothesis,

(S_{0}[x←L_{1}], Θ_{0} ∘ ({x←L_{1}}, ∅)) ⊢^{∗} (∅, Θ_{0} ∘ ({x←L_{1}}, ∅) ∘ Θ′)

for some ρ-unifier Θ′ such that for every L′_{i} =^{?} R′_{i} ∈ S_{0}[x←L_{1}], L′_{i}Θ′ =_{st} R′_{i}Θ′, and L′_{i}Ψ′ = R′_{i}Ψ′ is in Ω(L′_{i}Θ′ = R′_{i}Θ′). By applying U1,

({L_{1} =^{?} x} ∪ S_{0}, Θ_{0}) ⊢ (S_{0}[x←L_{1}], Θ_{0} ∘ ({x←L_{1}}, id)).

Therefore,

({L_{1} =^{?} x} ∪ S_{0}, Θ_{0}) ⊢^{∗} (∅, Θ_{0} ∘ ({x←L_{1}}, id) ∘ Θ′).

Let Θ = ({x←L_{1}}, id) ∘ Θ′, we are done.

Case 2: (One of them is Φ_{N} and another one is a ground N-term.) Let us assume that L_{1} = s[u←Φ_{N}(h_{1}[u_{1}←⋄], l_{1})] and R_{1} = Φ_{N}(h_{2}[u_{2}←⋄], l_{2}). If L_{1} and R_{1} are strongly equivalent, which means L_{1}[N←i] = R_{1}[N←i] for all i ≥ 0, then the premise can be stated as : for all (L_{i}, R_{i}) ∈ S_{0}, L_{i}Ψ = R_{i}Ψ. By induction hypothesis, we have

(S_{0}, Θ_{0}) ⊢^{∗} (∅, Θ_{0} ∘ Θ′)

such that

L_{i}Θ′ = R_{i}Θ′, and L_{i}Ψ = R_{i}Ψ is in Ω(L_{i}Θ′ = R_{i}Θ′).

By application of U8 and Corollary 4.1, ({L_{1} =^{?} R_{1}} ∪ S, Θ_{0}) ⊢ (S_{0}, Θ_{0}), we let Θ = Θ′ and we are done. If L_{1} ≠_{st} R_{1}, there exists a p such that for all i ≥ p, L_{1}[N←i] ≠ R_{i}[N←i]. Thus, there is some N←k ∈ ẽs where k < p such that L_{1}[N←k] = R_{1}[N←k]. Now let us write Ψ as (ϕ, {N←k}) ∘ (α, ẽs′) where ẽs′ is ẽs − {N←k}. Let Ψ′ = (α, ẽs′). By corollary 4.1, {N←k} is an unfolding unifier of L_{1} and R_{1}. Then by U8, ({L_{1} =^{?} R_{1}} ∪ S_{0}, Θ_{0}) ⊢ (S′_{0}, Θ_{0} ∘ (ϕ, {N←k})) where

S′_{0} = {L_{i}[N←k] =^{?} R_{i}[N←k] : L_{i} =^{?} R_{i} ∈ S_{0}}. Now, for L′_{i} =^{?} R′_{i} ∈ S′_{0}, L′_{i}Ψ′ = R′_{i}Ψ′. Then by

induction hypothesis, there is a derivation (S′_{0}, Θ_{0} ∘ (ϕ, {N←k})) ⊢^{∗} (∅, Θ_{0} ∘ (ϕ, {N←k}) ∘ Θ′) such that for each L′_{i} =^{?} R′_{i} ∈ S′_{0}, L′_{i}Θ′ =_{st} R′_{i}Θ′ and L′_{i}Ψ′ = R′_{i}Ψ′ is in Ω(L′_{i}Θ′ = R′_{i}Θ′). Let Θ denote (ϕ, {N←k}) ∘ Θ′. The lemma follows.

Case 3: (One of them is a ground N-term s[u←Φ_{N}] and another one is Φ_{M}). Let us assume L_{1} = s[u←Φ_{N}] and R_{1} = Φ_{M}. Since both L_{1}Ψ and R_{1}Ψ are ground first order terms, then for some integers k and r, ẽs_{0} = {N←k, M←r} ⊆ ẽs. Thus, Ψ = (ϕ, ẽs_{0}) ∘ (α, ẽs′) where ẽs′ = ẽs−ẽs_{0}. According to corollary 4.1, U7 is provided with a complete set EU of unfoldingunifiers of L_{1} and R_{1}. Thus, either ẽs_{0} ∈ EU or ẽs_{0} is less general than es_{0} for some es_{0} ∈ EU. If it is the former, the induction hypothesis and the rule U7 can be applied to conclude the lemma. Otherwise, es_{0} = {N←p′ ∗ Q′ + k′, M←q′ ∗ Q′ + r′}, and ẽs_{0} = es_{0} ∘ {Q′←q′′} for some q′′. Thus, Ψ can be represented as (ϕ, es_{0}) ∘ Ψ′ where Ψ′ = (ϕ, {Q←q′′}) ∘ (α, ẽs′). Since for each L_{i} =^{?} R_{i} ∈ S_{0}, L_{i}Ψ = R_{i}Ψ, it follows that (L_{i} ∘ es_{0})Ψ′ = (R_{i} ∘ es_{0})Ψ′. By rule 8,

({L_{1} =^{?} R_{1}} ∪ S_{0}, Θ_{0}) ⊢ (S_{0} ∘ es_{0}, Θ_{0} ∘ (ϕ, es_{0})).

Clearly, the complexity measure of S_{0}∘es_{0} is smaller than (A, B, D, E). By induction hypoth-

esis, (S_{0} ∘ es_{0}, Θ_{0} ∘ (ϕ, es_{0})) ⊢^{∗} (∅, Θ_{0} ∘ (ϕ, es_{0}) ∘ Θ′) and for each L_{i} ∘ es_{0} =^{?} R_{i} ∘ es_{0} ∈ S_{0} ∘ es_{0},

(L_{i} ∘ es_{0})Θ′ =_{st} (R_{i} ∘ es_{0})Θ′, Θ′ ≤ Ψ′. Let Θ = (ϕ, es_{0}) ∘ Θ′, and we are done.

Case 4 : L_{1} = f(s_{1}, ..., s_{n}) and R_{1} = f(t_{1}, ..., t_{n}). Notice that for Ψ, L_{1}Ψ = R_{1}Ψ if and only s_{1}Ψ = t_{1}Ψ, ⋯, s_{n}Ψ = t_{n}Ψ. If at least one of L_{1} and R_{1} has first order variables, then the application of U3 rule decreases D, and then decreases the complexity measure. Notice that U3 does not introduce any ρ-substitution. By the induction hypothesis, the lemma follows. Similar argument applies when at least one of L_{1} and R_{1} contains more than one generators. In this case, E is decreased.

It then leaves the cases where (i) both L_{1} and R_{1} are ground terms; (ii) L_{1} is a ground term and R_{1} is a ground N-term; (iii) L_{1} and R_{1} are ground N-term and M-term respectively (N and M can be the same degree variable). In case (i), L_{1} = R_{1}. By U2, we have ({L_{1} =^{?} R_{1}} ∪ S_{0}, Θ_{0}) ⊢ (S_{0}, Θ_{0}). Since S_{0} is finite, either finitely many applications of U2 lead to a successful derivation from which the lemma follows or another rule has to be applied.

In case (ii), Ψ can be rewritten as

Ψ = (α, {N←k} ∘ ẽs′) = (ϕ, {N←k}) ∘ (α, ẽs′) for a k such that L_{1} = R_{i}[N←k].

It then follows that

for each L′_{i} =^{?} R′_{i} ∈ S_{0}[N←k], L′_{i} ∘ (α, ẽs′) = R′_{i} ∘ (α, ẽs′).  (4)

After k applications of U7, and an application of U6, interleaved with finitely many applications of U3 and U10, we have

({L_{1} =^{?} R_{1}} ∪ S_{0}, Θ_{0}) ⊢^{∗} (S_{0}[N←k], (ϕ, Θ_{0} ∘ {N←k})).

Thus by the condition given by equation 4, and induction hypothesis, the lemma follows easily.

In case (iii), after finitely many decompositions, we will have

({L_{1} =^{?} R_{1}} ∪ S_{0}, Θ_{0}) ⊢^{∗} ({w_{1} =^{?} w′_{1}, ⋯, w_{m} =^{?} w′_{m}} ∪ S_{0}, Θ_{0})

where at most one of w_{i} is a ground N-term, at most one of w′_{i} is a ground M-term, at least one of w_{i} and w′_{i} is a generator, and rest of w_{j} and w′_{j} are ground terms. Thus, one of the cases (Case 2, Case 3, Case 4-i, Case 4-ii) we have discussed can be applied and the lemma follows.

Case 5 : (L_{1} = f(s_{1}, ..., s_{n}) and R_{1} = Φ_{N} where L_{1} is neither a ground N-term nor a ground M-term.) The case where L_{1} is a ground term has been proved in Case 4-ii. The remaining cases will be (i) L_{1} contains first order variables x_{1}, ..., x_{m}; (ii) L_{1} has more than one generators.

By premise and the fact that R_{1} is a ground N-term, L_{1}Ψ = R_{1}Ψ implies that for some k, R_{1}[N←k] = R_{1}Ψ.

If k = 0, then Ψ can be written as (ϕ, {N←0}) ∘ (α, ẽs′) where ẽs′ = ẽs − {N←0}. Thus, the premise L_{i}Ψ = R_{i}Ψ implies that

L_{i}[N←k] ∘ (α, ẽs′) = R_{i}[N←k] ∘ (α, ẽs′).  (5)

U6 can be applied. Then by equation 6 and the induction hypothesis, the lemma follows.

If k > 0 then Ψ can be written as (ϕ, {N←M + 1}) ∘ (α, ẽs′) where ˜(es′) = (ẽs − {N←k}) ∪ {M←k − 1}. Thus, the premise L_{i}Ψ = R_{i}Ψ implies that

L_{i}[N←M + 1] ∘ (α, ẽs′) = R_{i}[N←M + 1] ∘ (α, ẽs′).  (6)

We have the corresponding derivation

({f(s_{1}, ..., s_{n}) =^{?} Φ_{N}} ∪ S_{0}, Θ_{0}) ⊢_{U7} ({f(s′_{1}, ..., s′_{n}) =^{?} f(t′_{1}, ..., t′_{n})} ∪ S′_{0}, Θ_{0} ∘ (ϕ, {N←M + 1})).

In case (i), U3 decreases D. In case (ii), U3 decreases E. In both cases, the complexity measure is decreased. Thus, by induction hypothesis and the result of Case 4, lemma follows. □