OAI/Computability/FiniteCompiler/Surface.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Surface alphabet, preprocessing, and grading estimates.

  1. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Head line 15

    Source documentation

    The complete head alphabet; internal control excludes raw, quota and cleanup.

    inductive Head (H : Type*)
  | raw | pending | cleanup
  | internal : H → Head H
  deriving DecidableEq, Fintype

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.raw

  2. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector line 20
  3. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells line 22
  4. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.RawStep line 25

    Source documentation

    Literal clean-anchor slides, oriented to the leftmost reachable head gap.

    inductive RawStep (blank : Γ) : Sector S Γ H → Sector S Γ H → Prop
  | slide (a : S) (l r : Cells S Γ) (lb rb : Bool) :
      RawStep blank ⟨Validator.cell blank (.anchor a)::l,.raw,r,lb,rb⟩
        ⟨l,.raw,Validator.cell blank (.anchor a)::r,lb,rb⟩

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.raw

  5. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawStep_deterministic line 30
  6. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.grade line 34
  7. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawStep_grade line 38
  8. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawStep_skeleton line 44
  9. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep line 51
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep_reaches line 58
  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep_terminal line 75
  12. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal line 92
  13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_reaches line 97
  14. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_terminal line 103
  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_invariant line 109
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_grade line 115
  17. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.raw line 124

    Source documentation

    Literal raw singleton; in particular no program is evaluated on it.

    def raw (w : List S) : Sector S Γ H :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector

  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_raw line 127
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep_clean line 129
  20. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.QuotaStep line 146

    Source documentation

    The quota rule is applicable only at the literal clean right cut.

    inductive QuotaStep : Sector S Γ H → Sector S Γ H → Prop
  | trim (l r : Cells S Γ) (lb rb : Bool) :
      QuotaStep ⟨Validator.cell blank .workspace::l,.pending,
          Validator.cell blank .cutD::r,lb,rb⟩
        ⟨l,.pending,Validator.cell blank .cutD::r,lb,rb⟩

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaStep_deterministic line 152
  22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaStep_grade line 156
  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaStep_left line 161
  24. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.trimQuota line 168
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.trimQuota_terminal line 172
  26. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal line 183
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.trimQuota_reaches line 188
  28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal_reaches line 202
  29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal_terminal line 217
  30. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal_invariant line 236
  31. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal_grade line 242
  32. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.unmerge line 252

    Source documentation

    Unmerge after trimming. The outer boundaries may be absent and the outer cells may be arbitrarily dirty. Only the two displayed cut cells are tested.

    def unmerge (v : Sector S Γ H) : List (Sector S Γ H) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector

  33. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess line 261
  34. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess_invariant line 264
  35. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.listGrade line 268
  36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.unmerge_grade line 270
  37. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess_grade line 288
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.trimQuota_workspace line 292
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess_merge line 299

    Source documentation

    The literal merge is undone, even on dirty/incomplete surroundings.

    theorem pendingPreprocess_merge (l r : Cells S Γ) (s : ℕ) (lb rb : Bool) :
    pendingPreprocess (H := H) blank
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess

  40. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupHead line 313
  41. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.ofCleanup line 317
  42. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupNormal line 319
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupNormal_ofCleanup line 325
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupNormal_grade line 330
  45. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess line 346
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_grade line 349
  47. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_ofCleanup line 354
  48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_invariant line 359
  49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_rawStep line 364
  50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_success line 372

    Source documentation

    Successful cleanup is exactly a full raw singleton, without any call to the program on the returned string.

    theorem cleanupPreprocess_success (l : Cells S Γ) (out : List S) (n : ℕ)
    (h : Simulator.anchorView l = out.map some ++ List.replicate n none) :
    cleanupPreprocess (H := H) blank ⟨l.reverse,.cleanup,[],true,true⟩ = raw blank out := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.raw

  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_raw line 379
  52. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Entry line 389

    Source documentation

    Literal entry and successful exit tests, both finite data predicates.

    def Entry (blank : Γ) (v : Sector S Γ Q) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Sector

  53. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Success line 392
  54. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Control.entryDecidable line 395
  55. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Control.successDecidable line 398
  56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.entry_cases line 401
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.entry_validator line 410
  58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.success_cases line 416
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.entries_unique line 426
  60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.successes_unique line 434
  61. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.representative line 445
  62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.representative_connected line 448
  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.representative_eq line 452
  64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.representative_entry line 456
  65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.representative_success line 461
  66. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess line 480

    Source documentation

    Internal finite-component search, with entry priority. No invocation of the compiled machine as an evaluator occurs here.

    def internalPreprocess (v : Control.Sector S Γ Q) : List (Sector S Γ (Control.Head S Q)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head

  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess_invariant line 488
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess_entry line 493
  69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess_success line 498
  70. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess line 507

    Source documentation

    Complete sector preprocessing, prior to the only partial operation: maximal full-raw-run evaluation. Headless sectors will be preserved by the parser.

    def preprocess (v : Sector S Γ (Control.Head S Q)) : List (Sector S Γ (Control.Head S Q)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head

  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_raw line 514
  72. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.skeletonGrade line 521
  73. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.grade_skeleton line 524
  74. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.grade_eq_of_skeleton line 529
  75. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.internalPreprocess_grade line 537
  76. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_grade line 554
  77. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_rawStep line 563
  78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_quotaStep line 568
  79. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_ofCleanup line 573
  80. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_cleanupStep line 578
  81. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_entryStep line 582
  82. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess_internalStep line 588
  83. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess_cleanEntry line 600

    Source documentation

    The two outputs of unmerging a clean full entry are precisely the two full raw words. This includes zero workspace and empty x or y.

    theorem pendingPreprocess_cleanEntry (x y : List S) (s : ℕ) :
    pendingPreprocess (H := Control.Head S Q) A.blank
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess, OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head