Data Structures & AlgorithmsHeight-Balanced Trees — Concept & Invariants

Height-Balanced Trees — Concept & Invariants

LevelIntermediate

Duration75 mins

TopicHeight-Balanced Trees — Concept & Invariants

3 / 4

What Invariants Balanced Trees Maintain

The Contracts That Hold Everything Together

Every robust data structure rests on a foundation of invariants—properties that are always true, no matter what operations have been performed. Invariants are the contracts that the data structure maintains with itself: "I promise that X is always true, and every operation I support will preserve X."

For balanced binary search trees, invariants are particularly important because they bridge two concerns:

Correctness: The tree must remain a valid BST (elements correctly ordered)
Efficiency: The tree must remain balanced (height bounded by log n)

Understanding invariants isn't just academic—it's the key to reasoning about data structure behavior, debugging implementations, and extending structures with new capabilities.

What You Will Learn

By the end of this page, you will understand what invariants are and why they matter, the specific invariants maintained by balanced BSTs, how invariants compose to provide guarantees, how operations must preserve invariants, and how to use invariant thinking for debugging and verification.

What Is an Invariant?

An invariant is a property that remains true throughout the lifetime of a data structure, preserved by every operation that modifies the structure.

Formal definition:

An invariant I is a predicate such that:

I is true after the data structure is initialized (establishment)

If I is true before any operation, I remains true after the operation (preservation)

The power of invariants comes from this preservation property: if we can prove that an invariant holds initially and that every operation preserves it, we know the invariant holds at all times without having to check it after every operation.

Analogy: The Bank Account Invariant

Consider a bank account with the invariant "balance ≥ 0" (no negative balances allowed). Every operation—deposit, withdrawal, transfer—must preserve this invariant:

Deposit: Adds positive amount → invariant preserved
Withdrawal: Checks balance first, rejects if insufficient → invariant preserved
Transfer: Combination of withdrawal and deposit, both preserve invariant → invariant preserved

No matter how many operations you perform, you can trust that the balance is never negative.

Invariants as Mental Shortcuts

Invariants free you from having to trace through every possible operation sequence. Instead of asking 'is the tree balanced after this sequence of 1000 insertions?', you ask 'does each individual operation preserve balance?' If yes, then balance holds after any sequence.

The BST Ordering Invariant

The most fundamental invariant of any binary search tree is the ordering property. This invariant is what makes a BST a BST:

The BST Ordering Invariant:

For every node X in the tree:

All values in X's left subtree are less than X's value

All values in X's right subtree are greater than X's value

Note the precision here: it's not just "left child < node < right child"—it's all nodes in the entire left subtree and all nodes in the entire right subtree. This is a much stronger statement.

bst-invariant-check.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
// The BST invariant must hold for all nodes, not just immediate children
 
// CORRECT BST - invariant satisfied
//        10
//       /  \
//      5    15
//     / \   / \
//    3   7 12  20
//
// At node 10: All left subtree values {3, 5, 7} < 10 ✓
//             All right subtree values {12, 15, 20} > 10 ✓
// At node 5:  All left subtree values {3} < 5 ✓
//             All right subtree values {7} > 5 ✓
// ... and so on for every node
 
 
// INCORRECT - looks like BST but violates invariant
//        10
//       /  \
//      5    15
//     / \
//    3   12  <-- 12 is in left subtree of 10 but 12 > 10!
//
// The immediate parent-child relationships look fine:
// 3 < 5, 12 > 5, 5 < 10, 15 > 10
// But 12 is in the LEFT subtree of 10, yet 12 > 10. VIOLATION!
 
 
// Verification function checks entire subtree ranges
function isBST<T>(
    node: BSTNode<T> | null, 
    min: T | null = null, 
    max: T | null = null
): boolean {
    // Empty tree is valid BST
    if (node === null) return true;
    
    // Check current node against range constraints
    if (min !== null && node.value <= min) return false;  // violates min bound
    if (max !== null && node.value >= max) return false;  // violates max bound
    
    // Recursively check subtrees with tightened bounds
    // Left subtree: all values must be < current value
    // Right subtree: all values must be > current value
    return isBST(node.left, min, node.value) && 
           isBST(node.right, node.value, max);
}

What the ordering invariant provides:

Binary search capability — At each node, we can eliminate half the remaining candidates by comparing with the node's value
Inorder traversal produces sorted order — Left subtree (smaller) → node → right subtree (larger)
Predecessor/successor relationships — For any node, we can find the next smaller or larger element efficiently
Range queries — We can find all elements in a given range without visiting the entire tree

