🚀 go-pugleaf

Some weeks ago John G. Cleary (University of Calgary) wrote

  Recent postings about NU-Prolog and the use of delayed computation have
  reminded me of a problem which I have never quite been able to solve. The
  background is that in NU-Prolog it is possible to permute a list of objects
  with many different programs. For example a straightforward permute can be
  driven backward by instantiating its 'output' and seeing what appears on
  its 'input'. Similarly any sorting program can be driven backward to generate
  permutations. Well almost any sort program. It works fine for simple ones
  like insertion sort or merge sort. However, I tried to reverse quicksort
  and came across a problem. It goes into an infinite loop after giving the
  first solution and I was quite unable to concoct a set of delays which
  prevented this.

  The challenge is to use NU-Prolog (or some other Prolog with delays) to run
  quicksort backward ( and forward).

  ...

The following simple meta-interpreter delays goals that are not 'sufficiently'
instantiated. It will run quicksort forward and backward, will generate all
'unsorted' lists from a sorted one, and will not go into an infinite loop.

---------------------------------

% prove(Goal) :-
% Goal is true with respect to the Prolog program being interpreted.
% The interpreter will only try to prove a goal if it is ready, i.e. 
% sufficiently instantiated.
% The interpreter transforms conjunctive goals into lists.
% MacProlog 2.5 version

prove(Goal) :-
  proveL([Goal]).

proveL(Goals) :- 
  remove(Ready,Goals,Goals_without_Ready),   %	pick a goal
  ready(Ready),                              %	is it ready ?
  !,                                         %	no backtracking
  prove_one(Ready,Goals_without_Ready).      %	prove the goal
proveL([]).                                  %	all done

prove_one(Goal,Goals) :-
  idef(Goal),                                %  user predicate 
  clause(Goal,Body),
  make_list(Body,Body_as_List),
  append(Body_as_List,Goals,NewGoals),
  proveL(NewGoals).
prove_one(Goal,Goals) :-
  sdef(Goal),                                %	system predicate
  call(Goal),
  proveL(Goals).
													

% make_list(Goals, Goals_as_List) :- Goals_as_List is a list whose  
% elements are the goals of the conjunctive goal Goals
make_list((A,B),[A|B_as_List]) :-
  make_list(B,B_as_List).
make_list(true,[]).
make_list(A,[A]) :-
  A \= (_,_),
  A \= true.


% ready(P) :- P is sufficiently instantiated to be executed
% not/1: no variables 
ready(not(P)) :- 
  !,
  varsin(P,[]).																								
% append/3: first or last argument must be instantiated
ready(append(Xs,Ys,Zs)) :- 
  !, 
  (nonvar(Xs); nonvar(Zs)).		
% partition/4: first and second or second, third and fourth arguments 
% must be instantiated
ready(partition(Xs, X, Littles,Bigs)) :-
  !,
  ((nonvar(Xs), nonvar(X)); (nonvar(X), nonvar(Littles), nonvar(Bigs))). 
% quicksort/2: first or last argument must be instantiated
ready(quicksort(Xs,Ys)) :- 
  !, 
  (nonvar(Xs); nonvar(Ys)).
% catch-all
ready(_).


% quicksort(Xs,Ys) :- the list Ys is an ordered permutation of the list Xs
quicksort([X|Xs],Ys) :-
  partition(Xs,X,Littles,Bigs),
  quicksort(Littles,Ls),
  quicksort(Bigs,Bs), 
  append(Ls,[X|Bs],Ys).
quicksort([],[]).

% partition(Xs,X,Littles,Bigs) :- the list Littles (Bigs) contains all
% elements of the list Xs that are not larger (larger) than X
partition([X|Xs],Y,[X|Ls],Bs) :- 
  X =< Y, 
  partition(Xs,Y,Ls,Bs).
partition([X|Xs],Y,Ls,[X|Bs]) :- 
  X >  Y, 
  partition(Xs,Y,Ls,Bs).
partition([],Y,[],[]).



The meta-interpreter prove/1 will generate all 'unsorted' lists without getting
into an infinite loop.


:-  prove(quicksort(Xs, [1, 2, 3]))

No1  Xs = [1, 2, 3]

No2  Xs = [1, 3, 2]

No3  Xs = [2, 1, 3]

No4  Xs = [2, 3, 1]

No5  Xs = [3, 1, 2]

No6  Xs = [3, 2, 1]

No more solutions


   --- nef (fuchs@ifi.unizh.ch)