Rational hitting lists: finite compiler

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/FiniteCompiler.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

noncomputable def Complexity.RationalHitting.StackLanguage.Compiler.stackConstant {K : Type} [DecidableEq K] (p : Program K) : ℕ

Program-dependent coefficient bounding stack-access simulation overhead.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Compiler.stackConstant_bound {K : Type} [DecidableEq K] (p : Program K) (l : Labels K) (hl : l ∈ support p) : TMTime.StackToOne.stackWeight (machine p l) + 1 ≤ stackConstant p

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Compiler.TapeAlphabet (K : Type) : Type

The multi-track tape alphabet used to simulate the Boolean stacks.

Equations

• Complexity.RationalHitting.StackLanguage.Compiler.TapeAlphabet K = Turing.TM2to1.Γ' K fun (x : K) => Bool

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Compiler.TapeLabels (K : Type) : Type

The tape-machine control labels produced by stack compilation.

Equations

• Complexity.RationalHitting.StackLanguage.Compiler.TapeLabels K = Turing.TM2to1.Λ' K (fun (x : K) => Bool) (Complexity.RationalHitting.StackLanguage.Labels K) (Option Bool)

noncomputable def Complexity.RationalHitting.StackLanguage.Compiler.tapeSupport {K : Type} [DecidableEq K] (p : Program K) : Finset (TapeLabels K)

The finite tape-machine support generated by the stack program.

Equations

• Complexity.RationalHitting.StackLanguage.Compiler.tapeSupport p = Turing.TM2to1.trSupp (Complexity.RationalHitting.StackLanguage.machine p) (Complexity.RationalHitting.StackLanguage.support p)

noncomputable def Complexity.RationalHitting.StackLanguage.Compiler.tapeConstant {K : Type} [DecidableEq K] (p : Program K) : ℕ

Program-dependent coefficient bounding compilation to ordinary tape steps.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.Compiler.tapeConstant_bound {K : Type} [DecidableEq K] (p : Program K) (l : TapeLabels K) (hl : l ∈ tapeSupport p) : TMTime.OneToZero.weight (Turing.TM2to1.tr (machine p) l) ≤ tapeConstant p

theorem Complexity.RationalHitting.StackLanguage.Compiler.tapeSupported {K : Type} [DecidableEq K] (p : Program K) : Turing.TM1.Supports (Turing.TM2to1.tr (machine p)) (tapeSupport p)

theorem Complexity.RationalHitting.StackLanguage.Compiler.finite_compilation {K : Type} [DecidableEq K] (p : Program K) : ∃ (m : ℕ) (G : Turing.TM0.Machine (TapeAlphabet K) (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (k : K) (w : List Bool) (v : Store K) (t : ℕ), Eval p (Function.update (fun (x : K) => []) k w) v t → ∃ u ≤ C * (w.length + t + 3) ^ 2, ∃ (a : Turing.TM0.Cfg (TapeAlphabet K) (Fin (m + 1))), TMTime.exec (Turing.TM0.step G) u (Turing.TM0.init (Turing.TM2to1.trInit k w)) = some a ∧ Turing.TM0.step G a = none ∧ ∃ (b : Turing.TM1.Cfg (TapeAlphabet K) (TapeLabels K) (Option Bool)), Turing.TM2to1.TrCfg { l := none, var := none, stk := v } b ∧ a.Tape = b.Tape

A single finite-state TM0, independent of the input word, with quadratic cost in stack execution time plus input length. The output is the encoded family of stacks.

def Complexity.RationalHitting.TMTime.Alphabet.writesWeight {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} : Turing.TM1.Stmt Γ Λ σ → ℕ

Number of deferred writes along the longest branch.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.TMTime.Alphabet.writesWeight (Turing.TM1.Stmt.move a q) = Complexity.RationalHitting.TMTime.Alphabet.writesWeight q
• Complexity.RationalHitting.TMTime.Alphabet.writesWeight (Turing.TM1.Stmt.load a q) = Complexity.RationalHitting.TMTime.Alphabet.writesWeight q
• Complexity.RationalHitting.TMTime.Alphabet.writesWeight (Turing.TM1.Stmt.write a q) = Complexity.RationalHitting.TMTime.Alphabet.writesWeight q + 1
• Complexity.RationalHitting.TMTime.Alphabet.writesWeight (Turing.TM1.Stmt.goto a) = 0
• Complexity.RationalHitting.TMTime.Alphabet.writesWeight Turing.TM1.Stmt.halt = 0

theorem Complexity.RationalHitting.TMTime.Alphabet.continuation_time {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ) (enc0 : enc default = List.Vector.replicate n false) (encdec : ∀ (a : Γ), dec (enc a) = a) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ) (L R : Turing.ListBlank Γ) : ∃ t ≤ writesWeight q, exec (Turing.TM1.step (Turing.TM1to1.tr enc dec M)) t (Turing.TM1.stepAux (Turing.TM1to1.trNormal dec q) v (Turing.TM1to1.trTape' enc0 L R)) = some (Turing.TM1to1.trCfg enc enc0 (Turing.TM1.stepAux q v (Turing.Tape.mk' L R)))

