A Compositional Semantic Basis for the

Analysis of Equational Horn Programs^{∗}

María Alpuente ^{§}  Moreno Falaschi ^{¶}  Germán Vidal^{§}

September 4, 1996

Abstract We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equational setting and that the test of satisfiability in this setting can be done in parallel.

Keywords: Semantic analysis, compositionality, equational logic programming, conditional term rewriting systems.

1 Introduction

Compositionality is a desirable property which has been recognised as fundamental in the semantics of programming languages [38, 40]. Compositionality has to do with a (syntactic) composition operator ⋄, and holds when the meaning (semantics) S(C_{1} ⋄ C_{2}) of a compound construct is defined by composing the meanings of the constituents S(C_{1}) and S(C_{2}), i.e. for a suitable function f_{⋄}, S(C_{1} ⋄ C_{2}) = f_{⋄}(S(C_{1}), S(C_{2})). In the case of logic programs [13], the properties of two most important operators have been widely investigated, namely AND-composition (of atoms in a goal or in a clause body) and OR-composition, i.e. composition of (sets of) clauses. In the context of equational logic programming [20, 24], compositionality of the semantics has not been much investigated yet. In this paper, we address the problem of solving equations in equationally defined theories: we want to define compositionally the meaning of the union of E-unification problems. Let a theory E be fixed and consider two finite equation sets Γ_{1}, Γ_{2}. We want to define the meaning of Γ_{1} ∪ Γ_{2} (with respect to E) in terms of the meanings of Γ_{1} and Γ_{2}. Throughout the paper, E is assumed to be axiomatized as an equational Horn theory, which is called the ‘program’ [14, 20, 24]. We do not consider compositionality with respect to the union of programs in this paper. For this topic we refer to [4]. [4] defines a compositional semantics for the direct union of complete theories which correctly models the computational properties related to the use of logical variables.

∗This work has been partially supported by CICYT under grant TIC 95-0433-C03-03 and by HCM project CONSOLE.

§Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo.

22012, 46071 Valencia, Spain. e.mail:{alpuente,gvidal}@dsic.upv.es

¶Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy. e.mail:

falaschi@dimi.uniud.it

The semantics of equational Horn programs is usually defined as some variant of narrowing, a method for generating complete sets of E-unifiers with respect to a canonical set of clauses. Simple restrictions on narrowing, like narrowing only at basic positions, are still complete for theories which satisfy some additional properties [31]. The use of narrowing as the operational mechanism for computing leads to a powerful extension of ordinary logic programs [20, 35] and the computation model has many opportunities for parallelism. For example, [12] describes a kind of OR-parallelism in which, for each position in the term and each rule in the program, alternative narrowings are explored concurrently according to some heuristic function. Our work concerns an AND-parallel computation model of equational Horn programs, where all subexpressions can be narrowed independently and the computed substitutions obtained so far can then be composed. This mechanism of computation was also mentioned in [35]. We extend the notion of parallel composition of substitutions introduced in [22, 33] to the case of equational logic programs. Hence we show how complete sets of E-unifiers for a given goal ⇐ Γ_{1}, Γ_{2} can be generated by composing the complete sets of E-unifiers computed by narrowing for the separate subgoals ⇐ Γ_{1} and ⇐ Γ_{2}. This allows us to model the combination of substitutions computed by AND-parallel ‘narrowing processes’, i.e. by agents which narrow subexpressions in parallel. We show that for unrestricted narrowing a ‘semantic’ composition operator would be necessary. However, for basic narrowing we achieve a stronger result and show that the substitutions can be composed syntactically.

We have recently defined an equational logic language [1] as an instance of Constraint Logic Programming [23], where the equations to be solved with respect to an equational theory are considered as constraints. For a computational step in this framework, it is essential to be able to (semi-)decide if a set of equations is satisfiable. The computation of complete sets of E-unifiers is less striking in this context, while it is essential a mechanism to evaluate the satisfiability of the constraints incrementally [1]. In [2], we have defined a lazy procedure which does not prove the satisfiability of the equational constraint c but just checks that c is not unsatisfiable by means of an approximated narrower. We show that a compositional narrowing can be taken as a basis for a compositional analysis for the problem of unsatisfiability. Then we show that compositionality leads, as a by-product, to an incremental implementation for the analysis. Therefore, while OR-compositionality, i.e. compositionality w.r.t. union of programs, has proven significant for programming with modules [4, 13], we show that AND-compositionality can lead to incremental computations.

This paper is organized as follows. After introducing some preliminary notions in Section 2, Section 3 defines an operator which describes the operational semantics of equational Horn programs in a compositional way. In Section 4, we introduce compositional conditional narrowing, an AND-parallel computation model for equational Horn programs. We characterize compositionally the success set of a goal, i.e. the set of the computed answer substitutions corresponding to all successful narrowing derivations. That is, we prove that the meaning of a composite goal can be obtained by composing the meanings of its conjuncts, when considering the success set as observable. Then we state the completeness of our semantics. In Section 5 we recall an abstract algorithm for the static analysis of unsatisfiability of equation sets [2, 3] and modify it to perform the analysis compositionally.

The analysis is based on two ideas. First, the construction of a finite graph of terms built from the equational theory, which helps one to know the narrowing derivations which definitely terminate. Secondly, the approximation of the narrowing derivations by means of an abstract calculus whose derivations cover all concrete computations. Our method introduces a generic technique of loop detection to ensure termination. We also present a specific loop-check which does not depend on the equation set to be solved. Section 6 formulates an incremental analyzer for equational constraints and presents some encouraging results from the implementation of the analyzer. Section 7 concludes. The proofs of the theorems are given in Appendix A. A preliminary version of this paper appeared in [5].

2 Preliminaries

We briefly recall some known results about equations, conditional rewrite systems and equational unification. For full definitions refer to [11, 25]. Throughout this paper, V will denote a countably infinite set of variables and Σ denotes a set of function symbols, each with a fixed associated arity. τ(Σ ∪ V ) and τ(Σ) denote the sets of terms and ground terms built on Σ ∪ V and Σ, respectively. A Σ-equation s = t is a pair of terms s, t ∈ τ(Σ ∪ V ). Terms are viewed as labelled trees in the usual way. Occurrences are represented by sequences, possibly empty, of natural numbers used to address subterms of t, and they are ordered by the prefix ordering u ≤ v if there exists w such that uw = v. We let Λ denote the empty sequence. O(t) denotes the set of occurrences of a term t. Ō(t) denotes the set of nonvariable occurrences of a term t. t_{|u} is the subterm at the occurrence u of t. t[r]_{u} is the term t with the subterm at the occurrence u replaced with r. t[u] denotes the label in t at occurrence u ∈ Ō(t). These notions extend to equations in a natural way. Identity of syntactic objects is denoted by ≡. Var(s) is the set of distinct variables occurring in the syntactic object s. A fresh variable is a variable that appears nowhere else. The symbol denotes a finite sequence of symbols.

We describe the lattice of equation sets following [7]. We let Eqn denote the set of possibly existentially quantified finite sets of equations over terms. Elements of Eqn are regarded as (quantified) conjunctions of equations and treated modulo logical equivalence. We let fail denote the unsatisfiable equation set, which (logically) implies all other equation sets. Likewise, the empty equation set, denoted by true, is implied by all elements of Eqn. We write E ≤ E′ if E′ logically implies E. Thus Eqn is a lattice ordered by ≤ with bottom element true and top element fail. An equation set is solved if it is either fail or it has the form ∃y_{1} … ∃y_{m}. {x_{1} = t_{1}, …, x_{n} = t_{n}}, where each x_{i} is a distinct variable not occurring in any of the terms t_{i} and each y_{i} occurs in some t_{j} . Any set of equations E can be transformed into an equivalent one solve(E) which is solved. We restrict our interest to the set of idempotent substitutions over τ(Σ∪V ), which is denoted by Sub. There is a natural isomorphism between substitutions and unquantified equation sets. Given a solved unquantified equation set E = {x_{1} = t_{1}, …, x_{n} = t_{n}}, we let sub(E) = {x_{1}/t_{1}, …, x_{n}/t_{n}}. Also, the equational representation of a substitution θ = {x_{1}/t_{1}, …, x_{n}/t_{n}} is the set of equations θ̂ = {x_{1} = t_{1}, …, x_{n} = t_{n}}. The identity function on V is called the empty substitution and denoted by ϵ. Given a substitution θ and a set of variables W ⊆ V , we denote by θ_{|Ẁ} the substitution obtained from θ by restricting its domain, Dom(θ), to W .

We consider the usual preorder on substitutions ≤: θ ≤ σ iff ∃γ. σ ≡ θγ. Note that θ ≤ σ iff σ̂ ⇒ θ̂ [33]. A substitution {x_{1}/t_{1}, …, x_{n}/t_{n}} is a unifier of an equation set E iff {x_{1} = t_{1}, …, x_{n} = t_{n}} ⇒ E. We denote the set of unifiers of E by unif (E) and mgu(E) denotes the most general unifier of the unquantified equation set E. In abuse of notation, we let fail denote failure when computing the mgu(E). While every unquantified equation set has a most general unifier [28], this is not generally true for equation sets with existentially quantified variables [7]. We write s =^{?} t when we want to point out the fact that two terms s and t do unify.

We define an equational Horn theory E to be a finite set of (universally quantified) equational Horn clauses of the form e ⇐ e_{1}, …, e_{n}, n ≥ 0, where e, e_{i}, i = 1, …, n, are equations. An equational goal is an equational Horn clause with no head. We let Goal denote the set of equational goals. The set of states is defined by State = Goal × Sub.

A Conditional Term Rewriting System (CTRS for short) is a pair (Σ, R) where R is a finite set of reduction (or rewrite) rule schemes of the form (λ → ρ ⇐ C ), λ, ρ ∈ τ(Σ ∪ V ), λ ∉ V and Var(ρ) ⊆ Var(λ). The condition C is a possibly empty conjunction e_{1}, …, e_{n}, n ≥ 0, of equations. Variables in C that do not occur in λ are called extra-variables. If a rewrite rule has no condition we write λ → ρ. When the condition in every rule in R is empty the system is said to be unconditional. Otherwise, it is said to be conditional. We will often write just R instead of (Σ, R). We let Ctrs denote the set of conditional term rewriting systems.

A term s conditionally rewrites to a term t, written s →_{R} t, if there exists a rule (λ → ρ ⇐ s_{1} = t_{1}, …, s_{n} = t_{n}) ∈ R, an occurrence u ∈ O(s), and a substitution σ such that s_{|u} = λσ, t = s[ρσ]_{u} and, for each i = 1, …, n, there exists a term w_{i} such that s_{i}σ →_{R}^{∗} w_{i} and t_{i}σ →_{R}^{∗} w_{i}. When no confusion can arise, we omit the subscript R.

An equational Horn theory E whose clauses λ = ρ ⇐ C satisfy the assumptions λ ∉ V and Var(ρ) ⊆ Var(λ) can be viewed as a CTRS R where the rules are the heads (implicitely oriented from left to right) and the conditions are the respective bodies. We assume that these assumptions hold for all theories we consider in this paper. The equational theory E is said to be canonical (complete) if the binary one-step conditional rewriting relation →_{R} defined by R is noetherian and confluent.

Let R be a CTRS. A function symbol f ∈ Σ is irreducible iff there is no rule (λ → ρ ⇐ C ) ∈ R such that f occurs as the outermost function symbol in λ, otherwise it is a defined function symbol. In theories where the above distinction is made, the signature Σ is partitioned as Σ = C ⨄ F, where C is the set of irreducible function symbols and F is the set of defined function symbols. The elements of C are often called constructors.

For CTRS R, r << R denotes that r is a new variant of a rule in R such that r contains no variable previously met during computation (standardised apart). The instantiated left-hand side λσ of a reduction rule (λ → ρ ⇐ C ) is called a redex (reducible expression) with contractum ρσ. Given a CTRS R, an equational goal clause ⇐ g conditionally narrows into a goal clause ⇐ g′ (in symbols ⇐ g ↪^{θ} ⇐ g′) if there exists an equation e ∈ g, u ∈ Ō(e), a standardised apart variant (λ → ρ ⇐ C ) << R and a substitution θ such that θ = mgu({e_{|u} = λ}) and g′ = ((g − {e}) ∪ {e[ρ]_{u}} ∪ C )θ. s is called a (narrowing) redex iff there exists a new variant (λ → ρ ⇐ C ) of a reduction rule in R and a substitution σ such that sσ ≡ λσ. A narrowing derivation is defined by ⇐ g ↪^{θ ∗} ⇐ g′ iff ∃θ_{1}, …, θ_{n}. ⇐ g ↪^{θ_{1}} … ↪^{θn} ⇐ g′ and θ = θ_{1} … θ_{n}. We say that the derivation has length n. If n = 0 then θ = ϵ. In order to treat syntactical unification as a narrowing step, we add to the CTRS R the rule (x = x → true ⇐), x ∈ V . Then ⇐ (t = s) ↪^{σ} ⇐ true holds iff σ = mgu({t = s}). A successful derivation for ⇐ g in R ∪ {x = x → true ⇐} is a narrowing derivation ⇐ g ↪^{θ ∗} ⇐ true and θ_{|V̀ar(g)} is called a computed answer substitution for ⇐ g in R.

An important kind of equational Horn theories are those which are level-confluent [15, 31]. Let →_{R} be the conditional rewrite relation corresponding to a Horn equational theory E. Then →_{R} is equivalent to →_{R}= ∪_{i≥0}{→_{Ri} }, where:

(1) →_{R_{0}}= ∅; and

(2) t →_{R_{n+1}} t′ holds iff there is a rule (λ → ρ ⇐ C ) ∈ R, a non-variable occurrence u of t and a substitution σ such that t_{|u} = λσ, t′ = t[ρσ]_{u} and sσ ↓_{Rn} s′σ for all (s = s′) ∈ C . →_{R} is called level-confluent [15] iff, for each n ≥ 0, the relation →_{Rn} is confluent. Level confluence can still be ensured by syntactic conditions [15]. Of course, level confluence implies confluence. We call R level-canonical if →_{R} is level-confluent and noetherian. This is equivalent to say that each →_{Rn} is canonical. The notion of level-canonicity of a conditional term rewriting system extends in the obvious way to equational Horn theories.

Each equational Horn theory E generates a smallest congruence relation =_{E} called E-equality on the set of terms τ(Σ ∪ V ) (the least equational theory which contains all logic consequences of E under the entailment relation ⊧ obeying the axioms of equality for E). E is a presentation or axiomatization of =_{E}. In abuse of notation, we sometimes speak of the equational theory E to denote the theory axiomatized by E. E-equality is extended to substitutions by σ=_{E}θ iff ∀x ∈ V . xσ=_{E}xθ.

A finite set of equations Γ = {s_{1} = t_{1}, …, s_{n} = t_{n}} together with an equational theory E is called an E-unification problem. A substitution σ is an E-unifier of the equation set Γ iff E ⊧ (σ̂ ⇒ Γ) [30]. By abuse of notation, σ is often called solution. The set U_{E}(Γ) of all E-unifiers of Γ is recursively enumerable [14, 20, 39].

For E-unification problems, the notion of most general unifier generalizes to complete sets of minimal (incomparable) E-unifiers. A set S of E-unifiers of the equation set Γ is complete iff every E-unifier σ of Γ factors into σ =_{E} θγ for some substitutions θ ∈ S and γ. A complete set of E-unifiers of a system of equations may be infinite. Minimal complete sets μU_{E}(Γ) of E-unifiers of Γ do not always exist. An E-unification procedure is complete if it generates a complete set of E-unifiers for all input equation system. Conditional narrowing has been shown to be a complete E-unification algorithm for canonical theories satisfying different restrictions [20, 31]. Since unrestricted narrowing has quite a large search space, several strategies to control the selection of redexes have been devised to improve the efficiency of narrowing by getting rid of some useless derivations (see [16] for a recent survey). Narrowing at only basic positions [15, 20, 21, 31, 32] has been proven to be a complete E-unification algorithm for level-canonical Horn equational theories.

3 Equational Parallel Composition

In the following, we recall the notion of parallel composition of substitutions, denoted by ⇑. Roughly speaking, parallel composition is the operation of unification generalized to substitutions.

