Building a nondeterministic machine from a deterministic one

Complexitylib.Models.TuringMachine.ChoiceTape runs one path of a given NTM deterministically. This file goes the other way, which is what a construction needs: it turns a deterministic machine that reads a guess tape into a nondeterministic machine whose choices supply that tape's contents.

The point is leverage. Every subroutine in Complexitylib.Models.TuringMachine.Subroutines is deterministic, and so is every Hoare-style contract proved about them. Assembling an NTM by hand forgoes all of it. Assembling a TM that consults one extra tape for its guesses, and then applying NTM.ofGuess, keeps the whole toolkit and confines the nondeterminism to a single tape read.

Conventions

The guess tape is the last work tape, matching NTM.choiceTM. A machine that uses it as a guess tape must, at every step, write the cell back unchanged and move that head one cell right — that is TM.GuessDiscipline. The discipline is what makes the guesses independent: the machine consumes exactly one fresh bit per step and can never revisit one.

Main definitions

• NTM.ofGuess — the nondeterministic machine a guess-reading deterministic machine denotes
• TM.GuessDiscipline — write the guess cell back, advance its head
• Tape.BoolFrom — the guess tape holds Boolean symbols for the next T cells

Main results

• NTM.choiceTM_ofGuess_δ — the round trip is the identity on transitions
• NTM.step_ofGuess — and on steps, wherever the guess cell holds a bit
• NTM.reachesIn_ofGuess_iff — and on runs
• NTM.ofGuess_simulates — a T-step run of M on a loaded guess tape is a trace of NTM.ofGuess M along the bits loaded onto it

def Complexity.Tape.BoolFrom (t : Tape) (T : ℕ) : Prop

The next T cells from the head hold Boolean symbols.

Equations

• t.BoolFrom T = ∀ j < T, ∃ (b : Bool), t.cells (t.head + j) = Complexity.Γ.ofBool b

theorem Complexity.Tape.BoolFrom.read {t : Tape} {T : ℕ} (h : t.BoolFrom (T + 1)) : ∃ (b : Bool), t.read = Γ.ofBool b

theorem Complexity.Tape.BoolFrom.read_ne_start {t : Tape} {T : ℕ} (h : t.BoolFrom (T + 1)) : t.read ≠ Γ.start

theorem Complexity.Tape.BoolFrom.move_right {t : Tape} {T : ℕ} (h : t.BoolFrom (T + 1)) : (t.move Dir3.right).BoolFrom T

theorem Complexity.Tape.BoolFrom.mono {t : Tape} {T T' : ℕ} (h : t.BoolFrom T) (hle : T' ≤ T) : t.BoolFrom T'

structure Complexity.TM.GuessDiscipline {k : ℕ} (M : TM (k + 1)) : Prop

The guess-tape discipline. At every transition the machine writes the last work tape's cell back unchanged and advances that head one cell right, so it consumes exactly one fresh guess per step and never revisits one.

