[mercury-users] Mutual Exclusivity & Exhaustiveness

[Simon Taylor]

On 03-Jan-2002, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Thu, Jan 03, 2002 at 12:15:57PM +1100, Ralph Becket wrote:
> > Lars Yencken, Thursday,  3 January 2002:
> > > > 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.
> 
> I think you *can* get away that easily.  Mercury's usual rule that variables
> are quantified as tightly as possible works fine here.  Or specialize it this
> way:  variables appearing in more than one atom in an exclusive or
> exhaustive declaration are universally quantified in all of them; variables
> appearing in only one are existentially quantified over that atom.

I'd prefer that the universally quantified variables be explicitly stated.

> On Thu, Jan 03, 2002 at 12:06:36PM +1100, Simon Taylor wrote:
> > You need to be able to declare the required instantiatedness of the
> > non-local variables for the pattern to match. You don't want to use
> > the rule `:- exclusive X = [], X = [_|_]' when X is not bound.
> 
> That's implicit.  The meaning of the declaration is clear without mode
> information. 

OK.

> Isn't :: supposed to be used for modes?  Is there another context in which
> it's used for insts?  This could be confusing.

Yes, but as you pointed out we can do without the insts.
 
> This is the way a compiler-writer would like to think about these
> declarations, not the way a user wants to see them.
> The syntax forces you to place restrictions on what goals are allowed
> where.

I don't understand your point. The layout of the goals in the promise
matches the way the promise is used.

> The simpler syntax doesn't:  it's just a list of atoms.

My suggested syntax is just a list of atoms separated by semi-colons.
 
> And how do you declare foo/2 and bar/2 exhaustive but not exclusive in this
> syntax?

Would something like the following be better?

:- promise_determinism
	all [X, Y]
		( foo(X, Y)
		; bar(X, Y)
		)
		is multi.

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