Operations must preserve this invariant:

Insert: New node goes in the correct position based on ordering
Delete: Node removal must not reorder remaining nodes
Rotations: The crucial constraint—rotations must preserve ordering!

Rotations Must Preserve BST Order

When we rebalance a tree using rotations, we're changing the structure but NOT the ordering. This is non-trivial! Rotations are carefully designed so that the BST property is maintained. We'll see this in detail when studying AVL rotations.

The Height Balance Invariant

The second critical invariant for balanced BSTs is the height balance property. We've already defined this mathematically; now let's frame it as an invariant:

The AVL Height Balance Invariant:

For every node X in the tree: |height(X.left) - height(X.right)| ≤ 1

Equivalently: balanceFactor(X) ∈ {-1, 0, +1}

This is a local invariant with global consequences. Each node only needs to check its immediate children's heights, but the cumulative effect constrains the entire tree's height to O(log n).

height-balance-check.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
// Checking the height balance invariant
 
function checkHeightBalanceInvariant<T>(node: AVLNode<T> | null): boolean {
    if (node === null) return true;
    
    const bf = getBalanceFactor(node);
    
    // Check local invariant at this node
    if (Math.abs(bf) > 1) {
        console.error(`Height balance violated at node ${node.value}: BF = ${bf}`);
        return false;
    }
    
    // Check invariant holds recursively in subtrees
    return checkHeightBalanceInvariant(node.left) && 
           checkHeightBalanceInvariant(node.right);
}
 
// More thorough check that also verifies height consistency
function verifyAVLTree<T>(node: AVLNode<T> | null): { valid: boolean; height: number } {
    if (node === null) {
        return { valid: true, height: -1 };
    }
    
    const leftResult = verifyAVLTree(node.left);
    const rightResult = verifyAVLTree(node.right);
    
    // Check for already-found violations
    if (!leftResult.valid || !rightResult.valid) {
        return { valid: false, height: -1 };
    }
    
    // Verify stored height matches computed height
    const computedHeight = 1 + Math.max(leftResult.height, rightResult.height);
    if (node.height !== computedHeight) {
        console.error(`Height mismatch at ${node.value}: stored=${node.height}, computed=${computedHeight}`);
        return { valid: false, height: -1 };
    }
    
    // Check balance factor
    const bf = leftResult.height - rightResult.height;
    if (Math.abs(bf) > 1) {
        console.error(`Balance violation at ${node.value}: BF = ${bf}`);
        return { valid: false, height: -1 };
    }
    
    return { valid: true, height: computedHeight };
}

How operations preserve the height balance invariant:

Insertion:

Perform standard BST insertion (preserves ordering invariant)
Walk back up toward the root, updating heights
At each node, check if balance factor has become ±2
If violation found, perform appropriate rotation(s) to restore balance
After rotation, subtree height returns to pre-insertion value (for AVL trees), so no further violations possible above

Deletion:

Perform standard BST deletion (preserves ordering invariant)
Walk back up toward the root, updating heights
At each node, check for balance violations
Unlike insertion, deletion may require multiple rotations up the tree, because fixing one violation might decrease the subtree's height, creating a new violation higher up

The key insight is that rotations are the mechanism for restoring the height balance invariant when it's violated. Rotations are specifically designed to:

Reduce the height difference at the violating node
Preserve the BST ordering invariant
Complete in O(1) time

Invariant Composition: Two Invariants Working Together

AVL trees maintain two invariants simultaneously:

BST Ordering Invariant → Enables efficient search (binary search logic)
Height Balance Invariant → Guarantees O(log n) height

These invariants are orthogonal but interacting:

Orthogonal: Ordering says nothing about heights; balance says nothing about ordering
Interacting: Operations on the tree must preserve BOTH invariants simultaneously

The composition challenge:

When we insert or delete, we potentially violate the balance invariant. To fix it, we perform rotations. But rotations change the tree's structure—they could potentially violate the ordering invariant!

The brilliance of tree rotations is that they're carefully designed to:

Change the tree's vertical structure (heights and balance factors)
Preserve the tree's horizontal structure (ordering relationships)

rotation-preserves-order.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
RIGHT ROTATION at node Y - Does it preserve BST ordering?
 
BEFORE:                          AFTER:
       Y                              X
      / \                            / \
     X   T3          →              T1  Y
    / \                                / \
   T1  T2                             T2  T3
 
