OAI/Computability/WLIdentification/ExpressionCompiler.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.WordExpressions.Expr.correct_cases line 10
  2. theorem OAI.WLIdentification.WordExpressions.Expr.correct_loop line 77
  3. theorem OAI.WLIdentification.WordExpressions.Expr.correct line 218

    Source documentation

    The finite word language executes on literal stacks, with polynomial cost in the lengths of all values in its evaluation.

    theorem correct {n} (e : Expr n) : e.Correct := by
…

    Mentions: OAI.WLIdentification.WordExpressions.Expr

  4. def OAI.WLIdentification.StackModel.Command.registers line 232
  5. def OAI.WLIdentification.StackModel.Command.small line 238
  6. def OAI.WLIdentification.StackModel.Command.finiteIndex line 240
  7. theorem OAI.WLIdentification.StackModel.Command.finiteIndex_val line 242
  8. theorem OAI.WLIdentification.StackModel.Command.restrict_update line 245
  9. theorem OAI.WLIdentification.StackModel.Command.Exec.restrict line 258

    Source documentation

    A syntactically finite register program has the same counted execution on its finite set of tracks, even though its correctness was proved with convenient natural register names.

    theorem Exec.restrict {c : Command ℕ R} {s S t T n} (hex : Exec c s S t T n)
    (N : ℕ) (hN : 0 < N) (hc : c.small N) :
    Exec (c.rename (finiteIndex N hN)) s (S ∘ Fin.val) t (T ∘ Fin.val) n := by
…

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Command.Exec, OAI.WLIdentification.StackModel.Command.finiteIndex

  10. theorem OAI.WLIdentification.StackModel.Command.small_exists line 280
  11. def OAI.WLIdentification.StackModel.Command.testProgram line 289

    Source documentation

    A three-instruction output test after a structured command, followed by a literal accepting or rejecting stack-machine halt.

    def testProgram {K : Type} (c : Command K (Option Bool)) (s : Option Bool) (out : K) :
    Program K (Option (Control c) ⊕ (Bool ⊕ Unit)) (Option Bool) where
…

    Mentions: OAI.WLIdentification.StackModel.Command, OAI.WLIdentification.StackModel.Program, OAI.WLIdentification.StackModel.Command.Control

  12. theorem OAI.WLIdentification.StackModel.Command.testProgram_embeds line 299
  13. theorem OAI.WLIdentification.StackModel.Command.Exec.testRun line 307
  14. def OAI.WLIdentification.ComputationBounds.Polynomial line 328
  15. theorem OAI.WLIdentification.ComputationBounds.constant line 330
  16. theorem OAI.WLIdentification.ComputationBounds.identity line 331
  17. theorem OAI.WLIdentification.ComputationBounds.add line 333
  18. theorem OAI.WLIdentification.ComputationBounds.mul line 342
  19. theorem OAI.WLIdentification.ComputationBounds.maximum line 352
  20. theorem OAI.WLIdentification.WordExpressions.Expr.cost_polynomial line 361
  21. def OAI.WLIdentification.WordExpressions.Expr.outputBound line 373
  22. theorem OAI.WLIdentification.WordExpressions.Expr.outputBound_polynomial line 376