OAI/Computability/Superstring/Instructions.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Superstring.BitCode.Store line 7
2. inductive OAI.Superstring.BitCode.Instr line 11

   Source documentation

   A finite-control bit-stack instruction. There is no unbounded internal state and no operation on an entire stack other than one push/pop/peek.

   inductive Instr (K L : Type)
     | push (k : K) (b : Bool) (next : L)
     | pop (k : K) (next : L)
     | branch (k : K) (empty low high : L)
     | jump (next : L)
   
   namespace Instr

3. def OAI.Superstring.BitCode.Instr.map line 19
4. def OAI.Superstring.BitCode.Instr.run line 25
5. theorem OAI.Superstring.BitCode.Instr.run_map line 34
6. def OAI.Superstring.BitCode.Instr.emit line 43
7. theorem OAI.Superstring.BitCode.Instr.finish_step line 56
8. theorem OAI.Superstring.BitCode.Instr.emit_step line 61
9. inductive OAI.Superstring.BitCode.Block line 77

   Source documentation

   Structured bit-stack code. Loops are ordinary operational loops, not unbounded-cost primitives. Their iteration count is charged in Exec.

   inductive Block (K : Type)
     | push (k : K) (b : Bool)
     | pop (k : K)
     | skip
     | branch (k : K) (empty low high : Block K)
     | seq (first second : Block K)
     | loop (k : K) (body : Block K)
   
   namespace Block

10. def OAI.Superstring.BitCode.Block.Label line 87
11. instance OAI.Superstring.BitCode.Block.labelFintype line 93
12. instance OAI.Superstring.BitCode.Block.labelDecidableEq line 108
13. def OAI.Superstring.BitCode.Block.start line 123
14. def OAI.Superstring.BitCode.Block.code line 129
15. inductive OAI.Superstring.BitCode.Steps line 157

    Source documentation

    Exact execution in the finite-control graph, stopping before a halt label is stepped. This is a finite trace, not an oracle for a computation.

    inductive Steps {L : Type} (code : L → Instr K (Option L)) :
        (Option L × Store K) → ℕ → (Option L × Store K) → Prop
      | refl (c) : Steps code c 0 c
      | step (l : L) (s : Store K) {n d} (h : Steps code ((code l).run s) n d) :
          Steps code (some l, s) (n + 1) d
    
    namespace Steps
    
    variable {L M : Type} {code : L → Instr K (Option L)}

    Mentions: OAI.Superstring.BitCode.Instr, OAI.Superstring.BitCode.Store

16. theorem OAI.Superstring.BitCode.Steps.trans line 167
17. theorem OAI.Superstring.BitCode.Steps.map line 173
18. inductive OAI.Superstring.BitCode.Block.Exec line 191

    Source documentation

    Big-step semantics with the exact number of primitive bit instructions.

    inductive Exec : Block K → Store K → Store K → ℕ → Prop
      | push (k b s) : Exec (.push k b) s (Function.update s k (b :: s k)) 1
      | pop (k s) : Exec (.pop k) s (Function.update s k (s k).tail) 1
      | skip (s) : Exec .skip s s 1
      | branch_none {k a b c s t n} (h : (s k).head? = none) (run : Exec a s t n) :
          Exec (.branch k a b c) s t (n + 1)
      | branch_false {k a b c s t n} (h : (s k).head? = some false) (run : Exec b s t n) :
          Exec (.branch k a b c) s t (n + 1)
      | branch_true {k a b c s t n} (h : (s k).head? = some true) (run : Exec c s t n) :
          Exec (.branch k a b c) s t (n + 1)
      | seq {a b s t u m n} (first : Exec a s t m) (second : Exec b t u n) :
          Exec (.seq a b) s u (m + n)
    …

    Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store

19. theorem OAI.Superstring.BitCode.Block.exec_steps line 207
20. def OAI.Superstring.BitCode.Block.machine line 251
21. def OAI.Superstring.BitCode.Block.pack line 262
22. theorem OAI.Superstring.BitCode.Block.steps_iterate line 265
23. def OAI.Superstring.BitCode.Block.exec_machine line 275
24. def OAI.Superstring.BitCode.single line 290

    Source documentation

    A single populated stack: the exact Mathlib initial/final convention.

    def single (k : K) (w : List Bool) : Store K := fun j => if j = k then w else []
    …

    Mentions: OAI.Superstring.BitCode.Store

25. theorem OAI.Superstring.BitCode.Block.init_eq line 294
26. theorem OAI.Superstring.BitCode.Block.halt_eq line 304
27. def OAI.Superstring.BitCode.Block.certificate line 315

    Source documentation

    Execution with a polynomial clock gives a polynomial-time TM2 certificate.

    noncomputable def certificate [Fintype K] {α β : Type}
        (ea : α → List Bool) (eb : β → List Bool) (f : α → β)
        (b : Block K) (i o : K) (P : Polynomial ℕ)
        (correct : ∀ a, ∃ n, n ≤ P.eval (ea a).length ∧
          b.Exec (single i (ea a)) (single o (eb (f a))) n) :
        Turing.TM2ComputableInPolyTime ea eb f where
    …

    Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single

28. theorem OAI.Superstring.BitCode.Block.certificate_finite line 339
29. def OAI.Superstring.BitCode.size line 352
30. theorem OAI.Superstring.BitCode.size_update line 354
31. theorem OAI.Superstring.BitCode.size_push line 369
32. theorem OAI.Superstring.BitCode.size_pop line 375
33. theorem OAI.Superstring.BitCode.Block.Exec.size_le line 383

    Source documentation

    Every actually executed primitive bit instruction increases total stored length by at most one; branch tests and iterations do not hide bulk operations.

    theorem Block.Exec.size_le {b : Block K} {s t : Store K} {n : ℕ}
        (h : b.Exec s t n) : size t ≤ size s + n := by
    …

    Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.size