Parallel composition corresponds to one of the basic operations performed by the AND-parallel execution model of logic programs [18, 22, 33]. Namely, when two subgoals (of the same goal) are run in parallel, the answer substitutions (computed independently) have to be combined to get the final result. This ‘combination’ can be done as follows [18, 22, 33]. Given two idempotent substitutions θ_{1} and θ_{2}, we let θ_{1} ⇑ θ_{2} = mgu(θ̂_{1} ∪ θ̂_{2}). Parallel composition is idempotent, commutative, associative and has a null element fail and an identical element ϵ. ⇑ is lifted to sets of substitutions by

Θ_{1} ⇑ Θ_{2} = \{ \begin{matrix}⋃_{θ_{1}∈Θ_{1},θ_{2}∈Θ_{2}}\{θ_{1} ⇑ θ_{2}\} & if it is different from \{fail\} \\ Ø & otherwise. \end{matrix}

Parallel composition was proposed in [33] as a basis for a compositional characterization of the semantics of Horn Clause Logic. We are able to generalize the notion of parallel composition to the case when unification in equational theories is considered. In the following definition we formalize the notion of equational parallel composition, denoted by ⇑_{E}.

Definition 3.1 Let θ_{1}, θ_{2} ∈ Sub. We define the operator ⇑_{E} : Sub × Sub → ℘(Sub) as follows:

θ_{1} ⇑_{E} θ_{2} = U_{E}(θ̂_{1} ∪ θ̂_{2}).

Example 1 Let E = {f (0) = 0, f (g(X )) = g(X ), g(0) = c(0), g(c(X )) = g(X )}.

1. Let θ_{1} = {X /g(Z )} and θ_{2} = {X /c(Z )}. Then {X /c(0), Z /0} ∈ θ_{1} ⇑_{E} θ_{2}.

2. Let θ_{1} = {X /f (0)} and θ_{2} = {X /g(Z )}. Then θ_{1} ⇑_{E} θ_{2} = Ø.

The operator ⇑_{E} can be lifted to sets of substitutions as follows.

Definition 3.2 Given Θ_{1}, Θ_{2} ∈ ℘(Sub), let:

Θ_{1} ⇑_{E} Θ_{2} = ⋃_{θ_{1}∈Θ_{1},θ_{2}∈Θ_{2}}θ_{1} ⇑_{E} θ_{2}.

It is straightforward to show that ⇑_{E} is commutative and associative and has null element Ø.

Given an E-unification problem Γ = Γ_{1} ∪ Γ_{2}, a compositional characterization of the set of all E-unifiers of Γ is given in the following proposition.

Proposition 3.3 Let Γ = Γ_{1} ∪ Γ_{2}, Θ_{1} = U_{E}(Γ_{1}) and Θ_{2} = U_{E}(Γ_{2}). Then U_{E}(Γ) = Θ_{1} ⇑_{E} Θ_{2}.

We note that it is much more complex to evaluate ⇑_{E} than the much simpler operation ⇑. However, equational parallel composition can be redefined in terms of ‘most general’ unifiers in the case of finitary theories, for which the solutions to an E-unification problem Γ can always be represented by a complete and minimal finite set μU_{E}(Γ) of (maximally general) E-unifiers, which is unique up to equivalence [39]. Equational theories which are of finitary unification type play an important role in logic programming with equality [24]. In general, the unification type of an equational theory is undecidable. On the other hand, for a finitary theory the minimality requirement is often too strong, since an algorithm which generates a superset of μU_{E}(Γ) may be far more efficient than a minimal one and hence sometimes preferable. In the following section, we will show that we can still work with ordinary parallel composition ⇑ when we consider the class of (level-)canonical equational theories, for which the problem of E-unification reduces to ordinary (syntactic) unification plus narrowing [21].

4 Compositional Conditional Narrowing

In this section we present a compositional structured operational semantics for our language. Following the standard definitions, what we observe about a goal ⇐ g in a program R is the success set. We describe the success set of a goal, i.e. the set of the computed answer substitutions corresponding to all successful narrowing derivations, by a formal operational semantics O : Goal ↦ ℘ Sub, based on a transition relation, which associates a set of substitutions with a goal.

Basic (conditional) narrowing is a restricted form of (conditional) narrowing where only terms at basic occurrences are considered to be narrowed [21, 31]. Informally, a basic occurrence is a nonvariable occurrence of the original goal or one that was introduced into the goal by the nonvariable part of the right-hand side or the condition of a rule applied in a preceeding narrowing step. The idea behind the concept of basic is to avoid narrowing steps on subterms that are introduced by instantiation. Basic conditional narrowing is a complete method for solving equations in the theory defined by a level-canonical conditional term rewriting system [31], and has been proposed as the operational model of equational logic programs in [20]. In the rest of this paper, we assume the level-canonical CTRS R to be fixed.

We formulate basic conditional narrowing according to the partition of equational goals into a skeleton and an environment part, as in [20]. The skeleton part is a set of equations g and the environment part is a substitution θ. Substitutions are composed in the environment part, but are not applied to the equations in the skeleton part, as opposed to ordinary (unrestricted) narrowing (cf. Section 2). Due to this representation, the basic occurrences in gθ are all in g, whereas the non-basic occurrences are all in the codomain of θ. This ensures that no narrowing step will reduce any expression brought by a substitution computed in a previous step. The calculus is defined as a transition system (State, ⇝) whose transition relation ⇝ ⊆ State × State formalizes the computation steps [34]. We define the basic conditional narrowing relation ⇝ as the smallest relation satisfying

\frac{e ∈ g ∧ u ∈ Ō(e) ∧ (λ → ρ ⇐ C ) << R ∧ σ = mgu(\{e_{|u}θ = λ\})}{⟨⇐ g, θ⟩ ⇝ ⟨⇐ (g − \{e\}) ∪ \{e[ρ]_{u}\} ∪ C , θσ⟩}

A basic conditional narrowing derivation is a sequence of states s_{1} ⇝ s_{2} ⇝ …, where s_{i} ≡ ⟨⇐ g_{i}, θ_{i}⟩ is the ith state in the sequence.

Based on this transition system, we define the operational semantics of an equational goal ⇐ g in the CTRS R ∪ {x = x → true ⇐} by the (non ground) set (success set)

O_{R}(⇐ g) = {θ_{|V̀ar(g)} | ⟨⇐ g, ϵ⟩ ⇝^{∗} ⟨⇐ true, θ⟩}.

We often write O(⇐ g) instead of O_{R}(⇐ g) when R is understood.

We want to give a compositional description of the answers computed by a goal. Our aim is to formulate a compositional calculus based on basic conditional narrowing. Informally, we consider the basic strategy here because, in order to prove the equivalence between the (standard) operational semantics and its compositional version, we need the standard semantics to be compositional w.r.t. the AND operator. It is easy to prove that this condition holds for basic conditional narrowing. The next theorem shows that the standard success set semantics O is compositional w.r.t. the AND operator^{1}.

1Here we do not consider the problem of the independent ‘standardization apart’ of the parallel computations for g_{1} and g_{2}

Theorem 4.1 O(⇐ g_{1}, g_{2}) = O(⇐ g_{1}) ⇑ O(⇐ g_{2})

The proof of Theorem 4.1 heavily depends on the fact we are dealing with the basic strategy. We note that this result does not hold for ordinary (unrestricted) narrowing, i.e. ordinary narrowing is not compositional using the parallel composition operator ⇑. Roughly speaking, what is wrong with ordinary narrowing is the fact that it transfers terms from the substitution part into the goal, thus introducing narrowing steps (at non-basic positions) that might not be proven when the subgoals are solved independently. The following example illustrates this point.

Example 2 Let R be the following program

R = {  z(s(0)) → 0 ⇐
z(one(X )) → 0 ⇐
one(0) → s(0) ⇐
one(s(X )) → one(X ) ⇐ },

and consider the goal ⇐ g ≡ ⇐ (g_{1}, g_{2}) ≡ ⇐ (X = s(0), z(X ) = 0). Then there exists the following (ordinary) narrowing derivation:

⇐ (X = s(0), z(X ) = 0) ↪^{{X /one(Y )}} ⇐ (one(Y ) = s(0), 0 = 0) ↪^{{Y /0}}
⇐ (s(0) = s(0), 0 = 0) ↪^{ϵ} ⇐ (true, 0 = 0) ↪^{ϵ} ⇐ true

with computed answer substitution θ = {X /one(0)}. However, since the goal ⇐ g_{1} ≡ ⇐ X = s(0) only computes the substitution {X /s(0)}, the solution θ cannot be obtained from the (syntactic) composition of the computed answers substitutions of ⇐ g_{1} and ⇐ g_{2}. Note that basic conditional narrowing does not compute the answer substitution {X /one(0)} for the goal ⇐ g.

Now we are ready to give a compositional characterization of the operational semantics of equational Horn programs in a style similar to that of [33] for logic programs.

Definition 4.2 (Compositional Conditional Narrowing). We define compositional conditional narrowing as a transition system (State, ⟼) whose transition relation ⟼ ⊆ State × State is the smallest relation which satisfies

(1) \frac{u ∈ Ō(e) ∧ (λ → ρ ⇐ C ) << R ∧ σ = mgu(\{e_{|u}θ = λ\})}{⟨⇐ \{e\}, θ⟩ ⟼ ⟨⇐ \{e[ρ]_{u}\} ∪ C , θσ⟩}

(2) \frac{⟨⇐ g_{1}, θ⟩ ⟼ ⟨⇐ g′_{1}, θθ_{1}⟩ ∧ ⟨⇐ g_{2}, θ⟩⟼ ⟨⇐ g′_{2}, θθ_{2}⟩ ∧ θ_{1} ⇑ θ_{2} ≢ fail}{⟨⇐ (g_{1}, g_{2}), θ⟩ ⟼ ⟨⇐ (g′_{1}, g′_{2}), θ(θ_{1} ⇑ θ_{2})⟩}

Roughly speaking, in the computation model formalized by the transition system above, all equations in the equational goal to be solved are reduced at the same time. Then, the substitutions resulting from these local computations are combined by means of the operator of parallel composition to obtain the global result of the computation.

which might cause the clash of variables in the operational semantics of the parallel subgoals. For solutions to this problem, we refer to [9, 37].

Example 3 Let R be the program of Example 2 and consider the goal ⇐ g ≡ ⇐ (W = one(Y ), z(Y ) = 0). Then there exists the following compositional narrowing derivation: ⟨⇐ (W = one(Y ), z(Y ) = 0), ϵ⟩ ⟼ ⟨⇐ (W = one(X ), 0 = 0), {Y /s(0), X /0}⟩ (using rule 2)

(since ⟨⇐ W = one(Y ), ϵ⟩ ⟼ ⟨⇐ W = one(X ), {Y /s(X )}⟩ (using rule 1) and
⟨⇐ z(Y ) = 0, ϵ⟩ ⟼ ⟨⇐ 0 = 0, {Y /s(0)}⟩ (using rule 1) and
{Y /s(X )} ⇑ {Y /s(0)} = {Y /s(0), X /0} ≢ fail)

⟨⇐ (W = one(X ), 0 = 0), {Y /s(0), X /0}⟩ ⟼ ⟨⇐ W = s(0), {Y /s(0), X /0}⟩ (using rule 2)

(since ⟨⇐ W = one(X ), {Y /s(0), X /0}⟩ ⟼ ⟨⇐ W = s(0), {Y /s(0), X /0}⟩ (using rule 1) and
⟨⇐ 0 = 0, {Y /s(0), X /0}⟩ ⟼ ⟨⇐ true, {Y /s(0), X /0}⟩ (using rule 1))

⟨⇐ W = s(0), {Y /s(0), X /0}⟩ ⟼ ⟨⇐ true, {Y /s(0), X /0, W /s(0)}⟩ (using rule 1) with computed answer substitution θ = {Y /s(0), W /s(0)}.

The computation model formalized in Definition 4.2 could be taken as a basis for an AND-parallel computation model of equational Horn programs. We note that the model has not been devised to achieve maximal parallelism in the sense that not all redexes in a given goal are allowed to perform one narrowing step independently. Namely, redexes which occur in a same equation are not reduced in parallel, while they could. To overcome this lack, it suffices to introduce the following flattening rule, which preserves the reachable solutions

(3) \frac{e ∈ g ∧ u ∈ Ō(e) ∧ x is a new variable}{⟨⇐ g, θ⟩ ⟼ ⟨⇐ (g − \{e\}) ∪ \{e[x]_{u}\} ∪ \{e_{|u} = x\}, θ⟩}

provided that both e_{|u} and e[x]_{u} contain at least one function symbol [32]. Note that we need not determine the level of granularity [27] (as it neither affects correctness nor completeness); this we consider to be an implementation issue that could enable (more) effective parallelizations.

Our approach differs from other AND-parallel execution models, such as e.g. [27], where subexpressions are only narrowed in parallel if they are independent, i.e. if they do not share (unbound) variables. A ‘need-driven’ synchronization model is imposed which compels processes to wait for the value of a parallel subexpression if such a value is needed. In [26], a dependent AND-parallel execution model is exploited, but the imposed synchronization mechanisms produce too much overhead.

A new operational semantics of an equational goal ⇐ g in the CTRS R ∪ {x = x → true ⇐} can now be defined by

Definition 4.3 O′(⇐ g) = {θ_{|V̀ar(g)} | ⟨⇐ g, ϵ⟩ ⟼^{∗} ⟨⇐ true, θ⟩}.

The new success set semantics O′ is compositional w.r.t. the AND operator. Formally,

Theorem 4.4 O′(⇐ g_{1}, g_{2}) = O′(⇐ g_{1}) ⇑ O′(⇐ g_{2}).

The following result states that the compositional conditional semantics and the standard basic conditional semantics coincide. The correspondence is restricted to successes, namely to the substitutions computed by all successfully terminating derivations.

Corollary 4.5 O(⇐ g) = O′(⇐ g).

As a consequence of Corollary 4.5, every solution found by basic conditional narrowing is found by compositional (basic) conditional narrowing as well. Hence, we have the following corollary for level-canonical systems.

Corollary 4.6 (completeness). Let E be a level-canonical equational Horn theory. The set O′(⇐ g) is a complete set of E-unifiers of g.

We note that, by forcing the join of the parallel solutions every time that all equations in the goal have performed a single step independently, the compositional execution model formalized by Definition 4.2 might not couch all the exploitable AND-parallelism. Corollary 4.5 suggests that many different computation schemes are possible. For instance, we can solve in parallel all (sub-)goals, joining the AND-parallel (sub-)goals when the (sub-)goals are completely solved, instead of forcing the syncronization of the ANDparallel branches at every single reduction step. In the following section, we show how this execution scheme can be efficiently exploited for program analysis.

5 Abstract Basic Conditional Narrowing

Abstract interpretation is a theory of semantic approximation which is used to provide statically sound answers to some questions about the run-time behaviour of programs [8]. The ‘concrete’ data and semantic operators are approximated and replaced by corresponding ‘abstract’ data and operators. The ‘answers’ obtained by using the abstract data and operators have to be proven sound by exploiting the correspondence with the concrete data and operators. In this section, we recall the framework of abstract interpretation for analysis of equational unsatisfiability we defined in [2]. Then we extend this framework by defining a compositional abstract semantics which safely approximates the observables.

Our analysis of unsatisfiability is an abstraction of the transition system semantics for basic conditional narrowing we have introduced in Section 4. We first recall the abstract domains and the associated abstract operators together with some previous results concerning them.

5.1 Abstract Domains and Operators

Some of the definitions at the beginning of this section are already in [2] and are reported for completeness. A difference with respect to [2] is that we present Definition 5.8 as parametric with respect to a functional dependency graph (or loop-check). The corresponding definition in [2] is an instance for the specific dependency graph considered there.

A description is the association of an abstract domain (D, ≤) (a poset) with a concrete domain (E, ≤) (a poset). When E = Eqn, E = Sub or E = State, the description is called an equation description, a substitution description or a state description, respectively. The correspondence between the abstract and concrete domain is established through a monotonic ‘concretization’ function γ : D → ℘E [7]. We say that d approximates e, written d ∝ e, iff e ∈ γ(d). The approximation relation can be lifted to relations and cross products as usual [7].

We approximate the behaviour of a CTRS and initial state by an abstract transition system which can be viewed as a finite transition graph with nodes labeled by state descriptions, where transitions are proved by (abstract) narrowing reduction [2]. State descriptions consist of a set of equations with substitution descriptions. The descriptions for equations, substitutions and term rewriting systems are defined as follows. By abuse of notation, we denote in the same way a preorder and the corresponding partial ordering induced on the equivalence classes of the equivalence relation associated with the preorder.

Definition 5.1 (term, equation poset). By T = (τ(Σ ∪ V ), ≤), we denote the standard domain of (equivalence classes of) terms ordered by the standard partial order ≤ induced by the preorder on terms given by the relation of being ‘more general’. Let ⊥ be an irreducible symbol, where ⊥ ∉ Σ. Let T_{A} = (τ(Σ ∪ V ∪ {⊥}), ⪯) be the domain of terms over the signature augmented by ⊥ (abstract terms), where the partial order ⪯ is defined as follows:

(a) ∀t ∈ T_{A}.⊥ ⪯ t and t ⪯ t and

(b) ∀s_{1}, …, s_{n}, s′_{1}, …, s′_{n} ∈ T_{A}, ∀f /n ∈ Σ. s′_{1} ⪯ s_{1} ∧ … ∧ s′_{n} ⪯ s_{n} ⇒ f (s′_{1}, …, s′_{n}) ⪯ f (s_{1}, …, s_{n}) This order can be extended to (abstract) equations: s′ = t′ ⪯ s = t iff s′ ⪯ s and t′ ⪯ t and to (abstract) sets of equations S, S′: S′ ⪯ S iff ∀e′ ∈ S′.∃e ∈ S such that e′ ⪯ e. Note that S′ ⪯ true ⇒ S′ ≡ true.

Roughly speaking, we introduce the special symbol ⊥ in the abstract domains to represent any concrete term. Logically, ⊥ stands for an existentially quantified variable [2, 29, 30]. Define [[S]] = S′, where the n-tuple of occurrences of ⊥ in S is replaced by an n-tuple of existentially quantified fresh variables in S′.

The following proposition shows how the preorder ⪯ defined on the set of abstract equation sets and the implication ordering ≤ defined on Eqn relate.

Proposition 5.2 [2] Let S, S′ be two abstract equation sets s.t. S′ ⪯ S. Then [[S′]] ≤ [[S]], that is, [[S]] ⇒ [[S′]].

Definition 5.3 (abstract substitution). An abstract substitution is a set of the form {x_{1}/t_{1}, …, x_{n}/t_{n}} where, for each i = 1, …, n, x_{i} is a distinct variable in V not occurring in any of the terms t_{1}, …, t_{n} and t_{i} ∈ τ(Σ ∪ V ∪ {⊥}). The preorder on abstract substitutions can be given as logical implication: let θ, κ ∈ Sub_{A}, κ ⪯ θ iff [[θ̂]] ⇒ [[κ̂]].

Let us introduce the abstract domains which we will use in our analysis.

Definition 5.4 (term, equation, substitution, state description). Let T = (τ(Σ∪V ), ≤) and T_{A} = (τ(Σ∪V ∪{⊥}), ⪯). The term description is ⟨T_{A}, γ, T ⟩ where γ : T_{A} → ℘ T is defined by: γ(t′) = {t ∈ T | t′ ⪯ t}.

Let Eqn be the set of finite sets of equations over τ(Σ ∪ V ) and Eqn_{A} be the set of finite sets of equations over τ(Σ ∪ V ∪ {⊥}). The equation description is ⟨(Eqn_{A}, ⪯), γ, (Eqn, ≤)⟩, where γ : Eqn_{A} → ℘ Eqn is defined by: γ(g′) = {g ∈ Eqn | g′ ⪯ g and g is unquantified }.

Let Sub be the set of substitutions over τ(Σ∪V ) and Sub_{A} be the set of substitutions over τ(Σ∪V ∪{⊥}). The substitution description is ⟨(Sub_{A}, ⪯), γ, (Sub, ≤)⟩, where γ : Sub_{A} → ℘ Sub is defined by: γ(κ) = {θ ∈ Sub | κ ⪯ θ}.

Define the abstract state domain State_{A} induced by Eqn_{A} and Sub_{A} to be State_{A} = {⟨⇐ g, κ⟩ | g ∈ Eqn_{A}, κ ∈ Sub_{A}}.

An abstract term rewriting system is a finite set of abstract reduction rules of the form (λ → ρ ⇐ C ), λ ∈ τ(Σ ∪ V ), ρ ∈ τ(Σ ∪ V ∪ {⊥}), λ ∉ V , Var(ρ) ⊆ Var(λ) and C ∈ Eqn_{A}. We let Ctrs_{A} denote the set of abstract term rewriting systems.

In the following, we formalize the idea that abstract narrowing reduction approximates narrowing reduction by replacing concrete states, unification and term rewriting systems with abstract states, abstract unification and abstract term rewriting systems. We define the abstract most general unifier for an equation set E′ ∈ Eqn_{A} as follows. First replace all occurrences of ⊥ in E′ by existentially quantified fresh variables. Then take a solved form of the resulting quantified equation set and finally replace the existentially quantified variables again by ⊥. Formally: let ∃y_{1} … ∃y_{n}.E = solve([[E′]]) and κ = {y_{1}/⊥, …, y_{n}/⊥}. Then mgu_{A}(E′) = sub(Eκ).

Example 4 Let E = {f (X , X ) = f (Y , ⊥), X = a}. Then, mgu_{A}(E) = {X /a, Y /a}.

We now extend the notion of parallel composition from substitutions to abstract substitutions by replacing unification by abstract unification.

Definition 5.5 Let κ_{1}, κ_{2} ∈ Sub_{A}. We define the abstract parallel composition ⇑_{A}: Sub_{A} × Sub_{A} → Sub_{A} by:

κ_{1} ⇑_{A} κ_{2} = mgu_{A}(κ̂_{1} ∪ κ̂_{2}).

It is straightforward to show that abstract parallel composition is idempotent, commutative, associative and has a null element fail and an identical element ϵ. ⇑_{A} can be lifted to sets of abstract substitutions in the obvious way.

Our notion of abstract term rewriting system is parametric with respect to a loop-check, i.e. a finite graph of functional dependencies built from the equational theory, which helps to recognize the narrowing derivations which definitely terminate. The purpose of a loop-check is to reduce the search space to end up with a finite search space.

Definition 5.6 (loop-check). A loop-check is a graph G_{R} associated with a term rewriting system R, i.e. a relation consisting of a set of pairs of terms, such that: (1) The transitive closure G_{R}^{+} is decidable, and (2) There is a function t^{∘} = t′ which assigns to a term t some node t′ in G_{R} such that, if there is an infinite sequence:

⟨⇐ g_{0}, θ_{0}⟩ ⇝ ⟨⇐ g_{1}, θ_{1}⟩ ⇝ … then

∃i ≥ 0. ⟨t_{i}^{∘}, t_{i}^{∘}⟩ ∈ G_{R}^{+}, where t_{i} = e_{|u}θ_{i}, e ∈ g_{i} and u ∈ Ō(e).

(we refer to ⟨t_{i}^{∘}, t_{i}^{∘}⟩ as a ‘cycle’ of G_{R}.)

A loop-check can be thought of as a sort of ‘oracle’ whose usefulness in proving the termination of basic narrowing derivations is stated in the following.

Remark 5.7 Let R be a term rewriting system and G_{R} be a loop-check for R. If there is no cycle in G_{R}, then every basic conditional narrowing derivation for R terminates.

To illustrate our definition, we consider a simple example here.

Example 5 Let R = {X + 0 → X ⇐, X + s(Y ) → s(X + Y ) ⇐} and define t^{∘} = t′ the (partial) function which, given a graph, assigns to a term t some node t′ in the graph such that t′ unifies with t, if there is some such node. Variables are implicitly renamed to be disjoint. Then the graph G = {⟨X + s(Y ), X + s(Y )⟩} is a loop-check for R.

Most papers on loop-checking consider the application of loop-checks at run-time. Static loop-checks have not received that much attention yet. [6, 36] consider a graph of terms which allows the detection of some loops in the search tree which do not lead to any solution. The graphs are built using information about the equations being narrowed as well as the reduction rules being used for narrowing. In the following we show how a loop-check which does not depend on the equation set to be solved can be used to obtain a form of (compiled) abstract program which always terminates and in which the semantics of a given goal can be approximated safely. A CTRS is abstracted by simplifying the right-hand side and the body of each rule. This definition is given inductively on the structure of terms and equations. The main idea is that terms which are mapped to a cycle of the loop-check are drastically simplified by replacing them by ⊥. This enforces termination.

Definition 5.8 (abstract term rewriting system). Let R be a CTRS. Let G_{R} be a loop-check for R. We define the abstraction of R using G_{R} as follows:

R_{A} = {λ → sh(ρ) ⇐ sh(C ) | λ → ρ ⇐ C ∈ R} (we also write R_{A} ∝ R), where the shell sh(x) of an expression x is defined inductively

sh(x) = \{ \begin{matrix}x & if x ∈ V \\ f (sh(t_{1}), …, sh(t_{k})) & if x = f (t_{1}, …, t_{k}) and ⟨x^{∘}, x^{∘}⟩ ∉ G_{R}^{+} \\ sh(l) = sh(r) & if x = (l = r) \\ sh(e_{1}), …, sh(e_{n}) & if x = e_{1}, …, e_{n} \\ ⊥ & otherwise \end{matrix}

Example 6 (Continued from Example 5) The abstraction of R using the loop-check G is: R_{A} = {X + 0 → X ⇐, X + s(Y ) → s(⊥) ⇐}.

In the following definition, we consider sets of CTRSs defined over a fixed signature Σ and we see a CTRS as a finite set of rules. Thus, CTRSs can be ordered by set inclusion. We define the term rewriting system description as follows.

Definition 5.9 Let (Ctrs, ⊇) be the poset of term rewriting systems and (Ctrs_{A}, ⊇) be the poset of abstract term rewriting systems ordered by set inclusion. The abstract term rewriting system description is ⟨(Ctrs_{A}, ⊇), γ, (Ctrs, ⊇)⟩, where γ : Ctrs_{A} → ℘(Ctrs) is defined by:

γ(R_{A}) = {R ∈ Ctrs | (λ → ρ_{A} ⇐ C_{A}) ∈ R_{A} ∧ ρ_{A} = sh(ρ) ∧ C_{A} = sh(C ) ∧ (λ → ρ ⇐ C ) ∈ R}.

We give an example which can help to understand these definitions and motivates the remainder of the section. Let us introduce the auxiliary function ⌊t⌋, which inductively replaces by a fresh variable any term whose outermost symbol is not an irreducible function symbol, i.e.

⌊t⌋ = \{ \begin{matrix}c(⌊t_{1}⌋, …, ⌊t_{k}⌋) & if t = c(t_{1}, …, t_{k}) and c ∈ C \\ y & otherwise, where y is a fresh variable. \end{matrix}

The following definition introduces a particular case of dependency graph I_{R} that is ‘induced’ by a term rewriting system R. Then we show that I_{R} is a loop-check. Another different, less accurate, loop-check can be found in [2].

Definition 5.10 Let R be a CTRS. The following transformation defines a directed graph I_{R} of functional dependencies induced by R. Define \overline{t} = f (⌊t_{1}⌋, …, ⌊t_{n}⌋) if t = f (t_{1}, …, t_{n}). To build I_{R}, the algorithm starts with ⟨R, ∅⟩ and applies the inference rules as long as they add new arrows. The symbol ∪ stands for set union.

(1)  \frac{r = (λ → ρ ⇐ C ) << R}{⟨R, I_{R}⟩ ⟼ ⟨R − \{r\}, I_{R} ∪ \{λ →^{R} \overline{t} | (t = ρ_{|u} ∧ u ∈ Ō(ρ)) or (t = e_{|u} ∧ e ∈ C ∧ u ∈ (Ō(e) − \{Λ\}))\}⟩}

(2) \frac{(λ →^{R} r) ∈ I_{R} ∧ (λ′ →^{R} r′) ∈ I_{R} ∧ r =^{?} λ′}{⟨R, I_{R}⟩ ⟼ ⟨R, I_{R} ∪ \{r →^{u} λ′\}⟩}

Termination of this calculus is ensured since the number of terms occurring in the rules in R is finite. Roughly speaking, in Definition 5.10, for each rule (λ → ρ ⇐ C ) in R and for each term f (t_{1}, …, t_{n}) occurring in ρ or in C , rule (1) adds an arrow λ →^{R} f (⌊t_{1}⌋, …, ⌊t_{n}⌋) to I_{R}. Rule (2) adds an arrow r →^{u} λ′ between the right-hand side r of an arrow λ →^{R} r in I_{R} and the left-hand side λ′ of each arrow λ′ →^{R} r′ with which r unifies. In the following, →^{∗} denotes a path in the graph that may contain arrows →^{R} and arrows →^{u}. Note that I_{R} associates a path with every basic narrowing derivation issued from a given goal and that it does not require the inspection of the equation set to be solved, as opposed to [6].

Also note that I_{R} consists of the graph of top symbols in [2] when \overline{t} (t^{∘}) is defined as the function \overline{t} = f if t = f (t_{1}, …, t_{n}). In general, I_{R} expresses more fine-grained representations of the recursive structure in a program. Our notion of loop-check I_{R} resembles that of the U-graphs [41] of pure logic programming, which differ from the standard predicate dependency graphs in the sense that unification is also taken into account [10]. U-graphs contain a node for each call (each atom) in the program, and also contain two types of arrows: clause arrows and unification arrows. There is a clause arrow from atom H to atom B, if H is the head of a clause and B is a body atom of the same clause. There is an unification arrow from atom B to atom H if B is a body atom which (after renaming) unifies with the head H of another (or the same) clause.

The following proposition shows that the induced dependency graph I_{R} is a loop-check.

Proposition 5.11 Let R be a CTRS and I_{R} be the graph of terms induced by R. Then I_{R} is a loop-check.

Example 7 Let us consider the following level-canonical CTRS R and its abstraction R_{A}.

R = {  R_{A} = {
r1) h(0)  → 0.  r1_{A}) h(0)  → 0.
r2) f (0)  → 0.  r2_{A}) f (0)  → 0.
r3) f (c(X )) → c(f (X )) ⇐ g(X ) = X . r3_{A}) f (c(X )) → c(⊥) ⇐ g(X ) = X .
r4) g(c(X )) → c(X ). }  r4_{A}) g(c(X )) → c(X ). }

