[mercury-users] Mutual Exclusivity & Exhaustiveness

[Lars Yencken]

> > :- 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, _).

It was my intention that X and A were universally quantified above, implicitly.
The extra syntax might be unnecessary. 


> > :- exclusive foo(X,Y,_A), bar(X,Y), bat(_B), mop(Y,_C).
> 
> This looks a bit strange to me.

It is very similar to your example above, except that I left A, B and C in.
Equivalently, taking them out we get

:- exclusive foo(X,Y,_), bar(X,Y), bat(_), mop(Y,_).

with X and Y implicitly universally quantified.

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

My intention was that variables A, B and C were to be existentially quantified,
and as such would be possible output variables.

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

You're probably right.


Thanks!

Lars

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