[mercury-users] Confused about "undefined behaviour" of promise_only_solution

[Ralph Becket]

Hi Stefan,

Kral Stefan, Thursday, 25 November 2004:
> 
> I'd like to commit to one particular solution of a 
> non-deterministic predicate. I really do not care 
> which one (first, last, or anything in between).
> 
> Having read through parts of the "Net Talk"-page 
> "N-Solutions in Mercury and Declarativity", 
> I think I can get what I want by using promise_only_solution.

promise_only_solution should only be used when there really is only one
solution, but the compiler can't infer this for itself.

If there are multiple solutions and you only want one of them, you
should give your predicate a determinism of cc_multi or cc_nondet rather
than plain multi or nondet.  The `cc' stands for "committed choice" and
is a clean version of Prolog's cut.

Using cc code places restrictions on what you can do.  The main
constraint is that your program can never backtrack into a cc goal (the
compiler detects this situation and reports an error).  The other
constraint is that any predicate which calls a cc predicate must itself
be cc (and this fact must be reflected in its determinism category).

The only way out of cc space is to wrap a call to a cc predicate with
promise_only_solution.  But you must be sure that this is really
warranted: if you lie to the compiler (not to mention other people
reading your code) then bad things will eventually happen.

> Then again, I am puzzled by section 6 of the mercury reference 
> manual, which explains the meaning of the predicate and states 
> "If the assumption [that there are no solutions X1, X2 for 
> which X1 \= X2 holds] is not satisfied, then the behaviour 
> is undefined."

Say I have a predicate p which, on backtracking, enumerates solutions
p(X1), p(X2), ..., p(Xn) and I know that X1 = X2 = ... = Xn then I can
safely wrap the call to p with promise_only_solution and prevent any
pointless backtracking into p in my program.

N.B. X1 = X2 = ... = Xn is just another way of saying
forall i, j in 1..n . not(Xi \= Xj)

> So far, so good -- I think I'm all confused...
> 
> 1) "Undefined" sounds very hard, in fact a bit repulsive, just 
>    like the possible effects of turning of checks of array indices.
>    The way I see it is that "If the assumption is not satisfied, 
>    then promise_only_solution returns an arbitrarily chosen solution 
>    of 'Pred(X)'."   Is my interpretation correct?

"Undefined" means "all bets are off".  Anything could happen.  So you
don't want to go there.  (*Anything* probably wouldn't happen, but you
are likely to end up with a program that doesn't do what you expect and
is a screaming nightmare to debug.)

> 2) In my app the predicate of interest has many syntactically 
>    different, but semantically equivalent solutions.
>    Is is okay to use promise_only_solution within this case?

Ahh, it sounds as though what you want is user-defined equality.
User-defined equality is useful where, say, you want to represent sets
using unordered lists.  In this case you would like Mercury to recognise
the following identities: [1, 2, 3] = [1, 3, 2] = [1, 1, 3, 1, 2] = ...
You can do this by supplying your own equality predicate for your set
type.  The reference manual section on this point is typically terse; if
you want some help on this aspect of Mercury just ask on the mailing
list.

Cheers,
-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------