[mercury-users] Mutual Exclusivity & Exhaustiveness

[Ralph Becket]

Lars Yencken, Thursday,  3 January 2002:
> > > :- 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. 

I don't think you can get away that easily!  But I think you have a
point - we can make all goal variables implicitly universally
quantified, but we do need to specify which variables have to be inputs
for the constraint to apply.

Perhaps

	:- exclusive [X, Y] (p(X, Y), ...)).

if we make exclusive a 2-place prefix operator.

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

I just meant that it was a strange thing to declare, which begs the
question of whether there are certain classes of exclusivity
declarations that are identifiable as probably errors?

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

Either way, you get the same result!

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