OAI/Computability/Logspace/RecursivePrograms.lean

GitHub source file

211 declarations, 0 contain sorry, 0 declared as axioms

Measured stack encodings and the realization of recursive programs with simultaneous space bounds.

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

  1. def OAI.ExactDerandomization.Relay.lb line 20
  2. lemma OAI.ExactDerandomization.Relay.lb_pos line 22
  3. lemma OAI.ExactDerandomization.Relay.lb_zero line 23
  4. lemma OAI.ExactDerandomization.Relay.lb_one line 24
  5. lemma OAI.ExactDerandomization.Relay.below line 25
  6. lemma OAI.ExactDerandomization.Relay.above line 26
  7. lemma OAI.ExactDerandomization.Relay.modest line 30
  8. lemma OAI.ExactDerandomization.Relay.growing line 38
  9. lemma OAI.ExactDerandomization.Relay.lb_le_inc line 42
  10. lemma OAI.ExactDerandomization.Relay.lb_mono line 44
  11. lemma OAI.ExactDerandomization.Relay.lb_succ line 46
  12. lemma OAI.ExactDerandomization.Relay.lb_plus line 48
  13. lemma OAI.ExactDerandomization.Relay.lb_times line 53
  14. lemma OAI.ExactDerandomization.Relay.lb_shift line 56
  15. def OAI.ExactDerandomization.Relay.cord line 64
  16. lemma OAI.ExactDerandomization.Relay.cord_bounds line 66
  17. lemma OAI.ExactDerandomization.Relay.lb_cord line 86
  18. lemma OAI.ExactDerandomization.Relay.cord_fine line 97
  19. def OAI.ExactDerandomization.Relay.discover line 105
  20. def OAI.ExactDerandomization.Relay.pierce line 108
  21. def OAI.ExactDerandomization.Relay.wing line 109
  22. def OAI.ExactDerandomization.Relay.middle line 110
  23. def OAI.ExactDerandomization.Relay.fore line 111
  24. def OAI.ExactDerandomization.Relay.aft line 112
  25. lemma OAI.ExactDerandomization.Relay.pierce_rule line 114
  26. lemma OAI.ExactDerandomization.Relay.wing_cord line 152
  27. lemma OAI.ExactDerandomization.Relay.middle_cord line 158
  28. lemma OAI.ExactDerandomization.Relay.fore_cord line 165
  29. lemma OAI.ExactDerandomization.Relay.aft_cord line 166
  30. def OAI.ExactDerandomization.Relay.bead line 170
  31. def OAI.ExactDerandomization.Relay.heed line 171
  32. def OAI.ExactDerandomization.Relay.readt line 172
  33. lemma OAI.ExactDerandomization.Relay.heed_eq line 174
  34. lemma OAI.ExactDerandomization.Relay.read_eq line 175
  35. lemma OAI.ExactDerandomization.Relay.bead_small line 177
  36. def OAI.ExactDerandomization.Relay.hunt line 190
  37. lemma OAI.ExactDerandomization.Relay.under_pow line 192
  38. lemma OAI.ExactDerandomization.Relay.found line 210
  39. lemma OAI.ExactDerandomization.Relay.run_huntE line 224

    Source documentation

    E calculation of a "current or small index" loop

    lemma run_huntE (f : NE) (p : ℕ→ℕ→Prop) [(x y : ℕ) → Decidable (p x y)]
    (hp : ∀ {g j:NE}, E g → E j → Counter.Pick (fun x a => decide (p (g x a) (j x a))))
    (h : E f) :
    E (fun x a => forNat
         (fun j v=> if p (f x a) j then j+1 else v) 0 (f x a)) := by