• write (q : M.Q) (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 written back unchanged.

• dir (q : M.Q) (iHead : Γ) (wHeads : Fin (k + 1) → Γ) (oHead : Γ) : (M.δ q iHead wHeads oHead).2.2.2.2.1 (Fin.last k) = Dir3.right

  The guess head advances one cell right.

def Complexity.NTM.ofGuess {k : ℕ} (M : TM (k + 1)) : NTM k

The nondeterministic machine a guess-reading deterministic machine denotes. The choice bit is fed to M as the symbol under the last work head, and that tape disappears.

Equations

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

@[simp]

theorem Complexity.NTM.ofGuess_Q {k : ℕ} (M : TM (k + 1)) : (ofGuess M).Q = M.Q

@[simp]

theorem Complexity.NTM.ofGuess_qhalt {k : ℕ} (M : TM (k + 1)) : (ofGuess M).qhalt = M.qhalt

@[simp]

theorem Complexity.NTM.ofGuess_qstart {k : ℕ} (M : TM (k + 1)) : (ofGuess M).qstart = M.qstart

theorem Complexity.NTM.choiceTM_ofGuess_δ {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) (q : M.Q) (iHead : Γ) (wHeads : Fin (k + 1) → Γ) (oHead : Γ) (b : Bool) (hb : wHeads (Fin.last k) = Γ.ofBool b) : (ofGuess M).choiceTM.δ q iHead wHeads oHead = M.δ q iHead wHeads oHead

The round trip is the identity on transitions. Reattaching the guess tape to NTM.ofGuess M recovers M, wherever the guess cell holds a bit.

theorem Complexity.NTM.step_ofGuess {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) {c : Cfg (k + 1) M.Q} (hb : ∃ (b : Bool), (c.work (Fin.last k)).read = Γ.ofBool b) : (ofGuess M).choiceTM.step c = M.step c

The round trip is the identity on steps, wherever the guess cell holds a bit.

theorem Complexity.NTM.work_last_stepCfg {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) (c : Cfg (k + 1) M.Q) (hread : (c.work (Fin.last k)).read ≠ Γ.start) : (M.stepCfg c).work (Fin.last k) = (c.work (Fin.last k)).move Dir3.right

A step leaves the guess tape alone and advances its head.

theorem Complexity.NTM.reachesIn_ofGuess_iff {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) (t : ℕ) (c c' : Cfg (k + 1) M.Q) : (c.work (Fin.last k)).BoolFrom t → ((ofGuess M).choiceTM.reachesIn t c c' ↔ M.reachesIn t c c')

The round trip is the identity on runs, as long as the guess tape holds bits for as many cells as the run has steps.

theorem Complexity.NTM.ofGuess_simulates {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) (T : ℕ) (c : Cfg (k + 1) M.Q) (hinv : (c.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c.work (Fin.last k)).head) (hbool : (c.work (Fin.last k)).BoolFrom T) : ∃ (c' : Cfg (k + 1) M.Q), ∃ t ≤ T, M.reachesIn t c c' ∧ (t < T → M.halted c') ∧ dropChoice c' = (ofGuess M).trace T (fun (j : Fin T) => choiceStream c ↑j) (dropChoice c)

A run of M on a loaded guess tape is a trace of NTM.ofGuess M. This is the transfer that lets a nondeterministic construction be carried out deterministically: build M, prove whatever is wanted of its runs with the deterministic toolkit, and read it off here as a statement about the paths of NTM.ofGuess M.

theorem Complexity.NTM.choiceStream_of_loaded {k : ℕ} {Q : Type} {c : Cfg (k + 1) Q} {g : ℕ → Bool} {T : ℕ} (h : ∀ j < T, (c.work (Fin.last k)).cells ((c.work (Fin.last k)).head + j) = Γ.ofBool (g j)) {j : ℕ} (hj : j < T) : choiceStream c j = g j

Reading back a loaded guess tape. A tape whose cells from the head onward spell g presents exactly g as its choice stream.

Loading a guess tape

def Complexity.NTM.loadTape (g : ℕ → Bool) : Tape

The guess tape carrying g: cell j + 1 holds g j, and the head starts on cell 1.

Equations

• Complexity.NTM.loadTape g = { head := 1, cells := fun (j : ℕ) => if j = 0 then Complexity.Γ.start else Complexity.Γ.ofBool (g (j - 1)) }

@[simp]

theorem Complexity.NTM.loadTape_head (g : ℕ → Bool) : (loadTape g).head = 1

theorem Complexity.NTM.loadTape_cells_succ (g : ℕ → Bool) (j : ℕ) : (loadTape g).cells (j + 1) = Γ.ofBool (g j)

theorem Complexity.NTM.loadTape_startInvariant (g : ℕ → Bool) : (loadTape g).StartInvariant

theorem Complexity.NTM.loadTape_boolFrom (g : ℕ → Bool) (T : ℕ) : (loadTape g).BoolFrom T

def Complexity.NTM.loadCfg {k : ℕ} (M : TM (k + 1)) (x : List Bool) (g : ℕ → Bool) : Cfg (k + 1) M.Q

The starting configuration of the deterministic machine: the input in place, every work tape blank except the last, which carries the guesses.

Equations

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

@[simp]

theorem Complexity.NTM.loadCfg_work_last {k : ℕ} (M : TM (k + 1)) (x : List Bool) (g : ℕ → Bool) : (loadCfg M x g).work (Fin.last k) = loadTape g

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

theorem Complexity.NTM.ofGuess_trace {k : ℕ} (M : TM (k + 1)) (hM : M.GuessDiscipline) (x : List Bool) (T : ℕ) (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 (fun (j : Fin T) => g ↑j) ((ofGuess M).initCfg x)

The paths of NTM.ofGuess M are the runs of M on a loaded guess tape. This is the form a construction uses: design M so that its run on guess string g does what the path along g should do, and this reads that back as a statement about NTM.ofGuess M.