hoppe@ipsi.UUCP (Heinz-Ulrich Hoppe) (03/26/91)
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.hoppe@ipsi.UUCP (Heinz-Ulrich Hoppe) (03/27/91)
Of course, the two predicates unique1 and unique2 have to be defined as: > unique1(Expr,Goal) :- > copy(Goal,CGoal), > !, > test_unique1(Expr,Goal,CGoal). ^^^^^^^^^^^^ > unique2(Expr,Goal) :- > copy(p(Expr,Goal),p(CExpr,CGoal)), > call(Goal), > !, > test_unique2(Expr,CExpr,CGoal). ^^^^^^^^^^^^ Ulrich Hoppe GMD-IPSI Dolivostr. 15 6100 Darmstadt (FRG) hoppe@ipsi.darmstadt.gmd.dbp.de
tom@quintus.UUCP (Tom Howland) (03/27/91)
Regarding the question about a "unique" predicate, wouldn't this do it? unique(X,G):-findall(X,G,L),sort(L,[X]). - Tom
jm@sics.se (Johan Montelius) (03/28/91)
>wouldn't this do it? >unique(X,G):-findall(X,G,L),sort(L,[X]). Does it work in Quintus? Try findall(X,member(X,[1,2,3|_]),L) and try to sort L. It does not work in SICStus. It does however work in AKL. unique(L,Goal):- bagof(L1,Goal), filter(L1,L). | ?- unique([A],X\member(X,[1,2,3|_])). no | ?- **** AKL**** Soon at a theatre near you. -- Johan Montelius SICS, PO Box 1263, S-164 28 Kista, Sweden. Phone: +46 8 752 15 68 Telefax: +46 8 751 72 30 Internet: jm@sics.se