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

[Fergus Henderson]

On 04-Jan-2002, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Thu, Jan 03, 2002 at 09:16:14PM +1100, Simon Taylor wrote:
> > Would something like the following be better?
> > 
> > :- promise_determinism
> > 	all [X, Y]
> > 		( foo(X, Y)
> > 		; bar(X, Y)
> > 		)
> > 		is multi.
> 
> I understand and appreciate the meaning behind this syntax.  In some ways
> it's very nice and logical.  As you say, it matches how it will be used.
> It's just that I don't think it reflects the way people will naturally tend
> to think about what they're saying about the relationship between these
> predicates, and therefore I see it as more error-prone than the more direct
> statement about mutual exclusivity or exhaustiveness.  And since these are
> unchecked promises, being more error-prone is a serious problem.

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.

Note however that some of the quantifiers should precede the declaration.
E.g. for this example, it should be

	:- all [X]
	     promise_at_most_one_solution
	       some [Y] (foo(X, Y) ; bar(X, Y)).

Simon's example

        :- promise_determinism
 	    all [X, Y]
 		( foo(X, Y)
 		; bar(X, Y)
 		)
 		is multi.

reads to me as saying that the determinism of the goal
`all [X, Y] ( foo(X, Y) ; bar(X, Y) )' is multi,
but that goal has no free variables, so its determinism
can only be det or semidet.

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