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

[Lars Yencken]

> 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.
> 
> For example, if you have
> 
> 	foo(yes, 1).
> 
> 	bar(yes, 1).
> 	bar(no, 2).
> 
> 	:- pred p(X::in, Y::out) is det.
> 	p(X, Y) :- foo(X, Y) ; bar(X, Y).
> 
> then for any given X the disjunction `foo(X, Y) ; bar(X, Y)' has
> at most one solution Y, even though the disjuncts are not mutually
> exclusive (for X = yes, both disjuncts will succeed, but they'll
> return the same answer Y = 1).  So it would be nice if the compiler were
> to allow code which relies on this, such as p/2 here.
> 
> Hence, rather than `promise_exclusive' and `promise_exhaustive' declarations,
> I think it would be better to have either `promise_determinism' declarations,
> as Simon suggested, or `promise_at_most_one_solution',
> `promise_at_least_one_solution', and `promise_exactly_one_solution'
> declarations.  These both solve the code duplication problem for things
> that are both exhaustive and exclusive.

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.

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