Ordering constraints BEFORE:
- All values in T1 < X
- All values in T2 > X and < Y (T2 is right of X, left of Y)
- All values in T3 > Y
- X < Y
 
Ordering constraints AFTER:
- All values in T1 < X ← unchanged, T1 still left of X
- All values in T2 > X ← unchanged, but now T2 is left of Y
- All values in T2 < Y ← true! T2 was between X and Y before
- All values in T3 > Y ← unchanged, T3 still right of Y
- X < Y ← still true, now X is parent
 
Every ordering relationship from BEFORE is preserved in AFTER!
The rotation only changed who is parent/child, not the left-to-right order.
 
INORDER TRAVERSAL:
Before: T1 → X → T2 → Y → T3
After:  T1 → X → T2 → Y → T3
 
SAME! The inorder sequence is identical before and after rotation.

The invariant composition theorem (informal):

If the BST ordering invariant and AVL balance invariant both hold before an insert/delete operation, and the operation follows the AVL algorithm correctly, then both invariants hold after the operation completes.

This is actually provable formally, but the key intuition is:

Standard BST insert/delete preserves ordering
Rotations preserve ordering (as shown above)
Rotations restore balance
Therefore: the complete operation preserves ordering AND restores balance

Multiple Invariants Are Common

Many data structures maintain multiple invariants. Red-black trees maintain BST ordering, color (red/black) constraints, and black-height balance. Heaps maintain the complete tree shape and heap ordering. Understanding invariant composition is essential for reasoning about complex structures.

Invariants in Other Balanced Trees

Different balanced tree variants maintain different invariants to achieve balance. Understanding these alternatives deepens our appreciation for the design space:

Red-Black Tree Invariants:

Red-black trees use a more relaxed balance condition enforced through color properties:

Red-Black Tree Properties (Invariants)

•Every node is colored red or black — A binary attribute attached to each node
•The root is black — Entry point convention
•Every null leaf is considered black — Simplifies reasoning about paths
•Red nodes cannot have red children — No two reds in a row on any path
•All paths from root to null leaves have the same black depth — The key balance constraint

These five properties together guarantee that the longest path is at most twice the shortest path, ensuring O(log n) height.

2-3 Tree Invariants:

2-3 trees are multi-way search trees with their own invariant structure:

2-3 Tree Properties (Invariants)

•Every internal node has 2 or 3 children — Hence the name
•All leaves are at the same depth — Perfect balance by definition
•2-nodes contain one key, 3-nodes contain two keys — Multi-key nodes
•Keys within a node are ordered — Enables search within nodes
•Subtrees between keys contain values in the appropriate range — BST-like ordering generalized

Comparing Balance Invariants Across Tree Types
Tree Type	Balance Mechanism	Height Bound	Rebalancing Complexity
AVL Tree	Height difference ≤ 1 at each node	h < 1.44 log₂(n)	Up to O(log n) rotations per delete
Red-Black Tree	Black-depth same on all paths + no red-red	h ≤ 2 log₂(n+1)	At most 2 rotations per insert, 3 per delete
2-3 Tree	All leaves at same depth	h = ⌊log₂(n)⌋ to ⌈log₃(n)⌉	Splits/merges propagate up
B-Tree	All leaves at same depth + node fill constraints	h = O(log_t(n))	Optimal for disk-based storage

The design trade-off:

Different invariants offer different trade-offs:

AVL trees have the strictest balance, giving shortest heights but requiring more rotations during updates
Red-black trees have looser balance, allowing taller trees but simpler, bounded rebalancing
2-3 and B-trees generalize to multi-way branching, which is ideal for disk I/O where reading a larger node is almost as fast as reading a smaller one

The invariant you choose depends on your access patterns and performance requirements.

Invariant Thinking for Debugging

One of the most practical applications of invariant understanding is debugging. When something goes wrong with a balanced tree implementation, invariants provide a systematic way to find the problem:

The debugging methodology:

Invariant-Based Debugging Steps

•Write verification functions for each invariant — These should independently check whether each invariant holds for the entire tree
•Run verification after every operation during testing — Expensive but catches violations immediately
•When a violation is detected, identify which invariant failed — This narrows down the bug type
•Check the operation that was just performed — The most recent operation likely caused the violation
•Trace through the operation with the failing input — Focus on the invariant-preservation logic

