Log-space transducers run in polynomial time

The finite reduced-configuration theorem for one-way-output deterministic transducers makes a logarithmic auxiliary-space bound into a polynomial time bound. Consequently L ⊆ P and FL ⊆ FP.

Main results

• TM.transducerConfigBound_bigO_polynomial — logarithmic space gives a polynomial reduced-configuration bound
• L_subset_P — deterministic log-space languages are polynomial-time
• FL_subset_FP — deterministic log-space functions are polynomial-time

theorem Complexity.TM.transducerConfigBound_bigO_polynomial {k : ℕ} (tm : TM k) {S : ℕ → ℕ} (hS : BigO S fun (n : ℕ) => Nat.log 2 n) : ∃ (c : ℕ), BigO (fun (n : ℕ) => tm.transducerConfigBound n (S n)) fun (x : ℕ) => x ^ (1 + (2 * c + 1) * k)

The reduced-configuration count of a deterministic transducer using O(log n) auxiliary space is polynomial in the input length.

theorem Complexity.L_subset_P : L ⊆ P

L ⊆ P: every language decided by a deterministic log-space transducer is decidable in polynomial time.

theorem Complexity.FL_subset_FP : FL ⊆ FP

FL ⊆ FP: every deterministic log-space transducer function is computable in polynomial time.