OAI/Computability/SpaceSimulation/StackMachine.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

A finite-control intermediate machine with a fixed number of stacks. Stack alphabet binary, top at the start of the lists. We bound lengths per stack; the fixed number of stacks makes this sufficient.

  1. inductive OAI.Fifths.StOp line 10
  2. def OAI.Fifths.StOp.apply line 16

    Source documentation

    Popping empty is allowed and does nothing.

    def apply : StOp → List Bool → List Bool
  | keep, l => l
  | push b, l => b :: l
  | pop, l => l.tail
end StOp

    Mentions: OAI.Fifths.StOp

  3. structure OAI.Fifths.Store line 22
  4. structure OAI.Fifths.StChange line 26
  5. structure OAI.Fifths.SAction line 30
  6. def OAI.Fifths.StChange.none line 35
  7. def OAI.Fifths.SAction.withState line 41
  8. def OAI.Fifths.SAction.none line 42
  9. def OAI.Fifths.Store.init line 48
  10. def OAI.Fifths.Store.see line 51
  11. def OAI.Fifths.Store.perform line 54
  12. theorem OAI.Fifths.Store.stationary line 57
  13. def OAI.Fifths.Store.ok line 60
  14. theorem OAI.Fifths.Store.ok.mono line 62
  15. structure OAI.Fifths.SM line 67

    Source documentation

    Usage as bounded computations will have X,J,K and Y finite.

    structure SM (X J K Y : Type) where
…
  16. abbrev OAI.Fifths.SM.Cfg line 77
  17. def OAI.Fifths.SM.step line 79
  18. abbrev OAI.Fifths.SM.Run line 85

    Source documentation

    Auxiliary runs at any program counter.

    abbrev Run (i : Inputs X J) (B : ℕ) : M.Cfg → M.Cfg → Y → Prop :=
…

    Mentions: OAI.Fifths.Inputs

  19. def OAI.Fifths.SM.Exec line 88
  20. theorem OAI.Fifths.SM.Exec.startOk line 93
  21. theorem OAI.Fifths.SM.Exec.endOk line 97
  22. theorem OAI.Fifths.SM.Exec.mono line 101
  23. theorem OAI.Fifths.SM.Exec.unique line 105