From 43fdfd4c91e7566862c5e3b7837702da3246e982 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan <46134216+barni120400@users.noreply.github.com> Date: Sun, 18 Oct 2026 17:48:05 +0300 Subject: [PATCH] refactor(MultiTape): remove the deterministic space measures Space is counted only on run and computation paths. The visitation and displacement lemmas hold for the run paths of nondeterministic machines, and the configuration bounds take `RunsInSpace` and count the storages and cores at the ends of computation paths: the computation paths of a deterministic machine are prefixes of one another, so the one visiting the most cells contains the windows of every other. The deterministic `visitedByTapeHead`, `spaceUsedByTape` and `space` go, with their lemmas and the unused `core_step_eq_of_core_eq`. Co-Authored-By: Claude Opus 5.5 --- .../Turing/MultiTape/ConfigBound.lean | 84 +++---- .../Turing/MultiTape/Deterministic.lean | 69 ++---- .../Machines/Turing/MultiTape/Space.lean | 34 +++ .../Machines/Turing/MultiTape/TapeLemmas.lean | 233 ++++++------------ 4 files changed, 179 insertions(+), 241 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean index 74303c236e..b23837b349 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean @@ -30,8 +30,8 @@ The results are layered, from the purely combinatorial to the machine-specific: * `MultiTapeTM.encard_fitsIn_le` is a counting statement about the type `Storage` alone and does not mention Turing machines: a memory whose non-blank cells and heads stay within per-tape windows of total size `s` can hold at most `storageBound Symbol State k s` different values. -* `MultiTapeTM.storage_fitsIn` is the geometric input: the storage reached after `t` steps stays - within the windows given by the space used up to step `t`. +* `MultiTapeNTM.ComputationPath.storage_fitsIn` is the geometric input: the storage at the end of a + computation path stays within the windows given by the per-tape space of the path. * `MultiTapeTM.encard_storages_le` combines the two: a machine bounded by space `s` passes through at most `storageBound Symbol State k s` storages *during its whole run*, no matter how long it runs and how long its input is. This is the form needed for arguments below logarithmic space, @@ -62,8 +62,9 @@ alphabet exponent. We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used area, but this is absorbed by the `O(s)` exponent in the final bound. -The windows for a whole run are available because a machine that is space-bounded at every point in -time attains its per-tape space usage at a single step (`MultiTapeTM.exists_spaceUsedByTape_max`). +The windows for a whole run are available because the computation paths of a deterministic +machine are prefixes of one another, so the one visiting the most cells contains the windows of +every other (`MultiTapeNTM.ComputationPath.spaceUsedByTape_le_of_space_le`). -/ @[expose] public section @@ -247,63 +248,58 @@ def Cfg.core (c : Cfg k Symbol State input) : Fin (input.length + 2) × Storage Symbol State k := (c.inputPos, c.storage) -/-- `step` never reads the output tape, so the core of the next configuration is determined by the -core of the current one. -/ -lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) : - (tm.step c₁).core = (tm.step c₂).core := by - rcases c₁ with ⟨q₁, i₁, w₁, p₁, out₁⟩ - rcases c₂ with ⟨q₂, i₂, w₂, p₂, out₂⟩ - simp only [Cfg.core, Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h - obtain ⟨rfl, rfl, rfl, rfl⟩ := h - cases q₁ with - | none => rw [MultiTapeTM.step_of_halt rfl, MultiTapeTM.step_of_halt rfl]; rfl - | some q => rw [MultiTapeTM.step_of_state rfl, MultiTapeTM.step_of_state rfl]; rfl - /-! ## The storages and cores of a space-bounded run These are the main results giving upper bounds on the number of storages and configuration cores reachable in bounded space. -/ -namespace MultiTapeTM +namespace MultiTapeNTM -/-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up -to step `t`. -/ -lemma storage_fitsIn (t : ℕ) : - (tm.runFrom (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) t) := by - constructor - · intro j - simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited - (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j) - · intro j - exact content_natAbs_le_spaceUsedByTape t +/-- The storage at the end of a computation path fits in the windows given by its per-tape space: +the tapes start blank, with every head at `0`. -/ +lemma ComputationPath.storage_fitsIn {ntm : MultiTapeNTM k Symbol State} + (p : ntm.ComputationPath input) : p.last.storage.FitsIn p.spaceUsedByTape := by + refine ⟨fun j => ?_, fun j z hz => ?_⟩ + · simpa [Cfg.storage, p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using + RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath + ((RunPath.mem_visitedByTapeHead _).mpr ⟨_, RelSeries.last_mem _, rfl⟩) + · simpa [p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using + RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath + (RunPath.mem_visitedByTapeHead_of_workTapes_ne _ + (by simpa [p.head_eq, Cfg.init, Cfg.storage] using hz)) + +end MultiTapeNTM + +namespace MultiTapeTM /-- A machine that uses at most `s` cells of work-tape space at every point in time passes through at most `storageBound Symbol State k s` different storages during its whole run — independently of the length of the input and of how long it runs. -/ theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ} - (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) : - (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard + (hs : tm.RunsInSpace input s) : + (Set.range fun p : tm.ComputationPath input => p.last.storage).encard ≤ storageBound Symbol State k s := by - obtain ⟨T, hT⟩ := tm.exists_spaceUsedByTape_max (tm.initCfg input) hs - refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs T)) - rintro _ ⟨t, rfl⟩ - exact Storage.FitsIn_mono (fun i => hT t i) (tm.storage_fitsIn t) + -- every storage fits in the windows of a computation path visiting the most cells + obtain ⟨p, hp⟩ := hs.exists_space_max + refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs p)) + rintro _ ⟨q, rfl⟩ + exact Storage.FitsIn_mono (q.spaceUsedByTape_le_of_space_le (hp q)) q.storage_fitsIn /-- The number of configuration cores that a machine bounded by space `s` can reach is at most `(n + 2) * storageBound Symbol State k s`, where `n` is the length of the input. -/ theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ} - (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) : - (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard + (hs : tm.RunsInSpace input s) : + (Set.range fun p : tm.ComputationPath input => p.last.core).encard ≤ (input.length + 2) * storageBound Symbol State k s := by - calc (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard + calc (Set.range fun p : tm.ComputationPath input => p.last.core).encard ≤ ((Set.univ : Set (Fin (input.length + 2))) - ×ˢ (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage)).encard := by + ×ˢ (Set.range fun p : tm.ComputationPath input => p.last.storage)).encard := by apply Set.encard_le_encard - rintro _ ⟨t, rfl⟩ - exact ⟨Set.mem_univ _, t, rfl⟩ + rintro _ ⟨p, rfl⟩ + exact ⟨Set.mem_univ _, p, rfl⟩ _ = (Set.univ : Set (Fin (input.length + 2))).encard - * (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard := Set.encard_prod + * (Set.range fun p : tm.ComputationPath input => p.last.storage).encard := Set.encard_prod _ ≤ (input.length + 2) * storageBound Symbol State k s := by refine mul_le_mul' ?_ (tm.encard_storages_le hs) simp [Set.encard_univ, ENat.card_eq_coe_fintype_card] @@ -312,8 +308,8 @@ theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ} passes through is at most `2 ^ (O(s))`, with constants depending only on the machine. -/ theorem encard_storages_le_pow [Finite Symbol] [Finite State] : ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ), - (∀ t, tm.space (tm.initCfg input) t ≤ s) → - (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard ≤ a * 2 ^ (c * s) := by + tm.RunsInSpace input s → + (Set.range fun p : tm.ComputationPath input => p.last.storage).encard ≤ a * 2 ^ (c * s) := by have : Fintype Symbol := Fintype.ofFinite Symbol have : Fintype State := Fintype.ofFinite State obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k) @@ -325,8 +321,8 @@ is at most `(n + 2) * 2 ^ (O(s))`, with constants depending only on the machine input. -/ theorem encard_cores_le_pow [Finite Symbol] [Finite State] : ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ), - (∀ t, tm.space (tm.initCfg input) t ≤ s) → - (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard + tm.RunsInSpace input s → + (Set.range fun p : tm.ComputationPath input => p.last.core).encard ≤ (input.length + 2) * a * 2 ^ (c * s) := by have : Fintype Symbol := Fintype.ofFinite Symbol have : Fintype State := Fintype.ofFinite State diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 84db17a4fe..33afcdebb2 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -34,7 +34,6 @@ We define a number of structures and concepts related to multi-tape Turing machi * `step`, `runFrom`: the successor configuration and iteration of this function * `MultiTapeNTM.RunPath.ofDeterministic`, `MultiTapeNTM.ComputationPath.ofDeterministic`: paths of a given length from an arbitrary or initial configuration -* `space`: the space of the path of the first `t` steps from a configuration * `Computes`: the machine halts with the given output on an input * `ComputesInTimeAndSpace`: the machine produces an output within the shared resource bounds * `ComputesFunInTimeAndSpace`: function computation with the shared time and space bounds @@ -225,6 +224,32 @@ lemma ComputationPath.eq_ofDeterministic (p : tm.ComputationPath input) : congr 1 exact (RunPath.eq_ofDeterministic p).trans (by rw [hp]; rfl) +/-- Deterministic run paths from the same configuration are prefixes of one another: the shorter one +is the longer one, cut at its length. -/ +lemma RunPath.eq_take {p q : tm.RunPath input} (hhead : p.head = q.head) (h : p.length ≤ q.length) : + p = q.take ⟨p.length, Nat.lt_succ_of_le h⟩ := by + refine p.eq_ofDeterministic.trans ((eq_ofDeterministic (q.take _)).trans ?_).symm + rw [RelSeries.head_take, hhead] + rfl + +/-- The computation paths of a deterministic machine are prefixes of one another, so a path visiting +at most as many cells as another visits at most as many on each tape. -/ +lemma ComputationPath.spaceUsedByTape_le_of_space_le (p : tm.ComputationPath input) + {q : tm.ComputationPath input} (h : p.space ≤ q.space) : + p.spaceUsedByTape ≤ q.spaceUsedByTape := by + -- a shorter path is a prefix of a longer one, so it visits fewer cells on each tape + have hmono {p q : tm.ComputationPath input} (h : p.time ≤ q.time) : + p.spaceUsedByTape ≤ q.spaceUsedByTape := fun i => by + change RunPath.spaceUsedByTape p.toRunPath i ≤ RunPath.spaceUsedByTape q.toRunPath i + rw [RunPath.eq_take (by rw [p.head_eq, q.head_eq]) h] + exact Finset.card_le_card (RunPath.visitedByTapeHead_take_subset _ _ i) + rcases le_total p.time q.time with hpq | hqp + · exact hmono hpq + -- a longer `p` visits no more cells than `q`, so it visits exactly those of `q` + have h : ∑ j, p.spaceUsedByTape j ≤ ∑ j, q.spaceUsedByTape j := h + exact fun i => ((Finset.sum_eq_sum_iff_of_le fun j _ => hmono hqp j).mp + (le_antisymm (Finset.sum_le_sum fun j _ => hmono hqp j) h) i (Finset.mem_univ i)).ge + /-- A step-preserving map sends the path of `t` steps from `cfg` to the path of `t` steps from the image of `cfg`. -/ lemma RunPath.map_ofDeterministic {k' : ℕ} {State' : Type*} {input' : List Symbol} @@ -281,48 +306,6 @@ lemma runsInTime_of_halted {input : List Symbol} {t : ℕ} rw [computationPath_last_eq_runFrom p, runFrom_eq_of_halt _ _ hp h] exact h -/-- The work-tape head moves by at most one cell in a single step. -/ -lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : - |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by - cases hstate : c.state with - | none => simp [step_of_halt hstate] - | some q => rw [step_of_state hstate]; exact workTapePos_apply_le _ c i - -section Space -/-! Now we define space usage and add some helper lemmas. -/ - -/-- The set of positions visited by the head of work tape `i` in the computation starting from -configuration `cfg` up to step `t`. -/ -noncomputable def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - Finset ℤ := - Finset.univ.image fun n : Fin (t + 1) => (tm.runFrom cfg n).workTapePos i - -/-- -The number of work tape cells visited by the head of tape `i` in the computation starting from -configuration `cfg` up to step `t`. --/ -noncomputable def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ := - (tm.visitedByTapeHead cfg t i).card - -/-- The number of work tape cells visited in the first `t` steps from `cfg`: the space of the path -of these steps. -/ -noncomputable abbrev space (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := - (MultiTapeNTM.RunPath.ofDeterministic tm cfg t).space - -/-- A zero-tape Turing machine uses zero space. -/ -@[simp] -lemma space_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) : - tm.space cfg t = 0 := by - subst h_zero - simp [MultiTapeNTM.RunPath.space] - -/-- Each tape's space usage is bounded by the total space used. -/ -lemma spaceUsedByTape_le_space (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - tm.spaceUsedByTape cfg t i ≤ tm.space cfg t := - Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i) - -end Space - /-- In `t` steps the input head moves at most `t` positions to the right. -/ lemma inputPos_runFrom_le (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Space.lean b/Cslib/Computability/Machines/Turing/MultiTape/Space.lean index e119511cb6..330a56806c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Space.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Space.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Data.Int.Interval +public import Mathlib.Order.Lattice.Nat public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic /-! @@ -98,6 +99,25 @@ lemma space_le_of_subset {p q : ntm.RunPath input} (h : ∀ c ∈ q, c ∈ p) : let ⟨n, hn⟩ := h c hc hn ▸ Finset.mem_image_of_mem _ (Finset.mem_univ n) +/-- A path visits exactly the head positions of its configurations. -/ +@[simp] +lemma mem_visitedByTapeHead (p : ntm.RunPath input) {i : Fin k} {z : ℤ} : + z ∈ p.visitedByTapeHead i ↔ ∃ c ∈ p, c.workTapePos i = z := by + simp [visitedByTapeHead, RelSeries.mem_def] + +/-- A prefix of a path visits only cells that the path visits. -/ +lemma visitedByTapeHead_take_subset (p : ntm.RunPath input) (j : Fin (p.length + 1)) (i : Fin k) : + visitedByTapeHead (p.take j) i ⊆ p.visitedByTapeHead i := + Finset.image_subset_iff.mpr fun n _ => + p.mem_visitedByTapeHead.mpr ⟨_, ⟨Fin.castLE j.isLt n, rfl⟩, rfl⟩ + +/-- Extending a path by a configuration visits its head positions as well. -/ +lemma visitedByTapeHead_snoc (p : ntm.RunPath input) (c : Cfg k Symbol State input) + (h : ntm.Step p.last c) (i : Fin k) : + visitedByTapeHead (p.snoc c h) i = insert (c.workTapePos i) (p.visitedByTapeHead i) := by + ext z + simp [RelSeries.mem_snoc, or_and_right, exists_or, eq_comm, or_comm] + /-! ### Windows -/ /-- Every head stays within the window `[-s, s]` along the path. -/ @@ -140,6 +160,10 @@ lemma space_map_le (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.st end RunPath +/-- The number of positions visited by the head of work tape `i` along a computation path. -/ +def ComputationPath.spaceUsedByTape (p : ntm.ComputationPath input) (i : Fin k) : ℕ := + RunPath.spaceUsedByTape p.toRunPath i + /-- The number of work tape cells visited along a computation path. -/ def ComputationPath.space (p : ntm.ComputationPath input) : ℕ := RunPath.space p.toRunPath @@ -153,6 +177,16 @@ lemma RunsInSpace.mono {s s' : ℕ} (h : ntm.RunsInSpace input s) (hs : s ≤ s' ntm.RunsInSpace input s' := fun p ↦ (h p).trans hs +/-- A machine running in space `s` has a computation path visiting the most cells. -/ +lemma RunsInSpace.exists_space_max {s : ℕ} (hs : ntm.RunsInSpace input s) : + ∃ p : ntm.ComputationPath input, ∀ q : ntm.ComputationPath input, q.space ≤ p.space := by + have hne : (Set.range fun p : ntm.ComputationPath input => p.space).Nonempty := + ⟨_, ⟨.singleton _ (ntm.initCfg input), rfl⟩, rfl⟩ + have hbdd : BddAbove (Set.range fun p : ntm.ComputationPath input => p.space) := + ⟨s, by rintro _ ⟨p, rfl⟩; exact hs p⟩ + obtain ⟨p, hp⟩ := Nat.sSup_mem hne hbdd + exact ⟨p, fun q => (le_csSup hbdd ⟨q, rfl⟩).trans_eq hp.symm⟩ + /-- A machine without work tapes satisfies every space bound. -/ @[simp] lemma runsInSpace_zero_tapes (ntm : MultiTapeNTM 0 Symbol State) (input : List Symbol) (s : ℕ) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index c7f2241f04..d38e77461c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -11,169 +11,94 @@ public import Mathlib.Data.Int.Interval public import Mathlib.Order.Lattice.Nat /-! -# Tape head visitation and space-usage lemmas +# Head movement along run paths -This file collects lemmas about the set of positions visited by a work-tape head -(`MultiTapeTM.visitedByTapeHead`) and the resulting space-usage measures -(`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.space`) and how the tape head positions -influence the cells that are modified on a tape. - -`MultiTapeTM.exists_spaceUsedByTape_max` shows that a computation whose space usage is bounded -attains its per-tape space usage at a single step, which makes a bound that holds at every point -in time usable as a bound for the whole run. +This file collects how a step moves the work-tape heads and changes the work tapes, and what this +implies for the cells visited along a run path: a head moves by at most one cell per step, so it +visits every cell between its first and last positions, and a cell changes only under its head. -/ @[expose] public section -namespace Turing.MultiTapeTM - -variable {k : ℕ} -variable {State Symbol : Type*} -variable {input : List Symbol} -variable {tm : MultiTapeTM k Symbol State} -variable {cfg : Cfg k Symbol State input} - -/-- If the work tape head is not at position `z`, then the tape does not change there. -/ -lemma step_workTapes_eq_of_ne - (cfg : Cfg k Symbol State input) - (j : Fin k) - (z : ℤ) - (hz : z ≠ cfg.workTapePos j) : - (tm.step cfg).workTapes j z = cfg.workTapes j z := by - cases hst : cfg.state with - | none => simp [step_of_halt hst] - | some q => - rw [step_of_state hst, Action.apply_workTapes] - rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workTapes j).1 <;> simp_all - -lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : - z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by - simp [visitedByTapeHead, Fin.exists_iff] - -lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - (tm.runFrom cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := - tm.mem_visitedByTapeHead.mpr ⟨t, by omega, rfl⟩ - -/-- The set of positions visited by a tape head is monotone in the number of steps. -/ -lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) {t t' : ℕ} (h : t ≤ t') : - tm.visitedByTapeHead cfg t i ⊆ tm.visitedByTapeHead cfg t' i := by - intro z hz - obtain ⟨n, hn, hz⟩ := tm.mem_visitedByTapeHead.mp hz - exact tm.mem_visitedByTapeHead.mpr ⟨n, by omega, hz⟩ - -/-- Starting from configuration `cfg`, every position between the initial head position of tape -`i` and the one after `t` steps is part of the "visited set" at step `t`. -/ -lemma uIcc_workTapePos_subset_visitedByTapeHead - (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) : - Finset.uIcc (cfg.workTapePos i) ((tm.runFrom cfg t).workTapePos i) - ⊆ tm.visitedByTapeHead cfg t i := by - induction t with - | zero => simpa [runFrom] using tm.mem_visitedByTapeHead_self cfg 0 i - | succ t ih => +namespace Turing.MultiTapeNTM + +variable {k k' : ℕ} {State State' Symbol : Type*} {input input' : List Symbol} +variable {ntm : MultiTapeNTM k Symbol State} {ntm' : MultiTapeNTM k' Symbol State'} + +/-- A work-tape head moves by at most one cell in a single step. -/ +lemma Step.workTapePos_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) : + |c'.workTapePos i - c.workTapePos i| ≤ 1 := by + unfold Step at h + split at h + · simp [h] + · obtain ⟨a, _, rfl⟩ := h + exact workTapePos_apply_le a c i + +/-- A step does not change a work-tape cell away from its head. -/ +lemma Step.workTapes_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') {i : Fin k} + {z : ℤ} (hz : z ≠ c.workTapePos i) : c'.workTapes i z = c.workTapes i z := by + unfold Step at h + split at h + · simp [h] + · obtain ⟨a, _, rfl⟩ := h + rw [Action.apply_workTapes] + cases ha : (a.workTapes i).1 <;> simp [ha, hz] + +namespace RunPath + +/-- Every position between the first and the last position of a head along a path is visited, +since the head moves by at most one cell per step. -/ +lemma uIcc_workTapePos_subset_visitedByTapeHead (p : ntm.RunPath input) (i : Fin k) : + Finset.uIcc (p.head.workTapePos i) (p.last.workTapePos i) ⊆ p.visitedByTapeHead i := by + induction p using RelSeries.inductionOn' with + | singleton c => + simp +instances [visitedByTapeHead, RelSeries.singleton, RelSeries.head, RelSeries.last] + | snoc p c h ih => + have hm := abs_le.mp (Step.workTapePos_le h i) + rw [RelSeries.head_snoc, RelSeries.last_snoc, visitedByTapeHead_snoc] intro z hz - have hstep : - |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := by - simpa only [runFrom, Function.iterate_succ_apply'] using - tm.workTapePos_step_le (tm.runFrom cfg t) i - have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t) - have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i - grind [Finset.mem_uIcc] - -/-- If a work tape cell is changed after `t` steps, it must have been visited by the tape head. -/ -lemma mem_visitedByTapeHead_of_workTapes_ne - (j : Fin k) - (t : ℕ) - (z : ℤ) - (h : (tm.runFrom cfg t).workTapes j z ≠ cfg.workTapes j z) : - z ∈ tm.visitedByTapeHead cfg t j := by - induction t with - | zero => exact absurd (by simp [runFrom]) h - | succ t ih => - rw [runFrom, Function.iterate_succ_apply', ← runFrom] at h - by_cases hz : z = (tm.runFrom cfg t).workTapePos j - · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) - (tm.mem_visitedByTapeHead_self cfg t j) - · rw [tm.step_workTapes_eq_of_ne _ j z hz] at h - exact tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (ih h) - -/-- Every position visited by the head of tape `i` lies within `spaceUsedByTape … i` of the -head's starting position. -/ -lemma natAbs_le_spaceUsedByTape_of_mem_visited - {i : Fin k} - {z : ℤ} - {t : ℕ} - (hz : z ∈ tm.visitedByTapeHead cfg t i) : - (z - cfg.workTapePos i).natAbs ≤ tm.spaceUsedByTape cfg t i := by - obtain ⟨t', ht', rfl⟩ := tm.mem_visitedByTapeHead.mp hz - have h1 := Finset.card_le_card - ((tm.uIcc_workTapePos_subset_visitedByTapeHead cfg i t').trans - (tm.visitedByTapeHead_mono cfg i (show t' ≤ t by omega))) - rw [Int.card_uIcc] at h1 - unfold spaceUsedByTape + by_cases he : z = c.workTapePos i + · exact he ▸ Finset.mem_insert_self _ _ + · exact Finset.mem_insert_of_mem (ih (by rw [Finset.mem_uIcc] at hz ⊢; omega)) + +/-- A work-tape cell that differs between the first and the last configuration of a path was +visited by its head. -/ +lemma mem_visitedByTapeHead_of_workTapes_ne (p : ntm.RunPath input) {i : Fin k} {z : ℤ} + (h : p.last.workTapes i z ≠ p.head.workTapes i z) : z ∈ p.visitedByTapeHead i := by + induction p using RelSeries.inductionOn' with + | singleton c => exact absurd rfl h + | snoc p c hs ih => + rw [visitedByTapeHead_snoc] + refine Finset.mem_insert_of_mem ?_ + by_cases hz : z = p.last.workTapePos i + · exact hz ▸ Finset.mem_image_of_mem _ (Finset.mem_univ (Fin.last _)) + · rw [RelSeries.last_snoc, RelSeries.head_snoc, Step.workTapes_eq_of_ne hs hz] at h + exact ih h + +/-- Every position visited by a head lies within the space of its tape from its first position. -/ +lemma natAbs_le_spaceUsedByTape_of_mem_visited (p : ntm.RunPath input) {i : Fin k} {z : ℤ} + (hz : z ∈ p.visitedByTapeHead i) : + (z - p.head.workTapePos i).natAbs ≤ p.spaceUsedByTape i := by + obtain ⟨n, -, rfl⟩ := Finset.mem_image.mp hz + -- the prefix up to `n` visits every position between the first position and the one at `n` + have h := Finset.card_le_card + ((uIcc_workTapePos_subset_visitedByTapeHead (p.take n) i).trans + (p.visitedByTapeHead_take_subset n i)) + rw [RelSeries.head_take, RelSeries.last_take, Int.card_uIcc] at h + change _ ≤ (p.visitedByTapeHead i).card omega -/-- Every non-blank cell on work tape `i` lies within `spaceUsedByTape … i t` of the origin. -/ -lemma content_natAbs_le_spaceUsedByTape - {i : Fin k} - (t : ℕ) - (z : ℤ) - (h : (tm.runFrom (tm.initCfg input) t).workTapes i z ≠ none) : - z.natAbs ≤ tm.spaceUsedByTape (tm.initCfg input) t i := by - -- The work tapes start out blank, so any non-blank cell has been visited by the head; the - -- initial head position is `0`, so the displacement bound is a bound on the position itself. - simpa using tm.natAbs_le_spaceUsedByTape_of_mem_visited - (tm.mem_visitedByTapeHead_of_workTapes_ne i t z h) - -/-- The number of cells visited by a single work-tape head grows by at most one each step. -/ -lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - tm.spaceUsedByTape cfg t i ≤ t + 1 := - Finset.card_image_le.trans_eq (by simp) - -/-- The space used by a computation is bounded linearly by the number of steps. -/ -lemma space_linear (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.space cfg t ≤ k * t + k := by - calc tm.space cfg t - = ∑ i, (tm.spaceUsedByTape cfg t i) := by rfl - _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i) - _ = k * t + k := by simp [Nat.mul_succ] - -/-- The space used by a single tape is monotone in the number of steps. -/ -lemma spaceUsedByTape_mono - (tm : MultiTapeTM k Symbol State) - (cfg : Cfg k Symbol State input) - (i : Fin k) : - Monotone (tm.spaceUsedByTape cfg · i) := by - intro t t' h - exact Finset.card_le_card (tm.visitedByTapeHead_mono cfg i h) - -/-- A computation whose total space usage stays below a bound reaches a step `T` at which the space -usage of *every* tape is maximal. This turns a bound that holds at every point in time into a -bound for the whole run. -/ -lemma exists_spaceUsedByTape_max (cfg : Cfg k Symbol State input) {s : ℕ} - (hs : ∀ t, tm.space cfg t ≤ s) : - ∃ T, ∀ t i, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg T i := by - -- The space usage of a single tape is bounded, so it attains its supremum at some step `T i`. - have h : ∀ i, ∃ Ti, ∀ t, tm.spaceUsedByTape cfg t i ≤ tm.spaceUsedByTape cfg Ti i := by - intro i - have hbdd : BddAbove (Set.range (tm.spaceUsedByTape cfg · i)) := - ⟨s, by rintro _ ⟨t, rfl⟩; exact (tm.spaceUsedByTape_le_space cfg t i).trans (hs t)⟩ - obtain ⟨Ti, hTi⟩ := Nat.sSup_mem (Set.range_nonempty (tm.spaceUsedByTape cfg · i)) hbdd - exact ⟨Ti, fun t => (le_csSup hbdd ⟨t, rfl⟩).trans hTi.ge⟩ - choose T hT using h - -- Monotonicity lets us use a single step that is late enough for every tape. - exact ⟨Finset.univ.sup T, fun t i => - (hT i t).trans (tm.spaceUsedByTape_mono cfg i (Finset.le_sup (Finset.mem_univ i)))⟩ - -/-- A run path that starts with every head at cell `0` and visits at most `s` cells keeps its heads +/-- A path that starts with every head at cell `0` and visits at most `s` cells keeps its heads within `[-s, s]`. -/ -lemma _root_.Turing.MultiTapeNTM.RunPath.inWindow_of_space_le {p : tm.RunPath input} {s : ℕ} - (h0 : ∀ i, p.head.workTapePos i = 0) (hs : p.space ≤ s) : p.InWindow s := by - rw [p.eq_ofDeterministic] at hs ⊢ - rintro _ ⟨n, rfl⟩ i - have hz := tm.natAbs_le_spaceUsedByTape_of_mem_visited - ((tm.mem_visitedByTapeHead (cfg := p.head) (t := p.time) (i := i)).mpr ⟨n, n.2, rfl⟩) +lemma inWindow_of_space_le {p : ntm.RunPath input} {s : ℕ} (h0 : ∀ i, p.head.workTapePos i = 0) + (hs : p.space ≤ s) : p.InWindow s := fun c hc i => by + have hz := p.natAbs_le_spaceUsedByTape_of_mem_visited + ((p.mem_visitedByTapeHead (i := i)).mpr ⟨c, hc, rfl⟩) rw [h0, sub_zero] at hz - exact mem_window.mpr (hz.trans ((tm.spaceUsedByTape_le_space _ _ i).trans hs)) + exact mem_window.mpr <| hz.trans <| + (Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)).trans hs + +end RunPath -end Turing.MultiTapeTM +end Turing.MultiTapeNTM