This operator is a hard nut.
I have some notes on the Prolog \+
here:
Here is an example for a floundering query:
% Complete list of rooms room(green). room(blue). room(red). room(white). % Complete list of persons person(jimmy). person(ricky). person(sally). person(cindy). person(nancy). person(johnny). % List of room occupations. % If this predicate is subject to a "closed world assumption", then % a room is unoccupied exactly if it doesn't appear in the location/2 % fact list. If our knowledge can be considered incomplete, other rooms % than those listed below may be occupied. location(jimmy,red). location(ricky,blue). location(cindy,green). % --- % Goal based on positive logic % --- % If "Room" is nonvar: Is the room "Room" provably occupied? % If "Room" is var: Is there any room "Room" such that "Room" is provably occupied? occupied(Room) :- assertion((var(Room);room(Room))), location(_Person,Room). % --- % Goal based on negation as failure. % The second argument gives the "approach" % --- % If "Room" is nonvar, the question is: % "Is Room unoccupied (as far as we know)?" % or "Is there no evidence that the Room is occupied?" not_occupied(Room,_) :- nonvar(Room), assertion(room(Room)), \+ location(_Person,Room). % If "Room" is var, the question is: % "Is there any Room such that the room is unoccupied?" % or "Is there any Room such that there is no info that the room is occupied?" % Approach 'x': Doesn't work, as the proof procedure answers the question "is there % no room that is occupied?" not_occupied(Room,x) :- var(Room), !, \+ location(_Person,Room). % Approach 'a': You can only ask about a *specific* room. If no specific "Room" % has been given, the negated goal is delayed until the "Room" has % been instantiated. not_occupied(Room,a) :- var(Room), % this test applies only "now", "Room" can be instantiated later !, when( ground(Room), (format("Querying with ~q~n",[Room]), \+ location(_Person,Room)) ). % Approach 'b': We will enumerate them all. This works nicely for a small number % of rooms, less well for infinitely large domain. not_occupied(Room,b) :- var(Room), !, room(Room), \+ location(_Person,Room).
Then:
Approach x
"flounders" and erroneously fails:
?- not_occupied(R,x). false.
Approach a
optimistically succeeds and spits out a residual constraint. This actually means that the answer hasn't been fully computed yet and the success is dubious:
?- not_occupied(R,a). when(ground(R),(format("Querying with ~q~n",[R]),\+location(_108418,R))).
Approach a
where R is instantiated "later" (presumably, when more is known) succeeds properly:
?- not_occupied(R,a),R=white. Querying with white R = white.
Or fails properly:
?- not_occupied(R,a),R=red. Querying with red false.
Note that the unfrozen goal is refrozen on backtracking (in fact, the situation before the unfreezing is restored)
?- not_occupied(R,a),format("=>~n"),member(R,[white,red,green]). => Querying with white R = white ; Querying with red Querying with green false.
Enumerating the "room" domain and testing each element also works:
?- not_occupied(R,b). R = white.
An application in conjunction with "naf naf"
Here we use "naf naf" to make sure any bindings are undone and computation has no effect ("pocket universe"), while using nb_setval/2, nb_getval/2 to smuggle computed information out ("wormhole"):
stringify_open_list_with_no_effect(Tip,Fin,String) :- assertion(var(String)), assertion(var(Fin)), \+ \+ (Fin = [], format(string(Printed), "~q", [Tip]), nb_setval(printed, Printed)), assertion(var(Fin)), nb_getval(printed,String), assertion(string(String)), nb_delete(printed).
?- stringify_open_list_with_no_effect([a,b,c,d|Fin],Fin,String), format("~q",[Fin]). _17460 String = "[a,b,c,d]"