Path: utzoo!utgpu!attcan!uunet!munnari!mulga!lee
From: lee@mulga.oz (Lee Naish)
Newsgroups: comp.lang.prolog
Subject: Re: setof
Message-ID: <2969@mulga.oz>
Date: 2 Sep 88 07:02:34 GMT
References: <1411@kulcs.kulcs.uucp>
Reply-To: lee@mulga.UUCP (Lee Naish)
Organization: Comp Sci, Melbourne Uni, Australia
Lines: 39

In article <1411@kulcs.kulcs.uucp> bimbart@kulcs.UUCP (Bart Demoen) writes:
> if setof/3 is non-logical when its solutions are not
>ground, that is because @</2 (and its sisters) are non-logical for non-ground
>arguments; after all, setof/3 tries to order with @</2 or doesn't it ?

(Sorry if I am reiterating anything - I missed the discussion so far.
I suggest reading "All Solutions Predicates in Prolog" which appeared in
the 1985 SLP in Boston, for a more detailed coverage.)

There are two kinds of variables which can appear in answers to all
solutions predicates: "global" variables which appear unquantified in
the goal; and "local" variables which are existentially quantified.
The following is an example of global vars:
	?- setof(X, (X = A ; X = B), L), ...
setof has to sort the list [A, B] without knowing what the values of A
and B will be (in fact A may end up less than, equal to *and* greater
than B due to Prolog's nondeterminism, so any answer will be wrong in
some cases).  The solutions/3 primitive of NU-Prolog delays the sorting
until A and B are instantiated.

Here is an example of a local variable appearing in the solution:
	?- setof(X, Loc ^ (X = Loc), L), ...
The answer with X bound to the local variable Loc indicates that the
goal is true for all values of X.  "Logically" L should therefore be
bound to the (sorted) list of all terms.  I dont know of any way around
this - solutions/3 gives an error when local variables appear in
answers.

The case where there are global variables in answers gets more complex
when global variables also get instantiated.  Questions concerning sound
negation (inequality to be precise) arise.  I think of this as a
separate issue but will give an example anyway:
	?- setof(X, (X = xxx ; A = B, X = f(B)), L), ...
The solution L = [xxx] should "logically" be returned iff A ~= B (in
general you need universal quantification on the inequality and if you
look at implementation details it gets even more hairy - see "Negation
and Quantifiers in NU-Prolog" in the 1986 ICLP, London).

	lee