…

    Mentions: OAI.ExactDerandomization.Counter.Pick

  40. lemma OAI.ExactDerandomization.Relay.log2E line 243
  41. lemma OAI.ExactDerandomization.Relay.lbE line 256
  42. lemma OAI.ExactDerandomization.Relay.digitsE line 257
  43. lemma OAI.ExactDerandomization.Relay.cordE line 265
  44. lemma OAI.ExactDerandomization.Relay.pierceE line 269
  45. lemma OAI.ExactDerandomization.Relay.wingE line 273
  46. lemma OAI.ExactDerandomization.Relay.middleE line 275
  47. lemma OAI.ExactDerandomization.Relay.foreE line 276
  48. lemma OAI.ExactDerandomization.Relay.aftE line 277
  49. def OAI.ExactDerandomization.Relay.Uni line 279
  50. class OAI.ExactDerandomization.Relay.Wire line 281
  51. abbrev OAI.ExactDerandomization.Relay.measure line 289
  52. instance OAI.ExactDerandomization.Relay.(instance at line 291) line 291
  53. lemma OAI.ExactDerandomization.Relay.enc_nat line 292
  54. instance OAI.ExactDerandomization.Relay.(instance at line 294) line 294
  55. instance OAI.ExactDerandomization.Relay.(instance at line 304) line 304
  56. lemma OAI.ExactDerandomization.Relay.dec_round line 313
  57. lemma OAI.ExactDerandomization.Relay.measure_pair line 314
  58. abbrev OAI.ExactDerandomization.Relay.PT line 318

    Source documentation

    Pointwise semantic LF functions requiring only wire encodings.

    abbrev PT (α β : Type) := Word→α→β

    Mentions: OAI.ExactDerandomization.Word

  59. def OAI.ExactDerandomization.Relay.Kn line 320
  60. lemma OAI.ExactDerandomization.Relay.Kn.identity line 325
  61. lemma OAI.ExactDerandomization.Relay.Kn.comp line 327
  62. lemma OAI.ExactDerandomization.Relay.Kn.tuple line 331
  63. lemma OAI.ExactDerandomization.Relay.Kn.first line 335
  64. lemma OAI.ExactDerandomization.Relay.Kn.next line 338
  65. lemma OAI.ExactDerandomization.Relay.Kn.left line 341
  66. lemma OAI.ExactDerandomization.Relay.Kn.right line 342
  67. lemma OAI.ExactDerandomization.Relay.Kn.wash line 343
  68. lemma OAI.ExactDerandomization.Relay.Kn.unpack line 344
  69. lemma OAI.ExactDerandomization.Relay.Kn.fix line 345
  70. lemma OAI.ExactDerandomization.Relay.Kn.word line 346
  71. lemma OAI.ExactDerandomization.Relay.Kn.add line 351
  72. lemma OAI.ExactDerandomization.Relay.Kn.sub line 352
  73. lemma OAI.ExactDerandomization.Relay.Kn.times line 353
  74. lemma OAI.ExactDerandomization.Relay.Kn.div line 354
  75. lemma OAI.ExactDerandomization.Relay.Kn.mod line 355
  76. lemma OAI.ExactDerandomization.Relay.Kn.power line 356
  77. lemma OAI.ExactDerandomization.Relay.Kn.succ line 357
  78. lemma OAI.ExactDerandomization.Relay.Kn.pred line 358
  79. lemma OAI.ExactDerandomization.Relay.Kn.cond line 360
  80. lemma OAI.ExactDerandomization.Relay.Kn.le line 366
  81. lemma OAI.ExactDerandomization.Relay.Kn.lt line 370
  82. lemma OAI.ExactDerandomization.Relay.Kn.eq line 372
  83. lemma OAI.ExactDerandomization.Relay.Kn.cond_le line 376
  84. lemma OAI.ExactDerandomization.Relay.Kn.cond_lt line 379
  85. lemma OAI.ExactDerandomization.Relay.Kn.cond_eq line 382
  86. lemma OAI.ExactDerandomization.Relay.Kn.cap line 385
  87. lemma OAI.ExactDerandomization.Relay.Kn.small line 388
  88. lemma OAI.ExactDerandomization.Relay.Kn.bl line 390
  89. lemma OAI.ExactDerandomization.Relay.Kn.push line 392
  90. lemma OAI.ExactDerandomization.Relay.Kn.top line 394
  91. lemma OAI.ExactDerandomization.Relay.Kn.tail line 396
  92. lemma OAI.ExactDerandomization.Relay.Kn.stroll line 400

    Source documentation

    LF state loops with a uniform numeric ceiling given by another LF expression

    lemma stroll (step : PT (α×ℕ×ℕ) ℕ)
    (n z limit : PT α ℕ)
    (h : Kn step) (hn:Kn n) (hz:Kn z) (he:Kn limit)
    (hp : ∀ x a,∀ j≤ n x a, forNat (fun k v=>step x (a,k,v)) (z x a) j ≤ limit x a) :
    Kn (fun x a=> forNat (fun k v=> step x (a,k,v)) (z x a) (n x a)) := by
