mark@adler.philosophie.uni-stuttgart.de (Mark Johnson) (03/05/91)
%neg.pl : A negation metainterpreter using anti-subsumption constraints.
%
%This file contains a metainterpreter for negation that runs
%in Quintus Prolog.
%
%The treatment of negation is a generalization of the standard
%negation as failure.
%
%Consider a (positive) goal p(X). The standard resolution proof of
%p(X) from a set of program axioms A yields a sequence of answer
%substitutions T1, .., Tn, such that A |= p(T) for any T that is
%subsumed by some Ti in T1, .., Tn.
%
%Assuming the completion, A |= ~p(T) iff for all answer substitutions
%Ti from a resolution proof of p(X), T is not subsumed by any such Ti.
%The metainterpreter below passes around a list of such anti-subsumption
%constraints, and continually checks them to see if they are violated.
%In a system with more advanced control facilities, these checks can
%be efficiently implemented (you can *almost* do it with freeze and diff;
%you need diff/3, where diff(X,Y,Goal) calls Goal when X is unified with Y).
%
%
%Here are some samples.
%
%| ?- m1(~X=a, Cs). % X is not a. Cs is a list of antisubsumption
% % constraints.
%X = _63,
%Cs = [[X]/>[a]] ; % X must not be subsumed by a.
%
%no
%| ?- m1(~X=Y, Cs). % This is diff(X,Y)
%
%X = _62,
%Y = _79,
%Cs = [[X,Y]/>[_465,_465]] ; % The pair X,Y must not be subsumed by U,U
%
%no
%| ?- m1(~member(X,[a,b,c]), Cs). % X is not a member of [a,b,c]
%
%X = _68,
%Cs = [[X]/>[a],[X]/>[b],[X]/>[c]] ; % X must not be subsumed by a, b, or c.
%
%no
%| ?- m1(~member(X,[a,Y]), Cs). % X is not a member of [a,Y]
%
%X = _68,
%Y = _91,
%Cs = [[X,Y]/>[a,_512],[X,Y]/>[_484,_484]] ; % X must not be subsumed by a,
% % and X,Y must not be subsumed by U,U
%no
%
% This next goal uses double negation and existential quantification.
% Literally it reads: L is a list, and it is not the case that there
% exists an X that is a member of L and not equal to a, i.e. every
% member of L is a.
%
%| ?- m1((list(L),~X^(member(X,L),~X=a)), Cs).
%
%L = Cs = [],
%X = _87 ;
%
%L = [a],
%X = _87,
%Cs = [] ;
%
%L = [a,a],
%X = _87,
%Cs = [] ;
%
%L = [a,a,a],
%X = _87,
%Cs = [] ....
:- op(950, xfx, <-). % Program clause constructor
:- op(950, fx, ~). % Negation operator
:- op(700, xfx, />). % Anti-subsumption constraint
:- op(800, xfx, &).
:- ensure_loaded(library(basics)).
:- ensure_loaded(library(freevars)).
:- ensure_loaded(library(subsumes)).
:- ensure_loaded(library(findall)).
% Starts the metainterpreter. G is the goal, and Cs is
% a list of anti-subsumption constraints from negations
% called in the proof.
m1(G, Cs) :-
meta1([G], [], Cs).
% meta1(Goals, ConstraintsIn, ConstraintsOut)
% Goals is a list of goals to prove.
% ConstraintsIn-ConstraintsOut is a difference
% list of anti-subsumption constraints.
meta1([], Cs, Cs).
meta1([G|G1s], C0s, C2s) :-
G <- G0s,
append(G0s, G1s, G01s),
check_negs(C0s, C1s),
meta1(G01s, C1s, C2s).
meta1([~G|Gs], C0s, C3s) :-
free_variables(G, [], [], FVs),
findall(FVs&Cs, m1(G,Cs), NewCs),
negate(NewCs, FVs, NegCs),
append(NegCs, C0s, C1s),
check_negs(C1s, C2s),
meta1(Gs, C2s, C3s).
% check_negs(CIns, COuts)
% Checks anti-subsumption constraints.
check_negs([], []).
check_negs([T0/>T1|C0s], C1s) :-
\+ T0=T1, % T1 can never subsume T0
!, % so delete this constraint
check_negs(C0s, C1s).
check_negs([T0/>T1|_], _) :-
subsumes(T1, T0), % T1 subsumes T0, so fail
!,
fail.
check_negs([C|C0s], [C|C1s]) :-
check_negs(C0s, C1s).
% negate(ToNegate, FVs, Cs)
% Converts the output of the findall of a negated goal
% in meta1 into anti-subsumption constraints.
negate([], _, []).
negate([Vals&_|NewCs], FVs, [FVs/>Vals|Cs]) :-
negate(NewCs, FVs, Cs).
negate([FVs&Negs|NewCs], FVs, Cs) :-
member(FV1s/>FV1s, Negs),
negate(NewCs, FVs, Cs).
/*********************************************************************
* t.pl Example programs for negation metainterpreter m1.
*/
:- op(700, xfx, /=).
% The next two clauses should really be part of the interpreter.
_^G <- [ % skip existential variables in goal.
G ].
(P1,P2) <- [ % handle conjunction.
P1,
P2 ].
X=X <- []. % equality
% Inequality, i.e. the diff of Prolog II and Sicstus
X/=Y <- [
~X=Y ].
% member(X, Xs) iff X appears in list Xs.
member(X, [X|_]) <- [].
member(X, [_|Xs]) <- [
member(X, Xs) ].
% append(L1, L2, L12) iff L12 is the append of L1 and L2
append([], Ys, Ys) <- [].
append([X|Xs], Ys, [X|XYs]) <- [
append(Xs, Ys, XYs) ].
% list(L) iff L is a proper list
list([]) <- [].
list([_|Xs]) <- [
list(Xs) ].
% list_of(E, Es) iff Es is a proper list, every
% member of which is E.
%| ?- m1(list_of(a, L), Cs).
%
%L = Cs = [] ;
%
%L = [a],
%Cs = [] ;
%
%L = [a,a],
%Cs = [] ;
%
%L = [a,a,a],
%Cs = [] ; ...
list_of(E, Es) <- [
list(Es),
~ X^(member(X,Es),E/=X) ].
% every(X,P,Q) iff forall X, P(X) implies Q(X)
% which is equivalent to ~ exists X, P(X) and ~ Q(X)
every(X,P,Q) <- [
~ X^(P,~Q) ].
% duplicated(E,L) iff E appears at least twice in L.
duplicated(E, L) <- [
append(_, [E|Es], L),
member(E, Es) ].
% unique_list(L) iff no element appears twice in L,
% i.e. there does not exist an E in L duplicated.
%| ?- m1(unique_list(L), Cs).
%
%L = Cs = [] ;
%
%L = [_412],
%Cs = [] ;
%
%L = [_412,_545],
%Cs = [[_412,_545]/>[_940,_940]] ; ....
unique_list(L) <- [
list(L),
~ E^duplicated(E, L) ].
% all_duplicates(L) iff every element in L appears at
% least once.
%| ?- m1(all_duplicates([a,b,U,V]), Cs).
%
%U = a,
%V = b,
%Cs = [] ;
%
%U = b,
%V = a,
%Cs = [] ;
%
%no
all_duplicates(L) <- [
list(L),
every(E, member(E,L), duplicated(E,L)) ].