Running one nondeterministic path deterministically

An NTM's transition function has exactly the shape of a TM's, plus a Bool. Feeding that Bool from a dedicated work tape — one cell per step, scanned left to right and written back unchanged — turns the nondeterministic machine into a deterministic one whose run is the chosen path.

This is the primitive that lets deterministic machines reason about nondeterministic runs: a decider that must evaluate "does tm accept x along choice sequence c" places c on the choice tape and runs choiceTM tm.

Main definitions

• NTM.choiceTM — the deterministic machine with a choice tape appended
• NTM.dropChoice — forget the choice tape from a configuration
• NTM.choiceStream — the choice bits under and to the right of the head

Main results

• NTM.choiceTM_step — one step of choiceTM is one step of the path
• NTM.choiceTM_simulates — a T-step run of choiceTM is tm.trace T along the choice bits found on the tape

def Complexity.TM.stepCfg {k : ℕ} (tm : TM k) (c : Cfg k tm.Q) : Cfg k tm.Q

The configuration update inlined in TM.step.

Equations

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

theorem Complexity.TM.step_of_not_halted {k : ℕ} (tm : TM k) {c : Cfg k tm.Q} (h : c.state ≠ tm.qhalt) : tm.step c = some (tm.stepCfg c)

A non-halted configuration steps to stepCfg.

def Complexity.NTM.choiceTM {k : ℕ} (tm : NTM k) : TM (k + 1)

The deterministic machine that runs one path of tm, reading its choice bits from the appended last work tape: each step consults the cell under that head, writes it back unchanged, and advances the head one cell right.

Equations

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

def Complexity.NTM.stepCfg {k : ℕ} (tm : NTM k) (b : Bool) (c : Cfg k tm.Q) : Cfg k tm.Q

One step of an NTM along a fixed choice bit: the configuration update inlined in NTM.trace.

Equations

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

theorem Complexity.NTM.trace_succ_of_not_halted {k : ℕ} (tm : NTM k) (T : ℕ) (choices : Fin (T + 1) → Bool) {c : Cfg k tm.Q} (h : c.state ≠ tm.qhalt) : tm.trace (T + 1) choices c = tm.trace T (fun (i : Fin T) => choices ⟨↑i + 1, ⋯⟩) (tm.stepCfg (choices ⟨0, ⋯⟩) c)

Unfolding one non-halted step of trace.

def Complexity.NTM.dropChoice {k : ℕ} {Q : Type} (c : Cfg (k + 1) Q) : Cfg k Q

Forget the choice tape from a configuration.

Equations

• Complexity.NTM.dropChoice c = { state := c.state, input := c.input, work := fun (i : Fin k) => c.work i.castSucc, output := c.output }

def Complexity.NTM.choiceStream {k : ℕ} {Q : Type} (c : Cfg (k + 1) Q) (j : ℕ) : Bool

The choice bits under and to the right of the choice head.

Equations

• Complexity.NTM.choiceStream c j = decide ((c.work (Fin.last k)).cells ((c.work (Fin.last k)).head + j) = Complexity.Γ.one)

theorem Complexity.NTM.choiceTM_step {k : ℕ} (tm : NTM k) (c : Cfg (k + 1) tm.Q) (hhalt : c.state ≠ tm.qhalt) (hread : (c.work (Fin.last k)).read ≠ Γ.start) : ∃ (c₁ : Cfg (k + 1) tm.choiceTM.Q), tm.choiceTM.step c = some c₁ ∧ dropChoice c₁ = tm.stepCfg (choiceStream c 0) (dropChoice c) ∧ c₁.work (Fin.last k) = (c.work (Fin.last k)).move Dir3.right

One step of choiceTM is one step of the chosen path. The choice tape is written back unchanged and its head advances one cell.

theorem Complexity.NTM.choiceTM_simulates {k : ℕ} (tm : NTM k) (T : ℕ) (c : Cfg (k + 1) tm.Q) (hinv : (c.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c.work (Fin.last k)).head) : ∃ (c' : Cfg (k + 1) tm.Q), ∃ t ≤ T, tm.choiceTM.reachesIn t c c' ∧ (t < T → tm.choiceTM.halted c') ∧ dropChoice c' = tm.trace T (fun (j : Fin T) => choiceStream c ↑j) (dropChoice c)

A T-step run of choiceTM is the T-step trace of tm along the choice bits on the tape. The run stops early exactly when the path halts; the choice tape is left untouched apart from its head, which advances one cell per step.