OAI/Computability/Logspace/ConfigurationGraph.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

Uniform numerical encodings and finite configuration graphs of randomized machines.

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

  1. abbrev OAI.ExactDerandomization.Base.front line 22
  2. def OAI.ExactDerandomization.Base.push line 23
  3. lemma OAI.ExactDerandomization.Base.push_front line 25
  4. lemma OAI.ExactDerandomization.Base.front_push line 27
  5. lemma OAI.ExactDerandomization.Base.div_push line 29
  6. def OAI.ExactDerandomization.Base.bit line 32
  7. lemma OAI.ExactDerandomization.Base.bit_push line 36
  8. lemma OAI.ExactDerandomization.Base.bit_zero line 37
  9. abbrev OAI.ExactDerandomization.Base.Zip line 39
  10. def OAI.ExactDerandomization.Base.Zip.act line 41
  11. def OAI.ExactDerandomization.Base.Zipped line 47

    Source documentation

    Right stack includes current cell.

    def Zipped (w : ℤ → Bool) (z : ℤ) (A : Zip) :=
…

    Mentions: OAI.ExactDerandomization.Base.Zip

  12. lemma OAI.ExactDerandomization.Base.Zipped.read line 51
  13. lemma OAI.ExactDerandomization.Base.upd_ne line 53
  14. lemma OAI.ExactDerandomization.Base.Zipped.move line 56
  15. lemma OAI.ExactDerandomization.Base.trunc_bits line 96
  16. lemma OAI.ExactDerandomization.Base.Zipped.bound line 111
  17. lemma OAI.ExactDerandomization.Base.Zip.unique line 119
  18. structure OAI.ExactDerandomization.Base.R line 143

    Source documentation

    Record of numeric registers (time separate from rest).

    @[ext] structure R (w h : ℕ) where
…
  19. def OAI.ExactDerandomization.Base.R.state line 152
  20. def OAI.ExactDerandomization.Base.R.out line 153
  21. def OAI.ExactDerandomization.Base.R.minput line 155
  22. lemma OAI.ExactDerandomization.Base.R.minput_fin line 160
  23. def OAI.ExactDerandomization.Base.R.action line 165
  24. def OAI.ExactDerandomization.Base.R.step line 171
  25. def OAI.ExactDerandomization.Base.R.start line 178
  26. def OAI.ExactDerandomization.Base.R.runs line 180
  27. structure OAI.ExactDerandomization.Base.R.OK line 185
  28. lemma OAI.ExactDerandomization.Base.R.OK.state line 191
  29. lemma OAI.ExactDerandomization.Base.R.OK.next line 194
  30. lemma OAI.ExactDerandomization.Base.R.runs_OK line 222
  31. lemma OAI.ExactDerandomization.Base.R.runs_out line 233
  32. def OAI.ExactDerandomization.Base.R.radix line 239

    Source documentation

    Work within radix, one chosen polynomial in n. cs: space coefficient, k,e time coefficient/exponent.

    def radix (q cs k e n : ℕ) : ℕ := q+2 + polynomialClock k e n +
…

    Mentions: OAI.ExactDerandomization.polynomialClock

  33. lemma OAI.ExactDerandomization.Base.R.radix_pos line 242
  34. def OAI.ExactDerandomization.Base.R.Small line 244
  35. lemma OAI.ExactDerandomization.Base.R.runs_small line 247
  36. lemma OAI.ExactDerandomization.Base.R.minput_range line 268
  37. abbrev OAI.ExactDerandomization.Base.R.Hint line 273

    Source documentation

    Step source determinable from destination and bounded side information.

    abbrev Hint (q w h : ℕ) := Bool × Fin (q+1) × (Fin h → Fin 3) × (Fin w → Bool)
  38. def OAI.ExactDerandomization.Base.R.hint line 275
  39. lemma OAI.ExactDerandomization.Base.R.step_inj line 278
  40. abbrev OAI.ExactDerandomization.Base.Vec line 310
  41. def OAI.ExactDerandomization.Base.wrap line 312
  42. def OAI.ExactDerandomization.Base.enc line 313
  43. def OAI.ExactDerandomization.Base.dec line 317
  44. def OAI.ExactDerandomization.Base.upper line 321
  45. lemma OAI.ExactDerandomization.Base.wrap_lo line 325
  46. lemma OAI.ExactDerandomization.Base.wrap_hi line 327
  47. lemma OAI.ExactDerandomization.Base.enc_dec line 330
  48. lemma OAI.ExactDerandomization.Base.dec_enc line 336
  49. lemma OAI.ExactDerandomization.Base.upper_le line 345
  50. lemma OAI.ExactDerandomization.Base.wrap_bound line 350
  51. lemma OAI.ExactDerandomization.Base.enc_bound line 354
  52. def OAI.ExactDerandomization.Base.R.id line 365
  53. def OAI.ExactDerandomization.Base.R.recov line 368
  54. lemma OAI.ExactDerandomization.Base.R.id_recov line 377
  55. lemma OAI.ExactDerandomization.Base.R.recov_id line 382
  56. def OAI.ExactDerandomization.Base.R.total line 390
  57. lemma OAI.ExactDerandomization.Base.R.id_lt line 392
  58. lemma OAI.ExactDerandomization.Base.R.recov_mono line 397
  59. structure OAI.ExactDerandomization.Base.Source line 413

    Source documentation

    Source machines with supplied polynomial clock parameters (need not be positive for building the graph) and controller space coefficient. Semantics will justify these externally.

    structure Source (q w h : ℕ) where