…

    Mentions: OAI.ExactDerandomization.Relay.PT, OAI.ExactDerandomization.Relay.Kn

  93. lemma OAI.ExactDerandomization.Relay.cord_mono line 428
  94. lemma OAI.ExactDerandomization.Relay.bead_mono line 431
  95. lemma OAI.ExactDerandomization.Relay.pair_mono line 432
  96. lemma OAI.ExactDerandomization.Relay.Kn.fold line 434
  97. def OAI.ExactDerandomization.Relay.mesh line 449
  98. lemma OAI.ExactDerandomization.Relay.mesh_length line 452
  99. lemma OAI.ExactDerandomization.Relay.mesh_pos line 456
  100. lemma OAI.ExactDerandomization.Relay.measure_mesh line 457
  101. lemma OAI.ExactDerandomization.Relay.mesh_append line 460
  102. lemma OAI.ExactDerandomization.Relay.mesh_reverse line 466
  103. def OAI.ExactDerandomization.Relay.ebb line 475
  104. def OAI.ExactDerandomization.Relay.sweep line 477
  105. lemma OAI.ExactDerandomization.Relay.Kn.sweepK line 482
  106. inductive OAI.ExactDerandomization.Relay.Scan line 506
  107. lemma OAI.ExactDerandomization.Relay.Scan.start line 509
  108. lemma OAI.ExactDerandomization.Relay.forNat_cons line 511
  109. lemma OAI.ExactDerandomization.Relay.exact_ebb line 519
  110. lemma OAI.ExactDerandomization.Relay.exact_sweep line 544
  111. def OAI.ExactDerandomization.Relay.caplen line 551
  112. def OAI.ExactDerandomization.Relay.windback line 552
  113. lemma OAI.ExactDerandomization.Relay.Kn.caplenK line 556
  114. lemma OAI.ExactDerandomization.Relay.Kn.windbackK line 557
  115. lemma OAI.ExactDerandomization.Relay.backscan line 560
  116. lemma OAI.ExactDerandomization.Relay.windback_mesh line 582
  117. structure OAI.ExactDerandomization.Relay.Cub line 602
  118. abbrev OAI.ExactDerandomization.Relay.Site line 606
  119. abbrev OAI.ExactDerandomization.Relay.Plot line 607
  120. abbrev OAI.ExactDerandomization.Relay.Slip line 608
  121. abbrev OAI.ExactDerandomization.Relay.Drain line 609
  122. abbrev OAI.ExactDerandomization.Relay.Flag line 610
  123. inductive OAI.ExactDerandomization.Relay.Cog line 612
  124. structure OAI.ExactDerandomization.Relay.Fare line 619
  125. def OAI.ExactDerandomization.Relay.Fare.atm line 622
  126. def OAI.ExactDerandomization.Relay.Fare.pull line 625
  127. inductive OAI.ExactDerandomization.Relay.Boots line 627
  128. lemma OAI.ExactDerandomization.Relay.Boots.fits line 648
  129. inductive OAI.ExactDerandomization.Relay.Act line 651
  130. structure OAI.ExactDerandomization.Relay.Grid line 657
  131. inductive OAI.ExactDerandomization.Relay.Grid.Route line 670

    Source documentation

    routes represent synchronous, hence restoring-program-frame execution. (They need not be cursor-restoring.)

    inductive Route (r:Grid) (x:Word) (F:Fare) : ℕ→ℕ→Site→ℕ→Site→Prop
   | edit {q i a j b f} : r.prog i=.edit f j → f.f x (q,a)=b →
          i≤r.slot → j≤r.slot → F.atm q a → F.atm q b → Route r x F q i a j b
   | toss {q i a j b q' a' p e} : r.prog i=.toss p e j →
          p.f x (q,a.1)=q' → e.f x ((q,a.1),a')=b →
          i≤r.slot → j≤r.slot → F.atm q a → F.atm q b → F.pull q a.1 q' →
          Route r x F q' r.entry (0,a.2) 0 a' →
          Route r x F q i a j b
   | fork {q i a j f s t} : r.prog i=.fork f s t → (if f.f x (q,a) then s else t)=j →
          i≤r.slot → j≤r.slot → F.atm q a → Route r x F q i a j a
   | seq {q i a j b l c} : Route r x F q i a j b → Route r x F q j b l c → Route r x F q i a l c

    Mentions: OAI.ExactDerandomization.Relay.Grid, OAI.ExactDerandomization.Word, OAI.ExactDerandomization.Relay.Fare, OAI.ExactDerandomization.Relay.Site

  132. lemma OAI.ExactDerandomization.Relay.Grid.Route.fits line 681
  133. def OAI.ExactDerandomization.Relay.Cog.Body line 688
  134. instance OAI.ExactDerandomization.Relay.Cog.(instance at line 693) line 693
  135. def OAI.ExactDerandomization.Relay.Cog.first line 696
  136. def OAI.ExactDerandomization.Relay.Cog.code line 701
  137. lemma OAI.ExactDerandomization.Relay.Cog.lays line 712
  138. lemma OAI.ExactDerandomization.Relay.Cog.room line 738
  139. abbrev OAI.ExactDerandomization.Relay.Grid.Motor line 769
  140. abbrev OAI.ExactDerandomization.Relay.Grid.Hood line 770
  141. abbrev OAI.ExactDerandomization.Relay.Grid.Carrier line 771
  142. def OAI.ExactDerandomization.Relay.Grid.fame line 774

    Source documentation

    which query was invoked from this instruction

    def fame (x:Word) (a q:ℕ) : ℕ :=
