[mercury-users] Mutually exclusive goals

[Peter Schachte]

On Thu, Jul 15, 1999 at 09:56:17AM +0100, Ralph Becket wrote:
> 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.

Nothing new there: if you write buggy source code, you get buggy
object code.  If you say goals are mutually exclusive when they're
not, then you'll fail to create a choicepoint in some cases where you
should, so some goals will fail when they should succeed.  If you say
a set of goals are exhaustive when they're not, you'll have some code
failing despite being det.  This seems like a bigger problem to me,
and it may be that the code generator would want to generate code that
counts on unverified assertions (or are these "specifications", to use
Fergus' nomenclature?) differently than code that counts on checked
declarations.

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

It might be that a fairly simple-minded checker would be quite useful.
It would be instructive to go through a large body of Mercury code,
(eg, the Mercury compiler) looking for code that works around this
problem.  It shouldn't be too hard to find places where exhaustiveness
declarations are needed, because they should have funny error goals
saying that the error should never happen.  I suspect that trying to
find places where exclusiveness declarations would help would be
pretty hard because they're probably all hacked around to make them
det.

Any Mercury hackers care to post some examples of where exclusivity or
exhaustiveness declarations would have helped?

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

Agreed.  It might also be useful to have an assertion "disprover"
which is invoked when the prover fails.  If the assertion can be
disproved, an error message could be issued.  As the prover and
disprover are improved, the infinite set of assertions that can
neither be proved nor disproved should get smaller and smaller, until
it's only a tiny infinite set :-).

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

Agreed.

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

Half-agreed.  The user should not be able to rely on
implementation-side assertions, but the compiler should.  Just because
the interface of a predicate says its multi, for example, doesn't mean
the compiler shouldn't (at the right optimization level) compile it
and its callers as if it's det, if it can prove the current
implementation actually is det.  This means that changing the source
for a module without changing the interface may require recompiling
client modules, but I think that's a fair trade-off when high
optimization levels are desired.

> > My guess is that it would
> > require a major modification of the language.

Nah, the change to the langauge should be pretty small, if you
introduce specialized declarations for exclusivity and exhaustiveness.
The changes to the compiler to support the language change would be
more significant.


-- 
Peter Schachte                     Any Idiot can face a crisis; it is this
mailto:schachte at cs.mu.OZ.AU        day-to-day living that wears you out.
http://www.cs.mu.oz.au/~schachte/      -- Anton Chekhov 
PGP: finger schachte at 128.250.37.3  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------