debug-avl-tree.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
// Comprehensive AVL tree verification for debugging
 
interface VerificationResult {
    valid: boolean;
    errors: string[];
}
 
function verifyAVLTreeComplete<T extends number>(
    root: AVLNode<T> | null
): VerificationResult {
    const errors: string[] = [];
    
    // Check 1: BST ordering invariant
    function checkBST(
        node: AVLNode<T> | null, 
        min: T | null, 
        max: T | null
    ): boolean {
        if (node === null) return true;
        
        if (min !== null && node.value <= min) {
            errors.push(`BST violation: ${node.value} ≤ min bound ${min}`);
            return false;
        }
        if (max !== null && node.value >= max) {
            errors.push(`BST violation: ${node.value} ≥ max bound ${max}`);
            return false;
        }
        
        return checkBST(node.left, min, node.value) && 
               checkBST(node.right, node.value, max);
    }
    
    // Check 2: Height consistency (stored heights match computed)
    function checkHeights(node: AVLNode<T> | null): number {
        if (node === null) return -1;
        
        const leftHeight = checkHeights(node.left);
        const rightHeight = checkHeights(node.right);
        const expectedHeight = 1 + Math.max(leftHeight, rightHeight);
        
        if (node.height !== expectedHeight) {
            errors.push(
                `Height mismatch at ${node.value}: stored=${node.height}, ` +
                                `expected=${expectedHeight}`
            );
        }
        
        return expectedHeight;
    }
    
    // Check 3: Balance factor invariant
    function checkBalance(node: AVLNode<T> | null): boolean {
        if (node === null) return true;
        
        const bf = getBalanceFactor(node);
        if (Math.abs(bf) > 1) {
            errors.push(`Balance violation at ${node.value}: BF = ${bf}`);
            return false;
        }
        
        return checkBalance(node.left) && checkBalance(node.right);
    }
    
    // Run all checks
    checkBST(root, null, null);
    checkHeights(root);
    checkBalance(root);
    
    return {
        valid: errors.length === 0,
        errors
    };
}
 
// Usage in testing
function testInsert() {
    const tree = new AVLTree<number>();
    const testValues = [10, 5, 15, 3, 7, 12, 20, 1, 4];
    
    for (const value of testValues) {
        tree.insert(value);
        const result = verifyAVLTreeComplete(tree.root);
        
        if (!result.valid) {
            console.error(`Invariant violation after inserting ${value}:`);
            result.errors.forEach(e => console.error(`  - ${e}`));
            throw new Error('AVL tree invariant violated');
        }
    }
    
    console.log('All insertions passed verification!');
}

Invariant Checks as Tests

In production code, you can optionally include invariant verification as an assertion that's enabled in debug builds but compiled out in release builds. This catches bugs during development without impacting production performance.

How Invariants Enable Reasoning About Complexity

Invariants aren't just for correctness—they're the foundation for analyzing time and space complexity. Here's how invariants enable complexity reasoning:

From invariant to complexity bound:

Invariants and Their Complexity Implications
Invariant	What It Implies	Complexity Consequence
\|BF\| ≤ 1 at every node	Height ≤ 1.44 log₂(n)	All path-following operations are O(log n)
BST ordering property	Binary search is valid	Each comparison eliminates half the candidates
Stored heights are accurate	BF can be computed in O(1)	Violation detection is constant time
Rotations preserve ordering	No need to re-sort after rebalancing	Rotations are O(1) operations

The reasoning chain for AVL operations:

Invariant: |BF| ≤ 1 everywhere
Theorem: This implies height ≤ 1.44 log₂(n)
Observation: Insert/search/delete all follow a path of length ≤ height
Conclusion: All these operations are O(log n)

For rebalancing:

Invariant: Heights are stored and kept accurate
Observation: We can compute BF in O(1) at any node
Observation: Rotations are O(1) operations
For insertion: Path length is O(log n), at most one rotation point
Conclusion: Insert with rebalancing is O(log n)

The power of the approach:

Note that we didn't have to analyze hundreds of insertion sequences or prove complex recurrences. We established invariants, proved they imply height bounds, and derived complexity from the structure. This is why invariant thinking is so powerful—it abstracts away the details of specific operation sequences.

Invariant-Based Proofs

Formal verification of data structures typically works by proving invariant preservation. Tools like Dafny, Coq, and Isabelle can mechanically verify these proofs, providing mathematical certainty that the implementation is correct.

Summary: Invariants as the Foundation of Balanced Trees

