🚀 go-pugleaf

A couple of points raised by Richard's postings:

>I repeat, THE ISSUE IS TREATMENT OF FREE VARIABLES.  Sorting is not
>the issue.

To quote from my all solutions paper: "The main difference between
findall and solutions is the way local variables are distinguished".
Setof-like treatment of free variables is as important as Richard says.

It turns out that sorting is also an issue - the fact that the IC-Prolog
all solutions primitive does not sort solutions allows var/1 to be
implemented (but only using by using the coroutining facilities).  To
avoid a logical specification of an all solutions construct allowing N
factorial different permutations being returned (or an unbounded number
of repeated elements), it seems necessary to specify some canonical
representation of the set of answers.

> Lee Naish's
>"little bit pregnant" slur is rather exaggerated.

What I said is you can argue both ways on this.  Richard obviously
thinks there are degrees of "non-logicalness".  From a practical point
of view I agree that setof/3 is nicer than findall/3 because it is closer
to the ideal logical construct.  However, that kind of argument is not
going to convince John Lloyd to put setof/3 into Goedel (for example).
Actually John is not entirely happy with any all solutions construct,
including solutions/3.  The semantics of solutions/3 was defined by a
schema: for any call to solutions with an instantiated generator, it
gives you an equivalent bit of logic.  Personally I'm happy with that.

There are a couple of rough edges.  One is what you do when the
generator is a variable.  Well, thats just like call/1, which again
doesn't worry me.  You can define call like this:

call(p(X)) :- p(X).
call(q(X, Y)) :- q(X, Y).
.....

Some people are very uptight about p/1 and q/2 being used as predicate
and function names.  The context always tells you whether something is a
predicate or function so if it worries you, add a superscript greek letter
to everything in sight.  The other rough edge is local variables in the
solutions to the generator.  What we really need to do is return an
infinite list of solutions.  Solutions/3 writes an error message, which
is like going into an infinite loop, but more useful.

> As soon as you allow inequality, you've restricted
>yourself to the Herbrand universe.

I don't think its quite as bad as that.  When you write a NU-Prolog
program, implicitly there are a whole lot of additional clauses:

a ~= b.
b ~= c.
....

These better be true in the intended interpretation (at least if you use
~= in your program), but it need not be a Herbrand interpretation.
Similarly, when you use negation as failure, the equality axioms (which
include the ~= case) better be true in the intended interpretation).
The equality axioms restrict the interpretation to look just like a
Herbrand interpretation, but it could be another (a Clark interpretation
perhaps?).  The solutions/3 semantics implicitly uses negation.

>	If every two solutions returned by the Generator either
>	do not unify or are absolutely identical,
>	setof/3 is as well-behaved as solutions/3, otherwise not.

The condition needs to be stronger:

1) no solution to the generator contains local variables (note that
solutions/3 just produces an error message when local variables are
present in answers - not much more clever than setof/3), and

2) every two solutions returned by the Generator the *global* variables
either do not unify or are identical.

If all solutions to the generator are ground (the condition mentioned by
Fernando), conditions 1) and 2) are satisfied.  To show why we need 2),
consider the following (NU-Prolog) goal:

?- solutions(Y, (Y = a, X = a ; Y = b), L), (X = a ; X = b).
L = [a, b],
X = a ;

L = [b],
X = b ;

fail.

The solutions call returns the answer L=[a,b], with X=a.  Setof/3
could do the same thing - no problems so far.

The next solution is L = [b], but that is only valid if X ~= a.
In NU-Prolog, the solutions call results in a delayed constraint
equivalent to X ~= a.  Poor old setof doesn't have the benefit of
delayed calls - there is nothing it can do to represent this answer
properly.

Note that if the goal is reversed, so the all solutions construct
is called last, setof produces the same set of answers as solutions.
Condition 2) is satisfied since there is no binding of global variables
by the "generator".

A final subtle point.  In a construct which can't use delaying, we need
a third restriction:

3) the set of answers must be constrained to be non-empty.

Consider the following:

?- solutions(Y, (Y = a, X = a), L), (X = a ; X = b).
L = [a],
X = a ;

L = [],
X = b ;

fail.

This goal satisfies conditions 1) and 2), but needs the constraint
X ~= b for the L = [] solution.  Fortunately, setof/3 and bagof/3
are defined to fail rather than return empty lists.

>If it is possible to get a better approximation to solutions/3 without
>coroutining, I would very much like to know how to do it.

There are a couple of things:

1) Do quantifiers *properly*.  With code which has variables which should
be local to the all solutions construct appearing elsewhere (eg

	setof(X, ...), ...... X ...

), either the different occurrences of X should be considered different
variables or the compiler should generate an error.  At the very least,
"style checkers" should COMPLAIN VERY LOUDLY.  I'm not sure what current
commercial Prolog systems do with such code.  Of course this case makes
a mess of the semantics (it can be as bad as findall) if not handled
properly.

1a) Just a point on implementation.  If you do quantifiers properly, you
can distinguish local and global variables at compile time, saving some
runtime overheads, ie, ITS FASTER.

2) It wouldn't hurt to have versions of setof/3 which produced errors
when called "outside their design envelope", rather than returning
*something*.

	lee