Conditional Narrowing with Constructive Negation^{⋆}

María José Ramírez^{1}, Moreno Falaschi^{2}

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

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

Abstract. In this paper, we present a narrower for conditional equational theories whose clauses allow disequations in their bodies (normal theories). Our approach deals with disequations in a constructive manner and thus allows non ground negative queries. We give a formal operational semantics for normal theories and define the notion of completion and stratification of a normal theory. We show that there exists one minimal model for the completion of a stratified normal theory. Then we prove the correctness of the operational semantics with respect to the completion of a stratified normal theory.

Keywords: Equational logic programming, constructive negation, term rewriting systems, narrowing.

1 Introduction

In this paper we are concerned with an algorithm specialized in solving equations and negated equations (disequations) with respect to a normal equational theory, i.e. a conditional equational theory which allows disequations in the conditions of the clauses (but not in the head). The ability to deal with disequations is not only of theoretical interest but also desirable in practice. Different approaches for handling disequations have been proposed. For instance, in the framework of logic programmig Colmerauer solves disequations in the algebra of rational trees for the semantic definition of Prolog II ([13]). Lassez, Maher and Marriott prove the solvability of systems of equations and disequations on the Herbrand Universe ([27]). In this paper we focus on conditional equations whose conditions may contain disequations. We solve disequations with an algorithm which follows an idea similar to that defined by Stuckey in [40]. On the other hand, our approach is different since we refer to equational theories, while [40] focuses on the use of constructive negation in Constraint Logic Programming.

⋆ This work has been partially supported by CICYT under grant TIC 92-0793

The introduction of negation has been widely investigated in the framework of logic programming [12, 16, 26, 29] and has also been recently investigated in the framework of equational programming [5, 6, 25]. Negation as failure (NAF) is the mechanism traditionally used in logic programming to implement negation. However, NAF can only handle ground negative subgoals since it cannot generate any new bindings for query variables. Constructive Negation [10, 11, 40] can be used to find answers for negative subgoals in the same way as for positive ones. The basic idea is that the answer for a negative goal is simply the negation of the set of answers for its positive version. In order to evaluate ∼Q, a subderivation with Q as the top query is executed until it reduces to a simplified formula F . Then, a normalisation and negation procedure is applied to F to compute the simplified formula for ∼Q. This operational mechanism subsumes negation as failure. We propose to use this idea in the context of equational programming. This allows to solve negative non-ground queries as well as positive ones. Kaplan [25] investigates the algebraic properties of positive/negative conditional term rewriting systems and defines the class of reducing systems for which there exists an algebra of normal forms as quasi-initial model. Bachmair and Ganzinger [5, 6] consider general equational clauses and give a criterion, based on a total ordering on ground terms, to prove that a consistent clause equality theory has a unique perfect model [37, 38]. Moreover, [6] introduces the concept of saturation as an extension of the Knuth-Bendix completion method to transform a set of conditional equations with negative and positive conditions into a confluent system. All these approaches [5, 6, 25] consider ground systems and the results can be easily applied to negative ground queries. Our approach aims to deal with negative non-ground queries as well.

We aim to develop a system which may also be suitable for the integration of different programming paradigms, such as logic and equational programming, in a single framework. There have been several proposals [7, 14, 18, 19, 32] on this, but the treatment of negation has not been widely investigated in any of them. One way to the integration of equational and logic programming is the use of narrowing strategies, see e.g. [18, 19, 32]. Narrowing is a strategy to solve a system of equations within an equational theory E: given an equational query, narrowing is able to find a complete set of E-unifiers for it. However, narrowing does not handle systems which include negation.

We present an algorithm (extended narrower) which solves equations and disequations with respect to a normal equational theory. Equations and disequations are handled in a similar way, following the idea that a simplified form of a negated formula can be obtained from its complementary positive one. We show that the answer to a conjunction of equations and disequations in an equational theory with constructors is a complex system involving negation and quantifiers, where the symbols of equality and disequality can be syntactically interpreted.

We give a formal operational semantics for normal theories and define the notion of completion and stratification of a normal theory. These definitions have similarities with those for logic programming [3, 4, 12]. Roughly speaking, completion for us means that we replace the implications in a conditional equational theory with co-implications, so that the resulting completed theory allows negative logical consequences. Completed theories are not necessarily consistent. Thus, we introduce the concept of stratified theory, which essentially means introducing some syntactic restrictions to disallow recursion through negation. We show that there exists one minimal model for the completion of a stratified normal theory. Then we prove the correctness of the operational semantics with respect to the completion of a stratified normal theory.

The paper is organized as follows. Section 2 contains a short introduction to equations, conditional rewrite systems and universal unification. In Section 3, we define normal equational theories. In Section 4 we give a formal operational semantics for our algorithm. The notions of completion and stratification for normal equational theories are given in Sections 5 and 6, respectively. In Section 7 we prove the correctness of the operational semantics. Finally, Section 8 concludes and mentions further research.

2 Preliminaries

In this section we briefly review some basic concepts about equations, conditional rewrite systems and E-unification. For any concept which is not explicitly defined the reader may refer to [21, 39].

We will use the symbols V , Σ and Π to denote the sets of variables, function symbols and predicate symbols respectively. τ(Σ) and τ(Σ ∪ V ) denote the sets of ground terms and terms built on Σ and V , respectively. τ(Σ) is usually called the Herbrand Universe (H_{Σ}) over Σ and it will be denoted by H. The set of variables occurring in a term t is denoted Var(t). This notation extends naturally to other syntactic objects.

A substitution is defined as an almost identical mapping from the set of variables V into the set of terms τ(Σ ∪ V ).

