Native finite-state compilation of nondeterministic query machines

Local linear-space callbacks compile to native binary-choice passes. The abstract state remains on the work tapes; finite native control stores only callback control states and routing states.

The abstract run may start in a state depending on the input, written by a native initializer computable in the target space; the passes and the finalizer do not depend on the input.

Main results

• Turing.NondeterministicQueryMachine.exists_recognizesInSpace: the native compiler preserves existential acceptance and bounds every computation prefix, with no halting hypothesis.
• Turing.NondeterministicQueryMachine.exists_decidesInSpace: given a common abstract clock, the compiled recognizer also halts on every branch.

@[reducible, inline]

noncomputable abbrev Turing.NondeterministicQueryMachine.Routines.machine {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) : MultiTapeNTM R.k Bool (Native.State R.SI R.SP R.SF)

The compiled native nondeterministic machine.

def Turing.NondeterministicQueryMachine.Routines.Inv {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) (ws : Fin R.k → List Bool) : Prop

The boundary invariant includes both possible continuation flags. Only the post-pass flag is used to choose whether to continue. Initialization enters the first pass unconditionally.

theorem Turing.NondeterministicQueryMachine.Routines.runsInSpace {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) : R.machine.RunsInSpace (enc a) (R.k * (2 * (R.c * S a) + 1))

All native prefixes remain in the shared workspace window.

noncomputable def Turing.NondeterministicQueryMachine.Routines.boundaryState {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (ws : Fin R.k → List Bool) : σ

Decode a boundary state for proof purposes only. It is never stored in finite control.

theorem Turing.NondeterministicQueryMachine.Routines.exists_runsInTime {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) {time : ℕ} (hhalt : (M.withInit (start a)).HaltsWithin (enc a) time) : ∃ (t : ℕ), R.machine.RunsInTime (enc a) t

A common abstract clock yields an all-branches native clock, without an encoded clock.

theorem Turing.NondeterministicQueryMachine.Routines.choose_output {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) (p : R.machine.RunPath (enc a)) (s : σ) (hs : (M.withInit (start a)).Reachable (enc a) s) (flag : Bool) (out : List Bool) (hhead : RelSeries.head p = wordsCfg (enc a) (some Native.State.choose) (R.boundary s flag) out) (hhalt : (RelSeries.last p).Halted) : ∃ (s' : σ), (M.withInit (start a)).Reachable (enc a) s' ∧ M.halted s' = true ∧ (RelSeries.last p).output = out ++ [M.accept s']

Reverse simulation of every halted native branch, including arbitrary native prefixes within routines. Passes do not emit; the final bit belongs to a reachable halted abstract state.

theorem Turing.NondeterministicQueryMachine.Routines.choose_realizes {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) (choices : List Bool) (s : σ) (hs : (M.withInit (start a)).Reachable (enc a) s) (hh : M.halted (M.replay (enc a) choices s) = true) (flag : Bool) (out : List Bool) : ∃ (p : R.machine.RunPath (enc a)), RelSeries.head p = wordsCfg (enc a) (some Native.State.choose) (R.boundary s flag) out ∧ (RelSeries.last p).Halted ∧ (RelSeries.last p).output = out ++ [M.accept (M.replay (enc a) choices s)]

Every finite abstract branch ending halted is realized by a native branch. The initially halted case uses one harmless self-loop pass, matching the unconditional native first pass.

theorem Turing.NondeterministicQueryMachine.Routines.accepts_iff {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) (a : α) : R.machine.Accepts (enc a) ↔ (M.withInit (start a)).Accepts (enc a)

Native acceptance is exactly existential halted acceptance of the query machine.

theorem Turing.NondeterministicQueryMachine.Routines.recognizesInSpace {α σ : Type} {M : NondeterministicQueryMachine σ} {start : α → σ} {enc : α ↪ List Bool} {S : α → ℕ} (R : M.Routines start enc S) {A : Set α} (hcorrect : ∀ (a : α), a ∈ A ↔ (M.withInit (start a)).Accepts (enc a)) (hS : ∀ (a : α), 1 ≤ S a) : R.machine.RecognizesInSpace enc A fun (a : α) => R.k * (2 * R.c + 1) * S a

The compiled machine recognizes A in O(S) visited-cell space whenever the abstract run on enc a, started in start a, accepts exactly the members of A. No halting is required.

theorem Turing.NondeterministicQueryMachine.exists_recognizesInSpace {α σ : Type} {enc : α ↪ List Bool} {encS : σ ↪ List Bool} (M : NondeterministicQueryMachine σ) (hquery : MultiTapeTM.ComputableInSpace M.query encS MultiTapeTM.encNat fun (s : σ) => (encS s).length) (hnext : MultiTapeTM.ComputableInSpace M.next (MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) encS fun (p : σ × Option Bool × Bool) => ((MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) p).length) (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (haccept : MultiTapeTM.ComputableInSpace M.accept encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (start : α → σ) {A : Set α} (hcorrect : ∀ (a : α), a ∈ A ↔ (M.withInit (start a)).Accepts (enc a)) (S : α → ℕ) (hlog : ∀ (a : α), (enc a).length.log2 + 1 ≤ S a) (hstart : MultiTapeTM.ComputableInSpace start enc encS S) (hsize : ∃ (c : ℕ), ∀ (a : α) (choices : List Bool), (encS ((M.withInit (start a)).run (enc a) choices)).length ≤ c * S a) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State) (c : ℕ), ntm.RecognizesInSpace enc A fun (a : α) => c * S a

Native finite-state compilation of recognizers. Linear-space local callbacks, a start state computable in space O(S), and a uniform bound on all encoded abstract prefixes yield a native nondeterministic recognizer in O(S) visited-cell space. Abstract branches need not halt. Neither an abstract state nor a choice history is stored in native finite control.

theorem Turing.NondeterministicQueryMachine.exists_decidesInSpace {α σ : Type} {enc : α ↪ List Bool} {encS : σ ↪ List Bool} (M : NondeterministicQueryMachine σ) (hquery : MultiTapeTM.ComputableInSpace M.query encS MultiTapeTM.encNat fun (s : σ) => (encS s).length) (hnext : MultiTapeTM.ComputableInSpace M.next (MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) encS fun (p : σ × Option Bool × Bool) => ((MultiTapeTM.encPair encS (MultiTapeTM.encPair (MultiTapeTM.encOption MultiTapeTM.encBool) MultiTapeTM.encBool)) p).length) (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (haccept : MultiTapeTM.ComputableInSpace M.accept encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (start : α → σ) (time : α → ℕ) (hhalt : ∀ (a : α), (M.withInit (start a)).HaltsWithin (enc a) (time a)) {A : Set α} (hcorrect : ∀ (a : α), a ∈ A ↔ (M.withInit (start a)).Accepts (enc a)) (S : α → ℕ) (hlog : ∀ (a : α), (enc a).length.log2 + 1 ≤ S a) (hstart : MultiTapeTM.ComputableInSpace start enc encS S) (hsize : ∃ (c : ℕ), ∀ (a : α) (choices : List Bool), (encS ((M.withInit (start a)).run (enc a) choices)).length ≤ c * S a) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : MultiTapeNTM k Bool State) (c : ℕ), ntm.DecidesInSpace enc A fun (a : α) => c * S a

Native finite-state compilation of deciders. Under the hypotheses of exists_recognizesInSpace, a common abstract clock on every input makes the compiled recognizer halt on every branch. The clock is used only in the proof; it is not stored in native finite control.