Invariants are the contracts that make balanced trees work. Let's consolidate the key insights:

Key Takeaways

•An invariant is a always-true property — Established at initialization and preserved by every operation
•AVL trees maintain two invariants — BST ordering (for correctness) and height balance (for efficiency)
•Invariants compose — Multiple invariants can work together, each providing different guarantees
•Rotations are designed to preserve ordering while restoring balance — This is the key insight that makes rebalancing work
•Different balanced trees use different invariants — AVL uses height difference, red-black uses color properties, 2-3 trees use node structure
•Invariants enable debugging — When something breaks, check which invariant was violated
•Invariants enable complexity analysis — From invariants flow height bounds, from height bounds flow O(log n) guarantees

What's next:

Now that we understand the invariants that balanced trees maintain, we're ready for the final piece: how do invariants guarantee height bounds? The next page provides a rigorous analysis showing how the simple local constraint |BF| ≤ 1 at each node mathematically implies the global constraint that tree height is O(log n).

Page Complete

You now understand invariants—the unchanging properties that make balanced trees both correct and efficient. The BST ordering invariant enables search; the height balance invariant guarantees speed. Together, maintained by carefully-designed operations, they give us the powerful guarantees that make balanced BSTs indispensable in computing.

3 / 4

Loading learning content...

Data Structures & AlgorithmsHeight-Balanced Trees — Concept & Invariants

Height-Balanced Trees — Concept & Invariants

LevelIntermediate

Duration75 mins

TopicHeight-Balanced Trees — Concept & Invariants

3 / 4

What Invariants Balanced Trees Maintain

The Contracts That Hold Everything Together

For balanced binary search trees, invariants are particularly important because they bridge two concerns:

Correctness: The tree must remain a valid BST (elements correctly ordered)
Efficiency: The tree must remain balanced (height bounded by log n)

Understanding invariants isn't just academic—it's the key to reasoning about data structure behavior, debugging implementations, and extending structures with new capabilities.

What You Will Learn

What Is an Invariant?

An invariant is a property that remains true throughout the lifetime of a data structure, preserved by every operation that modifies the structure.

Formal definition:

An invariant I is a predicate such that:

I is true after the data structure is initialized (establishment)

If I is true before any operation, I remains true after the operation (preservation)

Analogy: The Bank Account Invariant

Consider a bank account with the invariant "balance ≥ 0" (no negative balances allowed). Every operation—deposit, withdrawal, transfer—must preserve this invariant:

Deposit: Adds positive amount → invariant preserved
Withdrawal: Checks balance first, rejects if insufficient → invariant preserved
Transfer: Combination of withdrawal and deposit, both preserve invariant → invariant preserved

No matter how many operations you perform, you can trust that the balance is never negative.

Invariants as Mental Shortcuts

The BST Ordering Invariant

The most fundamental invariant of any binary search tree is the ordering property. This invariant is what makes a BST a BST:

The BST Ordering Invariant:

For every node X in the tree:

All values in X's left subtree are less than X's value

All values in X's right subtree are greater than X's value

bst-invariant-check.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
// The BST invariant must hold for all nodes, not just immediate children
 
// CORRECT BST - invariant satisfied
//        10
//       /  \
//      5    15
//     / \   / \
//    3   7 12  20
//
// At node 10: All left subtree values {3, 5, 7} < 10 ✓
//             All right subtree values {12, 15, 20} > 10 ✓
// At node 5:  All left subtree values {3} < 5 ✓
//             All right subtree values {7} > 5 ✓
// ... and so on for every node
 
 
// INCORRECT - looks like BST but violates invariant
//        10
//       /  \
//      5    15
//     / \
//    3   12  <-- 12 is in left subtree of 10 but 12 > 10!
//
// The immediate parent-child relationships look fine:
// 3 < 5, 12 > 5, 5 < 10, 15 > 10
// But 12 is in the LEFT subtree of 10, yet 12 > 10. VIOLATION!
 
 
// Verification function checks entire subtree ranges
function isBST<T>(
    node: BSTNode<T> | null, 
    min: T | null = null, 
    max: T | null = null
): boolean {
    // Empty tree is valid BST
    if (node === null) return true;
    
    // Check current node against range constraints
    if (min !== null && node.value <= min) return false;  // violates min bound
    if (max !== null && node.value >= max) return false;  // violates max bound
    
    // Recursively check subtrees with tightened bounds
    // Left subtree: all values must be < current value
    // Right subtree: all values must be > current value
    return isBST(node.left, min, node.value) && 
           isBST(node.right, node.value, max);
}

