Completeness of the Negation as Failure Rule

CO~L~ENESS OF TffE NEGATION AS FAILURE RULg

JoXB.n Jaffar*, Jean-Louis Lassez'¥ and John Lloyd#

¥ * [)ept . of Computer Science, t.1onash University , Clayton , Victoria. Dept . of Computer Science, University of ~elbourne, Parkville, Victoria .

A.BSTRA.CT

Let P be a Horn clause logic program and comp(P) be its completion in the sense of Clark . Clark gave a justification for the negation as failure rule by sho'.;ing that if a ground a tom A. is in the finite failure set of P, then - A. is a logic9.l consequence of comp( P) , th9. t is , the neg9.tion as failure rule is sound. We prove he re that the converse also holds, that is, the negation as failure rule is compl ete .

I INTRODUCriON

If P is a Horn clause logic program, then we c9.n use P to deduce "positive" information . In other words, if A. is a ground atom, then the interpreter, by using SLD- resolution, can attempt to prove that A. is indeed a logical consequence of P. However, we cannot deduce "negative" information using SLD-resolution . To be precise, we cannot prove that - A. is a logical consequence of P. The reason is that PU(A.j is satisfiable, ho!Ving the Her-brand base as a

model.

To r emedy this defect, logic programming interpreters are usually augmented by the negation as failure rule . This rule states that if A. is in the finite failure set of P, then -A. holds . Thus we interpret the failure of the attempt to prove A. as a "proof" that -A. holds . Rules very similar to the negation as failure rule have previously been widely used in arti ficial intelligence systems (for example, PLANNER, various non-monotonic logics) .

This research was partially supported by a grant from the Australian Computer Research Board .

'While the negation as failure rule is intuitively appeal ing , it is preferable to find some firm theoretical foundation for it . In particular, we would like - A. to be a logical consequence of something connected with P. Cla rk [2] showed that the "something" is the completion of P , denoted by comp(P) , which is essentially P toge ther with the only- if halves of each of its cl auses , plus some axioms to constrain the equality predicate. Cl ark showed that if A. is in the finit e fai lure set of P , then -A. is a l ogical consequence of comp(P) . This amount s to a soundness proof of the negation as failure rule . (We note that Clar k proves this r esult for a more general class of logic programs, ones where liter als in a clause body may be negated . For this c lass, the converse of his r esult is false).

In this paper , we give the corr esponding completeness proof of the rul e , that is, we show that if - A. is a logical consequence of comp(P),

then A. is in the finite failure set of P.

In the next sect i on, we discuss what is currently known about finite failure and put our theorem into that context . In the last section, we give the proof of the theorem.

II FINITE FAILURE AND THE COMPLETION OF ~ PROGRAM

Throughout this paper, P denotes a Horn clause logic program and B(P) the Herbrand base of P. A denotes an arbitrary element of B(P).

1 1/e make the usual identification between Herbrand interpretations for P and subsets of B(P) ([1].[5]) . Thus, for any Herbrand interpretation , the corresponding subset of the Herbrand base is the set of all ground a toms which are true in the interpretation . The set of all Herbrand interpretations of P is a complete lattice under the partial order of set inclusion . ~e define the usual mapping Tp from the lattice of Herbrand interpretations to itself as follows . interpretation. Then Let I be a Herbrand

A~B 1 , ... ,Bn is a ground instance of a clause in P and B 1 , .... , Bn e I l T is clearly monotonic. As in [1], we define p ou n Tpvw to be n~b(B(P)) ·

Next we define the finite failure set of P. The usual definition of finite failure ([1],[2]) is given in terms of finitely failed SLD trees. A gene ral definition of finite failure, independent of any implementation, is given in [4] and we adopt the same definition here.

Definition FFd' the set of atoms in B(P) which are finitely failed ~ depth i· is defined as follows:

• (a) AeFF 0 if A/!Tp(B(P)).
• (b) AeFFd' for d>O, if for each clause A'~B 1 , ..· ,Bn in P and for each substitution g such that A=A'Q and B 1 Q, .·· ,BnQ are groun~, there exists k such that 1 ~k~n and BkQeFFd_ 1 .

Definition The finite failure set FF of P is defined as follows: A e FF if there exists d such that A e FFd .

Next we . give the more usual definition of finite failure.

Definition The SLD ~ failure set of P

is the set of all A e B(P) for which there exists a finitely failed SLD tree which has ~A at the root .

Now in [1] the following theorem is proved (a much shorter proof of this result is given in [5]) : A is in the SLD finite failure set if and only if A I! 1' yw. However, it is easy to show p that FF = B(P)\1'pVW [4] and thus this result of [1 J can be considered as a form of soundness and completeness for an SLD implementation of finite failure. However, this is not quite satisfactory: SLD finit e failure only guarantees the existence of one finitely failed SLD tree - others may be infinite . The problem is to identify exactly those computation rules which guarantee to find a finitely failed SLD tree, if

one exists at all .

Definition A computation rule is a rule which selects the atom to be expanded in the current goal. A computation rule is fair if for every atom B in a derivation using this rule, either (some further instantiated version of) B is selected within a finite number of steps or (some further instantiated version of) B is in a failed goal. A fair SLD tree is an SLD tree obtained via a fair computation rule.

Then in [4] the following result is proved: A e FF iff, for every fair computation rule, the corresponding SLD tree with ~A at the root is finitely failed. Furthermore, the desirable strong form of completeness is obtained: all fair SLD trees are equivalent in the sense that if any one is finitely failed, all are.

Summarizing the results so far, we have:

Proposition 2.1 The following are

equivalent:

(a) A is in the finite failure set.

(b) A t TP yw ·

(c) There exists an SLD tree with ~A at the

root which is finitely failed.

(d) Every fair SLD tree with ~A at the root is finitely failed.

Naxt we give Clark 's definition of the completion of a program. Let p( t 1 , ... , tn) .._B 1 , ... , Bm be a cl ause in a program P. it{e ··ill require a new predicate =, whose intended interpretation is the equality relation. The first step is to transform the given clause into

p(x1 ' ... ,xn) .._ (x1 =t1) 1\ ... I\ (xn=tn) I\B11\ ... 1\Bm, where x 1 , ... ,xn are variables not appearing in the clause . Then, if y 1 , ... ,yd are the variables of the original clause, we transform this into

Now suppose this transformation is made for each clause which has the predicate p in the he3.d. Then we obtain k~1 transformed clauses of the form

where each Ei has the general form 3y1 ... 3yd ( (x1 =t1) 1\ ... I\ (xn=tn) I\B11\ .. . I\ Bm) . The completed definition of p is then the formula

However, if a predicate q in P does not appear in the head of any clause, the comple ted definition of q is

To prove his result, Clark needed the following equality axiom schemas:

1. cfd , for all pairs c,d of distinct constants. 2 . f(x 1 , . .. ,xn)fg(y 1 , ... ,ym), for all pairs f,g

of distinct functions. 3 . (x 1 f1 1 ) V ... V(xnfyn)~ f (x 1 , .. · ,xn)ff(y 1 , .. . ,yn), for each function f. 4. f( x 1 , ... , xn) fC, for each constant c and function f.

5. t[x]h, for each non-variable term t[x] containing x. 6. x=x.

7 · ( x1=y1)1\ ... l\(xn=yn)~ f(x1 ' .. . ,xn),;f(y1 ' ... ,yn)' for each function f. 8 · (x1=y1)1\ ... l\(xn=yn)~ (p(x , ... ,x )~p(y , .. . ,y )) , 1 n 1 n

for each predi cate p.

Definition The completion of ~. denote? comp(P), is the collection of the completed definitions for each predicate in P and the above equality axiom schemas .

The result of this paper is as follows:

Theo rem If -A is a logical consequence of comp(P), then A is in the finite failure set of P .

Using this theorem, proposition 2.1 and Cl ark 's theorem, we obtain the following result:

Theorem A is in the finite failure set of P iff -A is a logical consequence of comp(P) .

III PROOF OF THE THEOREM ------

This section contains a proof of our theorem. In fact, we prove the contrapositive of the result. Thus we assume that A is no~ in the finite failure set of P and prove that comp(P)U\A} has a model . Unfortunately, we cannot restrict attention to Herbrand models. It is easy to construct examples where A is not in the finite failure set and yet comp(P)U\A} has no Herbrand model. Indeed, this is the main difficulty of the proof - to find the right kind of model.

The first task is to generalize the mapping Tp introduced earlier . Let D be a fixed domain of interpretation for P and assume some fixed assignment of constarrts in P to elements of D and functions in P to functions on D. With all this fixed, we can now obtain a variety of interpretations for P by varying the assignments of the predicates of P. In fact, as for Herbrand interpretations, each such interpretation can be identified with some subset of "atoms" (where the predicate of each "a tom" is in P and each ar gument is in D). We simply make p(d 1 , .. . ,dn) true precisely when p(d 1 , ... ,d~) is in this subset.

As before, we can make a complete lattice out of the set of all such interpretations under the partial order of set inclusion. We also define a mapping , again denoted by Tp, from this lattice to itself as follows. Let I be such an

interpreta tion. Then

• 1'p(I) = (p(d 1 , ... ,dn) : B~B 1 , .. . ,Bn is a clause in P and there is some assignment of the variabl es in the clause to el ements of D such that with this assignment B is

It is easy to see that Tp is monotonic .

The following proposition, whose proof is strai ghtforward, is a major tool we employ in the proof of our theorem.

Proposition l·l Let I be an interpretation

of P, let the predicate = be assigned the identi ty relation on the domain of I and suppose the equality axioms 1 to 8 are satisfied. Then I is a fixpoint of Tp implies that I, together with = assigned the identity relation, is a model for comp(P) .

1'he domain D of our model, which we shall define later, will be a quot\ent of the set T of first order terms of P. We define T following Huet [3] . Let x 1 ,y 1 ,z 1 , ·.. ,x 2 ,y 2 ,z 2 , ... , ·.· constitute a denumerable set of variables V, where x,y,z, ... are the variables appearing in P. Let F denote the set of functions and constants ~n P. The set T is defined as the free F-algebra generated by V, that is, a term in T is either a variable in V or a constant in For is of the form f(t 1 , ... ,tn), for some n-ary function f € :r and some terms tie T, 1 ~i~n. We shall use the symbols s,t,u and v, possibly indexed, to denote terms.

* Let N denote the set of all finite lists of positive integers, 1\ the empty list and ·

the usual cons operator. Two lists i and a r e independent if neither one is a prefix of the other. For any te T, we define the set of * occurrences oft, OCC(t)CN, and , for any ieocc(t), the subterm of! at~. t/i, as follows:

• (a) If t is a vari able or a constant , then (i) OCC ( t) = ( 1\ ) and ( ii ) t/ 1\ = t .
• ( b) If t =f (t 1 , ... ,tn), then (i) OCC(t)=(l\) U (j .k : 1~j~n and keocc(tj)) and (ii) t/1\=t and t/j . k=t./k, for all j .keocc(t). J

Next, f or any s,teT and ieocc(s), we define the r eplacement of the subterm of ~ at ~ by l· s[ i~t ] , as follows:

(a) s[l\ ~t] =t.

To obtain our quotient of T, we now define certain binary relations upon T.

Definition A rewrite X: is of the form * <i,x,t>, where ieN I xev and teT. It defines a mapping from T into itself: given any s eT,

Two r ewrites <i, x,s> and <j ,y,t>, where x and y a r e not necessarily distinct, are independent if i and j are independent. A rewrite X: is superfluous for~ term t if tX:=t.

While a rewrite may closely resemble a substitution , it is important to not e that a r ewrite may alter at most ~ instance of any variable in any term . We shall use the symbols X: and Y, possibly indexed, to denote r ewrites .

Definition Having fixed a set R of rewrites on T,

• (a) s<nt if n is the smalles t integer l 0 such that sx: 1 x 2 · · ,x:n =t 1 for some x:i e R, 1 ~i~n. s<t if 3nl0 such that s< t. n
• (b) s"" t In if n is the smallest integer l 0 such that uX 1 ... X:k =s and uY 1 ... Ym=t, for some u e T, k+m=n and xi,Yje R, 1~i~k. 1~j~m. sit if 3nl0 such that · s1nt.
• (c) sy t if n is the smallest integer l 0 such
• n

that sX 1 .. . Xk = ty 1 .. . Ym, for some k+m=n and. xi,Yje R, 1~i~k, 1~j~m . s tt if 3n~O such that st t. n

The fo llo,·ing verified. proposition is easily

Proposition l·.?..

• (a) For any two distinct functions f and g and for any sequence of arguments u and v appropriate to f and g , r esp ., we have -(f( u)tg(v)) .
• (b) Fo r any n-ary function f, f (s 1 , ... ,s) t n m f(t 1 , ... ,tn) iff, for all i such that 1~i~n, we m 1 +m 2 + ... +mn=m. have s. t t.' ~ m. ~ ~ where
• (c) If X and Y are independent , then tXY=tYX .

We now have all t he tools needed for the proof of our

Theorem If l is not in the finit e failure set of P, then comp(P) U!l} has a model .

