Correctness of the generic finite-state scanner

Proofs that TM.scannerTM correctly implements a left-to-right fold with |x| + 2-step running time.

Main results

• TM.scannerTM_reachesIn — the scanner halts in |x| + 2 steps on every input x, writing finalOutput (x.foldl scanStep s₀) to output cell 1.
• TM.scannerTM_decidesInTime — bridge to DecidesInTime for any language characterized by x ∈ L ↔ finalOutput (x.foldl scanStep s₀) = Γw.one.

theorem Complexity.TM.scannerTM_reachesIn {S : Type} [DecidableEq S] [Fintype S] (s₀ : S) (scanStep : S → Bool → S) (finalOutput : S → Γw) (x : List Bool) : ∃ (c' : Cfg 0 (scannerTM s₀ scanStep finalOutput).Q), (scannerTM s₀ scanStep finalOutput).reachesIn (x.length + 2) ((scannerTM s₀ scanStep finalOutput).initCfg x) c' ∧ (scannerTM s₀ scanStep finalOutput).halted c' ∧ c'.output.cells 1 = (finalOutput (List.foldl scanStep s₀ x)).toΓ

scannerTM halts in |x| + 2 steps and emits the fold result.

Output cell 1 is set to finalOutput (x.foldl scanStep s₀), and the machine reaches a halted configuration in exactly |x| + 2 steps on every input.

theorem Complexity.TM.scannerTM_decidesInTime {S : Type} [DecidableEq S] [Fintype S] (s₀ : S) (scanStep : S → Bool → S) (accept : S → Bool) {L : Language} (hL : ∀ (x : List Bool), x ∈ L ↔ accept (List.foldl scanStep s₀ x) = true) : (scannerTM s₀ scanStep fun (s : S) => if accept s = true then Γw.one else Γw.zero).DecidesInTime L fun (n : ℕ) => n + 2

Bridge to DecidesInTime. Whenever a language L is characterized by a decision predicate accept : S → Bool applied to the fold, the scanner with finalOutput fun s => if accept s then .one else .zero decides L in time n + 2.