[mercury-users] Mutual Exclusivity & Exhaustiveness

[Peter Schachte]

On Thu, Jan 03, 2002 at 09:16:14PM +1100, Simon Taylor wrote:

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

Why?  They're not required on goals, why should they be required here, where
it's as least as clear what is intended?  I expect in most cases, all
variables will be universally quantified, and in most of the rest of the
cases, all non-universally quantified variables will be underscores.  I'd
rather keep the declaration as simple as possible, as long as it's clear.

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

It's a question of how you look at it.  I think of these declarations as
specifying that certain atoms are mutually exclusive and/or exhaustive.
You're looking at it as specifying that a certain disjunction of atoms has a
certain determinism.  Granted, this is how we are proposing to use this
information, but it's not the only way we could use it, and it's not the
way I expect users want to think about it.

I think I'm more likely to accidentally say that a disjunction is multi when
I really meant that it is semidet than I am to say that a set of atoms is
exhaustive when I meant that they are mutually exclusive.

> Would something like the following be better?
> 
> :- promise_determinism
> 	all [X, Y]
> 		( foo(X, Y)
> 		; bar(X, Y)
> 		)
> 		is multi.

I understand and appreciate the meaning behind this syntax.  In some ways
it's very nice and logical.  As you say, it matches how it will be used.
It's just that I don't think it reflects the way people will naturally tend
to think about what they're saying about the relationship between these
predicates, and therefore I see it as more error-prone than the more direct
statement about mutual exclusivity or exhaustiveness.  And since these are
unchecked promises, being more error-prone is a serious problem.

It also opens up other questions, like what if I replace the last line with
"is failure" or "is cc_nondet"?  The first makes sense but can't add any
information, since if the disjunction is false, than each disjunct is
individually.  The second makes no sense at all.


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