Time bounds from deterministic transducer space bounds

A one-way-output deterministic transducer has only finitely many execution- relevant configurations once its input length and auxiliary-space budget are fixed. A halting run cannot repeat one of these reduced snapshots, yielding an explicit time bound.

Main results

• TM.IsTransducer.reachesIn_succ_le_transducerConfigBound — exact halted-run bound
• TM.IsTransducer.reachesIn_le_transducerConfigBound — convenient weak bound
• TM.ComputesInSpace.computesInTime_configBound — space computation gives time
• TM.DecidesInSpace.decidesInTime_configBound — decision-space bound gives time

theorem Complexity.TM.IsTransducer.reachesIn_succ_le_transducerConfigBound {k : ℕ} {tm : TM k} (htrans : tm.IsTransducer) {x : List Bool} {space t : ℕ} {c : Cfg k tm.Q} (hreach : tm.reachesIn t (tm.initCfg x) c) (hhalt : tm.halted c) (hspace : ∀ (d : Cfg k tm.Q), tm.reaches (tm.initCfg x) d → d.WithinAuxSpace x.length space) : t + 1 ≤ tm.transducerConfigBound x.length space

A halting transducer run staying within auxiliary space space has one more time index than steps, and all those indices inject into the explicit type of reduced transducer snapshots.

theorem Complexity.TM.IsTransducer.reachesIn_le_transducerConfigBound {k : ℕ} {tm : TM k} (htrans : tm.IsTransducer) {x : List Bool} {space t : ℕ} {c : Cfg k tm.Q} (hreach : tm.reachesIn t (tm.initCfg x) c) (hhalt : tm.halted c) (hspace : ∀ (d : Cfg k tm.Q), tm.reaches (tm.initCfg x) d → d.WithinAuxSpace x.length space) : t ≤ tm.transducerConfigBound x.length space

A halting transducer run staying within auxiliary space space takes no more steps than the explicit number of reduced transducer snapshots.

theorem Complexity.TM.ComputesInSpace.computesInTime_configBound {k : ℕ} {tm : TM k} {f : List Bool → List Bool} {S : ℕ → ℕ} (hcomp : tm.ComputesInSpace f S) : tm.ComputesInTime f fun (n : ℕ) => tm.transducerConfigBound n (S n)

A total deterministic function transducer using space S computes within the corresponding finite reduced-configuration bound.

theorem Complexity.TM.DecidesInSpace.decidesInTime_configBound {k : ℕ} {tm : TM k} {L : Language} {S : ℕ → ℕ} (hdec : tm.DecidesInSpace L S) (htrans : tm.IsTransducer) : tm.DecidesInTime L fun (n : ℕ) => tm.transducerConfigBound n (S n)

A deterministic language decider with one-way output and auxiliary-space bound S decides within the corresponding finite reduced-configuration bound.