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

How? The arguments of foo and baz need not even have the same type.
 
> By the way, I don't think the connective should be ":-". 

Actually, my suggested syntax doesn't parse. Oops.

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

I'd rather not invent another connective just for this.

Maybe this would be better:

:- promise_exclusive(X::ground) is det where
	( foo(X)
	; baz(X)
	).
 
> 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)
> ].

The disjunction mimics how code using the promise is written.
It also has the correct variable scoping rules.
I don't see how a list is any more correct. The elements of
the "list" don't have the same type.
 
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
--------------------------------------------------------------------------