OAI/Computability/FiniteCompiler/Normalization.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

Raw-run folds, full word compilation, partial budgets, and bounded normalization.

  1. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item line 12
  2. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.itemGrade line 15

    Source documentation

    Full raw sectors have three structural letters alpha,Q,omega.

    def itemGrade (g : C → ℕ) : Item C S → ℕ
  | .inl c => g c
  | .inr w => w.length + 3

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item

  3. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade line 19
  4. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade_nil line 21
  5. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade_cons line 22
  6. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade_append line 24
  7. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.prepend line 29

    Source documentation

    Fold a nonempty raw run by adjacent pair replacement. We prove below that it agrees with the source's single call on the concatenated maximal run.

    def prepend (f : List S → List S) : Item C S → List (Item C S) → List (Item C S)
  | .inr x,.inr y::w => .inr (f (x++y))::w
  | a,w => a::w

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item

  8. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize line 33
  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_nil line 37
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_cons line 38
  11. structure OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget line 43

    Source documentation

    Budget laws are used only where the unreduced concatenation has bounded length. They are exactly the totality/length/context interface of the source.

    structure Budget (f : List S → List S) (m : ℕ) : Prop where
…
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.prepend_grade line 49
  13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_grade line 66
  14. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.triple line 78

    Source documentation

    The two bracketings of three adjacent raw inputs agree inside the same budget. No idempotence assumption on raw singleton sectors is made.

    theorem triple (h : Budget f m) (x y z : List S)
    (hm : (x++y++z).length ≤ m) : f (x++f (y++z)) = f (f (x++y)++z) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget

  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.prepend_pair line 85
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_left_context line 102

    Source documentation

    Left contexts commute with equality of folded normal forms, without any stability-of-sector-boundaries claim.

    theorem normalize_left_context {u v : List (Item C S)} (h : normalize f u = normalize f v)
    (a : List (Item C S)) : normalize f (a++u) = normalize f (a++v) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize

  17. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.pair_context line 110

    Source documentation

    Contextual invariance of pair versus its genuine returned singleton; this is the only nontrivial comparison at q_ok--cleanup with entry priority.

    theorem pair_context (g : C → ℕ) (h : Budget f m) (x y : List S) (a b : List (Item C S))
    (hm : grade g (a ++ .inr x :: .inr y :: b) ≤ m) :
    normalize f (a ++ .inr x :: .inr y :: b) =
      normalize f (a ++ .inr (f (x++y)) :: b) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize

  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_singleton line 123

    Source documentation

    On one full raw sector the evaluator never calls the program.

    @[simp] theorem normalize_singleton (x : List S) :
    normalize f ([.inr x] : List (Item C S)) = [.inr x] := rfl

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item

  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_run line 128

    Source documentation

    On a raw run of size at least two this fold is exactly a single application to the literal concatenation, as specified by the frozen source.

    theorem normalize_run (h : Budget f m) (x y : List S) (ws : List (List S))
    (hm : (x++y++ws.flatten).length ≤ m) :
    normalize f (((x::y::ws).map Sum.inr) : List (Item C S)) =
      [.inr (f (x++y++ws.flatten))] := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item

  20. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun line 145

    Source documentation

    Split off the entire initial raw run, without changing raw contents.

    def splitRun : List (Item C S) → List (List S) × List (Item C S)
  | [] => ([],[])
  | .inl c::w => ([],.inl c::w)
  | .inr x::w => let p := splitRun w; (x::p.1,p.2)

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item

  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun_join line 150
  22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun_length line 156
  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun_stops line 161
  24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade_raws line 170
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.prepend_append_separator line 177
  26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize_append_separator line 183
  27. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.source line 192

    Source documentation

    The literal source algorithm: a singleton does not invoke f; every longer maximal raw run invokes f once on its unmodified concatenation.

    def source (f : List S → List S) : List (Item C S) → List (Item C S)
  | [] => []
  | .inl c::w => .inl c::source f w
  | .inr x::w =>
    let p := splitRun w
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun

  28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.source_eq_normalize line 210

    Source documentation

    Bounded comparison with the fold is a theorem, not an alteration of the source algorithm. In particular source calls obey the same grade budget.

    theorem source_eq_normalize (g : C → ℕ) (h : Budget f m) (w : List (Item C S))
    (hm : grade g w ≤ m) : source f w = normalize f w := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.source, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.normalize

  29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.source_grade line 254
  30. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal line 266

    Source documentation

    Only a change of representation. The cell order and both literal boundary flags are retained exactly.

    def literal (m : H → K) (v : Sector H B T) : Path.Sector (B×T) K :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector

  31. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.unliteral line 269
  32. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal_unliteral line 272
  33. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.unliteral_literal line 274
  34. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal_injective line 277
  35. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.inLeft line 291

    Source documentation

    Zipper fragments of a literal cell instruction, before and after the specified cross/stay move.

    def inLeft (d : Direction) (c : B×T) : List (B×T) := if d = .left then [c] else []

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Direction

  36. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.inRight line 292
  37. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.outLeft line 293
  38. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.outRight line 295
  39. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.Rule line 298
  40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.cell_step line 310
  41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.rule_shape line 320
  42. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.rule_length line 327
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.prepare_rule line 340

    Source documentation

    Sector invariance for a deterministic table implies literal invariance for every cell and boundary equation in every word context.

    theorem prepare_rule (table : Table H B T) (m : H → K)
    (P : Path.Sector (B×T) K → List (Path.Sector (B×T) K))
    (hinv : ∀ v w, Step table v w → P (literal m v) = P (literal m w))
    {u v : List (Letter (B×T) K)} (h : Rule table m u v)
    (x y : List (Letter (B×T) K)) (hn : shape (x++u++y) ≠ .zero) :
    prepare P (x++u++y) = prepare P (x++v++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.Rule

  44. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Cell line 369
  45. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Head line 370
  46. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter line 371
  47. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Sector line 372
  48. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.encode line 374
  49. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Ordinary line 379

    Source documentation

    The actual source equations, separate from the exceptional accepting exit for which only the complete raw-run evaluator is invariant.

    inductive Ordinary (A : Simulator.Alphabet S Γ) (M : Simulator.Machine Q Γ)
    [DecidableEq S] [DecidableEq Γ] : List (Letter S Γ Q) → List (Letter S Γ Q) → Prop
  | raw (a : S) : Ordinary A M
      [.left (Validator.cell A.blank (.anchor a)),.head .raw]
      [.head .raw,.right (Validator.cell A.blank (.anchor a))]
  | merge : Ordinary A M [.head .raw,.leave,.enter,.head .raw]
      [.left (Validator.cell A.blank .cutC),.head .pending,.right (Validator.cell A.blank .cutD)]
  | quota : Ordinary A M
      [.left (Validator.cell A.blank .workspace),.head .pending,.right (Validator.cell A.blank .cutD)]
      [.head .pending,.right (Validator.cell A.blank .cutD)]
  | entry : Ordinary A M [.head .pending,.right (Validator.cell A.blank .cutD)]
      [.head (.internal .initial),.right (Validator.cell A.blank .cutD)]
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Alphabet, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.raw, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.cell

  50. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rule line 397
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ordinary_shape line 406
  52. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rule_shape line 416
  53. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ordinary_length line 422
  54. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rule_length line 433
  55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rules_finite line 442

    Source documentation

    The source presentation is finite, not a schema depending on arbitrary sector contexts. Every defining side has at most four letters.

    theorem rules_finite [Fintype S] [Fintype Γ] [Fintype Q] :
    {p : List (Letter S Γ Q) × List (Letter S Γ Q) | Rule A M p.1 p.2}.Finite := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rule

  56. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.sectorPreprocess line 452
  57. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess line 455
  58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.sectorPreprocess_literal line 458
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess_ordinary line 464

    Source documentation

    Every ordinary source equation has identical preprocessed sector lists in any literal nonzero context. Only the accepting exit needs a program law.

    theorem preprocess_ordinary {u v : List (Letter S Γ Q)} (h : Ordinary A M u v)
    (x y : List (Letter S Γ Q)) (hn : shape (x++u++y) ≠ .zero) :
    preprocess A M (x++u++y) = preprocess A M (x++v++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Ordinary, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess

  60. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.gradeCell line 520
  61. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade line 521
  62. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.chunksGrade line 522
  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_encode line 524
  64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_append line 531
  65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.chunksGrade_append line 534
  66. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.chunksGrade_flatten line 537
  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_raw line 543
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_letter_le line 550
  69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.sectorPreprocess_grade line 560
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.prepareChunk_grade line 569
  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.prepareChunks_grade line 578
  72. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess_grade line 586
  73. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.raw line 595
  74. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rawLetters line 599

    Source documentation

    Candidate extraction followed by a literal check recognizes only full, clean raw sectors. Dirty tags or absent boundaries cannot silently pass.

    def rawLetters (w : List (Letter S Γ Q)) : List S := w.filterMap fun a =>
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter

  75. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rawLetters_raw line 604
  76. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.readRaw line 610
  77. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.readRaw_raw line 614
  78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.readRaw_sound line 617
  79. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Item line 624
  80. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.classify line 626
  81. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.realize line 631
  82. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.classify_raw line 635
  83. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.realize_classify line 638
  84. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.itemGrade_classify line 644
  85. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_realize line 652
  86. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.classify_grade line 658
  87. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.realizeList_grade line 663
  88. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.exit_alternative line 680

    Source documentation

    The exact exceptional comparison. When entry priority changes the answer, both boundaries really exist, and a bounded run of the specified machine returns the output of cleanup. No program equation is assumed here.

    theorem exit_alternative
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    (l : Cells S Γ) (lb : Bool) :
    preprocess A M ⟨l,.internal (.machine .ok),[],lb,true⟩ =
      preprocess A M ⟨l,.cleanup,[],lb,true⟩ ∨
    ∃ x y out n c,
      preprocess A M ⟨l,.internal (.machine .ok),[],lb,true⟩ =
        [raw A.blank x,raw A.blank y] ∧
      preprocess A M ⟨l,.cleanup,[],lb,true⟩ = [raw A.blank out] ∧
      ReflTransGen (Simulator.TapeStep M)
        (Simulator.pad A (Simulator.initialTape A M (x++y)) (n+1)) c ∧
      Simulator.Halted A M c ∧ Simulator.Returns A c out := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Cells, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.preprocess, OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.raw, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.TapeStep, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.pad, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.initialTape, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Halted, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Returns

  89. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal line 734

    Source documentation

    The source algorithm, with the partial call separated as f. Its actual computable domain/realization is established at the program boundary.

    def normal (f : List S → List S) (w : List (Letter S Γ Q)) : List (Letter S Γ Q) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter

  90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_eq_fold line 738
  91. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_grade line 745
  92. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_ordinary line 756
  93. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_zero line 764
  94. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess_raw line 774
  95. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_raw line 782
  96. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt line 790

    Source documentation

    Finite tape realization at a bound. This is a lemma parameter, not an assumption of either main theorem; the partial-recursive adapter must prove it.

    def ComputesAt (f : List S → List S) (m : ℕ) : Prop :=
…
  97. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_exit line 795
  98. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_rule line 845

    Source documentation

    Every literal defining equation is invariant in arbitrary word contexts, including dirty and incomplete sectors, within the unchanged grade bound.

    theorem normal_rule
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    {f : List S → List S} {m : ℕ} (h : RawRuns.Budget f m) (hcomp : ComputesAt A M f m)
    {u v : List (Letter S Γ Q)} (hr : Rule A M u v) (a b : List (Letter S Γ Q))
    (h₁ : grade (a++u++b) ≤ m) (h₂ : grade (a++v++b) ≤ m) :
    normal A M f (a++u++b) = normal A M f (a++v++b) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rule, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal

  99. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_headed line 861
  100. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Literal.encode_step line 879
  101. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Reduce line 927

    Source documentation

    A literal equation in either direction, used without any grade increase.

    def Reduce (u v : List (Letter S Γ Q)) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter

  102. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Reduces line 929
  103. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_grade line 931
  104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_context line 936
  105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_context line 941
  106. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_append line 945
  107. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_reduce line 954
  108. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_reduces line 967
  109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_mono line 981
  110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.context_symm line 987
  111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.internal_rule_grade line 1002
  112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ordinary_grade line 1012
  113. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rule_grade line 1023
  114. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_rule line 1029
  115. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_rule_reverse line 1033
  116. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_internal line 1038
  117. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_internal line 1055
  118. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_of_context_rule line 1072
  119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_reverse line 1080
  120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_reverse line 1083
  121. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_headed line 1094
  122. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_rawStep line 1100
  123. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_rawNormal line 1108
  124. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_quotaNormal line 1112
  125. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_entry line 1122
  126. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_cleanup line 1129
  127. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_cleanupNormal line 1156
  128. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_cleanupPreprocess line 1165
  129. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_unmerge line 1169
  130. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_unmerge line 1181
  131. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_pendingPreprocess line 1205
  132. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduce_exit line 1209
  133. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_internalPreprocess line 1220
  134. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_sectorPreprocess line 1252
  135. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_prepareChunk line 1274
  136. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_prepareChunks line 1286
  137. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_preprocess line 1294
  138. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_zero line 1300
  139. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade_flatMap_encode line 1314
  140. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_rawPair_of_run line 1321
  141. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_rawPair line 1351
  142. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_prepend line 1367
  143. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_rawRuns line 1389
  144. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.reduces_normal line 1408

    Source documentation

    A literal, grade-nonincreasing derivation to the source's whole-word evaluator, not just equality in an assumed quotient.

     theorem reduces_normal {f : List S → List S} {m : ℕ}
    (h : RawRuns.Budget f m) (hcomp : ComputesAt A M f m)
    (w : List (Letter S Γ Q)) (hm : grade w ≤ m) :
    Reduces A M w (normal A M f w) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Reduces, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal

  145. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_idempotent line 1424
  146. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_context line 1442

    Source documentation

    The bounded context conclusion uses the nonincreasing literal derivations; the attachment need not preserve sector boundaries.

    theorem normal_context
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    {f : List S → List S} {m : ℕ} (h : RawRuns.Budget f m) (hcomp : ComputesAt A M f m)
    {u v : List (Letter S Γ Q)} (he : normal A M f u = normal A M f v)
    (x y : List (Letter S Γ Q))
    (hu : grade (x++u++y) ≤ m) (hv : grade (x++v++y) ≤ m) :
    normal A M f (x++u++y) = normal A M f (x++v++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade

  147. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rel line 1460

    Source documentation

    The compiler's finite monoid presentation is formed from the literal rule table; neither a normalizer nor program totality enters its definition.

    abbrev Rel (u v : FreeMonoid (Letter S Γ Q)) : Prop := Rule A M u v

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rule

  148. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Presentation line 1461
  149. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present line 1462
  150. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_append line 1466
  151. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_context line 1471
  152. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_reduce line 1477
  153. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_reduces line 1488
  154. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_normal line 1494
  155. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_conGen line 1502

    Source documentation

    No maximum grade of a presentation derivation is assumed. Its finitely many contextual uses are handled by the theorem at all finite budgets.

    theorem normal_conGen
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    {f : List S → List S} (h : ∀ m, RawRuns.Budget f m) (hcomp : ∀ m, ComputesAt A M f m)
    {u v : FreeMonoid (Letter S Γ Q)} (he : conGen (Rel A M) u v) :
    normal A M f u = normal A M f v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Rel, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal

  156. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_eq_iff_normal line 1538

    Source documentation

    Exact equality criterion for the finite presentation under the global (not assumed for constructing the presentation) evaluator hypotheses.

    theorem present_eq_iff_normal
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    {f : List S → List S} (h : ∀ m, RawRuns.Budget f m) (hcomp : ∀ m, ComputesAt A M f m)
    (u v : List (Letter S Γ Q)) :
    present A M u = present A M v ↔ normal A M f u = normal A M f v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Budget, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.ComputesAt, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal

  157. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_nil line 1558
  158. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_omega line 1561
  159. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_contains_omega line 1564
  160. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.preprocess_raw_pair line 1568
  161. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal_raw_product line 1587

    Source documentation

    Singleton raw words are fixed, but adjacent full raw words call the program on their concatenation, exactly as in the manuscript.

    theorem normal_raw_product (f : List S → List S) (u v : List S) :
    normal A M f (raw (Q := Q) A.blank u ++ raw A.blank v) = raw A.blank (f (u++v)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.raw

  162. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.present_nil_ne_omega line 1594
  163. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action line 1611

    Source documentation

    A nonraw literal sector, an unchanged singleton raw sector, or a genuine program call on an entire maximal raw run.

    inductive Action (C S : Type*)
  | keep (c : C)
  | raw (w : List S)
  | call (w : List S)
  deriving DecidableEq
  164. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan line 1617
  165. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.total line 1633
  166. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan_total line 1638
  167. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan_call_bound line 1654

    Source documentation

    Every program argument is bounded by the grade of the original item list, before any output from the program is computed.

    theorem plan_call_bound (g : C → ℕ) (w : List (Item C S)) {x : List S}
    (hx : Action.call x ∈ plan w) : x.length ≤ grade g w := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Item, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan, OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.grade

  168. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.partial line 1687
  169. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.execute line 1692
  170. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.execute_total_mem line 1696
  171. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.partialSource line 1710
  172. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.partialSource_total_mem line 1713
  173. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal line 1729

    Source documentation

    The manuscript's partial normalizer. It is defined even for a divergent program; no arbitrary value is inserted for an undefined call.

    def partialNormal (f : List S → Part (List S)) (w : List (Letter S Γ Q)) : Part (List (Letter S Γ Q)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter

  174. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_total_mem line 1735

    Source documentation

    Agreement only needs the values below the input's additive grade.

    theorem partialNormal_total_mem {f : List S → Part (List S)} {t : List S → List S}
    (w : List (Letter S Γ Q)) (h : ∀ x, x.length ≤ grade w → t x ∈ f x) :
    normal A M t w ∈ partialNormal A M f w := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Letter, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.grade, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.normal, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal

  175. structure OAI.FiniteAlgebraicEnvelopes.Compiler.PartialBudget line 1755

    Source documentation

    Literal domain/length/context premises of the finite compiler's bounded theorem. These are conditions on the given partial program, not a total replacement.

    structure PartialBudget {S : Type*} (f : List S → Part (List S)) (m : ℕ) : Prop where
…
  176. def OAI.FiniteAlgebraicEnvelopes.Compiler.partValue line 1763

    Source documentation

    Used only to state the bounded correctness proof of the partial algorithm. It has no place in its definition or in its claimed effective implementation.

    noncomputable def partValue {S : Type*} (p : Part (List S)) : List S := by
…
  177. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.partValue_mem line 1767
  178. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.partValue_eq line 1771
  179. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.PartialBudget.totalize line 1774
  180. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Realizes line 1792

    Source documentation

    The finite-machine adapter has to prove this execution specification for any supplied partial-recursive program. It is not an extra main hypothesis.

    def Realizes (f : List S → Part (List S)) : Prop :=
…
  181. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Realizes.computesAt line 1799
  182. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_eq_some line 1804
  183. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_terminates line 1810
  184. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_reduces line 1815
  185. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_rule line 1823
  186. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.partialNormal_context line 1832