Let θ be a substitution and let W ⊆ V be a set of variables. We define the restriction of θ to W by θ ↑_{W} (x) = xθ if x ∈ W , otherwise θ ↑_{W} (x) = x.

A substitution θ = {x_{1}/t_{1}, …, x_{n}/t_{n}} can be represented by a conjunction of equations θ̂ = (x_{1} = t_{1}, …, x_{n} = t_{n}), where x_{i} is a variable and t_{i} is a term over τ(Σ ∪ V ). θ̂ is called the equational representation of θ. The empty substitution is denoted by ϵ and its equational representation is ∅. The notions of application and composition are defined in the usual way [27, 33].

A sequence of terms t_{1}, …, t_{n} will be denoted by t̃. By considering the usual representation of a term by a labelled tree, the occurrences are sequences of integers denoting an access path in a term. O(t) and Ō(t) denote respectively the set of occurrences and non-variable occurrences of t. By t[u ← t′] we denote the replacement of the subterm of t at the occurrence u by the term t′. The definitions of occurrence sets, non-variable occurrence set, subterms and subterm replacement naturally extend to systems of equations [23].

A Σ-equation s = t is a pair of terms s and t (s, t ∈ τ(Σ∪V )). A Horn equational Σ-theory E is a finite set of equational Horn clauses of the form

l = r ⇐ e_{1}, …, e_{n}. with n ≥ 0 where e_{i} is an equation, 1 ≤ i ≤ n.

The Σ-equation in the head is implicitely oriented from left to right and the literals e_{i} in the body are ordinary non-oriented Σ-equations. A Σ-disequation is a formula s ≠ t where s, t are terms. The prefix Σ will be usually dropped when clear from the context.

Each Horn equational theory E generates a smallest congruence (=_{E}) over the set of terms τ(Σ ∪ V ). We will denote by H/E the finest partition τ(Σ)/_{=E} induced by E over the set of ground terms τ(Σ). A Horn equational theory E can be viewed as a conditional 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 unconditional, otherwise they are conditional. The equational theory E is said to be canonical if the binary one-step rewriting relation →_{R} defined by R is noetherian and confluent. Confluence can be ensured by syntactical characterizations [8, 28, 32]. We now recall the concept of E-unification, i.e. the problem of existence of a common instance of two terms under an equational theory E.

Let t = s be an equation. A substitution σ is called an E-unifier of t = s iff E ⊧ tσ = sσ, or equivalenty, tσ =_{E} sσ. In this case, t and s are said E-unifiable.

An E-unification algorithm defines a procedure to solve an equation t = s within the theory E. A solution is represented by an E-unifier. An E-unification algorithm is complete if it generates a complete set of E-unifiers for all E-unifiable input terms. Complete unification algorithms are known for various theories. Narrowing is a complete unification algorithm for unconditional canonical theories [15, 22] and conditional canonical theories satisfying different restrictions [20, 31]. [39] presents a classification of equational theories from the point of view of the universal unification.

Let E be a Horn equational theory. A function symbol f ∈ Σ is irreducible iff there is no clause (l = r ⇐ e_{1}, …, e_{n}) ∈ E such that l ∈ V or f occurs as the outermost function symbol in l. f is a defined function symbol if it is not irreducible.

In theories where the above distinction is made the signature Σ is partitioned as Σ = C ⨄ F , where C is the set of irreducible symbols and F is the set of defined function symbols.

Let E be a Horn equational theory and f be a defined function symbol. Then f is said to be completely defined (everywhere defined [9]) over its domain iff it does not occur in any ground term in normal form. E is said to be completely defined iff each defined function symbol is completely defined. In a completely defined theory the set of normal ground terms is the set of terms over C (τ(C )).

A completely defined Horn equational theory E will be called a Horn equational theory with constructors iff a further condition is satisfied: each equation in the left hand side of the head of any clause is of the form f (t_{1}, t_{2}, …, t_{n}) = t where f ∈ F and no defined symbols occur in any of t_{1}, …, t_{n}.

3 Normal Equational Theories

In the following we consider conjunctions of equations and disequations whose solvability will be checked with respect to a normal equational theory E^{∼}. Roughly speaking, a normal equational theory is an equational theory whose clauses may contain negation in their body. Formally:

Definition 1. A normal equational clause is a clause of the form

t = s ⇐ e_{1}, …, e_{m}, d_{1}, …, d_{n}. where the equation in the head is implicitely oriented from left to right, e_{1}, …, e_{m} are non-oriented equations, d_{1}, …, d_{n} are non-oriented disequations and m, n ≥ 0.

Definition 2. A normal equational theory E^{∼} is a finite set of normal equational clauses.

We notice that when the bodies of the clauses in the theory E^{∼} do not contain disequations then E^{∼} is a Horn equational theory.

Definition 3. A normal goal is a clause with no head.

Example 1. Let us consider a normal equational theory which defines the non-negative rational numbers represented as pairs of natural numbers [35]. /, +, ∗ are rational valued function symbols denoting division, addition and multiplication respectively, and +_{N}, ∗_{N} are the natural valued addition and multiplication functions.

E_{1}^{∼} = { 0/m = 0 ⇐ m ≠ 0.
m/c = n/d ⇐ m ∗_{N} d = c ∗_{N} n, c ≠ 0, d ≠ 0.
(m/c) + (n/d) = ((m ∗_{N} d) +_{N} (c ∗_{N} n))/(c ∗_{N} d).
(m/c) ∗ (n/d) = (m ∗_{N} n)/(c ∗_{N} d). }

