Deterministic prefixes of nondeterministic traces

Many NTM constructions (guess-and-verify, deterministic preprocessing before a nondeterministic phase) run through a deterministic prefix: an initial segment of the computation on which the two transition branches agree. On that segment the trace is independent of the choice bits and follows an ordinary DTM run.

The stepping stone is TM.ReachesInVia, a run whose step sources are annotated with a predicate. Annotating sources rather than imposing a step-closed invariant matters: the last prefix step typically exits the agreeing region (entering the nondeterministic phase), so no step-closed predicate can describe the prefix. Phase wraps produce annotated runs via TM.reachesInVia_of_stepCommute, and annotated runs concatenate with TM.ReachesInVia.trans.

Main results:

• NTM.det — project an NTM onto the DTM that always follows branch b.
• NTM.BranchesAgreeAt, NTM.det_step_congr — pointwise branch agreement, under which the projections take the same step.
• NTM.trace_succ_det — one non-halted trace step is one step of the det-projection selected by the current choice bit.
• NTM.trace_of_det_prefix — the workhorse: a det false run of t steps whose sources all satisfy BranchesAgreeAt lets any length-(s + t) trace restart from the run's endpoint with the first t choices discarded.

inductive Complexity.TM.ReachesInVia {n : ℕ} (tm : TM n) (A : Cfg n tm.Q → Prop) : ℕ → Cfg n tm.Q → Cfg n tm.Q → Prop

A DTM run of t steps from c to c' all of whose step sources satisfy A. Unlike a step-closed invariant, this can describe a run whose final step leaves the region described by A.

• zero {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {c : Cfg n tm.Q} : tm.ReachesInVia A 0 c c
• step {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {c c'' : Cfg n tm.Q} {t : ℕ} {c' : Cfg n tm.Q} : A c → tm.step c = some c'' → tm.ReachesInVia A t c'' c' → tm.ReachesInVia A (t + 1) c c'

theorem Complexity.TM.reachesInVia_zero_iff {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {c c' : Cfg n tm.Q} : tm.ReachesInVia A 0 c c' ↔ c = c'

A zero-step annotated run goes nowhere. Inversion form of ReachesInVia.zero, usable when the machine is a compound expression on which cases cannot abstract the configuration indices.

theorem Complexity.TM.reachesInVia_succ_iff {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {t : ℕ} {c c' : Cfg n tm.Q} : tm.ReachesInVia A (t + 1) c c' ↔ A c ∧ ∃ (c'' : Cfg n tm.Q), tm.step c = some c'' ∧ tm.ReachesInVia A t c'' c'

An annotated run of t + 1 steps factors as one step from an A-source followed by an annotated run of t steps. Inversion form of ReachesInVia.step.

theorem Complexity.TM.ReachesInVia.toReachesIn {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {t : ℕ} {c c' : Cfg n tm.Q} (h : tm.ReachesInVia A t c c') : tm.reachesIn t c c'

Forget the source annotations of an annotated run.

theorem Complexity.TM.ReachesInVia.mono {n : ℕ} {tm : TM n} {A B : Cfg n tm.Q → Prop} {t : ℕ} {c c' : Cfg n tm.Q} (hAB : ∀ (c : Cfg n tm.Q), A c → B c) (h : tm.ReachesInVia A t c c') : tm.ReachesInVia B t c c'

Weaken the source annotation of an annotated run.

theorem Complexity.TM.ReachesInVia.trans {n : ℕ} {tm : TM n} {A : Cfg n tm.Q → Prop} {t u : ℕ} {c c' c'' : Cfg n tm.Q} (h₁ : tm.ReachesInVia A t c c') (h₂ : tm.ReachesInVia A u c' c'') : tm.ReachesInVia A (t + u) c c''

Concatenate annotated runs.

theorem Complexity.TM.reachesInVia_of_invariant {n : ℕ} {tm : TM n} {P A : Cfg n tm.Q → Prop} (hPA : ∀ (c : Cfg n tm.Q), P c → A c) (hpres : ∀ {c c' : Cfg n tm.Q}, P c → tm.step c = some c' → P c') {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') (hP : P c) : tm.ReachesInVia A t c c'

Annotate a run with a step-closed invariant that implies the annotation.

theorem Complexity.TM.reachesInVia_of_stepCommute {n m : ℕ} {tm₁ : TM n} {tm₂ : TM m} {A : Cfg m tm₂.Q → Prop} (w : Cfg n tm₁.Q → Cfg m tm₂.Q) (hA : ∀ {c c' : Cfg n tm₁.Q}, tm₁.step c = some c' → A (w c)) (hcomm : ∀ {c c' : Cfg n tm₁.Q}, tm₁.step c = some c' → tm₂.step (w c) = some (w c')) {t : ℕ} {c c' : Cfg n tm₁.Q} (hreach : tm₁.reachesIn t c c') : tm₂.ReachesInVia A t (w c) (w c')

Transport a run through a step-commuting wrap w, annotating every source with membership in the image region described by A. This is how phase embeddings (whose sources all live inside one phase of a composed machine) produce annotated runs.

def Complexity.NTM.det {n : ℕ} (N : NTM n) (b : Bool) : TM n

Project an NTM onto the deterministic machine that always follows branch b. The projection shares the NTM's state space, so its configurations coincide with the NTM's.

Equations

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

def Complexity.NTM.BranchesAgreeAt {n : ℕ} (N : NTM n) (c : Cfg n N.Q) : Prop

The two transition branches of N agree at configuration c (on the symbols actually under the heads). This is the pointwise hypothesis under which a trace step is choice-independent.

Equations

• N.BranchesAgreeAt c = (N.δ true c.state c.input.read (fun (i : Fin n) => (c.work i).read) c.output.read = N.δ false c.state c.input.read (fun (i : Fin n) => (c.work i).read) c.output.read)

theorem Complexity.NTM.det_step_congr {n : ℕ} {N : NTM n} {c : Cfg n N.Q} (h : N.BranchesAgreeAt c) (b : Bool) : (N.det b).step c = (N.det false).step c

On a configuration where the branches agree, every det-projection takes the same step as det false.

theorem Complexity.NTM.trace_succ_det {n : ℕ} {N : NTM n} {c : Cfg n N.Q} {T : ℕ} (choices : Fin (T + 1) → Bool) (hne : c.state ≠ N.qhalt) : N.trace (T + 1) choices c = N.trace T (fun (i : Fin T) => choices ⟨↑i + 1, ⋯⟩) (((N.det (choices ⟨0, ⋯⟩)).step c).get ⋯)

One non-halted trace step applies the det-projection selected by the current choice bit.

theorem Complexity.NTM.trace_of_det_prefix {n : ℕ} {N : NTM n} {t : ℕ} {c c' : Cfg n N.Q} (hreach : (N.det false).ReachesInVia N.BranchesAgreeAt t c c') (s : ℕ) (choices : Fin (s + t) → Bool) : N.trace (s + t) choices c = N.trace s (fun (i : Fin s) => choices ⟨↑i + t, ⋯⟩) c'

Deterministic-prefix transport. A det false run of t steps whose sources all satisfy BranchesAgreeAt is followed identically by the trace along any choice sequence: a length-(s + t) trace equals the trace of the remaining s steps from the run's endpoint with the first t choices discarded.