How to fight semideterminism in Mercury?

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

  • Next message: Bart Demoen: "Re: How to fight semideterminism in Mercury?" 
    Date: 16 Oct 2004 16:28:18 -0700

    Hello,

    Please excuse my rather newbie question. I am in the process of
    getting acquainted with Mercury, and I have encountered one problem
    with determinism inference that I am not sure how to tackle best. I am
    writing a small logic programming textbook for students, and want to
    switch half of the examples to Mercury, so I decided to implement AVL
    search tree along the guidelines described in the Bratko's
    "Programming in Prolog for Artificial Intelligence".

    We need to keep the height of the tree at each point, so the type
    definition looks like:

    :- type tree(T) ---> nil; tree(T,avltree(T),avltree(T)).
    :- type avltree(T) ---> tree(T)/int.

    When we come to element addition predicate, it is defined as follows:

    :- func add(int,avltree(int)) = avltree(int).
    :- mode add(in,in) = out is semidet.
    add(X,nil/_) = tree(X,nil/0,nil/0)/1.
    add(X,tree(Y,L,R)/H) = Res :-
            X<Y ->
                    tree(Z,L1,R1)/_ = add(X,L),
                    Res = combine(L1,Z,R1,Y,R);
            X>Y ->
                    tree(Z,L1,R1)/_ = add(X,R),
                    Res = combine(L,Y,L1,Z,R1);
            Res = tree(X,L,R)/H.

    The problem is that the predicate should be deterministic, because
    there is always one way to add an element to the tree (unlike the
    Mercury library, I assume that if the element already exists, we just
    keep the tree unchanged). However, Mercury mode inference does not
    allow it to be deterministic, because at the point where we unify
    "tree(Z,L1,R1)/_ = add(X,L)" there could be other solution, "nil/0",
    returned by add, and this case is not considered in our definition.
    However, WE KNOW that add always returns non-empty tree, but the
    Mercury compiler naturally does not.

    My question is: how to avoid this problem and define the predicate to
    be deterministic? I see two possible directions:

    1. Consider the case when add returns empty subtree. This would allow
    for deterministic definition, but would be somewhat artificial - I
    would be writing a code that would never execute! I think this is not
    the right way to go for the modern programming language -- I believe
    the language should let me know when the dead code exists, and not the
    vice versa.

    2. Define some other type for non-empty AVL tree, and declare that add
    returns non-empty tree. However, at present I am not very sure how to
    define this in Mercury.

    I would be grateful for any possible help with solution of this
    problem.

    Thanks,

    Dmitri.

  • Next message: Bart Demoen: "Re: How to fight semideterminism in Mercury?"

    Relevant Pages

    • Re: Metainterpreter that prints call stack in case of failure.
      ... Mercury's notion of determinism puts bounds on the number of solutions ... determinism is a property not of a predicate, but of a *mode* of a predicate. ... every predicate is used in only one mode; in the Mercury programs I have ... Retrofitting a Mercury-style determinism system onto Prolog is not really ...
      (comp.lang.prolog)
    • Re: Determinism
      ... Doing so immeadately leads to the ... conclusion we are not some kind of "billiard balls" just blindly ... What has this to do with "determinism"? ... Once upon a time a young tree grew. ...
      (talk.origins)
    • Re: Determinism
      ... Doing so immeadately leads to the ... conclusion we are not some kind of "billiard balls" just blindly ... What has this to do with "determinism"? ... Once upon a time a young tree grew. ...
      (talk.origins)