A normal equational theory E^{∼} can be viewed as a conditional term rewriting system R where the rules are the heads and the conditions (containing disequations) are the respective bodies. The basis for the treatment of these rewriting systems is provided by [25]^{3}. In particular, he has proved that in the case of reducing P/N systems^{4} there exists a well-defined rewrite relation which can be constructed as a limit. Some properties of reducing P/N systems are also discussed in [25]. Thus, these systems are proved to be finitely terminating and the question of confluence is addressed by providing a complete critical pair criterion a la Knuth-Bendix. Another characterization of the confluence of normal equational theories can also be stated following [8, 34].

For the reasons we will state in the following section, throughout the paper we require normal equational theories to be theories with constructors.

4 Operational semantics

In this section we present our approach to solve normal goals in a normal equational theory E^{∼}. Our operational mechanism, Conditional N arrowing with Constructive N egation, is an adaptation of the innermost conditional narrowing algorithm to solve negated subgoals.

3 Such systems are called positive/negative systems (P/N systems) by Kaplan. 4 A P/N system R is called reducing if there exists a reduction ordering > such that if

t → s ⇐ B̃ ∈ R and σ is a substitution then tσ > sσ, uσ, vσ, u′σ, v′σ, for all u = v, u′ ≠ v′ in B̃.

4.1 Conditional Narrowing Calculus

Let us briefly recall the conditional narrowing algorithm. A goal is an expression of the form (g with θ) where g is a set of equations and θ is a substitution which is assumed to be restricted to the variables of the initial goal. To solve g the algorithm starts with the goal (g with ϵ) and tries to derive goals (recording applied substitution in the with-parts) until a terminal goal (Ø with θ) is rechead. Each substitution θ in a terminal goal is an E-unifier of g.

The children of a goal (g with θ) in a tree of narrowing (from now on, a search tree) for it are given by:

1. If g sintactically unifies with mgu σ then there is a unique child

Ø with θσ

2. Otherwise, if u ∈ Ō(g) then there is a child

(g[u ← r_{k}], B̃_{k})σ with θσ

for each clause

l_{k} = r_{k} ← B̃_{k}

from E such that σ = mgu(g/u, l_{k})^{5}.

Finally, we introduce our concept of frontier of a search tree which will be employed in the definition of the equational constructive negation rule.

Definition 4. [40] A frontier of a search tree for a goal G (or frontier of G) is the set of nodes at depth one in the search tree.

4.2 Equational Constructive Negation

We show that disequations in equational theories can be solved in a constructive way in equational theories, following a mechanism similar to that of [40], using a suitable conditional narrowing algorithm. This algorithm introduces negation and quantification in the constructed answer to a goal. The computed answer is a complex system involving elementary formulae. An elementary formula is either a (possibly quantified) equation (x = t or ˜∀ x = t) or a (possibly quantified) disequation (x ≠ t or ˜∀ x ≠ t) where x is a variable and t is a term distinct from x. A computed answer is a conjunction whose elements are elementary formulae or negated conjunctions of elementary formulae. Similarly, the goals involve throughout a computation a form which also includes negation and quantification. We extend the syntax of goals as follows:

Definition 5. An extended subgoal is recursively defined as either

– an equation,

5 The variables in g and in the clauses are assumed to be disjoint.

– or ∼ ∃Z̃(g_{1}, …, g_{n}□E), where every g_{i}, i = 1, … n, is an extended subgoal, E is a complex system involving elementary formulae and Z̃ denotes some variables in (g_{1}, …, g_{n}□E). Notice that (g_{1}, …, g_{n}□E) is shorthand for (g_{1} ∧…∧g_{n} ∧E).

The extended subgoals of the form ∼ ∃Z̃(g_{1}, …, g_{n}□E) are referred to as negated subgoals. The rest of the subgoals, the equations, are called non-negated subgoals. We define the complementary subgoal for a negated subgoal ∼ ∃Z̃(g_{1}, …, g_{n}□E) as (g_{1}, …, g_{n}□E).

A remark concerning the choice of the notation: as in constraint logic programming, we use the □ symbol in the extended subgoals since the system E will act as a constraint in our computational mechanism.

Definition 6. An extended goal is a conjunction of extended subgoals.

It is obvious to extend the syntax of a normal equational theory with bodies that are conjunctions of extended subgoals since a disequation, t ≠ s, can be expressed as the extended subgoal ∼ (t = s□∅). Similarly, a goal g can be shown as an extended goal g′ where each disequation, t ≠ s, of g has the form ∼ (t = s□∅) in g′.

The conditional narrowing algorithm can be modified to solve negated subgoals in a constructive way. Roughly speaking, when a negated subgoal is selected to be solved, a sub-derivation for the complementary subgoal is invoked. Then the first level of the search tree is considered. The substitution applied in each derivation step (represented as a system of equations) is added to the node of this branch as a constraint. Thus, we consider the nodes of the search tree containing a part which represents the subgoals yet to be solved and another one (the constraint) which represents a partial answer to the goal. Then, we define the search tree at depth one of the negated subgoal as a suitable transformation of these nodes. In what follows, g□E denotes a node of the search tree, where g is an extended goal and E is a partial answer of the initial goal. To solve a goal g_{0}, the algorithm starts with the extended goal g_{0}□Ø. We will often represent the set of nodes of a search tree as a disjunction. We will use E · E′ to denote the conjunction of the systems E and E′.

Let us define the constructive negation algorithm to solve negated subgoals with respect to normal equational theories.

Definition 7. Equational Constructive Negation Rule Let s ≡∼ ∃Z̃(g□E) be a selected negated subgoal to be solved. Then the frontier of the search tree for s is defined as follows:

– If g only contains equations, has no narrowable occurrences and does not syntactically unify, then the frontier of the search tree for s is empty.