We depict in Figure 1 the dependency graph induced by R. There is a cycle f (X ) →^{∗} f (X ) →^{∗} … in the graph.

[figure: h(0); 0; f (c(X )); f (X ); c(X ); g(X ); f (0); g(c(X )); R; u; R; u; R; u; R; R; R]

Figure 1: Graph of functional dependencies

5.2 Abstract Compositional Narrowing

Now we are ready to formalize an abstract compositional operational semantics. We first introduce abstract (basic) narrowing.

In the sequel, for e ∈ Eqn_{A}, we let Ō(e) denote the set of the occurrences u of e s.t. e_{|u} ∉ (V ∪ {⊥}).

Definition 5.12 Let R_{A} be an abstract CTRS. We define abstract (basic) narrowing as a transition system (State_{A}, ⇝_{A}) whose transition relation ⇝_{A} ⊆ State_{A} × State_{A} is defined as the smallest relation satisfying:

\frac{e ∈ g ∧ u ∈ Ō(e) ∧ (λ → ρ ⇐ C ) << R_{A} ∧ σ = mgu_{A}(\{e_{|u} = λ\}) ∧ κ ⇑_{A} σ ≢ fail}{⟨⇐ g, κ⟩ ⇝_{A} ⟨⇐ (g − \{e\}) ∪ \{e[ρ]_{u}\} ∪ C , κ ⇑_{A} σ⟩}

The following definition formalizes the abstract basic narrowing semantics for the success set.

Definition 5.13 (abstract semantics)

Δ_{R_{A}}(⇐ g) = {κ_{|V̀ar(g)} | ⟨⇐ g, ϵ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ⟩}.

The main purpose of introducing abstract basic narrowing here is to suggest a mechanism for the static analysis of the run-time behaviour of programs. We now establish some preliminary results that clarify our interest in abstract basic narrowing reduction. The following theorem can be proven as an immediate consequence of Lemma 6.3 of [2]. It basically states that in the abstract computations no solutions are lost, that is, each concrete computed answer is still ‘represented’ by a more general answer in the abstract semantics.

Theorem 5.14 Let R_{A} ∝ R and g′ ∝ g. Then, for every solution θ ∈ O_{R}(⇐ g) there exists κ ∈ Δ_{R_{A}}(⇐ g′) such that κ ∝ θ.

