Fixing a nondeterministic branch

An NTM's transition function is a Bool away from a TM's, so fixing the Bool turns it into a deterministic machine. Unlike NTM.choiceTM, which reads one choice bit per step off a tape and therefore runs a whole path, branchTM fixes the same choice for every step: it is the one-step successor operator of the configuration graph, not a path.

That is what a search of the configuration graph needs. Deterministic machinery — the encoded step Complexity.Cobham.stepFn of Cobham's algebra above all — applies to a TM and not to an NTM, so an edge of the graph is taken by one of the two branchTMs (Complexity.NTM.succ_iff, where the graph is defined).

Main definitions

• NTM.branchTM — the deterministic machine that always takes branch b

Main results

• NTM.branchTM_stepCfg — its step is the branch's step
• NTM.branchTM_step, NTM.branchTM_step_of_halted — the step, halted or not

def Complexity.NTM.branchTM {k : ℕ} (tm : NTM k) (b : Bool) : TM k

The deterministic machine that always takes branch b.

Equations

• tm.branchTM b = { Q := tm.Q, decEq := tm.decEq, finQ := tm.finQ, qstart := tm.qstart, qhalt := tm.qhalt, δ := tm.δ b, δ_right_of_start := ⋯ }

@[simp]

theorem Complexity.NTM.branchTM_Q {k : ℕ} (tm : NTM k) (b : Bool) : (tm.branchTM b).Q = tm.Q

@[simp]

theorem Complexity.NTM.branchTM_qstart {k : ℕ} (tm : NTM k) (b : Bool) : (tm.branchTM b).qstart = tm.qstart

@[simp]

theorem Complexity.NTM.branchTM_qhalt {k : ℕ} (tm : NTM k) (b : Bool) : (tm.branchTM b).qhalt = tm.qhalt

@[simp]

theorem Complexity.NTM.branchTM_δ {k : ℕ} (tm : NTM k) (b : Bool) : (tm.branchTM b).δ = tm.δ b

@[simp]

theorem Complexity.NTM.branchTM_stepCfg {k : ℕ} (tm : NTM k) (b : Bool) (c : Cfg k tm.Q) : (tm.branchTM b).stepCfg c = tm.stepCfg b c

One step of the fixed branch is one step of the nondeterministic machine on that branch.

theorem Complexity.NTM.branchTM_step {k : ℕ} (tm : NTM k) (b : Bool) {c : Cfg k tm.Q} (h : c.state ≠ tm.qhalt) : (tm.branchTM b).step c = some (tm.stepCfg b c)

A non-halted configuration steps to the branch's successor.

theorem Complexity.NTM.branchTM_step_of_halted {k : ℕ} (tm : NTM k) (b : Bool) {c : Cfg k tm.Q} (h : c.state = tm.qhalt) : (tm.branchTM b).step c = none

A halted configuration has no successor on either branch.