The RBT example in the tree is broken

[protz]

        let l, r =
          if x <= v
          then insert x l, r
          else l, insert x r in
        balance (mk (color t) l v r)

→ balance is called with its left child balanced, so

  let balance = function
    | Black ((Red (Red (a, x, b), y, c)
            | Red (a, x, Red (b, y, c))), z, d)

matching on a left child that is not balanced makes no sense.

(We'll talk about it on Monday and settle the thing about RBTs).

[protz]

Also, the final assertion fails, it's probably the same issue.

[gasche]

I had forgotten (in fact accidentally removed in my refactorization-frenziness) some part of the balancedness check on RBTs, which I just restored in master. With that additional check, you can verify that this part of the balance function is necessary: comment it out, and you'll find counter-examples against balancedness.

One issue with the current implementation is that while we can retrieve the counter-examples, we do not see how they were constructed. It's nice to get an unbalanced RBT as output (it tells us that we got something wrong), it would be even nicer to see that it is in fact insert 1 (insert 2 empty). We could implement that, but it is not immediate (currently function names are kept in the Elem constructor, but not accessible in (_, _) fn, which is the part where values are searched and generated).

You are right about the final assertion, I noticed it this morning, but it is a separate issue: to get something to fail when I added zipper, I added those read and write functions in the signature. But they are too powerful and can break the RBT invariants, as they allow you to replace any subtree with any other RBT (breaking the invariant that all paths from the node have the same number of blacks).

I think this assertion would not fail if I removed those two functions, but I've been working on something else in a branch I hope to push this afternoon. In the meantime, feel free to disable the test, remove those functions, or just ignore the failure.

[protz]

I'd rather put on hold the whole thing about RBTs until we can all chat about it in person tomorrow. I'm not sure the current version is crystal clear when it comes to the balancedness checks, but I'm unsure how we should do it.

~ jonathan

On Sun 09 Feb 2014 03:21:49 PM CET, gasche wrote:

I had forgotten (in fact accidentally removed in my refactorization-frenziness) some part of the balancedness check on RBTs, which I just restored in master. With that additional check, you can verify that this part of the balance function is necessary: comment it out, and you'll find counter-examples against balancedness.

One issue with the current implementation is that while we can retrieve the counter-examples, we do not see how they were constructed. It's nice to get an unbalanced RBT as output (it tells us that we got something wrong), it would be even nicer to see that it is in fact |insert 1 (insert 2 empty)|. We could implement that, but it is not immediate (currently function names are kept in the |Elem| constructor, but not accessible in |(, ) fn|, which is the part where values are searched and generated).

You are right about the final assertion, I noticed it this morning, but it is a separate issue: to get something to fail when I added zipper, I added those |read| and |write| functions in the signature. But they are too powerful and can break the RBT invariants, as they allow you to replace any subtree with any other RBT (breaking the invariant that all paths from the node have the same number of blacks).

I think this assertion would not fail if I removed those two functions, but I've been working on something else in a branch I hope to push this afternoon. In the meantime, feel free to disable the test, remove those functions, or just ignore the failure.

— Reply to this email directly or view it on GitHub https://github.com/braibant/articheck/issues/15#issuecomment-34575064.

[gasche]

I finally disabled read/write in master ( 03419e52ef5360 ). See copious commit message.

PS: yeah, let's discuss it tomorrow.

[braibant]

Hey, this is still broken: if we add an element that is already present, we add it in the left tree. I realized that when I debugged my graph-based branch, but I did not fix the existing implementation...