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

[Fergus Henderson]

On 04-Jan-2002, Lars Yencken <lljy at students.cs.mu.oz.au> wrote:
> > I don't think mutual exclusion is necessarily the right concept to
> > use here anyway.  The property that we need for determinism analysis
> > is that the disjunction has at most one distinct solution; mutual
> > exclusion of the disjuncts is a sufficient but not necessary condition.
...
> 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. 

No -- if you declare that this disjunction has exactly one solution,
then the compiler could safely infer that any disjunction
containing a subset of the disjuncts has at most one solution.
Hence it should consider such switches to be semidet rather than nondet.

So there's no difference between mutual exclusivity and
`promise_exactly_one_solution' here.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------