Compiler.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RationalHitting.TMTime.Link.left line 10
def OAI.RationalHitting.TMTime.Link.right line 11
def OAI.RationalHitting.TMTime.Link.machine line 13
lemma OAI.RationalHitting.TMTime.Link.step_left line 19
lemma OAI.RationalHitting.TMTime.Link.switch line 32
lemma OAI.RationalHitting.TMTime.Link.step_right line 38
lemma OAI.RationalHitting.TMTime.Link.run_left line 44
lemma OAI.RationalHitting.TMTime.Link.run_right line 54

theorem OAI.RationalHitting.TMTime.Link.finite_sequence line 65

Source documentation

Splice two halting finite transducers with exactly one glue step. The intermediate output is the literal tape required by the second input.

theorem finite_sequence [Fintype Λ] [Fintype Δ]
    (F : TM0.Machine Γ Λ) (G : TM0.Machine Γ Δ) :
    ∃ (m : ℕ) (H : TM0.Machine Γ (Fin (m+1))),
      ∀ (w v : List Γ) (t u : ℕ) (a : TM0.Cfg Γ Λ) (b : TM0.Cfg Γ Δ),
        exec (TM0.step F) t (TM0.init w)=some a → TM0.step F a=none →
        a.Tape=Tape.mk₁ v → exec (TM0.step G) u (TM0.init v)=some b → TM0.step G b=none →
        ∃ c, exec (TM0.step H) (t+1+u) (TM0.init w)=some c ∧ TM0.step H c=none ∧ c.Tape=b.Tape := by
…

Mentions: OAI.RationalHitting.TMTime.exec

abbrev OAI.RationalHitting.TMTime.BinaryLift.A line 94
def OAI.RationalHitting.TMTime.BinaryLift.bit line 95
def OAI.RationalHitting.TMTime.BinaryLift.bitMap line 96
lemma OAI.RationalHitting.TMTime.BinaryLift.bit_read line 97
def OAI.RationalHitting.TMTime.BinaryLift.stmt line 99
def OAI.RationalHitting.TMTime.BinaryLift.machine line 102
def OAI.RationalHitting.TMTime.BinaryLift.cfg line 104
lemma OAI.RationalHitting.TMTime.BinaryLift.step line 105
lemma OAI.RationalHitting.TMTime.BinaryLift.run line 112
lemma OAI.RationalHitting.TMTime.BinaryLift.run_init line 120
lemma OAI.RationalHitting.TMTime.Alphabet.tape_init line 133

theorem OAI.RationalHitting.StackLanguage.Compiler.raw_compilation line 147

Source documentation

End-to-end, finite-state, Fin4 one-tape compilation. Input and output are literal 1/2 digit strings, NOT different encodings hidden by an interface. The stack program is a single fixed finite syntax tree. Final scratch must be empty; the designated output stack has reversed output order, as explicitly stated.

theorem raw_compilation (p : Program K) (ki ko : K) :
    ∃ (m : ℕ) (G : TM0.Machine (Fin 4) (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ (w xs : List Bool) (t : ℕ), w≠[] →
        Eval p (Function.update (fun _ => []) ki w)
          (Function.update (fun _ => []) ko xs.reverse) t →
        ∃ u≤C*(w.length+t+xs.length+3)^2, ∃ a,
          exec (TM0.step G) u (TM0.init (w.map InputAdapter.raw))=some a ∧
          TM0.step G a=none ∧ a.Tape=Tape.mk₁ (xs.map OutputAdapter.raw) := by
…

Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.Eval

def OAI.RationalHitting.ExecutableGenerator.unaryWord line 199
Source documentation
A fixed finite stack program with literal unary input and exact canonical output, bounded by a fixed polynomial in the input length.
```
def unaryWord (n s : ℕ) : List Bool :=
…
```
def OAI.RationalHitting.ExecutableGenerator.StackImplementation line 202
lemma OAI.RationalHitting.ExecutableGenerator.run_eq_exec line 209
lemma OAI.RationalHitting.ExecutableGenerator.unaryWord_raw line 215
lemma OAI.RationalHitting.ExecutableGenerator.encoded_raw line 218
lemma OAI.RationalHitting.ExecutableGenerator.compilation_sum_bound line 221
lemma OAI.RationalHitting.ExecutableGenerator.compilation_square_bound line 225
theorem OAI.RationalHitting.ExecutableGenerator.implementation_of_stack line 232
Source documentation
The raw compiler preserves literal input/output and gives a fixed finite alphabet and state space with a polynomial transition bound.
```
theorem implementation_of_stack (h : StackImplementation) : Implementation := by
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.StackImplementation, OAI.RationalHitting.ExecutableGenerator.Implementation