[m-users.] Confusion with inferencing for determinism

artem.kozlov at posteo.net artem.kozlov at posteo.net
Wed Apr 19 01:58:01 AEST 2017


Thank you for the explanation!
Let me clarify that I understood it properly:
So basically if I call my_last(["a"], Res), the first disjunct will 
unify as well as second one, because ["a"] is equivalent to ["a" | []], 
even so later it will fail in the recursive call because there is no 
match for empty list.
But because inferencing is *local*, without going deep into the 
recursion we possible can get values from both clauses, right?


Artem.


On 18.04.2017 17:35, Zoltan Somogyi wrote:
> 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.


More information about the users mailing list