Delaying a nondeterministic machine's first choice

A machine begins with every head on ▷, and NTM.δ_right_of_start forces that first transition to move them all right. The transition may nevertheless branch: δ false and δ true can send the machine to different states. That is a nuisance for any construction that has to enter a simulated machine after the compulsory ▷-step — a composed machine can never hand a stage a head at cell zero — because the entry state would then fix the first choice.

NTM.delayNTM removes the branch. It spends one extra step doing nothing but the compulsory move, and only then consults the choice bit, jumping to whichever state the source machine's first transition would have produced. Its first step is therefore choice-independent, while its subsequent behaviour is the source machine's, one step later.

Main results

• NTM.delayNTM — the source machine with its first choice deferred by one step
• NTM.delayNTM_trace_embed — after the delay, the two machines run in lockstep
• NTM.delayNTM_trace_two_initCfg — two steps of the delayed machine reproduce one of the source
• NTM.delayNTM_allPathsHaltIn — the delay costs two steps
• NTM.delayNTM_acceptCount — the delay doubles the count of accepting paths

def Complexity.NTM.delayNTM {n : ℕ} (tm : NTM n) : NTM n

The source machine with its first choice deferred. The extra state Sum.inl () is both the start state and the state the machine sits in after the compulsory ▷-step; the two are distinguished by the input head's symbol, which is ▷ exactly on the first step.

Equations

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

@[simp]

theorem Complexity.NTM.delayNTM_qhalt {n : ℕ} (tm : NTM n) : tm.delayNTM.qhalt = Sum.inr tm.qhalt

@[simp]

theorem Complexity.NTM.delayNTM_qstart {n : ℕ} (tm : NTM n) : tm.delayNTM.qstart = Sum.inl ()

def Complexity.NTM.delayEmbed {n : ℕ} (tm : NTM n) (c : Cfg n tm.Q) : Cfg n tm.delayNTM.Q

A source configuration, viewed as one of the delayed machine's.

Equations

• tm.delayEmbed c = { state := Sum.inr c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.NTM.delayEmbed_halted_iff {n : ℕ} (tm : NTM n) (c : Cfg n tm.Q) : (tm.delayEmbed c).state = tm.delayNTM.qhalt ↔ c.state = tm.qhalt

theorem Complexity.NTM.delayNTM_trace_one_embed {n : ℕ} (tm : NTM n) (b : Bool) (c : Cfg n tm.Q) : tm.delayNTM.trace 1 (fun (x : Fin 1) => b) (tm.delayEmbed c) = tm.delayEmbed (tm.trace 1 (fun (x : Fin 1) => b) c)

One step, transported. On an embedded configuration the delayed machine's transition is literally the source's, wrapped.

theorem Complexity.NTM.delayNTM_trace_embed {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) : tm.delayNTM.trace T choices (tm.delayEmbed c) = tm.delayEmbed (tm.trace T choices c)

After the delay, the two machines run in lockstep. Every trace from an embedded configuration transports to the source machine's.

theorem Complexity.NTM.trace_one_of_heads_zero {n : ℕ} (tm : NTM n) (b : Bool) (c : Cfg n tm.Q) (hne : c.state ≠ tm.qhalt) (hin : c.input.head = 0) (hwork : ∀ (i : Fin n), (c.work i).head = 0) (hout : c.output.head = 0) (hin0 : c.input.cells 0 = Γ.start) (hwork0 : ∀ (i : Fin n), (c.work i).cells 0 = Γ.start) (hout0 : c.output.cells 0 = Γ.start) : tm.trace 1 (fun (x : Fin 1) => b) c = { state := (tm.δ b c.state Γ.start (fun (x : Fin n) => Γ.start) Γ.start).1, input := c.input.move Dir3.right, work := fun (i : Fin n) => (c.work i).move Dir3.right, output := c.output.move Dir3.right }

The sentinel step of a nondeterministic machine. From any configuration whose heads are at cell zero the reads are all ▷, so the writes are no-ops and every head moves right; only the state depends on the choice bit.

theorem Complexity.NTM.delayNTM_trace_one_pending {n : ℕ} (tm : NTM n) (b : Bool) (c : Cfg n tm.delayNTM.Q) (hstate : c.state = Sum.inl ()) (hin : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (hout : c.output.read ≠ Γ.start) : tm.delayNTM.trace 1 (fun (x : Fin 1) => b) c = { state := Sum.inr (tm.δ b tm.qstart Γ.start (fun (x : Fin n) => Γ.start) Γ.start).1, input := c.input, work := c.work, output := c.output }

The delayed machine's second step. Sitting in the extra state with every head off the marker, it consults the choice bit, jumps to the state the source machine's first transition would have produced, and leaves every tape exactly as it is.

theorem Complexity.NTM.delayNTM_trace_two_initCfg {n : ℕ} (tm : NTM n) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) (choices : Fin 2 → Bool) : tm.delayNTM.trace 2 choices (tm.delayNTM.initCfg x) = tm.delayEmbed (tm.trace 1 (fun (x : Fin 1) => choices ⟨1, delayNTM_trace_two_initCfg._proof_2⟩) (tm.initCfg x))

Two steps of the delayed machine reproduce one step of the source. The first step is the compulsory move off the marker and ignores its choice bit; the second consumes the choice the source machine would have made first.

theorem Complexity.NTM.delayNTM_trace_initCfg {n : ℕ} (tm : NTM n) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) (T : ℕ) (ch : Fin (T + 2) → Bool) : tm.delayNTM.trace (T + 2) ch (tm.delayNTM.initCfg x) = tm.delayEmbed (tm.trace (T + 1) (Fin.tail ch) (tm.initCfg x))

A whole run of the delayed machine, from its initial configuration. Two extra steps buy one step of the source machine, and thereafter the two run in lockstep.

theorem Complexity.NTM.delayNTM_allPathsHaltIn {n : ℕ} (tm : NTM n) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (hne : tm.qstart ≠ tm.qhalt) : tm.delayNTM.AllPathsHaltIn fun (m : ℕ) => f m + 2

The delay costs two steps. Every path of the source machine that halts within f |x| steps has its delayed counterpart halted within f |x| + 2.

theorem Complexity.NTM.delayNTM_acceptCount {n : ℕ} (tm : NTM n) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) (T : ℕ) : tm.delayNTM.acceptCount x (T + 2) = 2 * tm.acceptCount x (T + 1)

The delayed machine's accepting paths, counted. Its first choice bit does nothing, so each accepting path of the source machine lifts to exactly two of the delayed machine's.