[mercury-users] Why is
pbone at csse.unimelb.edu.au
Mon Mar 5 09:07:28 AEDT 2012
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?
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
member(Y, [X | Xs]) :-
Y :: in, % Not actually mercury syntax.
X :: in,
Xs :: in,
Y = X
Normal determinism checking (such as you suggest) would say that the
disjunction has between 0 and unbounded solutions. However, the reference
"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."
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 490 bytes
Desc: Digital signature
More information about the users