The Semantics of Equational Logic Programming as an instance of CLP ^{∗}

María Alpuente ^{‡} Moreno Falaschi ^{§} Maurizio Gabbrielli ^{§}

Giorgio Levi ^{§}

Abstract

We show how functional (i.e. equational) and logic programming can be integrated within the Constraint Logic Programming paradigm. The resulting language CLP(H/E) is specialized in solving equations with respect to a Horn equational theory E. CLP(H/E) inherits all the semantic properties of the CLP scheme, including a new semantics which models answer constraints. The operational semantics of CLP(H/E) is defined by a constraint solver based on conditional narrowing. Several strategies to obtain an incremental constraint solver are considered.

1. Introduction

ALPUENTE ET AL. : THE SEMANTICS OF EQUATIONAL LOGIC PROGRAMMING

In this paper we show how equational and logic programming can be integrated within the constraint logic programming paradigm thus inheriting all the CLP semantic properties. In the last few years several approaches to the integration of logic and equational programming have been developed [4, 9, 16, 22, 24, 29, 32, 7, 45, 46]. One relevant approach [29, 35] defines equational logic programs as logic programs augmented by Horn equational theories. Interpreted function symbols can appear as arguments of relations and existentially quantified variables can occur as arguments of functions. Function definition and evaluation are thus embedded in a logical framework. To properly cope with the equational theory, the conventional SLD-resolution mechanism based on a (syntactical) unification algorithm of logic programs has to be modified. The operational semantics of an equational logic language is based on some special form of equational resolution (such as SLDE resolution [5, 20, 24, 29]), where SLD-resolution is usually kept as the only inference rule but the syntactical unification algorithm is replaced by equational (semantic) unification (E-unification [10, 51, 52]). E-unification means the general unification w.r.t. an equational theory E, which is usually described by a set of equations. The set of E-unifiers of a pair of terms is only semidecidable, so that the process of semantic unification may run forever even if the equational theory is unconditional and canonical. Moreover, there is in general no single most general E-unifier. Infinitely many incomparable mgu’s over E of a pair of terms may exist. Three approaches are relevant to the problem of computing the set of E-unifiers of two terms, namely flat SLD resolution [6, 7, 53, 54], complete sets of transformations [21, 30, 43] and paramodulation [17, 48] or some special form of it, such as superposition [16] or narrowing [6, 8, 23, 31, 32, 38, 47, 50].

∗This work was supported by ESPRIT Basic Research Action P3020 “Integration”, by CICYT under grant TIC 91-0425, and by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo of C.N.R.” under grant n.9100880.PF69

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

§Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy

The Constraint Logic Programming paradigm CLP(X) has been proposed by Jaffar and Lassez [34, 33] in order to integrate a generic computational mechanism based on constraints with the logic programming framework. The benefits of such an integration are several. From a pragmatic point of view, CLP(X) allows to use a specific constraints domain X and a related constraint solver within the declarative paradigm of logic programming. From the theoretical viewpoint, CLP(X) provides a unified view of several extensions to pure logic programming within a framework which preserves the unique semantic properties of logic programs, in particular the existence of equivalent operational, model theoretic and fixpoint semantics [34]. Moreover, since the computation is performed over the particular domain of computation X, CLP(X) programs have an equivalent “algebraic” semantics [34] directly defined on the algebraic structure of X.

In this paper we are concerned with an instance of the CLP scheme specialized in solving equations with respect to a Horn equational theory E [29, 35]. The intended structure is given by the finest partition induced by E on the Herbrand Universe H over a finite one sorted alphabet Σ. = is the only predicate symbol for constraints (equational constraints) and is interpreted as semantic equality over the domain. In the following, we will refer to such a structure as H/E. The advantages of this approach are that, since the language is an instance of the scheme, all the above mentioned fundamental properties are automatically inherited by it. Besides, if an efficient algorithm to solve the constraints is developed it can easily be embedded into a general CLP interpreter and can cooperate with other constraint solvers.

Let us notice that for the language to be formally based on the semantics of the scheme, the structures must be solution compact as defined in [34, 33]. Informally, solution compactness means that every element of the domain can be described by a constraint and that the language of constraints must be precise enough to distinguish any object which does not satisfy a given constraint from those ones which do. Any structure which has no limit elements is trivially solution compact. This includes, in particular, the structure H/E.

A narrowing algorithm or some other E-unification procedure can be considered the kernel of the constraint solver which semidecides the solvability of the constraints in the structure H/E. Solvability has to be tested but the equations do not need to be completely solved at every computation step. This paper first deals with an abstract description of an incremental constraint solver for equational logic programming which relies on a narrowing calculus. Our constraint solver not only checks the solvability but also simplifies the constraints. Then we describe a calculus for a narrowing procedure which is heuristically guided from the discarded substitutions, while looking for solutions to new constraints. Finally we present another calculus which builds incrementally the search tree of a constraint. For the incremental construction of this tree we follow an approach which is similar to [25] and our results rely on the innermost selection narrowing defined in [6]. The main issues are how to achieve incrementality in the computation process and how to use finitely failed derivations as a heuristic for optimizing the algorithms in order to achieve an intelligent narrowing.

We mentioned the fact that defining a new language as an instance of CLP(X) allows to inherit all the semantic properties of the CLP scheme. This is also the case for some new semantics which have recently be proposed with the aim of modeling observational equivalences [18]. These semantics extend the results in [13, 14] to the case of constraint logic programs. The construction is based on a new notion of interpretation (set of constrained atoms), on a natural extension of the standard notion of truth and on the definition of various immediate consequences operators, whose least fixpoints on the lattice of interpretations are models corresponding to various observable properties. Within such a framework, the equivalence between the operational and the declarative semantics can be fully achieved. For example, the least fixpoint of one immediate consequences operator fully characterizes the ability to compute answer constraints. This semantics will be considered in this paper. Its instantiation to the case of the structure H/E is the semantics to be taken as the basis of a correct notion of program equivalence to be preserved by program transformation techniques, such as fold/unfold. Moreover, suitable abstract immediate consequence operators can be used for bottom-up abstract interpretation (i.e. fixpoint computation of the abstract model).

The paper is organized as follows. Section 2. considers the answer constraint semantics for CLP(X). In Section 3. we briefly recall some basic concepts on conditional term rewriting systems and universal unification. In Section 4. we define CLP(H/E) logic programs and an incremental constraint solver as a kernel of an operational semantics for them. Section 5. is devoted to the heuristic narrowing calculus. Section 6. presents the calculus which incrementally builds the search tree of a constraint. We assume the reader to be familiar with logic programming [42], constraint logic programming [18, 34, 33], equations and conditional rewriting systems [37]. A preliminary short paper on CLP(H/E) appeared in [1]. The proofs of the results mentioned in this paper can be found in [2] and [19].

2. An answer constraint semantics for CLP(X)

We will first recall the basic CLP concepts as defined in [34]. The CLP framework is defined using a many-sorted first order language, where SORT = ⋃ SORT_{i} denotes a finite set of sorts. A signature of an n-ary function, predicate or variable symbol f is a sequence of respectively n + 1, n, 1 elements of SORT. By the term sort of f we mean the last element in the signature of the function symbol f. By Σ , Π and V (possibly subscripted) we denote possibly denumerable collections of function symbols, predicate symbols and variables with their signatures and typical elements f, g, …, p, q … and X, Y, … respectively. We assume there is a denumerable number of variable symbols for each sort and that each sort contains at least two symbols. τ(Σ ∪ V) and τ(Σ) denote the set of terms and ground terms (i.e. terms without variables) built on Σ and V. τ(Σ) is usually called the Herbrand Universe (H_{Σ}) over Σ and will be called H when the signature is clear from the context. A (Π, Σ)-atom is an element p(t_{1}, …, t_{n}) where p ∈ Π is n-ary and t_{i} ∈ τ(Σ ∪ V), i = 1, …, n. A (Π, Σ)-constraint is a possibly empty or infinite conjunction of (Π, Σ)-atoms. The empty constraint will be denoted by true. The symbol ˜ will denote a finite sequence of symbols. For a syntactic object O, by var(O) we denote the set of variables occurring in O.

Definition 2.1 (CLP programs) [34] Let Π = Π_{C} ∪ Π_{B} and Π_{C} ∩ Π_{B} = ∅. A (Π, Σ)-program is a set of clauses of the form

H : −c□.  or  H : −c□B_{1}, …, B_{n}.

where c is a finite (Π_{C}, Σ)-constraint, H (the head) and B_{1}, …, B_{n} (the body) are (Π_{B}, Σ)-atoms. A goal is a program clause with no head and with a non-empty body.

Definition 2.2 Let Π = Π_{C} ∪ Π_{B} and Π_{C} ∩ Π_{B} = ∅. A (Π_{B}, Σ)-constrained atom is an object of the form c□p(X̃), where c is a (Π_{C}, Σ)-constraint and p(X̃) is a (Π_{B}, Σ)- atom.

In the CLP(X) framework, X stands for a specific constraint domain on which the computation is performed. The notion of structure gives the semantic interpretation of such a domain and is the key element in the algebraic semantics.

Definition 2.3 [34] Let Π = Π_{C} ∪ Π_{B} and Π_{C} ∩ Π_{B} = ∅. A structure ℜ(Π, Σ) is defined over (sorted) alphabets Π and Σ of predicate and function symbols, where Π contains the equality symbol (which needs no signature). ℜ(Π, Σ) consists of

1. a collection Dℜ of non-empty sets Dℜ_{s}, where s ranges over the sorts in SORT.

2. an assignment to each n-ary function symbol f ∈ Σ of a function Dℜ_{s_{1}} × … × Dℜ_{s_{n}} → Dℜ_{s} where (s_{1}, s_{2}, …, s_{n}, s) is the signature of f,

3. an assignment to each n-ary predicate symbol p ∈ Π_{C}, apart from = (interpreted as identity) of a function Dℜ_{s_{1}} × … × Dℜ_{s_{n}} → {T rue, F alse}, where (s_{1}, s_{2}, …, s_{n}) is the signature of p.

A ℜ(Π, Σ)-valuation for a (Π, Σ)-expression is a mapping θ : V → Dℜ, where V = ⋃_{s∈SORT} V_{s} is the set of all variables, and θ(X_{s}) ∈ Dℜ_{s}, where s is the sort of the variable X_{s}.

(Π, Σ)-programs, (Π_{C}, Σ)-constraints and (Π_{B}, Σ)-constrained atoms will be called programs, constraints and constrained atoms. Moreover ℜ(Π, Σ) will be denoted by ℜ. The notion of ℜ-valuation is extended in the obvious way to terms and constraints. If C is a possibly infinite set of atomic constraints, we write ℜ ⊧ Cθ iff ∀c ∈ C ℜ ⊧ cθ (cθ is ℜ-equivalent to true) holds. If A = p(t_{1}, …, t_{n}) is a (Π_{B}, Σ)-atom and θ is a ℜ-valuation on t_{1}, t_{2}, …, t_{n} then Aθ denotes p(t_{1}θ, …, t_{n}θ).

