Red-black tree

A binary search tree whose nodes are red or black, where no red node has a red child and every path from the root to a leaf has the same number of black nodes. In a functional setting insertion needs one rebalancing function with four symmetric cases, all rewritten to the same shape.

If every path has $b$ black nodes, the longest path is at most $2 b$ long, since reds cannot be adjacent, and the tree has at least $2^{b} - 1$ nodes. So a tree of $n$ nodes and height $h$ satisfies

h \leq 2 lo g_{2} (n + 1)

A new key is inserted as a red leaf, which keeps the black counts and may put a red node under a red parent. The parent's parent is then black, and the red pair sits in one of four positions below it. Okasaki's observation is that all four rebuild into the same tree:^[2]

The four violations, and the tree each becomes. x < y < z; a, b, c, d are subtrees; y and one of x, z are red.

        z             z             x             x
       / \           / \           / \           / \
      y   d         x   d         a   z         a   y
     / \           / \               / \           / \
    x   c         a   y             y   d         b   z
   / \               / \           / \               / \
  a   b             b   c         b   c             c   d
 
                           all become
 
                               y  (red)
                             /   \
                    (black) x     z (black)
                           / \   / \
                          a   b c   d

Insertion. The four cases are one or-pattern.

type color = R | B
type 'a t = E | T of color * 'a t * 'a * 'a t
 
(* The four ways a red node can have a red child under a black grandparent,
   all rebuilt into the same shape: a red node with two black children. *)
let balance = function
  | B, T (R, T (R, a, x, b), y, c), z, d
  | B, T (R, a, x, T (R, b, y, c)), z, d
  | B, a, x, T (R, T (R, b, y, c), z, d)
  | B, a, x, T (R, b, y, T (R, c, z, d)) ->
      T (R, T (B, a, x, b), y, T (B, c, z, d))
  | color, l, v, r -> T (color, l, v, r)
 
let insert x s =
  let rec ins = function
    | E -> T (R, E, x, E)
    | T (color, l, y, r) as s ->
        if x < y then balance (color, ins l, y, r)
        else if x > y then balance (color, l, y, ins r)
        else s
  in
  match ins s with T (_, l, y, r) -> T (B, l, y, r) | E -> assert false

Inserting 0 to n-1 in ascending order, the worst case for an unbalanced tree, and checking both invariants on the result. The black height counts the empty leaves.

n =      10  (ascending)  height  5   bound 2 log2(n+1) =  6.9   black height 4
n =    1000  (ascending)  height 15   bound 2 log2(n+1) = 19.9   black height 10
n =  100000  (ascending)  height 22   bound 2 log2(n+1) = 33.2   black height 17
n = 1000000  (ascending)  height 26   bound 2 log2(n+1) = 39.9   black height 20

An unbalanced tree would have height $n$ for this input. The root is repainted black after every insertion, which is where the black height grows.

Deletion is harder: removing a black node leaves a path one black node short, and repairing that takes more cases than insertion. Kahrs gave a version with the invariants enforced by types, and Germane and Might one with a temporary double-black colour.^[4]^[3]