[mercury-users] Mutual Exclusivity & Exhaustiveness

[Ralph Becket]

Simon Taylor, Thursday,  3 January 2002:
> 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)
> 		).

Hmm, from the above we can infer

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

which supports

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

So I'm not convinced that the above should necessarily be disallowed.

> The restriction above might be too restrictive.

Perhaps the restriction should be that there should be a non-empty
subset of the head variables that appears in each disjunct.

By the way, I don't think the connective should be ":-".  The usual
reading of "P :- Q" is "P if Q".  What we're trying to say here is
that the LHS implies the RHS!  So something like `for` would be a better
choice.

Going further, the use of disjunction is wrong, too.  Maybe a plain list
would be better:

:- promise_exclusive(X::ground) `for` [
	foo(X)
	bar(X, _)
	baz(X)
].

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

True.

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

I agree.

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