– If g only contains equations, has no narrowable occurrences and syntactically unifies with mgu σ then the frontier of the search tree for s has as node (Ø□∀Z̃ ∼ E · σ̂) if ∼ ∃Z̃ E · σ̂ is solvable.

– Otherwise, let (g_{1}□E · θ̂_{1}), …, (g_{m}□E · θ̂_{m}) be the frontier of the search tree for g□E, where every g_{i} is an extended goal and θ_{i} is the substitution applied in the reduction from g to g_{i}. Consider the disjunction:

∃Z̃, Ỹ_{1}(g_{1}□E_{1}) ∨ … ∨ ∃Z̃, Ỹ_{m}(g_{m}□E_{m})

where E_{i} is E · θ̂_{i} and Ỹ_{i}, 1 ≤ i ≤ m, denotes the variables in (g_{i}□E_{i}) which do not appear in (g□E). Then apply the following rules [40]:

1. \underline{Negation of the disjunction}. Apply the following De Morgan law:

∼ ⋁_{j =1}^{m} ∃ Z̃, Ỹ_{j} (g_{j} □E_{j} ) = ⋀_{j =1}^{m} ∼ ∃ Z̃, Ỹ_{j} (g_{j} □E_{j} )

2. \underline{Transformation of each conjunction}. Then, apply the rule of decomposition:

∼ ∃ Z̃, Ỹ_{k} (g_{k}□E_{k}) ↔ (Ø□∀ Z̃, Ỹ_{k} ∼ E_{k}) ∨ (∼ ∃ Z̃, Ỹ_{k} (g_{k}□E_{k}))

Finally, take the disjunctive normal form of the formulae resulting from (2).

The general form of each node of the frontier of the search tree for a negated subgoal ∼ ∃Z̃(g□E), obtained applying the equational constructive negation rule to the frontier {g_{1}□E_{1}, …, g_{m}□E_{m}} of its complementary subgoal, is a conjunction of extended subgoals yet to be solved. In the first node of this frontier, Ø□∀Z̃, Ỹ_{1} ∼ E_{1} · · · . . . · · · ∀Z̃, Ỹ_{m} ∼ E_{m}, the conjunction of subgoals to be solved is empty. Therefore, if the system ∀Z̃, Ỹ_{1} ∼ E_{1} · · · . . . · · · ∀Z̃, Ỹ_{m} ∼ E_{m} is solvable then this system is an answer for the negated subgoal. Indeed, for each application of the equational constructive negation rule, the system in the first node of this frontier is a possible answer to the negated subgoal. Thus, if a negated subgoal has a solution, then it is always found in a finite number of derivation steps. The other nodes of the frontier contain subgoals to be solved and (in their □ part) information about the answers to the negated subgoal. Figure 1 shows the relationship between the frontiers of the search trees of a negated subgoal,∼ ∃ Z̃, Ỹ g□E, and its complementary one, g□E, for the particular case m = 2. For the sake of readability, we use the concise notation ˜∃subgoal and ˜∀subgoal instead of the more precise ∃Z̃, Ỹ subgoal and ∀Z̃, Ỹ subgoal.

The transformation applied in the definition of the frontier of the search tree for a negated subgoal from the frontier of the search tree for its complementary subgoal introduces negation and quantification in the answer system. We are only interested in answer systems whose equations and disequations only involve variables and constructors terms, because answers with this form can be thought of as systems of syntactic equations and disequations whose solvability can be checked using well-known algorithms (such as [30]). If the narrowing algorithm uses a strategy which selects only innermost redexes and we restrict us to equational theories with constructors any answer is a system which satisfies the above requirement.^{6}

Let us define the operational mechanism to solve extended goals wrt normal equational theories.

6 Fribourg ([16]) has shown that for canonical Horn equational theories with constructors and using an innermost conditional narrowing algorithm, any computed answer is a substitution involving only terms formed solely from constructors and variables.

[figure: θ_{2}; θ_{1}; g_{2}□ \underbrace{E · θ̂_{2}}_{E_{2}}; g_{1}□ \underbrace{E · θ̂_{1}}_{E_{1}}; g□E]

[figure: ∼ ˜∃(g_{1}□E_{1}),; ∼ ˜∃(g_{2}□E_{2})□∅; ∼ ˜∃(g_{2}□E_{2})□; ˜∀ ∼ E_{1}; ∼ ˜∃(g_{1}□E_{1})□; ˜∀ ∼ E_{2}; ∅□˜∀ ∼ E_{1} · ˜∀ ∼ E_{2}; ∼ ˜∃(g□E)]

Fig. 1. Relationship between a negated subgoal and its complementary subgoal.

Definition 8. Operational mechanism solving extended goals. Given a goal (g□E) where g = g_{1}, …, g_{n} is an extended goal, and g_{j} a selected extended subgoal of g to be solved, the frontier of (g□E) is given by:

– If g_{j} is a negated subgoal, then the equational constructive negation rule is applied. If the search tree for g_{j} is empty then the unique node of the frontier of (g□E) is

g_{1}, …, g_{j −1}, g_{j +1}, …, g_{n}□E

Otherwise, if (⋁_{i=1}^{p} f_{i}□E_{i}) represents the frontier of g_{j} , then the disjunction ⋁_{i=1}^{p} g′_{i}□E · E_{i} represents the frontier of (g□E), where g′_{i} is the extended goal obtained replacing g_{j} by f_{i} in g.

– If g_{j} is an equation, then the frontier of (g□E) is given by the innermost conditional narrowing algorithm.

Example 2. Consider the following normal equational theory which defines the sum of natural numbers:

E^{∼} = { 0 + y = y.
s(x) + y = s(x + y). }

and the normal goal c ≡ x + y ≠ 0, represented by ∼ (x + y = 0□Ø). The algorithm starts with the goal g_{0} ≡∼ (x + y = 0□Ø)□Ø.

The sub-derivation for the complementary subgoal of ∼ (x + y = 0□Ø), has two nodes at depth one of the search tree

{(y = 0□x = 0), (s(x′ + y) = 0□x = s(x′))}.

The application of the equational constructive negation rule gives the following frontier of the search tree of the negated subgoal ∼ (x + y = 0□Ø):

(Ø□x ≠ 0 · ∀x′ x ≠ s(x′)) ∨
( ∼ (y = 0□x = 0)□∀x′ x ≠ s(x′)) ∨
( ∼ ∃x′(s(x′ + y) = 0□x = s(x′))□x ≠ 0 ) ∨
( ∼ (y = 0□x = 0), ∼ ∃x′(s(x′ + y) = 0□x = s(x′))□Ø)

The search tree at depth one for g_{0} coincides with the frontier of the search tree of the negated subgoal ∼ (x + y = 0□Ø), where the first node is pruned since the system x ≠ 0, ∀x′ x ≠ s(x′) is not solvable in the Herbrand universe over the signature of the natural numbers. Thus, the three nodes of the search tree for g_{0} at depth one are

(i) ∼ (y = 0□x = 0)□∀x′ x ≠ s(x′)
(ii) ∼ ∃x′(s(x′ + y) = 0□x = s(x′))□x ≠ 0
(iii) ∼ (y = 0□x = 0), ∼ ∃x′(s(x′ + y) = 0□x = s(x′))□Ø

The next derivation step for the first node has ∼ (y = 0□x = 0) as goal to be solved. Its search tree has a unique node Ø□ ∼ (x = 0, y = 0) since in the complementary subgoal, y = 0□x = 0, the equation y = 0 has no narrowable occurrences and syntactically unifies with mgu σ = {y/0}.

Hence, the node of the search tree of the selected goal (i) is

(i.1) Ø□∀x′ x ≠ s(x′)· ∼ (x = 0, y = 0)

whose system of equations and disequations is the first answer to x + y ≠ 0. Let us notice that this system represents an infinite set of solutions of the form x = 0, y = s(n) where n ∈ N .

4.3 Conditional N arrowing with Constructive N egation

In this section we present an innermost (conditional) narrowing algorithm to solve normal goals, which handles the negative subgoals following the approach presented in section 4.2. The algorithm is presented as a transition system, called Innermost Conditional N arrowing with constructive negation (ICN cn), following the structural operational semantic approach introduced by Plotkin [36].

Definition 9. An ICN cn-state is a tuple ⟨S, L⟩, where S is a list of systems involving elementary formulae and L is a (possibly empty) list of narrowing goals g□E where g is an extended goal and E is a complex system which represents a partial solution of the initial goal.

The first component of an ICN cn-state represents the list of answers for the initial goal and the second component represents the list of the nodes of the search tree yet to be narrowed. This list is treated as a queue to emulate a breadth-first strategy.

Definition 10. Initial ICN cn-state.

Let g be a goal. Then ⟨Ø, g□Ø⟩ is an initial ICN cn-state.

Definition 11. Terminal ICN cn-states.

A terminal ICN cn-state is a state of the form ⟨S, L⟩ where S is non-empty.

Roughly speaking, in order to solve an extended goal g, the algorithm selects an extended subgoal of g. If a non-negated subgoal is selected, then standard narrowing is performed at one innermost occurrence and the resulting list of the nodes of the search tree is added to the current list of goals. If the selected subgoal is a negated subgoal then the equational constructive negation rule is applied to obtain its frontier which is represented as a list. Then, each element in this list replaces the selected negated subgoal in the actual goal, resulting in the new goals. The list of these goals is then added to the current list of goals. Finally, when a terminal state ⟨S, L⟩ is achieved, each system E of the list S is an answer for g. The ICN cn calculus is defined by means of a stratified transition system. →_{E CN} formalizes the rules for constructive negation. →_{f} is built over →_{E CN} and formalizes the rules for the selection of subgoals and expansion of the frontier of the search tree. →_{ICNcn} is built over →_{f} , controls the expansion of the search tree (by means of →_{f} , rule (9)) and returns the answers for the initial subgoal. Formally:

Definition 12. ICN cn transition relation^{7}.

Unification Rules for Constructive Negation

7 We assume that in the following rules g is non-empty

(1) \frac{g only contains equations and syntactically unifies with mgu σ ∧ solvable(∼ ∃Z̃ E · σ̂)}{∼ ∃ Z̃ (g□E) →_{E CN} [Ø□∀Z̃ ∼ (E · σ̂)]}

(2) \frac{g only contains equations and syntactically unifies with mgu σ ∧ ∼ solvable(∼ ∃Z̃ E · σ̂)}{∼ ∃ Z̃ (g□E) →_{E CN} [Ø□false]}

Constructive Negation Rules

(3) \frac{⟨g□E⟩ →_{f} L ∧ e c n(L, ∼ ∃ Z̃ (g□E)) = L′}{∼ ∃ Z̃ (g□E) →_{E CN} L′}

(4) \frac{(1), (2) and (3) do not apply}{∼ ∃ Z̃ (g□E) →_{E CN} [ ]}

Frontier expansion Rules

