OAI/Computability/Logspace/CounterPrograms.lean

GitHub source file

141 declarations, 0 contain sorry, 0 declared as axioms

Bounded natural-register programs and their realization by finite deterministic machines.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. def OAI.ExactDerandomization.Counter.scan line 17
  2. lemma OAI.ExactDerandomization.Counter.scan_zero line 20
  3. lemma OAI.ExactDerandomization.Counter.scan_lt line 22
  4. lemma OAI.ExactDerandomization.Counter.marker_left line 25
  5. lemma OAI.ExactDerandomization.Counter.marker_right line 31
  6. lemma OAI.ExactDerandomization.Counter.scan_is_zero line 47
  7. def OAI.ExactDerandomization.Counter.dir line 53

    Source documentation

    dir = false means ascending

    def dir (q : ℕ) : Bool := decide (q%2=1)
  8. lemma OAI.ExactDerandomization.Counter.dir_zero line 55
  9. lemma OAI.ExactDerandomization.Counter.dir_next line 56
  10. def OAI.ExactDerandomization.Counter.digit line 60
  11. def OAI.ExactDerandomization.Counter.dirs line 64
  12. def OAI.ExactDerandomization.Counter.digits line 68
  13. lemma OAI.ExactDerandomization.Counter.dirs_zero line 72
  14. lemma OAI.ExactDerandomization.Counter.digits_zero line 79
  15. abbrev OAI.ExactDerandomization.Counter.obs line 86
  16. lemma OAI.ExactDerandomization.Counter.quot_bound line 88
  17. lemma OAI.ExactDerandomization.Counter.eq_zero_obs line 92
  18. def OAI.ExactDerandomization.Counter.symbol line 108
  19. lemma OAI.ExactDerandomization.Counter.symbol_obs line 112
  20. def OAI.ExactDerandomization.Counter.goLeft line 130

    Source documentation

    gray positive step at a digit: 'up' = increase overall number, 'rev' = digit reversed

    def goLeft (up rev : Bool) : Bool := decide (up = rev)
  21. def OAI.ExactDerandomization.Counter.spills line 131
  22. def OAI.ExactDerandomization.Counter.shift line 133
  23. def OAI.ExactDerandomization.Counter.attempt line 138

    Source documentation

    change orientation and multi-head moves, attempting to step (uses at interior, no overflow or underflow)

    def attempt (up : Bool) :
    (d : ℕ) → (Fin d → Bool) → (Fin d → InputSymbol) → (Fin d → Bool) × (Fin d → Direction)
  | 0, r, _ => (r, Fin.elim0)
  | d+1, r, s =>
    if spills up (r 0) (s 0) then
      let q := attempt up d (fun i => r i.succ) (fun i => s i.succ)
…

    Mentions: OAI.ExactDerandomization.InputSymbol, OAI.ExactDerandomization.Direction, OAI.ExactDerandomization.Counter.spills

  24. abbrev OAI.ExactDerandomization.Counter.steps line 147
  25. lemma OAI.ExactDerandomization.Counter.low_steps line 155
  26. lemma OAI.ExactDerandomization.Counter.high_steps line 168
  27. lemma OAI.ExactDerandomization.Counter.attempt_both line 183
  28. def OAI.ExactDerandomization.Counter.adj line 227
  29. def OAI.ExactDerandomization.Counter.ch line 234
  30. lemma OAI.ExactDerandomization.Counter.adj_spec line 240
  31. abbrev OAI.ExactDerandomization.Counter.Store line 272
  32. abbrev OAI.ExactDerandomization.Counter.Fit line 273
  33. structure OAI.ExactDerandomization.Counter.Jump line 276

    Source documentation

    bounded program instruction: read at i, set pc and maybe ±1 that same i.

    structure Jump (S : Type) where