…
  60. def OAI.ExactDerandomization.Base.Source.clock line 422
  61. def OAI.ExactDerandomization.Base.Source.mrad line 423
  62. def OAI.ExactDerandomization.Base.Source.size line 424
  63. def OAI.ExactDerandomization.Base.Source.dom line 425
  64. def OAI.ExactDerandomization.Base.Source.row line 427
  65. def OAI.ExactDerandomization.Base.Source.ident line 428
  66. def OAI.ExactDerandomization.Base.Source.first line 429
  67. instance OAI.ExactDerandomization.Base.Source.decSmall line 431
  68. def OAI.ExactDerandomization.Base.Source.legal line 433
  69. instance OAI.ExactDerandomization.Base.Source.decLegal line 434
  70. def OAI.ExactDerandomization.Base.Source.fin line 437
  71. def OAI.ExactDerandomization.Base.Source.next line 441
  72. def OAI.ExactDerandomization.Base.Source.reward line 447
  73. def OAI.ExactDerandomization.Base.Source.edge line 449
  74. def OAI.ExactDerandomization.Base.Source.S line 452
  75. lemma OAI.ExactDerandomization.Base.Source.steps_to line 454
  76. lemma OAI.ExactDerandomization.Base.Source.mem line 464
  77. lemma OAI.ExactDerandomization.Base.Source.forward line 468
  78. lemma OAI.ExactDerandomization.Base.Source.S_nonneg line 474
  79. lemma OAI.ExactDerandomization.Base.Source.S_le line 475
  80. lemma OAI.ExactDerandomization.Base.Source.S_pos line 477
  81. def OAI.ExactDerandomization.Base.Source.payoff line 481
  82. def OAI.ExactDerandomization.Base.Source.avg line 482
  83. lemma OAI.ExactDerandomization.Base.Source.avg_S line 486
  84. lemma OAI.ExactDerandomization.Base.Source.S_sub line 497
  85. lemma OAI.ExactDerandomization.Base.Source.dead line 503
  86. lemma OAI.ExactDerandomization.Base.Source.out_degree line 507
  87. lemma OAI.ExactDerandomization.Base.Source.in_degree line 518
  88. def OAI.ExactDerandomization.Base.Source.potential line 538

    Source documentation

    potential via bounded recursion.

    def potential (x : Word) : ℕ → ℕ → ℚ
 | 0 => P.reward x
 | k+1 => fun n=> P.reward x n + P.avg x n (potential x k)

    Mentions: OAI.ExactDerandomization.Word

  89. lemma OAI.ExactDerandomization.Base.Source.bounded line 542
  90. lemma OAI.ExactDerandomization.Base.Source.stable line 557
  91. def OAI.ExactDerandomization.Base.Source.pr line 577
  92. lemma OAI.ExactDerandomization.Base.Source.pr_eq line 579
  93. abbrev OAI.ExactDerandomization.Base.Source.Space line 582
  94. def OAI.ExactDerandomization.Base.Source.walker line 584
  95. lemma OAI.ExactDerandomization.Base.Source.visited line 586
  96. lemma OAI.ExactDerandomization.Base.Source.mem_first line 593
  97. lemma OAI.ExactDerandomization.Base.Source.step_true line 598
  98. lemma OAI.ExactDerandomization.Base.Source.pr_end line 607
  99. lemma OAI.ExactDerandomization.Base.Source.same line 614
  100. abbrev OAI.ExactDerandomization.Base.Source.Tapes line 622
  101. def OAI.ExactDerandomization.Base.Source.Toggle line 624
  102. lemma OAI.ExactDerandomization.Base.Source.fair line 629
  103. lemma OAI.ExactDerandomization.Base.enc_E line 699
  104. lemma OAI.ExactDerandomization.Base.dec_E line 706
  105. lemma OAI.ExactDerandomization.Base.PickAND line 717
  106. lemma OAI.ExactDerandomization.Base.front_E line 722
  107. lemma OAI.ExactDerandomization.Base.push_E line 725
  108. structure OAI.ExactDerandomization.Base.RE line 731
  109. lemma OAI.ExactDerandomization.Base.RE.code line 742
  110. lemma OAI.ExactDerandomization.Base.RE.recover line 746
  111. lemma OAI.ExactDerandomization.Base.RE.small line 753
  112. lemma OAI.ExactDerandomization.Base.RE.stPick line 760
  113. lemma OAI.ExactDerandomization.Base.RE.choose line 763
  114. lemma OAI.ExactDerandomization.Base.RE.step line 776
  115. lemma OAI.ExactDerandomization.Base.Source.eClock line 809
  116. lemma OAI.ExactDerandomization.Base.Source.eRad line 812
  117. lemma OAI.ExactDerandomization.Base.Source.eSize line 816
  118. lemma OAI.ExactDerandomization.Base.Source.eFirst line 819
  119. lemma OAI.ExactDerandomization.Base.Source.eLegal line 823
  120. lemma OAI.ExactDerandomization.Base.Source.eReward line 827
  121. lemma OAI.ExactDerandomization.Base.Source.eWeight line 833