(5) \frac{e ∈ g ∧ u ∈ Inner(e) ∧ s to l(\{⟨i, σ⟩ : narred(e, u, i, σ)\}) = [⟨i_{j} , σ_{j} ⟩]n_{j =1}}{⟨g□E⟩ →_{f} [(g \ \{e\} ∪ \{e[u ← r_{ij} ]\} ∪ B̃_{ij} )σ_{j} □E · σ̂_{j} ]n_{j =1}}

(6) \frac{∼ ∃ Z̃ (g′□E′) ∈ g ∧ ∼ ∃ Z̃ (g′□E′) →_{E CN} [gi^{′}□Ei^{′}]n_{i=0}}{⟨g□E⟩ →_{f} [g \ \{∼ ∃ Z̃ (g′□E′)\} ∪ \{gi^{′}\}□E · Ei^{′}]n_{i=0}}

(7) \frac{∼ ∃ Z̃ (g′□E′) ∈ g ∧ ∼ ∃ Z̃ (g′□E′) →_{E CN} [Ø□false]}{⟨g□E⟩ →_{f} [ ]}

Unification Rule for Equations

(8) \frac{g only contains equations and syntactically unifies with mgu σ ∧ solvable(E · σ̂)}{⟨S, (g□E) • L⟩ →_{ICN Ccn} ⟨E · σ̂ • S, L⟩}

Narrowing Rules

(9) \frac{⟨g□E⟩ →_{f} L′}{⟨S, (g□E) • L⟩ →_{ICN Ccn} ⟨S, L ∘ L′⟩}
(10) \frac{(6) and (7) do not apply}{⟨S, (g□E) • L⟩ →_{ICN Ccn} ⟨S, L⟩}

where:

1. Inner(e) is the set of innermost non-variable occurrences of e.

2. narred(e, u, i, σ) ⇔ ( u ∈ Ō(e) ∧ (l_{i} = r_{i} ⇐ B̃_{i}) ∈ E^{∼} ∧ σ = mgu(e/u, l_{i}) ), where e is an equation.

3. solvable(E) is true if E is a solvable system involving elementary formulae. As we have mentioned in Section 4.2 there exist known algorithms [30] checking the solvability of these systems.

4. e c n(L, g) transforms the list L which represents the frontier of the search tree for the complementary subgoal of g into another list which represents the frontier of the search tree for g, following the process described in the equational constructive negation rule (Definition 7).

5. • (front and rear of a list), ∘ (concatenation of two lists) and s to l (list of elements of a set) are defined as usual.

5 Completion of Normal Equational Theories

One way to reason about negative information is by introducing the concept of completion [12]. In this section we define the completion of a normal equational theory which involves adding to the theory the only if halves of the definitions of the function symbols^{8} together with an equality theory.

Definition 13. Completed definition of function symbol

Let E^{∼} be a normal equational theory. Consider the following sequence of transformation on the set of clauses in E^{∼}. Let

f (t_{1}, …, t_{n}) = t ⇐ B̃.

be any theory clause in E^{∼}. We transform this clause into

f (x_{1}, …, x_{n}) = w ⇐ ∃ y_{1}, …, y_{k} ( (x_{1} = t_{1}) ∧ … ∧ (x_{n} = t_{n}) ∧ (w = t) ∧ B̃ )

where y_{1}, …, y_{k} are the variables of the original clause, and x_{1}, …, x_{n}, w are distinct variables that do not appear anywhere in E^{∼}. Now all formulas obtained in the previous step with a function symbol f on the left-hand side of the head

f (x_{1}, …, x_{n}) = w ⇐ F_{1}
⋮
f (x_{1}, …, x_{n}) = w ⇐ F_{m}

are replaced by

f (x_{1}, …, x_{n}) = w ⇐ F_{1} ∨ … ∨ F_{m}

The completed definition of f is then the formula

∀ x_{1}, …, x_{n}, w (f (x_{1}, …, x_{n}) = w ⇔ F_{1} ∨ … ∨ F_{m})

Example 3. The completed definition of the function symbol + from Example 2 is

∀ x_{1}, x_{2}, w (+(x_{1}, x_{2}) = w ⇔ ∃ x, y ((x_{1} = 0) ∧ (x_{2} = y) ∧ (w = y)) ∨

∃ x, y ((x_{1} = s(x)) ∧ (x_{2} = y) ∧ (w = s(+(x, y)))))

We now define the completion of a normal equational theory.

Definition 14. Let E^{∼} be a normal equational theory. The completion of E^{∼}, denoted by comp(E^{∼}), is the collection of completed definitions of function symbols in E^{∼} together with the Clark’s equality theory (CET ) where the freeness axioms are defined over irreducible function symbols.

8 If f (t_{1}, …, t_{n}) = r ⇐ B̃. is a clause in an equational theory, then f is called the name of the clause. The set of all clauses with the same name f is called the definition of f .

The model theoretic semantics of a normal equational theory E^{∼} is based on considering models of comp(E^{∼}) rather than models of E^{∼} itself. Hence, the concept of a correct answer is defined as follows:

Definition 15. Correct answer

Let E^{∼} be a normal equational theory, g a goal and E an answer system for g with respect to E^{∼}. We say E is a correct answer for g with respect to comp(E^{∼}) if for all substitution θ such that CET ⊧ Eθ then gθ is a logical consequence of comp(E^{∼}).

The completion will play an important part in the soundness results for the equational constructive negation.

6 Stratified Equational Theories

Hölldobler has developed a model theory for equational theories giving a fixpoint characterization ([20]). He shows that the least fixpoint of the operator T defined as a mapping between interpretations is the least Herbrand E-model^{9} of the theory. However, this result can not be generalized to normal equational theories since the operator T does not need to be monotonic in presence of negation. It has been shown ([25]) that normal equational theories may have minimal models but no least model. Still, only one of these minimal models correspond to the intended meaning of the theory^{10}.

