feat(MultiTapeTM): TransformsTapes interface and sequential composition - #897
feat(MultiTapeTM): TransformsTapes interface and sequential composition#897crei wants to merge 1 commit into
Conversation
Introduce the word-level interface through which control-flow combinators use machines, the space-accounting lemmas it rests on, and sequential composition as the first non-trivial combinator over it. * `Plumbing/TransformsTapes.lean`: `tapeOfList` (a tape holding exactly a word), `wordsCfg` (a configuration whose tapes hold given words), `TransformsTapes` (started on word-holding tapes, halt in the normal form `wordsCfg input none ws' out` with the new words related to the old by a postcondition, within given time/space), its `.imp` weakening, and `exists_transformsTapes_nop` as the inhabiting example. * `Plumbing/Sequential.lean`: `transformsTapes_seq`, running one transformer then another. The halting configuration of the first is a valid starting configuration for the second, so the two chain by rewriting with the normal-form equality. * `TapeLemmas.lean`: add the visited-set / space-usage lemmas the interface needs (`visitedByTapeHead_add`, `spaceUsed_add_le`, `spaceUsed_eq_of_workTapePos`, `exists_visitedByTapeHead_eq_Icc`, `spaceUsed_le_of_one_moving`, ...). * `Configuration.lean`: add the state-remap embeddings `Cfg.mapState` and `Cfg.withState`, used to place a sub-machine's configurations into a larger one. * `Deterministic.lean`: add `runFrom_eq_of_halt` and `exists_minimal_halting_time`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Note that this conflicts with @SamuelSchlesinger 's PR sequence #871 #872 #873 #874 #875. I think it is useful to inject this layer of abstraction to simplify proofs down the line. This PR is a subset of an exploratory PR in my private fork where I validated the design by building combinators for function composition, loops and branches. |
| `∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine. -/ | ||
| def TransformsTapes (tm : MultiTapeTM k Symbol State) | ||
| (P : (input : List Symbol) → (Fin k → List Symbol) → Prop) | ||
| (Q : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop) |
There was a problem hiding this comment.
Could we maybe introduce abbrev Word := List Symbol?
There was a problem hiding this comment.
I'm not sure. If I read List Symbol I know what it is about. Word could be anything that resembles finite sequence (or maybe even infinite). It is kind of excessive in these two lines, but I think it's better to be explicit.
There was a problem hiding this comment.
That's fair, but we use word a lot in the documentation then we have List Symbol. It would be nice if the definitions read more like the documentation.
| (t s : ℕ) : Prop := | ||
| ∀ (input : List Symbol) (ws : Fin k → List Symbol) (out : List Symbol), P input ws → | ||
| ∃ τ ≤ t, ∃ ws', | ||
| tm.runFrom (wordsCfg input (some tm.q₀) ws out) τ = wordsCfg input none ws' out ∧ |
There was a problem hiding this comment.
I suspect the halting time witness is redundant here.
| /-- The machine that does nothing: it halts in one step, leaving every word as it was. Its | ||
| heads never move, so it visits one cell per tape. This is the first machine of the interface: it | ||
| checks that the specification format is inhabited exactly as intended. -/ | ||
| theorem exists_transformsTapes_nop (k : ℕ) (Symbol : Type*) : |
There was a problem hiding this comment.
If we expose nop we don't need the existential here.
|
|
||
| /-- The machine that does nothing: it halts on its first step, leaving the configuration | ||
| unchanged. -/ | ||
| private def nop (k : ℕ) (Symbol : Type*) : MultiTapeTM k Symbol Unit where |
There was a problem hiding this comment.
Please expose, Combinators will want the identity machine by name as the unit of seq.
| (hi_move : ∀ m ≤ t, lo ≤ (tm.runFrom cfg m).workTapePos i ∧ | ||
| (tm.runFrom cfg m).workTapePos i ≤ hi) | ||
| (hfixed : ∀ m ≤ t, ∀ j, j ≠ i → (tm.runFrom cfg m).workTapePos j = cfg.workTapePos j) : | ||
| tm.spaceUsed cfg t ≤ (hi + 1 - lo).toNat + k := by |
There was a problem hiding this comment.
The proof establishes k - 1, just tighten this up.
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
This will help substantially with my work, but please consider the changes I requested. Further, many of the definitions which are the same across my work and this one have had argument orders and names changed. Please justify in comments or align so the rebase can be easier.
2 participants
Introduce an abstraction over Turing machines that normalizes head positions and uses
List Symbolfor tape contents with a Hoare-style interface. This abstraction will be used by control-flow combinators to be introduced later.Here are the most important definitions and results:
Plumbing/TransformsTapes.lean:tapeOfList(a tape holding exactly a word),wordsCfg(a configuration whose tapes hold given words),TransformsTapes(started on word-holding tapes, halt in the normal formwordsCfg input none ws' outwith the new words related to the old by a postcondition, within given time/space), its.impweakening, andexists_transformsTapes_nopas the inhabiting example.Plumbing/Sequential.lean:transformsTapes_seq, running one transformer then another. The halting configuration of the first is a valid starting configuration for the second, so the two chain by rewriting with the normal-form equality.TapeLemmas.lean: add the visited-set / space-usage lemmas the interface needs (visitedByTapeHead_add,spaceUsed_add_le,spaceUsed_eq_of_workTapePos,exists_visitedByTapeHead_eq_Icc,spaceUsed_le_of_one_moving, ...).Configuration.lean: add the state-remap embeddingsCfg.mapStateandCfg.withState, used to place a sub-machine's configurations into a larger one.Deterministic.lean: addrunFrom_eq_of_haltandexists_minimal_halting_time.AI disclosure: Claude code was heavily used in a tight review loop.