[mercury-users] Newbie problem. :)

Richard A. O'Keefe ok at atlas.otago.ac.nz
Thu Jun 17 14:45:50 AEST 1999


	On Thu, 17 Jun 1999, Thomas Conway wrote:
	
	> If you restrict the declarations so that I can only declare
	> mutual exclusion for predicates defined in *this* module,
        > then checking should be possible.
	
    Robert Ernst Johann JESCHOFNIK <rejj at students.cs.mu.oz.au> wrote:
	
	This seems to be the intuitive way to do it, anyway.. I find it odd that
	people would suggest otherwise. As long as a module can export its mutual
	exclusion rules along with the exported predicates, then there should be
	no problem.
	Making an assertion like this about predicates you have imported from
	elsewhere seems.. well.. daft, as you have no information about their
	implementation.

What has it got to do with *implementation*?
Exclusion rules are claims about the *meaning* of predicates.
If I say that 'reliable(X)' and 'implemented_in(X, c_plus_plus)'
are incompatible, this has **NOTHING** to do with how they are
implented, and everything to do with what they mean.

What's more, people who think it is "daft" for an exclusion rule
to mention predicates imported from elsewhere just haven't thought
about it hard enough.  For example, suppose someone *else* has
written a linear algebra package which exports a `singular(Matrix)'
predicate.  Suppose I find it necessary to add a
`positive_definite(Matrix)' predicate.  Why should I be forbidden
to say that

    :- positive_definite(M), singular(M).

just because I didn't write *all* the predicates in the rule?
Or how about another example.  Suppose I would like the compiler
to know that all prime numbers are positive.  What I would really
like to say is

    N > 1 :- prime(N).

but of course I can't do that.  What I _might_ be able to write is

    :- prime(N), N =< 1.

Here again, (=<)/2 is imported from another module, not the one
defining prime/1.  Why should I be forbidden to write this just
because someone else defined (=<)/2?

In general, verifying that a negative rule is a consequence of
the positive rules may be impossible.  That's one reason why
you have to declare them.

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



More information about the users mailing list