[mercury-users] Why is mode member(in, in) semidet?

[Jeff Thompson]

Thanks for the detailed reply.  I'm trying to avoid Mercury code that 
compiles to throw an expensive Commit exception and I'm glad to see that 
the compiler is able to do this kind of "one solution" without throwing 
an exception.

Thanks,
- Jeff

On 3/4/2012 2:07 PM, Paul Bone wrote:
> On Sun, Mar 04, 2012 at 11:40:56AM -0800, Jeff Thompson wrote:
>> Hello.  I would like to check my understanding here.  List member is
>> defined as:
>>
>> member(X, [X | _]).
>> member(X, [_ | Xs]) :- member(X, Xs).
>>
>> It is counter-intuitive to me why mode member(in, in) is semidet.
>> If you call member(1, [1, 1]), why doesn't the code above match
>> twice which would make this mode nondet?
>>
> Good question.
>
> Remember that each predicate is compiled separately per mode, so the modes are
> known within the procedure body (this is one of the things that makes Mercury
> fast and awesome).  Looking at the modes and the disjunction within member we
> see:
>
> member(Y, [X | Xs]) :-
>      Y :: in, % Not actually mercury syntax.
>      X :: in,
>      Xs :: in,
>      (
>          Y = X
>      ;
>          member(Y, Xs)
>      ).
>
> Normal determinism checking (such as you suggest) would say that the
> disjunction has between 0 and unbounded solutions.  However, the reference
> manual says:
>
>      "If the inference process below reports that a goal can succeed more than
>      once, but the goal generates no outputs that are visible from outside the
>      goal, and the goal is not impure (see Impurity), then the final determinism
>      of the goal will be based on the goal succeeding at most once, since the
>      compiler will implicitly prune away any duplicate solutions."
>
>      http://www.mercury.csse.unimelb.edu.au/information/doc-release/mercury_ref/Determinism-checking-and-inference.html
>
> If we apply this rule to the disjunction as a whole we notice that because all
> the variables are bound before entering the disjunction (the disjunction has no
> outputs).  Then we know that the extra solutions are pure and the goal produces
> between 0 and 1 solutions (inclusive).
>
> Therefore the disjunction is semidet; and the procedure (the name for a
> predicate in a given mode) is also semidet.
>
> As Peter pointed out, the same determinism rule is also true for the call to
> member in this mode.
>
> Hint: If anyone starts a wiki, this is a pretty nice example for something that
> may not be intuitive.
>

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------