[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