…

    Mentions: OAI.ExactDerandomization.Word

  143. def OAI.ExactDerandomization.Relay.Grid.replay line 780
  144. lemma OAI.ExactDerandomization.Relay.Grid.numerous line 786

    Source documentation

    finite branch selection

    lemma numerous {α β : Type} [Wire α] [Wire β] (f: Act→ PT α β)
   (h:∀ p,Kn (f p)) (n:PT α ℕ) (hn:Kn n) :
    Kn (fun x a=> f (r.prog (n x a)) x a) := by
…

    Mentions: OAI.ExactDerandomization.Relay.Wire, OAI.ExactDerandomization.Relay.Act, OAI.ExactDerandomization.Relay.PT, OAI.ExactDerandomization.Relay.Kn

  145. lemma OAI.ExactDerandomization.Relay.Grid.fameK line 804
  146. lemma OAI.ExactDerandomization.Relay.Grid.replayK line 813
  147. def OAI.ExactDerandomization.Relay.Grid.advance line 817
  148. def OAI.ExactDerandomization.Relay.Grid.recede line 826
  149. def OAI.ExactDerandomization.Relay.Grid.roll line 832
  150. lemma OAI.ExactDerandomization.Relay.Grid.rollK line 838
  151. lemma OAI.ExactDerandomization.Relay.Grid.Scan.snatch line 866
  152. lemma OAI.ExactDerandomization.Relay.Grid.replay_s line 872
  153. lemma OAI.ExactDerandomization.Relay.Grid.parked line 876
  154. inductive OAI.ExactDerandomization.Relay.WPath line 888

    Source documentation

    bounded transitive closure

    inductive WPath {α} (safe:α→Prop) (g:α→α) : α→α→Prop
   | start {x} (h:safe x) : WPath safe g x x
   | next {x y z} : safe x → g x=y → WPath safe g y z → WPath safe g x z
  155. lemma OAI.ExactDerandomization.Relay.WPath.seq line 891
  156. def OAI.ExactDerandomization.Relay.Grid.elbow line 897
  157. lemma OAI.ExactDerandomization.Relay.Grid.elbow_hi line 898
  158. def OAI.ExactDerandomization.Relay.Grid.rooms line 899
  159. abbrev OAI.ExactDerandomization.Relay.Grid.fitsM line 900
  160. lemma OAI.ExactDerandomization.Relay.Grid.seats line 902
  161. lemma OAI.ExactDerandomization.Relay.Grid.extends_by line 929
  162. theorem OAI.ExactDerandomization.Relay.Grid.journey line 941
  163. abbrev OAI.ExactDerandomization.Relay.hitloop line 983
  164. lemma OAI.ExactDerandomization.Relay.conserve line 985
  165. lemma OAI.ExactDerandomization.Relay.forever line 989
  166. lemma OAI.ExactDerandomization.Relay.quick line 992
  167. lemma OAI.ExactDerandomization.Relay.WPath.clipIter line 1022
  168. abbrev OAI.ExactDerandomization.Relay.Grid.Job line 1033
  169. def OAI.ExactDerandomization.Relay.Grid.run line 1034
  170. lemma OAI.ExactDerandomization.Relay.Grid.runK line 1041
  171. lemma OAI.ExactDerandomization.Relay.Grid.actual line 1054
  172. theorem OAI.ExactDerandomization.Relay.realization line 1075

    Source documentation

    Compilation of simultaneous stack certificates. Partial logspace function extension on all certified executions.

    theorem realization (main:Cog) : ∃ f : PT Grid.Job Site, Kn f ∧ ∀ {x U F q a b},
   2^(F.meter q) ≤ U → F.limit ≤ U → Boots x F main q main a b →
    f x ((U,q),a)=b := by
