[m-dev.] Re: [mercury-users] Mutual Exclusivity & Exhaustiveness

[Lars Yencken]

On 04-Jan-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Lars Yencken, Friday,  4 January 2002:
> > 
> > There are also big advantages to being able to declare mutual exclusivity 
> > though. For example, if I could declare
> > 
> > 	:- all [X, Y] promise_exactly_one_solution (
> > 		X < Y
> > 		; X = Y
> > 		; X > Y
> > 	).
> > 
> > then a switch on just two of these would be considered nondet by the compiler 
> > instead of semidet, unless all 3 pairs of ordered signs were also declared 
> > using promise_at_most_one_solution. 
> >
> > If we don't use exclusivity declarations, then every time we do a partial 
> > switch instead of a full one our promised solutions are useless to us.
> 
> No - a disjunction cannot acquire more solutions by removing disjuncts!
> 
> Removing any two (or even one) of the above disjuncts may lead to
> semideterminism or failure, but not nondeterminism.

Sorry, you're right. We can still use the information to limit the partial
switch to one solution.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------