Proof By the results of section 2 , we have that any fair SLD t ree wi th root ~A is not finitely f ailed. Sel ect any non-failed branch BR in any such tree . Let � 0 =~A,� 1 ,G 2 , ... denote the goals in BRand let c 1 ,c 2 , ... denote the corresponding input clauses . We assume that the variables in P are no t indexed and that the variables in each C. are renamed so that each ~ has index i. Thus the sequence of mgu's 9 1 ,9 2 , ... , where Gi+ 1 is derived from Gi and Ci+ 1 using 9i+ 1 , are such that for any variable

x e v:

• (a) I f the bindings x/s and x/t appear in !9i}' then s=t.
• (b) For any sequence 9 of mgu's in !9i} such that xGrx , xG does not contain x.

In other words, for any variable x e V, (a) states that there is at ~ost one bind.ing for x and (b) states that once x has been substituted by any term t e T, no further substitutions upon t can result in a term containing x. We shall say that the substitutions !9 . J are univocal and ~ acyclic because of (a) and (b) , respectively.

We now define a set R of rewr ites based on the collection !9. }:

• ~ * R = !<i,x,t> : i eN and the binding x/ t appears in some 9j J.
• It is easy to see that, like the 9i' s , the rewrites in R are univocal and acyclic. That i s,
• (a) If <i ,x,s> and <j ,x,t> are in R, then s=t .
• (b) For any sequence X of rewrites in R such that xXrx, xX does not contain x.

