Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why does the AVL tree in Map of OCaml use balance factor (height diff) 2 instead of 1?

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?

like image 938
Jackson Tale Avatar asked Aug 10 '13 14:08

Jackson Tale


1 Answers

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.

like image 124
Daniel Bünzli Avatar answered Oct 21 '22 09:10

Daniel Bünzli