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

[John Staples]

On Sun, 26 Oct 1997, Don Smith wrote:

> Many algorithms include statements of the form "choose an arbitrary member
> of set S with property P ...".    Since it does not matter which element
> is selected, it is perfectly OK, in particular, to let the runtime system 
> break the symmetry and arbitrarily choose for us.  In fact, it is burdensome
> to do otherwise.    (For example, it's silly to have to calculate all solutions
> and then find the maximum, just to get a single solution.)
> 
> 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 ...
> 
> 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):
> <http://lal.cs.byu.edu/lal/holdoc/info-hol/02xx/0290.html>.
> 
I buy into this discussion with some misgivings, because I haven't
followed it from the beginning, but my experience is that the Hilbert
epsilon operator is widely misunderstood in the computing community as a
nondeterministic choice operator. It's a choice operator, but not at all
nondeterministic. That is, every reference `epsilon x P' (without free
variables) refers to the *same* choice (semantically - i.e. relative to a 
given model of the syntax). One might say that all the choices have been
made when the semantics is chosen (or by God, or by Hilbert!) 

When people
propose to implement this operator using the run-time system, however,
they often have in mind to allow a new choice at every reference, which is
not Hilbert's idea, and not referentially transparent.

Apologies to Don if all this is implicit in the accumulated discussion.

John Staples