What the ordering invariant provides:

Binary search capability — At each node, we can eliminate half the remaining candidates by comparing with the node's value
Inorder traversal produces sorted order — Left subtree (smaller) → node → right subtree (larger)
Predecessor/successor relationships — For any node, we can find the next smaller or larger element efficiently
Range queries — We can find all elements in a given range without visiting the entire tree

Operations must preserve this invariant:

Insert: New node goes in the correct position based on ordering
Delete: Node removal must not reorder remaining nodes
Rotations: The crucial constraint—rotations must preserve ordering!

Rotations Must Preserve BST Order

The Height Balance Invariant

The second critical invariant for balanced BSTs is the height balance property. We've already defined this mathematically; now let's frame it as an invariant:

The AVL Height Balance Invariant:

For every node X in the tree: |height(X.left) - height(X.right)| ≤ 1

Equivalently: balanceFactor(X) ∈ {-1, 0, +1}

This is a local invariant with global consequences. Each node only needs to check its immediate children's heights, but the cumulative effect constrains the entire tree's height to O(log n).

height-balance-check.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
// Checking the height balance invariant
 
function checkHeightBalanceInvariant<T>(node: AVLNode<T> | null): boolean {
    if (node === null) return true;
    
    const bf = getBalanceFactor(node);
    
    // Check local invariant at this node
    if (Math.abs(bf) > 1) {
        console.error(`Height balance violated at node ${node.value}: BF = ${bf}`);
        return false;
    }
    
    // Check invariant holds recursively in subtrees
    return checkHeightBalanceInvariant(node.left) && 
           checkHeightBalanceInvariant(node.right);
}
 
// More thorough check that also verifies height consistency
function verifyAVLTree<T>(node: AVLNode<T> | null): { valid: boolean; height: number } {
    if (node === null) {
        return { valid: true, height: -1 };
    }
    
    const leftResult = verifyAVLTree(node.left);
    const rightResult = verifyAVLTree(node.right);
    
    // Check for already-found violations
    if (!leftResult.valid || !rightResult.valid) {
        return { valid: false, height: -1 };
    }
    
    // Verify stored height matches computed height
    const computedHeight = 1 + Math.max(leftResult.height, rightResult.height);
    if (node.height !== computedHeight) {
        console.error(`Height mismatch at ${node.value}: stored=${node.height}, computed=${computedHeight}`);
        return { valid: false, height: -1 };
    }
    
    // Check balance factor
    const bf = leftResult.height - rightResult.height;
    if (Math.abs(bf) > 1) {
        console.error(`Balance violation at ${node.value}: BF = ${bf}`);
        return { valid: false, height: -1 };
    }
    
    return { valid: true, height: computedHeight };
}

How operations preserve the height balance invariant:

Insertion:

Perform standard BST insertion (preserves ordering invariant)
Walk back up toward the root, updating heights
At each node, check if balance factor has become ±2
If violation found, perform appropriate rotation(s) to restore balance
After rotation, subtree height returns to pre-insertion value (for AVL trees), so no further violations possible above

Deletion:

Perform standard BST deletion (preserves ordering invariant)
Walk back up toward the root, updating heights
At each node, check for balance violations
Unlike insertion, deletion may require multiple rotations up the tree, because fixing one violation might decrease the subtree's height, creating a new violation higher up

The key insight is that rotations are the mechanism for restoring the height balance invariant when it's violated. Rotations are specifically designed to:

Reduce the height difference at the violating node
Preserve the BST ordering invariant
Complete in O(1) time

Invariant Composition: Two Invariants Working Together

AVL trees maintain two invariants simultaneously:

BST Ordering Invariant → Enables efficient search (binary search logic)
Height Balance Invariant → Guarantees O(log n) height

These invariants are orthogonal but interacting:

Orthogonal: Ordering says nothing about heights; balance says nothing about ordering
Interacting: Operations on the tree must preserve BOTH invariants simultaneously

The composition challenge:

The brilliance of tree rotations is that they're carefully designed to:

Change the tree's vertical structure (heights and balance factors)
Preserve the tree's horizontal structure (ordering relationships)

rotation-preserves-order.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
RIGHT ROTATION at node Y - Does it preserve BST ordering?
 
