Binary work-tape loop combinator #
TM.forBinaryWorkTM driverIdx body invokes body once per Boolean cell on a
designated work tape and stops at the first blank. The body sees the current
bit; the loopback seam advances the driver. This supplies width-driven control
for bitwise algorithms without iterating over the represented numeric value.
Main results #
TM.ForBinaryWorkLoopSpec.reachesIncomposes an indexed exact-execution certificate for the complete loop.TM.ForBinaryWorkLoopSpaceSpec.prefix_withinAuxSpacebounds every prefix of the certified loop run.TM.IsTransducer.forBinaryWorkTMpreserves one-way output safety.
theorem
Complexity.TM.ForBinaryWorkLoopSpec.reachesIn
{n : ℕ}
{driverIdx : Fin n}
{body : TM n}
{bodyTime : ℕ → ℕ}
{total count value : ℕ}
(spec : ForBinaryWorkLoopSpec driverIdx body bodyTime total)
(htotal : value + count = total)
:
(forBinaryWorkTM driverIdx body).reachesIn (forBinaryWorkLoopTime bodyTime value count) (spec.scanCfg value)
spec.doneCfg
Exact remaining execution of a certified binary work-tape loop.
theorem
Complexity.TM.ForBinaryWorkLoopSpaceSpec.prefix_withinAuxSpace
{n : ℕ}
{driverIdx : Fin n}
{body : TM n}
{bodyTime : ℕ → ℕ}
{total inputLength spaceBound count value t : ℕ}
{spec : ForBinaryWorkLoopSpec driverIdx body bodyTime total}
(spaceSpec : ForBinaryWorkLoopSpaceSpec spec inputLength spaceBound)
{c : Cfg n (forBinaryWorkTM driverIdx body).Q}
(htotal : value + count = total)
(hreach : (forBinaryWorkTM driverIdx body).reachesIn t (spec.scanCfg value) c)
(htime : t ≤ forBinaryWorkLoopTime bodyTime value count)
:
c.WithinAuxSpace inputLength spaceBound
Every prefix up to the exact remaining runtime of a certified binary-work loop respects its all-reachable auxiliary-space budget.
theorem
Complexity.TM.IsTransducer.forBinaryWorkTM
{n : ℕ}
{driverIdx : Fin n}
{body : TM n}
(hbody : body.IsTransducer)
:
(TM.forBinaryWorkTM driverIdx body).IsTransducer
Iterating a one-way-output body over a binary work tape remains a transducer.