# determinism question

Don Smith dsmith at cs.waikato.ac.nz
Tue Nov 3 19:15:53 AEDT 1998

```Hello,

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.

:- 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?
You'd need to make sure that you didn't unfold so much that it looped at
compile time.

Don

```

More information about the users mailing list