Abstract narrowing computes, for a given goal and a program, a description of a superset of the computed answers. Therefore, if the superset is empty, then the goal fails w.r.t. the program. Our analysis of unsatisfiability is formalized in the following theorem.

Corollary 5.15 If Δ_{R_{A}}(⇐ g) = Ø, then g is unsatisfiable in R.

The following theorem basically states that abstract narrowing is compositional w.r.t. the AND operator.

Theorem 5.16 Δ_{R_{A}}(⇐ g_{1}, g_{2}) = Δ_{R_{A}}(⇐ g_{1}) ⇑_{A} Δ_{R_{A}}(⇐ g_{2}).

This theorem suggests the following method to extend abstract basic narrowing to a compositional rule.

Definition 5.17 Let R_{A} be an abstract CTRS. We define abstract compositional (basic) narrowing as a transition system (State_{A}, ⟼_{A}) whose transition relation ⟼_{A} ⊆ State_{A} ×State_{A} is defined as the smallest relation satisfying^{2}^{,}^{3}:

(1) \frac{⟨⇐ g_{1}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} κ_{1}⟩ ∧ ⟨⇐ g_{2}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} κ_{2}⟩ ∧ κ′ = (κ_{1} ⇑_{A} κ_{2}) ∧ κ′ ≢ fail}{⟨⇐ (g_{1}, g_{2}), κ⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ′⟩}

(2) \frac{⟨⇐ \{e\}, κ⟩ ⇝_{A} ⟨⇐ g′, κ′⟩}{⟨⇐ \{e\}, κ⟩ ⟼_{A} ⟨⇐ g′, κ′⟩}

(3) select don’t care (3.1) or (3.2):

(3.1) \frac{⟨⇐ g, κ⟩ ⇝_{A} ⟨⇐ g′, κ′⟩}{⟨⇐ g, κ⟩ ⟼_{A} ⟨⇐ g′, κ′⟩}  (3.2) \frac{⟨⇐ g, κ⟩ ⟼_{∥} ⟨⇐ g′, κ′⟩}{⟨⇐ g, κ⟩ ⟼_{A} ⟨⇐ g′, κ′⟩}

Roughly speaking, the calculus in Definition 5.17 basically considers two cases: the equation set g is a singleton or not. In the first case (rule 2), abstract compositional narrowing just proceeds like abstract basic narrowing (⇝_{A}). In the case when g has more than one equations (rule 3), g can be narrowed using abstract basic narrowing, or it can be split two ways, and each of the separate subgoals g_{1} and g_{2} can be solved independently (using the auxiliary arrow ⟼_{∥}, rule 1). The following propositions show the soundness and completeness of the compositional abstract narrower.

Proposition 5.18 (soundness). If ⟨⇐ g, κ⟩ ⟼_{A}^{∗} ⟨⇐ g′, κ′⟩ then ⟨⇐ g, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′, κ′⟩.

Proposition 5.19 (completeness). If ⟨⇐ g, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ′⟩ then ⟨⇐ g, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ′⟩.

Using these results, the compositionality of abstract basic narrowing can be easily lifted to the case of abstract compositional narrowing. The following result expresses this more formally.

Corollary 5.20 Let Δ′_{R_{A}}(⇐ g) = {κ_{|V̀ar(g)} | ⟨⇐ g, ϵ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ⟩}. Then

Δ′_{R_{A}}(⇐ g_{1}, g_{2}) = Δ′_{R_{A}}(⇐ g_{1}) ⇑_{A} Δ′_{R_{A}}(⇐ g_{2}).

As a consequence of Proposition 5.18 and Proposition 5.19, the analysis for a specific goal (the abstract meaning of a goal) can be determined by exploiting the AND-compositionality of the basic narrowing semantics and its abstract version. In Section 6 we will formalize the idea that the compositionality of the abstract semantics w.r.t. the union of E-unification problems, as established in Theorem 5.16 and Corollary 5.20, provides for incrementality when dealing with constraint satisfaction problems in the framework of constraint logic programming, where sets of constraints are incrementally added to a solver.

2For the sake of simplicity, in rules (3.1) and (3.2), g is not singleton and, in rule (1), g_{1} and g_{2} denote non empty equation sets.

3An implementation of rule (3) could always choose rule (3.1), or rule (3.2), or it could select arbitrarily one of them (but not the other) at each step.

6 Incremental Equational Analyzer

In the context of constraint logic programming [19, 23], incremental search consists of proving the solvability of a sequence of constraint problems by transforming the existing solution to each previously solved problem into a solution to the next problem [17].

When dealing with equational constraints [1], the tests of solvability can be extremely redundant. Termination is not even guaranteed. In [2] we propose a lazy resolution procedure [19] which incorporates an analysis of unsatisfiability which allows us to avoid some useless computations. To achieve efficiency, the analyses also need to be incremental, that is, when adding a new equation set c̃ to an already tested set c of constraints, the analysis should not start checking the accumulated constraint c ∪ c̃ from scratch. In this section, we formulate an incremental algorithm for analyzing the unsatisfiability of equation sets within a constraint setting [1]. The kernel of the algorithm is the calculus of abstract compositional (basic) narrowing reduction as formulated in Section 5.

We assume that constraints monotonically grow as long as the computation proceeds, and the question we consider is how to deal efficiently with the test of unsatisfiability for the accumulated constraints as long as new equations are added.

Definition 6.1 (incremental constraint satisfaction problem). Let c_{0}, c_{1}, c̃_{1}, …, c_{n}, c̃_{n} be constraints, where c_{i} = c_{i−1} ∪ c̃_{i}. The incremental constraint satisfaction problem consists of (efficiently) checking the (un)satisfiability of c_{i} by using some information from the computations of c_{0}, …, c_{i−1}, i = 1, …, n.

The idea here is to compute the abstract success set of ⇐ c ∪ c̃ by combining the sets Δ_{R_{A}}(⇐ c) (Δ′_{R_{A}}(⇐ c)) and Δ_{R_{A}}(⇐ c̃) (Δ′_{R_{A}}(⇐ c̃)) which describe the successes of ⇐ c and ⇐ c̃, respectively.

We define an incremental Equational Analyzer (iEA) as follows.

Definition 6.2 An iEA-state is a pair ⟨c, Θ⟩, where c is a set of equations and Θ is a set of abstract substitutions. The empty iEA-state is ⟨Ø, Ø ⟩.

Definition 6.3 (iEA transition relation ⟶^{c̃}_{iEA})

\frac{Θ′ = Θ ⇑_{A} Δ_{R_{A}}(⇐ c̃)}{⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Θ′⟩}

We note that, if the accumulated abstract success set Θ′ = Ø then c ∪ c̃ is unsatisfiable by Corollary 5.15. Our strategy proves the unsatisfiability of c ∪ c̃, or it builds the (non-empty) abstract success set Δ_{R_{A}}(⇐ c ∪ c̃), as stated by:

Theorem 6.4 Let c be a constraint and Θ = Δ_{R_{A}}(⇐ c) ≠ Ø. Then,

1. if a transition ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Θ′⟩ is proven, then Θ′ = Δ_{R_{A}}(⇐ c ∪ c̃);

2. if a transition ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Ø⟩ is proven, then the constraint c ∪ c̃ is unsatisfiable.

We note that the computed abstract answer set Δ_{R_{A}}(⇐ c ∪c̃) can be used to guide the final execution of a ‘full’ narrower which can find the concrete solutions and possibly recognize the unsatisfiability not detected by this lazy procedure, as described in [3].

constraints  CAn ICAn AbNar APCom  Speedup
Z = 0, parity(X) = even  0.52  0.54  0.42  0.00
Y + Z = s^{2}(0)  3.38  1.62  0.62  0.86
Y = X + Z  10.62  5.24  0.44  4.76  2
parity(X) = even  0.42  0.42  0.30  0.00
parity(Y) = even  3.88  2.80  0.32  1.20
X + Y = s^{2}(0)  18.24  3.44  0.44  2.92  5.3
parity(X) = even  0.40  0.40  0.28  0.00
Y = s(0), Z = X + Y  3.78  1.52  0.46  0.66
X + Z = s^{3}(0)  26.36  4.44  fail  5.9
X + Y = s^{4}(0)  0.72  0.72  0.54  0.00
parity(X) = even  3.66  2.10  0.32  1.46
parity(Y) = even  19.48  3.64  0.30  2.62  5.34
parity(X) = parity(Y)  3.62  3.66  2.30  0.00
X + Y = s(Z)  23.18  12.00  0.46  9.52
Z = 0  20.26  1.14  fail  17.8

CAn  Constraint Analyzer
ICAn  Incremental Constraint Analyzer
AbNar  Abstract Narrowing
APCom Abstract Parallel Composition

Table 1: Incremental vs. Non-Incremental constraint analyzer times (secs, using BIM-Prolog, SUN 3/80).

6.1 Performance Results

The concepts presented regarding compositionality can be used in practice to obtain speedups with respect to the original, non-incremental, execution. The analysis above has been implemented in Prolog and tested on several programs with good results. To demonstrate this point empirically, in this section we present actual run-times for a simple benchmark (parity/1).

    X + 0  → X  ⇐
    X + s(Y) → s(X + Y) ⇐
    parity(X) → even  ⇐ X = Y + Y

Table 1 gives execution times for the program running on a prototype sequential implementation and its optimized, incremental, version. We have not tried with the parallel interpreter yet. In order to test the relative performance of incremental and non-incremental analysis, we timed the analysis adding the equations one by one. That is, the analysis was first run for the first equation of each constraint benchmark. Then the next equation was added and the resulting accumulated constraint (re-)analyzed. The total time involved in this process is given in Table 1 by ICAn, for the case of incremental analysis, and by CAn, for the case of restarting the analysis from scratch every time an equation is added. We compare the time performances of the incremental vs. the non-incremental analyzers. The column Speedup (CAn/ICAn) shows the speedup obtained by incremental analysis. Given the current naïve implementation, the speedups are quite encouraging. If the incrementality was exploited, our interpreter was able to achieve up to 95% gain in efficiency. The time in the second column (ICAn) is the result of the sum of the time in the third and fourth columns: AbNar (time of Abstract Narrowing) and APCom (time of Abstract Parallel Composition) plus some extratime for some simplification rules which are only relevant for the implementation.

7 Conclusion and further research

The contribution of this paper is twofold. We have presented a formal compositional semantics for the success set of equational logic programs which is suitable for AND-parallel implementations. We have then shown that this semantics leads to compositional analyses and have given an example of an enhanced analysis of unsatisfiability which is suitable for theories where equations are considered as constraints.

The approach which we have taken is of general interest. In particular it applies to any kind of analysis where we look for properties which are satisfied by all (or some) success paths. For specific analyses, it will be necessary to provide the appropriate abstract domains and approximation of the term rewriting system. A groundness analysis which follows the approach proposed here is defined in [3].

Acknowledgements

We thank Catuscia Palamidessi for her detailed comments on a draft of this paper, and the anonymous referees for many useful suggestions. Part of this work was performed in the context of the CICYT project TIC 92-0793-C02-02. The final version of the paper was produced under partial support from CICYT project TIC 95-0433-C03-03.

References

[1] M. Alpuente, M. Falaschi, and G. Levi. Incremental Constraint Satisfaction for Equational Logic Programming. Theoretical Computer Science, 142(1):27–57, 1995.

[2] M. Alpuente, M. Falaschi, and F. Manzo. Analyses of Unsatisfiability for Equational Logic Programming. Journal of Logic Programming, 22(3):221–252, 1995.

[3] M. Alpuente, M. Falaschi, M.J. Ramis, and G. Vidal. Optimization of Equational Logic Programs Using Abstract Narrowing. Technical Report DSIC-II/1/93, UPV, 1993. Short version in J. Penjam and M. Bruynooghe, editors, Proc. of PLILP’93, volume 714 of Lecture Notes in Computer Science, pages 391-409, Springer-Verlag, Berlin, 1993.

[4] M. Alpuente, M. Falaschi, M.J. Ramis, and G. Vidal. A Compositional Semantics for Conditional Term Rewriting Systems. In H.E. Bal, editor, Proc. Sixth IEEE Int’l Conf. on Computer Languages ICCL’94, pages 171–182. IEEE Computer Society Press, 1994.

[5] M. Alpuente, M. Falaschi, and G. Vidal. Compositional Analysis for Equational Horn Programs. In G. Levi and M. Rodríguez-Artalejo, editors, Proc. of Fifth Int’l Conf. on Algebraic and Logic Programming, ALP’94, volume 850 of Lecture Notes in Computer Science, pages 77–94. Springer-Verlag, Berlin, 1994.

[6] J. Chabin and P. Réty. Narrowing directed by a graph of terms. In G. Goos and J. Hartmanis, editors, Proc. of RTA’91, volume 488 of Lecture Notes in Computer Science, pages 112–123. Springer-Verlag, Berlin, 1991.

[7] M. Codish, M. Falaschi, and K. Marriott. Suspension Analyses for Concurrent Logic Programs. ACM Transactions on Programming Languages and Systems, 16(3):649–686, 1994.

[8] P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238–252, 1977.

[9] F. S. de Boer and C. Palamidessi. On the asynchronous nature of communication in concurrent logic languages: A fully abstract model based on sequences. In J.C.M. Baeten and J.W. Klop, editors, Proc. of Concur 90, volume 458 of Lecture Notes in Computer Science, pages 175–194. Springer-Verlag, Berlin, 1990.

[10] D. de Schreye and S. Decorte. Termination of Logic Programs: the Never Ending Story. Journal of Logic Programming, 19/20:199–260, 1994.

[11] N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243–320. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

[12] N. Dershowitz and N. Lindenstrauss. An Abstract Concurrent Machine for Rewriting. In H. Kirchner and W. Wechler, editors, Proc. Second Int’l Conf. on Algebraic and Logic Programming, volume 463 of Lecture Notes in Computer Science, pages 318–331. Springer-Verlag, Berlin, 1990.

[13] M. Gabbrielli and G. Levi. On the Semantics of Logic Programs. In J. Leach Albert, B. Monien, and M. Rodriguez Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, volume 510 of Lecture Notes in Computer Science, pages 1–19. Springer-Verlag, Berlin, 1991.

[14] J.H. Gallier and S. Raatz. Extending SLD-resolution to equational Horn clauses using E-unification. Journal of Logic Programming, 6:3–43, 1989.

[15] E. Giovannetti and C. Moiso. A completeness result for E-unification algorithms based on Conditional Narrowing. In M. Boscarol, L. Carlucci, and G. Levi, editors, Foundations of Logic and Functional Programming, volume 306 of Lecture Notes in Computer Science, pages 157–167. Springer-Verlag, Berlin, 1986.

[16] M. Hanus. The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming, 19&20:583–628, 1994.

[17] P. Van Hentenryck and T. Le Provost. Incremental Search in Constraint Logic Programming. New Generation Computing, 9:257–275, 1991.

[18] M. Hermenegildo and F. Rossi. Strict and Non-Strict Independent And-Parallelism in Logic Programs: Correctness, Efficiency and Compile-Time Conditions. Journal of Logic Programming, 22(1):1–45, 1995.

[19] M. Höhfeld and G. Smolka. Definite relations over constraint languages. Technical report, IBM Deutschland GmbH, Stuttgart, 1988.

[20] S. Hölldobler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1989.

[21] J.M. Hullot. Canonical Forms and Unification. In 5th Int’l Conf. on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 318–334. Springer-Verlag, Berlin, 1980.

[22] J.-M. Jacquet. Conclog: A Methodological Approach to Concurrent Logic Programming. PhD thesis, University of Namur, Belgium, 1989.

[23] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, pages 111–119. ACM, 1987.

[24] J. Jaffar, J.-L. Lassez, and M.J. Maher. A theory of complete logic programs with equality. Journal of Logic Programming, 3:211–223, 1984.

[25] J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I, pages 1–112. Oxford University Press, 1992.

[26] H. Kuchen and W. Hans. An AND-Parallel Implementation of the Functional Logic Language Babel. In Aachener Informatik-Bericht, volume 12, pages 119–139, RWTH Aachen, 1991.

[27] H. Kuchen, J.J. Moreno-Navarro, and M. Hermenegildo. Independent AND-Parallel Implementation of Narrowing. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP’92, Leuven (Belgium), volume 631 of Lecture Notes in Computer Science, pages 24–38. Springer-Verlag, Berlin, 1992.