…
  34. def OAI.ExactDerandomization.Counter.tweak line 280
  35. theorem OAI.ExactDerandomization.Counter.tweak_self line 283
  36. theorem OAI.ExactDerandomization.Counter.tweak_other line 286
  37. theorem OAI.ExactDerandomization.Counter.tweak_stay line 289
  38. def OAI.ExactDerandomization.Counter.Jump.apply line 293
  39. structure OAI.ExactDerandomization.Counter.CM line 297
  40. inductive OAI.ExactDerandomization.Counter.CM.Runs line 305
  41. theorem OAI.ExactDerandomization.Counter.CM.Runs.fits line 310
  42. def OAI.ExactDerandomization.Counter.CM.tab line 315
  43. def OAI.ExactDerandomization.Counter.CM.rep line 331
  44. lemma OAI.ExactDerandomization.Counter.CM.rep_step line 335
  45. theorem OAI.ExactDerandomization.Counter.CM.realize line 351

    Source documentation

    A Runs derivation supplies an input-dependent but tape-independent clock.

    theorem realize {x : Word} {m d : ℕ}
    (hm : ∀ s j, p.prog s = .inr j → j.atReg < m)
    {s : S} {c : Store} {b : Bool} (h : p.Runs x ((x.length+2)^d) s c b) :
    ∀ t, (∀ coins, (p.tab m d).run x coins t = rep x.length m d s c) →
      ∃ u, ∀ coins, (p.tab m d).out ((p.tab m d).run x coins u).state = some b := by
…

    Mentions: OAI.ExactDerandomization.Word, OAI.ExactDerandomization.Counter.Store, OAI.ExactDerandomization.Counter.CM.rep

  46. theorem OAI.ExactDerandomization.Counter.CM.gives_L line 366
  47. inductive OAI.ExactDerandomization.Counter.Cmd line 406
  48. abbrev OAI.ExactDerandomization.Counter.Cmd.cond line 414
  49. inductive OAI.ExactDerandomization.Counter.Cmd.Run line 417
  50. lemma OAI.ExactDerandomization.Counter.Cmd.Run.fits line 427
  51. lemma OAI.ExactDerandomization.Counter.Cmd.Run.mono line 430
  52. def OAI.ExactDerandomization.Counter.Cmd.Node line 440
  53. instance OAI.ExactDerandomization.Counter.Cmd.(instance at line 446) line 446
  54. def OAI.ExactDerandomization.Counter.Cmd.enter line 449
  55. def OAI.ExactDerandomization.Counter.Cmd.code line 457
  56. lemma OAI.ExactDerandomization.Counter.Cmd.compile line 474
  57. abbrev OAI.ExactDerandomization.Counter.Cmd.States line 514
  58. def OAI.ExactDerandomization.Counter.Cmd.mach line 515
  59. theorem OAI.ExactDerandomization.Counter.Cmd.while_L line 523
  60. abbrev OAI.ExactDerandomization.Counter.High0 line 545
  61. abbrev OAI.ExactDerandomization.Counter.put line 546
  62. lemma OAI.ExactDerandomization.Counter.put_self line 548
  63. lemma OAI.ExactDerandomization.Counter.put_ne line 549
  64. lemma OAI.ExactDerandomization.Counter.put_same line 550
  65. lemma OAI.ExactDerandomization.Counter.put_over line 551
  66. lemma OAI.ExactDerandomization.Counter.put_swap line 553
  67. lemma OAI.ExactDerandomization.Counter.put_fit line 558
  68. lemma OAI.ExactDerandomization.Counter.put_high0 line 560
  69. lemma OAI.ExactDerandomization.Counter.tweak_put line 562
  70. abbrev OAI.ExactDerandomization.Counter.Tr line 565
  71. def OAI.ExactDerandomization.Counter.Room line 571

    Source documentation

    Counter program transformations, correctness with initial certified zeros available FROM threshold l onwards. l is quantified: we can request a program with the scratch moved out to make room. d bounds all counters throughout simultaneously.

    def Room (f : Tr) (l : ℕ) : Prop :=
