OAI/Computability/FiniteCompiler/SelfReference.lean

GitHub source file

168 declarations, 0 contain sorry, 0 declared as axioms

Controlled shorter-input evaluator calls, fixed points, totality, and tested-class realization.

  1. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.left line 13
  2. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.right line 15
  3. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.left_append line 18
  4. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.right_append line 19
  5. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.left_length line 20
  6. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.right_length line 21
  7. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.primrec_left line 24
  8. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Projection.primrec_right line 29
  9. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.X line 45
  10. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.Y line 46
  11. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.Class line 47
  12. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.combine line 49
  13. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.primrec_combine line 53
  14. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.family line 63

    Source documentation

    The literal tested class from the self-reference construction: zero precisely for the compiler zero output, and otherwise the compiler word together with a canonical, decidable coding of the actual auxiliary partial affine map.

    noncomputable def family (f : ℕ × List T → Part (List T)) (n : ℕ) (w : List (Y T Γ Q)) :
    Part (Option (Class T Γ Q)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.Y, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.Class

  15. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.partrec_family line 68
  16. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.letters line 78
  17. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.primrec_letters line 83
  18. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Tested.family_mem line 88
  19. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tail line 101
  20. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.encode line 104
  21. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tail_length line 107
  22. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.code_length line 113
  23. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.localCode line 124

    Source documentation

    A genuine block code on any finite alphabet injected into the displayed support. No choice of an enumeration at the parameter is used.

    def localCode [DecidableEq S] (b a c : S) (hba : b≠a) (hbc : b≠c) (hac : a≠c)
    (ls : List A) (i : B → A) (hi : Function.Injective i) (hm : ∀ x,i x∈ls) : BlockCode B S where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode

  24. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.localCode_encode line 139
  25. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_tail line 146
  26. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_encode line 153
  27. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.pickStep line 163
  28. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.pick line 167
  29. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.output line 170
  30. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.table line 174
  31. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute line 179
  32. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_pickStep line 191
  33. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_pick line 201
  34. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_output line 210
  35. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.primrec_table line 220
  36. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.partrec_compute line 233
  37. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute_specialize line 246
  38. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.bases line 264
  39. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tables line 272
  40. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.partrec_bases line 292
  41. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.partrec_tables line 308
  42. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tables_specialize line 317
  43. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.words line 332

    Source documentation

    Binary tails in their literal lexicographic order, with a before c.

    def words (a c : S) : ℕ → List (List S)
  | 0 => [[]]
  | n+1 => (words a c n).map (a::·) ++ (words a c n).map (c::·)
  44. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.length_words line 336
  45. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.mem_length line 341
  46. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.mem_letters line 348
  47. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.nodup line 361
  48. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.ordered line 373
  49. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.tail line 388
  50. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.encode line 391
  51. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.index_bound line 394
  52. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.code line 401
  53. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.code_encode line 426
  54. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.code_order line 434
  55. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.primrec_words line 449
  56. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.primrec_tail line 455
  57. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.primrec_encode line 459
  58. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.word line 469
  59. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.less line 471
  60. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.lex_map_iff line 475
  61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.shortlex_map_iff line 483
  62. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.index_injective line 487
  63. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.less_map line 492
  64. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.primrec_word line 501
  65. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Rank.primrec_less line 504
  66. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.restrict line 519

    Source documentation

    Forget the parameter delimiter as an input/output letter. Work symbols and transitions are not changed.

    def restrict (A : Alphabet (S ⊕ Unit) Γ) : Alphabet S Γ where
…
  67. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.restrict_decode line 527
  68. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.restrict_content line 537
  69. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.restrict_realizes line 543
  70. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.letters line 560
  71. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.parameter line 563
  72. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.letters_input line 566
  73. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.parameter_input line 570
  74. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.primrec_letters line 576
  75. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.primrec_parameter line 582
  76. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.universal line 589
  77. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.universal_input line 593
  78. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.partrec_universal line 598
  79. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.exists_parameter_machine line 606

    Source documentation

    The alphabet and all non-initializer control are now fixed once for the whole partial-recursive family. The only variable finite control is the explicit unary counter Fin (n+2), not a choice of an evaluator for each index.

    theorem exists_parameter_machine {S : Type} [Fintype S] [Primcodable S]
    {f : ℕ → List S → Part (List S)} (hf : Partrec₂ f) :
    ∃ (Γ Q : Type) (_ : Fintype Γ) (_ : Fintype Q) (_ : DecidableEq Γ)
      (A : Alphabet (S ⊕ Unit) Γ) (M : Machine Q Γ),
      (∀ g a, A.output g=some a → g=A.input a) ∧
      ∀ n, Compiler.Word.Realizes (restrict (alphabet A)) (machine A M (.inr ()) n) (f n) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Realizes, OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniversalMachine.restrict

  80. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Sigma line 627
  81. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.markers line 629
  82. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.raw line 631
  83. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.raw_encode line 634
  84. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.partrec_raw line 638
  85. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Y line 649
  86. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.Z line 650
  87. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.yLetters line 652
  88. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.zLetters line 653
  89. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.width line 656

    Source documentation

    A single common width, chosen effectively only from finite alphabets.

    noncomputable def width (k n : ℕ) : ℕ :=
…
  90. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeT line 659
  91. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeG line 661
  92. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.testT line 664
  93. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.testG line 668
  94. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables line 671
  95. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.primrec_width line 677
  96. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.primrec_codeT line 682
  97. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.primrec_codeG line 688
  98. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.partrec_testT line 692
  99. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.partrec_tables line 695
  100. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.exists_fixed_point line 709

    Source documentation

    Literal source fixed point. No termination or contextual correctness is assumed: equality here also preserves divergence of the two procedures.

     theorem exists_fixed_point (h : ComputablePred (fun w : FiniteAlgebraicEnvelopes.Word k => FiniteAlgebraicEnvelopes.evalWord s w=1)) :
    ∃ n,raw n=tableNormal (tables s A M n) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.raw, OAI.FiniteAlgebraicEnvelopes.Bootstrap.tableNormal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables

  101. theorem OAI.FiniteAlgebraicEnvelopes.Effect.traverse_map_output line 722
  102. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.answerMap line 736
  103. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.pickStep_map line 741
  104. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.pick_map line 747
  105. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.output_map line 756
  106. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.table_map line 762
  107. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute_map line 772
  108. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.pick_eq_canonical line 794
  109. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.output_full_support line 807
  110. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.table_full_support line 821
  111. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute_full_support line 841
  112. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute_domain_support line 852
  113. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.compute_members_support line 864
  114. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.RulesEq line 878
  115. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_rulesEq line 880
  116. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.critical_rulesEq line 887
  117. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.allowed_rulesEq line 893
  118. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.choose_rulesEq line 898
  119. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Selectors.process_rulesEq line 906
  120. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.fullTables line 926
  121. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tables_members_support line 932
  122. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.tables_domain_support line 947
  123. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.stable_support line 960
  124. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Uniform.good_support line 973
  125. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.FiniteY line 1002
  126. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.includeY line 1004
  127. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.includeY_injective line 1014
  128. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.includeY_mem line 1018
  129. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.mem_includeY_range line 1028
  130. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.list_preimage line 1037
  131. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteLetters line 1046
  132. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.map_finiteLetters line 1050
  133. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.mem_finiteLetters line 1054
  134. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rankT line 1060
  135. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rankG line 1061
  136. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rankT_injective line 1064
  137. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rankG_injective line 1066
  138. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.relT line 1069
  139. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.relG line 1070
  140. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.wf_relT line 1073
  141. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.wf_relG line 1074
  142. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tri_relT line 1076
  143. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tri_relG line 1078
  144. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.dec_relT line 1080
  145. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.dec_relG line 1081
  146. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.dec_shortlexT line 1083
  147. instance OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.dec_shortlexG line 1084
  148. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.widthBoundT line 1087
  149. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.widthBoundG line 1092
  150. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteCodeT line 1097
  151. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteCodeG line 1100
  152. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteCodeT_encode line 1105
  153. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteCodeG_encode line 1109
  154. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.lessT_map line 1115
  155. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.lessG_eq line 1122
  156. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.LexBinary.alphabet_bound line 1136
  157. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteTest line 1163
  158. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.finiteTables line 1165
  159. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tables_eq_finite line 1170
  160. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.stable line 1185
  161. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeT_order line 1193
  162. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeG_order line 1197
  163. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeT_alphabet line 1202
  164. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeG_alphabet line 1206
  165. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeT_avoid line 1211
  166. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codeG_avoid line 1218
  167. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.codes_disjoint line 1225
  168. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.good_of_tests line 1233