OAI/Computability/FiniteCompiler/TapeFolding.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

Safe tapes, literal folding, and uniform code-machine realization.

  1. structure OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.Cfg line 13
  2. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.step line 18
  3. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.view line 23
  4. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.append_at line 25
  5. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.replace_at line 31
  6. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.view_step line 47
  7. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.respects line 79
  8. inductive OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Side line 93
  9. instance OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.(instance at line 94) line 94
  10. structure OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Cell line 95
  11. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.position line 101
  12. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.read line 105
  13. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.command line 107
  14. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.machine line 115
  15. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Rel line 120

    Source documentation

    The two halves of the integer tape share one physical cell. The immutable origin flag makes crossing the fold a finite-control, zero-movement operation.

    def Rel (c : TM0.Cfg Γ Λ) (s : OneSided.Cfg (Cell Γ) (Side × Λ)) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MachineRealization.OneSided.Cfg, OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Cell, OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Side

  16. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.read_head line 127
  17. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.move_position line 134
  18. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.move_write line 143
  19. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.command_state line 148
  20. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.step_rel line 154
  21. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.respects line 216
  22. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.Safe line 233

    Source documentation

    Every writing subinstruction preserves the bottom track.

    def Safe : TM1.Stmt (TM2to1.Γ' K Γ) Λ σ → Prop
  | .move _ q => Safe q
  | .write f q => (∀ a v, (f a v).1 = a.1) ∧ Safe q
  | .load _ q => Safe q
  | .branch _ q r => Safe q ∧ Safe r
  | .goto _ => True
  | .halt => True
  23. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.safe_stAct line 241
  24. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.safe_normal line 246
  25. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.safe_tr line 249
  26. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.safe_sub line 258
  27. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.safe_stmts line 270
  28. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.trAux_write line 278
  29. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.Preserves line 294

    Source documentation

    A machine preserves the distinguished bottom marker on every write.

    def Preserves {L : Type*} [Inhabited L] (M : TM0.Machine (TM2to1.Γ' K Γ) L) : Prop :=
…
  30. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeSafety.finite_preserves line 297
  31. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_safe_tape line 323
  32. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.Marked line 360
  33. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.marked_step line 363
  34. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.TapeFold.marked_run line 387
  35. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.Gamma line 401
  36. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.cell_ext line 403
  37. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.blank line 407
  38. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.input line 408
  39. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.raw line 409
  40. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.canon line 410
  41. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.canon_rel line 414
  42. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.tape_neg line 418
  43. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.tape_fst line 422
  44. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.canon_marked line 429
  45. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.raw_cell line 433
  46. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.mark line 441
  47. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.clear line 442
  48. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.canon_cells line 445
  49. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.canon_clear line 464
  50. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.rel_canon_unique line 472
  51. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.folded_eval line 500
  52. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.After.path_cases line 533
  53. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.After.lift_reaches line 551
  54. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.After.eval_lift line 556
  55. abbrev OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.State line 579
  56. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.wrapper line 581
  57. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.lift line 590
  58. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.finish line 592
  59. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.initial line 594
  60. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.final line 595
  61. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.wrapper_lift line 598
  62. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.wrapper_finish line 606
  63. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.wrapper_initial line 609
  64. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.finish_canon line 615
  65. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.wrapper_eval line 620
  66. instance OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.(instance at line 634) line 634
  67. instance OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.(instance at line 636) line 636
  68. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.output line 639
  69. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.alphabet line 643
  70. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.output_decode line 650
  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.take_constant line 668
  72. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.interpret_content line 674
  73. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.semanticReturns_iff line 678
  74. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.view_initial line 703
  75. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.returns_final line 707
  76. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.realizes line 719
  77. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.WordEvaluator.exists_machine line 755

    Source documentation

    Every algorithmic partial word function has an actual one-sided finite machine with the literal first-blank readout used by the finite compiler.

    theorem exists_machine {f : List S →. List S} (hf : Partrec f) :
    ∃ (Γ Q : Type) (_ : Fintype Γ) (_ : Fintype Q)
      (A : Alphabet S Γ) (M : Machine Q Γ),
      (∀ g a, A.output g = some a → g = A.input a) ∧ Word.Realizes A M f := by
…
  78. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.eval_comp line 771
  79. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.quote line 777

    Source documentation

    A faithful syntactic encoding, not a choice of an evaluator for each index.

    def quote : Code → Nat.Partrec.Code
  | .zero' => .zero
  | .succ => .succ
  | .tail => .left
  | .cons a b => .pair (quote a) (quote b)
  | .comp a b => .comp (quote a) (quote b)
  | .case a b => .prec (quote a) (quote b)
  | .fix a => .rfind' (quote a)
  80. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.unquote line 786
  81. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.unquote_quote line 796
  82. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.quote_injective line 799
  83. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.numeral line 802
  84. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.numeral_eval line 806
  85. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.specialize line 812
  86. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.specialize_eval line 814
  87. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.primrec_quote_numeral line 818
  88. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.primrec_quote_specialize line 827
  89. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.exists_parameterized line 835

    Source documentation

    Parameter specialization is uniform at the literal code level. Only the single code implementing the two-variable function is selected.

    theorem exists_parameterized {f : ℕ → List ℕ →. List ℕ} (hf : Partrec₂ f) :
    ∃ C : ℕ → Code, Primrec (fun n => quote (C n)) ∧
      ∀ n w, (C n).eval (w.map Nat.succ) = (f n w).map (List.map Nat.succ) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.quote

  90. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.exists_word_parameterized line 876
  91. def OAI.FiniteAlgebraicEnvelopes.WordProgramming.eval line 902

    Source documentation

    An acceptable word-program numbering obtained from the pinned universal partial-recursive evaluator. Invalid decoded results remain undefined.

    def eval (c : Nat.Partrec.Code) (w : List S) : Part (List S) :=
…
  92. theorem OAI.FiniteAlgebraicEnvelopes.WordProgramming.partrec_eval line 905
  93. theorem OAI.FiniteAlgebraicEnvelopes.WordProgramming.fixed_point line 912

    Source documentation

    The source fixed-point equation for word algorithms, as literal equality of partial functions, including their domains.

    theorem fixed_point {F : Nat.Partrec.Code → List S →. List S}
    (hF : Partrec₂ F) : ∃ c, eval c = F c := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.WordProgramming.eval

  94. structure OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.Raw line 936

    Source documentation

    A literal raw-letter stack program, with its finite control part.

    structure Raw where
…
  95. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.raw line 944
  96. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.raw_correct line 955
  97. structure OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.TapeProgram line 973

    Source documentation

    A finite tape machine with distinguished literal input/output states.

    structure TapeProgram where
…
  98. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.tapeProgram line 984
  99. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.tapeProgram_correct line 1005
  100. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.compile line 1025
  101. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.compile_correct line 1031
  102. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.exists_family line 1040

    Source documentation

    One uniform syntactic program transformation feeds the specified model compiler. No evaluator is selected separately at each parameter.

    theorem exists_family {f : ℕ → List S →. List S} (hf : Partrec₂ f) :
    ∃ C : ℕ → Code, Primrec (fun n => UniformCode.quote (C n)) ∧
      ∀ n, Compiler.Word.Realizes FoldLiteral.alphabet (compile S (C n)) (f n) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.MachineRealization.UniformCode.quote, OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Realizes, OAI.FiniteAlgebraicEnvelopes.MachineRealization.FoldLiteral.alphabet, OAI.FiniteAlgebraicEnvelopes.MachineRealization.CodeMachine.compile