BEFORE:                          AFTER:
       Y                              X
      / \                            / \
     X   T3          →              T1  Y
    / \                                / \
   T1  T2                             T2  T3
 
Ordering constraints BEFORE:
- All values in T1 < X
- All values in T2 > X and < Y (T2 is right of X, left of Y)
- All values in T3 > Y
- X < Y
 
Ordering constraints AFTER:
- All values in T1 < X ← unchanged, T1 still left of X
- All values in T2 > X ← unchanged, but now T2 is left of Y
- All values in T2 < Y ← true! T2 was between X and Y before
- All values in T3 > Y ← unchanged, T3 still right of Y
- X < Y ← still true, now X is parent
 
Every ordering relationship from BEFORE is preserved in AFTER!
The rotation only changed who is parent/child, not the left-to-right order.
 
INORDER TRAVERSAL:
Before: T1 → X → T2 → Y → T3
After:  T1 → X → T2 → Y → T3
 
SAME! The inorder sequence is identical before and after rotation.

The invariant composition theorem (informal):

If the BST ordering invariant and AVL balance invariant both hold before an insert/delete operation, and the operation follows the AVL algorithm correctly, then both invariants hold after the operation completes.

This is actually provable formally, but the key intuition is:

Standard BST insert/delete preserves ordering
Rotations preserve ordering (as shown above)
Rotations restore balance
Therefore: the complete operation preserves ordering AND restores balance

Multiple Invariants Are Common

Invariants in Other Balanced Trees

Different balanced tree variants maintain different invariants to achieve balance. Understanding these alternatives deepens our appreciation for the design space:

Red-Black Tree Invariants:

Red-black trees use a more relaxed balance condition enforced through color properties:

Red-Black Tree Properties (Invariants)

•Every node is colored red or black — A binary attribute attached to each node
•The root is black — Entry point convention
•Every null leaf is considered black — Simplifies reasoning about paths
•Red nodes cannot have red children — No two reds in a row on any path
•All paths from root to null leaves have the same black depth — The key balance constraint

These five properties together guarantee that the longest path is at most twice the shortest path, ensuring O(log n) height.

2-3 Tree Invariants:

2-3 trees are multi-way search trees with their own invariant structure:

2-3 Tree Properties (Invariants)

•Every internal node has 2 or 3 children — Hence the name
•All leaves are at the same depth — Perfect balance by definition
•2-nodes contain one key, 3-nodes contain two keys — Multi-key nodes
•Keys within a node are ordered — Enables search within nodes
•Subtrees between keys contain values in the appropriate range — BST-like ordering generalized

Comparing Balance Invariants Across Tree Types
Tree Type	Balance Mechanism	Height Bound	Rebalancing Complexity
AVL Tree	Height difference ≤ 1 at each node	h < 1.44 log₂(n)	Up to O(log n) rotations per delete
Red-Black Tree	Black-depth same on all paths + no red-red	h ≤ 2 log₂(n+1)	At most 2 rotations per insert, 3 per delete
2-3 Tree	All leaves at same depth	h = ⌊log₂(n)⌋ to ⌈log₃(n)⌉	Splits/merges propagate up
B-Tree	All leaves at same depth + node fill constraints	h = O(log_t(n))	Optimal for disk-based storage

The design trade-off:

Different invariants offer different trade-offs:

AVL trees have the strictest balance, giving shortest heights but requiring more rotations during updates
Red-black trees have looser balance, allowing taller trees but simpler, bounded rebalancing
2-3 and B-trees generalize to multi-way branching, which is ideal for disk I/O where reading a larger node is almost as fast as reading a smaller one

The invariant you choose depends on your access patterns and performance requirements.

Invariant Thinking for Debugging

One of the most practical applications of invariant understanding is debugging. When something goes wrong with a balanced tree implementation, invariants provide a systematic way to find the problem:

The debugging methodology:

Invariant-Based Debugging Steps

•Write verification functions for each invariant — These should independently check whether each invariant holds for the entire tree
•Run verification after every operation during testing — Expensive but catches violations immediately
•When a violation is detected, identify which invariant failed — This narrows down the bug type
•Check the operation that was just performed — The most recent operation likely caused the violation
•Trace through the operation with the failing input — Focus on the invariant-preservation logic

debug-avl-tree.ts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
// Comprehensive AVL tree verification for debugging
 
interface VerificationResult {
    valid: boolean;
    errors: string[];
}
 
