[mercury-users] Mutually exclusive goals

[Ralph Becket]

Robert Bossy wrote on 15 Jul:
> 
> The point is, the mutual exclusion can't be left unchecked because
> Mercury is a LP language (isn't it a good reason?). Hey! What if I
> declare exclusion that is not actually correct? My software will be
> false (not exclusive) or buggy.

Hmm.  What you are asking for here is a complete and consistent
theorem prover with *extensive* knowledge of the program's environment
etc.  This is a Very Hard Thing to do and I don't believe this
approach is feasible.

Of course, one could have a fast, incomplete theorem prover for
exclusivity assertions that rejects formulae that are too hard for it
to prove (in the same sense as the current mode/determinism checker),
although I suspect that getting a useful version of such a thing would
be a nightmare.

I would be happy with unverified exclusivity declarations, treating them
in the same way as I would declarations about the type, mode and
determinism of a predicate implemented in C.  By all means include an
optional checker, like termination analysis, but don't make its use
mandatory.

As an aside, exclusivity declarations should be treated differently
depending upon which side of the `:- implementation' marker they fall.
A declaration in the interface is one which can be exploited by
importing code.  A declaration in the implementation section should
not escape since it presumably says something about that particular
implementation.  For example, I might have a set datatype whose
interface is a list of unique members, but whose implementation is as
a sorted list.  I don't want users of this datatype relying upon my
current implementation choice.

> X < Y and X >= Y always fails (can't succeed)
> X < Y or X >= Y always succeeds (can't fail)
> 
> 
> It seems that we want to declare a determinism according to
> unification (X and Y) instead of mode! My guess is that it would
> require a major modification of the language.

I don't understand: what have modes got to do with it?

Ralph

-- 
Ralph Becket  |  rwab1 at cam.sri.com  |  http://www.cam.sri.com/people/becket.html
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------