The configuration graph of a log-space machine is polynomially sized

⚠️ Unreviewed by Bolton

A machine using O(log n) space has only polynomially many configurations: each of the 4 ^ O(log n) tape contents is n ^ O(1), and the head positions contribute a further polynomial factor. This is what turns the graph reachability of Complexitylib.Classes.Containments.Internal.ConfigGraph into a polynomial-time search.

Main results

• exists_log_bound — an O(log n) bound holds everywhere after adding a constant
• four_pow_log_le — 4 ^ (C · log₂ n + D) is polynomially bounded
• exists_config_bound — the configuration count is A · (n + 1) ^ B

theorem Complexity.exists_log_bound {f : ℕ → ℕ} (hf : BigO f fun (n : ℕ) => Nat.log 2 n) : ∃ (C : ℕ) (D : ℕ), ∀ (n : ℕ), f n ≤ C * Nat.log 2 n + D

An asymptotic logarithmic bound becomes an everywhere bound after adding a constant: the finitely many exceptional inputs are absorbed into it.

theorem Complexity.four_pow_log_le (C D n : ℕ) : 4 ^ (C * Nat.log 2 n + D) ≤ 4 ^ D * (n + 1) ^ (2 * C)

Four to a logarithmic power is polynomial.

def Complexity.PolyBounded (g : ℕ → ℕ) : Prop

Bounded by a constant times a power of n + 1.

Equations

• Complexity.PolyBounded g = ∃ (A : ℕ) (B : ℕ), ∀ (n : ℕ), g n ≤ A * (n + 1) ^ B

theorem Complexity.PolyBounded.const (c : ℕ) : PolyBounded fun (x : ℕ) => c

theorem Complexity.PolyBounded.mono {g h : ℕ → ℕ} (hg : PolyBounded g) (hle : ∀ (n : ℕ), h n ≤ g n) : PolyBounded h

Transfer along a pointwise bound.

theorem Complexity.PolyBounded.mul {g h : ℕ → ℕ} (hg : PolyBounded g) (hh : PolyBounded h) : PolyBounded fun (n : ℕ) => g n * h n

theorem Complexity.PolyBounded.add {g h : ℕ → ℕ} (hg : PolyBounded g) (hh : PolyBounded h) : PolyBounded fun (n : ℕ) => g n + h n

theorem Complexity.PolyBounded.pow {g : ℕ → ℕ} (hg : PolyBounded g) (m : ℕ) : PolyBounded fun (n : ℕ) => g n ^ m

theorem Complexity.PolyBounded.id : PolyBounded fun (n : ℕ) => n

theorem Complexity.PolyBounded.of_log {f : ℕ → ℕ} (hf : BigO f fun (n : ℕ) => Nat.log 2 n) : PolyBounded f

A log-space bound is polynomially bounded, as is four to its power.

theorem Complexity.PolyBounded.four_pow {f : ℕ → ℕ} (hf : BigO f fun (n : ℕ) => Nat.log 2 n) (m : ℕ) : PolyBounded fun (n : ℕ) => 4 ^ (f n + m)

theorem Complexity.exists_config_bound {k : ℕ} (Q : Type) [Fintype Q] {f : ℕ → ℕ} (hf : BigO f fun (n : ℕ) => Nat.log 2 n) : PolyBounded fun (n : ℕ) => Fintype.card (Code Q k n (f n))

The configuration count of a log-space machine is polynomial.