The main r elationship between the substitutions !9. J and the r ewrites R which we ~ employ is this: if s9=t, for any t erms s and t and any sequence of substitutions 9 , then s<t.

We now show tha t t is an equivalence r elation on T. Tha:t it is r eflexive and symmetric is obvious. That it is transitive follows from the "Church-Rosser" property of <: sit implies stt. This i s proved as follows.

• s · t 1 m+n ' say ux 1 ... Xm=s and for some u e T. Proceeding by induction on m, we have
• (a) Basis : m~1 . The case m=O is obvious. Now suppose m=1. If x 1 is not equal to any Yi ' then x 1 is independent of all the Yi and , by n applications of proposition 3 . 2c , sY 1 ··'Yn=tX 1 and we are done . Otherwise , x 1 =Yj, for some j where 1~j~n . By j-1 applications of proposition 3 . 2c, we have that uY 1 ... Yj = uY .Y 1 .. . Y. 1 J JThus sY 1 ... Y. 1 Y. 1 · · · Y t · J- J+ n

( b) Induction step : m>1. and let s'=ux 1 ... xj. s'h, say Let j satisfy 1~j <m By the induction s' <v ' and t<v' . ( s ee hypothesis, Figure 1). Note that stv' Thus by again using the induction hypothesis, we have that stv ' , say s<v and v'<v. By the transitivity of <, we have t <v and we are done.

