Native query-loop termination

A decreasing natural rank at continuation boundaries gives a finite all-branches native time bound. The rank and the time bound are ghost data used in the proof. Neither is encoded or stored by the native machine.

Main definitions

• Turing.NondeterministicQueryMachine.Native.HaltsFrom: all paths from a configuration halt within a common number of native steps.

Main results

• Turing.NondeterministicQueryMachine.Native.choose_haltsFrom: a preserved word invariant and a decreasing rank on nonfinal passes imply an all-branches time bound.

def Turing.NondeterministicQueryMachine.Native.HaltsFrom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (c : Cfg k Bool (State SI SP SF) input) (t : ℕ) : Prop

All native paths from c of at least t steps end halted.

theorem Turing.NondeterministicQueryMachine.Native.finish_haltsFrom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} {ws : Fin k → List Bool} (out : List Bool) {t s : ℕ} (hF : F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) : HaltsFrom I P F C (wordsCfg input (some (State.finish F.q₀)) ws out) t

A tidy deterministic finalizer gives a common native halting bound from its start.

theorem Turing.NondeterministicQueryMachine.Native.choose_haltsFrom {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (Inv : (Fin k → List Bool) → Prop) (rank : (Fin k → List Bool) → ℕ) (hP : ∀ (b : Bool) (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ) (s : ℕ), (P b).TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 w' : Fin k → List Bool) (x_2 : List Bool) => Inv w' ∧ (w' C ≠ [] → rank w' < rank ws)) t s) (hF : ∀ (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ) (s : ℕ), F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) {ws : Fin k → List Bool} (hInv : Inv ws) (out : List Bool) : ∃ (t : ℕ), HaltsFrom I P F C (wordsCfg input (some State.choose) ws out) t

The native pass loop halts on every branch when continuation strictly decreases a natural rank. The proof takes maxima of two branch bounds; the machine stores neither rank nor clock.

theorem Turing.NondeterministicQueryMachine.Native.exists_runsInTime_of_transforms {k : ℕ} {SI SF : Type} {SP : Bool → Type} (I : MultiTapeTM k Bool SI) (P : (b : Bool) → MultiTapeTM k Bool (SP b)) (F : MultiTapeTM k Bool SF) (C : Fin k) {input : List Bool} (Inv : (Fin k → List Bool) → Prop) (rank : (Fin k → List Bool) → ℕ) {tI sI : ℕ} (hI : I.TransformsTapes (fun (inp : List Bool) (ws : Fin k → List Bool) => inp = input ∧ ws = fun (x : Fin k) => []) (fun (x : List Bool) (x_1 ws' : Fin k → List Bool) (x_2 : List Bool) => Inv ws') tI sI) (hP : ∀ (b : Bool) (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ) (s : ℕ), (P b).TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 w' : Fin k → List Bool) (x_2 : List Bool) => Inv w' ∧ (w' C ≠ [] → rank w' < rank ws)) t s) (hF : ∀ (ws : Fin k → List Bool), Inv ws → ∃ (t : ℕ) (s : ℕ), F.TransformsTapes (fun (inp : List Bool) (w : Fin k → List Bool) => inp = input ∧ w = ws) (fun (x : List Bool) (x_1 x_2 : Fin k → List Bool) (x_3 : List Bool) => True) t s) : ∃ (t : ℕ), (machine I P F C).RunsInTime input t

A tidy initializer followed by the ranked native loop has a per-input all-branches clock.