🚀 go-pugleaf

In several of my programs, I use a meta predicate I call  u n i q u e. 
unique(+Expr,+Goal) is similar to findall/3 or setof/3 in that it 
takes a goal as its second argument and an expression, typically 
sharing variables with Goal, as its first argument. unique/2 succeeds 
and instantiates Expr iff there is exactly one instantiation of Expr 
(irrespective of different naming of variables) derivable from any 
possible proof of Goal.

Examples:	?- unique(X,member(X,[1,2,3])).
		no

		?- unique([X,Y],( member(X,[1,2,1]),
			          member(Y,[2,3,2]),
			          X + Y =:= 3       ) ).
		X = 1
		Y = 2

For my applications of unique/2, the following requirements have to 
be met:
- The implementation has to allow for nested use (e.g. a goal inside 
  unique may directly or indirectly involve another call of unique).
- After having found two  d i f f e r e n t  solutions (in terms of 
  Expr), the computation has to terminate (with failure). This is not 
  only for efficiency reasons, but also allows for the processing of 
  goals with a potentially infinite number of (different) solutions.

In the following, I list two different implementations of unique/2, one 
correct and one incorrect. I am interested in any comments on the problem 
in general, but specifically in answers to the following questions:

(1) Do you know of any Prolog implementation where the uniqueness test 
    can be directly performed by a built-in predicate (in accordance with 
    the computational requirements)?

(2) Do you know of different implementations of a uniqueness test in 
    Prolog? (Please give ref. or send code!)

(3) Do you have suggestions how to improve the two versions listed?

Ulrich Hoppe
GMD-IPSI 
Dolivostr. 15
6100 Darmstadt (FRG)
hoppe@ipsi.darmstadt.gmd.dbp.de

________________________________________________________________________

% Version 1:      unique1(+Expr,+Goal) 
% Comments:
%   (1) A copy of the original goal with fresh variables is
%	generated as a reference term for comparison with future 
% 	instantiations which may be pairwise incompatible (in the 
%	instantiation of variables  n o t  shared with	Expr).
%   (2) A marker '$unitest'(Expr,Goal) may be left in the database
%	by a previous successful call of Goal. 
%	db_unify_fact('$unitest'(Expr,CGoal)) is used instead of
%	clause('$unitest'(Expr1,CGoal),true) in order to avoid the 
%	following behavior:
%		?- unique1(X,member(X,[[a,_],[a,1],[a,2]])).
%		X       = [a,_648]
%		?- unique1(X,member(X,[[a,1],[a,_],[a,2]])).
%		no
%	Instead, unique1 should fail (and does) in both cases. 
%	Still, it succeeds on
%		?-  unique1(X,member(X,[[a,_],[a,1]])).
%	giving  X = [a,1] irrespective of the order of elements.  
%	So, unique specialization of a solution is allowed.
%	"Fail" in this case causes a loop over call(Goal).
%   (3) If a previous solution exists and cannot be unified
%	with the current one, the database is cleared and 
%	and test_unique1/3 terminates with failure.
%   (4)	If there is no previous solution, the current solution
%	is asserted and "fail" causes the loop.
% Nested use is possible, because the different DB assertions are 
% distinguished by the goal. Given an original goal whose execution 
% terminates, we can be sure that it cannot appear again as a subgoal 
% of itself in the calling hierarchy (otherwise contradiction to non-
% termination). 
%

unique1(Expr,Goal) :-
	copy(Goal,CGoal), 	% (1)
	!,
	test_unique(Expr,Goal,CGoal).

test_unique1(Expr,Goal,CGoal) :-
	call(Goal), 
	(  db_unify_fact('$unitest'(Expr,CGoal)),	% (2)
	   fail
	 ; clause('$unitest'(Expr1,CGoal),true),	% (3)
	   Expr1 \= Expr,
	   !,
	   retract('$unitest'(Expr1,CGoal)),
	   fail 
	 ; not clause('$unitest'(Expr,CGoal),true),	% (4)
	   asserta('$unitest'(Expr,Goal)),
	   fail  ).
test_unique1(Expr,Goal,CGoal) :-
	retract('$unitest'(Expr,Goal)).

db_unify_fact(Fact) :-
	retract(Fact),
	asserta(Fact).


% Version 2:      unique2(+Expr,+Goal) 
% Comments:
% This version behaves exactly as unique1/2 if in test_unique1/3
% db_unify_fact(<marker>) were replaced by clause(<marker>,true).
% It does not require DB-interactions (except potentially for copy), 
% but is computationally less efficient than version 1 in that the 
% first solution of Goal (if there is one) is always calculated twice.
%   

unique2(Expr,Goal) :-
        copy(p(Expr,Goal),p(CExpr,CGoal)),
        call(Goal),
        !,
        alt_test(Expr,CExpr,CGoal).

test_unique2(Expr,CExpr,CGoal) :-
        call(CGoal), 
        (  Expr \= CExpr, !, fail
         ; fail ).
test_unique2(_,_,_) :- true.