OAI/Computability/SpaceSimulation/Stack/PortIO.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

I/O adaptors. Scan the extra read-only tape into a stack; return the heads home. Terminal values of fixed bit bound can be returned directly in finite control.

  1. def OAI.Fifths.SM.inputSeek line 14
  2. def OAI.Fifths.SM.endStep line 17
  3. def OAI.Fifths.SM.readStep line 23
  4. def OAI.Fifths.SM.loader line 30
  5. def OAI.Fifths.SM.just line 33
  6. theorem OAI.Fifths.SM.just_ok line 36
  7. theorem OAI.Fifths.SM.loader_end line 41
  8. theorem OAI.Fifths.SM.loader_start line 84
  9. theorem OAI.Fifths.SM.exec_loader line 138
  10. def OAI.Fifths.SM.understand line 151

    Source documentation

    The (fixed) program is specialized to a maximum length.

    def understand (k : K) : ℕ → (List Bool → Y) → SM X J K Y
  | 0,d => pure (d [])
  | n+1,d => (pop k).bind fun
    | none => pure (d [])
    | some b => understand k n (fun l => d (b :: l))

-- Zero length when trivial case, get empty; also restore to empty.

    Mentions: OAI.Fifths.SM, OAI.Fifths.SM.pure, OAI.Fifths.SM.pop, OAI.Fifths.SM.bind

  11. theorem OAI.Fifths.SM.exec_understand line 158

    Source comment

    Zero length when trivial case, get empty; also restore to empty.
    theorem exec_understand {i : Inputs X J} {s : Store J K} {B} (k : K) (n : ℕ)
    (d : List Bool → Y) (o : s.ok B) (h : (s.st k).length ≤ n) :
    (understand k n d).Exec i B s (s.set k []) (d (s.st k)) := by
…

    Mentions: OAI.Fifths.Inputs, OAI.Fifths.Store, OAI.Fifths.SM.understand, OAI.Fifths.SM.Exec