…

    Mentions: OAI.ExactDerandomization.Relay.Cog, OAI.ExactDerandomization.Relay.PT, OAI.ExactDerandomization.Relay.Grid.Job, OAI.ExactDerandomization.Relay.Site, OAI.ExactDerandomization.Relay.Kn, OAI.ExactDerandomization.Relay.Boots

  173. lemma OAI.ExactDerandomization.Relay.Boots.same line 1081
  174. abbrev OAI.ExactDerandomization.Relay.span line 1100
  175. abbrev OAI.ExactDerandomization.Relay.charge line 1101
  176. lemma OAI.ExactDerandomization.Relay.movespan line 1102
  177. lemma OAI.ExactDerandomization.Relay.leaner line 1105
  178. lemma OAI.ExactDerandomization.Relay.acock line 1108
  179. lemma OAI.ExactDerandomization.Relay.lax line 1112
  180. lemma OAI.ExactDerandomization.Relay.span_mono line 1122
  181. structure OAI.ExactDerandomization.Relay.Level line 1127
  182. structure OAI.ExactDerandomization.Relay.Lot line 1132

    Source documentation

    fixed syntactic play, prices ignored until the enclosing layer is ready.

    structure Lot where
…
  183. def OAI.ExactDerandomization.Relay.Lot.state line 1140
  184. def OAI.ExactDerandomization.Relay.Lot.jump line 1142
  185. inductive OAI.ExactDerandomization.Relay.Lot.Mane line 1148

    Source documentation

    The clock argument is in b. q is the immutable tuple seen by the inline recipe (may be virtual, i.e. regenerated via an inline frame).

    inductive Mane (l:Lot) (c : ℕ) (b : Level) (d : ℕ) (q : ℕ) : Cog→Site→Site→Prop
   | edit {p h j} : p.f l.x (q,h)=j → l.state c b h → l.state c b j →
         Mane l c b d q (.edit p) h j
   | toss {p e a a' u q'} :
       p.f l.x (q,a.1)=q' → e.f l.x ((q,a.1),a')=u →
       l.state c b a → l.state c b u → l.jump c b d a.1 q' →
       Boots l.x l.F l.P q' l.P (0,a.2) a' →
       Mane l c b d q (.toss p e) a u
   | seq {p s a y u} : Mane l c b d q p a y → Mane l c b d q s y u →
       Mane l c b d q (.seq p s) a u
   | yes {s u p a y} : s.f l.x (q,a)=true → Mane l c b d q p a y →
       Mane l c b d q (.bif s p u) a y
