diff --git a/Complexity.lean b/Complexity.lean index fb762678b4..ce126ef2f0 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1764,6 +1764,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Resour public import Complexity.Computability.Machines.Turing.MultiTape.Internal.StepMachineCompiler public import Complexity.Computability.Machines.Turing.MultiTape.Internal.UnaryMachines public import Complexity.Computability.Machines.Turing.MultiTape.Internal.WordPredicates +public import Complexity.Computability.Machines.Turing.MultiTape.Locality public import Complexity.Computability.Machines.Turing.MultiTape.Machine public import Complexity.Computability.Machines.Turing.MultiTape.Machine.ChoiceTable public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Clock @@ -1812,6 +1813,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileI public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Clock public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Closed public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean b/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean new file mode 100644 index 0000000000..3cb609e61e --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean @@ -0,0 +1,184 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas + +/-! +# Locality of a step + +A step of a multi-tape machine reads the cells under its heads, writes at most the cells under +its work heads, and moves every head by at most one cell. This file records these facts in the +form used to cut a computation into local pieces. + +The heads are indexed by `Option (Fin k)`: `none` is the read-only input head and `some i` the +head of work tape `i`. `Turing.Cfg.headPos` places them in coordinates where every head starts at +zero; the input head's stored position `inputPos` is shifted by one, so its coordinate ranges over +`[-1, n]` on an input of length `n`. The write-only output tape is never read and has no head +here. + +Two configurations *agree on* a family `W` of work-tape cells (`Turing.Cfg.AgreeOn`) when they have +the same control state and head positions and the same work-tape contents on `W`. If the work +heads lie in `W`, a step reads the same symbols in both, takes the same action, and preserves +agreement on `W`; both append the same symbol, if any, to their outputs +(`Turing.MultiTapeTM.agreeOn_step`). Contents outside `W` and earlier outputs may differ. + +## Main definitions + +* `Turing.Cfg.headPos`: head positions, starting at zero. +* `Turing.Cfg.AgreeOn`: same control and heads, and same work-tape contents on given cells. + +## Main results + +* `Turing.MultiTapeNTM.Step.abs_headPos_sub_le`: a step moves every head by at most one cell. +* `Turing.MultiTapeTM.agreeOn_step`: agreement on cells containing the work heads is preserved + by a step, which emits the same output in both configurations. +-/ + +public section + +namespace Turing + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- The position of a head, in coordinates where every head starts at zero: the input head +(`none`) at its stored position shifted by one, and the head of work tape `i` (`some i`). -/ +@[expose] def Cfg.headPos (cfg : Cfg k Symbol State input) : Option (Fin k) → ℤ + | none => (cfg.inputPos.val : ℤ) - 1 + | some i => cfg.workTapePos i + +@[simp] theorem Cfg.headPos_none (cfg : Cfg k Symbol State input) : + cfg.headPos none = (cfg.inputPos.val : ℤ) - 1 := rfl + +@[simp] theorem Cfg.headPos_some (cfg : Cfg k Symbol State input) (i : Fin k) : + cfg.headPos (some i) = cfg.workTapePos i := rfl + +/-- Every head starts at zero. -/ +theorem Cfg.headPos_init (q₀ : State) (head : Option (Fin k)) : + (Cfg.init q₀ input : Cfg k Symbol State input).headPos head = 0 := by + cases head with + | none => simp [Cfg.headPos] + | some i => rfl + +/-- The input head is at a coordinate in `[-1, n]` on an input of length `n`. -/ +theorem Cfg.headPos_none_mem_Icc (cfg : Cfg k Symbol State input) : + cfg.headPos none ∈ Set.Icc (-1) (input.length : ℤ) := by + have := cfg.inputPos.isLt + simp only [headPos_none, Set.mem_Icc] + omega + +/-- An action moves every head by at most one cell. -/ +theorem Action.abs_headPos_apply_sub_le (action : Action k Symbol State) + (cfg : Cfg k Symbol State input) (head : Option (Fin k)) : + |(action.apply cfg).headPos head - cfg.headPos head| ≤ 1 := by + cases head with + | none => + have hmove := val_moveInputPos_eq cfg.inputPos action.inputTape + have hlt := cfg.inputPos.isLt + have hcast : (action.inputTape.cast : ℤ) = -1 ∨ (action.inputTape.cast : ℤ) = 0 ∨ + (action.inputTape.cast : ℤ) = 1 := by + rcases action.inputTape with _ | _ | _ <;> simp [SignType.cast] + simp only [Cfg.headPos_none, Action.apply_inputPos, abs_le] + omega + | some i => exact workTapePos_apply_le action cfg i + +/-- **A step moves every head by at most one cell.** -/ +theorem MultiTapeNTM.Step.abs_headPos_sub_le {ntm : MultiTapeNTM k Symbol State} + {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (head : Option (Fin k)) : + |c'.headPos head - c.headPos head| ≤ 1 := by + unfold MultiTapeNTM.Step at h + split at h + · simp [h] + · obtain ⟨action, -, rfl⟩ := h + exact action.abs_headPos_apply_sub_le c head + +/-- Two configurations agree on the work-tape cells `W`: they have the same control state, the +same input and work head positions, and the same work-tape contents on `W`. Their outputs and +their contents outside `W` are unconstrained. -/ +structure Cfg.AgreeOn (W : Fin k → Set ℤ) (c c' : Cfg k Symbol State input) : Prop where + /-- The same control state. -/ + state_eq : c.state = c'.state + /-- The same input head position. -/ + inputPos_eq : c.inputPos = c'.inputPos + /-- The same work head positions. -/ + workTapePos_eq : c.workTapePos = c'.workTapePos + /-- The same work-tape contents on `W`. -/ + workTapes_eq : ∀ i, ∀ z ∈ W i, c.workTapes i z = c'.workTapes i z + +/-- A configuration agrees with itself on every family of cells. -/ +theorem Cfg.AgreeOn.refl (W : Fin k → Set ℤ) (c : Cfg k Symbol State input) : c.AgreeOn W c := + ⟨rfl, rfl, rfl, fun _ _ _ => rfl⟩ + +theorem Cfg.AgreeOn.symm {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') : c'.AgreeOn W c := + ⟨h.state_eq.symm, h.inputPos_eq.symm, h.workTapePos_eq.symm, + fun i z hz => (h.workTapes_eq i z hz).symm⟩ + +theorem Cfg.AgreeOn.trans {W : Fin k → Set ℤ} {c c' c'' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (h' : c'.AgreeOn W c'') : c.AgreeOn W c'' := + ⟨h.state_eq.trans h'.state_eq, h.inputPos_eq.trans h'.inputPos_eq, + h.workTapePos_eq.trans h'.workTapePos_eq, + fun i z hz => (h.workTapes_eq i z hz).trans (h'.workTapes_eq i z hz)⟩ + +/-- Agreement on more cells is agreement on fewer. -/ +theorem Cfg.AgreeOn.mono {W W' : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (hW : ∀ i, W' i ⊆ W i) : c.AgreeOn W' c' := + ⟨h.state_eq, h.inputPos_eq, h.workTapePos_eq, fun i z hz => h.workTapes_eq i z (hW i hz)⟩ + +/-- Agreeing configurations are at the same head positions. -/ +theorem Cfg.AgreeOn.headPos_eq {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') : c.headPos = c'.headPos := by + funext head + cases head with + | none => simp [h.inputPos_eq] + | some i => simp [h.workTapePos_eq] + +/-- Agreement on cells containing the work heads gives the same read symbols. -/ +theorem Cfg.AgreeOn.workTapeSymbols_eq {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (hpos : ∀ i, c.workTapePos i ∈ W i) : + c.workTapeSymbols = c'.workTapeSymbols := by + funext i + simp only [Cfg.workTapeSymbols, ← h.workTapePos_eq] + exact h.workTapes_eq i _ (hpos i) + +/-- One action applied to agreeing configurations keeps them agreeing on `W`: it writes the same +symbols under the same heads. -/ +theorem Cfg.AgreeOn.apply {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (action : Action k Symbol State) : + (action.apply c).AgreeOn W (action.apply c') := by + refine ⟨rfl, by simp [h.inputPos_eq], by funext i; simp [h.workTapePos_eq], fun i z hz => ?_⟩ + simp only [Action.apply_workTapes, ← h.workTapePos_eq] + cases (action.workTapes i).1 with + | none => exact h.workTapes_eq i z hz + | some s => + by_cases hz' : z = c.workTapePos i + · simp [hz'] + · simp only [Function.update_of_ne hz'] + exact h.workTapes_eq i z hz + +/-- **Locality of a step.** If two configurations agree on cells `W` containing their work +heads, one step keeps them agreeing on `W`, and both append the same word to their outputs. -/ +theorem MultiTapeTM.agreeOn_step (tm : MultiTapeTM k Symbol State) {W : Fin k → Set ℤ} + {c c' : Cfg k Symbol State input} (h : c.AgreeOn W c') (hpos : ∀ i, c.workTapePos i ∈ W i) : + (tm.step c).AgreeOn W (tm.step c') ∧ + ∃ e, (tm.step c).output = c.output ++ e ∧ (tm.step c').output = c'.output ++ e := by + cases hs : c.state with + | none => + have hs' : c'.state = none := h.state_eq ▸ hs + rw [MultiTapeTM.step_of_halt hs, MultiTapeTM.step_of_halt hs'] + exact ⟨h, [], by simp, by simp⟩ + | some q => + have hs' : c'.state = some q := h.state_eq ▸ hs + have hread : c.inputSymbol = c'.inputSymbol := by + simp only [Cfg.inputSymbol, h.inputPos_eq] + rw [MultiTapeTM.step_of_state hs, MultiTapeTM.step_of_state hs', hread, + h.workTapeSymbols_eq hpos] + exact ⟨h.apply _, _, Action.apply_output _ _, Action.apply_output _ _⟩ + +end Turing diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean new file mode 100644 index 0000000000..5a41b6e994 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Blocks.lean @@ -0,0 +1,330 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Locality +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic +public import Mathlib.Data.Fintype.Option +public import Mathlib.Data.Fintype.Pi +public import Mathlib.Basic.Sign.Defs +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Basic.Sign.Basic +import Mathlib.Tactic.Linarith + +/-! +# Time intervals and tape blocks of a choice-string run + +The blocking idea of Hopcroft, Paul and Valiant [HopcroftPaulValiant1977], in the form of +Lemma 2.1 of the note *Deterministic simulations of nondeterministic and randomized time* +(30 October 2026) formalized in issue #1833. It uses three neighbouring tape blocks instead of +making the machine block-respecting (compare [Williams2025], Lemma 2.1 and §3.2). The +statements here are the run-level facts of that lemma, for the replay +`Turing.MultiTapePTM.stepCoins` of a fair-coin table on a list of choice bits. + +Time is cut into intervals of `b` steps: interval `i` starts at +`Turing.MultiTapePTM.intervalStart b coins c i`, after the first `i * b` bits. Each tape is cut +into blocks `B_j = [b j, b (j + 1))`, so a head at coordinate `p` (`Turing.Cfg.headPos`) is in +block `p / b` at offset `p % b`. The blocked heads are the input head and the `k` work heads; +the write-only output tape is never read and is not blocked. + +* **Three blocks.** Within `b` steps a head moves at most `b` cells, so it stays in the blocks + `B_{j-1}, B_j, B_{j+1}` around its starting block `B_j` + (`Turing.MultiTapePTM.headPos_stepCoins_mem_Ico`), and its block index changes by at most one + (`Turing.MultiTapePTM.abs_blockIndex_stepCoins_sub_le`). +* **Schedules.** The *movement schedule* of a run (`Turing.MultiTapePTM.schedule`) records this + change in `{-1, 0, 1}` for every interval and head. There are `3 ^ ((k + 1) * q)` schedules of + `q` intervals (`Turing.MultiTapePTM.card_schedule`), every run has exactly one, and it + determines all block indices from the starting ones + (`Turing.MultiTapePTM.blockIndex_intervalStart`). +* **Locality.** An interval only reads and writes the window `Turing.Cfg.blockWindow` of three + blocks around each work head. Two configurations agreeing on their control, heads and window + contents still agree after `b` steps on the same bits, and emit the same output + (`Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`). So the interval is determined by its + bits, its entering state and head positions and the contents of its windows. Cells outside the + window are unchanged (`Turing.MultiTapePTM.workTapes_stepCoins_eq_of_notMem_blockWindow`), and + a cell lying outside the windows of a range of intervals is untouched throughout that range + (`Turing.MultiTapePTM.workTapes_intervalStart_eq_of_notMem_blockWindow`). + +All statements hold for every block length `b > 0` and number `q` of intervals; the choice +`q = ⌈t / b⌉` and the bound `2 ≤ b ≤ t` of the note only matter for counting. + +## Main definitions + +* `Turing.Cfg.blockWindow`: the three blocks around each work head. +* `Turing.MultiTapePTM.intervalStart`: the configuration at the start of a time interval. +* `Turing.MultiTapePTM.Schedule`, `Turing.MultiTapePTM.schedule`: movement schedules. + +## Main results + +* `Turing.MultiTapePTM.abs_headPos_stepCoins_sub_le`: a head moves at most one cell per bit. +* `Turing.MultiTapePTM.headPos_stepCoins_mem_Ico`: within `b` steps, three blocks. +* `Turing.MultiTapePTM.abs_blockIndex_stepCoins_sub_le`: block indices change by at most one. +* `Turing.MultiTapePTM.card_schedule`: there are `3 ^ ((k + 1) * q)` schedules. +* `Turing.MultiTapePTM.coe_schedule`: a schedule entry is the change of block index. +* `Turing.MultiTapePTM.blockIndex_intervalStart`: schedules determine block indices. +* `Turing.MultiTapePTM.agreeOn_stepCoins`: locality of a run on cells containing its heads. +* `Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`: an interval is determined by its window. +* `Turing.MultiTapePTM.workTapes_stepCoins_eq_of_notMem_blockWindow`: cells outside the window + are unchanged. +* `Turing.MultiTapePTM.workTapes_intervalStart_eq_of_notMem_blockWindow`: blocks outside the + windows of a range of intervals are untouched. + +## References + +* [J. Hopcroft, W. Paul, L. Valiant, *On Time Versus Space*][HopcroftPaulValiant1977] +* [R. Williams, *Simulating Time With Square-Root Space*][Williams2025] +-/ + +public section + +namespace Turing + +variable {k : ℕ} {Symbol State : Type} {input : List Symbol} + +/-! ### Block arithmetic -/ + +/-- Within distance `b` of a point of block `p / b`, the three blocks around it. -/ +private theorem mem_Ico_of_abs_sub_le {b p p' : ℤ} (hb : 0 < b) (h : |p' - p| ≤ b) : + b * (p / b - 1) ≤ p' ∧ p' < b * (p / b + 2) := by + have hdiv := Int.mul_ediv_add_emod p b + have hlo := Int.emod_nonneg p hb.ne' + have hhi := Int.emod_lt_of_pos p hb + have := abs_le.mp h + constructor <;> nlinarith + +/-- Within distance `b`, block indices differ by at most one. -/ +private theorem abs_ediv_sub_ediv_le_one {b p p' : ℤ} (hb : 0 < b) (h : |p' - p| ≤ b) : + |p' / b - p / b| ≤ 1 := by + obtain ⟨hlo, hhi⟩ := mem_Ico_of_abs_sub_le hb h + have hdiv := Int.mul_ediv_add_emod p' b + have hlo' := Int.emod_nonneg p' hb.ne' + have hhi' := Int.emod_lt_of_pos p' hb + have h₁ : p' / b < p / b + 2 := lt_of_mul_lt_mul_left (by linarith) hb.le + have h₂ : p / b - 1 < p' / b + 1 := lt_of_mul_lt_mul_left (by linarith) hb.le + rw [abs_le] + constructor <;> omega + +/-- The three blocks of length `b` around the block of each work head: the cells a work head can +visit within `b` steps. -/ +@[expose] def Cfg.blockWindow (b : ℕ) (c : Cfg k Symbol State input) (i : Fin k) : Set ℤ := + Set.Ico (b * (c.workTapePos i / b - 1)) (b * (c.workTapePos i / b + 2)) + +namespace MultiTapePTM + +variable (machine : MultiTapePTM k Symbol State) + +/-! ### Head movement -/ + +/-- A replayed bit is a step of the table with that coin fixed. -/ +private theorem step_withCoin (bit : Bool) (c : Cfg k Symbol State input) : + (machine.withCoin bit).toTM.Step c ((machine.withCoin bit).toTM.step c) := + MultiTapeTM.step_iff.mpr rfl + +/-- A head moves at most one cell per replayed bit. -/ +theorem abs_headPos_stepCoins_sub_le (coins : List Bool) (c : Cfg k Symbol State input) + (head : Option (Fin k)) : + |(machine.stepCoins coins c).headPos head - c.headPos head| ≤ coins.length := by + induction coins generalizing c with + | nil => simp + | cons bit coins ih => + rw [stepCoins_cons] + have h₁ := abs_le.mp (ih ((machine.withCoin bit).toTM.step c)) + have h₂ := abs_le.mp ((machine.step_withCoin bit c).abs_headPos_sub_le head) + rw [abs_le, List.length_cons] + push_cast + constructor <;> linarith + +/-- **Three blocks.** Within `b` replayed bits, a head stays in the three blocks of length `b` +around its starting block. -/ +theorem headPos_stepCoins_mem_Ico {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) (head : Option (Fin k)) : + (machine.stepCoins coins c).headPos head ∈ + Set.Ico ((b : ℤ) * (c.headPos head / b - 1)) (b * (c.headPos head / b + 2)) := + mem_Ico_of_abs_sub_le (by exact_mod_cast hb) + ((machine.abs_headPos_stepCoins_sub_le coins c head).trans (by exact_mod_cast hlen)) + +/-- Within `b` replayed bits, the block index of a head changes by at most one. -/ +theorem abs_blockIndex_stepCoins_sub_le {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) (head : Option (Fin k)) : + |(machine.stepCoins coins c).headPos head / b - c.headPos head / b| ≤ 1 := + abs_ediv_sub_ediv_le_one (by exact_mod_cast hb) + ((machine.abs_headPos_stepCoins_sub_le coins c head).trans (by exact_mod_cast hlen)) + +/-- A work-tape cell farther from the head than the number of replayed bits is unchanged. -/ +theorem workTapes_stepCoins_eq_of_lt_abs (coins : List Bool) (c : Cfg k Symbol State input) + {i : Fin k} {z : ℤ} (hz : (coins.length : ℤ) < |z - c.workTapePos i|) : + (machine.stepCoins coins c).workTapes i z = c.workTapes i z := by + induction coins generalizing c with + | nil => rfl + | cons bit coins ih => + have hstep := machine.step_withCoin bit c + have hmove := abs_le.mp (hstep.abs_headPos_sub_le (some i)) + simp only [Cfg.headPos_some] at hmove + simp only [List.length_cons, Nat.cast_add, Nat.cast_one] at hz + rw [stepCoins_cons, ih _ ?_] + · refine hstep.workTapes_eq_of_ne fun hzpos => ?_ + rw [hzpos, sub_self, abs_zero] at hz + omega + · rw [lt_abs] at hz ⊢ + omega + +/-- **Locality of a run.** If two configurations agree on cells `W`, and the work heads of the +first stay in `W` before each replayed bit, then after replaying the same bits they still agree +on `W` and have appended the same word to their outputs. -/ +theorem agreeOn_stepCoins {W : Fin k → Set ℤ} {c c' : Cfg k Symbol State input} + (h : c.AgreeOn W c') (coins : List Bool) + (hpos : ∀ j < coins.length, ∀ i, (machine.stepCoins (coins.take j) c).workTapePos i ∈ W i) : + (machine.stepCoins coins c).AgreeOn W (machine.stepCoins coins c') ∧ + ∃ e, (machine.stepCoins coins c).output = c.output ++ e ∧ + (machine.stepCoins coins c').output = c'.output ++ e := by + induction coins generalizing c c' with + | nil => exact ⟨h, [], by simp, by simp⟩ + | cons bit coins ih => + obtain ⟨hstep, e, he, he'⟩ := + MultiTapeTM.agreeOn_step (machine.withCoin bit).toTM h (hpos 0 (by simp)) + obtain ⟨hrest, e', hrest₁, hrest₂⟩ := ih hstep fun j hj => by + simpa only [List.take_succ_cons, stepCoins_cons] using + hpos (j + 1) (by simpa only [List.length_cons, Nat.add_lt_add_iff_right] using hj) + refine ⟨hrest, e ++ e', ?_, ?_⟩ + · rw [stepCoins_cons, hrest₁, he, List.append_assoc] + · rw [stepCoins_cons, hrest₂, he', List.append_assoc] + +/-- **An interval is determined by its window.** Two configurations agreeing on the three blocks +around each work head of the first still agree there after at most `b` replayed bits, and have +appended the same word to their outputs. -/ +theorem agreeOn_blockWindow_stepCoins {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) {c c' : Cfg k Symbol State input} + (h : c.AgreeOn (c.blockWindow b) c') : + (machine.stepCoins coins c).AgreeOn (c.blockWindow b) (machine.stepCoins coins c') ∧ + ∃ e, (machine.stepCoins coins c).output = c.output ++ e ∧ + (machine.stepCoins coins c').output = c'.output ++ e := + machine.agreeOn_stepCoins h coins fun j _ i => + machine.headPos_stepCoins_mem_Ico hb (coins := coins.take j) + ((List.length_take_le' j coins).trans hlen) c (some i) + +/-- Within `b` replayed bits, a work-tape cell outside the three blocks around its head is +unchanged. -/ +theorem workTapes_stepCoins_eq_of_notMem_blockWindow {b : ℕ} (hb : 0 < b) {coins : List Bool} + (hlen : coins.length ≤ b) (c : Cfg k Symbol State input) {i : Fin k} {z : ℤ} + (hz : z ∉ c.blockWindow b i) : + (machine.stepCoins coins c).workTapes i z = c.workTapes i z := by + refine machine.workTapes_stepCoins_eq_of_lt_abs coins c ?_ + have hb' : (0 : ℤ) < b := by exact_mod_cast hb + have hdiv := Int.mul_ediv_add_emod (c.workTapePos i) b + have hlo := Int.emod_nonneg (c.workTapePos i) hb'.ne' + have hhi := Int.emod_lt_of_pos (c.workTapePos i) hb' + have hlen' : (coins.length : ℤ) ≤ b := by exact_mod_cast hlen + simp only [Cfg.blockWindow, Set.mem_Ico, not_and_or, not_le, not_lt] at hz + rw [lt_abs] + rcases hz with hz | hz + · right + nlinarith + · left + nlinarith + +/-! ### Time intervals and schedules -/ + +/-- The configuration at the start of time interval `i`, of `b` steps each: replay the first +`i * b` bits. -/ +@[expose] noncomputable def intervalStart (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) + (i : ℕ) : Cfg k Symbol State input := + machine.stepCoins (coins.take (i * b)) c + +@[simp] theorem intervalStart_zero (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) : + machine.intervalStart b coins c 0 = c := by + simp [intervalStart] + +/-- Interval `i + 1` starts after replaying the `b` bits of interval `i`. -/ +theorem intervalStart_succ (b : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) (i : ℕ) : + machine.intervalStart b coins c (i + 1) = + machine.stepCoins ((coins.drop (i * b)).take b) (machine.intervalStart b coins c i) := by + rw [intervalStart, intervalStart, ← stepCoins_append, Nat.succ_mul, List.take_add] + +/-- The bits of an interval number at most `b`. -/ +theorem length_intervalCoins_le (b : ℕ) (coins : List Bool) (i : ℕ) : + ((coins.drop (i * b)).take b).length ≤ b := + List.length_take_le _ _ + +/-- A movement schedule of `q` intervals: the change, in `{-1, 0, 1}`, of the block index of +the input head (`none`) and of each work head (`some i`) across each interval. -/ +abbrev Schedule (k q : ℕ) := Fin q → Option (Fin k) → SignType + +/-- There are `3 ^ ((k + 1) * q)` movement schedules of `q` intervals. -/ +theorem card_schedule (k q : ℕ) : Fintype.card (Schedule k q) = 3 ^ ((k + 1) * q) := by + simp only [Fintype.card_fun, Fintype.card_option, Fintype.card_fin] + rw [show Fintype.card SignType = 3 from rfl, ← pow_mul, mul_comm] + +/-- The movement schedule of the run replaying `coins` from `c`, in `q` intervals of `b` bits: +the change of the block index of every head across every interval. -/ +noncomputable def schedule (b q : ℕ) (coins : List Bool) (c : Cfg k Symbol State input) : + Schedule k q := fun i head => + SignType.sign ((machine.intervalStart b coins c (i + 1)).headPos head / b - + (machine.intervalStart b coins c i).headPos head / b) + +/-- An integer of absolute value at most one is its own sign. -/ +private theorem coe_sign_eq_self {d : ℤ} (hd : |d| ≤ 1) : + ((SignType.sign d : SignType) : ℤ) = d := by + have : d = -1 ∨ d = 0 ∨ d = 1 := by rw [abs_le] at hd; omega + rcases this with rfl | rfl | rfl <;> rfl + +/-- A schedule entry is the change of block index across the interval. -/ +theorem coe_schedule {b : ℕ} (hb : 0 < b) (q : ℕ) (coins : List Bool) + (c : Cfg k Symbol State input) (i : Fin q) (head : Option (Fin k)) : + (machine.schedule b q coins c i head : ℤ) = + (machine.intervalStart b coins c (i + 1)).headPos head / b - + (machine.intervalStart b coins c i).headPos head / b := by + refine coe_sign_eq_self ?_ + rw [intervalStart_succ] + exact machine.abs_blockIndex_stepCoins_sub_le hb (length_intervalCoins_le _ _ _) _ head + +/-- **Schedules determine block indices.** At the start of interval `i ≤ q`, the block index of a +head is its starting block index plus the schedule entries of the earlier intervals. -/ +theorem blockIndex_intervalStart {b : ℕ} (hb : 0 < b) {q : ℕ} (coins : List Bool) + (c : Cfg k Symbol State input) (head : Option (Fin k)) {i : ℕ} (hi : i ≤ q) : + (machine.intervalStart b coins c i).headPos head / b = + c.headPos head / b + + ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE hi j) head : ℤ) := by + induction i with + | zero => simp + | succ i ih => + have hsum : ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE hi j.castSucc) head : ℤ) = + ∑ j : Fin i, (machine.schedule b q coins c (Fin.castLE (by omega) j) head : ℤ) := rfl + rw [Fin.sum_univ_castSucc, hsum, ← add_assoc, ← ih (by omega)] + have := machine.coe_schedule hb q coins c ⟨i, by omega⟩ head + simp only at this + change _ = _ + (machine.schedule b q coins c ⟨i, by omega⟩ head : ℤ) + rw [this] + ring + +/-- Across interval `i`, a work-tape cell outside the window of interval `i` is unchanged. -/ +theorem workTapes_intervalStart_succ_eq {b : ℕ} (hb : 0 < b) (coins : List Bool) + (c : Cfg k Symbol State input) (i : ℕ) {h : Fin k} {z : ℤ} + (hz : z ∉ (machine.intervalStart b coins c i).blockWindow b h) : + (machine.intervalStart b coins c (i + 1)).workTapes h z = + (machine.intervalStart b coins c i).workTapes h z := by + rw [intervalStart_succ] + exact machine.workTapes_stepCoins_eq_of_notMem_blockWindow hb + (length_intervalCoins_le _ _ _) _ hz + +/-- **Untouched blocks.** A work-tape cell outside the windows of intervals `i₁, …, i₂ - 1` has +the same contents at the start of interval `i₂` as at the start of interval `i₁`. -/ +theorem workTapes_intervalStart_eq_of_notMem_blockWindow {b : ℕ} (hb : 0 < b) + (coins : List Bool) (c : Cfg k Symbol State input) {h : Fin k} {z : ℤ} {i₁ i₂ : ℕ} + (hle : i₁ ≤ i₂) + (hz : ∀ i, i₁ ≤ i → i < i₂ → z ∉ (machine.intervalStart b coins c i).blockWindow b h) : + (machine.intervalStart b coins c i₂).workTapes h z = + (machine.intervalStart b coins c i₁).workTapes h z := by + induction i₂, hle using Nat.le_induction with + | base => rfl + | succ i₂ hle ih => + rw [machine.workTapes_intervalStart_succ_eq hb coins c i₂ (hz i₂ hle (by omega)), + ih fun i hi hi₂ => hz i hi (by omega)] + +end MultiTapePTM + +end Turing diff --git a/ComplexityTests/HPVBlocks.lean b/ComplexityTests/HPVBlocks.lean new file mode 100644 index 0000000000..8b8e0aa4a7 --- /dev/null +++ b/ComplexityTests/HPVBlocks.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks + +/-! Time intervals, tape blocks and schedules of a concrete choice-string run. -/ + +namespace ComplexityTests.HPVBlocks + +open Turing MultiTapeMachine + +/-- On one work tape, write the coin and move right on `true`, left on `false`. The input head +moves right on `true` too. -/ +private def zigzag : MultiTapePTM 1 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := if bit then 1 else 0, + workTapes := fun _ => (some (some bit), if bit then 1 else -1), + output := none, state := some () } + Empty.elim Empty.elim + +/-- Replays on upstream configurations, evaluated through the computable interpreter. -/ +private theorem stepCoins_eq (coins : List Bool) (cfg : Cfg 1 Bool Unit [true, false]) : + zigzag.stepCoins coins cfg = + (zigzag.runClosedConfigFromCoins coins { tapes := cfg }).tapes := + (MultiTapePTM.tapes_runClosedConfigFromCoins zigzag coins { tapes := cfg }).symm + +private def start : Cfg 1 Bool Unit [true, false] := Cfg.init () [true, false] + +private def coins : List Bool := [true, true, true, false, true, true] + +-- The work head visits 0, 1, 2, 3, 2, 3, 4; the input head is clamped at the right boundary. +example : ((zigzag.stepCoins coins start).headPos (some 0), + (zigzag.stepCoins coins start).headPos none) = (4, 2) := by + rw [stepCoins_eq] + rfl + +-- With blocks of length 2, the work head starts intervals 0, 1, 2, 3 in blocks 0, 1, 1, 2. +example : (List.range 4).map + (fun i => (zigzag.intervalStart 2 coins start i).headPos (some 0) / 2) = [0, 1, 1, 2] := by + simp only [List.range_succ, List.range_zero, List.nil_append, MultiTapePTM.intervalStart, + stepCoins_eq] + rfl + +-- So the schedule of the work head is `(1, 0, 1)`; the input head moves right then stays. +example : (List.ofFn fun i : Fin 3 => (zigzag.schedule 2 3 coins start i (some 0) : ℤ)) = + [1, 0, 1] ∧ + (List.ofFn fun i : Fin 3 => (zigzag.schedule 2 3 coins start i none : ℤ)) = [1, 0, 0] := by + simp only [List.ofFn_succ, List.ofFn_zero, MultiTapePTM.coe_schedule zigzag two_pos, + MultiTapePTM.intervalStart, stepCoins_eq] + constructor <;> rfl + +-- The block index at the end is recovered from the schedule. +example : (zigzag.intervalStart 2 coins start 3).headPos (some 0) / (2 : ℕ) = 2 := by + rw [zigzag.blockIndex_intervalStart two_pos coins start (some 0) le_rfl, Fin.sum_univ_three] + simp only [MultiTapePTM.coe_schedule zigzag two_pos, MultiTapePTM.intervalStart, stepCoins_eq] + rfl + +-- There are `3 ^ 6` schedules of three intervals for the input head and one work head. +example : Fintype.card (MultiTapePTM.Schedule 1 3) = 729 := by + rw [MultiTapePTM.card_schedule] + norm_num + +/-! ### Three blocks -/ + +/-- After one bit the work head is at offset `1` of block `0`, with blocks of length `2`. -/ +private theorem headPos_one : (zigzag.stepCoins [true] start).headPos (some 0) = 1 := by + rw [stepCoins_eq] + rfl + +-- Within two more bits it stays in blocks `-1, 0, 1`: here it reaches block `1`. +example : (zigzag.stepCoins [true, true] (zigzag.stepCoins [true] start)).headPos (some 0) = 3 ∧ + (3 : ℤ) ∈ Set.Ico (2 * (1 / 2 - 1)) (2 * (1 / 2 + 2)) := by + refine ⟨?_, by decide⟩ + rw [← MultiTapePTM.stepCoins_append, stepCoins_eq] + rfl + +-- The bound needs at most `b` bits: three bits leave the three blocks. +example : (zigzag.stepCoins [true, true, true] (zigzag.stepCoins [true] start)).headPos (some 0) ∉ + Set.Ico (2 * ((zigzag.stepCoins [true] start).headPos (some 0) / 2 - 1)) + (2 * ((zigzag.stepCoins [true] start).headPos (some 0) / 2 + 2)) := by + rw [headPos_one, ← MultiTapePTM.stepCoins_append, stepCoins_eq] + decide + +/-! ### Locality -/ + +/-- The start configuration with a written cell outside its window `[-2, 4)`. -/ +private def marked : Cfg 1 Bool Unit [true, false] := + { start with workTapes := fun _ z => if z = 5 then some false else none } + +private theorem agreeOn_marked : start.AgreeOn (start.blockWindow 2) marked := + ⟨rfl, rfl, rfl, fun _ z hz => by + simp only [Cfg.blockWindow, start, Cfg.init, Set.mem_Ico] at hz + simp [marked, start, show z ≠ 5 by omega]⟩ + +-- A window cell written by the run from `start` is written the same way from `marked`. +example : (zigzag.stepCoins [true, false] marked).workTapes 0 1 = some false := by + have hstart : (zigzag.stepCoins [true, false] start).workTapes 0 1 = some false := by + rw [stepCoins_eq] + rfl + rw [← hstart] + exact ((zigzag.agreeOn_blockWindow_stepCoins two_pos (by simp) agreeOn_marked).1.workTapes_eq + 0 1 (by simp [Cfg.blockWindow, start])).symm + +-- The cell outside the window keeps its mark. +example : (zigzag.stepCoins [true, false] marked).workTapes 0 5 = some false := + zigzag.workTapes_stepCoins_eq_of_notMem_blockWindow two_pos (by simp) marked + (by simp [Cfg.blockWindow, marked, start]) + +end ComplexityTests.HPVBlocks diff --git a/references.bib b/references.bib index cc6369c43d..62a5bcdbe1 100644 --- a/references.bib +++ b/references.bib @@ -2332,6 +2332,17 @@ @book{ Hopcroft2006 address = {USA} } +@article{HopcroftPaulValiant1977, + author = {Hopcroft, John and Paul, Wolfgang and Valiant, Leslie}, + title = {On Time Versus Space}, + journal = {Journal of the ACM}, + volume = {24}, + number = {2}, + pages = {332--337}, + year = {1977}, + doi = {10.1145/322003.322015} +} + @techreport{Hoza2022, author = {Hoza, William M.}, title = {Recent Progress on Derandomizing Space-Bounded Computation},