[mercury-users] determinism question

[Fergus Henderson]

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.
> 
>   :- pred p(int::out, list(int)::in,list(int)::out) is semidet.
>   p(0) --> [0].
>   p(N) --> [1],p(Tmp), {N is Tmp+1}.
>   p(N) --> [2],p(Tmp), {N is Tmp+2}.
>   p(N) --> [3],p(Tmp), {N is Tmp+3}.
> 
> 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.
> test.m:022:   Declared `semidet', inferred `nondet'.
> test.m:023:   Disjunction has multiple clauses with solutions.

In general, code which is logically equivalent may not be equivalent as
far as the compiler's determinism checking is concerned.  Determinism
and logical equivalance are both undecidable properties, in the general
case.  The compiler's determinism checking algorithm rejects code which
it cannot prove is determinism-correct.  If you write code which the
compiler cannot prove is determinism-correct, then you may need to
express it differently in order to get the compiler to accept it.  But
generally this is not difficult to do.

>   :- pred p(int::out, list(int)::in,list(int)::out) is semidet.
>   p(X) --> p0(X) ; p1(X) ; p2(X) ; p3(X).
>   
>   :- pred p0(int::out, list(int)::in,list(int)::out) is semidet.
>   :- pred p1(int::out, list(int)::in,list(int)::out) is semidet.
>   :- pred p2(int::out, list(int)::in,list(int)::out) is semidet.
>   :- pred p3(int::out, list(int)::in,list(int)::out) is semidet.
>   p0(0) --> [0].
>   p1(N) --> [1],p(Tmp), {N is Tmp+1}.
>   p2(N) --> [2],p(Tmp), {N is Tmp+2}.
>   p3(N) --> [3],p(Tmp), {N is Tmp+3}.
> 
> 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?  

If it did that, then the determinism-correctness of p/1 would depend
not only on the declarations of p0, p1, p2, and p3, but also on their
definitions.  This would be a violation of abstraction -- the
declarations (and documentation) should specify the interface, and
callers should depend for their correctness only on the documented
interface, not on the implementation details.

> You'd need to make sure that you didn't unfold so much that it looped at
> compile time.

That is of course easier said than done ;-)

So, to avoid violating abstraction, and to minimize compilation time,
the determinism checking algorithm does not do unfolding.

As mentioned above, it should be easy to rewrite your program
in a way that is acceptable to the compiler.  In the case of
your simple example, you showed this yourself -- the original
code with just p/1 and without p1, p2, p3, and p4 works fine.
But probably your question stems from a real program that is
a bit more complicated than the example you posted.  If you
want suggestions on how to structure the code in your real
program so that the compiler can infer the right determinism,
then we would need more information about your program.

Cheers,
	Fergus.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.