On the other hand, even if every normal equational theory is consistent, its completion may not be consistent. Let suppose, e.g, the following normal equational theory: E^{∼} : a = b ⇐ a ≠ b, which is inconsistent since (a = b ⇔ a ≠ b) is a formula of comp(E^{∼}).

For this reason we introduce some syntactic restrictions on the theory. Similarly to logic programming [3, 4], we propose a treatment of negation which is based on the restriction of normal equational theories to be stratified. Informally, first some function symbols should be defined in terms of themselves without the use of negation and, next, some new function symbols can be defined in terms of themselves without the use of negation and in terms of the previous function symbols, possibly with the use of negation. Note that, with these restrictions, recursion by negation is not allowed. The theory E^{∼} in the above example does not satisfy these conditions, hence it is not stratified.

Definition 16. Stratified equational theories A normal equational theory E^{∼} is called stratified if there exists a partition

E^{∼} = E_{1}^{∼} ˙∪ … ˙∪ E_{n}^{∼}

9 In this context, the Herbrand base of an equational theory is the set of ground equations that can be build from the elements of the Herbrand universe. An interpretation is a subset of the Herbrand base and an E-interpretation is an interpretation which obeys the axioms of equality.

10 This coincides with to the concept of supported model in logic programming ([3, 4]).

such that for every instance of the clauses of E^{∼}, the following two conditions hold for i = 1, …, n:

1. If a defined function symbol occurs in the head of a clause in E_{i}^{∼} (except those that E_{i}^{∼} defines) or in an equation in the body of a clause in E_{i}^{∼}, then the definition of this function symbol is contained within ⋃_{j ≤i} E_{j}^{∼}.

2. If a defined function symbol occurs in a disequation in the body of a clause in E_{i}^{∼}, then the definition of this function symbol is contained within ⋃_{j <i} E_{j}^{∼}.

We say that E^{∼} is stratified by E_{1}^{∼} ˙∪ … ˙∪E_{n}^{∼} and each E_{i}^{∼} is called an equational stratum of E^{∼}. An equational stratum defines new function symbols in terms of themselves (positively) and in terms of the function symbols from the previous strata (possibly negatively).

Example 4. Let E^{∼} be the following normal equational theory:

r = a.
q = b ⇐ r ≠ b.
p = a ⇐ q ≠ a.

Then E^{∼} is stratified by E^{∼} = {r = a.} ∪ {q = b ⇐ r ≠ b.} ∪ {p = a ⇐ q ≠ a.}.

Example 5. The following normal equational theory is not stratified:

f (x) = a ⇐ x ≠ a.

because there exists instances of this clause, for instance f (f (a)) = a ⇐ f (a) ≠ a, that do not satisfy condition 2.

Since we consider stratified equational theories we give a standard fixpoint characterization of them following the fixpoint theory of non-monotonic operators which is described in [3, 4] for logic programming with negation.

Definition 17. Given a normal equational theory E^{∼} stratified by E^{∼} = E_{1}^{∼} ˙∪ … ˙∪E_{n}^{∼} we define a sequence of Herbrand E-interpretations by putting

M_{1} = T_{E_{1}^{∼}} ⇑ ω(∅) M_{2} = T_{E_{2}^{∼}} ⇑ ω(M_{1})

⋮

M_{n} = T_{En^{∼}} ⇑ ω(M_{n−1})

where clearly M_{1} ⊆ M_{2} ⊆ ⋯ ⊆ M_{n}.

Let M_{E^{∼}} = M_{n}. The following theorem establishes the main result of this section.

Theorem 18. Let E^{∼} be a canonical normal equational theory stratified by E^{∼} = E_{1}^{∼} ˙∪ ⋯ ˙∪ E_{n}^{∼}. Then

1. M_{E^{∼}} is a Herbrand E-model of E^{∼}.

2. M_{E^{∼}} is a minimal Herbrand E-model of E^{∼}.

3. M_{E^{∼}} is a Herbrand E-model of comp(E^{∼}).

The proof of this theorem can be found in the appendix.

7 Soundness

In this section we give the soundness results of our equational constructive negation rule with respect to the completed program. Let us recall that the systems in the leaves of the search tree have a form which allows to test their solvability in CET .

First, we show that a canonical normal equational theory is a logical consequence of its completion. The proof can be found in the appendix.

Proposition 19. Let E^{∼} be a canonical normal equational theory. Then E^{∼} is a logical consequence of comp(E^{∼}).

To state the soundness results we need the following lemmata.

Lemma 20. If E is a canonical Horn equational theory with constructors and {G_{1}, …, G_{n}} is a frontier of a goal G then

comp(E) ⊧ G ⟷ (∃ Y_{1} G_{1}) ∨ … ∨ (∃ Y_{n} G_{n})

where Y_{i} is the set of variables in G_{i} not in G.

Proof. The lemma follows straightforwardly from proposition 19 and from the fact that if {G_{1}, …, G_{n}} is a frontier for G then every derivation for G passes through one frontier node since the operational mechanism which is used to build the search tree is correct and complete ([17]).

Lemma 21. If E^{∼} is a canonical stratified normal equational theory with constructors, G is a goal and {G_{1}, …, G_{n}} is a frontier of G then

comp(E^{∼}) ⊧ G ⟷ (∃ Y_{1} G_{1}) ∨ … ∨ (∃ Y_{n} G_{n})

where Y_{i} is the set of variables in G_{i} not in G.

