Why does the AVL tree in Map of OCaml use balance factor (height diff) 2 instead of 1?
avl-tree, binary-search-tree, ocaml
Solution
In AVL trees you can see the maximal height difference as a tweakable parameter. They must have chosen 2 to tradeoff between the rebalancing cost on insertion/removal and the lookup cost.
Since you seem to be interested in these things I suggest you have a look at this this paper that has formal proof of correctness of OCaml's Set's module which uses the same AVL tree, by doing do so they actually did find an error in the rebalancing scheme... Also while not strictly equivalent implementation wise, I learned quite a lot from this this paper.
Problem
According to AVL tree wiki The balance factor is calculated as follows: balanceFactor = height(left-subtree) - height(right-subtree). For each node checked, if the balance factor remains −1, 0, or +1 then no rotations are necessary. However, in OCaml, it seems it uses balance factor of 2 ``` let bal l x d r = let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in if hl > hr + 2 then begin match l with Empty -> invalid_arg "Map.bal" | Node(ll, lv, ld, lr, _) -> if height ll >= height lr then create ll lv ld (create lr x d r) else begin match lr with Empty -> invalid_arg "Map.bal" | Node(lrl, lrv, lrd, lrr, _)-> create (create ll lv ld lrl) lrv lrd (create lrr x d r) end end else if hr > hl + 2 then begin match r with Empty -> invalid_arg "Map.bal" | Node(rl, rv, rd, rr, _) -> if height rr >= height rl then create (create l x d rl) rv rd rr else begin match rl with Empty -> invalid_arg "Map.bal" | Node(rll, rlv, rld, rlr, _) -> create (create l x d rll) rlv rld (create rlr rv rd rr) end end else Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) ``` Why?