The transitivity oft can be easily seen to follow from the Church-Rosser property (see Figure 2) .

We now obtain the domain of our model by defining D to be T/t, the set of all t equivalence classes on T. Next we give the interpretation of the functions in P. Let [ t ] denote the v equivalence class of t. For each n-ary function f in P, we assign to f the function from Dn into D defined by ([s 1 ], ... , [ sn]) __;;. [f(s 1 , ... , sn)] . That this function is well-defined follows from proposition 3 . 2b.

~e assign each constant c in P to the e1uivalence class [c]. Note tha t if s and tare distinct ground terms, then [s] ~ [t ]. Thus D contains an isomorphic copy of the usual Herbrand universe . This completes the definition of the domain of the model and the assignment of the functions and constants . It remains to give the assignments of the predica tes. For this purpose, we are going to use the mapping Tp co rresponding to this particular domain and assignment of functions and constants.

First , recall the branch BR in the fair SLD tree for ~A. We construct a set 1 0 as follows: I 0 =(p([t 1 ], ... , [tn]):p(t 1 , ... ,tn) appears in BR}. Next we show that r 0 cTp(I 0 ). Let p([t 1 ] , ... , [ tn]) be any element in r 0 such that p(t 1 , ... ,tn) appears in some goal Gi ' U O. Because BR is from a fair SLD tree and BR is not failed , ther e exists j~O such that p(s1 , ... ,sn) p(t1 , ... ,tn) 11 i+1 11 i+2''' 11i+j appears in the goal Gi+j and p(s 1 , ... ,sn) is the selected atom in Gi+j' Suppose Ci+j+ 1 takes the form p(u 1 , .·· ,un)~B 1 , .·· ,Bm. By the definition of TP, p([ u 1 gi+j+ 1 ], ... , [ unl:li+j+ 1 ])eTp(I 0 ). Also, we note that by the abovementioned relationship between substitutions and rewrites and our

