Scanning several tapes in lockstep with a finite control

Most of what a machine does to a fixed-width register is a scan: check that a layout is well formed, read a bounded amount of information out of it, compare it against another register, rewrite it. Each of those is a finite automaton walking the register from left to right, and none of them can be written with TM.loopTM, whose body forgets its control state between iterations.

Complexity.Scanner is that automaton, and Complexity.TM.twoPassTM runs it. The scan is two passes: rightward to the first blank, gathering into the control state, then leftward back to the left marker, this time checking what it passes against everything the rightward pass learned. A single verdict bit is left on a result tape. Two passes is what makes the pattern useful — one pass cannot act on what it has not yet read.

The scan only ever reads. That costs nothing, because on a nondeterministic machine anything that would have to be computed can instead be guessed and checked — and checking is a scan. Tape contents are therefore invariant across a scan, which is what keeps its contract short.

All the tapes move together, so a column of the scan is the tuple of symbols under the heads. Tape 0 is the one whose blank ends the rightward pass; the others are read for as long as it lasts.

Main definitions

• Complexity.Scanner — a two-pass finite-state transducer over j + 1 tapes
• Complexity.TM.twoPassTM — the machine that runs it
• Complexity.Scanner.runR, Complexity.Scanner.runL, Complexity.Scanner.run — what a scan computes
• Complexity.Scanner.prefixed — read parameters off the first cells, then run the check they choose
• Complexity.Scanner.bitsStep — the reader that puts several registers' leading bits in the control
• Complexity.Scanner.chunkRun, Complexity.Scanner.chunkStepCell — folding three columns at a time
• Complexity.Scanner.comap — run a check on a wider tape set by naming its columns
• Complexity.Scanner.upTo, Complexity.Scanner.after — freeze a check once it has read its own cells, or start it after a prefix, so checks of different lengths and positions share a scan
• Complexity.Scanner.all, Complexity.Scanner.or — run several checks in one scan, conjoining or disjoining their verdicts
• Complexity.Scanner.eq, Complexity.Scanner.eq_range_run — the comparison scanner, and what it decides when restricted to a range of cells
• Complexity.Scanner.isConst, Complexity.Scanner.isConst_cell, Complexity.Scanner.isNotConst, Complexity.Scanner.isNotConst_cell — checking one cell against a fixed symbol, or against its failing to be one
• Complexity.Scanner.isConst_range_run, Complexity.Scanner.isNotConst_range_run — the same over a range of cells, which is how a field is tested for being all zeros
• Complexity.Scanner.plusOne — the increment-check scanner
• Complexity.Scanner.andAll, Complexity.Scanner.andSome, Complexity.Scanner.andFirst, Complexity.Scanner.firstCol — the scanners that combine verdicts

Main results

• Complexity.TM.checkTM, Complexity.TM.checkTM_hoareTime — a check run on the whole register set, reading the columns its map names
• Complexity.TM.twoPassCfg_run — a scan of a length-len tape takes 2 * len + 3 steps and halts with the automaton's verdict on the result tape, every other tape untouched
• Complexity.TM.twoPassTM_hoareTime — the same as a Hoare triple, for composition
• Complexity.Scanner.eq_run — the smallest example: comparing two of the tapes
• Complexity.Scanner.prefixed_run — a parameterized scan reports what its parameters chose
• Complexity.Scanner.bitsStep_run — what the field reader has read
• Complexity.Scanner.cellFold_chunk — three cells make a chunk
• Complexity.Scanner.cellFold_shift, Complexity.Scanner.runR_eq_cellFold — a check proved at the start of a scan applies wherever the scan puts it
• Complexity.Scanner.plusOne_run — one scan checks that one register holds one more than another
• Complexity.Scanner.andAll_run, Complexity.Scanner.andSome_run, Complexity.Scanner.andFirst_run, Complexity.Scanner.firstCol_run — and one scan reports any function of the verdicts

structure Complexity.Scanner (j : ℕ) : Type 1

A two-pass finite-state transducer over j + 1 tapes scanned in lockstep. The rightward pass only reads; the leftward pass may rewrite the column it is on.

• σ : Type

  The control states of the automaton.

• decEqσ : DecidableEq self.σ
• finσ : Fintype self.σ
• start : self.σ

  Where the rightward pass starts.

• stepR : self.σ → (Fin (j + 1) → Γ) → self.σ

  The rightward pass: read a column, update the state.

• stepL : self.σ → (Fin (j + 1) → Γ) → self.σ

  The leftward pass: read a column, update the state.

• emit : self.σ → Bool

  The verdict left on the result tape.

def Complexity.Scanner.runR {j : ℕ} (S : Scanner j) (cols : ℕ → Fin (j + 1) → Γ) : ℕ → S.σ

The state after the rightward pass has read cells 1 through p.

Equations

• S.runR cols 0 = S.start
• S.runR cols p.succ = S.stepR (S.runR cols p) (cols (p + 1))

def Complexity.Scanner.runL {j : ℕ} (S : Scanner j) (cols : ℕ → Fin (j + 1) → Γ) : ℕ → S.σ → S.σ

The state the leftward pass ends in, having read cells p down to 1.

Equations

• S.runL cols 0 x✝ = x✝
• S.runL cols p.succ x✝ = S.runL cols p (S.stepL x✝ (cols (p + 1)))

def Complexity.Scanner.run {j : ℕ} (S : Scanner j) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) : S.σ

What a whole scan computes: the rightward pass over cells 1 … len, then the leftward pass back over len … 1.

Equations

• S.run cols len = S.runL cols len (S.runR cols len)

Scanners that only read on the way out

When everything a check needs is available before the cells it has to check — which is arranged by laying the parameters out in the first few cells of the scan and starting the data after them — the leftward pass has nothing to do.

def Complexity.Scanner.ofRight {j : ℕ} (τ : Type) [DecidableEq τ] [Fintype τ] (start : τ) (step : τ → (Fin (j + 1) → Γ) → τ) (emit : τ → Bool) : Scanner j

