OAI/Computability/RationalHitting/OutputAdapter.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Literal tape-preserving linkage for the raw-input/stack/output compiler. There is no implicit recoding between machines.

  1. abbrev OAI.RationalHitting.TMTime.OutputAdapter.A line 7
  2. abbrev OAI.RationalHitting.TMTime.OutputAdapter.Q line 8
  3. abbrev OAI.RationalHitting.TMTime.OutputAdapter.Word line 9
  4. abbrev OAI.RationalHitting.TMTime.OutputAdapter.V line 10
  5. abbrev OAI.RationalHitting.TMTime.OutputAdapter.Stmt line 11
  6. abbrev OAI.RationalHitting.TMTime.OutputAdapter.Cfg line 12
  7. def OAI.RationalHitting.TMTime.OutputAdapter.raw line 13
  8. def OAI.RationalHitting.TMTime.OutputAdapter.bit line 14
  9. def OAI.RationalHitting.TMTime.OutputAdapter.jump line 16
  10. def OAI.RationalHitting.TMTime.OutputAdapter.move line 17
  11. def OAI.RationalHitting.TMTime.OutputAdapter.leftTo line 18
  12. def OAI.RationalHitting.TMTime.OutputAdapter.readBlock line 21
  13. def OAI.RationalHitting.TMTime.OutputAdapter.block line 26
  14. def OAI.RationalHitting.TMTime.OutputAdapter.fill line 27
  15. lemma OAI.RationalHitting.TMTime.OutputAdapter.fill_apply line 30
  16. lemma OAI.RationalHitting.TMTime.OutputAdapter.fill_all line 39
  17. lemma OAI.RationalHitting.TMTime.OutputAdapter.head₂ line 43
  18. lemma OAI.RationalHitting.TMTime.OutputAdapter.right₂ line 44
  19. lemma OAI.RationalHitting.TMTime.OutputAdapter.left₂ line 46
  20. lemma OAI.RationalHitting.TMTime.OutputAdapter.left_empty line 48
  21. lemma OAI.RationalHitting.TMTime.OutputAdapter.write₂ line 50
  22. lemma OAI.RationalHitting.TMTime.OutputAdapter.bit_beq_one line 52
  23. lemma OAI.RationalHitting.TMTime.OutputAdapter.bit_ne_three line 53
  24. lemma OAI.RationalHitting.TMTime.OutputAdapter.raw_ne_three line 54
  25. lemma OAI.RationalHitting.TMTime.OutputAdapter.readBlock_spec line 56
  26. def OAI.RationalHitting.TMTime.OutputAdapter.M line 68
  27. def OAI.RationalHitting.TMTime.OutputAdapter.state line 83
  28. def OAI.RationalHitting.TMTime.OutputAdapter.invariant line 84
  29. lemma OAI.RationalHitting.TMTime.OutputAdapter.scan_right line 87
  30. lemma OAI.RationalHitting.TMTime.OutputAdapter.scan_left line 98
  31. lemma OAI.RationalHitting.TMTime.OutputAdapter.zeros_cons line 114
  32. lemma OAI.RationalHitting.TMTime.OutputAdapter.consume_some line 120
  33. lemma OAI.RationalHitting.TMTime.OutputAdapter.emit_one line 130
  34. lemma OAI.RationalHitting.TMTime.OutputAdapter.consume_none line 175
  35. lemma OAI.RationalHitting.TMTime.OutputAdapter.clear_blanks line 190
  36. lemma OAI.RationalHitting.TMTime.OutputAdapter.finish line 200
  37. def OAI.RationalHitting.TMTime.OutputAdapter.stream line 241
  38. def OAI.RationalHitting.TMTime.OutputAdapter.cost line 245
  39. lemma OAI.RationalHitting.TMTime.OutputAdapter.decode_stream line 249
  40. lemma OAI.RationalHitting.TMTime.OutputAdapter.cost_bound line 268
  41. lemma OAI.RationalHitting.TMTime.OutputAdapter.start line 287
  42. theorem OAI.RationalHitting.TMTime.OutputAdapter.prepare line 295

    Source documentation

    Literal block input to literal digit output; both head position and blank outside the output are guaranteed, with quadratic bit-time.

    theorem prepare {b} (hb : 1≤b) (get : Word b → Option Bool)
    (code : Bool → Bool → Word b) (stop : Bool → Word b)
    (hc : ∀ f x,get (code f x)=some x) (hs : ∀ f,get (stop f)=none)
    (xs : List Bool) :
    ∃ t≤(3*b+34)*(xs.length+1)^2, ∃ u : V b,
      exec (TM1.step (M get)) t (TM1.init (stream code stop true xs))=
        some ⟨none,u,Tape.mk₁ (xs.map raw)⟩ := by
