[m-users.] Why has this the determinism category "nondet"?

Volker Wysk post at volker-wysk.de
Sat Feb 16 06:42:23 AEDT 2019


Hi!

I'm learning Mercury, and have this little predicate, which computes the 
longest common prefix of two lists:

:- pred vorder(list(T)::in, list(T)::in, list(T)::out) is det.

vorder([X|A], [X|B], [X|C]) :-
   vorder(A,B,C).

vorder([X|_], [Y|_], []) :-
   X \= Y.

vorder([_|_], [], []).

vorder([], [_|_], []).

vorder([], [], []).

The compiler complains:

verpacken.m:010: In `vorder'(in, in, out):
verpacken.m:010:   error: determinism declaration not satisfied.
verpacken.m:010:   Declared `det', inferred `nondet'.
verpacken.m:093:   Inside the case [|](V_21, V_20) of the switch on 
HeadVar__1:
verpacken.m:093:   inside the case [|](V_23, V_22) of the switch on 
HeadVar__2:
verpacken.m:093:   disjunction has multiple clauses with solutions.
verpacken.m:093:   In argument 2 of clause head:
verpacken.m:093:   unification with `X' can fail.
verpacken.m:097:   Negated goal can succeed.

So this is "nondet", not "det". But why? To me it looks like it's 
deterministic. It really computes only one solution (I've tested with 
solutions.solutions/2).

Thanks
Volker




More information about the users mailing list