OAI/Computability/RationalHitting/StackLanguage.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

A finite structured binary-stack language. Every primitive is a push, pop, or transfer.

  1. def OAI.RationalHitting.TMTime.exec line 8
  2. lemma OAI.RationalHitting.TMTime.exec_zero line 12
  3. lemma OAI.RationalHitting.TMTime.exec_add line 14
  4. lemma OAI.RationalHitting.TMTime.exec_trans line 21
  5. lemma OAI.RationalHitting.TMTime.exec_positive_congr line 25
  6. def OAI.RationalHitting.TMTime.OneToZero.weight line 35

    Source documentation

    Syntactic statement bound, fixed once the finite machine is fixed.

    def weight : TM1.Stmt Γ Λ σ → ℕ
  | .move _ q | .write _ q | .load _ q => weight q+1
  | .branch _ q r => max (weight q) (weight r)+1
  | .goto _ | .halt => 1
  7. lemma OAI.RationalHitting.TMTime.OneToZero.weight_pos line 40
  8. theorem OAI.RationalHitting.TMTime.OneToZero.statement_time line 46

    Source documentation

    Each TM1 macro-step takes at most its statement size in real TM0 steps. Load and branch are absorbed into the next primitive step by Mathlib's compiler.

    theorem statement_time (M : Λ → TM1.Stmt Γ Λ σ) (q : TM1.Stmt Γ Λ σ) (v : σ) (T : Tape Γ) :
    ∃ t, 0<t ∧ t ≤ weight q ∧
      exec (TM0.step (TM1to0.tr M)) t ⟨(some q,v),T⟩ =
        some (TM1to0.trCfg M (TM1.stepAux q v T)) := by
…

    Mentions: OAI.RationalHitting.TMTime.OneToZero.weight, OAI.RationalHitting.TMTime.exec

  9. theorem OAI.RationalHitting.TMTime.OneToZero.execution_time line 91

    Source documentation

    Linear transition overhead for a finitely supported TM1 program.

    theorem execution_time (M : Λ → TM1.Stmt Γ Λ σ) (S : Finset Λ)
    (hs : TM1.Supports M S) (C : ℕ) (hC : ∀ l ∈ S, weight (M l) ≤ 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 (TM0.step (TM1to0.tr M)) u (TM1to0.trCfg M a) =
      some (TM1to0.trCfg M b) := by
…

    Mentions: OAI.RationalHitting.TMTime.OneToZero.weight, OAI.RationalHitting.TMTime.exec

  10. theorem OAI.RationalHitting.TMTime.OneToZero.halts line 117
  11. inductive OAI.RationalHitting.StackLanguage.Program line 132
  12. abbrev OAI.RationalHitting.StackLanguage.Store line 142
  13. abbrev OAI.RationalHitting.StackLanguage.Labels line 143
  14. def OAI.RationalHitting.StackLanguage.transfer line 147

    Source documentation

    Move one head symbol if present, popping the first register before updating the second, including when both registers coincide.

    def transfer (a b : K) (s : Store K) : Store K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Store

  15. inductive OAI.RationalHitting.StackLanguage.Eval line 153
  16. abbrev OAI.RationalHitting.StackLanguage.Stmt line 173
  17. def OAI.RationalHitting.StackLanguage.jump line 175
  18. def OAI.RationalHitting.StackLanguage.instruction line 178
  19. def OAI.RationalHitting.StackLanguage.machine line 193
  20. def OAI.RationalHitting.StackLanguage.cfg line 197
  21. theorem OAI.RationalHitting.StackLanguage.jump_eval line 200
  22. theorem OAI.RationalHitting.StackLanguage.eval_compiles line 205

    Source documentation

    Exact big-step correctness in real TM2 steps, with no unbounded internal state or alphabet.

    theorem eval_compiles {p : Program K} {s v : Store K} {t : ℕ}
    (h : Eval p s v t) (main : Program K) (ps : List (Program K)) :
    exec (TM2.step (machine main)) t (cfg (p::ps) s) = some (cfg ps v) := by
…

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.machine, OAI.RationalHitting.StackLanguage.cfg

  23. def OAI.RationalHitting.StackLanguage.successors line 243

    Source documentation

    Possible jump targets; inspecting a head has only three finite cases.

    def successors : List (Program K) → Finset (List (Program K))
  | [] => ∅
  | .skip :: ps => {ps}
  | .push _ _ :: ps | .drop _ :: ps | .transfer _ _ :: ps => {ps}
  | .seq p q :: ps => {p::q::ps}
  | .branch _ p q r :: ps => {p::ps,q::ps,r::ps}
  | .loop k p :: ps => {ps,p::.loop k p::ps}

/-- Finite control locations, computed structurally, despite unbounded loop
iteration counts. -/

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.transfer, OAI.RationalHitting.StackLanguage.locations

  24. def OAI.RationalHitting.StackLanguage.locations line 253

    Source documentation

    Finite control locations, computed structurally, despite unbounded loop iteration counts.

    def locations : Program K → List (Program K) → Finset (List (Program K))
  | p@(.skip),ps | p@(.push ..),ps | p@(.drop ..),ps | p@(.transfer ..),ps => {p::ps,ps}
  | p@(.seq a b),ps => insert (p::ps) (locations a (b::ps) ∪ locations b ps)
  | p@(.branch _ a b c),ps => insert (p::ps) (locations a ps ∪ locations b ps ∪ locations c ps)
  | p@(.loop _ a),ps => insert (p::ps) (insert ps (locations a (p::ps)))

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

  25. theorem OAI.RationalHitting.StackLanguage.entry_mem line 259
  26. theorem OAI.RationalHitting.StackLanguage.exit_mem line 262
  27. lemma OAI.RationalHitting.StackLanguage.root_closed line 265
  28. lemma OAI.RationalHitting.StackLanguage.locations_closed line 277
  29. def OAI.RationalHitting.StackLanguage.support line 314
  30. lemma OAI.RationalHitting.StackLanguage.instruction_supported line 316
  31. theorem OAI.RationalHitting.StackLanguage.machine_supported line 324
  32. theorem OAI.RationalHitting.StackLanguage.complete_run line 340

    Source documentation

    Entry and halting are one actual macrostep apiece.

    theorem complete_run {p : Program K} {s v : Store K} {t : ℕ} (h : Eval p s v t) :
    exec (TM2.step (machine p)) (t+2) ⟨some none,none,s⟩ = some ⟨none,none,v⟩ := by
…

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