…

    Mentions: OAI.RationalHitting.TMTime.OutputAdapter.Word, OAI.RationalHitting.TMTime.OutputAdapter.code, OAI.RationalHitting.TMTime.OutputAdapter.stop, OAI.RationalHitting.TMTime.OutputAdapter.V, OAI.RationalHitting.TMTime.exec, OAI.RationalHitting.TMTime.OutputAdapter.M, OAI.RationalHitting.TMTime.OutputAdapter.stream, OAI.RationalHitting.TMTime.OutputAdapter.raw

  43. theorem OAI.RationalHitting.TMTime.OutputAdapter.finite_output line 311

    Source documentation

    A genuine Fin4 finite TM0 output transducer; the encoding/decoding functions are fixed finite tables and no unbounded state or oracle is used.

    theorem finite_output {b} (hb : 1≤b) (get : Word b → Option Bool)
    (code : Bool → Bool → Word b) (stop : Bool → Word b)
    (hc : ∀ f x,get (code f x)=some x) (hs : ∀ f,get (stop f)=none) :
    ∃ (m : ℕ) (G : TM0.Machine A (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ xs : List Bool, ∃ t≤C*(xs.length+1)^2, ∃ a,
        exec (TM0.step G) t (TM0.init (stream code stop true xs))=some a ∧
        TM0.step G a=none ∧ a.Tape=Tape.mk₁ (xs.map raw) := by
…

    Mentions: OAI.RationalHitting.TMTime.OutputAdapter.Word, OAI.RationalHitting.TMTime.OutputAdapter.code, OAI.RationalHitting.TMTime.OutputAdapter.stop, OAI.RationalHitting.TMTime.OutputAdapter.A, OAI.RationalHitting.TMTime.exec, OAI.RationalHitting.TMTime.OutputAdapter.stream, OAI.RationalHitting.TMTime.OutputAdapter.raw

  44. lemma OAI.RationalHitting.TMTime.StackTape.unique line 333

    Source documentation

    At the boundary of a stack macrostep, the simulator's tape is determined by the actual stack contents. There is no junk-cell assumption.

    lemma unique {K Λ σ : Type*} {Γ : K → Type*}
    {a b : TM2.Cfg Γ Λ σ} {c d : TM1.Cfg (TM2to1.Γ' K Γ) (TM2to1.Λ' K Γ Λ σ) σ}
    (h : TM2to1.TrCfg a c) (h' : TM2to1.TrCfg b d) (hs : a.stk=b.stk) : c.Tape=d.Tape := by
…
  45. lemma OAI.RationalHitting.TMTime.StackTape.clean line 349
  46. lemma OAI.RationalHitting.TMTime.OutputAdapter.blockVector line 362
  47. abbrev OAI.RationalHitting.TMTime.OutputAdapter.StackAlphabet line 371
  48. def OAI.RationalHitting.TMTime.OutputAdapter.code line 372
  49. def OAI.RationalHitting.TMTime.OutputAdapter.stop line 374
  50. def OAI.RationalHitting.TMTime.OutputAdapter.getter line 377
  51. lemma OAI.RationalHitting.TMTime.OutputAdapter.getter_code line 380
  52. lemma OAI.RationalHitting.TMTime.OutputAdapter.getter_stop line 387
  53. lemma OAI.RationalHitting.TMTime.OutputAdapter.stream_false line 399
  54. lemma OAI.RationalHitting.TMTime.OutputAdapter.stream_encoding line 408
  55. lemma OAI.RationalHitting.TMTime.OutputAdapter.width_pos line 438
  56. theorem OAI.RationalHitting.TMTime.OutputAdapter.raw_stack_output line 453

    Source documentation

    Exact inverse interface for a clean output stack, including the bottom marker, right-side blank padding and output order.

    theorem raw_stack_output {b} (k : K) (enc : StackAlphabet K → List.Vector Bool b)
    (dec : List.Vector Bool b → StackAlphabet K) (h0 : enc default=List.Vector.replicate b false)
    (hd : ∀ a,dec (enc a)=a) :
    ∃ (m : ℕ) (G : TM0.Machine A (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ xs : List Bool, ∃ t≤C*(xs.length+1)^2, ∃ a,
        exec (TM0.step G) t (TM0.init
          (((TM2to1.trInit k xs.reverse).flatMap (fun z => (enc z).toList)).map bit))=some a ∧
        TM0.step G a=none ∧ a.Tape=Tape.mk₁ (xs.map raw) := by
…

    Mentions: OAI.RationalHitting.TMTime.OutputAdapter.StackAlphabet, OAI.RationalHitting.TMTime.OutputAdapter.A, OAI.RationalHitting.TMTime.exec, OAI.RationalHitting.TMTime.OutputAdapter.bit, OAI.RationalHitting.TMTime.OutputAdapter.raw