Framed native routines for nondeterministic query machines

The abstract state is framed on a work tape. The initializer writes the start state of the input, which may depend on the input. Each deterministic pass reads the input in place, performs one selected transition, and writes the continuation flag. Only the finalizer emits.

Main definitions

• Turing.NondeterministicQueryMachine.Routines: finite native routines and their specifications.

Main results

• Turing.NondeterministicQueryMachine.exists_routines: constructs the routines from local linear-space computability and a start state computable in space O(S), with one space bound for all reachable boundary states.

structure Turing.NondeterministicQueryMachine.Routines {α σ : Type} (M : NondeterministicQueryMachine σ) (start : α → σ) (enc : α ↪ List Bool) (S : α → ℕ) : Type 1

Concrete finite routines, sharing tape origins and a common linear space budget. On the input enc a the abstract run starts in start a; the passes and the finalizer do not depend on a.

• k : ℕ

  The shared number of work tapes.

• SI : Type

  Finite control of the initialization routine.

• SP : Bool → Type

  Finite control of each binary-choice pass routine.

• SF : Type

  Finite control of the final verdict routine.

• finiteI : Finite self.SI
• finiteP (b : Bool) : Finite (self.SP b)
• finiteF : Finite self.SF
• I : MultiTapeTM self.k Bool self.SI

  The initialization machine.

• P (b : Bool) : MultiTapeTM self.k Bool (self.SP b)

  The pass machine selected by one nondeterministic bit.

• F : MultiTapeTM self.k Bool self.SF

  The machine emitting the final verdict.

• C : Fin self.k

  The tape holding the continuation flag.

• boundary : σ → Bool → Fin self.k → List Bool

  The encoded abstract state and flag at the common tape origins.

• boundary_flag (s : σ) (b : Bool) : self.boundary s b self.C = MultiTapeTM.flagWord b
• boundary_injective (s : σ) (b : Bool) (s' : σ) (b' : Bool) : self.boundary s b = self.boundary s' b' → s = s'
• c : ℕ

  A common coefficient for the routines' space windows.

• initial_spec (a : α) : ∃ (t : ℕ), self.I.TransformsTapes (fun (inp : List Bool) (ws : Fin self.k → List Bool) => inp = enc a ∧ ws = fun (x : Fin self.k) => []) (fun (x : List Bool) (x_1 ws' : Fin self.k → List Bool) (e : List Bool) => ws' = self.boundary (start a) false ∧ e = []) t (self.c * S a)
• pass_spec (a : α) (s : σ) : (M.withInit (start a)).Reachable (enc a) s → ∀ (choice flag : Bool), ∃ (t : ℕ), (self.P choice).TransformsTapes (fun (inp : List Bool) (ws : Fin self.k → List Bool) => inp = enc a ∧ ws = self.boundary s flag) (fun (x : List Bool) (x_1 ws' : Fin self.k → List Bool) (e : List Bool) => ws' = self.boundary (M.step (enc a) s choice) !M.halted (M.step (enc a) s choice) ∧ e = []) t (self.c * S a)
• final_spec (a : α) (s : σ) : (M.withInit (start a)).Reachable (enc a) s → ∀ (flag : Bool), ∃ (t : ℕ), self.F.TransformsTapes (fun (inp : List Bool) (ws : Fin self.k → List Bool) => inp = enc a ∧ ws = self.boundary s flag) (fun (x : List Bool) (x_1 x_2 : Fin self.k → List Bool) (e : List Bool) => e = [M.accept s]) t (self.c * S a)

theorem Turing.NondeterministicQueryMachine.exists_routines {α σ : 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 : α → σ) (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) : Nonempty (M.Routines start enc S)

Compile local query-machine callbacks and a start state computable in space O(S) into concrete finite native routines.