Alphabet coding adds at most one macrostep per deferred write.

theorem Complexity.RationalHitting.TMTime.Alphabet.execution_time {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ) (enc0 : enc default = List.Vector.replicate n false) (encdec : ∀ (a : Γ), dec (enc a) = a) [Inhabited Λ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) (C : ℕ) (hC : ∀ l ∈ S, writesWeight (M l) + 1 ≤ C) (t : ℕ) (a b : Turing.TM1.Cfg Γ Λ σ) (ha : a.l ∈ Finset.insertNone S) (hr : exec (Turing.TM1.step M) t a = some b) : ∃ u ≤ C * t, exec (Turing.TM1.step (Turing.TM1to1.tr enc dec M)) u (Turing.TM1to1.trCfg enc enc0 a) = some (Turing.TM1to1.trCfg enc enc0 b)

Linear macrostep time overhead for the finite-alphabet compiler. Physical moves and reads are subsequently counted by the quantitative TM1->TM0 compiler.

theorem Complexity.RationalHitting.TMTime.Alphabet.halts {Γ : Type v_1} {Λ : Type v_2} {σ : Type v_3} [Inhabited Γ] {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ) (enc0 : enc default = List.Vector.replicate n false) (_encdec : ∀ (a : Γ), dec (enc a) = a) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (a : Turing.TM1.Cfg Γ Λ σ) (ha : Turing.TM1.step M a = none) : Turing.TM1.step (Turing.TM1to1.tr enc dec M) (Turing.TM1to1.trCfg enc enc0 a) = none

theorem Complexity.RationalHitting.TMTime.Alphabet.compiled_init {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] {b : ℕ} (enc : Γ → List.Vector Bool b) (h0 : enc default = List.Vector.replicate b false) (w : List Γ) : Turing.TM1to1.trCfg enc h0 (Turing.TM1.init w) = Turing.TM1.init (List.flatMap (fun (a : Γ) => (enc a).toList) w)

@[instance_reducible]

noncomputable instance Complexity.RationalHitting.StackLanguage.Compiler.finiteTapeAlphabet {K : Type} [DecidableEq K] [Fintype K] : Fintype (TapeAlphabet K)

Equations

• Complexity.RationalHitting.StackLanguage.Compiler.finiteTapeAlphabet = id (id inferInstance)

theorem Complexity.RationalHitting.StackLanguage.Compiler.binary_compilation {K : Type} [DecidableEq K] [Fintype K] (p : Program K) : ∃ (b : ℕ) (enc : TapeAlphabet K → List.Vector Bool b) (dec : List.Vector Bool b → TapeAlphabet K) (h0 : enc default = List.Vector.replicate b false), (∀ (a : TapeAlphabet K), dec (enc a) = a) ∧ ∃ (m : ℕ) (G : Turing.TM0.Machine Bool (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (k : K) (w : List Bool) (v : Store K) (t : ℕ), Eval p (Function.update (fun (x : K) => []) k w) v t → ∃ u ≤ C * (w.length + t + 3) ^ 2, ∃ (a : Turing.TM0.Cfg Bool (Fin (m + 1))), TMTime.exec (Turing.TM0.step G) u (Turing.TM0.init (List.flatMap (fun (z : TapeAlphabet K) => (enc z).toList) (Turing.TM2to1.trInit k w))) = some a ∧ Turing.TM0.step G a = none ∧ ∃ (c : Turing.TM1.Cfg (TapeAlphabet K) (TapeLabels K) (Option Bool)), Turing.TM2to1.TrCfg { l := none, var := none, stk := v } c ∧ a.Tape = Turing.TM1to1.trTape h0 c.Tape

Polynomial-time compilation to a binary finite-state TM0, preserving an explicit fixed block encoding.

theorem Complexity.RationalHitting.TMTime.OneToZero.supports_univ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Fintype Λ] (q : Turing.TM1.Stmt Γ Λ σ) : Turing.TM1.SupportsStmt Finset.univ q

theorem Complexity.RationalHitting.TMTime.OneToZero.finite_compiler {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Λ] [Fintype σ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) : ∃ (m : ℕ) (G : Turing.TM0.Machine Γ (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (w : List Γ) (t : ℕ) (a : Turing.TM1.Cfg Γ Λ σ), exec (Turing.TM1.step M) t (Turing.TM1.init w) = some a → Turing.TM1.step M a = none → ∃ u ≤ C * t, ∃ (b : Turing.TM0.Cfg Γ (Fin (m + 1))), exec (Turing.TM0.step G) u (Turing.TM0.init w) = some b ∧ Turing.TM0.step G b = none ∧ b.Tape = a.Tape

Every fixed finite-control TM1 has an ordinary finite-state TM0 compiling all runs at a fixed linear cost and preserving the literal tape.