Guessing in designated states

Complexitylib.Models.TuringMachine.GuessTape pairs NTM.ofGuess M with NTM.choiceTM, which forces M to consume a guess at every step. No machine assembled from Complexitylib.Models.TuringMachine.Combinators does that: the handoff step of TM.seqTM, and every step of a subroutine that has no interest in the guesses, leaves the tape's head where it is. This file drops that requirement.

A machine here nominates a set of advancing states. In an advancing state it consumes the cell under the guess head and moves that head on; in every other state it neither consults the guess tape nor moves its head. Between the two lies the whole deterministic subroutine library, usable unchanged.

The price is that the guess tape's head and the step counter part company: at step i the head sits at the cursor, the number of advancing steps so far. NTM.ofGuess M still consumes one choice per step, so the correspondence between a loaded tape and a choice sequence is no longer the identity — it is the cursor. NTM.exists_guessTape is what makes it work in the direction a soundness proof needs: every choice sequence is realized by some loaded tape, because the choices made at non-advancing steps are the ones the machine never looks at.

Main definitions

• TM.traceD — run a deterministic machine for a fixed number of steps, halting in place
• TM.GuessProtocol — advance and consume in the nominated states, hold elsewhere
• NTM.guessBit — the bit the machine reads at a given step

Main results

• NTM.dropChoice_stepCfg — one step of M is one step of NTM.ofGuess M along the bit read
• NTM.dropChoice_traceD — and a run is a trace along the bits read
• TM.traceD_of_reachesIn, TM.traceD_add, TM.traceD_of_reachesIn_halted — a run of a fixed length is the deterministic trace, traces compose, and a halted trace stays put
• NTM.exists_guessTape — every choice sequence comes from a loaded guess tape

def Complexity.TM.traceD {n : ℕ} (M : TM n) : ℕ → Cfg n M.Q → Cfg n M.Q

Run a deterministic machine for T steps, staying put once halted. The deterministic counterpart of NTM.trace.

Equations

• M.traceD 0 x✝ = x✝
• M.traceD T.succ x✝ = if x✝.state = M.qhalt then x✝ else M.traceD T (M.stepCfg x✝)

@[simp]

theorem Complexity.TM.traceD_zero {n : ℕ} (M : TM n) (c : Cfg n M.Q) : M.traceD 0 c = c

theorem Complexity.TM.traceD_succ_of_not_halted {n : ℕ} (M : TM n) (T : ℕ) {c : Cfg n M.Q} (h : c.state ≠ M.qhalt) : M.traceD (T + 1) c = M.traceD T (M.stepCfg c)

theorem Complexity.TM.traceD_of_halted {n : ℕ} (M : TM n) (T : ℕ) {c : Cfg n M.Q} (h : c.state = M.qhalt) : M.traceD T c = c

theorem Complexity.TM.traceD_succ_back {n : ℕ} (M : TM n) (T : ℕ) (c : Cfg n M.Q) : M.traceD (T + 1) c = if (M.traceD T c).state = M.qhalt then M.traceD T c else M.stepCfg (M.traceD T c)

A run of T + 1 steps is a run of T steps followed by one more.

theorem Complexity.TM.reachesIn_traceD {n : ℕ} (M : TM n) (T : ℕ) (c : Cfg n M.Q) : ∃ t ≤ T, M.reachesIn t c (M.traceD T c) ∧ (t < T → M.halted (M.traceD T c))

A fixed-length run is a reachesIn run, stopped early exactly when the machine halts.

def Complexity.TM.visible {k : ℕ} {Q : Type} (r : Q × (Fin (k + 1) → Γw) × Γw × Dir3 × (Fin (k + 1) → Dir3) × Dir3) : Q × (Fin k → Γw) × Γw × Dir3 × (Fin k → Dir3) × Dir3

The part of a transition that survives forgetting the guess tape.

Equations

• Complexity.TM.visible r = (r.1, fun (j : Fin k) => r.2.1 j.castSucc, r.2.2.1, r.2.2.2.1, fun (j : Fin k) => r.2.2.2.2.1 j.castSucc, r.2.2.2.2.2)

structure Complexity.TM.GuessProtocol {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) : Prop

The guess protocol. In an advancing state the machine consumes the cell under the guess head and moves that head on; in every other state it holds the head still and nothing visible depends on what the cell holds. The guess tape's contents are never altered.

