FiniteCompiler.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Raw unary input adapter for the finite block-coded stack compiler. The alphabet is exactly Fin 4. No list-processing oracle is an instruction.

def OAI.RationalHitting.StackLanguage.Compiler.stackConstant line 10
lemma OAI.RationalHitting.StackLanguage.Compiler.stackConstant_bound line 13
abbrev OAI.RationalHitting.StackLanguage.Compiler.TapeAlphabet line 20
abbrev OAI.RationalHitting.StackLanguage.Compiler.TapeLabels line 21
def OAI.RationalHitting.StackLanguage.Compiler.tapeSupport line 22
def OAI.RationalHitting.StackLanguage.Compiler.tapeConstant line 24
lemma OAI.RationalHitting.StackLanguage.Compiler.tapeConstant_bound line 28
lemma OAI.RationalHitting.StackLanguage.Compiler.tapeSupported line 36

theorem OAI.RationalHitting.StackLanguage.Compiler.finite_compilation line 43

Source documentation

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.

theorem finite_compilation (p : Program K) :
    ∃ (m : ℕ) (G : TM0.Machine (TapeAlphabet K) (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ (k : K) (w : List Bool) (v : Store K) (t : ℕ),
        Eval p (Function.update (fun _ => []) k w) v t →
        ∃ u ≤ C*(w.length+t+3)^2, ∃ a,
          exec (TM0.step G) u (TM0.init (TM2to1.trInit k w))=some a ∧
          TM0.step G a=none ∧
          ∃ b : TM1.Cfg (TapeAlphabet K) (TapeLabels K) (Option Bool),
            TM2to1.TrCfg (⟨none,none,v⟩ : TM2.Cfg (fun _ : K => Bool) (Labels K) (Option Bool)) b ∧
            a.Tape=b.Tape := by
…

Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.Compiler.TapeAlphabet, OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.Compiler.TapeLabels, OAI.RationalHitting.StackLanguage.Labels

def OAI.RationalHitting.TMTime.Alphabet.writesWeight line 106

Source documentation

Number of deferred writes along the longest branch.

def writesWeight : TM1.Stmt Γ Λ σ → ℕ
  | .move _ q | .load _ q => writesWeight q
  | .write _ q => writesWeight q+1
  | .branch _ q r => max (writesWeight q) (writesWeight r)
  | .goto _ | .halt => 0

include encdec

/-- Alphabet coding adds at most one macrostep per deferred write. -/

Mentions: OAI.RationalHitting.Alphabet

theorem OAI.RationalHitting.TMTime.Alphabet.continuation_time line 115

Source documentation

Alphabet coding adds at most one macrostep per deferred write.

theorem continuation_time (M : Λ → TM1.Stmt Γ Λ σ) (q : TM1.Stmt Γ Λ σ)
    (v : σ) (L R : ListBlank Γ) :
    ∃ t ≤ writesWeight q,
      exec (TM1.step (TM1to1.tr enc dec M)) t
        (TM1.stepAux (TM1to1.trNormal dec q) v (TM1to1.trTape' enc0 L R)) =
        some (TM1to1.trCfg enc enc0 (TM1.stepAux q v (Tape.mk' L R))) := by
…

Mentions: OAI.RationalHitting.TMTime.Alphabet.writesWeight, OAI.RationalHitting.TMTime.exec

theorem OAI.RationalHitting.TMTime.Alphabet.execution_time line 159

Source documentation

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

theorem execution_time [Inhabited Λ] (M : Λ → TM1.Stmt Γ Λ σ) (S : Finset Λ)
    (hs : TM1.Supports M S) (C : ℕ) (hC : ∀ l ∈ S, writesWeight (M l)+1 ≤ C)
    (t : ℕ) (a b : TM1.Cfg Γ Λ σ) (ha : a.l ∈ Finset.insertNone S)
    (hr : exec (TM1.step M) t a = some b) :
    ∃ u ≤ C*t, exec (TM1.step (TM1to1.tr enc dec M)) u
      (TM1to1.trCfg enc enc0 a) = some (TM1to1.trCfg enc enc0 b) := by
…

Mentions: OAI.RationalHitting.TMTime.Alphabet.writesWeight, OAI.RationalHitting.TMTime.exec

theorem OAI.RationalHitting.TMTime.Alphabet.halts line 191
lemma OAI.RationalHitting.TMTime.Alphabet.compiled_init line 203
instance OAI.RationalHitting.StackLanguage.Compiler.finiteTapeAlphabet line 218
Source comment
The alphabet is finite because the number of stacks is fixed.
```
noncomputable instance finiteTapeAlphabet : Fintype (TapeAlphabet K) := by
…
```
Mentions: OAI.RationalHitting.StackLanguage.Compiler.TapeAlphabet

theorem OAI.RationalHitting.StackLanguage.Compiler.binary_compilation line 225

Source documentation

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

theorem binary_compilation (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,dec (enc a)=a) ∧
      ∃ (m : ℕ) (G : TM0.Machine Bool (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ (k : K) (w : List Bool) (v : Store K) (t : ℕ),
        Eval p (Function.update (fun _ => []) k w) v t →
        ∃ u ≤ C*(w.length+t+3)^2, ∃ a,
          exec (TM0.step G) u (TM0.init ((TM2to1.trInit k w).flatMap (fun z => (enc z).toList)))=some a ∧
          TM0.step G a=none ∧
          ∃ c : TM1.Cfg (TapeAlphabet K) (TapeLabels K) (Option Bool),
…

lemma OAI.RationalHitting.TMTime.OneToZero.supports_univ line 312

theorem OAI.RationalHitting.TMTime.OneToZero.finite_compiler line 318

Source documentation

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

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

Mentions: OAI.RationalHitting.TMTime.exec