OAI/Combinatorics/ParityLifts/StackRoutines.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.Words line 7
  2. def OAI.ParityWL.Complexity.applyOps line 9
  3. inductive OAI.ParityWL.Complexity.StackExec line 12
  4. lemma OAI.ParityWL.Complexity.StackExec.output line 20
  5. lemma OAI.ParityWL.Complexity.StackExec.iterate line 27
  6. lemma OAI.ParityWL.Complexity.StackExec.map line 34
  7. def OAI.ParityWL.Complexity.StackMachine.andThen line 49

    Source documentation

    Structured sequential composition; one finite-control step starts the second routine once the first has returned. No external simulator is presumed.

    def StackMachine.andThen {Q R : Type} {t a : ℕ}
    (P : StackMachine Q t a) (T : StackMachine R t a) : StackMachine (Q ⊕ R) t a where
…

    Mentions: OAI.ParityWL.Complexity.StackMachine

  8. def OAI.ParityWL.Complexity.StackConfiguration.inl line 59
  9. def OAI.ParityWL.Complexity.StackConfiguration.inr line 62
  10. lemma OAI.ParityWL.Complexity.StackExec.andThen_right line 65
  11. lemma OAI.ParityWL.Complexity.StackExec.andThen line 73
  12. def OAI.ParityWL.Complexity.StackMachine.repeat line 98

    Source documentation

    Repeat a returning routine until it returns true, removing the halt marker on false. Restarting takes one local stack step and does not touch data.

    def StackMachine.repeat {Q : Type} {t a : ℕ} (P : StackMachine Q t a) : StackMachine Q t a where
…

    Mentions: OAI.ParityWL.Complexity.StackMachine

  13. lemma OAI.ParityWL.Complexity.StackExec.repeat_true line 105
  14. lemma OAI.ParityWL.Complexity.StackExec.repeat_false line 117
  15. def OAI.ParityWL.Complexity.primitive line 138

    Source documentation

    One finite-table operation, including a return bit chosen from scanned tops. All alphabets and control sets of this routine are visibly finite.

    def primitive {t a : ℕ}
    (ops : (Fin (t + 1) → Option (StackSymbol a)) → Fin (t + 1) → StackOp a)
    (test : (Fin (t + 1) → Option (StackSymbol a)) → Bool) :
    StackMachine (Option Bool) t a where
…

    Mentions: OAI.ParityWL.Complexity.StackSymbol, OAI.ParityWL.Complexity.StackOp, OAI.ParityWL.Complexity.StackMachine

  16. lemma OAI.ParityWL.Complexity.primitive_exec line 146
  17. def OAI.ParityWL.Complexity.Runs line 156
  18. lemma OAI.ParityWL.Complexity.Runs.andThen line 160
  19. lemma OAI.ParityWL.Complexity.Runs.compiled line 169
  20. structure OAI.ParityWL.Complexity.MacroMachine line 182

    Source documentation

    A finite control-flow chart whose nodes are verified stack routines.

    structure MacroMachine (Q : Type) (t a : ℕ) where
…
  21. def OAI.ParityWL.Complexity.MacroMachine.lower line 189
  22. def OAI.ParityWL.Complexity.MacroMachine.lift line 197
  23. lemma OAI.ParityWL.Complexity.MacroMachine.exec_routine line 201
  24. inductive OAI.ParityWL.Complexity.MacroExec line 223
  25. lemma OAI.ParityWL.Complexity.MacroExec.lower line 232
  26. lemma OAI.ParityWL.Complexity.MacroExec.compiled line 242
  27. def OAI.ParityWL.Complexity.transferStep line 252

    Source documentation

    A finite-table transfer step. The source is popped; a prescribed subset of other stacks receives its top symbol. An empty source returns true.

    def transferStep {t a : ℕ} (src : Fin (t + 1)) (dst : Finset (Fin (t + 1))) :
    StackMachine (Option Bool) t a :=
…

    Mentions: OAI.ParityWL.Complexity.StackMachine

  28. def OAI.ParityWL.Complexity.transfer line 259
  29. def OAI.ParityWL.Complexity.transferred line 262
  30. lemma OAI.ParityWL.Complexity.transfer_run line 266
  31. lemma OAI.ParityWL.Complexity.clear_run line 314

    Source documentation

    Emptying a stack never modifies another stack.

    lemma clear_run {t a : ℕ} (src : Fin (t + 1)) (w : Words t a) :
    Runs (transfer src ∅) w (2 * (w src).length + 1) (Function.update w src []) true := by
…

    Mentions: OAI.ParityWL.Complexity.Words, OAI.ParityWL.Complexity.Runs, OAI.ParityWL.Complexity.transfer