[mercury-users] determinism question

[Peter Schachte]

On Tue, Nov 03, 1998 at 07:59:55PM +1100, Fergus Henderson wrote:
> On 03-Nov-1998, Don Smith <dsmith at cs.waikato.ac.nz> wrote:

> > For the following code, the Mercury compiler is able to verify
> > the determinism declaration.
...
> > But for the following logically equivalent code, the compiler says
> > test.m:022: In `p(out, in, out)':
> > test.m:022:   error: determinism declaration not satisfied.
...
> > Couldn't the compiler unfold the definitions of p0, p1, p2, and p3 and
> > thereby infer that the disjuncts in the rule for p/1 are mutually exclusive?  

I believe Fergus's point is that if you make the correctness
(acceptability to the compiler) of a predicate depend on properties
inferred about /other/ predicates, then it becomes possible for
changes to one predicate to make another unacceptable to the compiler.
That should be avoided.  I agree.

I think Don's point is that within a single module the compiler ought
to be free to do anything to make the compiled code more efficient.
Since det code is more efficient than nondet code, the compiler should
feel free, within a module, to implement a nondet predicate without
using the nondet stack when it safely can.  I agree with this too.
But that doesn't mean the compiler should accept a det declaration for
such a predicate.  If the rules the compiler uses to determine
determinism aren't reasonably straightforward, it'll be hard for users
to predict which predicates will be accepted as det and which won't.
Don's frustration at the compiler's unwillingness to accept his second
example predicate when it accepted the first would be much greater if
it accepted the second, but refused the accept a third which was
different from the second in a subtler way.

The problem here, it seems to me, is that the user doesn't have very
good control over Mercury's perception of the property that decides
determinism: mutual exclusion of goals.  If a program is rejected as
mode-incorrect, you can alway go and add more modes for some of the
predicates it calls to make it mode-correct.(1) If you can't, then
your program is buggy, and you thank the Mercury compiler and go fix
it.  If a program is determinism-incorrect, however, you have to edit
the code to fix it.  There is no way to declare two goals to be
mutually exclusive.

Perhaps the solution to this problem is to allow users to make
promises of exclusivity.  Something like

	:- promise_exclusive p(X), q(X), X = r(Y).

which means

	for all X,Y : ((p(X) <=> not q(X)) and
	               (p(X) <=> not X=r(Y)) and
	               (q(X) <=> not X=r(Y))).

These promises could be put in interface or implementation sections.
The compiler would be required to consider all visible declared
exclusions in determinism analysis.  This shouldn't be a big
performance penalty in the compiler because it doesn't require a
many-step derivation to see if two things are exclusive.  Either
they've been declared to be exclusive or they haven't.

This proposal has another thing to recommend it: it helps type
classes.  append(in, in, out) is accepted to be det because the
compiler knows that the []/0 and ./2 constructors are mutually
exclusive.  If you have a sequence type class that has empty/1 and
first_rest/3 predicates (or, nicer still, []/0 and ./2 functions!),
the compiler won't be able to determine that append(in,in,out) on this
type class is det, because it won't know that the empty/1 and
first_rest/3 predicates are mutually exclusive.  If you allow
exclusivity promises in type classes, and make that require the
corresponding promises in instances, you fix this deficiency.

_____
(1) Of course, to get the compiler to accept the new modes you've
    added for the other predicates, you may have to go and add more
    modes for still other predicates, ad nauseum.  This is because
    Mercury doesn't give you a concise (or any) way of specifying what
    modes a predicate /could/ support without specifying that you
    acutally want to generate code for that mode.


-- 
Peter Schachte                | Nearly all men can stand adversity, but if
mailto:pets at cs.mu.OZ.AU       | you want to test a man's character, give him
http://www.cs.mu.oz.au/~pets/ | power.
PGP: finger pets at 128.250.37.3 |     -- Abraham Lincoln