[m-users.] Confusion with inferencing for determinism

[Zoltan Somogyi]

On Tue, 18 Apr 2017 16:59:32 +0200, artem.kozlov at posteo.net wrote:
> The first immediate solution that I tried was:
> my_last([X], X) .
> my_last([_ | XS], X) :- my_last(XS, X) .

This code, and ...

> my_last(YS, X) :- (YS = [X] ; YS = [_ | XS], my_last(XS, X)) .

.. this code have the same determinism because in Mercury,
unlike in Prolog, clauses have the same semantics as disjunctions.

The reason why the Mercury compiler cannot prove that this
predicate cannot have more than one solution is because
as far it can see, it is possible for *both* disjuncts to generate
a solution in some cases. Specifically, if Ys = [X] succeeds,
then YS = [_ | XS] will succeed too. Both disjunctions unify
YS with the *same* function symbol, cons, so this disjunction
is *not* a switch. It is not a switch on the tail of YS either;
the first disjunct unifies it with nil, but the second does not
unify it with anything.
 
> it still nondet. In comparison to built in one:
> 
> my_last([H | T], Last) :- ( T = [], Last = H ; T = [_ | _], my_last(T, 
> Last)).
> 
> which is semidet.

The disjunction in this code has the two disjuncts unify the
same variable, T, with two *different* function symbols,
nil and cons, so this disjunction *is* a switch. Since the value
of T will be known before the switch, and since the value
cannot be both nil *and* cons at the same time, he compiler
knows that at most one arm of the switch will be able to
generate solutions.

Your code also tests the tail of Ys against both nil and cons,
but while it tests nil visibly in the first disjunction, it hides
the test against cons in the second disjunct inside the
recursive call. Determinism inference in Mercury is *local*;
it does not look across call boundaries.

The rules of determinism inference are described in section 6.2
of the Mercury reference manual. They are designed to be
simple and therefore easily predictable.

We know that determinism inference is incomplete,
in that it cannot always prove that a procedure has
at least one or at most one solution. However, this
incompleteness cannot be avoided even in theory,
because doing so would require a solution to the
halting problem.

Zoltan.