• write (q : M.Q) : q ≠ M.qhalt → ∀ (iHead : Γ) (wHeads : Fin (k + 1) → Γ) (oHead : Γ), (M.δ q iHead wHeads oHead).2.1 (Fin.last k) = readBackWrite (wHeads (Fin.last k))

  The guess cell is always written back unchanged.

• dir (q : M.Q) : q ≠ M.qhalt → ∀ (iHead : Γ) (wHeads : Fin (k + 1) → Γ) (oHead : Γ), wHeads (Fin.last k) ≠ Γ.start → (M.δ q iHead wHeads oHead).2.2.2.2.1 (Fin.last k) = if Adv q = true then Dir3.right else Dir3.stay

  The guess head advances in advancing states and holds still elsewhere.

• indep (q : M.Q) : q ≠ M.qhalt → ¬Adv q = true → ∀ (iHead : Γ) (ww : Fin k → Γ) (oHead g g' : Γ), visible (M.δ q iHead (Fin.snoc ww g) oHead) = visible (M.δ q iHead (Fin.snoc ww g') oHead)

  Outside the advancing states the guess is not consulted.

theorem Complexity.TM.traceD_of_reachesIn {n : ℕ} (M : TM n) (t : ℕ) {c c' : Cfg n M.Q} : M.reachesIn t c c' → M.traceD t c = c'

A run of a fixed length is the deterministic trace. A machine's step is a function, so the configuration reached in exactly t steps is TM.traceD t.

theorem Complexity.TM.traceD_add {n : ℕ} (M : TM n) (a b : ℕ) (c : Cfg n M.Q) : M.traceD (a + b) c = M.traceD b (M.traceD a c)

Traces compose.

theorem Complexity.TM.traceD_of_reachesIn_halted {n : ℕ} (M : TM n) {t T : ℕ} (hle : t ≤ T) {c c' : Cfg n M.Q} (h : M.reachesIn t c c') (hhalt : M.halted c') : M.traceD T c = c'

Once halted, a longer trace stays put.

theorem Complexity.NTM.ofGuess_δ {k : ℕ} (M : TM (k + 1)) (b : Bool) (q : M.Q) (iHead : Γ) (ww : Fin k → Γ) (oHead : Γ) : (ofGuess M).δ b q iHead ww oHead = TM.visible (M.δ q iHead (Fin.snoc ww (Γ.ofBool b)) oHead)

The transition of NTM.ofGuess M is the visible part of M's.

theorem Complexity.NTM.dropChoice_stepCfg {k : ℕ} (M : TM (k + 1)) {c : Cfg (k + 1) M.Q} {b : Bool} (hread : (c.work (Fin.last k)).read = Γ.ofBool b) : dropChoice (M.stepCfg c) = (ofGuess M).stepCfg b (dropChoice c)

One step of M is one step of NTM.ofGuess M along the bit under the guess head.

def Complexity.NTM.nrunAt {k : ℕ} (N : NTM k) (choices : ℕ → Bool) (c : Cfg k N.Q) : ℕ → Cfg k N.Q

Run a nondeterministic machine forward, taking the i-th choice at step i. Unlike NTM.trace, which consumes its choices from the front, this indexes them absolutely, which is what a statement about "the step at which a guess was consumed" needs.

Equations

• N.nrunAt choices c 0 = c
• N.nrunAt choices c i.succ = if (N.nrunAt choices c i).state = N.qhalt then N.nrunAt choices c i else N.stepCfg (choices i) (N.nrunAt choices c i)

@[simp]

theorem Complexity.NTM.nrunAt_zero {k : ℕ} (N : NTM k) (choices : ℕ → Bool) (c : Cfg k N.Q) : N.nrunAt choices c 0 = c

theorem Complexity.NTM.nrunAt_succ {k : ℕ} (N : NTM k) (choices : ℕ → Bool) (c : Cfg k N.Q) (i : ℕ) : N.nrunAt choices c (i + 1) = if (N.nrunAt choices c i).state = N.qhalt then N.nrunAt choices c i else N.stepCfg (choices i) (N.nrunAt choices c i)

theorem Complexity.NTM.nrunAt_of_halted {k : ℕ} (N : NTM k) (choices : ℕ → Bool) {c : Cfg k N.Q} (h : c.state = N.qhalt) (i : ℕ) : N.nrunAt choices c i = c

theorem Complexity.NTM.nrunAt_succ_front {k : ℕ} (N : NTM k) (choices : ℕ → Bool) {c : Cfg k N.Q} (h : c.state ≠ N.qhalt) (i : ℕ) : N.nrunAt choices c (i + 1) = N.nrunAt (fun (j : ℕ) => choices (j + 1)) (N.stepCfg (choices 0) c) i

theorem Complexity.NTM.trace_eq_nrunAt {k : ℕ} (N : NTM k) (choices : ℕ → Bool) (T : ℕ) (c : Cfg k N.Q) : N.trace T (fun (i : Fin T) => choices ↑i) c = N.nrunAt choices c T

The absolutely-indexed run is NTM.trace.

def Complexity.NTM.guessBit {k : ℕ} (M : TM (k + 1)) (c : Cfg (k + 1) M.Q) (i : ℕ) : Bool

The bit the machine reads off its guess tape at step i.

Equations

• Complexity.NTM.guessBit M c i = decide (((M.traceD i c).work (Fin.last k)).read = Complexity.Γ.one)

theorem Complexity.NTM.boolFrom_stepCfg {k : ℕ} (M : TM (k + 1)) {Adv : M.Q → Bool} (hP : M.GuessProtocol Adv) {T : ℕ} {c : Cfg (k + 1) M.Q} (hq : c.state ≠ M.qhalt) (h : (c.work (Fin.last k)).BoolFrom (T + 1)) : ((M.stepCfg c).work (Fin.last k)).BoolFrom T

A step preserves the guess tape and moves its head at most one cell right, so a tape holding bits for T + 1 cells still holds them for T.

theorem Complexity.NTM.dropChoice_traceD {k : ℕ} (M : TM (k + 1)) {Adv : M.Q → Bool} (hP : M.GuessProtocol Adv) (T : ℕ) (c : Cfg (k + 1) M.Q) : (c.work (Fin.last k)).BoolFrom T → dropChoice (M.traceD T c) = (ofGuess M).trace T (fun (i : Fin T) => guessBit M c ↑i) (dropChoice c)

A run of M is a trace of NTM.ofGuess M along the bits it reads.

Every choice sequence comes from a loaded tape

theorem Complexity.NTM.stepCfg_indep {k : ℕ} (M : TM (k + 1)) {Adv : M.Q → Bool} (hP : M.GuessProtocol Adv) {c : Cfg k M.Q} (hq : c.state ≠ M.qhalt) (h : ¬Adv c.state = true) (b b' : Bool) : (ofGuess M).stepCfg b c = (ofGuess M).stepCfg b' c

Outside the advancing states the choice bit does not matter.

def Complexity.NTM.attach {k : ℕ} {Q : Type} (d : Cfg k Q) (τ : Tape) : Cfg (k + 1) Q

Attach a guess tape to a configuration.

Equations

• Complexity.NTM.attach d τ = { state := d.state, input := d.input, work := Fin.snoc d.work τ, output := d.output }

@[simp]

theorem Complexity.NTM.attach_work_last {k : ℕ} {Q : Type} (d : Cfg k Q) (τ : Tape) : (attach d τ).work (Fin.last k) = τ

@[simp]

theorem Complexity.NTM.dropChoice_attach {k : ℕ} {Q : Type} (d : Cfg k Q) (τ : Tape) : dropChoice (attach d τ) = d

@[simp]

theorem Complexity.NTM.attach_state {k : ℕ} {Q : Type} (d : Cfg k Q) (τ : Tape) : (attach d τ).state = d.state

theorem Complexity.NTM.loadCfg_eq_attach {k : ℕ} (M : TM (k + 1)) (x : List Bool) (g : ℕ → Bool) : loadCfg M x g = attach ((ofGuess M).initCfg x) (loadTape g)

def Complexity.NTM.searchIdx (P : ℕ → Bool) : ℕ → ℕ

The largest index below T at which P holds, or 0 if there is none.

Equations

• Complexity.NTM.searchIdx P 0 = 0
• Complexity.NTM.searchIdx P i.succ = if P i = true then i else Complexity.NTM.searchIdx P i

theorem Complexity.NTM.searchIdx_eq {P : ℕ → Bool} {T i : ℕ} (hi : i < T) (hP : P i = true) (huniq : ∀ (j : ℕ), P j = true → j = i) : searchIdx P T = i

def Complexity.NTM.consumes {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) (i : ℕ) : Bool

Whether the nondeterministic run consumes a guess at step i.

Equations

• Complexity.NTM.consumes M Adv choices d i = (!decide (((Complexity.NTM.ofGuess M).nrunAt choices d i).state = M.qhalt) && Adv ((Complexity.NTM.ofGuess M).nrunAt choices d i).state)

def Complexity.NTM.cursor {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) : ℕ → ℕ

Where the guess head sits after i steps: one cell on for every guess consumed.

Equations

• Complexity.NTM.cursor M Adv choices d 0 = 1
• Complexity.NTM.cursor M Adv choices d i.succ = Complexity.NTM.cursor M Adv choices d i + if Complexity.NTM.consumes M Adv choices d i = true then 1 else 0

theorem Complexity.NTM.one_le_cursor {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) (i : ℕ) : 1 ≤ cursor M Adv choices d i

theorem Complexity.NTM.cursor_le_succ {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) (i : ℕ) : cursor M Adv choices d i ≤ cursor M Adv choices d (i + 1)

theorem Complexity.NTM.cursor_mono {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) {i j : ℕ} : i ≤ j → cursor M Adv choices d i ≤ cursor M Adv choices d j

theorem Complexity.NTM.cursor_lt_of_consumes {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) {i j : ℕ} (hij : i < j) (hi : consumes M Adv choices d i = true) : cursor M Adv choices d i < cursor M Adv choices d j

theorem Complexity.NTM.cursor_inj_of_consumes {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) {i j : ℕ} (hi : consumes M Adv choices d i = true) (hj : consumes M Adv choices d j = true) (h : cursor M Adv choices d i = cursor M Adv choices d j) : i = j

def Complexity.NTM.guessOf {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) (T p : ℕ) : Bool

The guess string that realizes a choice sequence. Cell p + 1 holds the choice made at the step whose cursor is p + 1; cells no advancing step ever reads hold whatever falls out.

Equations

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

theorem Complexity.NTM.guessOf_eq {k : ℕ} (M : TM (k + 1)) (Adv : M.Q → Bool) (choices : ℕ → Bool) (d : Cfg k M.Q) {T i : ℕ} (hi : i < T) (hc : consumes M Adv choices d i = true) : guessOf M Adv choices d T (cursor M Adv choices d i - 1) = choices i

theorem Complexity.NTM.work_last_stepCfg' {k : ℕ} (M : TM (k + 1)) {Adv' : M.Q → Bool} (hP : M.GuessProtocol Adv') (c : Cfg (k + 1) M.Q) (hq : c.state ≠ M.qhalt) (hread : (c.work (Fin.last k)).read ≠ Γ.start) : (M.stepCfg c).work (Fin.last k) = (c.work (Fin.last k)).move (if Adv' c.state = true then Dir3.right else Dir3.stay)

A step moves the guess head on exactly in the advancing states.

theorem Complexity.NTM.traceD_guessOf {k : ℕ} (M : TM (k + 1)) (choices : ℕ → Bool) (d : Cfg k M.Q) {Adv : M.Q → Bool} (hP : M.GuessProtocol Adv) (T i : ℕ) : i ≤ T → dropChoice (M.traceD i (attach d (loadTape (guessOf M Adv choices d T)))) = (ofGuess M).nrunAt choices d i ∧ (M.traceD i (attach d (loadTape (guessOf M Adv choices d T)))).work (Fin.last k) = { head := cursor M Adv choices d i, cells := (loadTape (guessOf M Adv choices d T)).cells }

Every choice sequence is realized by a loaded guess tape. Running M on the tape NTM.guessOf builds reproduces, step for step, the path of NTM.ofGuess M along choices: the guesses land where the advancing steps read them, and the bits the machine never looks at are free.

theorem Complexity.NTM.exists_loadTape {k : ℕ} (M : TM (k + 1)) {Adv : M.Q → Bool} (hP : M.GuessProtocol Adv) (x : List Bool) (T : ℕ) (choices : Fin T → Bool) : ∃ (g : ℕ → Bool) (c' : Cfg (k + 1) M.Q), ∃ t ≤ T, M.reachesIn t (loadCfg M x g) c' ∧ (t < T → M.halted c') ∧ dropChoice c' = (ofGuess M).trace T choices ((ofGuess M).initCfg x)

A path of NTM.ofGuess M is a run of M on a loaded guess tape. This is the transfer a nondeterministic construction is built on: design and verify M deterministically, with its guesses arriving on the last work tape, and read the result off here as a statement about the paths of NTM.ofGuess M. Unlike NTM.ofGuess_trace it asks nothing of M between guesses, so M may be assembled from the ordinary deterministic combinators.