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

[Ralph Becket]

Kral Stefan, Saturday, 27 November 2004:
> 
> Hi All.
> 
> Thanks for all of your answers.
> 
> On Fri, 26 Nov 2004, Ralph Becket wrote:  
> > 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). [...]
> > 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. 
> Sound like green cuts. However, I want to do something red, just like 
> 	( member(X, Xs), someTest(X) -> true ).
> 
> It's red, but not so bloody red, so I can fold the test into
> member, yielding a semi-det predicate that uses higher-order
> features, findfirstsuchthat(X,Xs,someTest).

There's nothing dodgy about that (you don't need a cut).  I've often
wanted a function like this; I think I'll add it to the library.

> But I am not too happy with that approach, either, because the actual
> problem is a lot more complicated. 
> 
> Suppose, I want to write a committed-choice term rewriting system
> (that does not give actual guarantees about the order in which rules
> are tried), can I actually write nondeterministic code and then 
> commit at every step or do I have to write a deterministic program
> to do the job? (Representing rules as data, instead of being able 
> to compile them into actual code.)

A predicate with a committed choice determinism category is akin to a
Prolog predicate with a cut at the end of each clause.  The difference
with mercury is that if a calls b and b is cc_something then a must be
cc_something, too.  Unlike Prolog, however, a cannot backtrack into b.

Your problem outline suggests that cc code is what you want, unless you
need to backtrack over this stuff, in which case perhaps you could give
us a small example - then we could make more concrete suggestions.

> > Ahh, it sounds as though what you want is user-defined equality.
> That sounds very good, and like a lot of work.

It's more work than most people would like, but if you absolutely have
to have it, you can.

> Maybe I should reformulate my original question. 
> My applications usually look something like this:
>    p(S0,S) :-
> 	( multipart1(S0,S1) -> true ),	% some CC term-writing
> 	detpart1(S1,S2),
> 	( multipart2(S2,S3) -> true ),	% some DFID for instr. sel.
> 	detpart2(S3,S4),
> 	...,
> 	detpartN(Sn,S).

If I understand you correctly, if any multipart call fails then p must
fail, otherwise any multipart solution is immediately committed.

One way to write this in Mercury is as follows (I'll use state variable
notation rather than S0, S1, ...):

:- pred p(...) is cc_nondet.

p(!S) :-
	( multipart1(!S) ->
		detpart1(!S),
		( multipart2(!S) ->
			...
			( multipartN(!S) ->
				detpartN(!S)
			;
				fail
			)
		;
			fail
		)
	;
		fail
	).

:- pred multipart1(...) is cc_nondet.
:- pred multipart2(...) is cc_nondet.
...
:- pred multipartN(...) is cc_nondet.

> Do I have to fundamentally restructure my application to do this
> in Mercury? I have not yet understood the idea behind the
> cc-modes. Does it all boils down to "Do not care that the 
> program declaratively describes zillions of solutions, or
> indeed does not terminate universally. Just declare 
> everything non-deterministic as CC-nondet/CC-multi, 
> and think of the program exit as some kind of red cut."?

A committed choice determinism category expresses the idea that you are
interested in (at most one) solution and that therefore the compiler can
compile your predicate as though it were (semi)det and avoid mucking
around with non-determinism stacks and so forth.  In that sense it's a
kind of optimization.  However, in order to preserve the declarative
reading of your program under this optimization, you can never backtrack
into a cc predicate.  So cc determinism categories are quite
restrictive.  In practice you usually use them in situations where you
know that all solutions to a given predicate are effectively equal, in
which case you can mark the predicate as cc and wrap calls to it in
promise_only_solution if necessary.

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