OAI/Computability/FiniteCompiler/Control.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

Finite control and bounded compiler orbit normalization.

  1. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Head line 13
  2. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.(instance at line 17) line 17
  3. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Sector line 19
  4. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.emit line 23

    Source documentation

    Exactly the cleanup letter prescribed in the finite compiler. Output marks on nonanchors are deliberately ignored even on dirty configurations.

    def emit (c : Base S × Tag S Γ) : Option S :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

  5. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.letter line 28
  6. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output line 30
  7. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.step line 35

    Source documentation

    The left sweep deletes every consumed tagged cell, and only marks on anchors produce a clean right-hand anchor. The boundary test is literal.

    def step (blank : Γ) (v : Sector S Γ) : Option (Sector S Γ) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Sector

  8. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Step line 42
  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.deterministic line 44
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output_nil line 48
  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output_append line 50
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output_singleton line 54
  13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.sweep line 60

    Source documentation

    Each consumed cell is emitted before all previously emitted cells. This proves the leftward cleanup's order on arbitrary—not only clean—data.

    theorem sweep (blank : Γ) (l r : List (Base S × Tag S Γ)) (a b : Bool) :
    ReflTransGen (Step blank) ⟨l,.cleanup,r,a,b⟩
      ⟨[],.cleanup,output blank l.reverse ++ r,a,b⟩ := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output

  14. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.normal line 72

    Source documentation

    Normalization of a cleanup head, with or without a left boundary.

    def normal (blank : Γ) (v : Sector S Γ) : Sector S Γ :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Sector

  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.normal_reached line 78
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.normal_terminal line 89
  17. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.normal_invariant line 96

    Source documentation

    Cleanup normal forms are invariant under either direction of any local cleanup equation, including in dirty sectors with missing boundaries.

    theorem normal_invariant (blank : Γ) {v w : Sector S Γ}
    (h : EqvGen (Step blank) v w) : normal blank v = normal blank w := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.normal

  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.emit_anchorView line 114

    Source documentation

    Cleanup forgets empty marks, not anchor order.

    theorem emit_anchorView (l : List (Base S × Tag S Γ)) :
    l.filterMap emit = (Simulator.anchorView l).filterMap id := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.emit, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView

  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.emit_returned line 122
  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.success line 129

    Source documentation

    Exact successful cleanup, including empty returned strings.

    theorem success (blank : Γ) (l : List (Base S × Tag S Γ)) (out : List S) (n : ℕ)
    (h : Simulator.anchorView l = out.map some ++ List.replicate n none) :
    ReflTransGen (Step blank) ⟨l.reverse,.cleanup,[],true,true⟩
      ⟨[],.raw,out.map (letter blank),true,true⟩ := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.anchorView, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.letter

  21. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.grade line 136
  22. def OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.cellsGrade line 141
  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.cellsGrade_append line 143
  24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.cellsGrade_reverse line 146
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output_grade_le line 151

    Source documentation

    Grade is nonincreasing for EVERY tagged cleanup cell. Workspace marks do not emit letters, so grade-zero workspace can never create positive grade.

    theorem output_grade_le (blank : Γ) (l : List (Base S × Tag S Γ)) :
    cellsGrade (output blank l) ≤ cellsGrade l := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.cellsGrade, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.output

  26. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.boundedLists line 171

    Source documentation

    An explicit bounded list enumeration, used only for finite internal search. This bound counts cells, not grade, and thus never admits quota insertion.

    def boundedLists (α : Type*) [Fintype α] [DecidableEq α] : ℕ → Finset (List α)
  | 0 => {[]}
  | n+1 => {[]} ∪ ((Finset.univ : Finset α) ×ˢ boundedLists α n).image (fun p => p.1::p.2)
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_boundedLists line 175
  28. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.boundedSectors line 188

    Source documentation

    The finite search universe consists of actual list-zipper sectors.

    def boundedSectors (k : ℕ) : Finset (Sector H B T) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector

  29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_boundedSectors line 193
  30. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.searchUniverse line 200

    Source documentation

    Filtering by bases and boundary flags gives exactly the source's fixed internal-search state space. This is computable from the literal sector.

    def searchUniverse (v : Sector H B T) : Finset (Sector H B T) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector

  31. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.skeleton_length line 205
  32. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_universe line 210
  33. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Fixed line 217
  34. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedFintype line 219
  35. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedSelf line 222
  36. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedStep line 224
  37. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedStepDecidable line 227
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.connected_skeleton line 231
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedConnected_iff line 241

    Source documentation

    A weak path with fixed baselines lifts to the finite search universe.

    theorem fixedConnected_iff (table : Table H B T) (v : Sector H B T) (a b : Fixed v) :
    EqvGen (fixedStep table v) a b ↔ EqvGen (Step table) a.val b.val := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Fixed, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.fixedStep, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step

  40. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.connectedDecision line 276

    Source documentation

    Operational component equality has a finite decision procedure. Its only primitives are the finite table, tagged cells, and bounded finite search.

    def connectedDecision (table : Table H B T) (v : Sector H B T) (w : Fixed v) : Bool :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Fixed

  41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.connectedDecision_eq_true line 279
  42. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineSector line 292
  43. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Cfg line 293
  44. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed line 296

    Source documentation

    The fresh handoff is one state, not two copies joined by an artificial edge.

    def embed (v : MachineSector S Γ Q) : Cfg S Γ Q :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineSector, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Cfg

  45. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.project line 301
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.project_embed line 305
  47. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_injective line 309
  48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_active line 313
  49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_project line 317
  50. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineRel line 327
  51. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step line 330
  52. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.machine_deterministic line 333
  53. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.deterministic line 338
  54. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.bases line 341
  55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_bases line 345
  56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.machine_bases line 349
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.entries_unique line 355

    Source documentation

    The manuscript's uniqueness of entries, now for the concrete copy/run/read table, not for an unspecified simulated relation.

    theorem entries_unique {a b : Validator.Sector S Γ}
    (ha : Validator.Entry A.blank a) (hb : Validator.Entry A.blank b)
    (h : EqvGen (Step A M) (.inl a) (.inl b)) : a = b :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step

  58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_step line 361
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed_run line 365
  60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.validator_run line 372
  61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.active_step line 379
  62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.path_decomposition line 387

    Source documentation

    A path retains its actual simulator suffix after the unique validation handoff. This rules out a dirty intermediate state being treated as input.

    theorem path_decomposition {a : Validator.Sector S Γ} {b : Cfg S Γ Q}
    (h : ReflTransGen (Step A M) (.inl a) b) :
    (∃ v, b = .inl v ∧ ReflTransGen (Validator.Step A.blank) a v) ∨
    ∃ v u, ReflTransGen (Validator.Step A.blank) a v ∧ v.head = .start ∧
      b = embed u ∧ ReflTransGen (Scan.Step (Simulator.table A M)) (project (.inl v)) u := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Cfg, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.project

  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.ok_terminal line 406
  64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.ok_unique line 420

    Source documentation

    Arbitrary dirty accepting sectors are unique within a weak component.

    theorem ok_unique {u v : MachineSector S Γ Q} (hu : u.head = .ok) (hv : v.head = .ok)
    (h : EqvGen (Step A M) (embed u) (embed v)) : u = v :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineSector, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed

  65. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.cleanEntry line 430

    Source documentation

    The literal entry and handoff of compiler-clean-entry.

    def cleanEntry (blank : Γ) (x y : List S) (s : ℕ) : Validator.Sector S Γ :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector

  66. def OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.handoff line 435
  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.cleanEntry_entry line 441
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.cleanEntry_reaches line 444
  69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.validator_start_terminal line 448
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.handoff_unique line 453
  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.project_handoff line 465
  72. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.accepting_entry_runs line 474

    Source documentation

    Clean entries that meet an accepting internal sector really passed the validator and then ran this very machine. No cleanliness is assumed of the sector used for finding its weak component.

    theorem accepting_entry_runs {a : Validator.Sector S Γ} {b : MachineSector S Γ Q}
    (ha : Validator.Entry A.blank a) (hb : b.head = .ok)
    (h : EqvGen (Step A M) (.inl a) (embed b)) :
    ∃ x y s, a = cleanEntry A.blank x y s ∧
      ReflTransGen (Scan.Step (Simulator.table A M))
        ⟨(Simulator.body A [] x [] y [] s).reverse,.start,[],true,true⟩ b := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineSector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.cleanEntry, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.body

  73. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.accepting_entry_sound line 495

    Source documentation

    Concrete soundness part of Lemma compiler-components: true halted output, the exact length bound, AND the mandated literal cleanup word. Quota insufficiency is ruled out by the previously proved rejection theorem.

    theorem accepting_entry_sound
    (hdecode : ∀ g a, A.output g = some a → g = A.input a)
    {a : Validator.Sector S Γ} {b : MachineSector S Γ Q}
    (ha : Validator.Entry A.blank a) (hb : b.head = .ok)
    (h : EqvGen (Step A M) (.inl a) (embed b)) :
    ∃ x y s n c out, ∃ (result : List (Base S × Tag S Γ)),
      a = cleanEntry A.blank x y s ∧ s = x.length+y.length+n+1 ∧
      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 ∧
      out.length ≤ x.length+y.length ∧ b = ⟨result.reverse,.ok,[],true,true⟩ ∧
      ReflTransGen (Cleanup.Step A.blank) ⟨result.reverse,.cleanup,[],true,true⟩
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.MachineSector, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Entry, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.Step, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.embed, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag, OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.cleanEntry, 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, OAI.FiniteAlgebraicEnvelopes.Compiler.Cleanup.Step

  74. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Compiled.clean_success line 516

    Source documentation

    Conversely an actual finite halted computation with the required output bound has some quota and gives entry-to-ok reachability and exact cleanup.

    theorem clean_success (x y out : List S)
    (c : Simulator.Tape (S := S) (Γ := Γ) (Q := Q))
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Tape

  75. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.(instance at line 540) line 540
  76. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.toScan line 543
  77. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.ofScan line 546
  78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.toScan_ofScan line 549
  79. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.ofScan_toScan line 551
  80. def OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.table line 556

    Source documentation

    The displayed validator equations as an executable finite scan table.

    def table : Table Head (Base S) (Tag S Γ) where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

  81. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_toScan line 577
  82. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_ofScan line 581
  83. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.step_iff_scan line 646
  84. instance OAI.FiniteAlgebraicEnvelopes.Compiler.Validator.stepDecidable line 650
  85. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mapHead line 660
  86. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mapInstruction line 663
  87. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.skeleton_mapHead line 666
  88. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mapHead_injective line 669
  89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step_mapHead line 680

    Source documentation

    A literal relabeling of finite control commutes with one scan step. Only agreement at the current head is needed, permitting fused control tables.

    theorem step_mapHead (f : H → H') (t : Table H B T) (t' : Table H' B T)
    (v : Sector H B T)
    (hd : t'.direction (f v.head) = t.direction v.head)
    (hc : ∀ b a, t'.cell (f v.head) b a = (t.cell v.head b a).map (mapInstruction f))
    (hb : t'.boundary (f v.head) = (t.boundary v.head).map f) :
    step t' (mapHead f v) = (step t v).map (mapHead f) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mapInstruction, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.step, OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mapHead

  90. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head line 719

    Source documentation

    Finite internal-head alphabet, with a single fresh handoff/start state.

    inductive Head (S Q : Type*)
  | initial | left | right | workspace | suffix
  | machine : Simulator.Head S Q → Head S Q
  deriving DecidableEq, Fintype

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Control.machine, OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.Head

  91. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.validatorHead line 724
  92. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.toValidator line 732
  93. abbrev OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Sector line 740
  94. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.validator line 742
  95. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.machine line 745
  96. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.toCfg line 748
  97. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.cfg_validator line 757
  98. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.cfg_machine line 760
  99. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.table line 767

    Source documentation

    The literal finite union of validation and simulation equations.

    def table : Table (Head S Q) (Base S) (Tag S Γ) where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Table, OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Head, OAI.FiniteAlgebraicEnvelopes.Compiler.Base, OAI.FiniteAlgebraicEnvelopes.Compiler.Tag

  100. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.step_machine line 784
  101. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.step_validator line 791
  102. def OAI.FiniteAlgebraicEnvelopes.Compiler.Control.ofCfg line 805
  103. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.ofCfg_embed line 809
  104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.ofCfg_toCfg line 814
  105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.cfg_injective line 818
  106. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.sector_cases line 821
  107. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.validator_step line 836
  108. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.machine_step line 842
  109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.cfg_step line 848
  110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.ofCfg_step line 862
  111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.cfg_connected line 871
  112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.ofCfg_runs line 879
  113. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literalComponent line 894

    Source documentation

    Literal configurations, rather than an oracle for connectivity, returned by exhaustive search on the fixed finite base skeleton.

    def literalComponent (table : Table H B T) (v : Sector H B T) : Finset (Sector H B T) :=
…

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

  114. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.mem_literalComponent line 897
  115. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literalComponent_nonempty line 909
  116. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literalComponent_eq line 913
  117. def OAI.FiniteAlgebraicEnvelopes.Compiler.prioritySet line 926

    Source documentation

    The priority order in source compiler-normalization: entry first, success second, and arbitrary component member only when neither is present.

    def prioritySet (P Q : α → Prop) [DecidablePred P] [DecidablePred Q] (s : Finset α) : Finset α :=
…
  118. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.prioritySet_subset line 930
  119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.prioritySet_nonempty line 938
  120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.prioritySet_first line 945
  121. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.prioritySet_second line 953
  122. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative line 973
  123. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_mem line 977
  124. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_connected line 981
  125. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_eq line 986
  126. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_first line 991
  127. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.representative_second line 996