[mercury-users] Re: first_soluition/1, etc

[Fergus Henderson]

Don Smith wrote:
> 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. 

If your algorithm doesn't care about the order of solutions, then it
is using unordered lists to represent sets.  So it would make sense
to use an explicit set data type, e.g.

	:- type unsorted_set(T) ---> unsorted_set(list(T))
		where equality is unsorted_set_equals.

or the standard library `set_unordlist' type.

Then you can use `unsorted_solutions' and `promise_one_solution' to 
define a det `unsorted_solutions_set':

	:- pred unsorted_solutions_set(pred(T), my_set(T)).
	:- mode unsorted_solutions_set(pred(out) is nondet, out) is det.
	unsorted_solutions_set(Pred, SolutionsSet) :-
		SolutionsSet = promise_one_solution(
			pred(Set::out) is cc_multi :-
				unsorted_solutions(Pred, List),
				Set = unsorted_set(List)
		).

Using a set type documents the fact that your algorithm doesn't care about
the order.

> 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?

There's three possible cases:

	(a) you don't care which solution you get

	(b) you don't care which solution you get, except that
	    you want to get the same solution each time

	(c) you do care which solution you get, but
	    all the solutions to this query are guaranteed to be
	    equal.

Case (a) corresponds to committed choice nondeterminism.

Case (c) corresponds to the use of promise_one_solution
(perhaps with use of user-defined equality so that "equivalent"
becomes "equal").

Case (b) corresponds to the Hilbert-style choice function.

>From your description of your program, I think (c) is the most
appropriate choice.

However, this discussion has convinced me that there _are_ some
circumstances in which (b) is appropriate -- Andrew Bromage's
example is one of them.  In his example, the reason why he
needs to get the same solution each time is because of the
externally imposed interface requirement.

So, the problem then is that (b) is rather tricky to implement :-(

> 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.

Well, that is one possible solution: a first_solution/1 function is not
referentially transparent, but a first_solution/4 predicate could be.

	:- pred first_solution(pred(T), T, io__state, io__state).
	:- mode first_solution(pred(out) is cc_multi, out, di, uo) is det.

	% implementation same as for `promise_one_solution'

Of course, this will only work if you have an io__state around.

> 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.

In Mercury, identity of first-order terms is not just syntactic.
Arithmetic is done with functions, i.e. by changing the equality
theory and using something similar to SLDE.

But in any case, for first_solution, the argument is a higher-order term.

> 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.

In the presence of separate compilation, how can the compiler figure out
whether a predicate will be called from inside a first_solution goal?
The first_solution goal may not even be written at the time the
predicate is compiled.

I guess it would be possible to leave that responsibility to the
programmer.

> (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.

That's what the compiler does for predicates with `cc' determinisms.
But for case (b), which we are trying to solve, we want to
be able to call them from a `det' predicate.  There is no way
the compiler can control where they are used (the caller may have
been compiled before the callee).

> 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.

The last condition here is the one which is causing difficulty.
Mercury's existing support for committed choice nondeterminism
lets you write code that depends on operational details, so long
as you don't care which solution is returned, and so long as you
don't mind that identical calls might return different 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.

Absolutely, I agree.  But support for these things doesn't require
identical calls to return identical solutions.  In other words,
ordinary committed choice is enough, you don't need Hilbert choice.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.