…

    Mentions: OAI.ExactDerandomization.Counter.Tr

  72. def OAI.ExactDerandomization.Counter.Op line 575
  73. lemma OAI.ExactDerandomization.Counter.fit_mono line 577
  74. lemma OAI.ExactDerandomization.Counter.high_mono line 578
  75. lemma OAI.ExactDerandomization.Counter.self_pow line 580
  76. lemma OAI.ExactDerandomization.Counter.Op.trans line 584
  77. lemma OAI.ExactDerandomization.Counter.Op.hide line 596
  78. lemma OAI.ExactDerandomization.Counter.Op.atom line 607
  79. lemma OAI.ExactDerandomization.Counter.Op.identity line 616
  80. lemma OAI.ExactDerandomization.Counter.Op.inc line 618
  81. lemma OAI.ExactDerandomization.Counter.Op.dec line 619
  82. lemma OAI.ExactDerandomization.Counter.Op.bif line 621
  83. lemma OAI.ExactDerandomization.Counter.Op.loop line 639

    Source documentation

    Iterate transformation while condition true, supplied sequence of finite states proves termination and the two bounds on the trajectory.

    lemma Op.loop {f g : Tr} (i) (t : InputSymbol → Bool) (h : Op f)
    (e : ∃ k, ∀ l, k≤l → ∃ d : ℕ, 0<d ∧ ∀ x a B, x.length+2≤B →
       High0 a l → Fit a B → ∃ (n : ℕ) (r : ℕ → Store),
       r 0=a ∧ (∀ j, j≤n → High0 (r j) l ∧ Fit (r j) (B^d)) ∧
       (∀ j, j<n → Cmd.cond i t x (r j)=true ∧ r (j+1) = f x (r j)) ∧
       Cmd.cond i t x (r n)=false ∧ g x a=r n) :
    Op g := by
…

    Mentions: OAI.ExactDerandomization.Counter.Tr, OAI.ExactDerandomization.InputSymbol, OAI.ExactDerandomization.Counter.Op, OAI.ExactDerandomization.Counter.High0, OAI.ExactDerandomization.Counter.Fit, OAI.ExactDerandomization.Counter.Store, OAI.ExactDerandomization.Counter.Cmd.cond

  84. def OAI.ExactDerandomization.Counter.nz line 665
  85. lemma OAI.ExactDerandomization.Counter.cond_nz line 667
  86. lemma OAI.ExactDerandomization.Counter.Op.zero line 670
  87. lemma OAI.ExactDerandomization.Counter.sum_lt_cube line 681
  88. lemma OAI.ExactDerandomization.Counter.Op.send line 684
  89. lemma OAI.ExactDerandomization.Counter.Op.sendTwo line 703
  90. lemma OAI.ExactDerandomization.Counter.Op.copy line 725
  91. abbrev OAI.ExactDerandomization.Counter.NE line 750
  92. abbrev OAI.ExactDerandomization.Counter.Agree line 752
  93. lemma OAI.ExactDerandomization.Counter.Agree.mono line 753
  94. lemma OAI.ExactDerandomization.Counter.Agree.put line 755
  95. abbrev OAI.ExactDerandomization.Counter.Local line 759
  96. abbrev OAI.ExactDerandomization.Counter.setE line 760
  97. def OAI.ExactDerandomization.Counter.E line 761
  98. lemma OAI.ExactDerandomization.Counter.E.bound line 763
  99. lemma OAI.ExactDerandomization.Counter.E.var line 778
  100. lemma OAI.ExactDerandomization.Counter.E.succ line 780
  101. lemma OAI.ExactDerandomization.Counter.E.pred line 785
  102. lemma OAI.ExactDerandomization.Counter.E.const line 790
  103. lemma OAI.ExactDerandomization.Counter.put_restore line 795
  104. lemma OAI.ExactDerandomization.Counter.E.bif line 799
  105. lemma OAI.ExactDerandomization.Counter.E.ite line 817
  106. lemma OAI.ExactDerandomization.Counter.E.gives_L line 821
  107. lemma OAI.ExactDerandomization.Counter.drive line 831

    Source documentation

    Synthetic state trajectory. Like Op.loop, but allows loop valid just between a setup and teardown block, for one requested room.

    lemma drive {beg step done ans : Tr} (l i : ℕ) (t : InputSymbol → Bool)
    (hg : Op beg) (hf : Op step) (hj : Op done)
    (h : ∃ (u d : ℕ), 0<d ∧ ∀ x a B, x.length+2≤B →
       High0 a l → Fit a B → ∃ (n : ℕ) (r : ℕ → Store),
       r 0=beg x a ∧ (∀ j, j≤n → High0 (r j) u ∧ Fit (r j) (B^d)) ∧
       (∀ j, j<n → Cmd.cond i t x (r j)=true ∧ r (j+1) = step x (r j)) ∧
       Cmd.cond i t x (r n)=false ∧ ans x a=done x (r n) ∧ High0 (ans x a) l) :
    Room ans l := by
