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

Lars Yencken lljy at students.cs.mu.oz.au
Fri Jan 4 15:34:42 AEDT 2002

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