[mercury-users] Mutual Exclusivity & Exhaustiveness

[Peter Schachte]

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.

If you like, you can throw in the requirement that at least one variable
should be shared by all the atoms, though that's not strictly correct.  For
example

	:- exclusive true, fail.
	:- exhaustive true, fail.

are quite correct (though not very interesting, so it would be OK to add the
restriction).

> > > What about possible output variables?

Modes have nothing to do with the meaning of the declaration, only with when
they can be used.

There should probably be some statement of the semantics of these
declarations.  Here's what I would suggest:

	:- exclusive p(X), q(X,Y), r(X,Y,Z).

means

	( all [X,Y} p(X) => \+ q(X,Y), \+ (some (Z) r(X,Y,Z)) ),
	( all [X,Y} q(X,Y) => \+ p(X), \+ (some (Z) r(X,Y,Z)) ),
	( all [X,Y} (some (Z) r(X,Y,Z)) => \+ p(X), \+ q(X,Y) ).

and

	:- exhaustive p(X), q(X,Y), r(X,Y,Z).

means

	( all [X,Y] p(X) ; q(X,Y) ; (some (Z) r(X,Y,Z)) ).


On Thu, Jan 03, 2002 at 12:06:36PM +1100, Simon Taylor wrote:
> On 03-Jan-2002, Lars Yencken <lljy at students.cs.mu.oz.au> wrote:
> > 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.
> 
> 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.  So I think Lars' proposal is better because it's much simpler
and easier to read.

OK, one can construct cases where one could give better exclusivity (but not
exhaustiveness) information with explicit insts than using the implicit
ground inst for all the universally quantified variables.  But I don't think
the number of times that would actually be useful justifies the much more
complicated syntax.

> It should be explicitly stated in the declaration that the programmer
> is making a promise that the compiler cannot check, so use
> `promise_exclusive' rather than `exclusive'.

That's a good point.

> I'd suggest something like this:
> 
> 	% exhaustive match.
> :- promise_exclusive(X::ground, Y::ground) is det :-
> 	( X < Y
> 	; X = Y
> 	; X > Y
> 	).
> 
> 	% non-exhaustive match.
> :- promise_exclusive(X::ground, Y::ground) is semidet :-
> 	( foo(X, Y)
> 	; bar(X, Y)
>  	).

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

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.  The simpler syntax
doesn't:  it's just a list of atoms.

And how do you declare foo/2 and bar/2 exhaustive but not exclusive in this
syntax?


-- 
Peter Schachte              I have not yet begun to procrastinate. 
schachte at cs.mu.OZ.AU        
www.cs.mu.oz.au/~schachte/  
Phone: +61 3 8344 9166      
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------