🚀 go-pugleaf

In article <11500020@hpldola.HP.COM>, patch@hpldola.HP.COM (Pat Chkoreff) writes:
> 
> Negation worries me.  A language feature should either be essential for
> computation, or defined in terms of something that is.  Negation is NOT
> essential for computation, so I HOPE that it can be defined in terms of pure
> Horn clauses, which are.  Is there an effective procedure for removing
> negation from a first-order logic program, resulting in a pure Horn clause
> program?  I wouldn't necessarily USE the procedure -- I just want to know if
> it exists.  If not, then something stinks.

There is a simple translation of negation to first order logic that requires
a correct implementation of not equals.  Given a predicate say p(X1,...) which
is called somewhere in the form not(p(Y1...)) then the call can be replaced
by a positive call np(Y1,...) where the definition of np can be derived
systematicly from that for p.
If p is defined as follows:

	p(X1,...) :- a11(...), ..... a1n1(....)
        p(X1,...) :- a21(...), ......a2n2(....)
	...
	p(X1,...) :- am1(...), ..... amnm(....)

then np is defined as

	np(X1,...):- not(a11(...)), not(a21(...)), ... not(am1(...))
	np(X1,...):- not(a11(...)), not(a21(...)), ... not(am2(...))
        ....
	np(X1,...):- not(a1n1(...)), not(a21(...)), ... not(amnm(...))

where each of the not(aij(..)) can be further translated or if they
are of the form not(not(q(...)) replced by q(...).
Warning there can be a lot of these clauses: n1*n2*n3*...nm to be precise.
Also I have assumed the heads of teh clauses contain only free variables
so the aij(...) may be equality(=). To avoid a circular definition of not(_=_)
this needs to be done explicitly.  Given a finite Herbrand Universe
there are only a finite (but possibly large) number of pairs of things that
are not equal so this too can be written down (it is however different for
each program).

I am not entirely sure of the theoretical status of this translation.
It assumes that the completion of the program is what you really meant 
and gives the usual semantics for stratified programs as near as I can tell.
For nostratified programs, for example:

	p:- not(p)

the translated program is:
	p:- not_p

	not_p:-p.
which would conclude that both p and not_p are false.  So in there is no 
guarantee that the result will be consistent in these cases.

The standard minimal meta-interpreter for Prolog can be extended to give this
type of behavior as follows.  Assume that the program is represented by the 
clauses(...) predicate which representes all the clauses for a particular
program as a single list of clauses.  The positive call is given by call(...)
and the negative by neg(...).

	call(true):- true.
	call((A,B)):- call(A), call(B).
	call(not(A)):- neg(A).
	call(X=X):- true.
        call(A):- clauses(List), scan(A,List).

	scan(A,[(A:-B)|_]):- call(B).
	scan(A,[_|Tail]):- scan(A,Tail).

	neg((A,B)):- neg(A).
	neg((A,B)):- neg(B).
	neg(X=Y):- not_equals(X,Y).
	neg(not(A)):- call(A).
        neg(A):- clauses(List), neg_scan(A,List).

	neg_scan(A,[(H:-B)|Tail]):- not_equals(A,H), neg_scan(A,Tail).
	neg_scan(A,[(A:-B)|Tail]):- neg(B), neg_scan(A,Tail).

	not_equals(...) %needs to be defined depending on the program

As you say you might not want to use this although depending on the 
circumstances programs translated or interpreted this way can be efficient
and these techniques contain the essence of a number of the approaches
to negation that are available.
> 
> I'll continue to use the eager Prolog that's available to me.  I need to
> find out about NU-Prolog, even if I don't use it.  At least it might give me
> a "meta-language" for documenting (and thinking about) the termination
> properties of my predicates.
> 
My personal experience is that NU-Prolog is a wonderful language for 
programming in.  In fact the step up from Prolog to NU-Prolog was almost
as much fun as the step from imperative languages to Prolog.
You need many fewer cuts and can adopt a much freer and more expressive
programming style.  Try it you'll love it.
As for efficiency it is not intrinsicly much less efficient than standard
Prologs and I am sure that if as much effort was put into its implementtion
as into other systems out there it would run just as fast (I have heard
figures of 10% to 15% slowdown over eager Prologs but this is surely
application dependent).


	John G. Cleary
	Department of Computer Science
	University of Calgary
	2500 University Drive 
	N.W. Calgary
	Alberta T2N 1N4
	Canada

	cleary@cpsc.UCalgary.ca
	Phone: (403)282-5711 or (403)220-6087