Definition 2.4 (solvability)[34] A constraint c is ℜ-solvable iff there exists a ℜvaluation θ such that ℜ ⊧ cθ. θ is called an ℜ-solution of c. A constrained atom c□p(X̃) is ℜ-solvable iff c is ℜ-solvable.

The structures considered in CLP are the “solution compact” ones as defined in [34, 33]. Since we are not concerned with negation, we will require the first condition only, namely

• ∀ sort s and ∀d ∈ Dℜ_{s}, there exists a possibly infinite set C of constraints on the variable X such that for each ℜ-solution θ of C, Xθ = d holds [34].

2.1. n-interpretations and n-models

We introduce the new notion of n-model and show its relation with the standard notion of ℜ-model as introduced in [34]. Since the structure ℜ is the intended domain of computation for CLP, interpretations for CLP programs can be based on ℜ. All the following definitions are related to a given ℜ (and therefore to a given (Π, Σ)). Let us first introduce an operator on constrained atoms which returns the set of the “ground” instances.

Definition 2.5 [34] The set of “domain instances” [c□p(X̃)] of a constrained atom c□p(X̃) is defined as

[c□p(X̃)] = {p(X̃)θ | θ is an ℜ-solution of c}.

This definition can be extended to sets of constrained atoms. Let S be a set of constrained atoms. Then [S] = ⋃_{A∈S}[A]

Let us now define a preorder on constrained atoms which represents the relation “being more constrained”. Since we are not concerned with a specific domain of computation, we cannot give a syntactic characterization of the preorder. Hence we give the following definition, in terms of solutions of the constraints.

Definition 2.6 Let A be the set of the constrained atoms for program P. We define the relation ⊑ on A as follows

c_{1}□p(X̃) ⊑ c_{2}□p(X̃) iff [c_{1}□p(X̃)] ⊆ [c_{2}□p(X̃)].

We denote by ≡ the equivalence induced by the preorder ⊑ on the set of constrained atoms, (c_{1} ≡ c_{2} iff c_{1} ⊑ c_{2} and c_{2} ⊑ c_{1}).

Note that in case var(c_{1}) ⊆ var(c_{2}) ⊆ X̃, c_{1}□p(X̃) ⊑ c_{2}□p(X̃) iff c_{1} implies c_{2}. The following definitions introduce the notions of interpretations base, interpretations and models for CLP programs.

Definition 2.7 (n-ℜ-base) Let P be a (Π, Σ)-program and let A be the set of all the ℜ(Π, Σ)-solvable constrained atoms for P. The n-ℜ-base of interpretations B is the quotient set of A w.r.t. the equivalence relation ≡. The ordering induced by ⊑ on B will still be denoted by ⊑. For the sake of simplicity A will represent the equivalence class of the constrained atom A.

Definition 2.8 (n-interpretation) An n-interpretation is any subset of B. The set of all the n-interpretations is denoted by I.

Definition 2.9 (truth) Let I be an interpretation. A constrained atom c□p(X̃) is true in I iff [c□p(X̃)] ⊆ [I]. A clause H ← c□B_{1}, …, B_{n} is true in I iff for each ℜ-valuation θ such that θ is a ℜ-solution of c, {B_{1}θ, …, B_{n}θ} ⊆ [I] implies Hθ ∈ [I].

Definition 2.10 (n-models) An n-model of a CLP program P is any n-interpretation in which all the clauses of P are true.

Let us now show the relation between our concepts and the concepts of ℜ-base, ℜinterpretations and ℜ-models defined in [34]. The ℜ-base B_{ℜ} can be defined in terms of our base as B_{ℜ} = [B]. ℜ-interpretations of [34] are defined as usual as subsets of B_{ℜ} and are a special case of our n-interpretations. Indeed, given the solution compactness of the ℜ structure, every “domain instance” p(d_{1}, …, d_{n}) can be represented by the constrained atom c□p(X_{1}, …, X_{n}) where for each solution θ of the (possibly infinite) constraint c, p(d_{1}, …, d_{n}) = p(X_{1}, …, X_{n})θ. ℜ-models are ℜ-interpretations in which all the clauses of the program are true. It is worth noting that our notion of truth is consistent with the truth defined in [34] on ℜ-interpretations, since it is defined on sets of “domain instances” of the form p(X̃)θ where θ is an ℜ-valuation. Hence also ℜ-models are just a special case of n-models.

A parallel with the logic programming case can clarify the picture. Pure logic programming can be obtained from the general CLP framework by considering the structure H({=} ∪ Π_{B}, Σ) where = is the only predicate symbol for constraints, the only H-domain is the Herbrand universe over a finite one sorted alphabet Σ and = is interpreted as syntactic equality over the domain. In the following we will refer to such a structure as H. The logic programs standard semantics defines models as sets of ground atoms and this is exactly what is obtained by H-models defined according to [34]. The new Herbrand base defined in [13] contains non-ground atoms in the models, where a non-ground atom stands for an implicit definition of the (possibly infinite) set of all its ground instances. This mechanism is generalized in the CLP case by allowing constrained atoms in the n-ℜ-base, each constrained atom c□p(X̃) describing the set of elements p(X̃)θ where θ is any ℜ-solution for the constraint c. In order to abstract from the particular syntactic representation of atoms, in the logic programming case the new Herbrand base is defined modulo variance. Indeed, the H structure has the important property of the existence of a unique (up to variable renaming) canonical form of ({=} ∪ Π_{B}, Σ)-constraints which allows to syntactically identify H-equivalent constraints, namely the solved form of [39]. This property allows to compute on the Herbrand universe in a purely syntactic way using unification theory. In particular the unification algorithm which computes the idempotent mgu can be considered the constraint solver which decides the solvability of constraints and, if possible, returns the unique (up to variable renaming) canonical form.

When considering just the H structure, our definitions boil down to those of the s-semantics [13], since Theorem 2.1 is a straightforward consequence of the results in [39].

Theorem 2.1 Let A_{1} = e_{1}□p(X̃) and A_{2} = e_{2}□p(Ỹ) be two H-constrained atoms. Then if the Herbrand universe is not trivial the following propositions hold

1. [A_{1}] = [A_{2}] = ∅ iff e_{i} is not unifiable, i = 1, 2,

2. [A_{1}] = [A_{2}] ≠ ∅ iff p(X̃)ϑ_{1} ≡_{t} p(X̃)ϑ_{2} where ϑ_{i} is an idempotent mgu of the set of equations e_{i} for i = 1, 2, and ≡_{t} is the variance equivalence.

2.2. Operational semantics

We first show the CLP computational rule as defined in [34]. Then an operational semantics given in terms of transition systems is defined. The next step is the formalization of the success set SS(P, ℜ), which induces an equivalence ≈ on programs, which will be shown to characterize the operational behaviour of programs in terms of answer constraints.

Definition 2.11 ((P, ℜ)-derivation step)[34] Let P be a program. A (P, ℜ)-deriva-tion step of a goal : −(c□A_{1}, …, A_{n}) results in a goal of the form : −(c̃□B̃_{1}, …, B̃_{n}), and is denoted by (c□A_{1}, …, A_{n}) →^{(P,ℜ)} (c̃□B̃_{1}, …, B̃_{n}), if there exist n variants of clauses in P, H_{i} : −c_{i}□B̃_{i}, i = 1, …, n, with no variables in common with G and with each other, such that c̃ = {c, c_{1}, c_{2}, …, c_{n}, A_{1} = H_{1}, …, A_{n} = H_{n}} is ℜ-solvable. A (P, ℜ)-derivation of a goal G is a finite or infinite sequence of goals such that every goal, apart from G, is obtained from the previous one by means of a (P, ℜ)-derivation step. A successful (P, ℜ)-derivation of a goal G is a finite sequence whose last element is a goal of the form (c□.) where c is the answer constraint of the derivation. All other finite (P, ℜ)-derivation are finitely failed. The successful derivation of a goal G yielding the answer constraint c is denoted by G ⟶^{(P,ℜ)_{⋆}} (c□.)

The above derivation step can be specified as a transition relation, following the operational approach to semantics based on transition systems [49]. A structural operational approach to the semantics of CLP is also taken in [26]. We need to specify the set Γ of configurations (states), the transition relation →_{CLP} and the set of terminal configurations.

Definition 2.12 (CLP(X) configurations) Let P be a program and G = ← c□A_{1}, …, A_{n}. be a goal. We define a CLP(X) configuration C as a pair

C = ⟨← s[c] ◇ A_{1}, …, A_{n}⟩

where s[c] denotes a constraint solver state, whose structure is left unspecified as it depends on the specific constraint solver, but which includes at least the constraint c. When the constraint c is clear from the context s[c] will simply be denoted by s.

Definition 2.13 (CLP(X) transition relation →_{CLP}) The rule describing a (P, ℜ)- computation step from a configuration ⟨← s_{i} ◇ A_{1}, …, A_{n}⟩ where s_{i} includes c_{i} is given by

\frac{s_{i} ↪^{c̃} s_{i+1}}{⟨← s_{i}◇A_{1}, …, A_{n}⟩ →_{CLP} ⟨← s_{i+1}◇B̃_{1}, …, B̃_{n}⟩}

if there exist n variants of clauses in P, H_{j} ← c′_{j}□B̃_{j}., j = 1, …, n, with no variables in common with ← c_{i}□A_{1}, …, A_{n}. and with each other and c̃ = {c′_{1}, c′_{2}, …, c′_{n}, A_{1} = H_{1}, …, A_{n} = H_{n}}. The condition s_{i} ↪^{c̃} s_{i+1} means that some constraint solver can make a move verifying the ℜ-solvability of the constraint c_{i} ∪ c̃ and returning the new constraint solver state s_{i+1} which includes (a possibly simplified version of) this constraint, c_{i+1}.

Definition 2.14 (CLP(X) initial configuration (C_{0})) Let G_{0} =← c_{0}□B̃. be a goal and s_{0} be the “empty” CLP constraint solver state. If c_{0} is not an empty constraint and s_{0} ↪^{c_{0}} s then C_{0} = ⟨← s ◇ B̃⟩ is the CLP(X) initial configuration. If c_{0} is empty then C_{0} = ⟨← s_{0} ◇ B̃⟩.

Definition 2.15 (CLP(X) terminal configurations (C)) A terminal configuration C has the form C = ⟨← s[c] ◇ ⟩, where c represents the answer constraint.

Let us notice that when the constraint solver is designed for simply testing the ℜ(Π, Σ)-Solvability of the constraint c_{i} ∪ c̃ , the above defined transition relation becomes the standard (P, ℜ)-derivation step as defined in [34]:

\frac{ℜ(Π, Σ) ⊧ (˜∃)(c_{i} ∪ c̃)}{⟨← c_{i}□A_{1}, …, A_{n}.⟩ →_{CLP} ⟨← c_{i} ∪ c̃ □B̃_{1}, …, B̃_{n}.⟩}