[28] J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Los Altos, Ca., 1988.

[29] M. J. Maher. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In Proc. Third IEEE Symp. on Logic In Computer Science, pages 348–357. Computer Science Press, New York, 1988.

[30] M. J. Maher. On parameterized substitutions. Technical Report RC 16042, IBM - T.J. Watson Research Center, Yorktown Heights, NY, 1990.

[31] A. Middeldorp and E. Hamoen. Completeness results for basic narrowing. AAECC, 5:213–253, 1994.

[32] W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295– 317, 1989.

[33] C. Palamidessi. Algebraic properties of idempotent substitutions. In M. S. Paterson, editor, Proc. of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 386–399. Springer-Verlag, Berlin, 1990.

[34] G. Plotkin. A structured approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[35] U.S. Reddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. Second IEEE Int’l Symp. on Logic Programming, pages 138–151. IEEE, 1985.

[36] P. Réty, C. Kirchner, H. Kirchner, and P. Lescanne. NARROWER: A new algorithm for unification and its applications to logic programming. In Proc. of RTA’85, volume 202 of Lecture Notes in Computer Science, pages 141–157. Springer-Verlag, Berlin, 1985.

[37] V. Saraswat, M. Rinard, and P. Panangaden. Semantic Foundation of Concurrent Constraint Programming. In Proc. Eighteenth Annual ACM Symp. on Principles of Programming Languages POPL’91, pages 333–352, 1991.

[38] D. Scott. Domains for Denotational Semantics. In Proc. ICALP’82, volume 140 of Lecture Notes in Computer Science, pages 577–613. Springer-Verlag, Berlin, 1982.

[39] J.H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7:207–274, 1989.

[40] J.E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

[41] B. Wang and R.K. Shyamasundar. Methodology for Proving the Termination of Logic Programs. In Proc. of PLILP’90, volume 456 of Lecture Notes in Computer Science, pages 204–221. Springer-Verlag, Berlin, 1990.

A Appendix

In this appendix we give the proofs of the theorems we previously stated. In doing so, we will also state and prove a number of technical results.

Proof of Proposition 3.3

Proposition 3.3 Let Γ = Γ_{1} ∪ Γ_{2}, Θ_{1} = U_{E}(Γ_{1}) and Θ_{2} = U_{E}(Γ_{2}). Then U_{E}(Γ) = Θ_{1} ⇑_{E} Θ_{2}. Proof.

(⊆) Let ϑ ∈ U_{E}(Γ_{1} ∪ Γ_{2}). Then ϑ ∈ U_{E}(Γ_{1}) = Θ_{1} and ϑ ∈ U_{E}(Γ_{2}) = Θ_{2}. Thus ϑ ∈ ϑ ⇑_{E} ϑ ⊆ Θ_{1} ⇑_{E} Θ_{2}. (⊇) Let θ ∈ Θ_{1} ⇑_{E} Θ_{2}. Then, by Definition 3.2, ∃θ_{1} ∈ Θ_{1}, ∃θ_{2} ∈ Θ_{2} such that θ ∈ U_{E}(θ̂_{1} ∪ θ̂_{2}). Since

θ ∈ U_{E}(θ̂_{1}) ⇒ θ ∈ U_{E}(Γ_{1})

θ ∈ U_{E}(θ̂_{2}) ⇒ θ ∈ U_{E}(Γ_{2})
then θ ∈ U_{E}(Γ_{1} ∪ Γ_{2}).
□

Proof of Theorem 4.1

In order to prove Theorem 4.1 we need some technical lemmata. Lemma A.1 [28, 33] Let ϑ_{1}, ϑ_{2} be idempotent substitutions. Then

ϑ_{1} ⇑ ϑ_{2} = ϑ_{1}mgu(ϑ̂_{2}ϑ_{1}) = ϑ_{2}mgu(ϑ̂_{1}ϑ_{2}). Lemma A.2 Let θ, σ be idempotent substitutions. Then θ ≤ (θ ⇑ σ). Proof. [proof of Lemma A.2] By Lemma A.1, θ ⇑ σ = θmgu(σ̂θ) ≥ θ. □ Lemma A.3 Let θ, σ be idempotent substitutions. If Var(σ) ∩ Dom(θ) = Ø then θ ⇑ σ = θσ. Proof. [proof of Lemma A.3] We have the following equalities.

θ ⇑ σ  = (by Lemma A.1) θmgu(σ̂θ) = (since Var(σ) ∩ Dom(θ) = Ø) θmgu(σ̂) = (since σ is idempotent) θσ.  □

Lemma A.4 Let θ, θ′ be idempotent substitutions. Then θ ≤ θ′ ⇒ eθ′ = eθθ′. Proof. [proof of Lemma A.4] Since θ ≤ θ′ then there exists γ such that θ′ = θγ. Hence eθθ′ = eθθγ = eθγ = eθ′. □

Lemma A.5 Let e be a set of equations and θ be an idempotent substitution. Then mgu(eθ) = mgu(m̂gu(e)θ).

Proof. [proof of Lemma A.5] mgu(eθ) = mgu(e ∧ θ̂)_{|V̀ar(e)} = mgu(m̂gu(e) ∧ m̂gu(θ̂))_{|V̀ar(e)} = mgu(m̂gu(e)θ). □

Lemma A.6 ⟨⇐ (g_{1}, g_{2}), σ⟩ ⇝^{∗} ⟨⇐ g′, σθ⟩ iff

⟨⇐ g_{1}, σ⟩ ⇝^{∗} ⟨⇐ g′_{1}, σθ_{1}⟩ and ⟨⇐ g_{2}, σ⟩ ⇝^{∗} ⟨⇐ g′_{2}, σθ_{2}⟩, θ = θ_{1} ⇑ θ_{2} ≢ fail and g′ = g′_{1} ∪ g′_{2}.

Proof. [proof of Lemma A.6]

(⇒) Let ⟨⇐ (g_{1}, g_{2}), σ⟩ ≡ ⟨⇐ h_{1}, σϑ_{1}⟩ ⇝ … ⇝ ⟨⇐ h_{n}, σϑ_{n}⟩ ⇝ ⟨⇐ g′, σθ⟩, (ϑ_{1} ≡ ϵ). The proof is done by induction on the length n of the derivation.

(n=1) Straightforward.

Let us consider the inductive case. If ⟨⇐ (g_{1}, g_{2}), σ⟩ ≡ ⟨⇐ h_{1}, σϑ_{1}⟩ ⇝ … ⇝ ⟨⇐ h_{n}, σϑ_{n}⟩ ⇝ ⟨⇐ g′, σϑ_{n}δ⟩ ≡ ⟨⇐ g′, σθ⟩, then there exist (λ → ρ ⇐ C ) << R, e ∈ h_{n} and u ∈ Ō(e) such that δ = mgu({λ = e_{|u}σϑ_{n}}) ≢ fail and g′ = (h_{n} − {e}) ∪ {e[ρ]_{u}} ∪ C . By the inductive hypothesis, there exist ⟨⇐ g_{1}, σ⟩ ≡ ⟨⇐ g_{11}, σϑ_{11}⟩ ⇝ … ⇝ ⟨⇐ g_{1m}, σϑ_{1m}⟩ and ⟨⇐ g_{2}, σ⟩ ≡ ⟨⇐ g_{21}, σϑ_{21}⟩ ⇝ … ⇝ ⟨⇐ g_{2k}, σϑ_{2k}⟩, (ϑ_{11} ≡ ϑ_{21} ≡ ϵ), such that ϑ_{n} = ϑ_{1m} ⇑ ϑ_{2k} ≢ fail and h_{n} = g_{1m} ∪ g_{2k}. Since h_{n} = g_{1m} ∪ g_{2k} then e ∈ g_{1m} or e ∈ g_{2k}. Let e ∈ g_{1m} (the case when e ∈ g_{2k} is perfectly analogous). It suffices to show that ⟨⇐ g_{1m}, σϑ_{1m}⟩ ⇝ ⟨⇐ g′_{1}, σθ_{1}⟩ and θ = θ_{1} ⇑ ϑ_{2k} ≢ fail and g′ = g′_{1} ∪ g_{2k}. Since mgu({λ = e_{|u}σ(ϑ_{1m} ⇑ ϑ_{2k})}) = mgu({λ = e_{|u}σϑ_{n}}) = δ ≢ fail, then δ′ = mgu({λ = e_{|u}σϑ_{1m}}) ≢ fail. Therefore ⟨⇐ g_{1m}, σϑ_{1m}⟩ ⇝ ⟨⇐ g′_{1}, σϑ_{1m}δ′⟩ ≡ ⟨⇐ g′_{1}, σθ_{1}⟩, where θ_{1} = ϑ_{1m}δ′ and g′_{1} = (g_{1m} − {e}) ∪ {e[ρ]_{u}} ∪ C . Since θ_{1} = ϑ_{1m}δ′ then

θ_{1} ⇑ ϑ_{2k}  =
(ϑ_{1m}δ′) ⇑ ϑ_{2k}  = (by Lemma A.3, since Var(δ′) ∩ Dom(ϑ_{1m}) = Ø)
ϑ_{1m} ⇑ δ′ ⇑ ϑ_{2k}  = (by commutativity of ⇑)
ϑ_{1m} ⇑ ϑ_{2k} ⇑ δ′  = (since ϑ_{n} = ϑ_{1m} ⇑ ϑ_{2k})
ϑ_{n} ⇑ δ′  = (by Lemma A.1)
ϑ_{n}mgu(δ̂′ϑ_{n})  =
ϑ_{n}mgu(m̂gu({λ = e_{|u}σϑ_{1m}})ϑ_{n})  = (by Lemma A.5)
ϑ_{n}mgu({λ = e_{|u}σϑ_{1m}}ϑ_{n})  =
ϑ_{n}mgu({λ = e_{|u}σϑ_{1m}ϑ_{n}})  = (since ϑ_{n} = ϑ_{1m} ⇑ ϑ_{2k})
ϑ_{n}mgu({λ = e_{|u}σϑ_{1m}(ϑ_{1m} ⇑ ϑ_{2k})}) = (by Lemma A.4)
ϑ_{n}mgu({λ = e_{|u}σ(ϑ_{1m} ⇑ ϑ_{2k})})  =
ϑ_{n}mgu({λ = e_{|u}σϑ_{n}})  =
ϑ_{n}δ  =
θ  ≢ fail

Finally we prove that g′ = g′_{1} ∪ g_{2k}. Since h_{n} = g_{1m} ∪ g_{2k} then g′ = (h_{n} − {e}) ∪ {e[ρ]_{u}} ∪ C = ((g_{1m} ∪ g_{2k}) − {e}) ∪ {e[ρ]_{u}} ∪ C = g′_{1} ∪ g_{2k}.

(⇐) Let ⟨⇐ g_{1}, σ⟩ ≡ ⟨⇐ g_{10}, σϑ_{10}⟩ ⇝ … ⇝ ⟨⇐ g_{1m}, σϑ_{1m}⟩ ⇝ ⟨⇐ g′_{1}, σϑ_{1m}δ⟩ ≡ ⟨⇐ g′_{1}, σθ_{1}⟩ and ⟨⇐ g_{2}, σ⟩ ≡ ⟨⇐ g_{20}, σϑ_{20}⟩ ⇝ … ⇝ ⟨⇐ g_{2k}, σϑ_{2k}⟩ ≡ ⟨⇐ g′_{2}, σθ_{2}⟩, (ϑ_{10} ≡ ϑ_{20} ≡ ϵ), and (m + 1) + k = n, n ≥ 1. The proof is done by induction on the sum n of the lengths of the derivations.

(n=1) Straightforward.

Let us consider the inductive case. Since ⟨⇐ g_{1m}, σϑ_{1m}⟩ ⇝ ⟨⇐ g′_{1}, σϑ_{1m}δ⟩, then there exist (λ → ρ ⇐ C ) << R, e ∈ g_{1m} and u ∈ Ō(e) such that δ = mgu({λ = e_{|u}σϑ_{1m}}) and g′_{1} = (g_{1m} − {e}) ∪ {e[ρ]_{u}} ∪ C . By the inductive hypothesis, there exists a derivation ⟨⇐ (g_{1}, g_{2}), σ⟩ ⇝^{∗} ⟨⇐ (g_{1m}, g′_{2}), σ(ϑ_{1m} ⇑ θ_{2})⟩. Then, it suffices to show that ⟨⇐ (g_{1m}, g′_{2}), σ(ϑ_{1m} ⇑ θ_{2})⟩ ⇝ ⟨⇐ (g′_{1}, g′_{2}), σ(θ_{1} ⇑ θ_{2})⟩. Since

(ϑ_{1m} ⇑ θ_{2})mgu({λ = e_{|u}σ(ϑ_{1m} ⇑ θ_{2})})  = (by Lemma A.2 and Lemma A.4)
(ϑ_{1m} ⇑ θ_{2})mgu({λ = e_{|u}σϑ_{1m}(ϑ_{1m} ⇑ θ_{2})})  = (by Lemma A.5)
(ϑ_{1m} ⇑ θ_{2})mgu(m̂gu({λ = e_{|u}σϑ_{1m}})(ϑ_{1m} ⇑ θ_{2})) = (by Lemma A.1)
ϑ_{1m} ⇑ θ_{2} ⇑ mgu({λ = e_{|u}σϑ_{1m}})  =
ϑ_{1m} ⇑ θ_{2} ⇑ δ  = (by commutativity of ⇑)
ϑ_{1m} ⇑ δ ⇑ θ_{2}  = (by Lemma A.3, since Var(δ) ∩ Dom(ϑ_{1m}) = Ø)
(ϑ_{1m}δ) ⇑ θ_{2}  =
θ_{1} ⇑ θ_{2}  ≢ fail,

then δ = mgu({λ = e_{|u}σ(ϑ_{1m} ⇑ θ_{2})}) ≢ fail, and thus ⟨⇐ (g_{1m}, g′_{2}), σ(ϑ_{1m} ⇑ θ_{2})⟩ ⇝ ⟨⇐ (g′_{1}, g′_{2}), σ(ϑ_{1m} ⇑ θ_{2})δ⟩ ≡ ⟨⇐ (g′_{1}, g′_{2}), σ(θ_{1} ⇑ θ_{2})⟩, which is as desired.

□

We let | D | denote the length of the derivation D. We have the following property.

Lemma A.7 Let g_{1} and g_{2} be non empty equation sets and D ≡ ⟨⇐ (g_{1}, g_{2}), σ⟩ ⇝^{∗} ⟨⇐ true, σθ⟩. Then there exist D_{1} ≡ ⟨⇐ g_{1}, σ⟩ ⇝^{∗} ⟨⇐ true, σθ_{1}⟩ and D_{2} ≡ ⟨⇐ g_{2}, σ⟩ ⇝^{∗} ⟨⇐ true, σθ_{2}⟩, with θ = θ_{1} ⇑ θ_{2} ≢ fail, | D |>| D_{1} | and | D |>| D_{2} |.

Proof. [proof of Lemma A.7] The proof is done along the lines of the proof of Lemma A.6. Routine. □

Now we can prove the desired result.

Theorem 4.1 O(⇐ g_{1}, g_{2}) = O(⇐ g_{1}) ⇑ O(⇐ g_{2}).

Proof. The result is a particular case of Lemma A.6 for σ ≡ ϵ and g′_{1} ≡ g′_{2} ≡ true. □

Proof of Theorem 4.4

To prove Theorem 4.4 we first need the following lemmata. ⋆

separo el lemma en dos porque en esta direccion ⇒ las longitudes no tienen porque coincidir (aunque en la prueba no se considera el caso en que g1^{′} o g2^{′} sean vacios…)

Lemma A.8 If ⟨⇐ (g_{1}, g_{2}), σ⟩ ⟼^{∗} ⟨⇐ g′, σθ⟩ then

⟨⇐ g_{1}, σ⟩ ⟼^{∗} ⟨⇐ g′_{1}, σθ_{1}⟩ and ⟨⇐ g_{2}, σ⟩ ⟼^{∗} ⟨⇐ g′_{2}, σθ_{2}⟩,

where θ = θ_{1} ⇑ θ_{2} ≢ fail and g′ = g′_{1} ∪ g′_{2}.