A scanner whose leftward pass is idle.

Equations

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

@[simp]

theorem Complexity.Scanner.ofRight_runL {j : ℕ} (τ : Type) [DecidableEq τ] [Fintype τ] (start : τ) (step : τ → (Fin (j + 1) → Γ) → τ) (emit : τ → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : τ) : (ofRight τ start step emit).runL cols p s = s

theorem Complexity.Scanner.ofRight_run {j : ℕ} (τ : Type) [DecidableEq τ] [Fintype τ] (start : τ) (step : τ → (Fin (j + 1) → Γ) → τ) (emit : τ → Bool) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) : (ofRight τ start step emit).run cols len = (ofRight τ start step emit).runR cols len

Running a scanner on a wider tape set

A check is written against the few registers it reads. Running it on a machine that has many registers is a matter of saying which columns those are — not of moving the registers next to one another, and not of giving each check its own copy of them.

def Complexity.Scanner.comap {j jj : ℕ} (S : Scanner j) (f : Fin (j + 1) → Fin (jj + 1)) : Scanner jj

Read a scanner's columns through a map: the same automaton, run on a wider tape set.

Equations

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

@[simp]

theorem Complexity.Scanner.comap_emit {j jj : ℕ} (S : Scanner j) (f : Fin (j + 1) → Fin (jj + 1)) : (S.comap f).emit = S.emit

theorem Complexity.Scanner.comap_runR {j jj : ℕ} (S : Scanner j) (f : Fin (j + 1) → Fin (jj + 1)) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) : (S.comap f).runR cols p = S.runR (fun (q : ℕ) (i : Fin (j + 1)) => cols q (f i)) p

theorem Complexity.Scanner.comap_runL {j jj : ℕ} (S : Scanner j) (f : Fin (j + 1) → Fin (jj + 1)) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) (s : S.σ) : (S.comap f).runL cols p s = S.runL (fun (q : ℕ) (i : Fin (j + 1)) => cols q (f i)) p s

theorem Complexity.Scanner.comap_run {j jj : ℕ} (S : Scanner j) (f : Fin (j + 1) → Fin (jj + 1)) (cols : ℕ → Fin (jj + 1) → Γ) (len : ℕ) : (S.comap f).run cols len = S.run (fun (q : ℕ) (i : Fin (j + 1)) => cols q (f i)) len

A scanner run through a map reads exactly the columns the map names.

Stopping a check early

Checks read different numbers of cells, but a machine's scan has one length. A right-only check can simply be frozen once it has read the cells it cares about: the columns past that point are read and discarded, so a short check and a long one can share a scan.

def Complexity.Scanner.RightOnly {j : ℕ} (S : Scanner j) : Prop

A scanner whose leftward pass does nothing — the shape of every check built with Complexity.Scanner.ofRight or Complexity.Scanner.prefixed.

Equations

• S.RightOnly = ∀ (s : S.σ) (cols : Fin (j + 1) → Complexity.Γ), S.stepL s cols = s

theorem Complexity.Scanner.rightOnly_ofRight {j : ℕ} (τ : Type) [DecidableEq τ] [Fintype τ] (start : τ) (step : τ → (Fin (j + 1) → Γ) → τ) (emit : τ → Bool) : (ofRight τ start step emit).RightOnly

theorem Complexity.Scanner.rightOnly_comap {j jj : ℕ} {S : Scanner j} (h : S.RightOnly) (f : Fin (j + 1) → Fin (jj + 1)) : (S.comap f).RightOnly

theorem Complexity.Scanner.runL_of_rightOnly {j : ℕ} {S : Scanner j} (hS : S.RightOnly) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : S.σ) : S.runL cols p s = s

A right-only scanner's leftward pass leaves the state alone.

def Complexity.Scanner.upToIdx (w p : ℕ) : Fin (w + 1)

The saturating position counter a frozen check carries.

Equations

• Complexity.Scanner.upToIdx w p = ⟨min p w, ⋯⟩

def Complexity.Scanner.upTo {j : ℕ} (S : Scanner j) (w : ℕ) : Scanner j

Run a scanner over the first w cells, then freeze.

Equations

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