In this case, the concepts of (P,ℜ)-derivation and successful and finitely failed (P,ℜ)- derivations can be defined in the usual way [34]. The constraint in the last goal of a successful derivation is the answer constraint of the derivation.

Definition 2.16 Let P be a program. The success set SS(P, ℜ) is defined as follows

SS(P, ℜ) = {c□p(X̃) | c□p(X̃) ∈ B, (true□p(X̃)) ⟶^{(P,ℜ)} (c□.) }.

Let us show an example of the semantics SS(P, R) for a CLP (R) program (CLP (R) is defined on an arithmetical domain R of reals numbers [12]).

Example 2.1 [12] The following program P computes the mortgage repayments. P is the principal, T is the mortgage lifetime in months, I is the annual percentage interest rate, R is the monthly repayment and B is the outstanding balance.

P = { mortgage(P, T, I, R, B) : − T = 1, B + R = P ∗ (1 + I/1200).
mortgage(P, T, I, R, B) : − T > 1□

mortgage(P ∗ (1 + I/1200) − R, T − 1, I, R, B). } Program P can be queried in several different way. For example the goal true□ mortgage(100000,360,12,R,0) computes the answer constraint R = 1028.61 while the goal true □ mortgage(P,120,12,R,B) has answer constraint P = 0.303 ∗ B + 69.7 ∗ R.

The SS(P, R) semantics of program P in the example 2.1 is the following set, where m stands for mortgage(P, T, I, R, B)

{ T = 1, B + R = P ∗ (1 + I/1200)□m,
T = 2, B + R = P ∗ (1 + I/1200)2 − R ∗ (1 + I/1200)□m,
T = 3, B + R = P ∗ (1 + I/1200)3 − R ∗ (1 + I/1200)2+
−R ∗ (1 + I/1200)□m,
⋮
}.

Let us now show the soundness and completeness results for SS(P, ℜ). As resulting from the following Theorem 2.2 SS(P, ℜ) can fully characterize the operational behaviour of programs. The proof of the theorem is based on the observation that if a goal G = c_{0}□p_{1}(t̃_{1}), …, p_{n}(t̃_{n}) has a successful derivation with answer constraint c_{ans}, then defining \overline{c} = c_{0} ∪ (⋃_{i=1,...,n} X̃_{i} = t̃_{i}, c_{i}) where the c_{i} are the answer constraints of the goals c_{0}□p_{i}(X̃_{i}), \overline{c} is equivalent (up to variables in G) to c_{ans} (and analogously for the converse).

Theorem 2.2 Let P be a CLP program and G = (c_{0}□A_{1}, …, A_{n}) any goal. Then G →^{(P,ℜ)} (c_{ans}□.) iff there exists n constrained atoms (c_{i}□B_{i}) ∈ SS(P, ℜ), i = 1, … n, which share no variables with G and with each other, such that c_{0} ∪c_{1} ∪…∪c_{n} ∪A_{1} = B_{1} ∪ … ∪ A_{n} = B_{n} and c_{ans} have the same solutions for the variables in G.

2.3. Fixpoint semantics

Let us now introduce an immediate consequence operator, which allows to characterize the SS(P, ℜ) operational semantics.

Definition 2.17 Let P be a CLP program and let J ⊆ B.

T_{(P,ℜ)}(J) = { c□p(X̃) ∈ B |
∃ a renamed clause p(t̃) : −c_{0}□p_{1}(t̃_{1}), …, p_{n}(t̃_{n}) in P
∃ c_{i}□p_{i}(X̃_{i}) ∈ J, 1 ≤ i ≤ n which share no variables
c′ = c_{0} ∪ {X̃_{i} = t̃_{1}, …, X̃_{n} = t̃_{n}} ∪ {c_{1}, …, c_{n}}
c′ is ℜ-solvable, finite and c = c′ ∪ {X̃ = t̃}  }.

Note that previous operator is defined in terms of the CLP derivation rule. Indeed T_{(P,ℜ)}(J) can be seen as the result of the unfolding of program P wrt the set of unit clauses extracted from J (see later). This is the key property which allows to model answer constraints by means of a bottom-up fixpoint semantics. Moreover, note that the standard immediate consequence operator defined in [34] can be obtained by considering the “domain instances” [T_{(P,ℜ)}(J)] of the defined operator.

Theorem 2.3 The mapping T_{(P,ℜ)} is continuous on the cpo (I_{P} , ⊆). There exists a least fixpoint lfp(T_{(P,ℜ)}) of T_{(P,ℜ)} which is T_{(P,ℜ)} ↑ ω.

Definition 2.18 Let P be a program. Then the fixpoint semantics F ix(P, ℜ) of P is defined as F ix(P, ℜ) = T_{(P,ℜ)} ↑ ω.

2.4. Unfolding semantics and equivalence results

The equivalence between the operational and the fixpoint semantics can be proved in a concise and elegant way by introducing the intermediate notion of unfolding semantics Unf(P, ℜ) [40, 41]. Unf(P, ℜ) is obtained as the limit of the unfolding process. The proof of the equivalence between Unf(P, ℜ) and SS(P, ℜ) is straightforward since these semantics are based on the same inference rule (applied to clauses and goals respectively). On the other side, the equivalence between Unf(P, ℜ) and F ix(P, ℜ) can be based on the strict relation existing between T_{(P,ℜ)}(I) and the unfolding rule (see below).

Definition 2.19 Let P and Q be CLP programs. Then the unfolding of P w.r.t. Q is defined as unf_{P} (Q) = {(A : −c_{0}, c_{1}, …, c_{n}□L̃_{1}, …, L̃_{n}) | ∃ A : −c_{0}□p_{1}(t̃_{1}), …, p_{n}(t̃_{n}) ∈ P ∃ p_{i}(m̃_{i}) : −c′_{i}□L̃_{i} ∈ Q for i = 1, …, n c_{0}, c_{1}, …, c_{n} is ℜ-solvable where c_{i} = c′_{i} ∪ t̃_{i} = m̃_{i} }

The following definition allows to extract from a CLP program P an n-interpretation and vice versa.

Definition 2.20 Let P be an CLP program and I be an n-interpretation. Then we define

α(P) = {c ∪ X̃ = t̃□p(X̃) ∈ B | p(t̃) : −c□. ∈ P }

and

γ(I) = {p(t̃) : −c□. | c ∪ X̃ = t̃□p(X̃) = μ(c_{a}) and c_{a} ∈ I}.

where μ(c_{a}) returns one element of the the equivalence class c_{a}.

Definition 2.21 Let P be an CLP program. Then we define the collection of programs

\begin{matrix}P_{1} = P \\ P_{i} = unf_{P_{i−1}}(P) \end{matrix}

The unfolding semantics Unf(P, ℜ) of the program P is defined as

Unf(P, ℜ) = ⋃_{i=1,2,...} α(P_{i}).

The following theorem states the equality of the unfolding and the operational semantics. Its proof is easy since both the semantics are top-down.

Theorem 2.4 Let P be an Ω-open program. Then Unf(P, ℜ) = SS(P, ℜ).

Note that T_{(P,ℜ)}(I) = α(unf_{P} (γ(I))) holds. This relation allows to prove the following theorem.

Theorem 2.5 Let P be a program. Then F ix(P, ℜ) = Unf(P, ℜ).

Corollary 2.1 (equivalence of the operational and the fixpoint semantics) Let P be a program. Then SS(P, ℜ) = F ix(P, ℜ).

2.5. The model-theoretic semantics

In this section we discuss the models introduced by the fixpoint and the operational semantics. Since we are concerned with the algebraic semantics, i.e. the semantics on the particular structure ℜ considered as domain of computation, we will consider the notion ⊧_{ℜ} of logical consequence in ℜ-models as opposed to the standard notion of logical consequence ⊧.

Definition 2.22 Let P be a program and G be a constrained atom. P ⊧_{ℜ} G iff G is true in every ℜ-model of P, i.e. according to definition 2.9, if ∀M ℜ-model of P,

[G] ⊆ M.

An ℜ-interpretation I, can be regarded as a particular n-interpretation I_{n}. Indeed, since the structure ℜ is solution compact, we can represent each “domain instance” p(d̃) by a constrained atom c□p(X̃) such that the solutions of the (possibly infinite) constraint c define the elements d̃. Formally we can give the following definition.

Definition 2.23 Let I be an ℜ-interpretation. Then we define the corresponding n-interpretation η(I) as follows

η(I) = {c□p(X̃) ∈ B | ∃ p(d̃) ∈ I ∧ ∀ θ solution of c, p(X̃)θ = p(d̃)}.

The following theorem shows that η(I) and I are equivalent from the model theoretic point of view.

Theorem 2.6 Let I be an ℜ-interpretation and c a clause. Then c is true in I iff c is true in η(I).

