feat(MultiTapeTM): add sequential composition and tape extension - #871
feat(MultiTapeTM): add sequential composition and tape extension#871SamuelSchlesinger wants to merge 2 commits into
Conversation
| /-- Every padded halting run has a least halting time. -/ | ||
| lemma exists_minimal_halting_time (tm : MultiTapeTM k Symbol State) | ||
| (cfg : Cfg k Symbol State input) (t : ℕ) | ||
| (hhalt : (tm.runFrom cfg t).state = none) : |
There was a problem hiding this comment.
Not really related to this PR but should we change haltsAtStep to use = none as well? Is haltsAtStep useful at all?
| (q : Option State') : Cfg k Symbol State' input := | ||
| ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩ | ||
|
|
||
| @[simp] |
There was a problem hiding this comment.
I think we should be able to obtain most of these by adding @[simps] to Cfg.withState.
|
|
||
| /-- A family of configurations with the prescribed steps agrees with `runFrom`. -/ | ||
| lemma runFrom_eq_of_step (tm : MultiTapeTM k Symbol State) | ||
| (path : ℕ → Cfg k Symbol State input) (n : ℕ) |
There was a problem hiding this comment.
Would it be easier to use List (Cfg k Symbol State input) here instead of path and n?
There was a problem hiding this comment.
also hstep should be List.IsChain for the transition relation.
| · funext j p | ||
| by_cases hj : j ∈ Set.range e | ||
| · obtain ⟨i, rfl⟩ := hj | ||
| simp only [extend_apply] |
| simp only [extend_apply] | ||
| · simp [extend, hj] | ||
|
|
||
| /-- Extending the tape count does not change the execution time. -/ |
There was a problem hiding this comment.
This proves much more: It shows how to map every element of an execution path.
| `seq` runs two machines with the same work-tape count. The transition that would halt the first | ||
| machine instead enters the second machine's initial state. Tape contents, head positions, and | ||
| accumulated output are carried across, with no extra transition for the handoff. | ||
| -/ |
There was a problem hiding this comment.
We could also add: No information is passed via the finite state.
|
|
||
| variable {k : ℕ} {Symbol State State₀ State₁ : Type*} {input : List Symbol} | ||
|
|
||
| /-- Run two machines on the same tapes, handing off on the first halting transition. -/ |
There was a problem hiding this comment.
| /-- Run two machines on the same tapes, handing off on the first halting transition. -/ | |
| /-- Run two machines sequentially on the same tapes, handing off on the first halting transition. -/ |
| q₀ := .inl tm₀.q₀ | ||
| tr q input work := match q with | ||
| | .inl q => | ||
| let out := tm₀.tr q input work |
There was a problem hiding this comment.
not sure if the rename was already merged but we call this "Action" now instead of 'TransitionOut' (it was a non-descriptive name and clashes with the "output symbol"), so maybe rename out -> action.
|
|
||
| end Sequential | ||
|
|
||
| /-- Sequential execution splits at the first machine's earliest halt. The second machine receives |
There was a problem hiding this comment.
Oh wow, this file is super short! Nice!
2 participants
Add sequential execution for machines with the same work-tape count and tape extension along an injection. Prove their
runFrombehavior, including preservation of unused tapes and the exact space cost of extension.Part 2/6 of the TM composition stack. Depends on #870. Next: #872.
Validation: strict build, import checks, full tests, and linters.
This PR was composed with Astra via Codex.