theorem Complexity.Scanner.upTo_runR {j : ℕ} (S : Scanner j) (w : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (S.upTo w).runR cols p = (S.runR cols (min p w), upToIdx w p)

theorem Complexity.Scanner.upTo_runL {j : ℕ} (S : Scanner j) (w : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : (S.upTo w).σ) : (S.upTo w).runL cols p s = (S.runL cols p s.1, s.2)

theorem Complexity.Scanner.upTo_emit_run {j : ℕ} (S : Scanner j) (hS : S.RightOnly) (w len : ℕ) (hw : w ≤ len) (cols : ℕ → Fin (j + 1) → Γ) : (S.upTo w).emit ((S.upTo w).run cols len) = S.emit (S.run cols w)

A frozen check gives the verdict it would have given on its own cells.

def Complexity.Scanner.after {j : ℕ} (S : Scanner j) (w : ℕ) : Scanner j

Skip the first w cells, then run a scanner over the rest. Together with Complexity.Scanner.upTo this restricts a check to any range of cells, which is what pins a guessed value against a field that does not sit at the start of its register.

Equations

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

theorem Complexity.Scanner.rightOnly_after {j : ℕ} {S : Scanner j} (h : S.RightOnly) (w : ℕ) : (S.after w).RightOnly

theorem Complexity.Scanner.after_runR {j : ℕ} (S : Scanner j) (w : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (S.after w).runR cols p = (S.runR (fun (q : ℕ) => cols (w + q)) (p - w), upToIdx w p)

theorem Complexity.Scanner.after_runL {j : ℕ} (S : Scanner j) (w : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : (S.after w).σ) : (S.after w).runL cols p s = (S.runL cols p s.1, s.2)

theorem Complexity.Scanner.after_emit_run {j : ℕ} (S : Scanner j) (hS : S.RightOnly) (w len : ℕ) (cols : ℕ → Fin (j + 1) → Γ) : (S.after w).emit ((S.after w).run cols len) = S.emit (S.run (fun (q : ℕ) => cols (w + q)) (len - w))

A check that skips a prefix reads the cells after it.

theorem Complexity.Scanner.range_emit_run {j : ℕ} (S : Scanner j) (hS : S.RightOnly) (w₁ w₂ len : ℕ) (hw : w₂ ≤ len) (cols : ℕ → Fin (j + 1) → Γ) : ((S.after w₁).upTo w₂).emit (((S.after w₁).upTo w₂).run cols len) = S.emit (S.run (fun (q : ℕ) => cols (w₁ + q)) (w₂ - w₁))

A check restricted to a range of cells.

Running several checks in one scan

A machine has one result tape, and a two-pass scan writes it at the very end. Rather than give each check its own tape and combine the verdicts afterwards, the checks run together: one automaton whose state is the tuple of theirs, whose verdict is their conjunction. Each component still runs exactly the scan it would have run alone, so the lemmas about the individual checks apply unchanged.

noncomputable def Complexity.Scanner.all {jj : ℕ} (n : ℕ) (S : Fin n → Scanner jj) : Scanner jj

Run several scanners at once, emitting the conjunction of their verdicts.

Equations

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

theorem Complexity.Scanner.all_runR {jj : ℕ} (n : ℕ) (S : Fin n → Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) (i : Fin n) : (all n S).runR cols p i = (S i).runR cols p

theorem Complexity.Scanner.all_runL {jj : ℕ} (n : ℕ) (S : Fin n → Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) (s : (all n S).σ) (i : Fin n) : (all n S).runL cols p s i = (S i).runL cols p (s i)

theorem Complexity.Scanner.all_run {jj : ℕ} (n : ℕ) (S : Fin n → Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (len : ℕ) (i : Fin n) : (all n S).run cols len i = (S i).run cols len

Each component of a joint scan runs its own scan.

theorem Complexity.Scanner.all_emit_run {jj : ℕ} (n : ℕ) (S : Fin n → Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (len : ℕ) : (all n S).emit ((all n S).run cols len) = true ↔ ∀ (i : Fin n), (S i).emit ((S i).run cols len) = true

A joint scan accepts exactly when every component does.

def Complexity.Scanner.or {jj : ℕ} (S T : Scanner jj) : Scanner jj

Run two scanners at once, emitting the disjunction of their verdicts: the walk's step either keeps its configuration or advances it.

Equations

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

theorem Complexity.Scanner.or_runR {jj : ℕ} (S T : Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) : (S.or T).runR cols p = (S.runR cols p, T.runR cols p)

theorem Complexity.Scanner.or_runL {jj : ℕ} (S T : Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (p : ℕ) (s : S.σ × T.σ) : (S.or T).runL cols p s = (S.runL cols p s.1, T.runL cols p s.2)

theorem Complexity.Scanner.or_emit_run {jj : ℕ} (S T : Scanner jj) (cols : ℕ → Fin (jj + 1) → Γ) (len : ℕ) : (S.or T).emit ((S.or T).run cols len) = true ↔ S.emit (S.run cols len) = true ∨ T.emit (T.run cols len) = true

A disjunctive scan accepts exactly when one of its halves does.

Reading parameters before checking

A check usually needs a few values — a symbol to compare against, a direction to move — that are themselves on a register. Laying them out in the first cells of the scan and starting the data after them lets one scan do both: read the parameters into the control, then run a check chosen by them.

def Complexity.Scanner.auxRun {j : ℕ} {α : Type} (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (cols : ℕ → Fin (j + 1) → Γ) : ℕ → α

The accumulated parameters after reading p columns.

Equations

• Complexity.Scanner.auxRun a₀ readStep cols 0 = a₀
• Complexity.Scanner.auxRun a₀ readStep cols p.succ = readStep (Complexity.Scanner.auxRun a₀ readStep cols p) (cols (p + 1))

def Complexity.Scanner.mainRun {j : ℕ} {α τ : Type} (c : ℕ) (a : α) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (cols : ℕ → Fin (j + 1) → Γ) (t₀ : τ) : ℕ → τ

The state of the parameterized check after q columns beyond the parameter block.

Equations

• Complexity.Scanner.mainRun c a mainStep cols t₀ 0 = t₀
• Complexity.Scanner.mainRun c a mainStep cols t₀ p.succ = mainStep a (Complexity.Scanner.mainRun c a mainStep cols t₀ p) (cols (c + p + 1))

def Complexity.Scanner.prefixed {j : ℕ} (c : ℕ) (α τ : Type) [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) : Scanner j

Read c columns of parameters, then check.

Equations

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

theorem Complexity.Scanner.rightOnly_prefixed {j : ℕ} {α τ : Type} [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (c : ℕ) (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) : (prefixed c α τ a₀ readStep t₀ mainStep emit).RightOnly

theorem Complexity.Scanner.prefixed_stepR {j : ℕ} {α τ : Type} [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (c : ℕ) (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) (s : Fin (c + 1) × α × τ) (col : Fin (j + 1) → Γ) : (prefixed c α τ a₀ readStep t₀ mainStep emit).stepR s col = if h : ↑s.1 < c then (⟨↑s.1 + 1, ⋯⟩, readStep s.2.1 col, if ↑s.1 + 1 = c then t₀ (readStep s.2.1 col) else s.2.2) else (s.1, s.2.1, mainStep s.2.1 s.2.2 col)

theorem Complexity.Scanner.prefixed_runR_le {j : ℕ} {α τ : Type} [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (c : ℕ) (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : p ≤ c → ↑((prefixed c α τ a₀ readStep t₀ mainStep emit).runR cols p).1 = p ∧ ((prefixed c α τ a₀ readStep t₀ mainStep emit).runR cols p).2.1 = auxRun a₀ readStep cols p

Through the parameter block, the scan is just accumulating parameters.

theorem Complexity.Scanner.prefixed_runR {j : ℕ} {α τ : Type} [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (c : ℕ) (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) (cols : ℕ → Fin (j + 1) → Γ) (hc : 0 < c) (q : ℕ) : (prefixed c α τ a₀ readStep t₀ mainStep emit).runR cols (c + q) = (⟨c, ⋯⟩, auxRun a₀ readStep cols c, mainRun c (auxRun a₀ readStep cols c) mainStep cols (t₀ (auxRun a₀ readStep cols c)) q)

Past the parameter block, the scan runs the check the parameters chose.

theorem Complexity.Scanner.prefixed_run {j : ℕ} {α τ : Type} [DecidableEq α] [Fintype α] [DecidableEq τ] [Fintype τ] (c : ℕ) (a₀ : α) (readStep : α → (Fin (j + 1) → Γ) → α) (t₀ : α → τ) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (emit : α → τ → Bool) (cols : ℕ → Fin (j + 1) → Γ) (hc : 0 < c) (q : ℕ) : (prefixed c α τ a₀ readStep t₀ mainStep emit).emit ((prefixed c α τ a₀ readStep t₀ mainStep emit).run cols (c + q)) = emit (auxRun a₀ readStep cols c) (mainRun c (auxRun a₀ readStep cols c) mainStep cols (t₀ (auxRun a₀ readStep cols c)) q)

What a parameterized scan reports: the check the parameters chose, run on the data after them.

Reading fixed-width fields into the control

The parameters a check needs — a state, a symbol, a direction — sit in the first few cells of their own registers. This reads all of them at once: s registers, w cells each, into a table of bits the check can consult.

def Complexity.Scanner.bitAt {j : ℕ} (cols : ℕ → Fin (j + 1) → Γ) (a : Fin (j + 1)) (p : ℕ) : Bool

The bit a scan sees on a register at a given cell.

Equations

• Complexity.Scanner.bitAt cols a p = decide (cols p a = Complexity.Γ.one)

def Complexity.Scanner.bitsStep {j : ℕ} (s w : ℕ) (regs : Fin s → Fin (j + 1)) (x : Fin (w + 1) × (Fin s → Fin w → Bool)) (col : Fin (j + 1) → Γ) : Fin (w + 1) × (Fin s → Fin w → Bool)

Read the first w cells of each of s registers into a table of bits.

Equations

• Complexity.Scanner.bitsStep s w regs x col = if h : ↑x.1 < w then (⟨↑x.1 + 1, ⋯⟩, fun (t : Fin s) => Function.update (x.2 t) ⟨↑x.1, h⟩ (decide (col (regs t) = Complexity.Γ.one))) else x

theorem Complexity.Scanner.auxRun_bitsStep_congr {j s w : ℕ} (regs : Fin s → Fin (j + 1)) (cols cols' : ℕ → Fin (j + 1) → Γ) (h : ∀ (q : ℕ) (t : Fin s), cols q (regs t) = cols' q (regs t)) (x₀ : Fin s → Fin w → Bool) (p : ℕ) : auxRun (⟨0, ⋯⟩, x₀) (bitsStep s w regs) cols p = auxRun (⟨0, ⋯⟩, x₀) (bitsStep s w regs) cols' p

A field reader sees only the registers it names. Two scans whose named registers agree read the same table — which is what makes several checks reading the same parameter register agree on the parameters.

theorem Complexity.Scanner.bitsStep_run {j : ℕ} (s w : ℕ) (regs : Fin s → Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (x₀ : Fin s → Fin w → Bool) (p : ℕ) : p ≤ w → ↑(auxRun (⟨0, ⋯⟩, x₀) (bitsStep s w regs) cols p).1 = p ∧ ∀ (t : Fin s) (i : Fin w), ↑i < p → (auxRun (⟨0, ⋯⟩, x₀) (bitsStep s w regs) cols p).2 t i = bitAt cols (regs t) (↑i + 1)

What the field reader has read. After p ≤ w columns the table holds the first p bits of every register.

Folding three columns at a time

A marked block stores each cell as a chunk of three bits — the head marker first, so that a rightward pass knows whether the head is on a cell before it reads that cell's symbol. Checks on such a block are naturally written a chunk at a time, and Complexity.Scanner.cellFold_chunk says that a cell-level fold which buffers two columns and acts on the third computes exactly the chunk-level fold.

def Complexity.Scanner.cellFold {j : ℕ} {σ : Type} (g : σ → (Fin (j + 1) → Γ) → σ) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (s₀ : σ) : ℕ → σ

A plain fold over the columns from off + 1 onwards.

Equations

• Complexity.Scanner.cellFold g cols off s₀ 0 = s₀
• Complexity.Scanner.cellFold g cols off s₀ p.succ = g (Complexity.Scanner.cellFold g cols off s₀ p) (cols (off + p + 1))

theorem Complexity.Scanner.mainRun_eq_cellFold {j : ℕ} {α τ : Type} (c : ℕ) (a : α) (mainStep : α → τ → (Fin (j + 1) → Γ) → τ) (cols : ℕ → Fin (j + 1) → Γ) (t₀ : τ) (q : ℕ) : mainRun c a mainStep cols t₀ q = cellFold (mainStep a) cols c t₀ q

theorem Complexity.Scanner.cellFold_shift {j : ℕ} {σ : Type} (g : σ → (Fin (j + 1) → Γ) → σ) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (s₀ : σ) (p : ℕ) : cellFold g cols off s₀ p = cellFold g (fun (t : ℕ) => cols (off + t)) 0 s₀ p

A fold started later is the same fold on shifted columns, so a check proved at the start of a scan applies wherever the scan puts it.

theorem Complexity.Scanner.runR_eq_cellFold {j : ℕ} (S : Scanner j) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : S.runR cols p = cellFold S.stepR cols 0 S.start p

A scanner's rightward pass is a plain fold.

def Complexity.Scanner.chunkRun {j : ℕ} {χ : Type} (f : χ → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → χ) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (x₀ : χ) : ℕ → χ

A fold that consumes three columns at a time.

Equations

• Complexity.Scanner.chunkRun f cols off x₀ 0 = x₀
• Complexity.Scanner.chunkRun f cols off x₀ p.succ = f (Complexity.Scanner.chunkRun f cols off x₀ p) (cols (off + 3 * p + 1)) (cols (off + 3 * p + 2)) (cols (off + 3 * p + 3))

def Complexity.Scanner.chunkStepCell {j : ℕ} {χ : Type} (f : χ → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → χ) (s : Fin 3 × (Fin (j + 1) → Γ) × (Fin (j + 1) → Γ) × χ) (col : Fin (j + 1) → Γ) : Fin 3 × (Fin (j + 1) → Γ) × (Fin (j + 1) → Γ) × χ

The cell-level step that buffers two columns and acts on the third.

Equations

• Complexity.Scanner.chunkStepCell f s col = if s.1 = 0 then (1, col, s.2.2.1, s.2.2.2) else if s.1 = 1 then (2, s.2.1, col, s.2.2.2) else (0, s.2.1, s.2.2.1, f s.2.2.2 s.2.1 s.2.2.1 col)

theorem Complexity.Scanner.cellFold_chunk {j : ℕ} {χ : Type} (f : χ → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → (Fin (j + 1) → Γ) → χ) (cols : ℕ → Fin (j + 1) → Γ) (off : ℕ) (x₀ : χ) (u v : Fin (j + 1) → Γ) (p : ℕ) : (cellFold (chunkStepCell f) cols off (0, u, v, x₀) (3 * p)).1 = 0 ∧ (cellFold (chunkStepCell f) cols off (0, u, v, x₀) (3 * p)).2.2.2 = chunkRun f cols off x₀ p

Three cells make a chunk.

A first scanner: register equality

def Complexity.Scanner.eq (j : ℕ) (a b : Fin (j + 1)) : Scanner j

Compare two of the scanned tapes cell by cell.

Equations

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

theorem Complexity.Scanner.rightOnly_eq (j : ℕ) (a b : Fin (j + 1)) : (eq j a b).RightOnly

@[simp]

theorem Complexity.Scanner.eq_runL (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : Bool) : (eq j a b).runL cols p s = s

theorem Complexity.Scanner.eq_runR (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (eq j a b).runR cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → cols q a = cols q b

theorem Complexity.Scanner.eq_run (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) : (eq j a b).run cols len = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ len → cols q a = cols q b

What the equality scanner reports.

theorem Complexity.Scanner.eq_range_run (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (w₁ w₂ len : ℕ) (hw : w₂ ≤ len) : (((eq j a b).after w₁).upTo w₂).emit ((((eq j a b).after w₁).upTo w₂).run cols len) = true ↔ ∀ (q : ℕ), w₁ < q → q ≤ w₂ → cols q a = cols q b

A comparison restricted to a range of cells decides equality there. This is how a small guessed register is pinned against a field sitting anywhere inside a bigger one.

def Complexity.Scanner.isConst (j : ℕ) (a : Fin (j + 1)) (g : Γ) : Scanner j

Check that a register carries a fixed symbol. Frozen to one cell by Complexity.Scanner.upTo this reads a single cell, which is how a one-cell register — a direction, say — is checked against a constant.

Equations

• Complexity.Scanner.isConst j a g = Complexity.Scanner.ofRight Bool true (fun (s : Bool) (cols : Fin (j + 1) → Complexity.Γ) => s && decide (cols a = g)) id

theorem Complexity.Scanner.isConst_runR (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (isConst j a g).runR cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → cols q a = g

theorem Complexity.Scanner.isConst_runL (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : Bool) : (isConst j a g).runL cols p s = s

theorem Complexity.Scanner.isConst_run (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) : (isConst j a g).run cols len = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ len → cols q a = g

theorem Complexity.Scanner.rightOnly_isConst (j : ℕ) (a : Fin (j + 1)) (g : Γ) : (isConst j a g).RightOnly

theorem Complexity.Scanner.isConst_upTo_run (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (w len : ℕ) (hlen : w ≤ len) : ((isConst j a g).upTo w).emit (((isConst j a g).upTo w).run cols len) = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ w → cols q a = g

A check over a prefix of cells.

theorem Complexity.Scanner.isConst_cell (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) (hlen : 1 ≤ len) : ((isConst j a g).upTo 1).emit (((isConst j a g).upTo 1).run cols len) = true ↔ cols 1 a = g

A one-cell check.

def Complexity.Scanner.isNotConst (j : ℕ) (a : Fin (j + 1)) (g : Γ) : Scanner j

Check that a register does not carry a fixed symbol. Frozen to one cell this is the negation of Complexity.Scanner.isConst, which is what a loop's test needs when a failed check should stop it.

Equations

• Complexity.Scanner.isNotConst j a g = Complexity.Scanner.ofRight Bool false (fun (s : Bool) (cols : Fin (j + 1) → Complexity.Γ) => s || decide (cols a ≠ g)) id

theorem Complexity.Scanner.isNotConst_runR (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (isNotConst j a g).runR cols p = true ↔ ∃ (q : ℕ), 1 ≤ q ∧ q ≤ p ∧ cols q a ≠ g

theorem Complexity.Scanner.isNotConst_runL (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (s : Bool) : (isNotConst j a g).runL cols p s = s

theorem Complexity.Scanner.rightOnly_isNotConst (j : ℕ) (a : Fin (j + 1)) (g : Γ) : (isNotConst j a g).RightOnly

theorem Complexity.Scanner.isNotConst_cell (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) (hlen : 1 ≤ len) : ((isNotConst j a g).upTo 1).emit (((isNotConst j a g).upTo 1).run cols len) = true ↔ cols 1 a ≠ g

A one-cell inequality check.

theorem Complexity.Scanner.isConst_range_run (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (w₁ w₂ len : ℕ) (hw : w₂ ≤ len) : (((isConst j a g).after w₁).upTo w₂).emit ((((isConst j a g).after w₁).upTo w₂).run cols len) = true ↔ ∀ (q : ℕ), w₁ < q → q ≤ w₂ → cols q a = g

A constant check restricted to a range of cells.

theorem Complexity.Scanner.isNotConst_range_run (j : ℕ) (a : Fin (j + 1)) (g : Γ) (cols : ℕ → Fin (j + 1) → Γ) (w₁ w₂ len : ℕ) (hw : w₂ ≤ len) : (((isNotConst j a g).after w₁).upTo w₂).emit ((((isNotConst j a g).after w₁).upTo w₂).run cols len) = true ↔ ∃ (q : ℕ), w₁ < q ∧ q ≤ w₂ ∧ cols q a ≠ g

A difference check restricted to a range of cells.

A scanner that takes a conjunction

Each check writes its verdict to its own register; one more scan over those registers reports whether they all said yes.

def Complexity.Scanner.andAll (j : ℕ) : Scanner j

Report whether every scanned tape carries Γ.one throughout.

Equations

• Complexity.Scanner.andAll j = Complexity.Scanner.ofRight Bool true (fun (s : Bool) (cols : Fin (j + 1) → Complexity.Γ) => s && decide (∀ (i : Fin (j + 1)), cols i = Complexity.Γ.one)) id

@[simp]

theorem Complexity.Scanner.andAll_stepR (j : ℕ) (s : Bool) (cols : Fin (j + 1) → Γ) : (andAll j).stepR s cols = (s && decide (∀ (i : Fin (j + 1)), cols i = Γ.one))

theorem Complexity.Scanner.andAll_runR (j : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (andAll j).runR cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → ∀ (i : Fin (j + 1)), cols q i = Γ.one

theorem Complexity.Scanner.andAll_run (j : ℕ) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (andAll j).run cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → ∀ (i : Fin (j + 1)), cols q i = Γ.one

What the conjunction scanner reports.

def Complexity.Scanner.andSome (j : ℕ) (P : Fin (j + 1) → Bool) : Scanner j

Report whether the designated tapes all carry Γ.one. The verdict registers of a composite check are scattered — each check owns a contiguous block, so their result tapes are not adjacent — so the combining scan reads every tape and looks only at the ones it is told to.

Equations

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

@[simp]

theorem Complexity.Scanner.andSome_stepR (j : ℕ) (P : Fin (j + 1) → Bool) (s : Bool) (cols : Fin (j + 1) → Γ) : (andSome j P).stepR s cols = (s && decide (∀ (i : Fin (j + 1)), P i = true → cols i = Γ.one))

theorem Complexity.Scanner.andSome_runR (j : ℕ) (P : Fin (j + 1) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (andSome j P).runR cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → ∀ (i : Fin (j + 1)), P i = true → cols q i = Γ.one

theorem Complexity.Scanner.andSome_run (j : ℕ) (P : Fin (j + 1) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (andSome j P).run cols p = true ↔ ∀ (q : ℕ), 1 ≤ q → q ≤ p → ∀ (i : Fin (j + 1)), P i = true → cols q i = Γ.one

What the selective conjunction scanner reports.

def Complexity.Scanner.andFirst (j : ℕ) (P : Fin (j + 1) → Bool) : Scanner j

Report whether the designated tapes carry Γ.one in their first cell. A verdict register holds a single bit and blanks after it, so a scan whose length is set by some longer register must look only at the first column.

Equations

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

theorem Complexity.Scanner.andFirst_runR (j : ℕ) (P : Fin (j + 1) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (andFirst j P).runR cols p = (if p = 0 then true else decide (∀ (i : Fin (j + 1)), P i = true → cols 1 i = Γ.one), decide (0 < p))

theorem Complexity.Scanner.andFirst_run (j : ℕ) (P : Fin (j + 1) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (hp : 0 < p) : (andFirst j P).emit ((andFirst j P).run cols p) = true ↔ ∀ (i : Fin (j + 1)), P i = true → cols 1 i = Γ.one

What the first-cell conjunction scanner reports.

def Complexity.Scanner.firstCol (j : ℕ) (f : (Fin (j + 1) → Γ) → Bool) : Scanner j

Report an arbitrary function of the first column. Verdict registers hold a single bit each, so a composite decision — "these checks all passed, or those did" — is a function of one column, however long the scan turns out to be.

Equations

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

theorem Complexity.Scanner.firstCol_runR (j : ℕ) (f : (Fin (j + 1) → Γ) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : (firstCol j f).runR cols p = (if p = 0 then true else f (cols 1), decide (0 < p))

theorem Complexity.Scanner.firstCol_run (j : ℕ) (f : (Fin (j + 1) → Γ) → Bool) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) (hp : 0 < p) : (firstCol j f).emit ((firstCol j f).run cols p) = f (cols 1)

What the first-column scanner reports.

A scanner that checks an increment

Registers hold little-endian bits, so a scan meets them least significant first — which is the order an increment carries in.

def Complexity.Scanner.valUpTo (f : ℕ → Bool) : ℕ → ℕ

The value of the first p bits of a register, read little-endian.

Equations

• Complexity.Scanner.valUpTo f 0 = 0
• Complexity.Scanner.valUpTo f p.succ = Complexity.Scanner.valUpTo f p + if f (p + 1) = true then 2 ^ p else 0

def Complexity.Scanner.plusOne (j : ℕ) (a b : Fin (j + 1)) : Scanner j

Check that register b holds one more than register a.

Equations

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

theorem Complexity.Scanner.valUpTo_lt (f : ℕ → Bool) (p : ℕ) : valUpTo f p < 2 ^ p

The value of p bits fits in p bits.

theorem Complexity.Scanner.plusOne_runR (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (p : ℕ) : ∃ (c : Bool) (v : Bool), (plusOne j a b).runR cols p = (c, v) ∧ (c = true ↔ valUpTo (bitAt cols a) p + 1 = 2 ^ p) ∧ (v = true ↔ (valUpTo (bitAt cols b) p + if c = true then 2 ^ p else 0) = valUpTo (bitAt cols a) p + 1)

The invariant of the increment check. The carry is exactly "every bit of a so far was one", and the running verdict says exactly that the bits of b so far are those of a + 1.

theorem Complexity.Scanner.plusOne_run (j : ℕ) (a b : Fin (j + 1)) (cols : ℕ → Fin (j + 1) → Γ) (len : ℕ) : (plusOne j a b).emit ((plusOne j a b).run cols len) = true ↔ valUpTo (bitAt cols b) len = valUpTo (bitAt cols a) len + 1

What the increment scanner reports.

inductive Complexity.TM.TwoPassPhase : Type

The control phases of TM.twoPassTM.

• right : TwoPassPhase

  Walking right to the first blank of tape 0.

• left : TwoPassPhase

  Walking back left to the left marker.

• emit : TwoPassPhase

  Publishing the verdict.

• done : TwoPassPhase

  Halted.

@[instance_reducible]

instance Complexity.TM.instDecidableEqTwoPassPhase : DecidableEq TwoPassPhase

Equations

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

@[instance_reducible]

instance Complexity.TM.instFintypeTwoPassPhase : Fintype TwoPassPhase

Equations

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

@[reducible, inline]

abbrev Complexity.TM.TwoPassQ {j : ℕ} (S : Scanner j) : Type

The control states of the scanning machine: a phase and the automaton's own state.

Equations

• Complexity.TM.TwoPassQ S = (Complexity.TM.TwoPassPhase × S.σ)

@[instance_reducible]

instance Complexity.TM.instDecidableEqTwoPassQ {j : ℕ} (S : Scanner j) : DecidableEq (TwoPassQ S)

Equations

• Complexity.TM.instDecidableEqTwoPassQ S a b = instDecidableEqProd a b

@[instance_reducible]

instance Complexity.TM.instFintypeTwoPassQ {j : ℕ} (S : Scanner j) : Fintype (TwoPassQ S)

Equations

• Complexity.TM.instFintypeTwoPassQ S = { elems := Finset.univ ×ˢ Finset.univ, complete := ⋯ }

def Complexity.TM.twoPassTM {j : ℕ} (S : Scanner j) : TM (j + 2)

The scanning machine. Work tapes 0 … j are scanned in lockstep and work tape j + 1 receives the verdict.

Equations

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

What one step does

def Complexity.TM.scanCol {j : ℕ} (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) : Fin (j + 1) → Γ

The column of symbols under the scanned heads when they are all at cell h.

Equations

• Complexity.TM.scanCol cells h i = cells i h

def Complexity.TM.twoPassCfg {j : ℕ} (S : Scanner j) (q : TwoPassQ S) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) : Cfg (j + 2) (twoPassTM S).Q

A configuration of the scanning machine: every scanned head at cell h.

Equations

• Complexity.TM.twoPassCfg S q inp cells h res out = { state := q, input := inp, work := Fin.snoc (fun (i : Fin (j + 1)) => { head := h, cells := cells i }) res, output := out }

structure Complexity.TM.ScanOk (inp res out : Tape) : Prop

The tapes a scan leaves alone: their heads are off the left marker, so every step writes them back unchanged and idles them.

• inp : inp.read ≠ Γ.start

  The input head is off the left marker.

• res : res.read ≠ Γ.start

  The result head is off the left marker.

• out : out.read ≠ Γ.start

  The output head is off the left marker.

theorem Complexity.TM.twoPassCfg_step_right {j : ℕ} (S : Scanner j) (s : S.σ) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) (hok : ScanOk inp res out) (hc : ∀ (i : Fin (j + 1)), cells i h ≠ Γ.start) (hne : cells 0 h ≠ Γ.blank) : (twoPassTM S).stepCfg (twoPassCfg S (TwoPassPhase.right, s) inp cells h res out) = twoPassCfg S (TwoPassPhase.right, S.stepR s (scanCol cells h)) inp cells (h + 1) res out

The rightward pass, while tape 0 has not run out.

theorem Complexity.TM.twoPassCfg_step_turn {j : ℕ} (S : Scanner j) (s : S.σ) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) (hok : ScanOk inp res out) (hc : ∀ (i : Fin (j + 1)), cells i h ≠ Γ.start) (hb : cells 0 h = Γ.blank) : (twoPassTM S).stepCfg (twoPassCfg S (TwoPassPhase.right, s) inp cells h res out) = twoPassCfg S (TwoPassPhase.left, s) inp cells (h - 1) res out

The turn: tape 0 has run out, so the scan starts back.

theorem Complexity.TM.twoPassCfg_step_left {j : ℕ} (S : Scanner j) (s : S.σ) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) (hok : ScanOk inp res out) (hc : ∀ (i : Fin (j + 1)), cells i h ≠ Γ.start) : (twoPassTM S).stepCfg (twoPassCfg S (TwoPassPhase.left, s) inp cells h res out) = twoPassCfg S (TwoPassPhase.left, S.stepL s (scanCol cells h)) inp cells (h - 1) res out

The leftward pass, while the left marker is not yet in sight.

theorem Complexity.TM.twoPassCfg_step_stop {j : ℕ} (S : Scanner j) (s : S.σ) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (res out : Tape) (hok : ScanOk inp res out) (hs : ∀ (i : Fin (j + 1)), cells i 0 = Γ.start) : (twoPassTM S).stepCfg (twoPassCfg S (TwoPassPhase.left, s) inp cells 0 res out) = twoPassCfg S (TwoPassPhase.emit, s) inp cells 1 res out

The leftward pass reaches the marker and the scan turns to publishing.

theorem Complexity.TM.twoPassCfg_step_emit {j : ℕ} (S : Scanner j) (s : S.σ) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) (hok : ScanOk inp res out) (hc : ∀ (i : Fin (j + 1)), cells i h ≠ Γ.start) : (twoPassTM S).stepCfg (twoPassCfg S (TwoPassPhase.emit, s) inp cells h res out) = twoPassCfg S (TwoPassPhase.done, S.start) inp cells h (res.write (Γ.ofBool (S.emit s))) out

Publishing the verdict: one bit onto the result tape, then halt.

What a whole scan does

structure Complexity.TM.ScanTape {j : ℕ} (cells : Fin (j + 1) → ℕ → Γ) (len : ℕ) : Prop

The tape shape a scan expects: every tape carries its left marker and nothing else does, and tape 0 runs for exactly len cells.

• start (i : Fin (j + 1)) : cells i 0 = Γ.start

  Cell zero of every scanned tape is the left marker.

• ne_start (i : Fin (j + 1)) (q : ℕ) : 1 ≤ q → cells i q ≠ Γ.start

  No other cell is.

• ne_blank (q : ℕ) : 1 ≤ q → q ≤ len → cells 0 q ≠ Γ.blank

  Tape 0 is non-blank throughout its length.

• blank : cells 0 (len + 1) = Γ.blank

  And blank immediately after.

theorem Complexity.TM.twoPassCfg_run_right {j : ℕ} (S : Scanner j) (inp res out : Tape) (cells : Fin (j + 1) → ℕ → Γ) (len : ℕ) (hok : ScanOk inp res out) (ht : ScanTape cells len) (d p : ℕ) : p + d = len → (twoPassTM S).reachesIn d (twoPassCfg S (TwoPassPhase.right, S.runR (scanCol cells) p) inp cells (p + 1) res out) (twoPassCfg S (TwoPassPhase.right, S.runR (scanCol cells) len) inp cells (len + 1) res out)

The rightward pass.

theorem Complexity.TM.twoPassCfg_run_left {j : ℕ} (S : Scanner j) (inp res out : Tape) (cells : Fin (j + 1) → ℕ → Γ) (len : ℕ) (hok : ScanOk inp res out) (ht : ScanTape cells len) (h : ℕ) (s : S.σ) : (twoPassTM S).reachesIn h (twoPassCfg S (TwoPassPhase.left, s) inp cells h res out) (twoPassCfg S (TwoPassPhase.left, S.runL (scanCol cells) h s) inp cells 0 res out)

The leftward pass.

theorem Complexity.TM.twoPassCfg_run {j : ℕ} (S : Scanner j) (inp res out : Tape) (cells : Fin (j + 1) → ℕ → Γ) (len : ℕ) (hok : ScanOk inp res out) (ht : ScanTape cells len) : (twoPassTM S).reachesIn (2 * len + 3) (twoPassCfg S (twoPassTM S).qstart inp cells 1 res out) (twoPassCfg S (TwoPassPhase.done, S.start) inp cells 1 (res.write (Γ.ofBool (S.emit (S.run (scanCol cells) len)))) out)

A whole scan. Started with every scanned head on cell one, the machine walks tape 0 to its first blank and back, and halts with the automaton's verdict written on the result tape. Nothing else on any tape moves.

theorem Complexity.TM.twoPassCfg_halted {j : ℕ} (S : Scanner j) (inp : Tape) (cells : Fin (j + 1) → ℕ → Γ) (h : ℕ) (res out : Tape) : (twoPassTM S).halted (twoPassCfg S (TwoPassPhase.done, S.start) inp cells h res out)

A scan ends halted.

theorem Complexity.TM.twoPassTM_hoareTime {j : ℕ} (S : Scanner j) (cells : Fin (j + 1) → ℕ → Γ) (len : ℕ) (inp₀ out₀ res₀ : Tape) (hok : ScanOk inp₀ res₀ out₀) (ht : ScanTape cells len) : (twoPassTM S).HoareTime (fun (inp : Tape) (work : Fin (j + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = Fin.snoc (fun (i : Fin (j + 1)) => { head := 1, cells := cells i }) res₀) (fun (inp : Tape) (work : Fin (j + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = Fin.snoc (fun (i : Fin (j + 1)) => { head := 1, cells := cells i }) (res₀.write (Γ.ofBool (S.emit (S.run (scanCol cells) len))))) (2 * len + 3)

The scan as a Hoare triple, which is the form TM.seqTM and TM.loopTM compose.

def Complexity.TM.checkTM {jd jj : ℕ} (S : Scanner jd) (f : Fin (jd + 1) → Fin (jj + 1)) : TM (jj + 2)

A check on the whole register set. The scanner names the columns it reads, so a check needs neither its registers moved next to one another nor a private copy of them.

Equations

• Complexity.TM.checkTM S f = Complexity.TM.twoPassTM (S.comap f)

theorem Complexity.TM.checkTM_hoareTime {jd jj : ℕ} (S : Scanner jd) (f : Fin (jd + 1) → Fin (jj + 1)) (cells : Fin (jj + 1) → ℕ → Γ) (len : ℕ) (inp₀ out₀ res₀ : Tape) (hok : ScanOk inp₀ res₀ out₀) (ht : ScanTape cells len) : (checkTM S f).HoareTime (fun (inp : Tape) (work : Fin (jj + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = Fin.snoc (fun (i : Fin (jj + 1)) => { head := 1, cells := cells i }) res₀) (fun (inp : Tape) (work : Fin (jj + 2) → Tape) (out : Tape) => inp = inp₀ ∧ out = out₀ ∧ work = Fin.snoc (fun (i : Fin (jj + 1)) => { head := 1, cells := cells i }) (res₀.write (Γ.ofBool (S.emit (S.run (fun (q : ℕ) (i : Fin (jd + 1)) => cells (f i) q) len))))) (2 * len + 3)

Its contract: the verdict of the scanner, read off the named columns.