OAI/Computability/SpaceSimulation/Stack/FromTM.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Calls to fixed accessor programs can be used in binary stack computations. The arguments are small (the conversion charges space for them too). Do not simulate the public input head with a counter: pass it straight through, and rewind when done.

  1. def OAI.Fifths.WorkSplit.bit line 17
  2. def OAI.Fifths.WorkSplit.buf line 20
  3. def OAI.Fifths.WorkSplit.read line 23
  4. theorem OAI.Fifths.WorkSplit.read_eq line 25
  5. def OAI.Fifths.WorkSplit.stepCenter line 39
  6. def OAI.Fifths.WorkSplit.stepOp line 45
  7. theorem OAI.Fifths.WorkSplit.stepCenter_eq line 50
  8. theorem OAI.Fifths.WorkSplit.stepOp_eq line 58
  9. def OAI.Fifths.ArgSplit.buf line 65
  10. def OAI.Fifths.ArgSplit.stepCenter line 67
  11. def OAI.Fifths.ArgSplit.stepOp line 73
  12. theorem OAI.Fifths.ArgSplit.stepCenter_eq line 81
  13. theorem OAI.Fifths.ArgSplit.stepOp_eq line 86
  14. abbrev OAI.Fifths.TM.stkIdx line 95
  15. abbrev OAI.Fifths.TM.stkQ line 96
  16. def OAI.Fifths.TM.asSM line 104
  17. structure OAI.Fifths.TM.SRep line 122
  18. def OAI.Fifths.TM.SRep.cfg line 131
  19. def OAI.Fifths.TM.SRep.after line 137
  20. theorem OAI.Fifths.TM.SRep.cfg_ok line 147
  21. theorem OAI.Fifths.TM.SRep.sees line 159
  22. theorem OAI.Fifths.TM.SRep.centers line 168
  23. theorem OAI.Fifths.TM.SRep.halt line 172
  24. theorem OAI.Fifths.TM.SRep.continue_step line 178
  25. theorem OAI.Fifths.TM.SRep.emulate line 196
  26. def OAI.Fifths.TM.loaded line 218

    Source documentation

    Work stacks empty. Argument j on its right stack.

    def loaded (x : J → List Bool) : M.stkIdx → List Bool :=
…
  27. theorem OAI.Fifths.TM.asSM_exec line 221
  28. def OAI.Fifths.SM.clears line 250
  29. def OAI.Fifths.SM.wiped line 254
  30. theorem OAI.Fifths.SM.clears_exec line 257
  31. def OAI.Fifths.SM.cleanup line 277

    Source documentation

    Wipe stacks and rewind public input, yielding the initial empty stack configuration (no arg tapes).

    noncomputable def cleanup [Fintype K] : SM X Empty K Unit := by
…

    Mentions: OAI.Fifths.SM

  32. theorem OAI.Fifths.SM.cleanup_exec line 280
  33. def OAI.Fifths.TM.subroutine line 302

    Source documentation

    Any ordinary space-bounded TM with small arguments can be used as a subroutine. The result is a binary stack machine seeing just the public input, expecting the (small) arguments from the caller on designated stacks. No length counter for x.

    noncomputable def subroutine : SM X Empty M.stkIdx Y :=
…

    Mentions: OAI.Fifths.SM

  34. theorem OAI.Fifths.TM.subroutine_exec line 304