Read-only-input loop combinator — definitions

TM.forInputTM body scans the Boolean input from left to right and invokes body after each bit. When body preserves the input tape, this is exactly one invocation per original input bit. The input itself is the loop fuel, so the combinator does not materialize a linear-size unary counter on an auxiliary tape.

inductive Complexity.TM.ForInputPhase : Type

Driver states for the read-only-input loop.

• scan : ForInputPhase
• done : ForInputPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqForInputPhase : DecidableEq ForInputPhase

Equations

• Complexity.TM.instDecidableEqForInputPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeForInputPhase : Fintype ForInputPhase

ForInputPhase has exactly two states.

Equations

• Complexity.TM.instFintypeForInputPhase = { elems := {Complexity.TM.ForInputPhase.scan, Complexity.TM.ForInputPhase.done}, complete := ⋯ }

def Complexity.TM.forInputTM {n : ℕ} (body : TM n) : TM n

Advance over a Boolean input symbol and run body.

The driver skips an initial left-end marker, advances the read-only input by one cell before each body invocation, and halts whenever scanning encounters a blank. Work and output tapes take the structurally safe read-back/idle action in driver states. Nonhalting body transitions are embedded exactly, so the usual once-per-original-symbol behavior requires the body to preserve the input tape.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.forInputLoopTime (bodyTime : ℕ → ℕ) (value : ℕ) : ℕ → ℕ

Exact remaining time for an input-driven loop whose body takes bodyTime value steps on iteration value. The terminal input-blank exit takes one step. Each nonterminal iteration takes one scanner step, the body run, and one loopback step.

Equations

• Complexity.TM.forInputLoopTime bodyTime value 0 = 1
• Complexity.TM.forInputLoopTime bodyTime value count.succ = 1 + bodyTime value + 1 + Complexity.TM.forInputLoopTime bodyTime (value + 1) count

structure Complexity.TM.ForInputLoopSpec {n : ℕ} (body : TM n) (bodyTime : ℕ → ℕ) (total : ℕ) : Type

Wrapper-free certificate for the exact control flow of an input-driven loop. All configurations use the public state type of forInputTM body, so clients need not mention the internal body-state embedding.

total is the first scanner index whose input symbol is blank.

• scanCfg : ℕ → Cfg n body.forInputTM.Q

  Canonical scanner configuration at iteration value.

• bodyStartCfg : ℕ → Cfg n body.forInputTM.Q

  Canonical combined-machine configuration at the start of the body.

• bodyDoneCfg : ℕ → Cfg n body.forInputTM.Q

  Canonical combined-machine configuration after the exact body run.

• doneCfg : Cfg n body.forInputTM.Q

  Canonical final driver configuration.

• scanStep (value : ℕ) : value < total → body.forInputTM.step (self.scanCfg value) = some (self.bodyStartCfg value)

  A nonterminal scanner step enters the body.

• bodyRun (value : ℕ) : value < total → body.forInputTM.reachesIn (bodyTime value) (self.bodyStartCfg value) (self.bodyDoneCfg value)

  The body has the advertised exact runtime.

• loopbackStep (value : ℕ) : value < total → body.forInputTM.step (self.bodyDoneCfg value) = some (self.scanCfg (value + 1))

  The preserving seam step advances to the next scanner configuration.

• blankStep : body.forInputTM.step (self.scanCfg total) = some self.doneCfg

  The scanner exits on the first blank.

structure Complexity.TM.ForInputLoopSpaceSpec {n : ℕ} {body : TM n} {bodyTime : ℕ → ℕ} {total : ℕ} (spec : body.ForInputLoopSpec bodyTime total) (inputLength spaceBound : ℕ) : Prop

Space obligations needed to turn a ForInputLoopSpec into an all-prefix auxiliary-space certificate. The body obligation concerns only prefixes of its advertised exact run; later combined-machine execution may already have crossed the loopback seam.

• scanWithin (value : ℕ) : value ≤ total → (spec.scanCfg value).WithinAuxSpace inputLength spaceBound

  Every canonical scanner configuration is within the space budget.

• doneWithin : spec.doneCfg.WithinAuxSpace inputLength spaceBound

  The canonical final configuration is within the space budget.

• bodyPrefixWithin (value t : ℕ) (c : Cfg n body.forInputTM.Q) : value < total → t ≤ bodyTime value → body.forInputTM.reachesIn t (spec.bodyStartCfg value) c → c.WithinAuxSpace inputLength spaceBound

  Every prefix of each exact body run is within the space budget.