…

    Mentions: OAI.ExactDerandomization.Relay.Lot, OAI.ExactDerandomization.Relay.Level, OAI.ExactDerandomization.Relay.Cog, OAI.ExactDerandomization.Relay.Site, OAI.ExactDerandomization.Relay.Boots

  186. lemma OAI.ExactDerandomization.Relay.Lot.Mane.spots line 1166
  187. lemma OAI.ExactDerandomization.Relay.Lot.Mane.mono line 1169
  188. theorem OAI.ExactDerandomization.Relay.Lot.Mane.issue line 1184
  189. def OAI.ExactDerandomization.Relay.hold line 1208
  190. def OAI.ExactDerandomization.Relay.mark line 1209
  191. def OAI.ExactDerandomization.Relay.unseat line 1210
  192. lemma OAI.ExactDerandomization.Relay.marked line 1212
  193. lemma OAI.ExactDerandomization.Relay.unseats0 line 1213
  194. lemma OAI.ExactDerandomization.Relay.holdcap line 1214
  195. def OAI.ExactDerandomization.Relay.Cog.locate line 1227
  196. lemma OAI.ExactDerandomization.Relay.Cog.location line 1229
  197. lemma OAI.ExactDerandomization.Relay.Cog.binds line 1234
  198. theorem OAI.ExactDerandomization.Relay.Cog.markK line 1237
  199. theorem OAI.ExactDerandomization.Relay.Cog.unseatK line 1239
  200. def OAI.ExactDerandomization.Relay.Cog.guard0 line 1242
  201. def OAI.ExactDerandomization.Relay.Cog.focus line 1245

    Source documentation

    Inlining carries an inner tuple regenerated from q and the piece o.

    def focus (v:Cog) : Cog :=
…

    Mentions: OAI.ExactDerandomization.Relay.Cog

  202. lemma OAI.ExactDerandomization.Relay.Cog.hitmark line 1260
  203. lemma OAI.ExactDerandomization.Relay.Cog.focus_word line 1263
  204. abbrev OAI.ExactDerandomization.Relay.Lore line 1299
  205. abbrev OAI.ExactDerandomization.Relay.Pause line 1300
  206. def OAI.ExactDerandomization.Relay.topNote line 1302
  207. def OAI.ExactDerandomization.Relay.etch line 1305
  208. def OAI.ExactDerandomization.Relay.gear line 1306
  209. lemma OAI.ExactDerandomization.Relay.gear_at line 1309
  210. lemma OAI.ExactDerandomization.Relay.etches line 1311
  211. lemma OAI.ExactDerandomization.Relay.Kn.bneg line 1316