Finite-configuration run bounds — proof internals #
A halting deterministic transducer run cannot repeat a reduced snapshot. If it did, finite snapshot determinism would reproduce the final halt state at an earlier time. The run's time indices therefore inject into the finite snapshot type.
theorem
Complexity.TM.IsTransducer.reachesIn_succ_le_transducerConfigBound_internal
{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)
:
The time indices of a halting transducer run staying within auxiliary
space space inject into the reduced transducer snapshots.
theorem
Complexity.TM.ComputesInSpace.computesInTime_configBound_internal
{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 space-bounded transducer computes within its finite reduced- configuration bound.
theorem
Complexity.TM.DecidesInSpace.decidesInTime_configBound_internal
{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 total space-bounded language decider that also has one-way output decides within its finite reduced-configuration bound.