[mercury-users] Mutual Exclusivity & Exhaustiveness

[Ralph Becket]

Lars Yencken, Thursday,  3 January 2002:
> 
> Hi everyone
> 
> I'm digging up the topic of mutual exclusivity and exhaustiveness
> declarations again, in the interest of actually developping them. For
> past posts on this topic, do a search for determinism detection on the
> mailing lists. The declarations I had in mind were quite simple, like
> these below:
> 
> :- exclusive X < A, X = A, X > A.
> 
> :- exhaustive X < A, X = A, X > A.

Presumably you're constraining all arguments to be ground?

Perhaps it would be better to have the declaration look like

:- all [X, Y] exclusive p(X, Y), q(X, Y, _), r(X, Y, _).

with the constraint that the declaration only applies when X and Y are
ground, but allowing q/3 and r/3 to also have output variables.

[Question: is groundness required?  What about if some arguments are
partially instantiated?  Or unused?]

Ditto for `exhaustive'.

> Places where these declarations would be useful have currently been
> hacked around using if-then-else's. This change would allow the
> programmer to state the exclusiveness/exhaustiveness explicitly rather
> than assuming it and continuing. The actual implementation of it will
> have the compiler do the if-then-else rearranging instead.
> 
> It should aslo handle declarations like the following, where many
> different predicates of different variables are used, although I
> imagine it to be more rare that an example like this will be used:
> 
> :- exclusive foo(X,Y,_A), bar(X,Y), bat(_B), mop(Y,_C).

This looks a bit strange to me.

The above declaration is equivalent to the formula

	all [X, Y, A, B] (
		not (foo(X, Y, A),  bar(X, Y)), 
		not (foo(X, Y, A),  bat(B)), 
		not (foo(X, Y, A),  mop(Y, C)), 
		not (bar(X, Y),     bat(B)), 
		not (bar(X, Y),     mop(Y, C)), 
		not (bat(B),        mop(Y, C))
	)

But this is equivalent to saying that if there is *any* solution to
bat/1 then no solutions exist for the other goals.

What about possible output variables?

> Does anyone have any suggestions or comments? I'm also stumped for a
> good way of declaring both at once.

Exclusivity and completeness are orthogonal.  Since it's so easy to do a
cut'n'paste job when you want both, I wouldn't worry about having a
combined declaration.

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