5 AVL tree

An AVL (Adelson-Velsky and Landis) tree is a self-balancing binary search tree. A binary search tree is represented by a tuple (N,P_L,P_R,v) (recall that v is a function mapping nodes to values). An AVL tree is represented by a tuple (N,P_L,P_R,v,b), where b represents a function mapping a node to its “balance factor”.

The balance factor of a node n is defined as follows: b(n) = max({|p(n,m)||m ∈ N ∧A(n,m)(∃(n,l) ∈ P_L : A(l,m)∨m = l)})−max({|p(n,m)||m ∈ N ∧(∃(n,r) ∈ P_R : A(r,m)∨m = r)}). This big mess is really just saying the b(n) is the height of the left subtree of n minus the height of the right subtree of n. If the subtree rooted at n is balanced, then b(n) = 0. If the subtree rooted at n is badly balanced then |b(n)| is a large number.