The last step in the definition our model is as follows: using the above result and the

------t Knaster-Tarski theorem about fixpoints for monotonic functions, there exists an 1 such that I 0 C I and I=Tp(I) . Thus A is true in I.

We assign to = the identity relation on D. According to proposition 3 .1, it only remains to check that equality axioms 1 to 8 are satisfied . Axioms 6 to 3 are obviously satisfied because = is assigned the identity relation. Axioms 1 and 4 a re satisfied because every rewrite is superfluous for constants. Axiom 2 is satisfied by proposition 3 . 2a and axiom 3 by proposition 3 . 2b . Only axiom 5 requires some effort . We prove this as follows.

Let s~t (set) denote that sis a (proper) subterm of t . 1 Ne now prove that for all k~O , sCt implies -(sykt). This is clearly true for k=O. For the induction step, we assume that the st3.tement is false, that is, svm+nt , say sX 1 ... Xm=tY 1 ... Yn=u , where m+n21, and obtain a contradiction . Let s=t/i 0 , for some i 0 f l\ .

Case 1: s is a variable, say x . Clearly, m~1. Thus x 1 must be of the form < 1\, x , r> and, because R is acyclic, u cannot contain x. Thus n~1 . Now since t<u, there exists some j , where 1~j~n and Yj is of the form <i 0 ,x,r>. Note tha t the last component in this rewrite must coincide with the last component in x 1 because R is univocal . By j-1 applications of proposition 3 .2c, we have that tY 1 ... Yj = tYjY 1 ... Yj_ 1 . Let s'=sX 1 and t'=tYj, so that s'x 2 ... xm t'Y 1 ... Yj_ 1 Yj+ 1 ... Yn. Noting that we have just shown that s' C t' and s 'vm+n- 2 t ' , we have the desired contradiction of our induction hypothesis .

Case 2 : s is not a variable . If s does not contain a variable, then clearly we are finished since all rewrites on s are superfluous. So we assume otherwise and we show that, for some term t' C t and some variable x appearing in both s and t ', xvit ', for some i~m+n. This will bring us back into case 1 .

We proceed by reducing the size (that is, the number of symbols) of s . Let s be of the form f(s 1 , ... ,sd), for some d21; by proposition 3 . 2a , t must t ake a "similar" form, say f(t 1 , ... ,td) . Since sCt, we have sCtj' for some j such that 1 ~j~d; thus s. Ct. and using J J proposition 3 . 2b , s.v . t., for some i~m+n. We J ~ J are now finished , since if s. is a variable we J are back in case 1 and , if otherwise, we apply the process again .

Thus axiom 5 is satisfied and the proof of the theorem is finished.