Proof. Let ⟨⇐ (g_{1}, g_{2}), σ⟩ ≡ ⟨⇐ h_{1}, σϑ_{1}⟩ ⟼ … ⟼ ⟨⇐ h_{n}, σϑ_{n}⟩ ⟼ ⟨⇐ g′, σϑ_{n}δ⟩ ≡ ⟨⇐ g′, σθ⟩, (ϑ_{1} ≡ ϵ), and assume h_{n} = ⋃_{i=1,...,kn}{e_{i}}, k_{n} ≥ 1. The proof is done by induction on the length of the derivation.

Let n = 1 and consider the sets I_{1} = {i | e_{i} ∈ g_{1}} = {i_{1}, …, i_{m}} and I_{2} = {j | e_{j} ∈ g_{2}} = {j_{1}, …, j_{p}}, I_{1} ⊆ {1, …, k}, I_{2} ⊆ {1, …, k}, I_{1} ∩ I_{2} = Ø and I_{1} ∪ I_{2} = {1, …, k}, with k = k_{1}. If ⟨⇐ (g_{1}, g_{2}), σ⟩ ⟼ ⟨⇐ g′, σθ⟩ then, by rules (1) and (2) of Definition 4.2, there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}) and δ_{i} = mgu({λ_{i} = e_{i}_{|ui} σ}) ≢ fail, i ∈ {1, …, k} such that ⟨⇐ {e_{i}}, σ⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, σδ_{i}⟩ ≡ ⟨⇐ c_{i}, σδ_{i}⟩,

g′ = ⋃_{i=1,...,k}c_{i} and θ = δ_{1} ⇑ … ⇑ δ_{k} ≢ fail. Then, ⟨⇐ g_{1}, σ⟩ ⟼ ⟨⇐ ⋃_{i∈I_{1}}c_{i}, σθ_{1}⟩ ≡ ⟨⇐ g′_{1}, σθ_{1}⟩ and

⟨⇐ g_{2}, σ⟩ ⟼ ⟨⇐ ⋃_{i∈I_{2}}c_{i}, σθ_{2}⟩ ≡ ⟨⇐ g′_{2}, σθ_{2}⟩, θ_{1} = δ_{i_{1}} ⇑ … ⇑ δ_{im} , θ_{2} = δ_{j_{1}} ⇑ … ⇑ δ_{jp} , θ_{1} ⇑ θ_{2} = θ and

g′ = g′_{1} ∪ g′_{2}.

Now we consider the inductive case. By the inductive hypothesis, there exist ⟨⇐ g_{1}, σ⟩ ≡ ⟨⇐ g_{11}, σϑ_{11}⟩ ⟼ … ⟼ ⟨⇐ g_{1n}, σϑ_{1n}⟩ and ⟨⇐ g_{2}, σ⟩ ≡ ⟨⇐ g_{21}, σϑ_{21}⟩ ⟼ … ⟼ ⟨⇐ g_{2n}, σϑ_{2n}⟩, (ϑ_{11} ≡ ϑ_{21} ≡ ϵ) such that ϑ_{n} = ϑ_{1n} ⇑ ϑ_{2n} ≢ fail and h_{n} = g_{1n} ∪ g_{2n}. Let I_{1} = {i | e_{i} ∈ g_{1n}} = {i_{1}, …, i_{m}} and I_{2} = {j | e_{j} ∈ g_{2n}} = {j_{1}, …, j_{p}}, I_{1} ⊆ {1, …, k_{n}}, I_{2} ⊆ {1, …, k_{n}}, I_{1} ∩ I_{2} = Ø and I_{1} ∪ I_{2} = {1, …, k_{n}}.

Now it suffices to show that ⟨⇐ g_{1n}, σϑ_{1n}⟩ ⟼ ⟨⇐ g′_{1}, σϑ_{1n}δ′⟩ and ⟨⇐ g_{2n}, σϑ_{2n}⟩ ⟼ ⟨⇐ g′_{2}, σϑ_{2n}δ′′⟩ and ϑ_{n}δ = (ϑ_{1n}δ′) ⇑ (ϑ_{2n}δ′′) and g′ = g′_{1} ∪ g′_{2}.

If ⟨⇐ h_{n}, σϑ_{n}⟩ ⟼ ⟨⇐ g′, σϑ_{n}δ⟩ then there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}) and δ_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{n}}) ≢ fail, i ∈ {1, …, k_{n}} such that ⟨⇐ {e_{i}}, σϑ_{n}⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, σϑ_{n}δ_{i}⟩ ≡

⟨⇐ c_{i}, σϑ_{n}δ_{i}⟩, g′ = ⋃_{i=1,...,kn}c_{i} and δ = δ_{1} ⇑ … ⇑ δ_{kn} ≢ fail.

Since δ_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{n}}) ≢ fail and ϑ_{n} = ϑ_{1n} ⇑ ϑ_{2n} then there exist δ′_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{1n}}) ≢ fail, i ∈ I_{1} and δ′′_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{2n}}) ≢ fail, i ∈ I_{2}. Therefore, by an argument similar to the basic case, ⟨⇐ g_{1n}, σϑ_{1n}⟩ ⟼ ⟨⇐ g′_{1}, σϑ_{1n}δ′⟩ and ⟨⇐ g_{2n}, σϑ_{2n}⟩ ⟼ ⟨⇐ g′_{2}, σϑ_{2n}δ′′⟩, δ′ = δ′_{i_{1}} ⇑ … ⇑ δ′_{im} , δ′′ = δ′′_{j_{1}} ⇑ … ⇑ δ′′_{jp} and g′ = g′_{1} ∪ g′_{2}.

Finally, we prove that (ϑ_{1n}δ′) ⇑ (ϑ_{2n}δ′′) = ϑ_{n}δ.

(ϑ_{1n}δ′) ⇑ (ϑ_{2n}δ′′)  = (by Lemma A.3, since
Var(δ′) ∩ Dom(ϑ_{1n}) = Ø)
ϑ_{1n} ⇑ δ′ ⇑ (ϑ_{2n}δ′′)  = (by Lemma A.3, since
Var(δ′′) ∩ Dom(ϑ_{2n}) = Ø)
ϑ_{1n} ⇑ δ′ ⇑ ϑ_{2n} ⇑ δ′′  = (by commutativity of ⇑)
ϑ_{1n} ⇑ ϑ_{2n} ⇑ δ′ ⇑ δ′′  =
ϑ_{n} ⇑ δ′ ⇑ δ′′  =
ϑ_{n} ⇑ (δ′_{i_{1}} ⇑ … ⇑ δ′_{im} ) ⇑ (δ′′_{j_{1}} ⇑ … ⇑ δ′′_{jp} )  =
(ϑ_{n} ⇑ δ′_{i_{1}}) ⇑ … ⇑ (ϑ_{n} ⇑ δ′_{im} ) ⇑ (ϑ_{n} ⇑ δ′′_{j_{1}}) ⇑ … ⇑ (ϑ_{n} ⇑ δ′′_{jp} ) = (by Lemma A.1)
ϑ_{n}mgu(δ̂′_{i_{1}}ϑ_{n}) ⇑ … ⇑ ϑ_{n}mgu(δ̂′′_{jp} ϑ_{n})  =

ϑ_{n}mgu(m̂gu({e_{i_{1}}_{|ui_{1}} σϑ_{1n}})ϑ_{n}) ⇑ …

… ⇑ ϑ_{n}mgu(m̂gu({e_{jp}_{|ujp} σϑ_{2n}})ϑ_{n})  = (by Lemma A.5)
ϑ_{n}mgu({e_{i_{1}}_{|ui_{1}} σϑ_{1n}}ϑ_{n}) ⇑ … ⇑ ϑ_{n}mgu({e_{jp}_{|ujp} σϑ_{2n}}ϑ_{n}) =
ϑ_{n}mgu({e_{i_{1}}_{|ui_{1}} σϑ_{1n}ϑ_{n}}) ⇑ … ⇑ ϑ_{n}mgu({e_{jp}_{|ujp} σϑ_{2n}ϑ_{n})} = (by Lemmata A.2 and A.4)
ϑ_{n}mgu({e_{i_{1}}_{|ui_{1}} σϑ_{n}}) ⇑ … ⇑ ϑ_{n}mgu({e_{jp}_{|ujp} σϑ_{n})}  =
(ϑ_{n}δ_{i_{1}}) ⇑ … ⇑ (ϑ_{n}δ_{im} ) ⇑ (ϑ_{n}δ_{j_{1}}) ⇑ … ⇑ (ϑ_{n}δ_{jp} )  = (by Lemma A.3, since
Var(δ_{i}) ∩ Dom(ϑ_{n}) = Ø)
(ϑ_{n} ⇑ δ_{i_{1}}) ⇑ … ⇑ (ϑ_{n} ⇑ δ_{im} ) ⇑ (ϑ_{n} ⇑ δ_{j_{1}}) ⇑ … ⇑ (ϑ_{n} ⇑ δ_{jp} ) =
ϑ_{n} ⇑ (δ_{i_{1}} ⇑ … ⇑ δ_{im} ⇑ δ_{j_{1}} ⇑ … ⇑ δ_{jp} )  =
ϑ_{n} ⇑ δ  = (by Lemma A.3, since
Var(δ) ∩ Dom(ϑ_{n}) = Ø)

ϑ_{n}δ, and therefore the thesis follows. □

Lemma A.9 If ⟨⇐ g_{1}, σ⟩ ⟼^{n} ⟨⇐ g′_{1}, σθ_{1}⟩ and ⟨⇐ g_{2}, σ⟩ ⟼^{n} ⟨⇐ g′_{2}, σθ_{2}⟩ then

⟨⇐ (g_{1}, g_{2}), σ⟩ ⟼^{n} ⟨⇐ g′, σθ⟩,

where θ = θ_{1} ⇑ θ_{2} ≢ fail and g′ = g′_{1} ∪ g′_{2}.

Proof. Let ⟨⇐ g_{1}, σ⟩ ≡ ⟨⇐ g_{11}, σϑ_{11}⟩ ⟼ … ⟼ ⟨⇐ g_{1n}, σϑ_{1n}⟩ ⟼ ⟨⇐ g′_{1}, σϑ_{1n}δ′⟩ ≡ ⟨⇐ g′_{1}, σθ_{1}⟩ and ⟨⇐ g_{2}, σ⟩ ≡ ⟨⇐ g_{21}, σϑ_{21}⟩ ⟼ … ⟼ ⟨⇐ g_{2n}, σϑ_{2n}⟩ ⟼ ⟨⇐ g′_{2}, σϑ_{2n}δ′′⟩ ≡ ⟨⇐ g′_{2}, σθ_{2}⟩, (ϑ_{11} ≡ ϑ_{21} ≡ ϵ), such that θ_{1} ⇑ θ_{2} ≢ fail, and assume g_{1n} = ⋃_{i=1,...,qn}{e_{i}}, q_{n} ≥ 1 and g_{2n} = ⋃_{i=1,...,pn}{e_{i}}, p_{n} ≥ 1.

We prove the claim by induction on the length of the derivations.

Let n = 1. It follows trivially by rule (2) of Definition 4.2.

Now we consider the inductive case. By the inductive hypothesis, there exist a derivation ⟨⇐ (g_{1}, g_{2}), σ⟩ ⟼^{n−1} ⟨⇐ (g_{1n}, g_{2n}), σ(ϑ_{1n} ⇑ ϑ_{2n})⟩. Then it suffices to show that ⟨⇐ (g_{1n}, g_{2n}), σ(ϑ_{1n} ⇑ ϑ_{2n})⟩ ⟼ ⟨⇐ (g′_{1}, g′_{2}), σ(θ_{1} ⇑ θ_{2})⟩. If ⟨⇐ g_{1n}, σϑ_{1n}⟩ ⟼ ⟨⇐ g′_{1}, σϑ_{1n}δ′⟩ then there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}), e_{i} ∈ g_{1n} and δ′_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{1n}}) ≢ fail, i ∈ {1, …, q_{n}} such that ⟨⇐ {e_{i}}, σϑ_{1n}⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, σϑ_{1n}δ′_{i}⟩ ≡

⟨⇐ c′_{i}, σϑ_{1n}δ′_{i}⟩, g′_{1} = ⋃_{i=1,...,qn}c′_{i} and δ′ = δ′_{1} ⇑ … ⇑ δ′_{qn} ≢ fail. Analogously, if ⟨⇐ g_{2n}, σϑ_{2n}⟩ ⟼ ⟨⇐

g′_{2}, σϑ_{2n}δ′′⟩ then there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}), e_{i} ∈ g_{2n} and δ′′_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{2n}}) ≢ fail, i ∈ {1, …, p_{n}} such that ⟨⇐ {e_{i}}, σϑ_{2n}⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, σϑ_{2n}δ′′_{i}⟩ ≡ ⟨⇐ c′′_{i}, σϑ_{2n}δ′′_{i}⟩, g′_{2} =

⋃_{i=1,...,pn}c′′_{i} and δ′′ = δ′′_{1} ⇑ … ⇑ δ′′_{pn} ≢ fail.

Assume that g_{1n} ∪ g_{2n} = ⋃_{i=1,...,kn}e_{i}.  Now suppose that, for all i in {1, …, k_{n}},

there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R and u_{i} ∈ Ō(e_{i}) such that δ_{i} = mgu({λ_{i} = e_{i}_{|ui} σϑ_{n}}), δ = δ_{1} ⇑ … ⇑ δ_{kn} . By a similar argument as in the proof of Lemma A.8, ϑ_{n}(δ_{1} ⇑ … ⇑ δ_{kn} ) = (ϑ_{1n}δ′) ⇑ (ϑ_{2n}δ′′) = θ_{1} ⇑ θ_{2} and then we have

⟨⇐ (g_{1n}, g_{2n}), σϑ_{n}⟩ ⟼ ⟨⇐ ( ⋃_{i=1,...,qn}c′_{i}, ⋃_{i=1,...,pn}c′′_{i}), σϑ_{n}(δ_{1} ⇑ … ⇑ δ_{kn} )⟩ ≡ ⟨⇐ (g′_{1}, g′_{2}), σ(θ_{1} ⇑ θ_{2})⟩, which

gives the claim.

□

The following result is now immediate.

Theorem 4.4 O′(⇐ g_{1}, g_{2}) = O′(⇐ g_{1}) ⇑ O′(⇐ g_{2}).

Proof. The result is a particular case of Lemma A.8 for σ ≡ ϵ and g′_{1} ≡ g′_{2} ≡ true and Lemma A.9 for σ ≡ ϵ, g′_{1} ≡ g′_{2} ≡ true and considering as many transitions ⟨⇐ true, θ⟩ ⟼ ⟨⇐ true, θ⟩ as needed to make the length of the (independent) derivations coincide. □

Proof of Corollary 4.5 and Corollary 4.6

The following corollary shows that there is a correspondence between (successful) basic conditional narrowing derivations and compositional conditional narrowing derivations. By this correspondence, we get an indirect proof of the completeness of compositional conditional narrowing.

Corollary 4.5 O(⇐ g) = O′(⇐ g).

Proof.

(⊆) We prove that, for every successful basic narrowing sequence ⟨⇐ g_{0}, σ⟩ ⇝ … ⇝ ⟨⇐ true, σϑ_{m}⟩ such that ϑ_{m} ≢ fail there exists a corresponding successful compositional conditional narrowing sequence ⟨⇐ g_{0}, σ⟩ ⟼ … ⟼ ⟨⇐ true, σθ_{nm} ⟩ such that ϑ_{m} = θ_{nm} . The proof is done by induction on the length m of the former derivation. For the sake of simplicity, we assume that the clause renaming chosen for basic conditional narrowing reduction is the same as in compositional narrowing reduction.

Let m = 1. If ⟨⇐ g_{0}, σ⟩ ⇝ ⟨⇐ true, σϑ_{1}⟩, then the rule (x = x → true ⇐) has been applied, and there exists an equation e such that g_{0} = {e} and ϑ_{1} = mgu({eσ}). By rule (1) of Definition 4.2, ⟨⇐ g_{0}, σ⟩ ≡ ⟨⇐ {e}, σ⟩ ⟼ ⟨⇐ true, σθ⟩, with θ = mgu({eσ}) = ϑ_{1}.

Now we consider the inductive case. If m > 1 then ⟨⇐ g_{0}, σ⟩ ⇝ ⟨⇐ g_{1}, σϑ_{1}⟩ ⇝ … ⇝ ⟨⇐ true, σϑ_{m}⟩, with ϑ_{m} ≢ fail. We consider two cases:

