Can one_solution/2 and unsorted_solutions/2 be det?

[Don Smith]

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

Fergus wrote:
> But [regarding one_solution/2 as deterministic] is only safe if there really 
> is only one solution to the predicate, logically speaking.  
With choice predicates, there really is only one solution!  And this is just what
we want.

  Don (dsmith at cirl.uoregon.edu)