In general, since we have one concept of truth only (definition 2.9, being true in every ℜ-model is equivalent to being true in every n-model, i.e. from the model theoretic point of view, n-models and ℜ-models are equivalent. Note that the intersection of a set of n-models is not always an n-model. For example, consider the program P = {p(X) : −X = a□} on the Herbrand domain. Clearly both M_{1} = {X = a□p(X)} and M_{2} = {X = Y □p(X)} are n-model of P, but M ∩ M_{2} = ∅ is not an n-model of P. Therefore in general there exists no minimal n-model with respect to set inclusion. We will then introduce an ordering < and a lattice structure on n-interpretations which allow to restore the model intersection property. The model theoretic semantics of a program P is then defined as the greatest lower bound of the set of all n-models of P. Theorem 2.9 shows that this model theoretic semantics definition is the same of the usual one given in [34] in terms of ℜ-models.

Definition 2.24 (ordering on n-interpretations) We define a relation < on I as follows. Let I_{1}, I_{2} ∈ I Then I_{1} ≤ I_{2} iff ∀A_{1} ∈ I_{1}∃A_{2} ∈ I_{2} such that A_{1} ⊑ A_{2} and I_{1} < I_{2} iff (I_{1} ≤ I_{2}) and (I_{2} ≤ I_{1} implies I_{1} ⊆ I_{2}).

The intuitive meaning of the above defined relations is the following. I_{1} ≤ I_{2} means that every contrained atom verified by I_{1} is also verified by I_{2} (I_{2} contains more positive information). I_{1} < I_{2} means that either I_{2} strictly contains more positive information than I_{1} or (if the amount of positive information is the same), that I_{1} expresses it by less elements than I_{2} (I_{2} is more redundant).

Definition 2.25 Let P be a program. Its model theoretic semantics M_{P} is defined as M_{P} = glb{N | N is a n-model of P }.

The previous definitions extend to the CLP case results given in [14] for logic programs. In the particular case of ℜ-interpretations the < ordering is set-inclusion, and the following theorem shows that there exists the minimal R-model w.r.t. set inclusion.

Theorem 2.7 [34] Let P be a CLP and let M be the set of all the ℜ-models of P. Then M_{ℜ} = ⋂_{m∈M} m is the least ℜ-model of P w.r.t. set inclusion.

M_{ℜ} can be considered as the CLP counterpart of the standard least Herbrand model for logic programs. The following theorems show that indeed the M_{ℜ} minimal model is the “same” (up to the η transformation) of the least n-model defined according to the < ordering on n-interpretations. The proofs are based on the observation that [M] = [η([M])], on the monotonicity of η and on the definition of the ordering <.

Theorem 2.8 Let M be an n-model of a program P. Then η([M]) is an R-model of P and η([M]) < M.

Theorem 2.9 Given a program P let M_{ℜ} be its least ℜ-model. Then η(M_{ℜ}) = M_{P}.

Analogously to the logic programming case, the least model characterizes the set of the “ground” ℜ-logical consequences of the program and is equal to the “ground” fixpoint and operational semantics defined in [33]. The answer constraint semantics is also an n-model, as shown by the following theorem. Note that SS(P, ℜ) is not a minimal model.

Lemma 2.2 Let P be a program. Then SS(P, ℜ) is an n-model of P and if c□p(X̃) ∈ SS(P, ℜ) then c□p(X̃) ≡ c′□p(X̃) where c′ is finite.

Finally let us mention that, as shown in [34], it is possible to have a complete correspondence between the algebraic and logical semantics, by considering a theory ℑ which corresponds to ℜ, in the sense that

(i) ℜ ⊧ ℑ, i.e. ℜ models ℑ (ii) ℜ ⊧ ∃C implies ℑ ⊧ ∃C for all constraints C. Therefore considering the algebraic semantics only is not a restriction. Indeed our approach can be adapted to the logical semantics as well, following the previously mentioned correspondence.

3. Basic definitions on equations and term rewriting systems

Let us briefly recall some basic notions and results about equations, conditional rewrite systems and universal unification. Full definitions can be found in [37, 51].

Definition 3.1 A Σ-equation s=t is a pair of terms s and t of the same sort (s, t ∈ τ(Σ ∪ V)). A Horn equational Σ-theory E consists of a finite set of equational Horn clauses of the form l = r ← e_{1}, e_{2}, ..., e_{n}, n ≥ 0, where the Σ-equation l = r in the head is implicitely oriented from left to right and the literals e_{i} in the body are ordinary non-oriented Σ-equations. Σ-equations and Σ-theories will often be called equations and theories, respectively.

A Horn equational theory E can be viewed as a term rewriting system R where the rules are the heads and the conditions are the respective bodies. If all clauses in E have an empty body then E and R are said to be unconditional, otherwise they are said to be conditional. An equational theory E has no extra-variables if every variable occurring in the body or in the right-hand side of the head of a clause in E also occurs in the left-hand side of the head. The equational theory E is said to be canonical if the binary one-step rewriting relation →_{R} defined by R is noetherian and confluent. For syntactical characterizations of confluent conditional theories refer to [45]. Each Horn equational theory E generates a smallest congruence relation =_{E} called E-equality on the set of terms τ(Σ ∪ V). We will denote by H/E the finest partition τ(Σ)/ =_{E} induced by E over the set of ground terms τ(Σ).

Definition 3.2 Given two terms s and t, we say that they are E-unifiable (or Eequal) iff there exists a substitution σ such that sσ and tσ are in the congruence =_{E}, i.e. such that sσ =_{E} tσ or, equivalently^{1}, E ⊧ sσ = tσ. The substitution σ is called an E-unifier of s and t.

Roughly speaking S is a complete set of unifiers for e if any other unifier can be obtained by instance from some element of S (see [51] for a formal definition). Complete sets of minimal E-unifiers do not always exists [51]. E-unification can be viewed as the process of solving an equation within the theory E. Since E-unification is only semidecidable, an E-unification algorithm can be viewed as a semidecision procedure for testing the solvability of equational constraints over the quotient H/E. Each instance of an E-unifier represents a solution over this structure (an H/E-solution).

A E-unification procedure is complete if it generates a complete set of E-unifiers for all input equations. A number of E-unification procedures have been developed in order to deal with conditional equational theories [9, 16, 22, 30, 32, 37]. For instance, conditional narrowing has been shown to be complete for conditional theories satisfying different restrictions [9, 29, 37].

Definition 3.3 Let E be a Horn equational theory. A function symbol f ∈ Σ is called irreducible iff there is no clause (l = r ← e_{1}, e_{2}, ..., e_{n}) ∈ E such that f occurs as the outermost function symbol in l or l is a variable; otherwise it is a defined function symbol.

1We assume that interpretations obey the axioms of equality, i.e. the reflexivity, symmetry, transitivity and the substitutivity for functions and predicates. Hence, satisfiability and logical consequence are defined w.r.t. these axioms.

The use of irreducible function symbols is justified from the several optimization techniques defined in [32]. This affects the size of the search tree of the E-unifiers for a set of equations. In the best case an infinite search tree can be reduced to a finite one. 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 definite function ones. The members of C are also called constructors. Terms are viewed as labelled trees in the usual way [31]. We will use, among others, the following standard notions: Occurrences are represented by sequences, possibly empty, of naturals. The empty sequence is represented by λ. t/u is the subterm at the occurrence u of t. t[u ← r] is the term t with the subterm at the occurrence u replaced with r.

4. The language CLP(H/E) and its Operational Semantics

4.1. CLP(H/E) logic programs

In this section we define the language CLP(H/E), which is an instance of CLP that caters for solving constraints in the structure H/E, defined as the finest partition induced by a canonical Horn equational theory without extra variables E on the Herbrand Universe H over a finite one sorted alphabet Σ. = is the only predicate symbol for constraints and is interpreted as semantic equality over the domain. This structure is solution compact since has no limit element [33]. It is known [35] that the equational theory E and the structure H/E correspond in the sense defined in [33], i.e. H/E ⊧ E, i.e. H/E models E and H/E ⊧ ˜∃c implies E ⊧ ˜∃c for all constraint c. Thus, a constraint c is E-unifiable iff it is H/E-solvable. We assume that (Π_{C}, Σ)-constraints are sets of Σ-equations to be solved in E by a suitable conditional narrowing algorithm which will be described in the following. 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}}.

Definition 4.1 CLP(H/E) programs Let Π_{C} = {=}, Π = Π_{C} ∪ Π_{B} and Π_{C} ∩ Π_{B} = Ø. We define a CLP(H/E) (Π, Σ)- program as a (Π, Σ)-program augmented by a canonical Horn equational Σ-theory without extra variables E.

Example 4.1 What follows is a CLP(H/E) program P ∪ E:

Number of nodes of a binary tree

P = { (p1) nn( Λ, 0).

(p2) nn( t(L_{t}, E, R_{t}), N) ← N = s(0) + L_{n} + R_{n} □ nn(L_{t}, L_{n}), nn(R_{t}, R_{n}).} E = { (e1) 0 + y = y.

(e2) s(x) + y = s(x + y). } CLP(H/E) programs enjoy the following property [35]: there is a canonical domain of computation, namely H/E, over which a canonical class of interpretations can be built. This is analogous to the canonicity of Herbrand interpretations for definite clause programs. For reasoning about negation, the theory E should be extended to be satisfaction complete, i.e. ℑ ⊧ ¬c whenever not ℑ ⊧ ˜∃c. Roughly speaking, satisfaction completeness means that every constraint is either provably satisfiable or provably unsatisfiable [34]. Unfortunately this is not possible. Hence the soundness and completeness results for finite failure and negation as failure are not inherited.

4.2. CLP(H/E) Incremental Constraint Solver

The standard way to integrate narrowing and resolution [5, 24] is using narrowing to generate the solutions which are then tested by the logic program. This method does not fit in the CLP scheme and requires some complex interactions between the backtrackings of the narrowing and the resolution algorithms. Instead, narrowing can be used as a procedure to test the consistency of the new constraint, looking for a solution, since the constraint is proved consistent once a solution has been found. Thus we consider how to incrementally reuse the work done in the previous step to keep smaller the cost of solving the new set. An approach that does not try to exploit the information which can be gathered from the previous steps to guide the search would be impractical [25].

In the CLP(H/E) framework it seems very natural to reuse the solution θ to the constraint c found in the previous step to check the solvability of the new constraint c∪c̃. In [25] the matter of incremental constraint satisfaction is also addressed. [25] shows that an approach based on backtracking is inadequate since it can only use passively the new constraints to test if they are satisfied by the newly generated tentative solutions. In the context of CLP it seems to be more appropriate using actively the new constraints to guide the search towards a solution. Accordingly, [25] presents a scheme based on reexecution and pruning of the search tree of resolution. We have a similar problem, yet related to the search tree of the constraint solving algorithm. In this section we are concerned with an incremental algorithm for testing the solvability and an appropriate simplified representation for constraints. In the following we describe a constraint solver for CLP(H/E) programs by means of a transition system labeled on (Π_{C}, Σ)-constraints and specially tailored to be incremental.

Definition 4.2 ICS-representation of a solvable constraint Let c be a solvable constraint. Let us suppose that c can be written in the form c_{1} ∪c_{2} (either of which can be empty) where c_{1} has a unique mgu θ over E. Then r_{c} = (θ̂, c_{2}) is the ICS-representation of the simplified constraint θ̂∪ c_{2}. The ICS-representation of an empty constraint is (Ø, Ø), which will be abbreviated as ().

Let us notice that if r_{c} = (θ̂ , Ø) then the constraint c has a unique mgu θ over E.

Definition 4.3 ICS-states We define an Incremental Constraint Solver (ICS) state s as a triple s = ⟨ θ, f, r_{c} ⟩, where r_{c} is the ICS-representation of a (Π_{C}, Σ)-constraint c, θ represents a E-unifier of c and f is a set of (Π, Σ)-substitutions.

Roughly speaking, for the Incremental Constraint Solver which will be described next, r_{c} represents the accumulated simplified constraint and f represents the set of substitutions which have already been unsuccessfully tried by the constraint solver and that are useful for a heuristic search of other solutions.

Definition 4.4 empty ICS-state, terminal ICS-states ⟨ ϵ, Ø, () ⟩ is the empty ICS-state. Any ICS-state can be a terminal ICS-state.

Definition 4.5 ICS-labels An ICS label c̃ is a (Π_{C}, Σ)-constraint. It represents the new constraint c̃ to be added to the accumulated simplified constraint c in order to test the solvability of the new set c ∪ c̃.