(i) Let g_{0} = {e}. By the inductive hypothesis, there exists ⟨⇐ g_{1}, σϑ_{1}⟩ ⟼ … ⟼ ⟨⇐ true, σθ_{nm} ⟩ such that ϑ_{m} = θ_{nm} . Since ⟨⇐ g_{0}, σ⟩ ⇝ ⟨⇐ g_{1}, σϑ_{1}⟩ and g_{0} = {e}, then by rule (1) of Definition 4.2, ⟨⇐ g_{0}, σ⟩ ⟼ ⟨⇐ g_{1}, σθ_{1}⟩ with θ_{1} = ϑ_{1}.

(ii) Let g_{0} = g′_{0} ∪ g′′_{0}, where g′_{0} and g′′_{0} are non empty equation sets. Then, by Lemma A.7, there exist D_{1} ≡ ⟨⇐ g′_{0}, σ⟩ ⇝ … ⇝ ⟨⇐ true, σϑ′_{i}⟩ and D_{2} ≡ ⟨⇐ g′′_{0}, σ⟩ ⇝ … ⇝ ⟨⇐ true, σϑ′′_{k}⟩ such that ϑ_{m} = ϑ′_{i} ⇑ ϑ′′_{k}, ϑ_{m} ≢ fail, m > | D_{1} | and m > | D_{2} |. By the inductive hypothesis, there exist ⟨⇐ g′_{0}, σ⟩ ⟼ … ⟼ ⟨⇐ true, σθ′_{ni} ⟩ and ⟨⇐ g′′_{0}, σ⟩ ⟼ … ⟼ ⟨⇐ true, σθ′′_{nk} ⟩ such that ϑ′_{i} = θ′_{ni} and ϑ′′_{k} = θ′′_{nk} . Finally, from Lemma A.8 (⇐), there exists the derivation ⟨⇐ g_{0}, σ⟩ ≡ ⟨⇐ (g′_{0}, g′′_{0}), σ⟩ ⟼ … ⟼ ⟨⇐ true, σθ_{nm} ⟩ such that θ_{nm} = θ′_{ni} ⇑ θ′′_{nk} = ϑ′_{i} ⇑ ϑ′′_{k} = ϑ_{m}.

(⊇) We prove the more general assertion that, for every compositional conditional narrowing sequence ⟨⇐ g_{0}, ϵ⟩ ⟼ … ⟼ ⟨⇐ g_{n}, θ_{n}⟩ such that θ_{n} ≢ fail, there exists a corresponding basic conditional narrowing sequence ⟨⇐ g′_{0}, ϵ⟩ ⇝ … ⇝ ⟨⇐ g′_{mn} , ϑ_{mn} ⟩ such that g′_{mn} = g_{n} and ϑ_{mn} = θ_{n}. The proof is done by induction on the length n of the former derivation. We make the same assumption about clauses renaming as above.

Let n = 1 and assume g_{0} = ⋃_{i=1,...,k}{e_{i}}, k ≥ 1. If ⟨⇐ g_{0}, ϵ⟩ ⟼ ⟨⇐ g_{1}, θ_{1}⟩ then, by rules (1) and

(2) of Definition 4.2, there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}) and σ_{i} = mgu({λ_{i} = e_{i}_{|ui} }) ≢

fail, i ∈ {1, …, k} such that ⟨⇐ {e_{i}}, ϵ⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, σ_{i}⟩ ≡ ⟨⇐ c_{i}, σ_{i}⟩ and g_{1} = ⋃_{i=1,...,k}c_{i},

θ_{1} = σ_{1} ⇑ … ⇑ σ_{k}, θ_{1} ≢ fail. Then by the definition of basic conditional narrowing and Lemma A.6

(⇐), ⟨⇐ g_{0}, ϵ⟩ ⇝^{∗} ⟨⇐ g_{m_{1}}, ϑ_{m_{1}}⟩, g_{m_{1}} = ⋃_{i=1,...,k}c_{i} = g_{1} and ϑ_{m_{1}} = σ_{1} ⇑ … ⇑ σ_{k} = θ_{1}.

Let us consider the inductive case. If n > 1 then ⟨⇐ g_{0}, ϵ⟩ ⟼ … ⟼ ⟨⇐ g_{n−1}, θ_{n−1}⟩ ⟼ ⟨⇐ g_{n}, θ_{n}⟩, with θ_{n} ≢ fail, and by the inductive hypothesis, there exists ⟨⇐ g′_{0}, ϵ⟩ ⇝ … ⇝ ⟨⇐ g′_{m_{n−1}}, ϑ_{m_{n−1}}⟩ such that g′_{m_{n−1}} = g_{n−1} and ϑ_{m_{n−1}} = θ_{n−1}. Assume that g_{n−1} = ⋃_{i=1,...,k}{e_{i}}, k ≥ 1. If ⟨⇐ g_{n−1}, θ_{n−1}⟩ ⟼

⟨⇐ g_{n}, θ_{n}⟩ then, by rules (1) and (2) of Definition 4.2, there exist (λ_{i} → ρ_{i} ⇐ C_{i}) << R, u_{i} ∈ Ō(e_{i}) and σ_{i} = mgu({λ_{i} = e_{i}_{|ui} θ_{n−1}}) ≢ fail, i ∈ {1, …, k} such that ⟨⇐ {e_{i}}, θ_{n−1}⟩ ⟼ ⟨⇐ {e_{i}[ρ_{i}]_{ui} } ∪ C_{i}, θ_{n−1}σ_{i}⟩ ≡ ⟨⇐ c_{i}, θ_{n−1}σ_{i}⟩, g_{n} = ⋃_{i=1,...,k}c_{i} and θ_{n} = θ_{n−1}(σ_{1} ⇑ … ⇑ σ_{k}) ≢ fail. Then,

by the definition of basic conditional narrowing, ⟨⇐ {e_{i}}, θ_{n−1}⟩ ⇝ ⟨⇐ c_{i}, θ_{n−1}σ_{i}⟩ and, by Lemma A.6

(⇐), ⟨⇐ g′_{m_{n−1}}, ϑ_{m_{n−1}}⟩ ⇝^{∗} ⟨⇐ g′_{mn} , ϑ_{mn} ⟩, g_{mn} = ⋃_{i=1,...,k}c_{i} = g_{n} and ϑ_{mn} = θ_{n−1}(σ_{1} ⇑ … ⇑ σ_{k}) =

θ_{n}, as desired.

□

Corollary 4.6 (completeness).

Let E be a level-canonical equational Horn theory. The set O′(⇐ g) is a complete set of E-unifiers of g.

Proof. Immediate from Corollary 4.5. □

Proof of Proposition 5.11

Proposition 5.11 Let R be a CTRS and I_{R} be the graph of terms induced by R. Then I_{R} is a loop-check.

Proof. The proof is based on a well-founded complexity measure on goals whose is decreased by narrowing steps. Consider the infinite derivation:

D ≡ ⟨⇐ g_{0}, θ_{0}⟩ ⇝ ⟨⇐ g_{1}, θ_{1}⟩ ⇝ … and assume, by contradiction, that I_{R} has no cycle associated with any of the terms occurring in D. For t ∈ T , let m(t) denote the maximal length of the paths in I_{R} starting from any node t′ in the left-hand side of an arrow →^{R} such that t′ unifies with \overline{t} (variables are implicitly renamed to be disjoint). Let \overline{t} be one of such nodes, with a path which length is m(t). We associate with each ⟨⇐ g_{i}, θ_{i}⟩ in the derivation a set H_{i} = {⟨e, u, n⟩ | e ∈ g_{i}, u ∈ Ō(e), e[u] ∈ F, n = m(e_{|u}θ_{i})}, i ≥ 0. We define the complexity M_{i} of the goal ⟨⇐ g_{i}, θ_{i}⟩ as the finite multiset of natural numbers consisting of the third components of the triples in the set H_{i}. Since I_{R} has no cycle associated with any term occurring in D, these third components are finite for all i ≥ 0.

Let us define a well-founded total ordering <_{mul} over multiset complexities by extending the well-founded ordering < on IN to the set M (IN ) of finite multisets over IN . The set M (IN ) is well-founded under the ordering <_{mul} since IN is well-founded under < [11, 25]. Let M, M′ be multiset complexities. M <_{mul} M′ ↔ ∃X ⊆ M, X′ ⊆ M′ such that M = (M′ − X′) ∪ X and ∀n ∈ X ∃n′ ∈ X′. n < n′.

From the definition of basic conditional narrowing, at each derivation step ⟨⇐ g_{i}, θ_{i}⟩ ⇝ ⟨⇐ g_{i+1}, θ_{i+1}⟩, the selected occurrence either comes from the nonvariable occurrences of the equations in g_{0} or it comes from the right-hand side or from the condition of a rewrite rule used in a previous step. Let e and u denote, respectively, the selected equation and occurrence in g_{i}. By definition of I_{R}, for all i, i ≥ 0, ∀⟨e′, u′, n′⟩ ∈ (H_{i+1} − H_{i}) there exists l →^{R} r ∈ I_{R} such that l=^{?}e_{|u}θ_{i} and r=^{?}\overline{e′_{|u′}}. Since there exists r →^{u} λ′, for each λ′ such that r=^{?}λ′, then m(e_{|u}θ_{i}) = 2+m(e′_{|u′}) and thus ∀⟨e′, u′, n′⟩ ∈ (H_{i+1} −H_{i}). n′ < m(e_{|u}θ_{i}). Hence, by the definition of the ordering <_{mul}, it is immediate that for all i, i ≥ 0, M_{i+1} <_{mul} M_{i}. From the definition of basic conditional narrowing, if there is a k > 0 such that every element in M_{k} is 0 then no more narrowing steps are possible. Thus, by the well-foundness of the multiset ordering <_{mul} over M (IN ), only finite decreasing chains are possible and the narrowing derivation terminates. □

Proof of Theorem 5.14 and Corollary 5.15

Theorem 5.14 can easily be proved as a consequence of the following lemmata.

Lemma A.10 [2] Let g, g′ be (unquantified) finite sets of equations over τ(Σ ∪ V ) and τ(Σ ∪ V ∪ {⊥}), respectively. Let θ ∈ Sub and θ′ ∈ Sub_{A}. If θ′ ∝ θ, and g′ ∝ g, then mgu_{A}(g′ ∪ θ̂′) ∝ mgu(g ∪ θ̂).

Lemma A.11 [2] Let s ≡ ⟨⇐ g, θ⟩, s′ ≡ ⟨⇐ g′, θ′⟩ and s′ ∝ s. Assume that s ⇝ t (by a basic narrowing step), and let u ∈ Ō(e) be the occurrence in e ∈ g selected for this step. If ∄ e′ ∈ g′ such that e′ ∝ e and u ∈ Ō(e′), then s′ ∝ t.

Lemma A.12 Let s′ ∝ s. If there is a (basic) narrowing reduction from s to t, then there is an abstract narrowing reduction from s′ to some t′ such that t′ ∝ t, or s′ ∝ t.

Proof. The proof is similar to the proof of Lemma 6.3 of [2]. Let s ≡ ⟨⇐ g, θ⟩ and s′ ≡ ⟨⇐ g′, κ⟩. Since s′ ∝ s, then g′ ∝ g and κ ∝ θ. Now, since s ⇝ t, then t = ⟨(g ∼ {e}) ∪ {e[ρ]_{u}} ∪ C , θσ⟩, where e ∈ g, u ∈ Ō(e), (λ → ρ ⇐ C ) << R and σ = mgu({(e_{|u})θ = λ}). We consider two cases.

1. Assume that there exists e′ ∈ g′ s.t. e′ ∝ e and u ∈ Ō(e′). Thus it is immediate that (e′_{|u}) ∝ (e_{|u}). By Lemma A.10, there exists mgu_{A}({(e′_{|u}) = λ} ∪ κ̂) ∝ mgu({(e_{|u}) = λ} ∪ θ̂) ⇔ θ ∘ mgu({(e_{|u})θ = λ}) = θσ. Let σ′ = mgu_{A}({(e′_{|u}) = λ}). Then κ ⇑_{A} σ′ = mgu_{A}(κ̂ ∪ σ̂′) = mgu_{A}(κ̂ ∪ m̂gu_{A}({(e′_{|u}) = λ})) = mgu_{A}({(e′_{|u}) = λ} ∪ κ̂) ∝ θσ. Since (κ ⇑_{A} σ′) ∝ θσ and θσ ≢ fail, then (κ ⇑_{A} σ′) ≢ fail. Therefore, by Definition 5.12, s′ ⇝_{A} ⟨⇐ (g′ ∼ {e′}) ∪ {e′[sh(ρ)]_{u}} ∪ sh(C ), κ ⇑_{A} σ′⟩. From Definition 5.8^{4} it is immediate that sh(ρ) ∝ ρ and sh(C ) ∝ C . Hence t′ ∝ t.

2. If there does not exist e′ ∈ g′ such that e′ ∝ e and u ∈ Ō(e′), then the lemma follows immediately from Lemma A.11.

□

Lemma A.13 Let s′_{1} ∝ s_{1}. If there exists a basic narrowing derivation s_{1} ⇝ … ⇝ s_{n}, then there exists an abstract basic narrowing derivation s′_{1} ⇝_{A} … ⇝_{A} s′_{m} such that s′_{m} ∝ s_{n}, m ≤ n.

Proof. We prove the lemma by induction on the length n of the basic narrowing derivation. Let n = 1. The claim follows directly from Lemma A.12. Let us consider the inductive case n > 1. Since s′_{1} ∝ s_{1} and s_{1} ⇝ … ⇝ s_{n−1}, by the inductive hypothesis, there exists an abstract basic narrowing derivation s′_{1} ⇝_{A} … ⇝_{A} s′_{k}, k ≤ n − 1, such that s′_{k} ∝ s_{n−1}. Since s′_{k} ∝ s_{n−1} and s_{n−1} ⇝ s_{n}, then by Lemma A.12, either 1) s′_{k} ⇝_{A} s′_{k+1} and s′_{k+1} ∝ s_{n}, or 2) s′_{k} ∝ s_{n}. First, we consider case 1). In this case, it suffices to take m = k +1 and we have s′_{m} ∝ s_{n}, m ≤ n. Now we consider case 2). In this case, we take m = k, and have s′_{m} ∝ s_{n}, m ≤ n − 1 ≤ n, which proves the claim. □

Now we can prove the desired result.

Theorem 5.14 Let R_{A} ∝ R and g′ ∝ g. Then, for every solution θ ∈ O_{R}(⇐ g), there exists κ ∈ Δ_{R_{A}}(⇐ g′) such that κ ∝ θ.

Proof. The result is a particular case of Lemma A.13 for s_{1} ≡ ⟨⇐ g, ϵ⟩, s_{n} ≡ ⟨⇐ true, θ⟩, s′_{1} ≡ ⟨⇐ g′, ϵ⟩ ∝ s_{1}, and s′_{m} ≡ ⟨⇐ g′_{m}, κ⟩ ∝ s_{n}. Hence, s′_{m} = ⟨⇐ true, κ⟩, since g′_{m} ∝ true implies that g′_{m} ≡ true.

4We assume for the sake of simplicity that the clause renaming chosen for the abstract narrowing reduction is the same as in the (basic) narrowing reduction.

□

Corollary 5.15 If Δ_{R_{A}}(⇐ g) = Ø, then g is unsatisfiable in R.

Proof. Immediate from Theorem 5.14. □

Proof of Theorem 5.16

In order to prove Theorem 5.16 we need the following lemma.

Lemma A.14 ⟨⇐ (g_{1}, g_{2}), κ⟩ ⇝_{A}^{∗} ⟨⇐ g′, κ ⇑_{A} θ⟩ iff

⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{1}, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g_{2}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{2}, κ ⇑_{A} θ_{2}⟩, θ = θ_{1} ⇑_{A} θ_{2} ≢ fail and g′ = g′_{1} ∪ g′_{2}.

Proof. [proof of Lemma A.14]

(⇒) Let ⟨⇐ (g_{1}, g_{2}), κ⟩ ≡ ⟨⇐ h_{1}, κ ⇑_{A} ϑ_{1}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ h_{n}, κ ⇑_{A} ϑ_{n}⟩ ⇝_{A} ⟨⇐ g′, κ ⇑_{A} θ⟩, (ϑ_{1} ≡ ϵ). The proof is done by induction on the length n of the derivation.

(n=1) Straightforward.

