From the Cormen book I was studying the chapter focused on the red black tree. I was particularly interested in why the procedures for insert/delete fixup works (namely a formal proof).

I report both the algorithms, taken from the book:


enter image description here

The book gives a generic explanation of why they works, but doesn't give any formal proof. Could you suggest me how to prove the result, or could where I find the proof? For example if I focus on the insert, I would look at the node $z$ and I would assume by induction that one subtree has black height $h-1$ while the other has black height $h$, then I would show that after an iteration both subtree have black height $h$. I would try something similar for the delete procedure.

I'm not entirely sure that this is the best way to prove the correctness, and I can't actually find a formal proof of the result.

(The main reason is actually that every time I read the book and specifically such chapter I just try to memorize the procedures. Since this kind of tree implementation is quite common I think is time I understand why it works.

  • 2
    $\begingroup$ Understanding how red-black trees work is definitely not best approached looking at the code. Have a look at the pictures and diagrams in the book. They precisely show the heights of respective subtrees before and after rotation at a certain node. Insertion is probably not proved by induction, as there is just a precise node where the rotation occurs. $\endgroup$ – Hendrik Jan Apr 25 '16 at 9:08
  • $\begingroup$ I actually looked at the pictures, however shouldn't I use the pseudo-code to prove it? $\endgroup$ – user8469759 Apr 25 '16 at 9:10
  • $\begingroup$ From the code I do not see what is happening. From the pictures I can construct the code. $\endgroup$ – Hendrik Jan Apr 25 '16 at 12:32
  • $\begingroup$ So what approach do you suggest? I don't actually understand what are you trying to suggest. $\endgroup$ – user8469759 Apr 25 '16 at 13:16
  • $\begingroup$ So, any thoughts about my question? $\endgroup$ – user8469759 May 6 '16 at 8:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.