Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!bloom-beacon!mcgill-vision!iros1!ouareau!tarau
From: tarau@ouareau.iro.umontreal.ca (Paul Tarau)
Newsgroups: comp.lang.prolog
Subject: Re: Higher Order Extensions
Keywords: Constructive "all solutions" in pure Prolog
Message-ID: <1019@mannix.iros1.UUCP>
Date: 8 May 89 15:41:33 GMT
References: <11500013@hpldola.HP.COM> <783@gould.doc.ic.ac.uk>
Sender: news@iros1.UUCP
Reply-To: tarau@iros1.UUCP (Paul Tarau)
Organization: Universite de Montreal
Lines: 109

In article <783@gould.doc.ic.ac.uk> cdsm@doc.ic.ac.uk (Chris Moss) writes:

>  1. The predicate to find the set of all solutions can easily be written 
>in pure Prolog with negation. (It's the list of which there are no
>other solutions). The only problem is that it is O(N^2). 
>"setof" (defined in Warren's paper) also needs metalogical predicates such
>as var, though these _can_ be defined in Prolog with cut.
>  2. findall cannot be defined in Prolog without assert/retract or equivalent
>as far as I know (I've never seen a proof). The problem here is precisely
>showing that there are multiple solutions.
>

Defining a findall-like predicate in pure Prolog is relatively easy,
if we use a data-structure representation of the database.

Prolog's implementation of SLD-resolution uses a partially destructive
unification (substitutions are "applied" to goals, although input clauses are
used as fresh variants). All we have to do is to replace it with a
no-side-effect unification predicate:

	unify(X,Y,Mgu)

where Mgu is a most general unifier of X and Y, which contains
only fresh variables.


% Constructive "all-answers" predicate in pure Prolog

:-op(600,xfx,<=).

all_answers(Pattern,Goal,Answers):-
	clauses(Cs),
	solve_all([Pattern<=[Goal]],Cs,[],Answers).

solve_all([],_,As,As):-!.			% no more goals
solve_all([G|Gs],Cs,OldAs,NewAs):-
	solve_one(G,Cs,Gs,NewGs,OldAs,As),	% solve the first goal
	solve_all(NewGs,Cs,As,NewAs).		% solve the others

solve_one(Answer<=[],_,Gs,Gs,As,[Answer|As]):-!.	% keep Answer
solve_one(Goal,Cs,Gs,NewGs,As,As):-			% 
	reduce_all(Cs,Goal,Gs,NewGs).			% reduce Goal

reduce_all([],_,OldGs,OldGs):-!.		% no more clauses
reduce_all([Clause|Cs],Goal,OldGs,NewGs):- 	% select the first clause
	reduce_one(Clause,Goal,OldGs,Gs),	% reduce the others
	reduce_all(Cs,Goal,Gs,NewGs).

reduce_one(Clause,Goal,Gs,[NewGoal|Gs]):-	% successful reduction
	reduce(Goal,Clause,NewGoal),!.		% giving NewGoal
reduce_one(_,_,Gs,Gs).				% failure: no new goal

reduce(Answer<=Goal,Head<=Body,NewAnswer<=NewBody):-	% reduces a goal
	unify(tuple(Answer,	Goal,	_	),	% and an input clause
	      tuple(_,		Head,	Body	),	% giving a new goal
	      tuple(NewAnswer,	_,	NewBody	)).


% data

clauses([
	[app([],Ys,Ys)|Cont]<=Cont,
	[app([A|Xs],Ys,[A|Zs])|Cont]<=[app(Xs,Ys,Zs)|Cont],

	[nrev([],[])|Cont]<=Cont,
	[nrev([X|Xs],R)|Cont]<=[nrev(Xs,T),app(T,[X],R)|Cont],

	[perm([],[])|Cont]<=Cont,
	[perm([X|Xs],Ys)|Cont]<=[perm(Xs,Zs),ins(X,Zs,Ys)|Cont],

	[ins(X,Xs,[X|Xs])|Cont]<=Cont,
	[ins(X,[Y|Ys],[Y|Zs])|Cont]<=[ins(X,Ys,Zs)|Cont]
]).

% tests

t1(Xs):-all_answers(X,nrev([a,b,c],X),Xs). 

t2(Xs):-all_answers(X,perm([1,2,3],X),Xs). 

t3(R):-all_answers([X,Y],app(X,Y,[a,b]),R). 


Although non-destructive unification is at least as "logical" as
its Prolog cousin, one can easily avoid it by using "numbervars" 
and "melt-new" (arithmetic and "structure inspection" predicates
have pure Prolog equivalents).

In Quintus-Prolog a practical definition is:

	unify(X,Y,U):-copy_term(X,U),copy_term(Y,U).

In ALS-Prolog (a nice system, by the way) we can use "$$bagof" which
creates terms directly on the heap, without "assert" and "retract".

	unify(X,Y,U):-$$bagof(X,X=Y,[U]).

In other prologs the fastest predicate is probably:

	unify(X,Y,U):-findall(X,X=Y,Us),Us=[U].


With a unify(X,Y,U) predicate which never fails, returning a 
"bottom" element if X and Y are not unifiable, it is
even possible to give a version of the previous program which
does not use the "negation-as-failure" implicit in the "red" cut
of reduce_one/4.

Paul Tarau