In the following we describe the ICS transition system. Roughly speaking, let s = ⟨ θ, f, r_{c} ⟩ be an ICS-state. In order to achieve incrementality, the costs of testing the solvability of the new set of constraints c ∪ c̃ should be as close as possible to the cost of solving the new constraint c̃ plus the cost of combining the new solution with the previous one. With this aim, since the substitution θ represents an E-unifier of the accumulated solvable constraint c, we search for an E-unifier to the new set c ∪ c̃ looking for the solutions to c̃θ . If c̃θ has no solution, we must start from scratch, looking for the solutions to the whole constraint c ∪ c̃ and add θ to the set of unsuccessfully tried substitutions. We use a Heuristic Conditional N arrowing procedure N which will be described later for the search of a solution θ′ of this constraint and combine adequately θ and θ′ to obtain a new accumulated solution and a new accumulated simplified constraint.

Definition 4.6 ICS transition relation^{2} ⟶^{c̃}_{ICS}

Single Solution Rules

(1) \frac{N (c̃θ, Ø) has a unique solution θ′}{⟨ θ, f, (θ̂, Ø) ⟩ ⟶^{c̃}_{ICS} ⟨ θθ′, f, (θ̂θ′, Ø) ⟩}

2For the sake of simplicity, in this set of rules c_{2} denotes a non empty constraint

(2) \frac{N (c̃θ, Ø) has a unique solution θ′ ∧ N ((c_{2} ∪ c̃)θ_{1}, Ø) has a unique sol θ′′}{⟨ θ, f, (θ̂_{1}, c_{2}) ⟩ ⟶^{c̃}_{ICS} ⟨ θ_{1}θ′′, f, (θ̂_{1}θ′′, Ø) ⟩}

Multiple Solution Rules

(3) \frac{N (c̃θ, Ø) has a unique solution θ′ ∧ N ((c_{2} ∪ c̃)θ_{1}, Ø) has a first sol θ′′}{⟨ θ, f, (θ̂_{1}, c_{2}) ⟩ ⟶^{c̃}_{ICS} ⟨θθ′, f, (θ̂_{1}, c_{2} ∪ c̃) ⟩}

(4) \frac{N (c̃θ, Ø) has a first solution θ′}{⟨ θ, f, (θ̂_{1}, c′) ⟩ ⟶^{c̃}_{ICS} ⟨ θθ′, f, (θ̂_{1}, c′ ∪ c̃) ⟩}

Start from Scratch Rules

(5) \frac{N (c̃θ, Ø) has no solution ∧ N (θ̂_{1} ∪ c_{2} ∪ c̃, f ∪ θ) has a unique solution θ′}{⟨ θ, f, (θ̂_{1}, c_{2}) ⟩ ⟶^{c̃}_{ICS} ⟨ θ′, f ∪ θ , (θ̂′, Ø) ⟩}

(6) \frac{N (c̃θ, Ø) has no solution ∧ N (θ̂_{1} ∪ c_{2} ∪ c̃, f ∪ θ) has a first solution θ′}{⟨ θ, f, (θ̂_{1}, c_{2}) ⟩ ⟶^{c̃}_{ICS} ⟨ θ′, f ∪ θ, (θ̂_{1}, c_{2} ∪ c̃) ⟩}

Let us notice that each transition of this system depends on the termination of the N arrowing procedure N. We assume that if N arrowing procedure N (c, f) terminates returning the output no solution then the constraint c has no E-unifier, if the output unique solution θ then θ is the unique mgu over E of c and if the output is first solution θ then θ is an E-unifier of c but, possibly, it is not the unique mgu over E of c. In the following we will define a transition system for CLP (H/E) which depends on the ICS solver. The transition relation for CLP (H/E) will depend on one single ICS transition step. Therefore, we do not rely on a termination proof for the ICS system.

The following theorem establishes the correctness of the Incremental Constraint Solver.

Theorem 4.1 (Correctness of ICS) If an ICS transition ⟨ θ, f, r_{c} ⟩ ⟶^{c̃}_{ICS} ⟨θ′, f′, r′_{c} ⟩ can be proved then the constraint c ∪ c̃ is solvable in H/E. r′_{c} represents the simplified form of this constraint and θ′ represents an E-unifier to it. f′ represents the set of substitutions unsuccessfully tried.

Obviously the incremental constraint solver as defined above is, in general, not complete because narrowing may loop forever in the evaluation of the condition of a rule not only when the constraint is not E-unifiable but also when it has a unique mgu over E that has already been found and it tries to obtain another solution. However, for some classes of problems, an incomplete but efficient constraint solver might turn out to be valuable from a programming standpoint, as pointed out in [26].

4.3. CLP(H/E) Operational Model

The following definitions instantiate definitions 2.13, 2.14 and 2.15 to the case of CLP(H/E) programs.

Definition 4.7 CLP(H/E) transition relation →_{CLP (H/E)} Let P ∪ E be a CLP(H/E) (Π, Σ)-program. The CLP(H/E) Transition Relation is given by the following rule describing a computation step from a configuration ⟨← s_{i} ◇ A_{1}, …, A_{n}⟩ where s_{i} = ⟨ θ_{i} , f_{i} , r_{c_{i}} ⟩:

\frac{s_{i} ⟶^{c̃}_{ICS} s_{i+1}}{⟨← s_{i}◇A_{1}, …, A_{n}⟩ →_{CLP (H/E)} ⟨← s_{i+1}◇B̃_{1}, …, B̃_{n}⟩}

if there exist n variants of clauses in P, H_{j} ← c′_{j}□B̃_{j}, j = 1, …, n, with no variables in common with ← c_{i}□A_{1}, …, A_{n}. and with each other and c̃ = {c′_{1}, c′_{2}, …, c′_{n}, A_{1} = H_{1}, …, A_{n} = H_{n}}.

Definition 4.8 CLP(H/E) initial configuration, CLP(H/E) terminal configurations Let G_{0} = ← c_{0}□B̃. be a goal. If c_{0} is not an empty constraint and the empty ICSstate s_{0} ⟶^{c_{0}}_{ICS} s then C_{0} = ⟨← s ◇ B̃⟩ is the CLP(H/E) initial configuration. If c_{0} is empty then C_{0} = ⟨← s_{0} ◇ B̃⟩. A terminal configuration has the form ⟨← s ◇ ⟩, where s = ⟨ θ, f, (θ̂_{1}, c_{2}) ⟩ is an ICS-state and c = (θ̂_{1} ∪ c_{2})_{|v̀ar(G_{0})}^{3} is the answer constraint.

As in the generic case, when the constraint solver is designed for simply testing the solvability of constraints, the above defined transition relation →_{CLP (H/E)} becomes the standard definition of derivation of goals. We give an example that illustrates the definitions above.

Example 4.2 Let us consider the following CLP(H/E) program^{4} P ∪ E [28]:

