🚀 go-pugleaf

Thanks for pointing out clearly our differences and points of agreement.
Well, the main question still left is:

Richard A. O'Keefe writes:

>        - I claim that bestof/3's interface is defective in precisely
>          the same sense as findall/3's; that (when used within its
>          domain of definition) setof/3's interface is better, and
>          that NU-Prolog's solutions/3 (which generalises setof/3)
>          is better still.

OK, I'll try to fix that. Let's call it _angelic bestof/3_ for reasons I 
will discuss later. Here it is:

% bestof/3(Winner,Game,Generator) is true iff Winner is an answer
% to Generator, Game is a closure that works as a total order on
% alternative answers to Generator and Winner is maximal with respect
% to the total order on the set of the answers.
% The implementation must ensure that:
% - no bindings travel between distinct OR-branches used to prove Generator
% - no bindings are made on possibly uninstantiated variables of the 
%   closure Game

bestof(Winner,Game,Generator):-
	gather_solutions(Winner,Generator,[X|Xs]),
	let_them_play(Xs,Game,X,Winner).
	
let_them_play([],_,Winner,Winner).
let_them_play([Challenger|Xs],Game,Incumbent,Winner) :-
	is_better(NewIncumbent,Game,Incumbent,Challenger),
	let_them_play(Xs,Game,NewIncumbent,Winner).

is_better(Winner,Game,Incumbent,Challenger):-
	\+ \+ 	%  ensures that the winner does not steal bindings
	call_with_closure(Game,[Challenger,Incumbent]),
	!,
	Winner=Challenger.
is_better(Incumbent,_Game,Incumbent,_Challenger).

call_with_closure(Closure,Args):- % may be replaced by call/N
	Closure=..L1,
	append(L1,Args,L2),
  Test=..L2,
  Test.

gather_solutions(X,G,Xs):-findall(X,G,Xs). % just to have it working

% tests

max(Xs,X):-bestof(X,>,member(X,Xs)).

test_max(X):-max([1,2,3,4,3,4,2,1],X).

thief(K1-_V,K2-_V):-K1>K2.

thief_max(Xs,X):-bestof(X,thief,member(X,Xs)).

test_thief(X):-
	% comment out \+ \+ in is_better/4 to steal bindings
	thief_max([1-f(_,b), 2-f(a,_), 4-f(_,_), 3-c], X).


1-st order "soundness" of _angelic bestof/3_:

If P and G are a definite program and a definite goal both possibly
containing occurrences of bestof/3 and $\theta$ is a computed answer
of P+{G}, then $\theta$ is also a computed answer of P'+{G'} where 
P' and G' are obtained by replacing each occurrence of
bestof(X,Order,Generator) by Generator in P and G.

Therefore answers computed by P+{G} are sound as answers of P'+{G'}.

The nice thing is that now we can see bestof/3 as a _pragma_ that is
guiding the search without interfering with the proof itself. That's 
one reason I call it "angelic". The other one is that on top of a 
definite program it works like a meta logical pruning
operator: it cuts off "declaratively" branches of the search tree without
interfering with the final proof. It also has efficient OR-parallel
execution when working with an appropriate generator.

Let's call the version without \+ \+ "unrestricted bestof". You can try
out some of its not always desirable powers by executing test_thief/1.

(Angelic) bestof/3 is like \+ as it cuts some parts of the tree without 
making any bindings. However \+ is more difficult as it reverses success
and failure while even unrestricted bestof/3 only gets things more
instantiated when it goes with the winning OR-branch.

Obviously some of the hidden information exchange capabilities between
different OR-branches of unrestricted bestof/3 are lost as a price for
this strong soundness property, but I agree that if that's what we want
to do, then Richard's:

> combine_solutions(Function, Term, Generator, Answer) :-
>  gather_solutions(Term, Generator, [Solution|Solutions]),
>  reduce(Function, Solutions, Solution, Answer).

does the job quite well.

Paul Tarau
tarau@iro.umontreal.ca