[mercury-users] Re: can one_solution/2 and unsorted_solutions/2 be det?

[Lee Naish]

In message <199710280856.JAA20188 at raavak.cs.kuleuven.ac.be> Bart wrote:
>Now there is no garantee that for
>
>	a :- once(member(X,[1,2])), once(member(Y,[1,2])), X = Y.
>
>	?- a.
>
>succeeds. It doesn't scare me a bit: I can already write it purely;
>once/1 is just that kind of a predicate.

all P (some X P(X)) => (some [X,Y] (P(X), P(Y), X=Y)) is a theorem in
second order logic so you can't do the above in a pure way (unless a
single call to once can fail).

>I picked up once (sic) more the pruneslides.dvi that Lee recommended.
>There is a striking sentence on page 18 with different uses of once/1:
>
>	compile(I,O) - you want any solution (this may affect
>	  completeness if used other than at the top level)
>
>
>One person's top level is another person's goal ...

If you allow arbitrarey pruning other than at the top level then the top
level can fail when it should succeed or (if negation is present) return
a wrong answer.  It would be nice to be able to conclude that no answer
exists if the program fails; soundness would be nice also.  One of the
dangers of making slides available is that people read them and think
they have the whole story...

>In real life, I very often want any solution (of a restricted set
>though) and fortunately it is mostly not at my top level.

There are various logical reasons you might want this.  I argued in the
paper that the different reasons should be expressed using different
(declarative) constructs which don't compromise soundness and
completeness.

	lee