[mercury-users] New to mercury: structure reuse and efficiency

[Ralph Becket]

Gregory D. Weber, Thursday, 29 July 2004:
> There are a few of points here that I don't understand.
> 
> Peter Schachte writes:
>  > Gregory D. Weber wrote:
>  > 
>  > >There's an implied question here which I don't think has been answered:
>  > >how _does_ he do what he wants to do here, which, I believe, is to
>  > >make sure that H does not equal T before making the recursive call?
>  > >
>  > > > member([H|T], H).
>  > > > 
>  > > > member([H|T], X) :- not(X=H), member(T, X).
>  > >  
>  > >
>  > I think the best answer to your question is:  you don't, the compiler 
>  > does it for you.  This definition does what he wants:
>  > 
>  > member([H|T], H).
>  Let's call this rule 1 ...
> 
>  > 
>  > member([_|T], X) :- member(T, X).
> ... and this rule 2.

[By the way, you have the arguments the wrong way round here.
list__member takes a T as its first parameter and a list(T) as its
second parameter.  In my explanation below I use this correct argument
order.]

>  > 
>  > 
>  > In fact, it's better than what he's asking for, because the compiler 
>  > does it in a more flexible way than you could do it yourself.  The 
>  > compiler is smart enough to notice a call member(L, X) where L and  X 
>  > are both sure to be ground, and it forces the call to be deterministic 
> 
> [Ralph: s/deterministic/semi-deterministic/]
> 
>  > for you, 
> 
> Am I correct in thinking that you are assuming certain mode declarations,
> such as
> 
>      :- mode list__member(in, in) is semidet.
>      :- mode list__member(out, in) is nondet.

Yes, if you supply only the second mode, but call list__member with
(in, in) arguments, then it will infer the first mode for you.  The rule
is this: a non-deterministic goal that produces no outputs is
semi-deterministic.

Here's how it works.  Say you write

	list__member(X, Ys)

the compiler will turn this into the quantified goal

	some [V1, V2] (
		list__member(V1, V2),
		V1 = X,
		V2 = Ys
	)

(where V1 and V2 are fresh variables) and then reorder the goals as
necessary to ensure that variable bindings are established before the
point they are needed.  So if both X and Ys are ground, but we have only
declared the mode

:- mode list__member(out, in) is nondet.

then the compiler will turn the quantified goal into

	some [V1, V2] (
		V2 = Ys,		% Assignment to V2 (*)
		list__member(V1, V2),	% mode (out, in) is nondet
		V1 = X			% Equality test (*)
	)

since X and Ys are ground at the start of this goal and V1 and V2 are
local variables, this goal as a whole has no outputs.  So even though it
looks non-deterministic because of the call to list__member, the
compiler is smart enough to work out that it can treat this goal as
semi-deterministic.

That might look a little involved, but in practice programmers very,
very rarely need to understand details at this level.  Usually your
intuition will be correct.

[(*) Mercury separates unifications X = Y into four categories:
assignment, where X is free and Y is bound; construction where X is free
and Y is a data constructor term whose arguments are all bound
variables; deconstruction where X is bound and Y is a data constructor
term whose arguments are all free variables; and equality tests.]

> > so you don't try to see if the element is in the tail of the 
>  > list when you've already seen that it matches the head.  
> 
> Why would I (= the member process?) already have seen that it matches
> the head?

No.  Does my explanation above clear this up for you?

> In an earlier message, Ralph said the compiler would freely
> rearrange code, but "already" implies that it orders rule 1 before
> rule 2.

No, it doesn't.  You can't rely upon disjunctions being evaluated in any
particular order.  If this is *necessary*, use an if-then-else.
Otherwise write code where the "ordering" of disjuncts is irrelevant.

> Do we really know this?  If we do, is it because, as a
> general principle, the compiler will always arrange to try a base case
> rule before a recursive step rule?

No, you're thinking the "clever" part happens inside list__member.  It
doesn't: the "clever" part happens because of the code transformation I
illustrated above.

> > However, when X 
>  > is unbound, then it will match every element of the list, so you don't 
>  > want to commit yourself to the first match.  Consider this predicate to 
>  > determine whether two lists have any elements in common:
>  > 
>  >     overlap(L1, L2) :- member(L1, X), member(L2, X).
>  > 
>  > Here the first call to member will have X unbound and the second will 
>  > have it bound, so the first must not commit to the first match (because 
>  > it may not be the first elment of L1 that appears on L2), but the second 
>  > one can (because we don't care how many times an element of L1 appears 
>  > on L2).  
> 
> Again, if the compiler is free to rearrange code, isn't it possible
> it tries member(L2, X) first?

Absolutely, but it doesn't matter which way the compiler chooses.
Either the compiler generates

:- mode overlap(in, in) is semidet.

overlap(L1, L2) :-
	some [X] (
		some [V1, V2] (
			V2 = L1,	% Assignment to V2
			member(V1, V2),	% mode(out, in) is nondet
			V1 = X		% Assignment to X
		),  % This whole subgoal is nondet (it has an output, X)
		some [V3, V4] (
			V4 = L2,	% Assignment to V4,
			member(V3, V4),	% mode(out, in) is nondet
			V3 = X		% Equality test
		)   % This whole subgoal is semidet (it has no outputs)
	).  % This whole subgoal is semidet (it has no outputs)

or...

:- mode overlap(in, in) is semidet.

overlap(L1, L2) :-
	some [X] (
		some [V1, V2] (
			V2 = L2,	% Assignment to V2
			member(V1, V2),	% mode(out, in) is nondet
			V1 = X		% Assignment to X
		),  % This whole subgoal is nondet (it has an output, X)
		some [V3, V4] (
			V4 = L1,	% Assignment to V4,
			member(V3, V4),	% mode(out, in) is nondet
			V3 = X		% Equality test
		)   % This whole subgoal is semidet (it has no outputs)
	).  % This whole subgoal is semidet (it has no outputs)

Lo, we get the same result.

> > But further, once we find an element in common, we can commit 
>  > to that, because we don't care which elements are in common, just that 
>  > at least one is.  The Mercury compiler will do all that for you without 
>  > you having to say anything.
> 
> Except for the mode declarations?  :-)

You could ask the compiler to infer modes for you, but then it would
construct a separate mode for each different way that member is called.
And the error messages the compiler might generate would be much less
helpful.

Trust us: type and mode declarations are your friends!

-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------