diff --git a/Cslib.lean b/Cslib.lean index 8cfe47e01..ff72cef29 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -58,6 +58,8 @@ public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index 93e8aa70f..6c131577c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -148,6 +148,18 @@ def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Sy /-- A configuration is halted when it has no state to continue from. -/ abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none +/-- The same configuration in a different control state, possibly of 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⟩ + +/-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work +tapes, the work-tape heads and the output alone. This is the shape of embedding used to place a +sub-machine's configurations into a larger machine built from it. -/ +@[simps] def Cfg.mapState {State' : Type*} (φ : Option State → Option State') + (c : Cfg k Symbol State input) : Cfg k Symbol State' input := + ⟨φ c.state, c.inputPos, c.workTapes, c.workTapePos, c.output⟩ + /-- The initial configuration for a starting state and an input string. -/ @[simp] def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input := diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 602953c79..a587e2771 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -191,6 +191,26 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n tm.runFrom cfg n = cfg := Function.iterate_fixed (step_of_halt h) n +/-- Nothing changes after the machine has halted. -/ +lemma runFrom_eq_of_halt + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) + (hhalt : (tm.runFrom cfg τ).state = none) : + tm.runFrom cfg t = tm.runFrom cfg τ := by + conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] + rw [runFrom_add, runFrom_of_halt _ hhalt] + +/-- Every halted run has a first halting time no later than the supplied one. -/ +lemma exists_minimal_halting_time + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) (t : ℕ) + (hhalt : (tm.runFrom cfg t).state = none) : + ∃ u ≤ t, (tm.runFrom cfg u).state = none ∧ ∀ s < u, (tm.runFrom cfg s).state ≠ none := by + classical + have hex : ∃ n, (tm.runFrom cfg n).state = none := ⟨t, hhalt⟩ + exact ⟨Nat.find hex, Nat.find_min' hex hhalt, Nat.find_spec hex, + fun s hs => Nat.find_min hex hs⟩ + @[simp] lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : tm.outputSymbol cfg = none := by diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean new file mode 100644 index 000000000..b5722a468 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean @@ -0,0 +1,161 @@ +/- +Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. 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.Plumbing.TransformsTapes + +/-! +# Sequential composition of machines on shared tapes + +`seq tm₀ tm₁` behaves like `tm₀` until `tm₀` would halt, at which point it continues as `tm₁`, +started in its initial state on the tapes as `tm₀` left them. The state space is +`State₀ ⊕ State₁`, and the *halting transition* of the first phase is mapped to the initial state +of the second, so the handoff costs no extra step. + +At the specification level this is `transformsTapes_seq`: transformations compose, with the time +and space bounds adding. The postcondition of `TransformsTapes` is what makes the proof direct: +the first machine halts in a full `wordsCfg`, which is exactly a starting configuration for the +second. + +## Main results + +* `Turing.MultiTapeTM.seq`: the composed machine. +* `Turing.MultiTapeTM.transformsTapes_seq`: transformations compose, bounds adding. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol} + +/-- The sequential composition of `tm₀` and `tm₁`: it behaves like `tm₀` until `tm₀` would halt, +at which point it switches to the initial state of `tm₁` and behaves like `tm₁`. The switch is +folded into the halting transition of `tm₀`, so it costs no step. -/ +def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) : + MultiTapeTM k Symbol (State₀ ⊕ State₁) where + q₀ := .inl tm₀.q₀ + tr q inp work := + match q with + | .inl q₀ => + let a := tm₀.tr q₀ inp work + { a with state := some (a.state.elim (.inr tm₁.q₀) .inl) } + | .inr q₁ => + let a := tm₁.tr q₁ inp work + { a with state := a.state.map .inr } + +variable {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} + +namespace Sequential + +/-- A configuration of the first phase: a configuration of `tm₀`, with a halted state mapped to +the initial state of the second phase. Under this map, the whole first phase of `seq` mirrors the +run of `tm₀`, *including* its halting step. -/ +def leftCfg (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) : + Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.mapState (fun st => some (st.elim (.inr tm₁.q₀) .inl)) + +/-- A configuration of the second phase. Under this map, the second phase of `seq` mirrors the +run of `tm₁`. -/ +def rightCfg (cfg : Cfg k Symbol State₁ input) : + Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.mapState (Option.map .inr) + +lemma step_leftCfg (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) : + (tm₀.seq tm₁).step (leftCfg tm₁ cfg) = leftCfg tm₁ (tm₀.step cfg) := by + obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h + have h1 : (leftCfg tm₁ cfg).state = some (Sum.inl q : State₀ ⊕ State₁) := by + simp [leftCfg, Cfg.mapState, hq] + simp only [step, h1, hq] + rfl + +lemma step_rightCfg (cfg : Cfg k Symbol State₁ input) : + (tm₀.seq tm₁).step (rightCfg cfg) = rightCfg (tm₁.step cfg) := by + cases hq : cfg.state with + | none => + have h1 : (rightCfg (State₀ := State₀) cfg).state = none := by simp [rightCfg, Cfg.mapState, hq] + simp only [step, h1, hq] + | some q => + have h1 : (rightCfg (State₀ := State₀) cfg).state = some (Sum.inr q : State₀ ⊕ State₁) := by + simp [rightCfg, hq] + simp only [step, h1, hq] + rfl + +/-- The second phase of `seq` mirrors the run of `tm₁`. -/ +lemma runFrom_rightCfg (cfg : Cfg k Symbol State₁ input) (n : ℕ) : + (tm₀.seq tm₁).runFrom (rightCfg cfg) n = rightCfg (tm₁.runFrom cfg n) := + runFrom_comm_of_step rightCfg (fun c => step_rightCfg c) cfg n + +/-- While `tm₀` is running, `seq` mirrors it. -/ +lemma runFrom_leftCfg (cfg : Cfg k Symbol State₀ input) (n : ℕ) + (h : ∀ m < n, (tm₀.runFrom cfg m).state ≠ none) : + (tm₀.seq tm₁).runFrom (leftCfg tm₁ cfg) n = leftCfg tm₁ (tm₀.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => + rw [runFrom_succ_eq_step', runFrom_succ_eq_step', ih fun m hm => h m (by omega), + step_leftCfg _ (h n (by omega))] + +@[simp] +lemma workTapePos_leftCfg (cfg : Cfg k Symbol State₀ input) : + (leftCfg tm₁ cfg).workTapePos = cfg.workTapePos := rfl + +@[simp] +lemma workTapePos_rightCfg (cfg : Cfg k Symbol State₁ input) : + (rightCfg (State₀ := State₀) cfg).workTapePos = cfg.workTapePos := rfl + +end Sequential + +open Sequential in +/-- **Sequential composition of transformations.** If the postcondition of the first +transformation implies the precondition of the second, the composed machine performs the two +transformations one after the other, with the time and space bounds adding. -/ +theorem transformsTapes_seq + {P₀ P₁ : (input : List Symbol) → (Fin k → List Symbol) → Prop} + {Q₀ Q₁ : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop} + {t₀ s₀ t₁ s₁ : ℕ} + (h₀ : TransformsTapes tm₀ P₀ Q₀ t₀ s₀) (h₁ : TransformsTapes tm₁ P₁ Q₁ t₁ s₁) + (hmid : ∀ input ws ws', P₀ input ws → Q₀ input ws ws' → P₁ input ws') : + TransformsTapes (tm₀.seq tm₁) P₀ + (fun input ws ws'' => ∃ ws', Q₀ input ws ws' ∧ Q₁ input ws' ws'') + (t₀ + t₁) (s₀ + s₁) := by + intro input ws out hP₀ + obtain ⟨τ₀, hτ₀, ws', hrun₀, hQ₀, hspace₀⟩ := h₀ input ws out hP₀ + obtain ⟨τ₁, hτ₁, ws'', hrun₁, hQ₁, hspace₁⟩ := h₁ input ws' out (hmid input ws ws' hP₀ hQ₀) + -- the first halting time of the first machine + obtain ⟨u, hu, huhalt, huactive⟩ := exists_minimal_halting_time tm₀ + (wordsCfg input (some tm₀.q₀) ws out) τ₀ (by simp [hrun₀]) + have hu_run : tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) u = + wordsCfg input none ws' out := by + rw [← runFrom_eq_of_halt tm₀ _ hu huhalt, hrun₀] + -- the first phase mirrors the first machine, ending in the handoff configuration + have hleft : ∀ m ≤ u, (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) m + = leftCfg tm₁ (tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) m) := by + intro m hm + have : wordsCfg (State := State₀ ⊕ State₁) input (some (tm₀.seq tm₁).q₀) ws out = + leftCfg tm₁ (wordsCfg input (some tm₀.q₀) ws out) := rfl + rw [this, runFrom_leftCfg _ m fun r hr => + huactive r (by omega)] + -- the handoff configuration is the second machine's start, seen through the right embedding + have hhandoff : leftCfg tm₁ (tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) u) = + rightCfg (wordsCfg input (some tm₁.q₀) ws' out) := by + rw [hu_run] + rfl + refine ⟨u + τ₁, by omega, ws'', ?_, ⟨ws', hQ₀, hQ₁⟩, ?_⟩ + · rw [runFrom_add, hleft u le_rfl, hhandoff, runFrom_rightCfg, hrun₁] + rfl + · refine le_trans (spaceUsed_add_le _ _ _) (Nat.add_le_add ?_ ?_) + · -- the first phase visits what the first machine visits + refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ u fun m hm => ?_)) + (le_trans (spaceUsed_mono tm₀ _ hu) hspace₀) + rw [hleft m hm, workTapePos_leftCfg] + · -- the second phase visits what the second machine visits + rw [hleft u le_rfl, hhandoff] + refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ τ₁ fun m hm => ?_)) hspace₁ + rw [runFrom_rightCfg, workTapePos_rightCfg] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean new file mode 100644 index 000000000..4dcba97bf --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. 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.TapeLemmas + +/-! +# Machines as transformers of tape words + +The interface through which combinators use machines: a machine reads words from its work tapes +and leaves words on them. A combinator composing such machines talks about words only, never about +individual cells, head positions or the set of tapes a machine has touched. + +Configurations are described by *equalities*: `wordsCfg input q ws out` is the configuration whose +work tape `i` holds exactly the word `ws i` (contents `tapeOfList (ws i)`, head at the start), with +the input head at the start of the input and output `out`. A specification +`TransformsTapes tm P Q t s` says: started on word-holding tapes satisfying `P`, the machine halts +within `t` steps in the *normal form* `wordsCfg input none ws' out` (every head reset to its +initial position, tapes blank outside their words, output untouched), with the new words related to +the old ones by `Q` and using at most `s` work-tape cells. Requiring this normal form is what lets +specifications compose by rewriting: the halting configuration of one machine is already a valid +start for the next, so which words survived a step is read off the equation, not re-established cell +by cell. + +## Main definitions + +* `Turing.MultiTapeTM.tapeOfList`: the tape holding exactly a given word. +* `Turing.MultiTapeTM.wordsCfg`: the configuration whose tapes hold given words. +* `Turing.MultiTapeTM.TransformsTapes`: the specification format described above. + +## Main results + +* `Turing.MultiTapeTM.TransformsTapes.imp`: strengthen the precondition, weaken the postcondition + and raise the bounds. +* `Turing.MultiTapeTM.exists_transformsTapes_nop`: the machine that does nothing, the first + machine of the interface and the check that the format is inhabited as intended. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/ +def tapeOfList (xs : List Symbol) : ℤ → Option Symbol + | .ofNat n => xs[n]? + | .negSucc _ => none + +@[simp] +lemma tapeOfList_ofNat (xs : List Symbol) (n : ℕ) : tapeOfList xs n = xs[n]? := rfl + +@[simp] +lemma tapeOfList_negSucc (xs : List Symbol) (n : ℕ) : + tapeOfList xs (.negSucc n) = none := rfl + +/-- Appending one symbol writes precisely the cell after the existing word. -/ +lemma tapeOfList_append_single (xs : List Symbol) (x : Symbol) : + tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (xs.length : ℤ) (some x) := by + funext z + cases z with + | negSucc n => simp [tapeOfList] + | ofNat n => grind [tapeOfList] + +/-- The blank tape holds the empty word. -/ +@[simp] +lemma tapeOfList_nil : tapeOfList ([] : List Symbol) = fun _ => none := by + funext z + cases z <;> simp + +/-- The cell at position `0` holds the first symbol of the word. -/ +lemma tapeOfList_zero (xs : List Symbol) : tapeOfList xs 0 = xs.head? := by + have h : (0 : ℤ) = ((0 : ℕ) : ℤ) := rfl + rw [h, tapeOfList_ofNat] + cases xs <;> rfl + +/-- The configuration whose work tape `i` holds exactly the word `ws i` with its head at the +start, whose input head is at the start of the input, in state `q` with output `out`. -/ +@[simps] +def wordsCfg (input : List Symbol) (q : Option State) + (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input := + ⟨q, 1, fun i => tapeOfList (ws i), fun _ => 0, out⟩ + +/-- Remapping the state of a `wordsCfg` remaps its state and leaves the words alone. -/ +@[simp] +lemma mapState_wordsCfg {State' : Type*} (φ : Option State → Option State') + (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : + (wordsCfg input q ws out).mapState φ = wordsCfg input (φ q) ws out := rfl + +/-- The initial configuration is the word configuration with blank tapes and no output. -/ +lemma initCfg_eq_wordsCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) : + tm.initCfg input = wordsCfg input (some tm.q₀) (fun _ => []) [] := by + refine Cfg.ext rfl rfl ?_ rfl rfl + funext i + simp [Cfg.init, wordsCfg] + +/-- `TransformsTapes tm P Q t s`: started in its initial state on tapes holding words `ws` that +satisfy the precondition `P`, the machine halts after at most `t` steps in the configuration whose +tapes hold words `ws'` with `Q input ws ws'`, having used at most `s` work-tape cells. + +The bounds are numbers; a specification whose bounds depend on the data is a *family* +`∀ 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) + (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 ∧ + Q input ws ws' ∧ + tm.spaceUsed (wordsCfg input (some tm.q₀) ws out) τ ≤ s + +/-- A `TransformsTapes` statement can be read with a stronger precondition, a weaker postcondition +and larger bounds. -/ +theorem TransformsTapes.imp {tm : MultiTapeTM k Symbol State} + {P P' : (input : List Symbol) → (Fin k → List Symbol) → Prop} + {Q Q' : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop} + {t s t' s' : ℕ} (h : TransformsTapes tm P Q t s) + (hP : ∀ input ws, P' input ws → P input ws) + (hQ : ∀ input ws ws', P' input ws → Q input ws ws' → Q' input ws ws') + (ht : t ≤ t') (hs : s ≤ s') : + TransformsTapes tm P' Q' t' s' := by + intro input ws out hP' + obtain ⟨τ, hτ, ws', hrun, hQ', hspace⟩ := h input ws out (hP input ws hP') + exact ⟨τ, hτ.trans ht, ws', hrun, hQ input ws ws' hP' hQ', hspace.trans hs⟩ + +section Nop + +/-- 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 + q₀ := () + tr _ _ _ := { inputTape := 0, workTapes := fun _ => (none, 0), output := none, state := none } + +private lemma step_nop (ws : Fin k → List Symbol) (out : List Symbol) : + (nop k Symbol).step (wordsCfg input (some ()) ws out) = wordsCfg input none ws out := by + refine Cfg.ext rfl ?_ ?_ ?_ ?_ <;> + simp [step, nop, Action.apply, wordsCfg, SignType.cast] + +/-- 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*) : + ∃ (State : Type) (_ : Finite State) (tm : MultiTapeTM k Symbol State), + TransformsTapes tm (fun _ _ => True) (fun _ ws ws' => ws' = ws) 1 k := by + refine ⟨Unit, inferInstance, nop k Symbol, fun input ws out _ => ?_⟩ + have hrun : (nop k Symbol).runFrom (wordsCfg input (some ()) ws out) 1 = + wordsCfg input none ws out := by + rw [runFrom_succ_eq_step', runFrom_zero, step_nop] + -- the heads never move, so each tape touches only the single cell `0` + refine ⟨1, le_rfl, ws, hrun, rfl, spaceUsed_le_of_workTapePos_const _ 1 fun m hm => ?_⟩ + rcases (by omega : m = 0 ∨ m = 1) with rfl | rfl + · rw [runFrom_zero] + · rw [hrun]; funext i; simp only [wordsCfg_workTapePos] + +end Nop + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index b6a2574d3..c8df87ea2 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -148,4 +148,132 @@ lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State intro t t' h exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h) + +/-- The cells a run visits are the ones visited by its two halves. -/ +lemma visitedByTapeHead_add (cfg : Cfg k Symbol State input) (a b : ℕ) (i : Fin k) : + tm.visitedByTapeHead cfg (a + b) i = + tm.visitedByTapeHead cfg a i ∪ tm.visitedByTapeHead (tm.runFrom cfg a) b i := by + ext z + simp only [mem_visitedByTapeHead, Finset.mem_union] + constructor + · rintro ⟨r, hr, rfl⟩ + rcases Nat.lt_or_ge r (a + 1) with h | h + · exact Or.inl ⟨r, h, rfl⟩ + · exact Or.inr ⟨r - a, by omega, + by rw [← runFrom_add, show a + (r - a) = r from by omega]⟩ + · rintro (⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩) + · exact ⟨r, by omega, rfl⟩ + · exact ⟨a + r, by omega, by rw [runFrom_add]⟩ + +/-- Splitting a run into two phases can only overcount the cells it visits, since the two phases +may revisit each other's cells. -/ +lemma spaceUsed_add_le (cfg : Cfg k Symbol State input) (a b : ℕ) : + tm.spaceUsed cfg (a + b) ≤ tm.spaceUsed cfg a + tm.spaceUsed (tm.runFrom cfg a) b := by + rw [spaceUsed, spaceUsed, spaceUsed, ← Finset.sum_add_distrib] + refine Finset.sum_le_sum fun i _ => ?_ + rw [spaceUsedByTape, visitedByTapeHead_add] + exact Finset.card_union_le _ _ + +/-- Space usage only depends on where the work-tape heads are at each step, so two runs whose head +positions agree use the same space. This is what lets a machine be replaced by a simulation of +it. -/ +lemma spaceUsed_eq_of_workTapePos {State' : Type*} {input' : List Symbol} + {tm' : MultiTapeTM k Symbol State'} (cfg : Cfg k Symbol State input) + (cfg' : Cfg k Symbol State' input') (t : ℕ) + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos = (tm'.runFrom cfg' m).workTapePos) : + tm.spaceUsed cfg t = tm'.spaceUsed cfg' t := by + refine Finset.sum_congr rfl fun i _ => congrArg Finset.card (Finset.image_congr fun m hm => ?_) + exact congrFun (h m (Nat.lt_succ_iff.mp (Finset.mem_range.mp hm))) i + +/-- The cells a head visits between two moments of one run all lie in the visited set. -/ +lemma uIcc_workTapePos_subset_visitedByTapeHead_of_le (cfg : Cfg k Symbol State input) + (i : Fin k) {t₁ t₂ t : ℕ} (h₁ : t₁ ≤ t₂) (h₂ : t₂ ≤ t) : + Finset.uIcc ((tm.runFrom cfg t₁).workTapePos i) ((tm.runFrom cfg t₂).workTapePos i) + ⊆ tm.visitedByTapeHead cfg t i := by + intro z hz + have h := tm.uIcc_workTapePos_subset_visitedByTapeHead (tm.runFrom cfg t₁) i (t₂ - t₁) + rw [← runFrom_add, show t₁ + (t₂ - t₁) = t₂ from by omega] at h + have hsub : tm.visitedByTapeHead (tm.runFrom cfg t₁) (t₂ - t₁) i + ⊆ tm.visitedByTapeHead cfg t i := by + intro y hy + obtain ⟨m, hm, rfl⟩ := mem_visitedByTapeHead.mp hy + rw [← runFrom_add] + exact mem_visitedByTapeHead.mpr ⟨t₁ + m, by omega, rfl⟩ + exact hsub (h hz) + +/-- **A head's visited set is an interval**: a head path is connected, so the visited cells are +exactly the integers between the leftmost and the rightmost, and the starting cell is among +them. -/ +lemma exists_visitedByTapeHead_eq_Icc (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : + ∃ l r : ℤ, l ≤ cfg.workTapePos i ∧ cfg.workTapePos i ≤ r ∧ + tm.visitedByTapeHead cfg t i = Finset.Icc l r := by + have hne : (tm.visitedByTapeHead cfg t i).Nonempty := + ⟨cfg.workTapePos i, mem_visitedByTapeHead.mpr ⟨0, by omega, rfl⟩⟩ + have hmem : cfg.workTapePos i ∈ tm.visitedByTapeHead cfg t i := + mem_visitedByTapeHead.mpr ⟨0, by omega, rfl⟩ + refine ⟨(tm.visitedByTapeHead cfg t i).min' hne, (tm.visitedByTapeHead cfg t i).max' hne, + Finset.min'_le _ _ hmem, Finset.le_max' _ _ hmem, ?_⟩ + apply Finset.Subset.antisymm + · intro z hz + exact Finset.mem_Icc.mpr ⟨Finset.min'_le _ _ hz, Finset.le_max' _ _ hz⟩ + · intro z hz + obtain ⟨t₁, ht₁, hpos₁⟩ := mem_visitedByTapeHead.mp (Finset.min'_mem _ hne) + obtain ⟨t₂, ht₂, hpos₂⟩ := mem_visitedByTapeHead.mp (Finset.max'_mem _ hne) + have hzu : z ∈ Finset.uIcc ((tm.runFrom cfg t₁).workTapePos i) + ((tm.runFrom cfg t₂).workTapePos i) := by + rw [hpos₁, hpos₂, Finset.uIcc_of_le (Finset.min'_le _ _ (Finset.max'_mem _ hne))] + exact hz + rcases Nat.le_total t₁ t₂ with h | h + · exact tm.uIcc_workTapePos_subset_visitedByTapeHead_of_le cfg i h (by omega) hzu + · rw [Finset.uIcc_comm] at hzu + exact tm.uIcc_workTapePos_subset_visitedByTapeHead_of_le cfg i h (by omega) hzu + +/-- A run that never moves a work-tape head visits one cell per tape. -/ +lemma spaceUsed_le_of_workTapePos_const (cfg : Cfg k Symbol State input) (u : ℕ) + (h : ∀ m ≤ u, (tm.runFrom cfg m).workTapePos = cfg.workTapePos) : + tm.spaceUsed cfg u ≤ k := by + have hcard : ∀ i, tm.spaceUsedByTape cfg u i ≤ 1 := by + intro i + refine le_trans (Finset.card_le_card ?_) (le_of_eq (Finset.card_singleton + (cfg.workTapePos i))) + intro z hz + obtain ⟨m, hm, rfl⟩ := mem_visitedByTapeHead.mp hz + rw [h m (by omega)] + exact Finset.mem_singleton_self _ + calc tm.spaceUsed cfg u ≤ ∑ _i : Fin k, 1 := Finset.sum_le_sum fun i _ => hcard i + _ = k := by simp + +/-- Space bound for a run in which one head stays inside an interval and every other head is +fixed: the moving tape contributes the interval, each other tape a single cell. -/ +lemma spaceUsed_le_of_one_moving (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) + (lo hi : ℤ) + (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 + have hi_tape : tm.spaceUsedByTape cfg t i ≤ (hi + 1 - lo).toNat := by + refine le_trans (Finset.card_le_card ?_) (le_of_eq (Int.card_Icc lo hi)) + intro z hz + obtain ⟨m, hm, rfl⟩ := mem_visitedByTapeHead.mp hz + exact Finset.mem_Icc.mpr (hi_move m (by omega)) + have hj_tape : ∀ j ∈ Finset.univ.erase i, tm.spaceUsedByTape cfg t j ≤ 1 := by + intro j hj + have hji : j ≠ i := Finset.ne_of_mem_erase hj + refine le_trans (Finset.card_le_card ?_) (le_of_eq (Finset.card_singleton + (cfg.workTapePos j))) + intro z hz + obtain ⟨m, hm, rfl⟩ := mem_visitedByTapeHead.mp hz + rw [hfixed m (by omega) j hji] + exact Finset.mem_singleton_self _ + calc tm.spaceUsed cfg t + = tm.spaceUsedByTape cfg t i + + ∑ j ∈ Finset.univ.erase i, tm.spaceUsedByTape cfg t j := + (Finset.add_sum_erase _ _ (Finset.mem_univ i)).symm + _ ≤ (hi + 1 - lo).toNat + ∑ _j ∈ Finset.univ.erase i, 1 := + Nat.add_le_add hi_tape (Finset.sum_le_sum hj_tape) + _ ≤ (hi + 1 - lo).toNat + k := by + rw [← Finset.card_eq_sum_ones, Finset.card_erase_of_mem (Finset.mem_univ i), + Finset.card_univ, Fintype.card_fin] + omega + end Turing.MultiTapeTM