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

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


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([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 
verpacken.m:093:   inside the case [|](V_23, V_22) of the switch on 
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 


More information about the users mailing list