-
Notifications
You must be signed in to change notification settings - Fork 197
feat(MultiTapeTM): add sequential composition and tape extension #871
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Closed
SamuelSchlesinger
wants to merge
2
commits into
samschles/tm-01-function-complexity
from
samschles/tm-02-basic-plumbing
Closed
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
66 changes: 66 additions & 0 deletions
66
Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Basic.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,66 @@ | ||
| /- | ||
| Copyright (c) 2026 Christian Reitwiessner. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Christian Reitwiessner, Samuel Schlesinger | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic | ||
|
|
||
| /-! # Configuration state replacement and execution paths | ||
|
|
||
| `Cfg.withState` changes the control state, possibly changing its type, and preserves all tapes, | ||
| head positions, and accumulated output. `runFrom_map` transports runs along maps that preserve | ||
| steps, and `runFrom_eq_of_isChain` identifies the endpoint of an explicit execution path. | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Turing.MultiTapeTM | ||
|
|
||
| variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} | ||
|
|
||
| /-- The configuration `cfg` with its state replaced by `q`, possibly over a different state | ||
| type. -/ | ||
| @[simps] | ||
| def Cfg.withState (cfg : Cfg k Symbol State input) {State' : Type*} | ||
| (q : Option State') : Cfg k Symbol State' input := | ||
| ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩ | ||
|
|
||
| @[simp] | ||
| lemma Cfg.withState_inputSymbol {cfg : Cfg k Symbol State input} {State' : Type*} | ||
| {q : Option State'} : (cfg.withState q).inputSymbol = cfg.inputSymbol := rfl | ||
|
|
||
| @[simp] | ||
| lemma Cfg.withState_workTapeSymbols {cfg : Cfg k Symbol State input} {State' : Type*} | ||
| {q : Option State'} : (cfg.withState q).workTapeSymbols = cfg.workTapeSymbols := rfl | ||
|
|
||
| @[simp] | ||
| lemma Cfg.withState_withState {cfg : Cfg k Symbol State input} {State' State'' : Type*} | ||
| {q : Option State'} {q' : Option State''} : | ||
| (cfg.withState q).withState q' = cfg.withState q' := rfl | ||
|
|
||
| @[simp] | ||
| lemma Cfg.withState_self {cfg : Cfg k Symbol State input} : | ||
| cfg.withState cfg.state = cfg := rfl | ||
|
|
||
| /-- A map that preserves steps maps every configuration of an execution. -/ | ||
| lemma runFrom_map {k' : ℕ} {Symbol' State' : Type*} {input' : List Symbol'} | ||
| (tm : MultiTapeTM k Symbol State) (tm' : MultiTapeTM k' Symbol' State') | ||
| (embed : Cfg k Symbol State input → Cfg k' Symbol' State' input') | ||
| (hstep : ∀ cfg, tm'.step (embed cfg) = embed (tm.step cfg)) | ||
| (cfg : Cfg k Symbol State input) (n : ℕ) : | ||
| tm'.runFrom (embed cfg) n = embed (tm.runFrom cfg n) := by | ||
| have h : Function.Semiconj embed tm.step tm'.step := fun cfg => (hstep cfg).symm | ||
| exact (h.iterate_right n cfg).symm | ||
|
|
||
| /-- An execution path ends at the configuration reached after one step per adjacent pair. -/ | ||
| lemma runFrom_eq_of_isChain (tm : MultiTapeTM k Symbol State) | ||
| {cfg cfg' : Cfg k Symbol State input} {path : List (Cfg k Symbol State input)} | ||
| (hpath : path.IsChainFromTo tm.TransitionRelation cfg cfg') : | ||
| tm.runFrom cfg (path.length - 1) = cfg' := by | ||
| apply (tm.relatesInSteps_iff_runFrom_eq cfg cfg' _).mp | ||
| exact hpath.relatesInSteps (by have := hpath.length_pos; omega) | ||
|
|
||
| end Turing.MultiTapeTM |
137 changes: 137 additions & 0 deletions
137
Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,137 @@ | ||
| /- | ||
| Copyright (c) 2026 Samuel Schlesinger. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Samuel Schlesinger | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic | ||
| public import Mathlib.Data.Fintype.Inv | ||
| public import Mathlib.Data.Fintype.Card | ||
|
|
||
| /-! | ||
| # Extending and reindexing work tapes | ||
|
|
||
| `extendTapes` embeds a machine's work tapes along an injection. The extra tapes are idle, and each | ||
| native step still takes exactly one step. The configuration embedding permits arbitrary contents | ||
| and head positions on the extra tapes, so the transformation also applies to intermediate runs. | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Turing.MultiTapeTM | ||
|
|
||
| variable {k k' : ℕ} {Symbol State : Type*} {input : List Symbol} | ||
|
|
||
| namespace ExtendTapes | ||
|
|
||
| /-- Extend a tape-indexed family along an injection, using `extra` outside its image. -/ | ||
| def extend {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) (extra : Fin k' → α) | ||
| (j : Fin k') : α := | ||
| if h : j ∈ Set.range e then values (e.invOfMemRange ⟨j, h⟩) else extra j | ||
|
|
||
| @[simp] | ||
| lemma extend_apply {α : Type*} (e : Fin k ↪ Fin k') (values : Fin k → α) | ||
| (extra : Fin k' → α) (i : Fin k) : extend e values extra (e i) = values i := by | ||
| simp [extend] | ||
|
|
||
| /-- Embed a native configuration while retaining arbitrary data on the unused tapes. -/ | ||
| def embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) | ||
| (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : | ||
| Cfg k' Symbol State input where | ||
| state := cfg.state | ||
| inputPos := cfg.inputPos | ||
| workTapes := extend e cfg.workTapes extraTapes | ||
| workTapePos := extend e cfg.workTapePos extraPos | ||
| output := cfg.output | ||
|
|
||
| end ExtendTapes | ||
|
|
||
| /-- Relabel the work tapes by an injection, leaving every tape outside its image idle. -/ | ||
| def extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : | ||
| MultiTapeTM k' Symbol State where | ||
| q₀ := tm.q₀ | ||
| tr q input work := | ||
| let action := tm.tr q input (work ∘ e) | ||
| ⟨action.inputMove, ExtendTapes.extend e action.workActions (fun _ => (none, 0)), | ||
| action.outS, action.q'⟩ | ||
|
|
||
| namespace ExtendTapes | ||
|
|
||
| variable (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') | ||
| variable (cfg : Cfg k Symbol State input) | ||
| variable (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) | ||
|
|
||
| /-- Tape extension preserves a step and every unused tape. -/ | ||
| lemma step_embed : | ||
| (tm.extendTapes e).step (embed e cfg extraTapes extraPos) = | ||
| embed e (tm.step cfg) extraTapes extraPos := by | ||
| have hwork : (embed e cfg extraTapes extraPos).workTapeSymbols ∘ e = cfg.workTapeSymbols := by | ||
| funext i | ||
| simp [embed, Cfg.workTapeSymbols] | ||
| cases hs : cfg.state with | ||
| | none => simp [step, embed, hs] | ||
| | some q => | ||
| simp only [step, embed, hs, extendTapes, Cfg.inputSymbol] at hwork ⊢ | ||
| rw [hwork] | ||
| apply Cfg.ext <;> try rfl | ||
| · funext j p | ||
| by_cases hj : j ∈ Set.range e | ||
| · obtain ⟨i, rfl⟩ := hj | ||
| simp [extend_apply] | ||
| · simp [extend, hj] | ||
| · funext j | ||
| by_cases hj : j ∈ Set.range e | ||
| · obtain ⟨i, rfl⟩ := hj | ||
| simp [extend_apply] | ||
| · simp [extend, hj] | ||
|
|
||
| /-- Tape extension maps each configuration of the native run, preserving the unused tapes. -/ | ||
| lemma runFrom_embed (n : ℕ) : | ||
| (tm.extendTapes e).runFrom (embed e cfg extraTapes extraPos) n = | ||
| embed e (tm.runFrom cfg n) extraTapes extraPos := | ||
| runFrom_map tm (tm.extendTapes e) (fun cfg => embed e cfg extraTapes extraPos) | ||
| (fun cfg => step_embed tm e cfg extraTapes extraPos) cfg n | ||
|
|
||
| /-- An injected tape visits exactly the native tape's positions. -/ | ||
| lemma spaceUsedByTape_embed (n : ℕ) (i : Fin k) : | ||
| (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n (e i) = | ||
| tm.spaceUsedByTape cfg n i := by | ||
| simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed] | ||
| simp only [embed, extend_apply] | ||
|
|
||
| /-- An unused tape visits just its initial cell. -/ | ||
| lemma spaceUsedByTape_extra (n : ℕ) (j : Fin k') (hj : j ∉ Set.range e) : | ||
| (tm.extendTapes e).spaceUsedByTape (embed e cfg extraTapes extraPos) n j = 1 := by | ||
| simp only [spaceUsedByTape, visitedByTapeHead, runFrom_embed] | ||
| simp [embed, extend, hj, Finset.image_const] | ||
|
|
||
| /-- The extra space is exactly one visited cell for each unused tape. -/ | ||
| lemma spaceUsed_embed (n : ℕ) : | ||
| (tm.extendTapes e).spaceUsed (embed e cfg extraTapes extraPos) n = | ||
| tm.spaceUsed cfg n + (k' - k) := by | ||
| unfold spaceUsed | ||
| rw [← Finset.sum_add_sum_compl (Finset.univ.map e)] | ||
| congr 1 | ||
| · simp [Finset.sum_map, spaceUsedByTape_embed] | ||
| · calc | ||
| _ = ∑ j ∈ (Finset.univ.map e)ᶜ, 1 := by | ||
| apply Finset.sum_congr rfl | ||
| intro j hj | ||
| exact spaceUsedByTape_extra tm e cfg extraTapes extraPos n j (by simpa using hj) | ||
| _ = k' - k := by simp [Finset.card_compl] | ||
|
|
||
| end ExtendTapes | ||
|
|
||
| /-- Starting with blank work tapes commutes with tape extension. -/ | ||
| lemma runFrom_extendTapes (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') | ||
| (input : List Symbol) (n : ℕ) : | ||
| (tm.extendTapes e).runFrom ((tm.extendTapes e).initCfg input) n = | ||
| ExtendTapes.embed e (tm.runFrom (tm.initCfg input) n) (fun _ _ => none) (fun _ => 0) := by | ||
| have hinit : (tm.extendTapes e).initCfg input = | ||
| ExtendTapes.embed e (tm.initCfg input) (fun _ _ => none) (fun _ => 0) := by | ||
| ext i p <;> simp [ExtendTapes.embed, ExtendTapes.extend, extendTapes] | ||
| rw [hinit, ExtendTapes.runFrom_embed] | ||
|
|
||
| end Turing.MultiTapeTM |
11 changes: 11 additions & 0 deletions
11
Cslib/Computability/Machines/Turing/MultiTape/Plumbing/README.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,11 @@ | ||
| # Machine transformations | ||
|
|
||
| These modules describe executable machines and their effects on configurations and `runFrom`. | ||
|
|
||
| - `Basic` changes a configuration's control state without changing its tapes, transports runs | ||
| along maps that preserve steps, and relates explicit execution paths to `runFrom`. | ||
| - `Sequential` runs machines with the same work-tape count consecutively. The first halting | ||
| transition hands its tapes, head positions, and accumulated output to the second machine, | ||
| which starts in its own fixed initial state. | ||
| - `ExtendTapes` places a machine's tapes along any injection. Time is unchanged; each unused tape | ||
| contributes one visited cell to space. Arbitrary data on unused tapes is preserved. |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not really related to this PR but should we change
haltsAtStepto use= noneas well? IshaltsAtStepuseful at all?