OAI/Computability/Logspace/TransitionTables.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite transition tables, configuration semantics, and reindexing into finite machines.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. structure OAI.ExactDerandomization.Table.Act line 25
  2. structure OAI.ExactDerandomization.Table.TM line 31
  3. structure OAI.ExactDerandomization.Table.Conf line 37
  4. def OAI.ExactDerandomization.Table.TM.init line 47
  5. def OAI.ExactDerandomization.Table.TM.applyAct line 50
  6. def OAI.ExactDerandomization.Table.TM.step line 56
  7. def OAI.ExactDerandomization.Table.TM.run line 63
  8. def OAI.ExactDerandomization.Table.TM.det line 68
  9. def OAI.ExactDerandomization.Table.TM.spaceThrough line 71
  10. def OAI.ExactDerandomization.Table.TM.halts line 74
  11. def OAI.ExactDerandomization.Table.TM.prob line 77
  12. def OAI.ExactDerandomization.Table.TM.idle line 81
  13. theorem OAI.ExactDerandomization.Table.TM.applyAct_idle line 83
  14. def OAI.ExactDerandomization.Table.TM.goStutter line 89

    Source documentation

    Uniform form of step: give halting states self-loop actions writing the scanned bits back.

    def goStutter (s : S) (i : H → InputSymbol) (v : W → Bool) (coin : Bool) :
    Act S W H :=
…

    Mentions: OAI.ExactDerandomization.InputSymbol, OAI.ExactDerandomization.Table.Act

  15. theorem OAI.ExactDerandomization.Table.TM.step_eq_apply line 93
  16. def OAI.ExactDerandomization.Table.TM.reindex line 100
  17. def OAI.ExactDerandomization.Table.TM.mapConf line 111
  18. theorem OAI.ExactDerandomization.Table.TM.step_reindex line 116
  19. theorem OAI.ExactDerandomization.Table.TM.run_reindex line 123
  20. theorem OAI.ExactDerandomization.Table.TM.out_reindex line 132
  21. theorem OAI.ExactDerandomization.Table.TM.prob_reindex line 139
  22. theorem OAI.ExactDerandomization.Table.TM.space_reindex line 144
  23. theorem OAI.ExactDerandomization.Table.TM.det_reindex line 150
  24. def OAI.ExactDerandomization.Table.TM.ofMachine line 156

    Source documentation

    Regard a Machine as a table (no reindexing).

    def ofMachine (M : Machine q w h) : TM (Fin (q+1)) (Fin w) (Fin h) :=
…

    Mentions: OAI.ExactDerandomization.Machine, OAI.ExactDerandomization.Table.TM

  25. theorem OAI.ExactDerandomization.Table.TM.reindex_refl line 161
  26. def OAI.ExactDerandomization.Table.TM.number line 166

    Source documentation

    The index equivalence is routine, but we record it to compile a nonempty-state table to the concrete Machine class.

    noncomputable def number [Fintype S] [Nonempty S] :
    S ≃ Fin (Fintype.card S - 1 + 1) :=
…