[mercury-users] Mutual Exclusivity & Exhaustiveness

[Simon Taylor]

On 03-Jan-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Simon Taylor, Thursday,  3 January 2002:
> > 2. All of the variables in the head of the rule must appear in each disjunct.
> 
> Why is that necessary?

We definitely want to disallow examples like:

:- promise_exclusive(X::ground, Y::ground) is det :-
		( foo(X)
		; bar(X, Y)
		; baz(Y)
		).

The restriction above might be too restrictive.

> I might want to say something like
> 
> :- promise_exclusive(X::ground, Y::ground) is semidet :-
> 	(	X = 0
> 	;	X `is_positive_divisor_of` Y
> 	).

The exclusivity of this example does not depend on the value of Y.
It should just be written as:

:- promise_exclusive(X::ground) is semidet :-
 	(	X = 0
 	;	X `is_positive_divisor_of` Y
 	).

The kind of case where it is useful to have a variable occur in only
some of the disjuncts has the form (I can't think of a real example):

:- promise_exclusive(X::ground, Y::ground) is semidet :-
		( p(X)
		; q(X, Y)
		; r(X, Y)
		).

Maybe we only need to require that one head variable occurs
in all the disjuncts?

Simon.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------