diff --git a/Complexity.lean b/Complexity.lean index bd5e471f8..e16898c89 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -985,6 +985,7 @@ public import Complexity.Computability.Communication.TopDown.Adversary public import Complexity.Computability.Communication.TopDown.Majority public import Complexity.Computability.Communication.TopDown.Parity public import Complexity.Computability.Communication.TopDown.Rectangle +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.AffineDisperser public import Complexity.Computability.Complexity.AffineDisperser.BinaryPolynomial public import Complexity.Computability.Complexity.AffineDisperser.Coordinates @@ -1178,6 +1179,7 @@ public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Completeness public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses.Principles public import Complexity.Computability.Complexity.Classes.Time +public import Complexity.Computability.Complexity.Classes.Time.AcceptCount public import Complexity.Computability.Complexity.Classes.Time.Polynomial public import Complexity.Computability.Complexity.Classes.Toda public import Complexity.Computability.Complexity.Classes.Toda.Counting @@ -1749,6 +1751,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 @@ -1796,6 +1799,8 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileC public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput 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 @@ -1803,6 +1808,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.C public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalTensor public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IterateWhile public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Loop public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OrElse diff --git a/Complexity/Computability/Complexity/AcceptCount.lean b/Complexity/Computability/Complexity/AcceptCount.lean new file mode 100644 index 000000000..c14ce50bb --- /dev/null +++ b/Complexity/Computability/Complexity/AcceptCount.lean @@ -0,0 +1,119 @@ +/- +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.Init +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Data.Fintype.Pi +import Complexity.Foundations.Data.BitString.WordCount + +/-! +# Counting accepted strings + +`Cslib.Complexity.acceptCount V a n` is the number of strings `w` of length `n` with +`V (a, w) = true`, for any Boolean predicate `V : α × List Bool → Bool`. No efficiency of `V` is +assumed. It counts the certificates of a verifier in the counting classes +(`Cslib.Complexity.SharpP`), the random strings accepted by a bounded-error or majority verifier, +and the choice strings accepted by a fair-coin machine (`Turing.MultiTapePTM.acceptCount`). + +## Main definitions + +* `Cslib.Complexity.acceptCount`: the number of accepted strings of a given length. + +## Main results + +* `Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`: the range + and support of the count. +* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. +* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, + `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +variable {α : Type} + +/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ +def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card + +section acceptCount + +variable {V : α × List Bool → Bool} {a : α} {n : ℕ} + +/-- At most all `2 ^ n` strings are accepted. -/ +theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := + (Finset.card_filter_le _ _).trans (by simp) + +/-- Some string of length `n` is accepted exactly when the count is positive. -/ +theorem acceptCount_pos_iff : + 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by + rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] + constructor + · rintro ⟨w, -, hw⟩ + exact ⟨List.ofFn w, List.length_ofFn, hw⟩ + · rintro ⟨w, rfl, hw⟩ + exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ + +/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ +theorem acceptCount_add_card_filter_eq_false : + acceptCount V a n + + (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by + have := Finset.card_filter_add_card_filter_not (s := Finset.univ) + fun w : Fin n → Bool => V (a, List.ofFn w) = true + simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, + Fintype.card_fin] using this + +/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the +strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ +theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : + acceptCount V a (m + n) = + ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by + have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true + simp only [List.take_append_drop] at h + exact h + +/-- Verifiers that agree on an instance accept the same strings with it. -/ +theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : + acceptCount V a n = acceptCount W a n := by + simp only [acceptCount, h] + +/-- With no bits there is one string, the empty one. -/ +theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : + acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by + unfold acceptCount + rw [Finset.univ_unique, Finset.filter_singleton] + split_ifs with h₁ h₂ h₂ <;> simp_all + +/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ +@[simp] +theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by + simp [acceptCount] + +/-- The verifier rejecting everything accepts no string. -/ +@[simp] +theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by + simp [acceptCount] + +/-- A verifier and its negation together accept every string once. -/ +theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by + simpa only [acceptCount, Bool.not_eq_true'] using + acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) + +/-- The negation of a verifier accepts the strings that it rejects. -/ +theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : + acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by + have := acceptCount_add_acceptCount_not V a n + omega + +end acceptCount + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/SharpP.lean b/Complexity/Computability/Complexity/Classes/SharpP.lean index c61dce990..a8141bc0e 100644 --- a/Complexity/Computability/Complexity/Classes/SharpP.lean +++ b/Complexity/Computability/Complexity/Classes/SharpP.lean @@ -7,12 +7,12 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Complexity.AcceptCount public import Complexity.Computability.Complexity.Classes.NP public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain public import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Algebra.Order.Group.Int public import Mathlib.Data.Fintype.Pi -import Complexity.Foundations.Data.BitString.WordCount /-! # The counting classes #P and GapP @@ -21,7 +21,8 @@ import Complexity.Foundations.Data.BitString.WordCount [Valiant][Valiant1979], [Arora and Barak, Chapter 17][AroraBarak09]: `f ∈ SharpP enc` when there are a polynomial `p` and a function `V : α × List Bool → Bool`, computable in polynomial time on inputs `encPair enc encBits (a, w) = frame (enc a) ++ w`, such that `f a` is the number of strings -`w` of length `p (enc a).length` with `V (a, w) = true`. The problems in `NP` are exactly the sets +`w` of length `p (enc a).length` with `V (a, w) = true`, the count `Cslib.Complexity.acceptCount` +of `Complexity.Computability.Complexity.AcceptCount`. The problems in `NP` are exactly the sets where functions in `#P` are nonzero (`mem_NP_iff_exists_SharpP`). `GapP` consists of the differences of two functions in `#P`. Fenner, Fortnow and Kurtz define it @@ -36,16 +37,11 @@ signed routing and the corresponding bidirectional `GapP` characterization. ## Main definitions -* `Cslib.Complexity.acceptCount`: the number of strings of a given length that a verifier accepts - together with an instance. * `Cslib.Complexity.SharpP`, `Cslib.Complexity.GapP`. ## Main results * `Cslib.Complexity.mem_NP_iff_exists_SharpP`: `NP` consists of the supports of functions in `#P`. -* `Cslib.Complexity.acceptCount_add`: counting accepted strings by their prefixes. -* `Cslib.Complexity.acceptCount_zero`, `Cslib.Complexity.acceptCount_add_acceptCount_not`, - `Cslib.Complexity.acceptCount_not`: counts of trivial and negated verifiers. * `Cslib.Complexity.SharpP.exists_le_two_pow`: functions in `#P` are at most exponential. * `Cslib.Complexity.GapP.exists_abs_le_two_pow`: every `GapP` function is bounded in absolute value by `2 ^ p(|x|)` for a polynomial `p`. @@ -66,80 +62,6 @@ open Turing.MultiTapeTM variable {α : Type} -/-- The number of strings `w` of length `n` with `V (a, w) = true`. -/ -def acceptCount (V : α × List Bool → Bool) (a : α) (n : ℕ) : ℕ := - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = true).card - -section acceptCount - -variable {V : α × List Bool → Bool} {a : α} {n : ℕ} - -theorem acceptCount_le_two_pow : acceptCount V a n ≤ 2 ^ n := - (Finset.card_filter_le _ _).trans (by simp) - -theorem acceptCount_pos_iff : - 0 < acceptCount V a n ↔ ∃ w : List Bool, w.length = n ∧ V (a, w) = true := by - rw [acceptCount, Finset.card_pos, Finset.filter_nonempty_iff] - constructor - · rintro ⟨w, -, hw⟩ - exact ⟨List.ofFn w, List.length_ofFn, hw⟩ - · rintro ⟨w, rfl, hw⟩ - exact ⟨fun i => w[i.val], Finset.mem_univ _, by rwa [List.ofFn_getElem]⟩ - -/-- The strings that `V` accepts together with `a` and those it rejects are all the strings. -/ -theorem acceptCount_add_card_filter_eq_false : - acceptCount V a n + - (Finset.univ.filter fun w : Fin n → Bool => V (a, List.ofFn w) = false).card = 2 ^ n := by - have := Finset.card_filter_add_card_filter_not (s := Finset.univ) - fun w : Fin n → Bool => V (a, List.ofFn w) = true - simpa only [acceptCount, Bool.not_eq_true, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, - Fintype.card_fin] using this - -/-- **Counting strings by their prefixes**: the strings of length `m + n` accepted by `V` are the -strings `u ++ w`, with `u` of length `m` and `w` of length `n` accepted with the prefix `u`. -/ -theorem acceptCount_add (V : α × List Bool → Bool) (a : α) (m n : ℕ) : - acceptCount V a (m + n) = - ∑ u : Fin m → Bool, acceptCount (fun x => V (x.1, List.ofFn u ++ x.2)) a n := by - have h := BitString.card_filter_ofFn_add m n fun u w => V (a, u ++ w) = true - simp only [List.take_append_drop] at h - exact h - -/-- Verifiers that agree on an instance accept the same strings with it. -/ -theorem acceptCount_congr {W : α × List Bool → Bool} (h : ∀ w, V (a, w) = W (a, w)) (n : ℕ) : - acceptCount V a n = acceptCount W a n := by - simp only [acceptCount, h] - -/-- With no bits there is one string, the empty one. -/ -theorem acceptCount_zero (V : α × List Bool → Bool) (a : α) : - acceptCount V a 0 = if V (a, []) = true then 1 else 0 := by - unfold acceptCount - rw [Finset.univ_unique, Finset.filter_singleton] - split_ifs with h₁ h₂ h₂ <;> simp_all - -/-- The verifier accepting everything accepts all `2 ^ n` strings of length `n`. -/ -@[simp] -theorem acceptCount_true (a : α) (n : ℕ) : acceptCount (fun _ => true) a n = 2 ^ n := by - simp [acceptCount] - -/-- The verifier rejecting everything accepts no string. -/ -@[simp] -theorem acceptCount_false (a : α) (n : ℕ) : acceptCount (fun _ => false) a n = 0 := by - simp [acceptCount] - -/-- A verifier and its negation together accept every string once. -/ -theorem acceptCount_add_acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount V a n + acceptCount (fun x => !V x) a n = 2 ^ n := by - simpa only [acceptCount, Bool.not_eq_true'] using - acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := n) - -/-- The negation of a verifier accepts the strings that it rejects. -/ -theorem acceptCount_not (V : α × List Bool → Bool) (a : α) (n : ℕ) : - acceptCount (fun x => !V x) a n = 2 ^ n - acceptCount V a n := by - have := acceptCount_add_acceptCount_not V a n - omega - -end acceptCount - /-- The functions counting the certificates that a polynomial-time verifier accepts, with certificates of polynomial length, with respect to the encoding `enc` of instances. -/ def SharpP (enc : α ↪ List Bool) : Set (α → ℕ) := diff --git a/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean new file mode 100644 index 000000000..714b56d7b --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Time/AcceptCount.lean @@ -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 +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Time +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount + +/-! +# Time classes through accepting choice strings + +Problems in `NTIME` and `BPTIME` are decided by comparing the accepting count of a fixed +binary-choice machine (`Turing.MultiTapePTM.acceptCount`) with a threshold, at every number `τ` +of choice bits at least a linear function of the time bound. This is the normal form used by +counting simulations of nondeterministic and probabilistic time, which compute the accepting +count exactly. + +* A nondeterministic decider is replayed by its choice table `Turing.MultiTapeNTM.choiceTable`, + which encodes each choice in binary and rejects at a stuck configuration: an instance is a + member exactly when the accepting count is positive + (`Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`). +* A bounded-error fair-coin decider accepts a member with probability at least `2 / 3` and a + nonmember with probability at most `1 / 3`, so an instance is a member exactly when more than + half of the choice strings accept + (`Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`). + +Both hold for every `τ` at least the clock: a halted table ignores further bits. + +## Main results + +* `Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos`: nondeterministic + acceptance is a positive accepting count. +* `Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount`: + bounded-error acceptance is a strict-majority accepting count. +* `Cslib.Complexity.exists_acceptCount_of_mem_NTIME`, + `Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`: the class-level normal forms. +-/ + +public section + +namespace Turing.MultiTapeNTM + +variable {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} + +/-- **Nondeterministic acceptance is a positive accepting count.** If `ntm` decides `A` within +`t`, then `a ∈ A` exactly when some choice string of length `τ` makes the choice table accept, +for every `τ` of at least `M * t a`, where `M` is the number of actions. -/ +theorem DecidesInTime.mem_iff_acceptCount_choiceTable_pos {ntm : MultiTapeNTM k Bool State} + {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} + (hτ : Nat.card (Turing.Action k Bool State) * t a ≤ τ) : + a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ := by + rw [h.mem_iff_exists_checkChoices hτ, Cslib.Complexity.acceptCount_pos_iff] + rfl + +end Turing.MultiTapeNTM + +namespace Turing.MultiTapePTM + +open Cslib +open scoped ENNReal + +variable {k : ℕ} {State : Type} {α : Type} {enc : α ↪ List Bool} + +/-- A probability of at least `2 / 3` is more than one half. -/ +private theorem inv_two_lt_of_two_div_three_le {p : ℝ≥0∞} (h : 2 / 3 ≤ p) : 2⁻¹ < p := by + refine lt_of_lt_of_le ?_ h + rw [ENNReal.lt_div_iff_mul_lt (by simp) (by simp), ← ENNReal.div_eq_inv_mul, + ENNReal.div_lt_iff (by simp) (by simp)] + norm_num + +/-- Two distinct outcomes have total probability at most one. -/ +private theorem apply_add_apply_le_one {β : Type} (P : PMF β) {b b' : β} (hb : b ≠ b') : + P b + P b' ≤ 1 := by + classical + rw [← Finset.sum_pair hb, ← P.tsum_coe] + exact sum_le_tsum _ + +/-- **Bounded-error acceptance is a strict-majority accepting count.** If `machine` decides `A` +with bounded error within `t`, then `a ∈ A` exactly when more than half of the choice strings of +length `τ` accept, for every `τ` of at least `t a`. -/ +theorem DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount + {machine : MultiTapePTM k Bool State} {A : Set α} {t : α → ℕ} + (h : machine.DecidesWithBoundedErrorInTime enc A t) {a : α} {τ : ℕ} (hτ : t a ≤ τ) : + a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ := by + obtain ⟨hhalt, hprob⟩ := h a + rw [← machine.eval_runClosed_eq_of_halted (enc a) hτ hhalt] at hprob + rw [← half_lt_eval_runClosed_apply_iff] + by_cases ha : a ∈ A + · simp only [MultiTapeTM.indicator, ha] at hprob + exact iff_of_true ha (inv_two_lt_of_two_div_three_le hprob) + · simp only [MultiTapeTM.indicator, ha] at hprob + refine iff_of_false ha fun htrue => ?_ + have hsum := apply_add_apply_le_one (ProbComp.eval (machine.runClosed τ (enc a))) + (b := [true]) (b' := [false]) (by simp) + exact absurd ((ENNReal.inv_two_add_inv_two.symm.trans_lt + (ENNReal.add_lt_add htrue (inv_two_lt_of_two_div_three_le hprob))).trans_le hsum) + (lt_irrefl 1) + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open _root_.Turing + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} + +/-- **Nondeterministic time as accepting counts.** A problem in `NTIME enc t` is decided by a +fixed binary-choice machine with a binary alphabet and finitely many states: for constants `c₁` +and `c₂`, an instance is a member exactly when its accepting count on `τ` choice bits is +positive, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_NTIME (h : A ∈ NTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → (a ∈ A ↔ 0 < machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, ntm, hntm⟩ := h + set M := Nat.card (Turing.Action k Bool State) + refine ⟨k, _, inferInstance, ntm.choiceTable, M * c₁, M * c₂, fun a τ hτ => + hntm.mem_iff_acceptCount_choiceTable_pos ?_⟩ + rw [Nat.mul_add, ← Nat.mul_assoc] + exact hτ + +/-- **Bounded-error probabilistic time as accepting counts.** A problem in `BPTIME enc t` is +decided by a fixed fair-coin machine with a binary alphabet and finitely many states: for +constants `c₁` and `c₂`, an instance is a member exactly when more than half of its choice +strings of length `τ` accept, for every `τ ≥ c₁ * t n + c₂` on instances of encoded length `n`. -/ +theorem exists_acceptCount_of_mem_BPTIME (h : A ∈ BPTIME enc t) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) (c₁ c₂ : ℕ), + ∀ a τ, c₁ * t (enc a).length + c₂ ≤ τ → + (a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ) := by + obtain ⟨c₁, c₂, k, State, hfinite, machine, hmachine⟩ := h + exact ⟨k, State, hfinite, machine, c₁, c₂, fun a τ hτ => + hmachine.mem_iff_two_pow_lt_two_mul_acceptCount hτ⟩ + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean b/Complexity/Computability/Machines/Turing/MultiTape/Locality.lean new file mode 100644 index 000000000..3cb609e61 --- /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/Machine/ChoiceTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean index 6394b5428..487783761 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Machine/ChoiceTable.lean @@ -87,10 +87,8 @@ inductive OutputTrack namespace OutputTrack -instance : Finite OutputTrack := - Finite.of_surjective (fun i : Fin 3 => [empty, accept, other][i]) fun t => by - cases t - exacts [⟨0, rfl⟩, ⟨1, rfl⟩, ⟨2, rfl⟩] +instance : Fintype OutputTrack := + ⟨{empty, accept, other}, fun t => by cases t <;> simp⟩ /-- The track of a word. -/ def ofWord (word : List Bool) : OutputTrack := @@ -120,6 +118,24 @@ theorem ofWord_eq_accept_iff (word : List Bool) : ofWord word = accept ↔ word unfold ofWord split_ifs with h₁ h₂ <;> simp_all +/-- Emitting the same word after words with the same track gives words with the same track. -/ +theorem ofWord_append_eq_of_eq {word word' : List Bool} (h : ofWord word = ofWord word') + (more : List Bool) : ofWord (word ++ more) = ofWord (word' ++ more) := by + induction more using List.reverseRecOn with + | nil => simpa using h + | append_singleton more symbol ih => + have hsym : [symbol] = (some symbol).toList := rfl + rw [← List.append_assoc, ← List.append_assoc, hsym, ofWord_append, ofWord_append, ih] + +/-- A word with a given track: `[]`, `[true]` or `[false]`. -/ +def toWord : OutputTrack → List Bool + | empty => [] + | accept => [true] + | other => [false] + +@[simp] theorem ofWord_toWord (track : OutputTrack) : ofWord track.toWord = track := by + cases track <;> rfl + end OutputTrack /-- The states of the choice table: the simulated state, the index of the candidate action, and diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean new file mode 100644 index 000000000..a81d09a82 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/AcceptCount.lean @@ -0,0 +1,89 @@ +/- +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.Complexity.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic + +/-! +# Accepting choice strings of a fair-coin table + +A closed fair-coin table `Turing.MultiTapePTM k Bool State` is the binary-choice normal form of a +machine: a run is a deterministic replay of a list of choice bits, one bit per live step. When +both branches of an instruction agree, its bit is ignored, and a halted configuration ignores all +further bits (`Turing.MultiTapePTM.stepCoins`). So every run on `τ` bits is padded to exactly `τ` +steps. A nondeterministic machine with finitely many states and a binary alphabet is put in this +form by its choice table `Turing.MultiTapeNTM.choiceTable`, which encodes each choice in binary and +rejects at a stuck configuration. + +The *accepting count* `Turing.MultiTapePTM.acceptCount machine input τ` is the number of bit +strings `y ∈ {0,1}^τ` on which the table emits `[true]` on `input`: the count `A_M(x)` of the +counting simulations of nondeterministic and probabilistic time. It is the generic count +`Cslib.Complexity.acceptCount` of the replay predicate, so the elementary lemmas about that count +(`Cslib.Complexity.acceptCount_le_two_pow`, `Cslib.Complexity.acceptCount_pos_iff`, …) apply +to it directly. Its fraction of all `2 ^ τ` +strings is exactly the probability that the closed fair-coin run outputs `[true]` +(`Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`). The membership characterizations +for nondeterministic and bounded-error deciders are in +`Complexity.Computability.Complexity.Classes.Time.AcceptCount`. + +## Main definitions + +* `Turing.MultiTapePTM.acceptCount`: the number of accepting choice strings of a given length. + +## Main results + +* `Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount`: the probability of output `[true]` + is the accepting count divided by `2 ^ τ`. +* `Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff`: strict majority acceptance, as an + integer comparison `2 ^ τ < 2 * acceptCount`. +* `Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins`: the replay on upstream + configurations. +-/ + +public section + +namespace Turing.MultiTapePTM + +open Cslib Cslib.Probability +open scoped ENNReal + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) + (τ : ℕ) + +/-- **The accepting count** `A_M(x)`: the number of choice strings `y ∈ {0,1}^τ` replaying +which the closed fair-coin table emits `[true]` on `input`. -/ +abbrev acceptCount : ℕ := + Complexity.acceptCount + (fun p : List Bool × List Bool => decide (machine.runClosedCoins p.2 p.1 = [true])) input τ + +/-- **Acceptance probability is the accepting fraction.** The closed fair-coin run with clock +`τ` outputs `[true]` with probability `acceptCount / 2 ^ τ`. -/ +theorem eval_runClosed_apply_eq_acceptCount : + ProbComp.eval (machine.runClosed τ input) [true] = + (machine.acceptCount input τ : ℝ≥0∞) / 2 ^ τ := by + rw [eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + simp only [Complexity.acceptCount, decide_eq_true_eq] + +/-- **Strict majority acceptance** is the integer comparison `2 ^ τ < 2 * acceptCount`. -/ +theorem half_lt_eval_runClosed_apply_iff : + 2⁻¹ < ProbComp.eval (machine.runClosed τ input) [true] ↔ + 2 ^ τ < 2 * machine.acceptCount input τ := by + rw [eval_runClosed_apply_eq_acceptCount, ENNReal.lt_div_iff_mul_lt (by simp) (by simp), + ← ENNReal.div_eq_inv_mul, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] + exact_mod_cast Iff.rfl + +/-- The replay on the configurations of the shared interpreter is the replay on upstream +configurations, by deterministic steps under each coin. -/ +theorem runClosedCoins_eq_output_stepCoins (coins : List Bool) : + machine.runClosedCoins coins input = + (machine.stepCoins coins (Cfg.init machine.initial input)).output := by + rw [runClosedCoins, tapes_runClosedConfigFromCoins] + rfl + +end Turing.MultiTapePTM 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 000000000..5a41b6e99 --- /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/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean new file mode 100644 index 000000000..18eaa4a01 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IntervalTensor.lean @@ -0,0 +1,351 @@ +/- +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.Probabilistic.AcceptCount +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks +public import Complexity.Computability.Machines.Turing.MultiTape.Machine.ChoiceTable +public import Mathlib.Data.ZMod.Defs +import Mathlib.Data.ZMod.Basic +import Mathlib.Logic.Equiv.Fin.Basic +import Mathlib.Tactic.Linarith + +/-! +# Interval tensors of a choice-string run + +The local pieces of the block-counting identity, Lemma 2.2 of the note *Deterministic +simulations of nondeterministic and randomized time* (30 October 2026) formalized in issue #1833, +which builds on the blocking of Hopcroft, Paul and Valiant [HopcroftPaulValiant1977] in the +three-block form of `Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Blocks` +(compare [Williams2025], Lemma 2.1 and §3.2). The proof idea is original to that note. + +Fix a block length `b > 0`. A configuration of a fair-coin table over `Bool` is seen through + +* its *block indices* `Turing.Cfg.blockIndex`: the block `p / b` of every head; +* its *control record* `Turing.Cfg.blockControl`: its state, the offset `p mod b` of every head + in its block, and the track (`Turing.MultiTapeNTM.ChoiceTable.OutputTrack`) of its output; +* its *window contents* `Turing.Cfg.windowContents`: the contents of the three blocks + `J - 1, J, J + 1` around given block indices `J` on every work tape. + +Conversely, `Turing.embedCfg` builds a configuration from block indices, a control record and +window contents, with blank cells outside the windows and an output of the right track. The +*interval step* `Turing.MultiTapePTM.IntervalStep` replays the bits of a time interval from such +an embedded configuration and compares the record, window contents and block indices it leaves +with prescribed ones. The *interval tensor* `Turing.MultiTapePTM.intervalCount` counts the bit +strings `u ∈ {0,1}^b` doing so: the entry `F_i` of the note's equation (3). + +**Matching the true run** (`Turing.MultiTapePTM.intervalStep_view_iff`). Embedding the view of a +configuration `c` gives a configuration that agrees with `c` on its state, its heads and its +windows, and whose output has the same track. By the locality of runs +(`Turing.MultiTapePTM.agreeOn_blockWindow_stepCoins`), an interval step from the view of `c` +holds exactly when the true replay from `c` leaves the prescribed record, contents and block +indices. The input tape is not blocked as a word: it is fixed by `input`, which the embedded +configuration shares. + +**Splitting the count by schedules** (`Turing.MultiTapePTM.acceptCount_eq_sum_card_schedule`). +The accepting count `A_M(x)` on `q * b` bits is the sum, over the movement schedules `σ` of `q` +intervals, of the number of accepting choice strings with schedule `σ`. The bits of interval `i` +of a choice string `y : Fin (q * b) → Bool` are `y (finProdFinEquiv (i, r))` for `r < b` +(`Turing.MultiTapePTM.intervalStart_succ_ofFn`). + +## Main definitions + +* `Turing.Cfg.blockIndex`, `Turing.Cfg.blockContents`, `Turing.Cfg.windowContents`: block + indices and block contents. +* `Turing.BlockControl`, `Turing.Cfg.blockControl`: control records. +* `Turing.embedCfg`: the configuration with given block indices, record and window contents. +* `Turing.MultiTapePTM.IntervalStep`, `Turing.MultiTapePTM.intervalCount`: interval steps and + interval tensors. + +## Main results + +* `Turing.MultiTapePTM.acceptCount_eq_sum_card_schedule`: the accepting count split by schedules. +* `Turing.MultiTapePTM.intervalStart_succ_ofFn`: the bits of each interval. +* `Turing.agreeOn_embedCfg_view`: an embedded view agrees with the configuration on its windows. +* `Turing.MultiTapePTM.intervalStep_view_iff`: interval steps from a view are the true replay. +* `Turing.MultiTapePTM.intervalCount_le`: interval tensor entries are at most `2 ^ b`. + +## 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 + +open MultiTapeNTM.ChoiceTable + +variable {k : ℕ} {Symbol State : Type} + +/-! ### Views of a configuration -/ + +section View + +variable (b : ℕ) [NeZero b] {input : List Symbol} + +/-- The block index of every head, with blocks of length `b`: a head at coordinate `p` is in +block `p / b`. -/ +@[expose] def Cfg.blockIndex (c : Cfg k Symbol State input) (head : Option (Fin k)) : ℤ := + c.headPos head / b + +/-- The contents of block `j` of work tape `h`, with blocks of length `b`: the cells +`b * j + r` for `r < b`. -/ +@[expose] def Cfg.blockContents (c : Cfg k Symbol State input) (h : Fin k) (j : ℤ) : + ZMod b → Option Symbol := + fun r => c.workTapes h (b * j + r.val) + +/-- The contents of the three blocks `J h - 1, J h, J h + 1` around block indices `J` on every +work tape `h`; entry `d : Fin 3` is block `J h + d - 1`. -/ +@[expose] def Cfg.windowContents (J : Option (Fin k) → ℤ) (c : Cfg k Symbol State input) : + Fin k → Fin 3 → ZMod b → Option Symbol := + fun h d => c.blockContents b h (J (some h) + d - 1) + +end View + +section Embed + +variable (b : ℕ) [NeZero b] {input : List Bool} + +/-- A *control record* with blocks of length `b`: a state, the offset of every head in its block, +and the track of the output. -/ +abbrev BlockControl (k : ℕ) (State : Type) (b : ℕ) := + Option State × (Option (Fin k) → ZMod b) × OutputTrack + +/-- The control record of a configuration: its state, the offset `p mod b` of every head, and the +track of its output. -/ +@[expose] def Cfg.blockControl (c : Cfg k Bool State input) : + BlockControl k State b := + (c.state, fun head => (c.headPos head : ZMod b), OutputTrack.ofWord c.output) + +/-- The input head position with coordinate `p`, that is, stored position `p + 1`, or the +left end when `p + 1` is out of range. -/ +@[expose] def inputPosOfCoord (input : List Bool) (p : ℤ) : Fin (input.length + 2) := + if h : 0 ≤ p + 1 ∧ p + 1 < input.length + 2 then ⟨(p + 1).toNat, by omega⟩ else 0 + +/-- Cell `z` of work tape `h` of the configuration with window contents `w` at block indices `J`: +the entry of `w` if `z` lies in one of the three blocks around `J h`, and blank otherwise. -/ +@[expose] def windowCell (J : Option (Fin k) → ℤ) (w : Fin k → Fin 3 → ZMod b → Option Bool) + (h : Fin k) (z : ℤ) : Option Bool := + if hz : 0 ≤ z / b - J (some h) + 1 ∧ z / b - J (some h) + 1 < 3 then + w h ⟨(z / b - J (some h) + 1).toNat, by omega⟩ z + else none + +/-- The configuration with block indices `J`, control record `c` and window contents `w`: every +head at `b * J + offset`, the work tapes holding `w` on the windows and blank elsewhere, and an +output with the track of `c`. -/ +@[expose] def embedCfg (J : Option (Fin k) → ℤ) (c : BlockControl k State b) + (w : Fin k → Fin 3 → ZMod b → Option Bool) : Cfg k Bool State input where + state := c.1 + inputPos := inputPosOfCoord input (b * J none + (c.2.1 none).val) + workTapes := windowCell b J w + workTapePos h := b * J (some h) + (c.2.1 (some h)).val + output := c.2.2.toWord + +variable {b} + +/-- A coordinate is its block start plus its offset. -/ +private theorem mul_ediv_add_val_intCast (p : ℤ) : + (b : ℤ) * (p / b) + ((p : ZMod b).val : ℤ) = p := by + rw [ZMod.val_intCast] + exact Int.mul_ediv_add_emod p b + +omit [NeZero b] in +/-- The embedded configuration has the output track of its record. -/ +@[simp] theorem ofWord_output_embedCfg (J : Option (Fin k) → ℤ) (c : BlockControl k State b) + (w : Fin k → Fin 3 → ZMod b → Option Bool) : + OutputTrack.ofWord (embedCfg (input := input) b J c w).output = c.2.2 := + OutputTrack.ofWord_toWord _ + +/-- The cells of the window entries lie in the three blocks around the block index. -/ +private theorem mem_blockWindow_of_window {c : Cfg k Bool State input} (h : Fin k) (d : Fin 3) + (r : ZMod b) : + b * (c.blockIndex b (some h) + d - 1) + (r.val : ℤ) ∈ c.blockWindow b h := by + have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b + have hr : (r.val : ℤ) < b := by exact_mod_cast ZMod.val_lt r + have hd : ((d : ℕ) : ℤ) < 3 := by exact_mod_cast d.isLt + simp only [Cfg.blockWindow, Cfg.blockIndex, Cfg.headPos_some, Set.mem_Ico] + constructor <;> nlinarith + +/-- **An embedded view agrees with the configuration.** Embedding the block indices, control +record and window contents of `c` gives a configuration with the state, heads and window contents +of `c`. -/ +theorem agreeOn_embedCfg_view (c : Cfg k Bool State input) : + (embedCfg b (c.blockIndex b) (c.blockControl b) + (c.windowContents b (c.blockIndex b))).AgreeOn (c.blockWindow b) c := by + have hb : (0 : ℤ) < b := by exact_mod_cast Nat.pos_of_neZero b + refine ⟨rfl, ?_, ?_, fun h z hz => ?_⟩ + · -- The input head is at its coordinate plus one, which is in range. + have hpos := mul_ediv_add_val_intCast (b := b) (c.headPos none) + have hlt := c.inputPos.isLt + change inputPosOfCoord input + (b * (c.headPos none / b) + ((c.headPos none : ZMod b)).val) = c.inputPos + rw [hpos, Cfg.headPos_none] + unfold inputPosOfCoord + split_ifs with hcond + · ext + simp only + omega + · exact absurd ⟨by omega, by omega⟩ hcond + · funext h + exact mul_ediv_add_val_intCast (c.headPos (some h)) + · -- A window cell `z` is entry `z / b - J + 1` of the window, at offset `z mod b`. + simp only [Cfg.blockWindow, Set.mem_Ico] at hz + have hlo := Int.emod_nonneg z hb.ne' + have hhi := Int.emod_lt_of_pos z hb + have hval := mul_ediv_add_val_intCast (b := b) z + have hdiv := Int.mul_ediv_add_emod z b + have hJ : c.blockIndex b (some h) = c.workTapePos h / b := rfl + have h₁ : c.workTapePos h / b - 1 ≤ z / b := by + by_contra hcon + have : b * (z / b) ≤ b * (c.workTapePos h / b - 2) := + mul_le_mul_of_nonneg_left (by omega) hb.le + nlinarith + have h₂ : z / b < c.workTapePos h / b + 2 := by + by_contra hcon + have : b * (c.workTapePos h / b + 2) ≤ b * (z / b) := + mul_le_mul_of_nonneg_left (by omega) hb.le + nlinarith + have hcond : 0 ≤ z / b - c.blockIndex b (some h) + 1 ∧ + z / b - c.blockIndex b (some h) + 1 < 3 := by + rw [hJ] + omega + change windowCell b (c.blockIndex b) (c.windowContents b (c.blockIndex b)) h z = _ + rw [windowCell, dite_eq_left hcond] + simp only [Cfg.windowContents, Cfg.blockContents] + rw [Int.toNat_of_nonneg hcond.1, + show c.blockIndex b (some h) + (z / b - c.blockIndex b (some h) + 1) - 1 = z / b by ring, + hval] + +end Embed + +namespace MultiTapePTM + +variable (machine : MultiTapePTM k Bool State) {input : List Bool} + +/-! ### Interval steps and interval tensors -/ + +section Interval + +variable (b : ℕ) [NeZero b] + +/-- **An interval step.** Replaying `coins` from the configuration embedded at block indices `J` +with entering control record `cIn` and window contents `wIn` leaves the control record `cOut`, +the contents `wOut` of the same windows, and moves the block of every head `h` by `δ h`. -/ +def IntervalStep (input : List Bool) (J : Option (Fin k) → ℤ) (δ : Option (Fin k) → SignType) + (cIn : BlockControl k State b) (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (coins : List Bool) (cOut : BlockControl k State b) + (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : Prop := + (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).blockControl b = cOut ∧ + (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).windowContents b J = wOut ∧ + ∀ head, (machine.stepCoins coins (embedCfg (input := input) b J cIn wIn)).blockIndex b head = + J head + δ head + +open scoped Classical in +/-- **The interval tensor**: the number of bit strings `u ∈ {0,1}^b` whose replay is an interval +step from the entering record `cIn` and contents `wIn` at block indices `J` to the leaving record +`cOut` and contents `wOut`, moving the blocks by `δ`. This is the entry `F_i` of the note's +equation (3). -/ +noncomputable def intervalCount (input : List Bool) (J : Option (Fin k) → ℤ) + (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b) + (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : ℕ := + (Finset.univ.filter fun u : Fin b → Bool => + machine.IntervalStep b input J δ cIn wIn (List.ofFn u) cOut wOut).card + +omit [NeZero b] in +/-- An interval tensor entry is at most the number `2 ^ b` of bit strings. -/ +theorem intervalCount_le (input : List Bool) (J : Option (Fin k) → ℤ) + (δ : Option (Fin k) → SignType) (cIn : BlockControl k State b) + (wIn : Fin k → Fin 3 → ZMod b → Option Bool) + (cOut : BlockControl k State b) (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : + machine.intervalCount b input J δ cIn wIn cOut wOut ≤ 2 ^ b := by + classical + unfold intervalCount + exact (Finset.card_filter_le _ _).trans (by simp) + +/-- **Interval steps from a view are the true replay.** For at most `b` bits, an interval step +from the view of `c` (its block indices, control record and window contents) holds exactly when +replaying the bits from `c` itself leaves the prescribed record and window contents and moves the +blocks by `δ`. -/ +theorem intervalStep_view_iff (c : Cfg k Bool State input) {coins : List Bool} + (hlen : coins.length ≤ b) (δ : Option (Fin k) → SignType) (cOut : BlockControl k State b) + (wOut : Fin k → Fin 3 → ZMod b → Option Bool) : + machine.IntervalStep b input (c.blockIndex b) δ (c.blockControl b) + (c.windowContents b (c.blockIndex b)) coins cOut wOut ↔ + (machine.stepCoins coins c).blockControl b = cOut ∧ + (machine.stepCoins coins c).windowContents b (c.blockIndex b) = wOut ∧ + ∀ head, (machine.stepCoins coins c).blockIndex b head = c.blockIndex b head + δ head := by + set e := embedCfg (input := input) b (c.blockIndex b) (c.blockControl b) + (c.windowContents b (c.blockIndex b)) + obtain ⟨hagree, word, hword, hword'⟩ := + machine.agreeOn_blockWindow_stepCoins (Nat.pos_of_neZero b) hlen + (agreeOn_embedCfg_view c).symm (coins := coins) + replace hagree := hagree.symm + -- The two replays have the same state, heads, output track and window contents. + have htrack : OutputTrack.ofWord (machine.stepCoins coins e).output = + OutputTrack.ofWord (machine.stepCoins coins c).output := by + rw [hword, hword'] + refine OutputTrack.ofWord_append_eq_of_eq ?_ word + rw [ofWord_output_embedCfg] + rfl + have hcontrol : (machine.stepCoins coins e).blockControl b = + (machine.stepCoins coins c).blockControl b := by + rw [Cfg.blockControl, Cfg.blockControl, hagree.state_eq, hagree.headPos_eq, htrack] + have hwindow : (machine.stepCoins coins e).windowContents b (c.blockIndex b) = + (machine.stepCoins coins c).windowContents b (c.blockIndex b) := by + funext h d r + exact hagree.workTapes_eq h _ (mem_blockWindow_of_window h d r) + have hindex : (machine.stepCoins coins e).blockIndex b = + (machine.stepCoins coins c).blockIndex b := by + funext head + rw [Cfg.blockIndex, Cfg.blockIndex, hagree.headPos_eq] + rw [IntervalStep, hcontrol, hwindow, hindex] + +end Interval + +/-! ### Splitting the accepting count -/ + +/-- **The accepting count split by schedules.** The accepting choice strings of `q` intervals of +`b` bits are counted schedule by schedule. -/ +theorem acceptCount_eq_sum_card_schedule (input : List Bool) (b q : ℕ) : + machine.acceptCount input (q * b) = ∑ σ : Schedule k q, + (Finset.univ.filter fun y : Fin (q * b) → Bool => + machine.runClosedCoins (List.ofFn y) input = [true] ∧ + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input) = σ).card := by + classical + rw [acceptCount, Cslib.Complexity.acceptCount, Finset.card_eq_sum_card_fiberwise + (f := fun y : Fin (q * b) → Bool => + machine.schedule b q (List.ofFn y) (Cfg.init machine.initial input)) + (t := Finset.univ) fun _ _ => Finset.mem_coe.mpr (Finset.mem_univ _)] + refine Finset.sum_congr rfl fun σ _ => ?_ + rw [Finset.filter_filter] + simp only [decide_eq_true_eq] + +/-- **The bits of an interval.** For a choice string `y` of `q` intervals of `b` bits, interval +`i` replays the bits `y (finProdFinEquiv (i, r))`, `r < b`. -/ +theorem intervalStart_succ_ofFn {q b : ℕ} (y : Fin (q * b) → Bool) (c : Cfg k Bool State input) + (i : Fin q) : + machine.intervalStart b (List.ofFn y) c (i + 1) = + machine.stepCoins (List.ofFn fun r : Fin b => y (finProdFinEquiv (i, r))) + (machine.intervalStart b (List.ofFn y) c i) := by + rw [intervalStart_succ] + congr 1 + have hi := i.isLt + have hle : i * b + b ≤ q * b := by nlinarith + refine List.ext_getElem (by simp; omega) fun r h₁ h₂ => ?_ + simp only [List.getElem_take, List.getElem_drop, List.getElem_ofFn] + congr 1 + ext + change i * b + r = r + b * i + ring + +end MultiTapePTM + +end Turing diff --git a/ComplexityTests/HPVBlocks.lean b/ComplexityTests/HPVBlocks.lean new file mode 100644 index 000000000..8b8e0aa4a --- /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/ComplexityTests/HPVChoiceCount.lean b/ComplexityTests/HPVChoiceCount.lean new file mode 100644 index 000000000..d76ffc8f3 --- /dev/null +++ b/ComplexityTests/HPVChoiceCount.lean @@ -0,0 +1,161 @@ +/- +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.Complexity.Classes.Time.AcceptCount + +/-! Accepting choice strings of concrete fair-coin and nondeterministic machines. -/ + +namespace ComplexityTests.HPVChoiceCount + +open Cslib Turing +open scoped ENNReal + +/-- Emit the first coin and halt. -/ +private def emitCoin : MultiTapePTM 0 Bool Unit where + initial := () + tr _ _ _ _ bit := .step + { inputTape := 0, workTapes := Fin.elim0, output := some bit, state := none } + Empty.elim Empty.elim + +-- No step is taken without a choice bit: nothing is accepted. +example : emitCoin.acceptCount [] 0 = 0 := by decide + +-- After the first step the machine has halted, and the remaining bits are ignored. +example : emitCoin.acceptCount [] 1 = 1 := by decide +example : emitCoin.acceptCount [true, false] 3 = 4 := by decide + +-- The accepted fraction is the probability of output `[true]`. +example : ProbComp.eval (emitCoin.runClosed 3 [true, false]) [true] = 4 / 8 := by + rw [MultiTapePTM.eval_runClosed_apply_eq_acceptCount, + show emitCoin.acceptCount [true, false] 3 = 4 by decide] + norm_num + +-- Exactly half accept: this is not a strict majority. +example : ¬ 2⁻¹ < ProbComp.eval (emitCoin.runClosed 3 []) [true] := by + rw [MultiTapePTM.half_lt_eval_runClosed_apply_iff, + show emitCoin.acceptCount [] 3 = 4 by decide] + decide + +/-- Run two steps, each ignoring its coin, then emit `true` exactly when the input is +nonempty. -/ +private def readInput : MultiTapePTM 0 Bool (Fin 2) where + initial := 0 + tr state symbol _ _ _ := .step + (if state = 0 then { inputTape := 0, workTapes := Fin.elim0, output := none, state := some 1 } + else { inputTape := 0, workTapes := Fin.elim0, output := some symbol.isSome, state := none }) + Empty.elim Empty.elim + +-- Ignored bits still count: every string accepts, or none does. +example : readInput.acceptCount [false] 3 = 8 := by decide +example : readInput.acceptCount [] 3 = 0 := by decide +-- Before the decision step, no string accepts. +example : readInput.acceptCount [false] 1 = 0 := by decide + +/-! ### A bounded-error decider and the strict-majority criterion -/ + +/-- Emit `true` exactly when the first input symbol is `true`, ignoring the coin. -/ +private def echo : MultiTapePTM 0 Bool Unit where + initial := () + tr _ symbol _ _ _ := .step + { inputTape := 0, workTapes := Fin.elim0, output := some (symbol == some true), state := none } + Empty.elim Empty.elim + +/-- `echo` decides `{true}` (encoded as one-symbol words) with no error within one step. -/ +private theorem echo_decides : + echo.DecidesWithBoundedErrorInTime MultiTapeTM.encBool {b | b = true} fun _ => 1 := by + intro a + refine ⟨fun final hfinal => ?_, ?_⟩ + · rw [MultiTapePTM.eval_runClosedConfigFrom_eq_map_coins, PMF.mem_support_map_iff] at hfinal + obtain ⟨coins, hcoins, rfl⟩ := hfinal + obtain ⟨c, rfl⟩ := List.length_eq_one_iff.mp + (BitString.mem_support_uniformList_iff.mp hcoins) + cases a <;> cases c <;> rfl + · rw [MultiTapePTM.eval_runClosed_eq_map_coins, BitString.uniformList_map_apply] + cases a + · rw [show MultiTapeTM.indicator {b : Bool | b = true} false = false by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool false) = [false]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + · rw [show MultiTapeTM.indicator {b : Bool | b = true} true = true by + simp [MultiTapeTM.indicator]] + rw [show (Finset.univ.filter fun r : Fin 1 → Bool => + echo.runClosedCoins (List.ofFn r) (MultiTapeTM.encBool true) = [true]).card = 2 by + decide] + norm_num [ENNReal.div_self] + exact ENNReal.div_le_of_le_mul (by norm_num) + +-- With more bits than the clock, a member is accepted by all `2 ^ 4` strings. +example : true ∈ {b : Bool | b = true} ↔ 2 ^ 4 < 2 * echo.acceptCount [true] 4 := + echo_decides.mem_iff_two_pow_lt_two_mul_acceptCount (a := true) (by norm_num) +example : echo.acceptCount [true] 4 = 16 ∧ echo.acceptCount [false] 4 = 0 := by decide + +/-! ### Nondeterministic deciders through their choice tables -/ + +/-- Halt with output `[b]`. -/ +private def emit (b : Bool) : Action 0 Bool Bool := + { inputTape := 0, workTapes := Fin.elim0, output := some b, state := none } + +/-- From its only running state, either accept or reject. -/ +private def guess : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr q _ _ action := q = false ∧ (action = emit true ∨ action = emit false) + +private theorem guess_decides : + guess.DecidesInTime (Function.Embedding.refl (List Bool)) Set.univ fun _ => 1 := by + intro a + refine ⟨MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun c hc => ?_, ?_⟩ + · simp only [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init] at hc + obtain ⟨action, ⟨-, rfl | rfl⟩, rfl⟩ := hc <;> rfl + · have hstep : guess.Step (guess.initCfg a) ((emit true).apply (guess.initCfg a)) := + ⟨emit true, ⟨rfl, .inl rfl⟩, rfl⟩ + exact iff_of_true trivial + ⟨⟨(RelSeries.singleton _ _).cons (guess.initCfg a) hstep, rfl⟩, rfl, rfl⟩ + +-- The accepting branch is encoded by some padded choice string, of every sufficient length. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + 0 < guess.choiceTable.acceptCount x τ := + (guess_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mp trivial + +/-- A machine permitting no action: its initial configuration is stuck. -/ +private def stuck : MultiTapeNTM 0 Bool Bool where + q₀ := false + Tr _ _ _ _ := False + +private theorem stuck_decides : + stuck.DecidesInTime (Function.Embedding.refl (List Bool)) ∅ fun _ => 1 := by + intro a + have hrun : stuck.RunsInTime a 1 := + MultiTapeNTM.runsInTime_one_of_forall_step_initCfg fun _ hc => by + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at hc + refine ⟨hrun, iff_of_false id fun hacc => ?_⟩ + obtain ⟨p, hp, -⟩ := (MultiTapeNTM.accepts_iff_exists_time_eq hrun).mp hacc + have h0 := p.toRunPath.step ⟨0, by + unfold MultiTapeNTM.ComputationPath.time MultiTapeNTM.RunPath.time at hp; omega⟩ + change stuck.Step (p.toRunPath 0) _ at h0 + rw [show p.toRunPath 0 = stuck.initCfg a from p.head_eq] at h0 + simp [MultiTapeNTM.Step, MultiTapeNTM.initCfg, Cfg.init, stuck] at h0 + +-- The choice table rejects at the stuck configuration: no choice string accepts. +example (x : List Bool) (τ : ℕ) (hτ : Nat.card (Action 0 Bool Bool) ≤ τ) : + stuck.choiceTable.acceptCount x τ = 0 := + Nat.eq_zero_of_not_pos fun h => + (stuck_decides.mem_iff_acceptCount_choiceTable_pos (a := x) (by simpa using hτ)).mpr h + +/-! ### Class-level normal forms -/ + +example : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1 := + ⟨1, 0, 0, Unit, inferInstance, echo, by simpa using echo_decides⟩ + +example (h : {b : Bool | b = true} ∈ Complexity.BPTIME MultiTapeTM.encBool fun _ => 1) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapePTM k Bool State) + (c₁ c₂ : ℕ), ∀ a τ, c₁ * 1 + c₂ ≤ τ → + (a ∈ {b : Bool | b = true} ↔ 2 ^ τ < 2 * machine.acceptCount (MultiTapeTM.encBool a) τ) := + Complexity.exists_acceptCount_of_mem_BPTIME h + +end ComplexityTests.HPVChoiceCount diff --git a/ComplexityTests/HPVIntervalTensors.lean b/ComplexityTests/HPVIntervalTensors.lean new file mode 100644 index 000000000..aceca6816 --- /dev/null +++ b/ComplexityTests/HPVIntervalTensors.lean @@ -0,0 +1,106 @@ +/- +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.IntervalTensor + +/-! Views, embeddings and interval steps of a concrete choice-string run, with blocks of +length `2`. -/ + +namespace ComplexityTests.HPVIntervalTensors + +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] + +/-! ### Embedding a view keeps the window and forgets the rest -/ + +/-- The start configuration with marks in its window `[-2, 4)` (cell `3`) and outside it +(cell `5`). -/ +private def marked : Cfg 1 Bool Unit [true, false] := + { start with workTapes := fun _ z => if z = 3 ∨ z = 5 then some false else none } + +/-- The configuration embedded from the view of `marked`. -/ +private noncomputable def markedView : Cfg 1 Bool Unit [true, false] := + embedCfg 2 (marked.blockIndex 2) (marked.blockControl 2) + (marked.windowContents 2 (marked.blockIndex 2)) + +-- The mark in the window is kept. +example : markedView.workTapes 0 3 = some false := + (agreeOn_embedCfg_view marked).workTapes_eq 0 3 (by simp [Cfg.blockWindow, marked, start]) + +-- The mark outside the window is forgotten: block `2` is not part of the view. +example : markedView.workTapes 0 5 = none := by + simp only [markedView, embedCfg, windowCell] + rw [dite_eq_right (by decide)] + +/-! ### Interval steps -/ + +/-- After `true, true` both heads have moved two cells to the right. -/ +private noncomputable def after : Cfg 1 Bool Unit [true, false] := + zigzag.stepCoins [true, true] start + +private theorem headPos_after : after.headPos = fun _ => 2 := by + funext head + cases head <;> (rw [after, stepCoins_eq]; rfl) + +-- The interval wrote `true` into cells `0` and `1`: offsets `0` and `1` of the middle block. +example : after.windowContents 2 (start.blockIndex 2) 0 1 = fun _ => some true := by + funext r + fin_cases r <;> (rw [after, stepCoins_eq]; rfl) + +/-- Both heads move one block to the right. -/ +private theorem blockIndex_after (head : Option (Fin 1)) : + after.blockIndex 2 head = start.blockIndex 2 head + ((1 : SignType) : ℤ) := by + simp only [Cfg.blockIndex, headPos_after, Cfg.headPos_init, start] + rfl + +-- From the view of `start`, the interval step on `true, true` leaves the record and window of +-- the true replay and moves both blocks by `+1`. +example : zigzag.IntervalStep 2 [true, false] (start.blockIndex 2) (fun _ => 1) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) [true, true] + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) := + (zigzag.intervalStep_view_iff 2 start (by decide) _ _ _).mpr ⟨rfl, rfl, blockIndex_after⟩ + +-- The schedule entry is checked: the step does not keep the work head in its block. +example : ¬ zigzag.IntervalStep 2 [true, false] (start.blockIndex 2) (fun _ => 0) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) [true, true] + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) := by + rw [zigzag.intervalStep_view_iff 2 start (by decide)] + rintro ⟨-, -, h⟩ + have := (h (some 0)).symm.trans (blockIndex_after (some 0)) + simp at this + +/-- An entry of the interval tensor counts at most the `4` bit strings of the interval. -/ +example : zigzag.intervalCount 2 [true, false] (start.blockIndex 2) (fun _ => 1) + (start.blockControl 2) (start.windowContents 2 (start.blockIndex 2)) + (after.blockControl 2) (after.windowContents 2 (start.blockIndex 2)) ≤ 4 := + zigzag.intervalCount_le 2 _ _ _ _ _ _ _ + +/-! ### Bits of an interval -/ + +-- With two intervals of two bits, interval `1` replays bits `2` and `3`. +example (y : Fin (2 * 2) → Bool) : + zigzag.intervalStart 2 (List.ofFn y) start 2 = + zigzag.stepCoins [y 2, y 3] (zigzag.intervalStart 2 (List.ofFn y) start 1) := by + exact zigzag.intervalStart_succ_ofFn y start 1 + +end ComplexityTests.HPVIntervalTensors diff --git a/references.bib b/references.bib index e41912a56..8d4525226 100644 --- a/references.bib +++ b/references.bib @@ -2288,6 +2288,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},