2%neg.pl : A negation metainterpreter using anti-subsumption constraints. 3% 4%This file contains a metainterpreter for negation that runs 5%in Quintus Prolog. 6% 7%The treatment of negation is a generalization of the standard 8%negation as failure. 9% 10%Consider a (positive) goal p(X). The standard resolution proof of 11%p(X) from a set of program axioms A yields a sequence of answer 12%substitutions T1, .., Tn, such that A |= p(T) for any T that is 13%subsumed by some Ti in T1, .., Tn. 14% 15%Assuming the completion, A |= ~p(T) iff for all answer substitutions 16%Ti from a resolution proof of p(X), T is not subsumed by any such Ti. 17%The metainterpreter below passes around a list of such anti-subsumption 18%constraints, and continually checks them to see if they are violated. 19%In a system with more advanced control facilities, these checks can 20%be efficiently implemented (you can *almost* do it with freeze and diff; 21%you need diff/3, where diff(X,Y,Goal) calls Goal when X is unified with Y). 22% 23% 24%Here are some samples. 25% 26%| ?- m1(~X=a, Cs). % X is not a. Cs is a list of antisubsumption 27% % constraints. 28%X = _63, 29%Cs = [[X]/>[a]] ; % X must not be subsumed by a. 30% 31%no 32%| ?- m1(~X=Y, Cs). % This is diff(X,Y) 33% 34%X = _62, 35%Y = _79, 36%Cs = [[X,Y]/>[_465,_465]] ; % The pair X,Y must not be subsumed by U,U 37% 38%no 39%| ?- m1(~member(X,[a,b,c]), Cs). % X is not a member of [a,b,c] 40% 41%X = _68, 42%Cs = [[X]/>[a],[X]/>[b],[X]/>[c]] ; % X must not be subsumed by a, b, or c. 43% 44%no 45%| ?- m1(~member(X,[a,Y]), Cs). % X is not a member of [a,Y] 46% 47%X = _68, 48%Y = _91, 49%Cs = [[X,Y]/>[a,_512],[X,Y]/>[_484,_484]] ; % X must not be subsumed by a, 50% % and X,Y must not be subsumed by U,U 51%no 52% 53% This next goal uses double negation and existential quantification. 54% Literally it reads: L is a list, and it is not the case that there 55% exists an X that is a member of L and not equal to a, i.e. every 56% member of L is a. 57% 58%| ?- m1((list(L),~X^(member(X,L),~X=a)), Cs). 59% 60%L = Cs = [], 61%X = _87 ; 62% 63%L = [a], 64%X = _87, 65%Cs = [] ; 66% 67%L = [a,a], 68%X = _87, 69%Cs = [] ; 70% 71%L = [a,a,a], 72%X = _87, 73%Cs = [] .... 74:- op(950, xfx, <-). % Program clause constructor 75:- op(950, fx, ~). % Negation operator 76:- op(700, xfx, />). % Anti-subsumption constraint 77:- op(800, xfx, &). 78 79:- ensure_loaded(library(basics)). 80:- ensure_loaded(library(freevars)). 81:- ensure_loaded(library(subsumes)). 82:- ensure_loaded(library(findall)). 83 84% Starts the metainterpreter. G is the goal, and Cs is 85% a list of anti-subsumption constraints from negations 86% called in the proof. 87m1(G, Cs) :- 88 meta1([G], [], Cs). 89 90% meta1(Goals, ConstraintsIn, ConstraintsOut) 91% Goals is a list of goals to prove. 92% ConstraintsIn-ConstraintsOut is a difference 93% list of anti-subsumption constraints. 94meta1([], Cs, Cs). 95meta1([G|G1s], C0s, C2s) :- 96 G <- G0s, 97 append(G0s, G1s, G01s), 98 check_negs(C0s, C1s), 99 meta1(G01s, C1s, C2s). 100meta1([~G|Gs], C0s, C3s) :- 101 free_variables(G, [], [], FVs), 102 findall(FVs&Cs, m1(G,Cs), NewCs), 103 negate(NewCs, FVs, NegCs), 104 append(NegCs, C0s, C1s), 105 check_negs(C1s, C2s), 106 meta1(Gs, C2s, C3s). 107 108% check_negs(CIns, COuts) 109% Checks anti-subsumption constraints. 110check_negs([], []). 111check_negs([T0/>T1|C0s], C1s) :- 112 \+ T0=T1, % T1 can never subsume T0 113 !, % so delete this constraint 114 check_negs(C0s, C1s). 115check_negs([T0/>T1|_], _) :- 116 subsumes(T1, T0), % T1 subsumes T0, so fail 117 !, 118 fail. 119check_negs([C|C0s], [C|C1s]) :- 120 check_negs(C0s, C1s). 121 122% negate(ToNegate, FVs, Cs) 123% Converts the output of the findall of a negated goal 124% in meta1 into anti-subsumption constraints. 125negate([], _, []). 126negate([Vals&_|NewCs], FVs, [FVs/>Vals|Cs]) :- 127 negate(NewCs, FVs, Cs). 128negate([FVs&Negs|NewCs], FVs, Cs) :- 129 member(FV1s/>FV1s, Negs), 130 negate(NewCs, FVs, Cs). 131 132 133/********************************************************************* 134 * t.pl Example programs for negation metainterpreter m1. 135 */ 136 137:- op(700, xfx, /=). 138 139% The next two clauses should really be part of the interpreter. 140 141_^G <- [ % skip existential variables in goal. 142 G ]. 143 144(P1,P2) <- [ % handle conjunction. 145 P1, 146 P2 ]. 147 148X=X <- []. % equality 149 150% Inequality, i.e. the diff of Prolog II and Sicstus 151X/=Y <- [ 152 ~X=Y ]. 153 154% member(X, Xs) iff X appears in list Xs. 155member(X, [X|_]) <- []. 156member(X, [_|Xs]) <- [ 157 member(X, Xs) ]. 158 159% append(L1, L2, L12) iff L12 is the append of L1 and L2 160append([], Ys, Ys) <- []. 161append([X|Xs], Ys, [X|XYs]) <- [ 162 append(Xs, Ys, XYs) ]. 163 164% list(L) iff L is a proper list 165list([]) <- []. 166list([_|Xs]) <- [ 167 list(Xs) ]. 168 169% list_of(E, Es) iff Es is a proper list, every 170% member of which is E. 171%| ?- m1(list_of(a, L), Cs). 172% 173%L = Cs = [] ; 174% 175%L = [a], 176%Cs = [] ; 177% 178%L = [a,a], 179%Cs = [] ; 180% 181%L = [a,a,a], 182%Cs = [] ; ... 183list_of(E, Es) <- [ 184 list(Es), 185 ~ X^(member(X,Es),E/=X) ]. 186 187% every(X,P,Q) iff forall X, P(X) implies Q(X) 188% which is equivalent to ~ exists X, P(X) and ~ Q(X) 189every(X,P,Q) <- [ 190 ~ X^(P,~Q) ]. 191 192% duplicated(E,L) iff E appears at least twice in L. 193duplicated(E, L) <- [ 194 append(_, [E|Es], L), 195 member(E, Es) ]. 196 197% unique_list(L) iff no element appears twice in L, 198% i.e. there does not exist an E in L duplicated. 199%| ?- m1(unique_list(L), Cs). 200% 201%L = Cs = [] ; 202% 203%L = [_412], 204%Cs = [] ; 205% 206%L = [_412,_545], 207%Cs = [[_412,_545]/>[_940,_940]] ; .... 208unique_list(L) <- [ 209 list(L), 210 ~ E^duplicated(E, L) ]. 211 212% all_duplicates(L) iff every element in L appears at 213% least once. 214%| ?- m1(all_duplicates([a,b,U,V]), Cs). 215% 216%U = a, 217%V = b, 218%Cs = [] ; 219% 220%U = b, 221%V = a, 222%Cs = [] ; 223% 224%no 225all_duplicates(L) <- [ 226 list(L), 227 every(E, member(E,L), duplicated(E,L)) ]