Native linear-workspace compact-graph routines

All runtime numbers use binary encodings. The table and register indices are fixed, so the algorithms below use finitely many linear-workspace arithmetic routines. These certificates charge no copy of the original input word: the edge routine receives only its length, two IDs, and the single supplied symbol. The time bound is unrestricted.

The routines take the radix as a computed argument, so they serve every radix, such as one stored by the caller.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.readRegisters_budget, Turing.MultiTapeNTM.ConfigurationGraph.valid_budget, Turing.MultiTapeNTM.ConfigurationGraph.nextRegisters_budget, Turing.MultiTapeNTM.ConfigurationGraph.matchesEntry_budget, Turing.MultiTapeNTM.ConfigurationGraph.fitsB_budget: register-level space-budget routines.
• Turing.MultiTapeNTM.ConfigurationGraph.queryIndex_budget: compute the only input query.
• Turing.MultiTapeNTM.ConfigurationGraph.edgeWithSymbol_budget: evaluate an edge locally.
• Turing.MultiTapeNTM.ConfigurationGraph.bad_budget: recognize an accepting halted vertex.
• Turing.MultiTapeNTM.ConfigurationGraph.overflow_budget: recognize a step leaving the radix.
• Turing.MultiTapeNTM.ConfigurationGraph.vertexBound_budget, Turing.MultiTapeNTM.ConfigurationGraph.startID_budget: the size and the start of the graph.

theorem Turing.MultiTapeNTM.ConfigurationGraph.readRegisters_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {B u : α → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) (i : Register k) : MultiTapeTM.ComputableInSpace (fun (a : α) => readRegisters (B a) (u a) i) enc MultiTapeTM.encNat S

Reading any fixed register preserves a common space budget.

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexBound_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {B : α → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => vertexBound (B a)) enc MultiTapeTM.encNat S

The ambient graph size is computable from the radix.

theorem Turing.MultiTapeNTM.ConfigurationGraph.valid_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {B n u : α → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => valid (B a) (n a) (u a)) enc MultiTapeTM.encBool S

Syntactic validity of a packed ID preserves a common space budget.

theorem Turing.MultiTapeNTM.ConfigurationGraph.nextRegisters_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {n : α → ℕ} {r : α → Register k → ℕ} (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hr : ∀ (i : Register k), MultiTapeTM.ComputableInSpace (fun (a : α) => r a i) enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) (act : Action k Bool State) (i : Register k) : MultiTapeTM.ComputableInSpace (fun (a : α) => nextRegisters (n a) (r a) act i) enc MultiTapeTM.encNat S

Updating any fixed register by a fixed native action preserves a common space budget.

theorem Turing.MultiTapeNTM.ConfigurationGraph.matchesEntry_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {n : α → ℕ} {symbol : α → Option Bool} {r : α → Register k → ℕ} (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hr : ∀ (i : Register k), MultiTapeTM.ComputableInSpace (fun (a : α) => r a i) enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableInSpace symbol enc (MultiTapeTM.encOption MultiTapeTM.encBool) S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) (t : Instruction k State) : MultiTapeTM.ComputableInSpace (fun (a : α) => matchesEntry (n a) (r a) (symbol a) t) enc MultiTapeTM.encBool S

Checking whether decoded registers match a fixed table entry preserves a common space budget.

theorem Turing.MultiTapeNTM.ConfigurationGraph.fitsB_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {B : α → ℕ} {r : α → Register k → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hr : ∀ (i : Register k), MultiTapeTM.ComputableInSpace (fun (a : α) => r a i) enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => fitsB (B a) (r a)) enc MultiTapeTM.encBool S

Checking that every register fits below the radix preserves a common space budget.

theorem Turing.MultiTapeNTM.ConfigurationGraph.edgeWithSymbol_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {B n u v : α → ℕ} {symbol : α → Option Bool} (ntm : MultiTapeNTM k Bool State) (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) (hv : MultiTapeTM.ComputableInSpace v enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableInSpace symbol enc (MultiTapeTM.encOption MultiTapeTM.encBool) S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => edgeWithSymbol ntm (B a) (n a) (u a) (v a) (symbol a)) enc MultiTapeTM.encBool S

Local edge evaluation preserves any budget covering the short arguments.

theorem Turing.MultiTapeNTM.ConfigurationGraph.overflow_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {B n u : α → ℕ} {symbol : α → Option Bool} (ntm : MultiTapeNTM k Bool State) (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) (hs : MultiTapeTM.ComputableInSpace symbol enc (MultiTapeTM.encOption MultiTapeTM.encBool) S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => overflow ntm (B a) (n a) (u a) (symbol a)) enc MultiTapeTM.encBool S

The overflow test preserves any budget covering the short arguments.

theorem Turing.MultiTapeNTM.ConfigurationGraph.queryIndex_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {B u : α → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) : MultiTapeTM.ComputableInSpace (fun (a : α) => queryIndex (B a) (u a)) enc MultiTapeTM.encNat S

Compute the only input query in native deterministic linear workspace.

theorem Turing.MultiTapeNTM.ConfigurationGraph.bad_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {B n u : α → ℕ} (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hn : MultiTapeTM.ComputableInSpace n enc MultiTapeTM.encNat S) (hu : MultiTapeTM.ComputableInSpace u enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => bad (B a) (n a) (u a)) enc MultiTapeTM.encBool S

Recognize the accepting halted vertices in native deterministic linear workspace.

theorem Turing.MultiTapeNTM.ConfigurationGraph.startID_budget {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {k : ℕ} {State : Type} [Fintype State] {B : α → ℕ} (ntm : MultiTapeNTM k Bool State) (hB : MultiTapeTM.ComputableInSpace B enc MultiTapeTM.encNat S) (hin : MultiTapeTM.BigOLe (fun (a : α) => (enc a).length) S) : MultiTapeTM.ComputableInSpace (fun (a : α) => startID ntm (B a)) enc MultiTapeTM.encNat S

Compute the input-independent start ID from the radix.