OAI/Computability/SpaceSimulation/Machine.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Finite table machines for the result. X is the public input alphabet (all uses for machines as space bounds have finite types); J indexes a fixed number of other read-only tapes, on a binary alphabet. Each read-only tape is endmarked and has one confined head. Work tapes for the simulator and accessor are two-way, with unit moves. Terminal output in a finite set may be specified in the transition table (equivalently transition to the associated halt state). TM transitions with writes write before moving.

Space convention is visited work cells (including the origin of each work tape), weighted by bits/symbol in the fixed alphabets, excluding read-only tapes. Since visited sets are intervals, we use a window certificate including all head positions during the run.

  1. inductive OAI.Fifths.Dir line 22

    Also declared: ComparatorChallenges/OneTapeSpace.lean:11 (same declaration text).

  2. instance OAI.Fifths.(instance at line 26) line 26
  3. def OAI.Fifths.Dir.delta line 30

    Also declared: ComparatorChallenges/OneTapeSpace.lean:18 (same declaration text).

  4. theorem OAI.Fifths.Dir.bounds line 35
  5. inductive OAI.Fifths.Mark line 40

    Source documentation

    Left endmarker at 0, then the word, then right endmarker.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:24 (same declaration text).

    inductive Mark (A : Type)
  | left
  | sym (a : A)
  | right
  deriving DecidableEq, Fintype

namespace Mark
variable {A : Type}
  6. def OAI.Fifths.Mark.see line 48

    Also declared: ComparatorChallenges/OneTapeSpace.lean:32 (same declaration text).

  7. theorem OAI.Fifths.Mark.see_zero line 55
  8. theorem OAI.Fifths.Mark.see_left line 56
  9. theorem OAI.Fifths.Mark.see_right line 61
  10. def OAI.Fifths.Mark.walk line 70

    Also declared: ComparatorChallenges/OneTapeSpace.lean:39 (same declaration text).

  11. theorem OAI.Fifths.Mark.walk_bound line 75
  12. inductive OAI.Fifths.Runs line 89

    Source documentation

    Deterministic halting runs. f s = inl y means the transition specifies halt with that label (no more working moves). P holds also at that final configuration.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:45 (same declaration text).

    inductive Runs {σ Y : Type} (f : σ → Y ⊕ σ) (P : σ → Prop) :
    σ → σ → Y → Prop
  | stop {s y} (ok : P s) (eqn : f s = Sum.inl y) : Runs f P s s y
  | step {s s' t y} (ok : P s) (eqn : f s = Sum.inr s')
      (tail : Runs f P s' t y) : Runs f P s t y

namespace Runs
variable {σ Y : Type} {f : σ → Y ⊕ σ} {P Q : σ → Prop} {s t : σ} {y : Y}
  13. theorem OAI.Fifths.Runs.mono line 97
  14. theorem OAI.Fifths.Runs.startOk line 102
  15. theorem OAI.Fifths.Runs.endOk line 103
  16. theorem OAI.Fifths.Runs.endStop line 104
  17. theorem OAI.Fifths.Runs.unique line 106
  18. structure OAI.Fifths.Inputs line 125

    Source documentation

    Common read-only inputs.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:51 (same declaration text).

    structure Inputs (X J : Type) where
…
  19. structure OAI.Fifths.Readers line 129

    Also declared: ComparatorChallenges/OneTapeSpace.lean:55 (same declaration text).

  20. structure OAI.Fifths.Reads line 133

    Also declared: ComparatorChallenges/OneTapeSpace.lean:59 (same declaration text).

  21. structure OAI.Fifths.Advances line 137

    Also declared: ComparatorChallenges/OneTapeSpace.lean:63 (same declaration text).

  22. def OAI.Fifths.Readers.home line 143

    Also declared: ComparatorChallenges/OneTapeSpace.lean:69 (same declaration text).

  23. def OAI.Fifths.Readers.see line 144

    Also declared: ComparatorChallenges/OneTapeSpace.lean:70 (same declaration text).

  24. def OAI.Fifths.Readers.walk line 147

    Also declared: ComparatorChallenges/OneTapeSpace.lean:72 (same declaration text).

  25. theorem OAI.Fifths.Readers.stationary line 150
  26. structure OAI.Fifths.Tape line 153

    Also declared: ComparatorChallenges/OneTapeSpace.lean:76 (same declaration text).

  27. structure OAI.Fifths.WriteMove line 157

    Also declared: ComparatorChallenges/OneTapeSpace.lean:80 (same declaration text).

  28. def OAI.Fifths.Tape.init line 163

    Also declared: ComparatorChallenges/OneTapeSpace.lean:86 (same declaration text).

  29. def OAI.Fifths.Tape.see line 164

    Also declared: ComparatorChallenges/OneTapeSpace.lean:87 (same declaration text).

  30. def OAI.Fifths.Tape.perform line 165

    Also declared: ComparatorChallenges/OneTapeSpace.lean:88 (same declaration text).

  31. structure OAI.Fifths.TAction line 169

    Also declared: ComparatorChallenges/OneTapeSpace.lean:92 (same declaration text).

  32. structure OAI.Fifths.TM line 176

    Source documentation

    Finiteness of X, J and Y supplied in main theorem. Finite functions in the table present no uniformity issue; all are fixed for the machine.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:97 (same declaration text).

    structure TM (X J Y : Type) where
…
  33. structure OAI.Fifths.TM.Cfg line 192

    Also declared: ComparatorChallenges/OneTapeSpace.lean:113 (same declaration text).

  34. def OAI.Fifths.TM.initial line 197

    Also declared: ComparatorChallenges/OneTapeSpace.lean:118 (same declaration text).

  35. def OAI.Fifths.TM.step line 200

    Also declared: ComparatorChallenges/OneTapeSpace.lean:121 (same declaration text).

  36. structure OAI.Fifths.TM.Window line 207

    Source documentation

    Per tape visited positions contained in [-l,h], both nonnegative.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:127 (same declaration text).

    structure Window where
…
  37. def OAI.Fifths.TM.width line 212

    Source documentation

    Bits per symbol (at least one).

    Also declared: ComparatorChallenges/OneTapeSpace.lean:131 (same declaration text).

    def width (k : M.K) : ℕ := max 1 (Fintype.card (M.W k) - 1).size
  38. theorem OAI.Fifths.TM.width_pos line 214
  39. def OAI.Fifths.TM.Window.ok line 220

    Also declared: ComparatorChallenges/OneTapeSpace.lean:135 (same declaration text).

  40. def OAI.Fifths.TM.Window.bits line 225

    Also declared: ComparatorChallenges/OneTapeSpace.lean:138 (same declaration text).

  41. theorem OAI.Fifths.TM.Window.span_le line 228
  42. def OAI.Fifths.TM.Within line 237

    Source documentation

    M outputs y using at most S bits.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:142 (same declaration text).

    def Within (i : Inputs X J) (y : Y) (S : ℕ) : Prop :=
…

    Mentions: OAI.Fifths.Inputs

  43. theorem OAI.Fifths.TM.Within.mono line 240
  44. theorem OAI.Fifths.TM.Within.unique line 245