Re: How to fight semideterminism in Mercury?

From: Dmitri Soshnikov (dsoshnikov_at_gmail.com)
Date: 10/19/04 

Date: 18 Oct 2004 15:30:41 -0700

Ralph,

Thank you very much for your thorough reply, which was extremely
helpful in making my understanding of mode/inst system better.

> Just as a point of style, it's usually preferable to use the built-in
> ordering function and a switch rather than if-then-elses:

If I understood correctly, the ordering function allows to define the
generic behaviour on any type T that supports ordering. I wonder if
there is any way to ensure that T is such a type...

> SOLUTION 2
>
> However, a simpler solution is to simply specify that your original
> add function always returns a non-empty AVL-tree:
>
> :- inst non_empty_tree ---> tree(ground, ground, ground).
> :- inst non_empty_avltree ---> non_empty_tree / ground.
>
> :- func add(T, avltree(T)) = avltree(T).
> :- mode add(in, in) = out(non_empty_avltree) is det.
>
> ...original definition of add...

I believe this is the "true" way to go in Mercury, because it keeps
the same declaratively clear definition, and just refines the mode
definition to better reflect the true specification of a function.

However, in the combine predicate there is still one small problem.
The code looks like:

combine(T1/H1, A, T2/H2, C, T3/H3) = R :-
        (H2>H1, H2>H3) -> T2=tree(B,T21,T22), Ha=H1+1, Hc=H3+1, Hb=Ha+1,
R=tree(B,tree(A,T1/H1,T21)/Ha,tree(C,T22,T3/H3)/Hc)/Hb;
        (H1>=H2, H1>=H3) -> Hc=max(H2,H3)+1, Ha=max(H1,Hc)+1,
R=tree(A,T1/H1,tree(C,T2/H2,T3/H3)/Hc)/Ha;
                            Ha=max(H1,H2)+1, Hc=max(Ha,H3)+1,
R=tree(C,tree(A,T1/H1,T2/H2)/Ha,T3/H3)/Hc.

Here, the unification T2=tree(B,T21,T22) is semidet, because it does
not know that the tree is not empty. While we cannot guarantee that
the tree T2/H2 would be non-empty in the first place, in the first
clause this is actually guaranteed by H2>H1 and H2>H3 clauses. Of
course, Mercury does not know this semantics and thus inferes the
unification as semidet.

To overcome the problem I use the idea from the solution 3 below and
move the unification inside the if clause... However, as you
mentioned, this is probably a bit of a hack... Would any other
solution be preferable? I cannot think of any, because, when I come to
think of the original definition, even declaratively the unification
belongs to the "IF" part (because in Prolog, when the unification
fails, the inference moves to the alternative branches of the
definition).
 
> Hope this helps,
> -- Ralph

It surely did! This is actually a thank-you posting more than anything
else, so my thoughts expressed here do not necessarily need answering
(in other words - I am pretty happy with current state of the
solution)...

Thanks a lot,

Dmitri.