Counting the nodes of a recursion tree

A recursion whose calls at depth d have at most b d children, with at most k levels below depth d, has at most Nat.recursionBound b k d nodes below and including a call at depth d: one for the call, plus b d subtrees of one level less (Nat.recursionBound_succ). This is at most k + 1 times the product of the branching factors (Nat.recursionBound_le).

Recursion trees of size 2 ^ O(n / √(log n)). If a call at depth j has at most 2 ^ (c ⌊log₂ n⌋ + e j) children, there are at most ⌊log₂ n⌋ levels, and the excess exponents sum to O(n / √⌊log₂ n⌋), then the tree has 2 ^ O(n / √⌊log₂ n⌋) nodes (Nat.mul_prod_le_two_pow_div_sqrt_log_two, with the explicit constant 1 + 16 c + E), in the natural-number scale of Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two. The polynomial factors 2 ^ (c ⌊log₂ n⌋) contribute 2 ^ O(log² n), which the scale absorbs. Excess exponents halving with the depth sum to at most twice the first one (Nat.sum_div_two_pow_le).

This is the call count in the proof of Theorem D.1 of [OAI26f] (Appendix D.4.7, p. 64): a call at depth d has s ^ O(1) exp(O(s / √λ · (√2 / 8) ^ d)) children and there are O(log λ) levels.

Main definitions

• Nat.recursionBound: the node bound of a recursion tree with given branching factors.

Main results

• Nat.recursionBound_le: at most k + 1 times the product of the branching factors.
• Nat.sum_div_two_pow_le: ∑ j < D, x / 2 ^ j ≤ 2 x.
• Nat.mul_prod_le_two_pow_div_sqrt_log_two: recursion trees of size 2 ^ O(n / √⌊log₂ n⌋), with an explicit constant.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix D.4.7 (p. 64).

def Nat.recursionBound (b : ℕ → ℕ) : ℕ → ℕ → ℕ

The node bound of a recursion tree whose calls at depth d have at most b d children, for a call at depth d with at most k levels below it.

@[simp]

theorem Nat.recursionBound_zero (b : ℕ → ℕ) (d : ℕ) : recursionBound b 0 d = 1

theorem Nat.recursionBound_succ (b : ℕ → ℕ) (k d : ℕ) : recursionBound b (k + 1) d = 1 + b d * recursionBound b k (d + 1)

A call is one node above its children's subtrees.

theorem Nat.recursionBound_le (b : ℕ → ℕ) (k d : ℕ) : recursionBound b k d ≤ (k + 1) * ∏ j ∈ Finset.range k, max 1 (b (d + j))

The node bound is at most k + 1 times the product of the branching factors.

theorem Nat.sum_div_two_pow_le (x D : ℕ) : ∑ j ∈ Finset.range D, x / 2 ^ j ≤ 2 * x

Halving excess exponents: ∑ j < D, x / 2 ^ j ≤ 2 x.

theorem Nat.log_two_sq_le_div_sqrt_log_two {n : ℕ} (hn : 2 ≤ n) : log 2 n ^ 2 ≤ 16 * (n / (log 2 n).sqrt)

The square of the logarithm is O(n / √⌊log₂ n⌋): ⌊log₂ n⌋ ^ 2 ≤ 16 (n / √⌊log₂ n⌋) from n = 2 on, since ⌊log₂ n⌋ ^ 2 √⌊log₂ n⌋ ≤ ⌊log₂ n⌋ ^ 3 ≤ 8 n.

theorem Nat.mul_prod_le_two_pow_div_sqrt_log_two (c E : ℕ) {n D : ℕ} {b e : ℕ → ℕ} (hn : 2 ≤ n) (hD : D ≤ log 2 n) (hb : ∀ j < D, b j ≤ 2 ^ (c * log 2 n + e j)) (he : ∑ j ∈ Finset.range D, e j ≤ E * (n / (log 2 n).sqrt)) : (D + 1) * ∏ j ∈ Finset.range D, max 1 (b j) ≤ 2 ^ ((1 + 16 * c + E) * n / (log 2 n).sqrt)

Recursion trees of size 2 ^ O(n / √⌊log₂ n⌋), with the constant 1 + 16 c + E. From n = 2 on: if a call at depth j < D has at most 2 ^ (c ⌊log₂ n⌋ + e j) children, D ≤ ⌊log₂ n⌋, and ∑ j < D, e j ≤ E (n / √⌊log₂ n⌋), then (D + 1) ∏ j < D, max 1 (b j) ≤ 2 ^ ((1 + 16 c + E) n / √⌊log₂ n⌋), which bounds the nodes of the recursion tree by recursionBound_le. The constant is linear in E, so a single clock serves a family of excess budgets growing linearly in a parameter.