first_soluition/1, etc

[Don Smith]

OK, here's a description of why I wanted choice predicates.
In a planning application, I needed to collect the list of all applicable 
action instances (actions whose preconditions are satisfied) and then the
list of all facts enabled by some applicable action instance.  These procedures
were inside a nondeterministic loop which selects subsets of relevant actions
to consider, and inside another, outer, iterative-deepening loop.  (One
could imagine yet another loop which examines the answers returned by 
the inner loops and evaluates them or finds the groups of 5 solutions and
then does something else.)

At first I tried using solutions/2 to do both of these aggregate collection
operations.  But the running time was horrendous, because the solution terms
contain pointers to earlier parts of the graph, and so the list was sorted
more than it needed to be.   I couldn't call unsorted_solutions/2 because
it's declared cc_multi, which means that I'd have to make all the outer
nondeterministic loops cc_multi too.      

Well, in fact, I was able to rewrite my code to avoid the problems -- I had
to -- but this was annoying and, I think, unnecessary, because I suspect that
we can make single solution predicates declaratively respectable.

Can we use a nonstandard equality theory and say that any permutation of the
list of solutions is the same as any other?  Maybe, but it really depends on 
my algorithm:  from the point of view of my algorithm, any order is OK. 

I think the case of "first_solution/1" is clearer than unsorted_solution/2.
>From the point of view of many algorithms (but not in any deeper sense), any
solution is equivalent to any other.  I'm not sure if this is semantic equality
or just committed choice nondeterminism.   The programmer simply doesn't care
which of many (semantically different) solutions is returned.  Why make her
overspecify things?

Fergus wrote:
>`first_solution' is not referentially transparent;
>it does not satisfy `P = Q => first_solution(P) = first_solution(Q)',
>because in Mercury, the declarative semantics of equality on higher-order
>terms is such that two predicates are equal iff they have the same
>set of solutions.

As I had written, one way to avoid this problem is to
> add an extra, distinguishing tag argument (e.g., a string representing the 
> static syntactic call with arguments) to calls to choice predicates.

Of course, the extra argument could be implicit.    And it _may_ even be necessary
to thread a changing tag around the program to make sure that different solutions 
are returned on different recursive calls.   But maybe not:  if the algorithm really
doesn't "care" which solution is returned, it should be OK to return the same
solution each time.

But Lee says:
>It simply doesn't work.  To get referential transparency you need to be
>able to replace equals by equals.  This is not replacing syntactic
>equals by equals (replacing "1+1" by "1+1" doesn't get you very far!) -
>its replacing *semantic* equals by equals (eg, replacing "1+1" by "0").
>Its not possible for a dumb machine, or even some smart humans, to
>figure out what symbols in my programs/e-mail messages mean addition
>(modulo 2).

So the essential point is that to support referential transparency, semantically 
identical calls to choice predicates must return semantically identical solutions.
Well, in Prolog (and Mercury, as far as I know), identity of first-order terms
_is_ syntactic.   Arithmetic is done via the is/2 relation, not via the changing
the equality theory and using SLDE.  So I don't understand your objection.  
Please elaborate.

It might be inefficient to record solutions to choice predicates in a table and to look
them up to ensure consistent solutions.     But another option is to compile
special, strict sequential code for predicates that appear in single solution (choice) 
calls.  This will ensure that identical calls will return identical solutions.

(Yet another option is for the compiler to allow single solution (choice) predicates only
in "safe" contexts.  For example, the compiler could reject their use inside negations,
if that might cause problems.    And optimizations that duplicate calls to choice predicates
might be disallowed. This might allow for the use of cheaper and more flexible implementation 
techniques.  But I do see that it might hinder optimizations and make for a less symmetric,
pure language.)

Choice predicates _depend_ on operational details, as Fergus said. But I don't think
that the programmer should need to reason or worry about these details, because it
doesn't matter which solution is returned, as long as one is, and as long as identical 
calls return identical solutions.

If Mercury is going to support lazy evaluation (as with BinProlog's engines, or as in Oz's
encapsulated search), it's going to need this sort of nondeterminism anyway.   

In lots of "declarative" specification languages (some of Estelle, Lotos, Lustre, Esterel, 
process algebras) nondeterminism of various sorts is desirable and builtin to the language.   
In a reactive system, one wants to depend on operational details.

Suppose a call first_solution(Tag, p(X,Y)) appears somewhere in the user's code
and that the unique solution p(f(1),g(2)) is returned as the chosen solution.
(It's easiest if we assume that Tag is ground.)    The language must make sure, 
it seems, that if there is similar call first_solution(Tag,p(X',Y')) where (X',Y') 
is an instance of (X,Y), then the same solution p(f(1),g(2)) is chosen.   Orgun
and Wadge require that all calls to choice predicates involve all unbound arguments.

> Purity is a practical issue, *not* a moral issue.

Let me make my self clearer.  Morality is (or should be) practical!  I was
just expressing my gut reaction to the tendency of declarative language
theorists to say:  "No, you must not do that."   We must not use gotos,
we must not use assignments, we must not use side effects, we must not use 
printf, we must not use untypable code, we must not use full unification, 
we must not use cuts, we must not use choice predicates.  So many nots!
I like gotos! I like choice predicates!  etc. (I have libertarian impulses.)  
But I understand that their undisciplined use can cause problems with 
understanding and optimizing code, etc.

   Trying to avoid a flame war, and hoping that we are getting closer to the truth,  

       Don