function verifyAVLTreeComplete<T extends number>(
    root: AVLNode<T> | null
): VerificationResult {
    const errors: string[] = [];
    
    // Check 1: BST ordering invariant
    function checkBST(
        node: AVLNode<T> | null, 
        min: T | null, 
        max: T | null
    ): boolean {
        if (node === null) return true;
        
        if (min !== null && node.value <= min) {
            errors.push(`BST violation: ${node.value} ≤ min bound ${min}`);
            return false;
        }
        if (max !== null && node.value >= max) {
            errors.push(`BST violation: ${node.value} ≥ max bound ${max}`);
            return false;
        }
        
        return checkBST(node.left, min, node.value) && 
               checkBST(node.right, node.value, max);
    }
    
    // Check 2: Height consistency (stored heights match computed)
    function checkHeights(node: AVLNode<T> | null): number {
        if (node === null) return -1;
        
        const leftHeight = checkHeights(node.left);
        const rightHeight = checkHeights(node.right);
        const expectedHeight = 1 + Math.max(leftHeight, rightHeight);
        
        if (node.height !== expectedHeight) {
            errors.push(
                `Height mismatch at ${node.value}: stored=${node.height}, ` +
                                `expected=${expectedHeight}`
            );
        }
        
        return expectedHeight;
    }
    
    // Check 3: Balance factor invariant
    function checkBalance(node: AVLNode<T> | null): boolean {
        if (node === null) return true;
        
        const bf = getBalanceFactor(node);
        if (Math.abs(bf) > 1) {
            errors.push(`Balance violation at ${node.value}: BF = ${bf}`);
            return false;
        }
        
        return checkBalance(node.left) && checkBalance(node.right);
    }
    
    // Run all checks
    checkBST(root, null, null);
    checkHeights(root);
    checkBalance(root);
    
    return {
        valid: errors.length === 0,
        errors
    };
}
 
// Usage in testing
function testInsert() {
    const tree = new AVLTree<number>();
    const testValues = [10, 5, 15, 3, 7, 12, 20, 1, 4];
    
    for (const value of testValues) {
        tree.insert(value);
        const result = verifyAVLTreeComplete(tree.root);
        
        if (!result.valid) {
            console.error(`Invariant violation after inserting ${value}:`);
            result.errors.forEach(e => console.error(`  - ${e}`));
            throw new Error('AVL tree invariant violated');
        }
    }
    
    console.log('All insertions passed verification!');
}

Invariant Checks as Tests

How Invariants Enable Reasoning About Complexity

Invariants aren't just for correctness—they're the foundation for analyzing time and space complexity. Here's how invariants enable complexity reasoning:

From invariant to complexity bound:

Invariants and Their Complexity Implications
Invariant	What It Implies	Complexity Consequence
\|BF\| ≤ 1 at every node	Height ≤ 1.44 log₂(n)	All path-following operations are O(log n)
BST ordering property	Binary search is valid	Each comparison eliminates half the candidates
Stored heights are accurate	BF can be computed in O(1)	Violation detection is constant time
Rotations preserve ordering	No need to re-sort after rebalancing	Rotations are O(1) operations

The reasoning chain for AVL operations:

Invariant: |BF| ≤ 1 everywhere
Theorem: This implies height ≤ 1.44 log₂(n)
Observation: Insert/search/delete all follow a path of length ≤ height
Conclusion: All these operations are O(log n)

For rebalancing:

Invariant: Heights are stored and kept accurate
Observation: We can compute BF in O(1) at any node
Observation: Rotations are O(1) operations
For insertion: Path length is O(log n), at most one rotation point
Conclusion: Insert with rebalancing is O(log n)

The power of the approach:

Invariant-Based Proofs

Summary: Invariants as the Foundation of Balanced Trees

Invariants are the contracts that make balanced trees work. Let's consolidate the key insights:

Key Takeaways

•An invariant is a always-true property — Established at initialization and preserved by every operation
•AVL trees maintain two invariants — BST ordering (for correctness) and height balance (for efficiency)
•Invariants compose — Multiple invariants can work together, each providing different guarantees
•Rotations are designed to preserve ordering while restoring balance — This is the key insight that makes rebalancing work
•Different balanced trees use different invariants — AVL uses height difference, red-black uses color properties, 2-3 trees use node structure
•Invariants enable debugging — When something breaks, check which invariant was violated
•Invariants enable complexity analysis — From invariants flow height bounds, from height bounds flow O(log n) guarantees

What's next:

Page Complete

3 / 4