Let us consider the inductive case. If ⟨⇐ (g_{1}, g_{2}), κ⟩ ≡ ⟨⇐ h_{1}, κ ⇑_{A} ϑ_{1}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ h_{n}, κ ⇑_{A} ϑ_{n}⟩ ⇝_{A} ⟨⇐ g′, κ ⇑_{A} ϑ_{n} ⇑_{A} δ⟩ ≡ ⟨⇐ g′, κ ⇑_{A} θ⟩, then there exist (λ → ρ ⇐ C ) << R_{A}, e ∈ h_{n} and u ∈ Ō(e) such that δ = mgu({λ = e_{|u}}) ≢ fail and g′ = h_{n} − {e} ∪ {e[ρ]_{u}} ∪ C . By the inductive hypothesis, there exist ⟨⇐ g_{1}, κ⟩ ≡ ⟨⇐ g_{11}, κ ⇑_{A} ϑ_{11}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ g_{1m}, κ ⇑_{A} ϑ_{1m}⟩ and ⟨⇐ g_{2}, κ⟩ ≡ ⟨⇐ g_{21}, κ ⇑_{A} ϑ_{21}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ g_{2p}, κ ⇑_{A} ϑ_{2p}⟩, (ϑ_{11} ≡ ϑ_{21} ≡ ϵ), such that ϑ_{n} = ϑ_{1m} ⇑_{A} ϑ_{2p} ≢ fail and h_{n} = g_{1m} ∪ g_{2p}. Since h_{n} = g_{1m} ∪ g_{2p}, then e ∈ g_{1m} or e ∈ g_{2p}. Let e ∈ g_{1m} (the case when e ∈ g_{2p} is perfectly analogous). It suffices to show that ⟨⇐ g_{1m}, κ ⇑_{A} ϑ_{1m}⟩ ⇝_{A} ⟨⇐ g′_{1}, κ ⇑_{A} θ_{1}⟩ and θ = θ_{1} ⇑_{A} ϑ_{2p} ≢ fail and g′ = g′_{1} ∪ g_{2p}. Since (κ ⇑_{A} ϑ_{n} ⇑_{A} δ) ≢ fail and ϑ_{n} = (ϑ_{1m} ⇑_{A} ϑ_{2p}), then (κ ⇑_{A} ϑ_{1m} ⇑_{A} δ) ≢ fail (by commutativity and associativity of ⇑_{A}). Now, since e ∈ g_{1m}, ⟨⇐ g_{1m}, κ ⇑_{A} ϑ_{1m}⟩ ⇝_{A} ⟨⇐ g′_{1}, κ ⇑_{A} ϑ_{1m} ⇑_{A} δ⟩ ≡ ⟨⇐ g′_{1}, κ ⇑_{A} θ_{1}⟩, where θ_{1} = ϑ_{1m} ⇑_{A} δ and g′_{1} = (g_{1m} − {e}) ∪ {e[ρ]_{u}} ∪ C . Then, θ_{1} ⇑_{A} ϑ_{2p} = (ϑ_{1m} ⇑_{A} δ) ⇑_{A} ϑ_{2p} = ϑ_{1m} ⇑_{A} ϑ_{2p} ⇑_{A} δ = ϑ_{n} ⇑_{A} δ = θ. Finally, we prove that g′ = g′_{1} ∪ g_{2p}. Since h_{n} = g_{1m} ∪ g_{2p} then g′ = (h_{n} − {e}) ∪ {e[ρ]_{u}} ∪ C = ((g_{1m} ∪ g_{2p}) − {e}) ∪ {e[ρ]_{u}} ∪ C = g′_{1} ∪ g_{2p}.

(⇐) Let ⟨⇐ g_{1}, κ⟩ ≡ ⟨⇐ g_{10}, κ ⇑_{A} ϑ_{10}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ g_{1m}, κ ⇑_{A} ϑ_{1m}⟩ ⇝_{A} ⟨⇐ g′_{1}, κ ⇑_{A} ϑ_{1m} ⇑_{A} δ⟩ ≡ ⟨⇐ g′_{1}, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g_{2}, κ⟩ ≡ ⟨⇐ g_{20}, κ ⇑_{A} ϑ_{20}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ g_{2p}, κ ⇑_{A} ϑ_{2p}⟩ ≡ ⟨⇐ g′_{2}, κ ⇑_{A} θ_{2}⟩, (ϑ_{10} ≡ ϑ_{20} ≡ ϵ), and (m + 1) + p = n, n ≥ 1. The proof is done by induction on the sum n of the lengths of the derivations.

(n=1) Straightforward.

Let us consider the inductive case. Since ⟨⇐ g_{1m}, κ ⇑_{A} ϑ_{1m}⟩ ⇝_{A} ⟨⇐ g′_{1}, κ ⇑_{A} ϑ_{1m} ⇑_{A} δ⟩, then there exist (λ → ρ ⇐ C ) << R_{A}, e ∈ g_{1m} and u ∈ Ō(e) such that δ = mgu({λ = e_{|u}}) and g′_{1} = (g_{1m} − {e}) ∪ {e[ρ]_{u}} ∪ C . By the inductive hypothesis, there exists a derivation ⟨⇐ (g_{1}, g_{2}), κ⟩ ⇝_{A}^{∗} ⟨⇐ (g_{1m}, g′_{2}), κ ⇑_{A} (ϑ_{1m} ⇑_{A} θ_{2})⟩. Then, it suffices to show that ⟨⇐ (g_{1m}, g′_{2}), κ ⇑_{A} (ϑ_{1m} ⇑_{A} θ_{2})⟩ ⇝_{A} ⟨⇐ (g′_{1}, g′_{2}), κ ⇑_{A} (θ_{1} ⇑_{A} θ_{2})⟩. Since (κ ⇑_{A} ϑ_{1m} ⇑_{A} δ) ≢ fail, (κ ⇑_{A} ϑ_{1m} ⇑_{A} θ_{2}) ≢ fail, and θ = (θ_{1} ⇑_{A} θ_{2}) = (ϑ_{1m} ⇑_{A} δ ⇑_{A} θ_{2}) ≢ fail, then (κ ⇑_{A} ϑ_{1m} ⇑_{A} θ_{2} ⇑_{A} δ) ≢ fail (by commutativity and associativity of ⇑_{A}), and ⟨⇐ (g_{1m}, g′_{2}), κ ⇑_{A} (ϑ_{1m} ⇑_{A} θ_{2})⟩ ⇝_{A} ⟨⇐ (g′_{1}, g′_{2}), κ ⇑_{A} ϑ_{1m} ⇑_{A} θ_{2} ⇑_{A} δ⟩, where g′_{1} = (g_{1m} − {e}) ∪ {e[ρ]_{u}} ∪ C . Finally, since θ_{1} = ϑ_{1m} ⇑_{A} δ, we have that (ϑ_{1m} ⇑_{A} θ_{2}) ⇑_{A} δ = (ϑ_{1m} ⇑_{A} δ) ⇑_{A} θ_{2} = θ_{1} ⇑_{A} θ_{2}, which proves the claim.

□

Now we can prove the desired result.

Theorem 5.16 Δ_{R_{A}}(⇐ g_{1}, g_{2}) = Δ_{R_{A}}(⇐ g_{1}) ⇑_{A} Δ_{R_{A}}(⇐ g_{2}).

Proof. The result is a particular case of Lemma A.14 for κ ≡ ϵ and g′_{1} ≡ g′_{2} ≡ true. □

Proof of Proposition 5.18 and Proposition 5.19

We proceed with Proposition 5.18 whose proof needs the following intermediate result.

Lemma A.15 If ⟨⇐ g, κ⟩ ⟼_{∥} ⟨⇐ true, κ′⟩ then ⟨⇐ g, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ′⟩.

Proof. [proof of Lemma A.15] If ⟨⇐ g, κ⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} θ⟩, then by rule (1) of Definition 5.17, there exist g_{1} and g_{2} such that g = g_{1} ∪ g_{2} and ⟨⇐ g_{1}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩, ⟨⇐ g_{2}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩ and θ = θ_{1} ⇑_{A} θ_{2} ≢ fail. We prove the claim by induction on the number n of applications of rule (1) which prove these latter derivations.

n = 0. Straightforward. Let n = 1 and assume ⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g_{2}, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩ (the case when ⟼_{∥} occurs in the derivation for g_{2} is perfectly analogous). Since ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ⟩, then by rule (1) of Definition 5.17, there exist g′_{11} and g′_{12} such that g′_{1} = g′_{11} ∪ g′_{12}, ⟨⇐ g′_{11}, κ ⇑_{A} κ_{1}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ_{1}⟩, ⟨⇐ g′_{12}, κ ⇑_{A} κ_{1}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ_{2}⟩ and δ = δ_{1} ⇑_{A} δ_{2} ≢ fail. Then, by Lemma A.14, ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ≡ ⟨⇐ (g′_{11}, g′_{12}), κ ⇑_{A} κ_{1}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and thus ⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩. By Lemma A.14, ⟨⇐ g, κ⟩ ≡ ⟨⇐ (g_{1}, g_{2}), κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} (θ_{1} ⇑_{A} θ_{2})⟩.

Let n > 1. Since ⟨⇐ g_{1}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g_{2}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩, then by rules (1) and (3) of Definition 5.17, either

\{ \begin{matrix}⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ_{1}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and \\ ⟨⇐ g_{2}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{2}, κ ⇑_{A} κ_{2}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{2} ⇑_{A} δ_{2}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{2}⟩, or \end{matrix}
\{ \begin{matrix}⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ_{1}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and \\ ⟨⇐ g_{2}, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩, or \end{matrix}
\{ \begin{matrix}⟨⇐ g_{1}, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and \\ ⟨⇐ g_{2}, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′_{2}, κ ⇑_{A} κ_{2}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{2} ⇑_{A} δ_{2}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{2}⟩ \end{matrix}

and the number of applications of rule (1) which prove the transitions ⟨⇐ g′_{i}, κ ⇑_{A} κ_{i}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{i} ⇑_{A} δ_{i}⟩, i ∈ {1, 2} is less than n. Let us consider only the first case since the other two cases are analogous. Since ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{1} ⇑_{A} δ_{1}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g′_{2}, κ ⇑_{A} κ_{2}⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} κ_{2} ⇑_{A} δ_{2}⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ_{2}⟩, then by the inductive hypothesis, ⟨⇐ g′_{1}, κ ⇑_{A} κ_{1}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g′_{2}, κ ⇑_{A} κ_{2}⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩. Since θ_{1} ⇑_{A} θ_{2} ≢ fail, then by Lemma A.14, ⟨⇐ g, κ⟩ ≡ ⟨⇐ (g_{1}, g_{2}), κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} (θ_{1} ⇑_{A} θ_{2})⟩ ≡ ⟨⇐ true, κ ⇑_{A} θ⟩, and the thesis follows. □

Proposition 5.18 (soundness). If ⟨⇐ g, κ⟩ ⟼_{A}^{∗} ⟨⇐ g′, κ′⟩ then ⟨⇐ g, κ⟩ ⇝_{A}^{∗} ⟨⇐ g′, κ′⟩.

Proof. Immediate from Lemma A.15. □

Now we proceed with the proof of Proposition 5.19.

Proposition 5.19 (completeness). If ⟨⇐ g, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, θ⟩ then ⟨⇐ g, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, θ⟩.

Proof. The proof is done by induction on the length n of the former derivation.

If n = 1 and ⟨⇐ g, κ⟩ ⇝_{A} ⟨⇐ true, κ ⇑_{A} σ⟩ ≡ ⟨⇐ true, θ⟩ then the rule (x = x → true ⇐) has been applied and there exists an equation e such that g = {e} and σ = mgu({e}). Then, by rule (2) of Definition 5.17, ⟨⇐ {e}, κ⟩ ⟼_{A} ⟨⇐ true, κ ⇑_{A} σ⟩.

Now we consider the inductive case. If n > 1 then ⟨⇐ g, κ⟩ ≡ ⟨⇐ g_{0}, κ ⇑_{A} ϑ_{0}⟩ ⇝_{A} ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ g_{n}, κ ⇑_{A} ϑ_{n}⟩ ≡ ⟨⇐ true, θ⟩, (ϑ_{0} ≡ ϵ). There are two cases to consider.

(1) Let g_{0} = {e}. By the inductive hypothesis, there exists ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ ⟼_{A} … ⟼_{A} ⟨⇐ true, θ⟩. Since ⟨⇐ {e}, κ⟩ ⇝_{A} ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ then, by rule (2) of Definition 5.17, ⟨⇐ {e}, κ⟩ ⟼_{A} ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩.

(2) Let g_{0} = g′_{0} ∪ g′′_{0} where g′_{0} and g′′_{0} are non empty equation sets.

We have to prove that ⟨⇐ g, κ⟩ ⟼_{A} … ⟼_{A} ⟨⇐ true, θ⟩. According to rule (3) of Definition 5.17, we need to show that:

(a) ⟨⇐ g, κ⟩ ≡ ⟨⇐ g_{0}, κ ⇑_{A} ϑ_{0}⟩ ⇝_{A} ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ ⟼_{A} … ⟼_{A} ⟨⇐ true, θ⟩, or

(b) ⟨⇐ g, κ⟩ ⟼_{∥} ⟨⇐ true, θ⟩.

(a) Since ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ ⇝_{A} … ⇝_{A} ⟨⇐ true, θ⟩ then, by the inductive hypothesis, there exists ⟨⇐ g_{1}, κ ⇑_{A} ϑ_{1}⟩ ⟼_{A} … ⟼_{A} ⟨⇐ true, θ⟩.

(b) Since ⟨⇐ g, κ⟩ ≡ ⟨⇐ (g′_{0}, g′′_{0}), κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} ϑ_{n}⟩ ≡ ⟨⇐ true, θ⟩, then by Lemma A.14, there exist ⟨⇐ g′_{0}, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩, ⟨⇐ g′′_{0}, κ⟩ ⇝_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩ and ϑ_{n} = θ_{1} ⇑_{A} θ_{2}. Then, by the inductive hypothesis, there exist ⟨⇐ g′_{0}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{1}⟩ and ⟨⇐ g′′_{0}, κ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ ⇑_{A} θ_{2}⟩. Therefore, by rule (1) of Definition 5.17, ⟨⇐ (g′_{0}, g′′_{0}), κ⟩ ⟼_{∥} ⟨⇐ true, κ ⇑_{A} (θ_{1} ⇑_{A} θ_{2})⟩ ≡ ⟨⇐ true, κ ⇑_{A} ϑ_{n}⟩ ≡ ⟨⇐ true, θ⟩, and this completes the proof.

□

The following is an immediate conclusion of previous results.

Corollary 5.20 Let Δ′_{R_{A}}(⇐ g) = {κ_{|V̀ar(g)} | ⟨⇐ g, ϵ⟩ ⟼_{A}^{∗} ⟨⇐ true, κ⟩}. Then

Δ′_{R_{A}}(⇐ g_{1}, g_{2}) = Δ′_{R_{A}}(⇐ g_{1}) ⇑_{A} Δ′_{R_{A}}(⇐ g_{2}).

Proof. Immediate from Theorem 5.16, Proposition 5.18 and Proposition 5.19. □

Proof of Theorem 6.4

Theorem 6.4 Let c be a constraint and Θ = Δ_{R_{A}}(⇐ c) ≠ Ø. Then,

1. if a transition ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Θ′⟩ is proven, then Θ′ = Δ_{R_{A}}(⇐ c ∪ c̃);

2. if a transition ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Ø⟩ is proven, then the constraint c ∪ c̃ is unsatisfiable.

Proof. We prove the two claims separately.

1. From Definition 6.3, ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Θ ⇑_{A} Δ_{R_{A}}(⇐ c̃)⟩ = ⟨c ∪ c̃, Δ_{R_{A}}(⇐ c) ⇑_{A} Δ_{R_{A}}(⇐ c̃)⟩ = ⟨c ∪ c̃, Δ_{R_{A}}(⇐ c ∪ c̃)⟩, by Theorem 5.16.

2. Assume, by contradiction, that the constraint c ∪ c̃ is satisfiable. It suffices to show that the transition ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c∪c̃, Ø⟩ cannot be proven for the hypothesis to be contradicted. By case 1, ⟨c, Θ⟩ ⟶^{c̃}_{iEA} ⟨c ∪ c̃, Δ_{R_{A}}(⇐ c ∪ c̃)⟩. By Corollary 5.15 and the assumption that c ∪ c̃ is satisfiable, Δ_{R_{A}}(⇐ c ∪ c̃) ≢ Ø.

□