0/1 Knapsack problem P = { (p1) knapsack(M, L, W) ← addweight(M) = W □ sublist(M, L).

3By (θ̂_{1} ∪ c_{2}) |` var(G_{0}) we denote the least subset E′ ⊆ E = θ̂_{1}|v̀ar(G_{0}) ∪ c_{2}θ_{1} containing all the equations in E in which a variable from the initial goal G_{0} occurs and such that no variable occurring in an equation in E′ occurs in any of the equations in E \ E′. Trivial equations of the form t = t are discarded.

4For convenience we often abbreviate s^{n}(0) to n.

(p2) sublist([ ], Z).

(p3) sublist([X | Y], [X | Z])← □ sublist(Y, Z).
(p4) sublist(Y, [X | Z]) ← □ sublist(Y, Z). }

E = { (e1) 0 + Y = Y.

(e2) s(X) + Y = s(X + Y).

(e3) weight(a) = 1.
(e4) weight(b) = 1.
(e5) weight(c) = 2.
(e6) addweight([ ]) = 0.
(e7) addweight([X | Y]) = weight(X) + addweight(Y). }

% knapsack(M, L, W) states that items in the sublist M of a given list L can be packed into a knapsack such that the knapsack weights exactly W %

Let us consider the initial goal G_{0} = ← □ knapsack(K, [a, b], 2). Since the constraint in G_{0} is empty, the initial CLP(H/E) configuration is C_{0} = ⟨ ← ⟨ϵ, Ø, ()⟩ ◇ knapsack(K, [a, b], 2) ⟩ considering (p1), the new constraint c̃ is c̃ = {addweight(M) = W, K = M, L = [a, b], W = 2} since (c̃ϵ) has a first solution^{5} θ = {M/[a, a], K/[a, a], L/[a, b], W/2}, applying (4), C_{0} →_{CLP (H/E)} C_{1} = ⟨ ← ⟨θ, Ø, (Ø, c̃)⟩ ◇ sublist(M, L) ⟩ considering (p3), the new constraint c̃′ is c̃′ = {M = [X | Y], L = [X | Z]} since (c̃′θ) has a unique solution θ′ = {X/a, Y/[a], Z/[b]} and c̃∪c̃′ has a first solution θθ′ = {M/[a, a], K/[a, a], L/[a, b], W/2, X/a, Y/[a], Z/[b]}, applying (3), C_{1} →_{CLP (H/E)} C_{2} = ⟨ ← ⟨θθ′, Ø, (Ø, c̃ ∪ c̃′)⟩ ◇ sublist(Y, Z) ⟩ considering again (p3), the new constraint c̃′′ is c̃′′ = {Y = [X′ | Y′], Z = [X′ | Z′]} since (c̃′′θθ′) has no solution and c̃ ∪ c̃′ ∪ c̃′′ has a unique solution^{6} θ′′ = {M/[a, b], K/[a, b], L/[a, b], W/2, X/a, Y/[b], Z/[b], X′/b, Y′/[ ], Z′/[ ]}, applying (5), C_{2} →_{CLP (H/E)} C_{3} = ⟨ ← ⟨θ′′, θθ′, (θ̂′′, Ø)⟩ ◇ sublist(Y′, Z′) ⟩ considering (p2), the new constraint c̃′′′ is c̃′′′ = {Y′ = [ ], Z′ = Z′′} since (c̃′′′θ′′) has a unique solution θ′′′ = {Z′′/[ ]}, applying (1), C_{3} →_{CLP (H/E)} C_{4} = ⟨ ← ⟨θ′′θ′′′, θθ′, (θ̂′′θ′′′, Ø)⟩ ◇ ⟩ finally, since a final ICS-configuration has been reached, the answer constraint associated to this transition sequence is (θ̂′′θ′′′ ∪ Ø)_{|v̀ar(G_{0})} = (K = [a, b])

5Note that other solutions (e.g. {M/[c], K/[c], L/[a, b], W/2}) can be found.

6The narrowing calculus we define in Section 5. is able to find this solution and prove its uniqueness.

As shown in the example, the accumulated solvable constraint is simplified when rules (1), (2) and (5) are applied and the solution found in the previous step is always reused to try to prove that the new accumulated constraint is solvable. Thus the test of the solvability results much less expensive than a solvability test for the whole (non simplified) constraint.

5. Heuristic Conditional Narrowing

In this section, we present a Heuristic Conditional N arrowing Calculus (HCN C), an adaptation of the Conditional Narrowing Algorithm CNA presented in [32] which was shown complete for noetherian and confluent rewrite systems without extra variables. We extend it by actively using heuristic information to quickly converge towards a solution.

Narrowing was originally introduced in the field of automated theorem proving as a restricted version of the paramodulation rule [29]. A narrowing procedure for first order unification in an equational theory defined by a canonical and unconditional term rewriting system was given by Fay [15] and later improved by Hullot in [31]. Fay worked with normalizing narrowing and Hullot introduced the notion of basic narrowing. Nutt, Rety and Smolka [47] studied basic narrowing and its optimizations combined with normalizing narrowing. Bosco et al. [5] introduced narrowing selection. Lazy narrowing stems from Reddy [50]. Padawitz [48] presented refinements of narrowing and proved the correctness of the optimizations. Dershowitz [9], Hussmann [32] and Kaplan [38] investigated narrowing for conditional term rewriting systems. Hussmann extended Fay/Hullot work to theories defined by a confluent (possibly nonterminating) system of conditional rewrite rules and a completeness result w.r.t. normalized substitutions was given which holds if the system is non-trivial and the usual no extra-variables condition in the right-hand sides of the heads and in the bodies of the equational clauses is imposed [29]. Giovannetti and Moiso [23] explored the consequences of allowing the presence of extra-variables and gave a sufficient condition for completeness. Hölldobler [29] generalized the results obtained by Hullot and Hussmann. Fribourg [16] employed an innermost case of strategy-controlled narrowing. Middeldorp [44] carefully analyzes the completeness results for conditional basic narrowing. Echahed [11] and Padawitz [48] studied criteria to ensure completeness of narrowing selection strategies.

Let us briefly recall the Conditional Narrowing Algorithm CNA presented in [32]. An expression of the form c with τ where c is a set of equations and τ is a substitution is called a (sub-)goal. The substitution τ is assumed to be restricted to var(c_{0}), i.e. the variables of the constraint in the initial state, and the variables in the equational clauses are standardized apart, i.e. the set of variables in c and in the clauses are disjoint. To solve c_{0}, the algorithm starts with the subgoal c_{0} with ϵ and tries to derive subgoals (recording applied substitutions in the with-parts) until a terminal goal of the form Ø with θ is reached. Each substitution θ in a terminal goal is an E-unifier of c_{0}. By abuse of notation, it will often be called solution. Let O′(c) be the set of nonvariable occurrences of a constraint c. We define narred(c, u, k, σ) ⇔ ( u ∈ O′(c) ∧ (l_{k} = r_{k} ← ẽ_{k}) ∈ E ∧ σ = mgu(c/u, l_{k}) )

The calculus CNA is defined by the following two rules:

CNA unification rule:

\frac{c syntactically unifies with mgu σ}{c with τ →_{CNA} Ø with τσ}

CNA narrowing rule:

narred(c, u, k, σ) holds
c with τ →_{CNA} (ẽ_{k}, c[u ← r_{k}])σ with τσ

This calculus defines an algorithm, since all the CNA-derivations (sequences of states) from a given subgoal can be easily enumerated. These derivations can be represented by a (possibly infinite) finitely branching tree. The nodes of this tree have to be visited following a complete search strategy (e.g. breadth first) while looking for unifiable nodes.

In the following, we present the Heuristic Conditional N arrowing Calculus (HCN C).

Definition 5.1 N -state An N -state is a triple ⟨n, θ, L⟩, where n is a positive integer ∈ {0, 1, 2}, θ is a (Π, Σ)- substitution and L is a (possibly empty) list [g_{i}]_{i=1}^{n} of subgoals g_{i} = c_{i} with τ_{i}, where c_{i} is a set of (Π_{c}, Σ)-constraints (a conjunction of equations) and τ_{i} is a (Π, Σ)- substitution. List constructors are denoted by [ ] and •. By abuse of notation, we assume • to be homomorphically extended to concatenation of lists.

Roughly speaking, the first component of an N -state represents the current number of solutions. The second component represents the solution to be returned and the third component represents the list of subgoals yet to be narrowed. The nodes of the narrowing search tree are stored in the list. This list is treated as a queue to emulate a breadth first search strategy of the search tree.

To solve the conjunction of equations c_{0} using the heuristic information f, the algorithm starts with the initial N -state N_{0} = ⟨0, ϵ, [ c_{0} with ϵ ]⟩ and tries to derive subgoals (recording applied substitutions in the with-parts) until a terminal N -state ⟨n, θ, L⟩ ↛_{HCN C} is reached. Terminal N −states are characterized by L = [ ]. The set f of substitutions unsuccessfully tried by the constraint solver are used for a heuristic search of the solutions. If ρ is a substitution which belongs to f, then, by the compactness theorem it can not solve the accumulated constraint c because there is a subset of c which can not be solved. Moreover, no substitution ρ′ such that, restricted to the variables of c_{0}, is an instance of ρ can solve c_{0} either.

Given a set of variables W we say that two substitutions θ, σ are equal on W, denoted by σ = θ[W], iff xσ = xθ ∀x ∈ W. Let us define the relation ⪯ over substitutions: a substitution θ is more general than σ on W, denoted by θ ⪯ σ[W], iff σ = θλ[W] for some substitution λ. In the following we assume W = var(c_{0}), where c_{0} is the constraint in the initial state, and thus it will be omitted.

Let ⟨n, θ, L⟩ be a N -state and c_{i} with τ_{i} be a subgoal in L. Let S = {⟨u, k, σ⟩ | narred(c_{i}, u, k, σ)}. If ⟨u′, k′, σ′⟩ ∈ S and (∃ρ ∈ f) such that ρ ⪯ τ_{i}σ′ then the corresponding subtree of the search tree which has as root the subgoal (ẽ_{k′}, c_{i}[u′ ← r_{k′}])σ′ with τ_{i}σ′ does not contain any solution. Since it is useless to explore this subtree, we will ’prune the search tree’ by removing the representation of its root (⟨u′, k′, σ′⟩) from S.

The set of substitutions f can be thought of as a characterization of non unifiability. The prune based on f involves an improvement comparable to the profit drawn from a perfect intelligent backtracking. Intelligent backtracking [55] analyzes unification failure to avoid thrashing which arises when backtracking would follow paths which predictably contain no solutions. We obtain this improvement simply by comparing the previously failed substitutions with the current one by means of the relationship ⪯. The cost of keeping the set f is linear with the length of the CLP (H/E) derivation.

Definition 5.2 Heuristic Conditional N arrowing Calculus (HCN C)

The HCN C calculus is defined by means of a stratified transition system^{7}:

Heuristic Branching Rules

(1) \frac{\{⟨u, k, σ⟩ | narred(c, u, k, σ) \} = Ø}{c with τ →_{Branch} [ ]}

(2) \frac{s to l(\{⟨u, k, σ⟩ | narred(c, u, k, σ) ∧ \{ρ ∈ f | ρ ⪯ τσ\} = Ø\}) = [⟨u_{i}, k_{i}, σ_{i}⟩]_{i=1}^{n}}{c with τ →_{Branch} [ (ẽ_{k_{i}}, c[u_{i} ← r_{k_{i}}])σ_{i} with τσ_{i} ]_{i=1}^{n}}

where the choice function s to l(S) returns a list composed by the elements of the set S.

Success Rules

7The states of the transition system for Branch are subgoals or list of subgoals

(3) \frac{c with τ →_{Branch} L′ ∧ c synt. unifies with mgu σ}{⟨0, ϵ, c with τ • L⟩ →_{HCN C} ⟨1, τσ, L • L′⟩}

(4) \frac{c with τ →_{Branch} L′ ∧ c synt. unifies with mgu σ ∧ (τσ) ⪯̸ θ ∧ θ ⪯̸ (τσ)}{⟨1, θ, c with τ • L⟩ →_{HCN C} ⟨2, θ, [ ]⟩}

Narrowing Rules

(5) \frac{c with τ →_{Branch} L′ ∧ c syntactically unifies with mgu σ ∧ θ ⪯ (τσ)}{⟨1, θ, c with τ • L⟩ →_{HCN C} ⟨1, θ, L • L′⟩}

(6) \frac{c with τ →_{Branch} L′ ∧ c syntactically unifies with mgu σ ∧ (τσ) ⪯ θ}{⟨1, θ, c with τ • L⟩ →_{HCN C} ⟨1, τσ, L • L′⟩}

(7) \frac{c with τ →_{Branch} L′ ∧ mgu(c) = Ø ∧ n ∈ \{0, 1\}}{⟨n, θ, c with τ • L⟩ →_{HCN C} ⟨n, θ, L • L′⟩}

Roughly speaking, the Narrowing and Success rules basically consider two cases: the constraint c has an mgu σ or not. In the latter case we just proceed. In the first case we compare τσ (where τ is the substitution accumulated by narrowing so far) with the first solution θ. In case they are incomparable we stop as a second solution for the initial constraint has been found. In case τσ is more general we replace the first solution by it (we have found a more general first solution). Finally, we just proceed in case the solution θ is more general than τσ. Let us now illustrate Definition 5.2 by the following:

Example 5.1 Let us consider the constraint c = {U + s(Z) = s(0)} within the equational theory E in Example 4.2. Let f = {{U/s(X)}}. The sequence

⟨0, ϵ, [U + s(Z) = s(0) with ϵ]⟩ ⟶^{(7)}_{HCN C} ⟨0, ϵ, [s(Z) = s(0) with {U/0}]⟩ ⟶^{(3)}_{HCN C}

⟨1, {U/0, Z/0}, [ ]⟩ shows that HCN C is able to find the (unique) solution {U/0, Z/0} for c. Notice that U + s(Z) = s(0) with ϵ →_{Branch} [s(Z) = s(0) with {U/0}] as U + s(Z) unifies with the heads of the clauses (e1) and (e2), but for the mgu ρ′ = {U/s(X′), Y′/s(Z)} with the head of (e2) there exists ρ = {U/s(X)} ∈ f such that ρ ⪯ ρ′.

Definition 5.3 Behaviour of the HCN C calculus Let N_{0} = ⟨0, ϵ, [ c_{0} with ϵ ]⟩. We define:

N (c_{0}, f) = \{ \begin{matrix}no solution & if N_{0} →∗_{HCN C} ⟨0, ϵ, [ ]⟩ \\ unique solution θ & if N_{0} →∗_{HCN C} ⟨1, θ, [ ]⟩ \\ first solution θ & if N_{0} →∗_{HCN C} ⟨2, θ, [ ]⟩ \end{matrix}

Let us notice that if f = Ø then the above algorithm explores (the prefix of) the search tree of CNA which would have been explored following a breadth first search strategy until the conditions characterizing a terminal N -state would have been reached. If HCN C does not terminate or terminates with L = [ ] and n ∈ {0, 1} then N (c, f) is equivalent to CNA as it explores exactly the same search tree.

When f ≠ Ø the heuristic pruning based on f only removes subtrees which do not contain any solution so that it is guaranteed that no solution is lost.

The following theorem establishes the correctness of the Heuristic Conditional N arrowing N (c, f).

Theorem 5.1 (Correctness of the Heuristic Conditional N arrowing) Let E be a canonical conditional Horn equational theory without extra variables. Let c be a constraint. Let f be a set of substitutions such that no instance of any of them can solve c. If N (c, f) returns the output no solution then the constraint c is not solvable. If the output is unique solution θ then θ is the unique mgu over E of c. If the output is first solution θ then θ is a solution over E to c.

Let us notice that when N (c, f) returns the output first solution θ, θ might be the unique mgu over E of c. In fact, the solutions are checked not to be syntactic instances of one another while only two solutions which are not E-instances of one another should be distinguished. This means that the incremental constraint solver may simplify the constraint less than it would be possible. The Heuristic Conditional Narrowing as defined above is a procedure to test the solvability of constraints over the structure H/E. If the constraint is solvable then the procedure finds a solution (an E-unifier) to it and looks for another incomparable E-unifier. If the constraint is not E-unifiable or if there is not a second solution, the procedure may run forever.

Even in the case of canonical theories, the use of narrowing as a semantic unification procedure presents several drawbacks since it may not terminate when there are no (more) solutions and the generation of an independent set of E-unifiers is not guaranteed. An infinite set of solutions can be derived even if the equation admits a finite complete minimal one [31]. This problem was also inherited by the various techniques developed for equational resolution, as SLDE-resolution, where a single resolution step may loop forever without producing any answer. In [31], a sufficient condition for termination is given for canonical non-conditional theories.

To overcome these difficulties, several proposals have been made. In [29] a lazy resolution rule is introduced. With this rule, the problem of the unification of a set of equations within the theory E must not be solved before the rule can be applied but the equations are added as a constraint to the derived goal clause without testing its solvability. For instance, the constraint solving could be delayed until all other goals are solved and eventually the accumulated constraint can be solved by a complete E-unification algorithm. This is similar to the postponement of the satisfiability test of non linear constraints in CLP(ℜ) [36]. [3] presents a static analysis which allows to approximate the problem of detection of unsatisfiability of a set of equations. [3] also shows how to use actively this analysis to prune the search tree of an incremental equational constraint solver.

5.1. Optimizations of HCN C

The high degree of non-determinism inherent to narrowing often causes the generation of many redundant derivations. It is clear that the above procedure should be optimized in order to be suitably implemented and embedded into CLP(H/E). In this section we recall two useful optimizations (defined in [32, 16, 47]) of HCN C that significantly reduce the size of the search tree.

1. This optimization is based on the concept of irreducible function symbol to detect the unsolvability of an equation :

If a subgoal in a N -state occurring in HCN C contains an equation f(t_{1}, t_{2}, …, t_{n}) = g(t′_{1}, t′_{2}, …, t′_{n}) and f, g are irreducible, then:

• if f ≠ g then the subgoal is not solvable and can be removed.

• if f = g then the equation can be replaced by the set of equations t_{1} = t′_{1}, t_{2} = t′_{2}, …, t_{n} = t′_{n}.

This optimization can reduce an infinite search tree to a finite one [32].

2. If a subgoal in a N -state occurring in HCN C contains an equation x = t or t = x where x ∈ V, x ∉ var(t) and all function symbols in t are irreducible, then the equation can be dropped. The substitution {x/t} has to be applied to the whole subgoal.

For other optimizations, we refer to [32, 48]. Several strategies to reduce the number of subterms that have to be narrowed can be considered [6, 23, 31, 47]. The following section proposes an optimization strategy based on the results about selection narrowing presented in [6, 23].

6. CLP(H/E) Optimized Incremental Constraint Solver

In this section we define another incremental constraint solver iCS for CLP(H/E) which allows to drastically cut the search space under certain circumstances. iCS reuses the work already done when a new constraint is incrementally added. The kernel of iCS is an innermost conditional narrowing calculus iCN C which explores (a prefix of) a search tree for the constraint c ∪ c̃ which is built by extending the innermost selection narrowing strategy defined in [6]. This tree is incrementally built as long as new constraints are added.

The innermost conditional narrowing calculus iCN C defines a strategy which looks for a single E-unifier θ of the input constraint c and returns as output the list L of subgoals yet to be narrowed.

We assume in the following a function select-don’t-care(Occ) which nondeterministically selects one innermost occurrence (i.e. an occurrence which is not the prefix of any other occurrence [6, 16]) in the set Occ. ♯c stands for the cardinality of the set c.

Definition 6.1 Innermost Conditional N arrowing Calculus (iCN C) An iCN C-state is a pair ⟨n, L⟩, where n ∈ {0, 1} and L is a (possibly empty) list [g_{i}]_{i=1}^{n} of subgoals g_{i} = c_{i} with (τ_{i}, Occ_{i}), where c_{i} is a set of (Π_{c}, Σ)-constraints (a conjunction of equations), τ_{i} is a (Π, Σ)- substitution and Occ_{i} is the set of narrowable occurrences of c_{i}.

The iCN C transition relation is the following^{8}:

Don’t-care Branching Rule

(1) \frac{u_{0} = select-don’t- care(Occ) ∧ s to l(\{⟨u_{0}, k, σ⟩ | narred(c, u_{0}, k, σ)\}) = [⟨u_{0}, k_{i}, σ_{i}⟩]_{i=1}^{n}}{\begin{matrix}c with (τ, Occ) →_{DcB} \\ c with (τ, (Occ \ \{u_{0}\})) • [ (c[u_{0} ← r_{k_{i}}], ẽ_{k_{i}})σ_{i} with \\ (τσ_{i}, ((Occ \ \{u_{0}\}) ∪ \{u_{0}.v | v ∈ O′(r_{k_{i}})\} ∪ O(c, ẽ_{k_{i}}))) ]_{i=1}^{n} \end{matrix}}

where O(c, c̃) = {(♯c + j).k | j.k ∈ O′(c̃)}.

Unification Rule

(2) \frac{c syntactically unifies}{⟨0, c with (τ, Ø) • L⟩ →_{iCN C} ⟨1, c with (τ, Ø) • L⟩}

Narrowing Rules

(3) \frac{c with (τ, Occ) →_{DcB} L′}{⟨0, c with (τ, Occ) • L⟩ →_{iCN C} ⟨0, L • L′⟩}

8We assume for simplicity that in the following rules Occ is a non empty set.

(4) \frac{mgu(c) = Ø}{⟨0, c with (τ, Ø) • L⟩ →_{iCN C} ⟨0, L⟩}

Roughly speaking, in Definition 6.1 the effect of the function select-don’t-care(Occ) is to limit the search at each application of rule (1) to one subterm only from all the possible ones. This strategy can be further optimized by the following test. Remove from the list in the second argument of the state any failed subgoal, i.e. any subgoal c with (τ, Occ) such that one equation e ∈ c is not unifiable and there is no occurrence in Occ for e. A node of a search tree is called failed if it contains a failed subgoal.

Definition 6.2 Behaviour of the iCN C calculus Let us define the function:

iN (L) = L′ if ⟨0, L⟩ →∗_{iCN C} ⟨1, L′⟩

We introduce an innermost search tree as a tree whose nodes are labeled by subgoals, the root is labeled by the constraint to be solved and at each node the innermost narrowable occurrence (nondeterministically chosen) is expanded by the innermost selection narrowing algorithm in [6] extended to conditional theories (innermost conditional narrowing for short).

Definition 6.3 An innermost search tree for a constraint c to be solved is a tree whose nodes are labeled by subgoals c_{i} with (τ_{i}, Occ_{i}), where the subgoal in the root is c with (ϵ, O′(c)).

Let g = c with (τ, Occ) be a node where Occ ≠ ∅. Let u_{0} = select-don’t-care(Occ) and assume that s to l({⟨u_{0}, k, σ⟩ | narred(c, u_{0}, k, σ)}) = [⟨u_{0}, k_{i}, σ_{i}⟩]_{i=1}^{m}. Then g has a child c with (τ, Occ\{u_{0}}) and m children (c[u_{0} ← r_{k_{i}}], ẽ_{k_{i}})σ_{i} with (τσ_{i}, ((Occ \ {u_{0}}) ∪ {u_{0}.v | v ∈ O′(r_{k_{i}})} ∪ O(c, ẽ_{k_{i}}))), i = 1, …, m.

Definition 6.4 Let us consider an innermost search tree t for the constraint c. The list L_{c} of the non-failed leaves of t is called the representation of t.

Notice that in Definition 6.4 L_{c} represents an execution state of the innermost conditional narrowing algorithm, i.e. the set of derived subgoals which are yet to be narrowed.

Definition 6.5 An iCS-state is a pair ⟨c , L⟩, where c is a constraint and L is a list of subgoals. The empty iCS-state is ⟨Ø , [ ]⟩.

Lemma 6.1 Let c be a constraint.

• iN (L_{c}) = L′ = c′ with (τ, Ø) • L′′ iff there exists a terminal iCN C-state ⟨1, L′⟩ such that σ = mgu(c′), θ = τσ is a solution for c and the list L′ represents an execution state of the innermost conditional narrowing algorithm when θ is found.

Definition 6.6 (iCS transition relation ) ↪^{c̃}_{iCS}

\frac{L′ = iN (merge(L, c̃))}{⟨c , L⟩ ↪^{c̃}_{iCS} ⟨c ∪ c̃ , L′⟩}

where

merge([ ], c̃) = [c̃ with (ϵ, O′(c̃))]

merge([c_{i} with (τ_{i}, Occ_{i})]_{i=1}^{n≥1}, c̃) = [(c_{i}, c̃τ_{i}) with (τ_{i}, Occ_{i} ∪ O(c_{i}, c̃))]_{i=1}^{n}

Roughly speaking, in definition 6.6, L is thought as the representation in form of a list of the search tree for the constraint c. The following lemma shows that the function merge(L, c̃) merges L and the constraint c̃ building the representation of a search tree for c ∪ c̃.

Lemma 6.2 Let L_{c} represent an innermost search tree for the constraint c denoting an execution state of the innermost conditional narrowing algorithm for c when the first solution to c is found. Then merge(L_{c}, c̃) represents an innermost search tree for c ∪ c̃ corresponding to this state.

Let us now illustrate Lemma 6.2 by an example.

Example 6.1 Let us consider the equational theory E in Example 4.2. Figure 1 shows an innermost search tree for the constraint c = {U + Z = s(0)} with respect to E.

[figure: {Y =s(0)} with ({U/0,Z/Y },∅); {s(X+Y)=s(0)} with ({U/s(X),Z/Y },{1.1.1}); {U+Z=s(0)} with (ϵ,{1.1}); {U+Z=s(0)} with (ϵ,∅); ×]

figure 1 The list L_{c} = [{Y = s(0)} with ({U/0, Z/Y }, ∅), {s(X +Y) = s(0)} with ({U/s(X), Z/Y }, {1.1.1})] of the leaves of the tree in Figure 1 represents the tree.

Let c̃ = {U + 0 = s(W)} be a new constraint. The list L_{c∪c̃} = merge(L_{c}, c̃) = [{Y = s(0), 0+0 = s(W)} with ({U/0, Z/Y }, {2.1}), {s(X +Y) = s(0), s(X)+0 = s(W)} with ({U/s(X), Z/Y }, {1.1.1, 2.1})] represents the innermost search tree for the constraint c ∪ c̃ which is shown in Figure 2. Note that the leftmost node in this tree can be dropped since the equation U + Z = s(0) in the node does not unify and no occurrence in the set {2.1} of the narrowable occurrences corresponds to this equation.

[figure: {Y =s(0),0+0=s(W)}; with ({U/0,Z/Y },{2.1}); {s(X+Y)=s(0),s(X)+0=s(W)}; with ({U/s(X),Z/Y },{1.1.1,2.1}); {U+Z=s(0),U+0=s(W)}; with (ϵ,{1.1,2.1}); {U+Z=s(0),U+0=s(W)}; with (ϵ,{2.1})]

figure 2

The strategy defined by the calculus iCS can be proved complete by using the following result of completeness of the conditional selection narrowing in [44].

Proposition 6.3 [23], [44] Let E be a conditional equational theory such that the associated term rewriting system is noetherian and level confluent. Then the conditional selection narrowing algorithm is complete for E.

Theorem 6.1 (Correctness and Completeness of iCS) An iCS transition ⟨c , L_{c}⟩ ↪^{c̃}_{iCS} ⟨c ∪ c̃ , L′⟩ is performed iff the constraint c ∪ c̃ is solvable in H/E, and L′ represents an innermost search tree of c ∪ c̃.

Let us notice that the above described techniques can also be easily adapted to the optimization of the Incremental Constraint Solver ICS described in Section 4.2..

7. Conclusions

In this paper we have considered the language CLP(H/E), its semantics and its constraint solver. On the semantics side, we have first defined an operational semantics SS(P, ℜ) and an equivalent fixpoint semantics F ix(P, ℜ) which fully characterize the operational behaviour of CLP programs. We have given a notion of n-model based on the truth on (standard) R-interpretations [34] and we have defined a complete partial order on n-models. This semantics is similar to the S-semantics of pure logic programs and turns out to be the adequate semantic framework for program analysis and transformation. This semantics is inherited by every instance of CLP and, in particular, by CLP(H/E).

Then we have presented, in a formal setup, several strategies to obtain an incremental narrower as constraint solver for canonical Horn equational theories. We have presented a calculus which allows to reuse the substitutions discarded as a heuristic to look for other solutions. Finally we have given a calculus which builds incrementally the search tree which represents the set of solutions to a constraint.

Our methods fits in the CLP scheme, as opposed to the standard way to integrate narrowing and resolution [24] where narrowing generates the solutions which are then tested by the logic program.

The CLP framework we have considered is the one originally introduced by Jaffar and Lassez [18, 33]. Our construction however could equivalently be defined in other CLP frameworks, such as the one proposed in [27].

References

[1] M. Alpuente and M. Falaschi. Narrowing as an Incremental Constraint Satisfaction Algorithm. In J. Maluszyński and M. Wirsing, editors, Proc. of PLILP’91, volume 528 of Lecture Notes in Computer Science, pages 111–122. Springer-Verlag, Berlin, 1991.

[2] M. Alpuente, M. Falaschi, and G. Levi. Incremental Constraint Satisfaction for Equational Logic Programming. Technical Report TR-20/91, Dipartimento di Informatica, Università di Pisa, 1991. To appear on Theoretical Computer Science.

[3] M. Alpuente, M. Falaschi, and F. Manzo. Analyses of unsatisfiability for incremental equational logic programming. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP’92, volume 631 of Lecture Notes in Computer Science, pages 443–457. Springer-Verlag, Berlin, 1992.

[4] M. Bellia and G. Levi. The relation between logic and functional languages. Journal of Logic Programming, 3:217–236, 1986.

[5] P. Bosco, E. Giovannetti, and C. Moiso. Refined strategies for semantic unification. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proc. of TAPSOFT’87, volume 250 of Lecture Notes in Computer Science, pages 276–290. Springer-Verlag, Berlin, 1987.

[6] P. Bosco, E. Giovannetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3–23, 1988.

[7] P.G. Bosco, E. Giovannetti, G. Levi, and C. Palamidessi. A complete semantic characterization of K-leaf, a logic language with partial functions. In Proceedings of the IEEE Symposium on Logic Programming, pages 318–327, 1987.

[8] N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

[9] N. Dershowitz and A. Plaisted. Logic Programming cum Applicative Programming. In Proc. First IEEE Int’l Symp. on Logic Programming, pages 54–66. IEEE, 1984.

[10] M. Dincbas and P. van Hentenryck. Extended Unification Algorithms for the Integration of Functional Programming into Logic Programming. Journal of Logic Programming, 4:197–227, 1987.

[11] R. Echahed. On completeness of narrowing strategies. In Proc. of CAAP’88, volume 299 of Lecture Notes in Computer Science, pages 89–101. Springer-Verlag, Berlin, 1988.

[12] N. Heintze et al. The CLP Programmer’s Manual. Dept. of Computer Science, Monash University, Australia, 1986.

[13] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

[14] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs. Technical Report TR 32/89, Dipartimento di Informatica, Università di Pisa, 1989. To appear in Information and Computation.

[15] M. Fay. First Order Unification in an Equational Theory. In 4th Int’l Conf. on Automated Deduction, pages 161–167, 1979.

[16] L. Fribourg. Slog: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. Second IEEE Int’l Symp. on Logic Programming, pages 172–185. IEEE, 1985.

[17] U. Furbach, S. Hölldobler, and J. Schreiber. Horn equality theories and paramodulation. Journal of Automated Reasoning, 5:309–337, 1989.

[18] M. Gabbrielli and G. Levi. Modeling Answer Constraints in Constraint Logic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 238– 252. The MIT Press, Cambridge, Mass., 1991.

[19] M. Gabbrielli and G. Levi. Modeling answer constraints in Constraint Logic Programs. Technical Report TR 4/91, Dipartimento di Informatica, Università di Pisa, 1991.

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

[21] J.H. Gallier and W. Snyder. A general complete E-unification procedure. In P. Lescanne, editor, Rewriting Techniques and Applications, volume 256 of Lecture Notes in Computer Science, pages 216–227. Springer-Verlag, Berlin, 1987.

[22] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42:139–185, 1991.

[23] 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.

[24] J. Goguen and J. Meseguer. Eqlog: Equality, Types and Generic Modules for Logic Programming. In D. de Groot and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986.

[25] P. Van Hentenryck. Incremental Constraint Satisfaction in logic programming. In D. H. D. Warren and P. Szeredi, editors, Proc. Seventh Int’l Conf. on Logic Programming, pages 189–202. The MIT Press, Cambridge, Mass., 1990.

[26] P. Van Hentenryck and Y. Deville. Operational Semantics of Constraint Logic Programming over Finite Domains. In J. Maluszyński and M. Wirsing, editors, Proc. of PLILP’91, volume 528 of Lecture Notes in Computer Science, pages 395–406. Springer-Verlag, Berlin, 1991.

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

[28] S. Hölldobler. Equational Logic Programming. In Proc. Second IEEE Symp. on Logic In Computer Science, pages 335–346. IEEE Computer Society Press, 1987.

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

[30] S. Hölldobler. Conditional equational theories and complete sets of transformations. Theoretical Computer Science, 75:85–110, 1990.

[31] 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.

[32] H. Hussman. Unification in conditional-equational theories. Technical report, Fakultät für Mathematik und Informatik, Universität Passau, 1986.

[33] 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.

[34] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. Technical report, Department of Computer Science, Monash University, June 1986.

[35] J. Jaffar, J.-L. Lassez, and M.J. Maher. A logic programming language scheme. In D. de Groot and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 441–468. Prentice Hall, Englewood Cliffs, NJ, 1986.

[36] J. Jaffar and S. Michaylov. Methodology and Implementation of a CLP System. In J.-L. Lassez, editor, Proc. Fourth Int’l Conf. on Logic Programming. The MIT Press, Cambridge, Mass., 1987.

[37] S. Kaplan. Conditional Rewrite Rules. Theoretical Computer Science, 33:175– 193, 1984.

[38] S. Kaplan. Fair conditional term rewriting systems: unification, termination and confluence. In H.-J. Kreowski, editor, Recent Trends in Data Type Specification, volume 116 of Informatik-Fachberichte, pages 136–155. Springer-Verlag, Berlin, 1986.

[39] 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.

[40] G. Levi. Models, Unfolding Rules and Fixpoint Semantics. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 1649–1665. The MIT Press, Cambridge, Mass., 1988.

[41] G. Levi and P. Mancarella. The Unfolding Semantics of Logic Programs. Technical Report TR-13/88, Dipartimento di Informatica, Università di Pisa, 1988.

[42] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[43] A. Martelli, C. Moiso, and G.F. Rossi. An algorithm for unification in equational theories. In Proc. IEEE Symp. on Logic Programming, pages 180–186. IEEE, 1986.

[44] A. Middeldorp and E. Hamoen. Counterexamples to completeness results for basic narrowing. In H. Kirchner and G. Levi, editors, Proc. Third Int’l Conf. on Algebraic and Logic Programming, volume 632 of Lecture Notes in Computer Science, pages 244–258. Springer-Verlag, Berlin, 1992.

[45] J.J. Moreno and M. Rodriguez-Artalejo. BABEL: A Functional and Logic Programming Language based on a constructor discipline and narrowing. In I. Grabowski, P. Lescanne, and W. Wechler, editors, Algebraic and Logic Programming, volume 343 of Lecture Notes in Computer Science, pages 223–232. Springer-Verlag, Berlin, 1988.

[46] J.J. Moreno and M. Rodriguez-Artalejo. Logic Programming with Functions and Predicates: The language Babel. Journal of Logic Programming, 12(3):191–224, 1992.

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

[48] P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1988.

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

[50] 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.

[51] J.H. Siekmann. Universal unification. In 7th Int’l Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 1–42. Springer-Verlag, Berlin, 1984.

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

[53] H. Tamaki. Semantics of a Logic Programming Language with a Reducibility Predicate. In Proc. First IEEE Int’l Symp. on Logic Programming, pages 259– 264. IEEE, 1984.

[54] M.H. van Emden and K. Yukawa. Logic Programming with Equations. Journal of Logic Programming, 4:265–288, 1987.

[55] D. A. Wolfram. Intractable unifiability problems and backtracking. In E. Y. Shapiro, editor, Proc. Third Int’l Conf. on Logic Programming, volume 225 of Lecture Notes in Computer Science, pages 107–121. Springer-Verlag, Berlin, 1986.