Read-only-input loop combinator #
TM.forInputTM body advances over a Boolean input symbol and invokes body
without copying the input into auxiliary space. For input-preserving bodies,
this iterates exactly once per original symbol. It is the input-fueled
counterpart of the unary-work-register loop TM.forRegTM.
Main results #
TM.IsTransducer.forInputTM— input-driven iteration preserves one-way output.TM.ForInputLoopSpec.reachesIn— exact indexed execution from a loop certificate.TM.ForInputLoopSpaceSpec.prefix_withinAuxSpace— every prefix of the exact loop run respects the certified auxiliary-space budget.
theorem
Complexity.TM.ForInputLoopSpec.reachesIn
{n : ℕ}
{body : TM n}
{bodyTime : ℕ → ℕ}
{total count value : ℕ}
(spec : body.ForInputLoopSpec bodyTime total)
(htotal : value + count = total)
:
body.forInputTM.reachesIn (forInputLoopTime bodyTime value count) (spec.scanCfg value) spec.doneCfg
Exact remaining execution of a certified input-driven loop.
theorem
Complexity.TM.ForInputLoopSpaceSpec.prefix_withinAuxSpace
{n : ℕ}
{body : TM n}
{bodyTime : ℕ → ℕ}
{total inputLength spaceBound count value t : ℕ}
{spec : body.ForInputLoopSpec bodyTime total}
(spaceSpec : ForInputLoopSpaceSpec spec inputLength spaceBound)
{c : Cfg n body.forInputTM.Q}
(htotal : value + count = total)
(hreach : body.forInputTM.reachesIn t (spec.scanCfg value) c)
(htime : t ≤ forInputLoopTime bodyTime value count)
:
c.WithinAuxSpace inputLength spaceBound
Every prefix up to the exact remaining runtime of a certified input-driven loop respects its all-reachable auxiliary-space budget.
theorem
Complexity.TM.IsTransducer.forInputTM
{n : ℕ}
{body : TM n}
(hbody : body.IsTransducer)
:
body.forInputTM.IsTransducer
Iterating a one-way-output body over the read-only input remains a one-way-output transducer.