[mercury-users] Can one_solution/2 and unsorted_solutions/2 be det?

[Fergus Henderson]

Don Smith, you wrote:
> Many algorithms include statements of the form "choose an arbitrary member
> of set S with property P ...".

Absolutely. 

The way this is spelt in Mercury is `mode p(...) is cc_multi'
(or `cc_nondet', if S can be empty).

> Mehmet Orgun (Macquarie U, in Sydney) and William Wadge (University
> of Victoria, Canada) have a paper "Extending Temporal Logic Programming
> with Choice Predicates Non-determinism" (to appear in Journal of Logic
> and Computation, also available on their web page).    They write:
> 
>    The problem is that, in many cases, we are interested in only one
>    solution to a given goal, but we do not want to make the choice
>    unnecessarily specific ...

This is exactly the problem which Mercury's support for committed choice
nondeterminism was designed to solve.  Personally I think that it does a
pretty good job.

> They investigate the model-theoretic of TLP with choice predicates and
> give some applications.   One thing they note is that if there are
> multiple calls to a choice predicate with the same input arguments,
> then the same output solutions must be chosen, to guarantee
> correctness.  It's as if the interpreter is parameterized by some
> arbitrary function for choosing solutions to choice predicates.
>
> Another way to think of this, I suspect, is that we are extending the logic 
> with Hilbert-style choice functions (epsilon operators):

Hilbert-style choice functions are great for mathematics and
specifications, but they're not very good for programming languages,
because they can't be implemented efficiently.
The simplest implementation would be to calculate all solutions and
then find the maximum, and as you note yourself, this is silly.

Note that it would _not_ be correct for an implementation to just
choose the first solution found.  For example, there might be two
logically equivalent predicates (with different predicate names) for
which the solutions are computed in a different order, yet the
semantics says that the chosen solution must be the same in both cases.

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