Proof. We prove the lemma by induction on the number of call to negative subderivations. In the base case, the selected subgoal of G is an equation and E^{∼} is a canonical Horn equational theory with constructors, then the lemma holds by lemma 20. For the induction step, the interesting case is if the selected subgoal of G is a negated subgoal ∼ ∃ Z̃ (g□E), then by the induction hypothesis the frontier {(g_{1}□E_{1}), …, (g_{n}□E_{n})} for the derivation of (g□E) is such that

comp(E^{∼}) ⊧ g□E ⟷ ∃ Y_{1} (g_{1}□E_{1}) ∨ … ∨ ∃ Y_{n} (g_{n}□E_{n})

Now, if F_{1}, …, F_{p} are the goals returned after negating the frontier, we have

comp(E^{∼}) ⊧∼ ∃ Z̃ (g□E) ⟷ F_{1} ∨ … ∨ F_{p}

Thus, every goal G is equivalent to the disjunction of its immediate children. So that, in the general case the lemma holds by building the frontier iteratively.

Theorem 22. Soundness

Let E^{∼} be a canonical stratified normal equational theory with constructors and g a normal goal. If ⟨[], [g□Ø]⟩ →_{ICN Ccn} ⟨S, L⟩ then every system E_{i} in S is a correct answer for g.

Proof. If ⟨[], [g□Ø]⟩ →_{ICN Ccn} ⟨S, L⟩ then there exists a system E_{i} ∈ S and a node in the search tree for g□Ø with frontier {g′_{1}, …, g′_{p}} such that g′_{j} is of the form Ø□E_{i}. Then by lemma 21

comp(E^{∼}) ⊧ g□Ø ⟷ ∃ Y_{1} g′_{1} ∨ … ∨ ∃ Y_{j} (Ø□E_{i}) ∨ … ∨ ∃ Y_{p} g′_{p}

Now, since E_{i} ∈ S then E_{i} is solvable. Thus, for all substitution θ such that CET ⊧ ∃ Y_{j} E_{i}θ the above disjuntion is true. Hence, comp(E^{∼}) ⊧ (g□Ø)θ.

Clearly then each computed answer E_{i} ∈ S is a correct answer for g□Ø.

8 Conclusion and further research

We have presented an algorithm based on constructive negation which extends narrowing to deal with systems of equations and disequations. We have then defined the notions of completion and stratified equational theories and have proved the soundness of the operational semantics with respect to the completion of a canonical stratified normal theory with constructors. We are currently investigating the completeness of our computation rule and how to use the extended narrower as a kernel for a language which integrates equational and logic programming as an instance of the Constraint Logic Programming Scheme [1, 2, 24].

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, Dipartimento di Informatica, Università di Pisa, 1991. submitted for publication.

3. K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

4. K. R. Apt, H. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–148. Morgan Kaufmann, Los Altos, Ca., 1988.

5. L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In E. Y. Shapiro, editor, Proc. 10th Int’l Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 427–441, 1990.

6. L. Bachmair and H. Ganzinger. Perfect Model Semantics for Logic Programs with Equality. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 645–659. The MIT Press, Cambridge, Mass., 1991.

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

8. J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.

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

10. D. Chan. Constructive Negation Based on the Completed Database. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 111– 125. The MIT Press, Cambridge, Mass., 1988.

11. D. Chan. An Extension of Constructive Negation and its Application in Coroutining. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 477–493. The MIT Press, Cambridge, Mass., 1989.

12. K.L. Clark. Negation as Failure. In H. Gallaire and J. Minker, editors, Logic and data bases. Plenum Press, New York, 1978.

13. A. Colmerauer. Equations and Inequations on Finite and Infinite Trees. In Proc. Int’l Conf. on Fifth Generation Computer Systems, pages 85–99. ICOT, Tokio, 1984.

14. 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.

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

16. M. Fitting. A Kripke-Kleene semantics for logic programs. In Journal of Logic Programming, volume 2, pages 295–312, 1985.

17. 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.

18. E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42, 1991.

19. 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.

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

21. G. Huet and D.C. Oppen. Equations and Rewrite Rules: a Survey. In Formal Languages: perspectives and open problems, pages 349–405. Academic Press, 1980.

22. 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.

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

24. 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.

25. S. Kaplan. Positive/negative conditional rewriting. In S.Kaplan and J.-P. Jouannaud, editors, Conditional Tern Rewriting Systems, volume 308 of Lecture Notes in Computer Science, pages 129–143. Springer-Verlag, Berlin, 1987.

26. K. Kunen. Negation in logic programming. Journal of Logic Programming, 4:289–308, 1987.

27. 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.

28. G. Levi, C. Palamidessi, P.G. Bosco, E. Giovannetti, and C. Moiso. A complete semantics caracterization of K-LEAF, a logic language with partial functions. In Proc. Second IEEE Symp. on Logic In Computer Science, pages 318–327. IEEE Computer Society Press, 1987.

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

30. 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.

31. A. Middeldorp and E. Hamoen. Counterexamples to Completeness Results for Basic Narrowing. Technical report, Centre for Mathematics and Computer Science, Amsterdam, 1991. in preparation.

32. 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.

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

34. M. O’Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1977.

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

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

37. T. Przymusinski. On the Declarative Semantics of Deductive Databases and Logic Programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193–216. Morgan Kaufmann, Los Altos, Ca., 1988.

38. T. Przymusinski. On the Declarative and Procedural Semantics of Logic Programs. Journal of Automated Reasoning, 5(2):201–228, 1989.

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

40. P. J. Stuckey. Constructive Negation for Constraint Logic Programming. In Proc. Sixth IEEE Symp. on Logic In Computer Science. IEEE Computer Society Press, 1991.

This article was processed using the LaTEX macro package with LLNCS style