…

    Mentions: OAI.ExactDerandomization.Counter.Tr, OAI.ExactDerandomization.InputSymbol, OAI.ExactDerandomization.Counter.Op, OAI.ExactDerandomization.Counter.High0, OAI.ExactDerandomization.Counter.Fit, OAI.ExactDerandomization.Counter.Store, OAI.ExactDerandomization.Counter.Cmd.cond, OAI.ExactDerandomization.Counter.Room

  108. def OAI.ExactDerandomization.Counter.forNat line 879

    Source documentation

    Fold counting up.

    def forNat {α : Type} (f : ℕ → α → α) (z : α) : ℕ → α
  | 0 => z
  | k+1 => f k (forNat f z k)
  109. lemma OAI.ExactDerandomization.Counter.E.iterate line 883
  110. lemma OAI.ExactDerandomization.Counter.E.plus_sum line 989
  111. lemma OAI.ExactDerandomization.Counter.E.addIter line 996
  112. lemma OAI.ExactDerandomization.Counter.E.subIter line 999
  113. lemma OAI.ExactDerandomization.Counter.E.mulIter line 1002
  114. lemma OAI.ExactDerandomization.Counter.E.add line 1007
  115. lemma OAI.ExactDerandomization.Counter.E.sub line 1016
  116. lemma OAI.ExactDerandomization.Counter.E.mul line 1025
  117. lemma OAI.ExactDerandomization.Counter.E.pow_const line 1037
  118. lemma OAI.ExactDerandomization.Counter.E.ite_le line 1042
  119. lemma OAI.ExactDerandomization.Counter.E.ite_lt line 1046
  120. lemma OAI.ExactDerandomization.Counter.E.minE line 1050
  121. lemma OAI.ExactDerandomization.Counter.E.scan_right line 1053
  122. lemma OAI.ExactDerandomization.Counter.E.length line 1057
  123. lemma OAI.ExactDerandomization.Counter.E.ite_eq line 1073
  124. lemma OAI.ExactDerandomization.Counter.E.powStep line 1080
  125. lemma OAI.ExactDerandomization.Counter.E.capPow line 1097
  126. lemma OAI.ExactDerandomization.Counter.E.searchDiv line 1111
  127. lemma OAI.ExactDerandomization.Counter.E.div line 1124
  128. lemma OAI.ExactDerandomization.Counter.E.mod line 1138
  129. def OAI.ExactDerandomization.Counter.Pick line 1155
  130. lemma OAI.ExactDerandomization.Counter.Pick.const line 1158
  131. lemma OAI.ExactDerandomization.Counter.Pick.bind line 1160
  132. lemma OAI.ExactDerandomization.Counter.Pick.map line 1164
  133. lemma OAI.ExactDerandomization.Counter.Pick.ite line 1167
  134. lemma OAI.ExactDerandomization.Counter.Pick.cond line 1174
  135. lemma OAI.ExactDerandomization.Counter.Pick.test_lt line 1182
  136. lemma OAI.ExactDerandomization.Counter.Pick.test_eq line 1189
  137. lemma OAI.ExactDerandomization.Counter.Pick.and line 1196
  138. lemma OAI.ExactDerandomization.Counter.Pick.tuple line 1200
  139. lemma OAI.ExactDerandomization.Counter.Pick.pos line 1215
  140. lemma OAI.ExactDerandomization.Counter.Pick.read line 1229
  141. lemma OAI.ExactDerandomization.Counter.Pick.all line 1243