From f64dca005030dcbcef0004bf8fb864d5d5e317bd Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:32:37 +0000 Subject: [PATCH 1/4] feat(LogSpace): configuration matrix of fair-coin machines (#474) Coin-driven transition matrices (Foundations) and, for a fair-coin machine on a closed set of views, the acceptance probability as an entry of N^t e, of the substochastic sum, and of (1 - S/2)^-1 e. BPL through polynomial-size configuration matrices. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Classes/LogSpace/Randomized.lean | 2 + .../Randomized/ConfigurationMatrix.lean | 379 ++++++++++++++++++ .../Complexity/LogSpace/Configurations.lean | 24 ++ .../Complexity/LogSpace/HaltingTime.lean | 26 +- .../Complexity/LogSpace/Reachability.lean | 16 +- .../LinearAlgebra/Matrix/CoinStep.lean | 204 ++++++++++ ComplexityTests/CoinStepMatrix.lean | 58 +++ ComplexityTests/RandomizedLogSpace.lean | 48 +++ references.bib | 21 + 10 files changed, 742 insertions(+), 38 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean create mode 100644 Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean create mode 100644 ComplexityTests/CoinStepMatrix.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f223..dccd119200 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1003,6 +1003,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Tr public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs @@ -2620,6 +2621,7 @@ public import Complexity.Foundations.LinearAlgebra.ExchangeReplacement public import Complexity.Foundations.LinearAlgebra.ImageSparsification public import Complexity.Foundations.LinearAlgebra.Interpolation public import Complexity.Foundations.LinearAlgebra.KernelVector +public import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep public import Complexity.Foundations.LinearAlgebra.Matrix.CutRank public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean index 414ac55d3d..a1f91e687b 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean @@ -32,6 +32,8 @@ instance. The threshold `1/2` for `RL` can be raised to `1 - 2 ^ (-r)` for any fixed `r` by repetition (`Cslib.Complexity.mem_RL_iff_error_le`), which also gives `Cslib.Complexity.RL_subset_BPL`. +The acceptance probability is an entry of a power or inverse of a polynomial-size configuration +matrix (`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). The model follows the decision recorded in issue #474: one-way coins, halting on every branch with the polynomial clock a derived lemma, acceptance by counting coin strings, and space as for `NL` diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean new file mode 100644 index 0000000000..7f786876f0 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean @@ -0,0 +1,379 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized +public import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep + +/-! +# The configuration matrix of a fair-coin machine + +A fair-coin machine moves each running view (`Turing.FiniteCfg`, the configuration with its work +tapes stored relative to their heads and its output summarized) to one of two views, selected by +the coin (`Turing.MultiTapePTM.viewCoinStep`); a halted view stays put. On a finite set `V` of +views closed under these steps, this gives two matrices indexed by `V`: + +* the *configuration matrix* `Turing.MultiTapePTM.configMatrix`, whose entry `(x, y)` counts the + coins moving `x` to `y`, so that half of it is the stochastic matrix of the run, with halted + views absorbing; +* the *live configuration matrix* `Turing.MultiTapePTM.liveConfigMatrix`, the same rows at + running views and zero rows at halted views, so that half of it is substochastic. + +With `e` the indicator of the accepting halted views (`Turing.FiniteCfg.acceptVec`), the number of +accepting coin strings of length `t` is the entry at the initial view of `N ^ t *ᵥ e` +(`Turing.MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec`), so the acceptance probability is +`((N / 2) ^ t *ᵥ e)(start)`. Splitting the coin strings by the time they halt gives the +substochastic form `∑ t ≤ T, ((S / 2) ^ t *ᵥ e)(start)` +(`Turing.MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix`). When every view of `V` is +reachable and every branch halts within `T` steps, `S / 2` is nilpotent, and the acceptance +probability is `((1 - S / 2)⁻¹ *ᵥ e)(start)` +(`Turing.MultiTapePTM.acceptCoins_div_eq_inv_mulVec`). + +The reachable views form such a set (`Turing.MultiTapePTM.exists_finset_reachable`), with at most +`2 ^ (2 * coreLengthBound k State n s + 1)` elements under a space bound `s`, polynomially many +under a logarithmic one. So a `BPL` language is decided by the entry at the initial view of +`(1 - S / 2)⁻¹ *ᵥ e` for a polynomial-size matrix `S` +(`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). This is the Markov chain of a probabilistic +machine on its configurations [Gill][Gill1977], whose powers and inverse Borodin, Cook and +Pippenger compute in parallel to place probabilistic space `s` in `DSPACE(s²)` +[Borodin, Cook and Pippenger][BorodinCookPippenger1983]; for `BPL` this gives +`BPL ⊆ DSPACE(log² n)` and `BPL ⊆ P` [Hoza, Section 4.3][Hoza2022]. Those algorithms are not +formalized here. + +The matrices are indexed by an arbitrary closed set of views rather than a set of +configurations of bounded size, and have no time layers: the model of `Cslib.Complexity.BPL` +requires every branch to halt, which already makes the live matrix nilpotent on the reachable +views. The form `N ^ t` with absorbing halted views is the one repeated squaring computes; the +form `(1 - S / 2)⁻¹` with a nilpotent substochastic matrix is the one of matrix inversion. + +## Main definitions + +* `Turing.MultiTapePTM.viewCoinStep`: the view reached under one coin. +* `Turing.FiniteCfg.acceptVec`: the indicator of the accepting halted views. +* `Turing.MultiTapePTM.configMatrix`, `Turing.MultiTapePTM.liveConfigMatrix`: the configuration + matrix and its rows at running views. + +## Main results + +* `Turing.MultiTapePTM.viewRep_foldl_viewCoinStep`: coin steps of views follow coin replays. +* `Turing.MultiTapePTM.reflTransGen_viewStep_toNTM_iff`: the reachable views are those reached by + coin strings. +* `Turing.MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec`: accepting coin strings are an + entry of a power of the configuration matrix. +* `Turing.MultiTapePTM.acceptCoins_div_eq_configMatrix_pow_mulVec`: the acceptance probability + is an entry of a power of the stochastic matrix. +* `Turing.MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix`: the substochastic form. +* `Turing.MultiTapePTM.liveConfigMatrix_pow_eq_zero`: under a halting time, the live matrix is + nilpotent on reachable views. +* `Turing.MultiTapePTM.acceptCoins_div_eq_inv_mulVec`: the acceptance probability is an entry of + `(1 - S / 2)⁻¹ *ᵥ e`. +* `Turing.MultiTapePTM.exists_finset_reachable`: the reachable views form a small closed set. +* `Cslib.Complexity.exists_configMatrix_of_mem_BPL`: `BPL` through polynomial-size configuration + matrices. + +## References + +* [A. Borodin, S. Cook, N. Pippenger, *Parallel computation for well-endowed rings and + space-bounded probabilistic machines*][BorodinCookPippenger1983] +* [W. Hoza, *Recent progress on derandomizing space-bounded computation*][Hoza2022] +* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977] +-/ + +@[expose] public section + +open Cslib.Turing + +namespace Turing + +open scoped Classical in +/-- The indicator of the accepting halted views in a set `V` of views: `1` at the halted views +with output `[true]`, `0` elsewhere. -/ +noncomputable def FiniteCfg.acceptVec {k : ℕ} {State : Type} (R : Type*) [Zero R] [One R] + (V : Finset (FiniteCfg k Bool State)) : V → R := + fun v => if (v : FiniteCfg k Bool State).state = none ∧ + (v : FiniteCfg k Bool State).output = [true] then 1 else 0 + +namespace MultiTapePTM + +open MultiTapeMachine Matrix + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) + +/-- **The view reached under one coin**: a halted view stays put; a running view takes the action +selected by the coin, and its output is summarized. -/ +noncomputable def viewCoinStep (finite : FiniteCfg k Bool State) (bit : Bool) : + FiniteCfg k Bool State := + match finite.state with + | none => finite + | some state => (finite.step ((machine.withCoin bit).toTM.tr state finite.inputSymbol + finite.workTapeSymbols)).summarizeOutput + +open scoped Classical in +/-- **The configuration matrix** on a set `V` of views: the entry at `(x, y)` counts the coins +that move `x` to `y`. Half of it is the stochastic matrix of the run, with halted views +absorbing. -/ +noncomputable def configMatrix (R : Type*) [CommSemiring R] (V : Finset (FiniteCfg k Bool State)) : + Matrix V V R := + Matrix.coinStepMatrix machine.viewCoinStep V + +open scoped Classical in +/-- **The live configuration matrix**: the rows of `Turing.MultiTapePTM.configMatrix` at running +views, and zero rows at halted views. Half of it is substochastic. -/ +noncomputable def liveConfigMatrix (R : Type*) [CommSemiring R] + (V : Finset (FiniteCfg k Bool State)) : Matrix V V R := + Matrix.liveCoinStepMatrix machine.viewCoinStep V fun finite => finite.state ≠ none + +variable {machine} + +/-- A halted view stays put. -/ +theorem viewCoinStep_of_halted {finite : FiniteCfg k Bool State} (h : finite.state = none) + (bit : Bool) : machine.viewCoinStep finite bit = finite := by + simp only [viewCoinStep, h] + +/-- **Coin steps of views follow coin steps of configurations.** -/ +theorem viewRep_viewCoinStep {input : List Bool} {finite : FiniteCfg k Bool State} + {cfg : Cfg k Bool State input} (h : MultiTapeNTM.ViewRep finite cfg) (bit : Bool) : + MultiTapeNTM.ViewRep (machine.viewCoinStep finite bit) + ((machine.withCoin bit).toTM.step cfg) := by + rcases hs : cfg.state with _ | state + · rw [MultiTapeTM.step_of_halt hs, viewCoinStep_of_halted (h.state.trans hs)] + exact h + · obtain ⟨hin, hwork⟩ := h.symbols + rw [MultiTapeTM.step_of_state hs] + simp only [MultiTapePTM.viewCoinStep, h.state.trans hs, hin, hwork] + exact h.step _ + +/-- **Coin strings replay on views as on configurations.** -/ +theorem viewRep_foldl_viewCoinStep {input : List Bool} {finite : FiniteCfg k Bool State} + {cfg : Cfg k Bool State input} (h : MultiTapeNTM.ViewRep finite cfg) (coins : List Bool) : + MultiTapeNTM.ViewRep (coins.foldl machine.viewCoinStep finite) + (machine.stepCoins coins cfg) := by + induction coins generalizing finite cfg with + | nil => exact h + | cons bit coins ih => exact ih (viewRep_viewCoinStep h bit) + +/-- The steps of the views of the nondeterministic view are the coin steps. -/ +theorem viewStep_toNTM_iff {finite next : FiniteCfg k Bool State} : + machine.toNTM.ViewStep finite next ↔ ∃ bit, machine.viewCoinStep finite bit = next := by + rcases hs : finite.state with _ | state + · simp only [MultiTapeNTM.ViewStep, hs, viewCoinStep_of_halted hs, exists_const] + exact eq_comm + · simp only [MultiTapeNTM.ViewStep, hs, viewCoinStep, tr_toNTM_iff, MultiTapeTM.tr_iff] + constructor + · rintro ⟨action, ⟨bit, rfl⟩, rfl⟩ + exact ⟨bit, rfl⟩ + · rintro ⟨bit, rfl⟩ + exact ⟨_, ⟨bit, rfl⟩, rfl⟩ + +/-- **The reachable views are those reached by coin strings.** -/ +theorem reflTransGen_viewStep_toNTM_iff {finite next : FiniteCfg k Bool State} : + Relation.ReflTransGen machine.toNTM.ViewStep finite next ↔ + ∃ coins : List Bool, coins.foldl machine.viewCoinStep finite = next := by + constructor + · intro h + induction h with + | refl => exact ⟨[], rfl⟩ + | tail _ hstep ih => + obtain ⟨coins, rfl⟩ := ih + obtain ⟨bit, rfl⟩ := viewStep_toNTM_iff.mp hstep + exact ⟨coins ++ [bit], by simp⟩ + · rintro ⟨coins, rfl⟩ + induction coins using List.reverseRecOn with + | nil => exact .refl + | append_singleton coins bit ih => + rw [List.foldl_append, List.foldl_cons, List.foldl_nil] + exact ih.tail (viewStep_toNTM_iff.mpr ⟨bit, rfl⟩) + +/-- The accepting coin strings are those whose replay on views ends in an accepting halted +view. -/ +private theorem acceptCoins_eq_card_views (input : List Bool) (t : ℕ) : + machine.acceptCoins input t = (Finset.univ.filter fun w : Fin t → Bool => + ((List.ofFn w).foldl machine.viewCoinStep (machine.toNTM.initView input)).state = none ∧ + ((List.ofFn w).foldl machine.viewCoinStep (machine.toNTM.initView input)).output = + [true]).card := by + classical + unfold acceptCoins + congr 1 + refine Finset.filter_congr fun w _ => ?_ + have h := viewRep_foldl_viewCoinStep (machine := machine) + (MultiTapeNTM.viewRep_init (ntm := machine.toNTM) input) (List.ofFn w) + rw [h.state, h.output, MultiTapeNTM.outputClass_eq_true_iff] + +open scoped Classical in +/-- **Accepting coin strings are an entry of a power of the configuration matrix**: on a set `V` +of views that contains the initial view and is closed under coin steps, the number of accepting +coin strings of length `t` is the entry at the initial view of `N ^ t *ᵥ e`. -/ +theorem acceptCoins_eq_configMatrix_pow_mulVec (R : Type*) [CommSemiring R] {input : List Bool} + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (t : ℕ) : + (machine.acceptCoins input t : R) = + (machine.configMatrix R V ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + classical + have := Matrix.coinStepMatrix_pow_mulVec (R := R) hV + (fun finite : FiniteCfg k Bool State => + if finite.state = none ∧ finite.output = [true] then 1 else 0) t ⟨_, hinit⟩ + rw [configMatrix] + convert this.symm using 1 + · rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_one, + acceptCoins_eq_card_views] + · rfl + +open scoped Classical in +/-- **The acceptance probability is an entry of a power of the stochastic matrix**: with +`P = N / 2` the stochastic matrix of the run, `acceptCoins input t / 2 ^ t` is the entry at the +initial view of `P ^ t *ᵥ e`. -/ +theorem acceptCoins_div_eq_configMatrix_pow_mulVec (R : Type*) [Field R] {input : List Bool} + {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (t : ℕ) : + (machine.acceptCoins input t : R) / 2 ^ t = + (((2 : R)⁻¹ • machine.configMatrix R V) ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + rw [smul_pow, Matrix.smul_mulVec, Pi.smul_apply, + ← acceptCoins_eq_configMatrix_pow_mulVec R hV hinit, smul_eq_mul, inv_pow, div_eq_inv_mul] + +open scoped Classical in +/-- **The substochastic form**: splitting the coin strings by the time the run halts, +`acceptCoins input T / 2 ^ T` is the entry at the initial view of `∑ t ≤ T, (S / 2) ^ t *ᵥ e`, +with `S` the live configuration matrix. No halting time is needed. -/ +theorem acceptCoins_div_eq_sum_liveConfigMatrix (R : Type*) [Field R] [CharZero R] + {input : List Bool} {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (T : ℕ) : + (machine.acceptCoins input T : R) / 2 ^ T = ∑ t ∈ Finset.range (T + 1), + (((2 : R)⁻¹ • machine.liveConfigMatrix R V) ^ t *ᵥ FiniteCfg.acceptVec R V) ⟨_, hinit⟩ := by + classical + have h := Matrix.coinStepMatrix_pow_mulVec_eq_sum (R := R) hV + (live := fun finite : FiniteCfg k Bool State => finite.state ≠ none) + (fun finite hfinite => viewCoinStep_of_halted (not_not.mp hfinite)) + (f := fun finite : FiniteCfg k Bool State => + if finite.state = none ∧ finite.output = [true] then 1 else 0) + (fun finite hfinite => ite_eq_right_iff.mpr fun h => absurd h.1 hfinite) T ⟨_, hinit⟩ + have hvec : (fun v : V => if (v : FiniteCfg k Bool State).state = none ∧ + (v : FiniteCfg k Bool State).output = [true] then (1 : R) else 0) = + FiniteCfg.acceptVec R V := rfl + rw [hvec] at h + rw [acceptCoins_eq_configMatrix_pow_mulVec R hV hinit, configMatrix] + convert congrArg (· / (2 : R) ^ T) h using 1 + · rw [Finset.sum_div] + refine Finset.sum_congr rfl fun t ht => ?_ + have htT : t ≤ T := Nat.lt_succ_iff.mp (Finset.mem_range.mp ht) + rw [smul_pow, Matrix.smul_mulVec, Pi.smul_apply, smul_eq_mul, liveConfigMatrix] + have h2 : (2 : R) ^ T = 2 ^ (T - t) * 2 ^ t := by rw [← pow_add, Nat.sub_add_cancel htT] + rw [h2, inv_pow, mul_div_mul_left _ _ (pow_ne_zero _ two_ne_zero), div_eq_inv_mul] + +open scoped Classical in +/-- **The live matrix is nilpotent on reachable views**: if every view of `V` is reachable and +every branch halts within `T` steps, then `S ^ (T + 1) = 0`. -/ +theorem liveConfigMatrix_pow_eq_zero (R : Type*) [CommSemiring R] {input : List Bool} {T : ℕ} + (ht : machine.toNTM.RunsInTime input T) {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hreach : ∀ finite ∈ V, + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) : + machine.liveConfigMatrix R V ^ (T + 1) = 0 := by + classical + refine Matrix.liveCoinStepMatrix_pow_eq_zero hV fun x hx w => ⟨Fin.last T, ?_⟩ + obtain ⟨coins, hcoins⟩ := reflTransGen_viewStep_toNTM_iff.mp (hreach x hx) + have h := viewRep_foldl_viewCoinStep (machine := machine) + (MultiTapeNTM.viewRep_init (ntm := machine.toNTM) input) (coins ++ (List.ofFn w).take T) + have hhalt := halted_stepCoins machine ht (coins := coins ++ (List.ofFn w).take T) + (by simp) + rw [List.foldl_append, hcoins] at h + simpa using h.state.trans hhalt + +open scoped Classical in +/-- **The acceptance probability is an entry of `(1 - S / 2)⁻¹ *ᵥ e`**: if every view of `V` is +reachable and every branch halts within `T` steps, then `acceptCoins input T / 2 ^ T` is the +entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e`, with `S` the live configuration matrix. -/ +theorem acceptCoins_div_eq_inv_mulVec (R : Type*) [Field R] [CharZero R] {input : List Bool} + {T : ℕ} (ht : machine.toNTM.RunsInTime input T) {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hreach : ∀ finite ∈ V, + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) + (hinit : machine.toNTM.initView input ∈ V) : + (machine.acceptCoins input T : R) / 2 ^ T = + ((1 - (2 : R)⁻¹ • machine.liveConfigMatrix R V)⁻¹ *ᵥ FiniteCfg.acceptVec R V) + ⟨_, hinit⟩ := by + rw [Matrix.inv_one_sub_eq_sum_pow (n := T + 1) (by + rw [smul_pow, liveConfigMatrix_pow_eq_zero R ht hV hreach, smul_zero]), + Matrix.sum_mulVec, Finset.sum_apply, acceptCoins_div_eq_sum_liveConfigMatrix R hV hinit] + +/-- **The reachable views form a small closed set**: under a space bound `s`, the views reachable +from the initial view form a finite set, closed under coin steps, with at most +`2 ^ (2 * coreLengthBound k State n s + 1)` elements. -/ +theorem exists_finset_reachable [Finite State] {input : List Bool} {s : ℕ} + (hs : machine.toNTM.RunsInSpace input s) : + ∃ V : Finset (FiniteCfg k Bool State), + (∀ finite, finite ∈ V ↔ + Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) finite) ∧ + (∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) ∧ + V.card ≤ 2 ^ (2 * MultiTapeNTM.coreLengthBound k State input.length s + 1) := by + set reach := {finite | Relation.ReflTransGen machine.toNTM.ViewStep + (machine.toNTM.initView input) finite} + have hfin : reach.Finite := by + by_contra hinf + obtain ⟨V, hsub, hcard⟩ := Set.Infinite.exists_subset_card_eq hinf + (2 ^ (2 * MultiTapeNTM.coreLengthBound k State input.length s + 1) + 1) + have := MultiTapeNTM.length_le_of_nodup_reachable hs V.nodup_toList + fun finite hf => hsub (Finset.mem_toList.mp hf) + rw [Finset.length_toList, hcard] at this + omega + refine ⟨hfin.toFinset, fun finite => hfin.mem_toFinset, fun finite hf bit => ?_, ?_⟩ + · rw [hfin.mem_toFinset] at hf ⊢ + exact Relation.ReflTransGen.tail hf (viewStep_toNTM_iff.mpr ⟨bit, rfl⟩) + · rw [← Finset.length_toList] + exact MultiTapeNTM.length_le_of_nodup_reachable hs (Finset.nodup_toList _) + fun finite hf => hfin.mem_toFinset.mp (Finset.mem_toList.mp hf) + +end MultiTapePTM + +end Turing + +namespace Cslib.Complexity + +open _root_.Turing Matrix + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} + +open scoped Classical in +/-- **`BPL` through polynomial-size configuration matrices**: a `BPL` machine has, on every +encoded instance of length `n`, a closed set `V` of at most `2 * (2 * (n + 1)) ^ d` views, +containing the initial view, such that the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is +at least `2/3` on members and at most `1/3` on non-members, with `S` the live configuration +matrix on `V` and `e` the indicator of the accepting halted views. -/ +theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : + ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : MultiTapePTM k Bool State) (d : ℕ), + ∀ a, ∃ (V : Finset (FiniteCfg k Bool State)) (hinit : M.toNTM.initView (enc a) ∈ V), + V.card ≤ 2 * (2 * ((enc a).length + 1)) ^ d ∧ + (∀ finite ∈ V, ∀ bit, M.viewCoinStep finite bit ∈ V) ∧ + (a ∈ A → 2 / 3 ≤ ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩) ∧ + (a ∉ A → ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ ≤ 1 / 3) := by + obtain ⟨k, State, hfin, M, c, hM⟩ := h + refine ⟨k, State, hfin, M, 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1), + fun a => ?_⟩ + obtain ⟨hs, t, ht, hmem, hnot⟩ := hM a + obtain ⟨V, hreach, hV, hcard⟩ := M.exists_finset_reachable hs + have hinit : M.toNTM.initView (enc a) ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, hcard.trans (MultiTapeNTM.two_pow_coreLengthBound_log_le k State c _), hV, + fun ha => ?_, fun ha => ?_⟩ + all_goals + rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV (fun finite hf => (hreach _).mp hf)] + · have h : ((2 * 2 ^ t : ℕ) : ℚ) ≤ ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) := + Nat.cast_le.mpr (hmem ha) + push_cast at h + rw [le_div_iff₀ (by positivity)] + linarith + · have h : ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) ≤ ((2 ^ t : ℕ) : ℚ) := + Nat.cast_le.mpr (hnot ha) + push_cast at h + rw [div_le_iff₀ (by positivity)] + linarith + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean index 192d768942..c3d7bdd0a2 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Configurations.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Space public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding public import Complexity.Foundations.Data.BitString.Enumeration import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength +import Complexity.Foundations.Data.Nat.Log import Mathlib.Data.Nat.Size import Mathlib.Tactic.Linarith @@ -39,6 +40,8 @@ views are reachable (`Turing.MultiTapeNTM.length_le_of_nodup_reachable`), polyno * `Turing.MultiTapeNTM.coreCode_injective`: the code identifies views with the same input. * `Turing.MultiTapeNTM.length_coreCode_le`: reachable views have short codes. * `Turing.MultiTapeNTM.length_le_of_nodup_reachable`: few distinct views are reachable. +* `Turing.MultiTapeNTM.two_pow_coreLengthBound_log_le`: under a logarithmic space bound, + polynomially many. ## References @@ -145,4 +148,25 @@ theorem length_le_of_nodup_reachable (hs : ntm.RunsInSpace input s) (Cslib.BitString.length_padWord (length_coreCode_le hs (hreach finite hf))) simpa using hcodes.length_le_of_subset hsub +omit [Finite State] in +/-- **Logarithmic space has polynomially many views**: under the space bound `c * (log₂ n + 1)`, +the bound `2 ^ (2 * coreLengthBound k State n s + 1)` of +`Turing.MultiTapeNTM.length_le_of_nodup_reachable` is at most `2 * (2 * (n + 1)) ^ d`, with an +exponent `d` depending only on `k`, `State` and `c`. -/ +theorem two_pow_coreLengthBound_log_le (k : ℕ) (State : Type) (c n : ℕ) : + 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) ≤ + 2 * (2 * (n + 1)) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := by + set K := 8 + 2 * Nat.card (Option State) + 200 * k + have hcore : + coreLengthBound k State n (c * (Nat.log2 n + 1)) = K * (c + 1) * (Nat.log2 n + 1) := by + simp only [coreLengthBound, K] + ring + calc 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) + = 2 * (2 ^ (Nat.log2 n + 1)) ^ (2 * K * (c + 1)) := by + rw [hcore, ← pow_mul, pow_succ] + ring_nf + _ ≤ 2 * (2 * (n + 1)) ^ (2 * K * (c + 1)) := by + gcongr + exact Nat.two_pow_log2_succ_le n + end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean index 119aebd755..f7efea936a 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/HaltingTime.lean @@ -196,29 +196,6 @@ theorem runsInTime_of_runsInSpace {s t : ℕ} (hs : ntm.RunsInSpace input s) have hstate := (hrep i (by omega)).state exact hrun ⟨i, by omega⟩ (hstate.symm.trans (hqrep.state.trans hhalt)) -/-- The polynomial clock of `exists_runsInTime_polynomial_of_runsInSpace_log`, with its exponent -spelled out. -/ -private theorem runsInTime_polynomial_of_runsInSpace_log {c t : ℕ} - (hs : ntm.RunsInSpace input (c * (Nat.log2 input.length + 1))) - (ht : ntm.RunsInTime input t) : - ntm.RunsInTime input (2 * (2 * (input.length + 1)) ^ - (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1))) := by - refine (runsInTime_of_runsInSpace hs ht).mono ?_ - set K := 8 + 2 * Nat.card (Option State) + 200 * k - set L := Nat.log2 input.length - have hlog : 2 ^ L ≤ input.length + 1 := by - rcases Nat.eq_zero_or_pos input.length with h | h - · simp [L, h] - · rw [show L = Nat.log 2 input.length from Nat.log2_eq_log_two] - exact (Nat.pow_log_le_self 2 h.ne').trans (Nat.le_succ _) - have hcore : coreLengthBound k State input.length (c * (L + 1)) = K * (c + 1) * (L + 1) := by - simp only [coreLengthBound, K, L] - ring - have hbase : 2 ^ (L + 1) ≤ 2 * (input.length + 1) := by rw [pow_succ]; omega - calc 2 ^ (2 * coreLengthBound k State input.length (c * (L + 1)) + 1) - = 2 * (2 ^ (L + 1)) ^ (2 * K * (c + 1)) := by rw [hcore, ← pow_mul, pow_succ]; ring_nf - _ ≤ 2 * (2 * (input.length + 1)) ^ (2 * K * (c + 1)) := by gcongr - /-- **Logarithmic space gives a polynomial clock.** For every space constant `c` there is an exponent `d` such that on every input of length `n`, if every computation path stays within space `c * (log₂ n + 1)` and every computation path halts within some time, then every computation path @@ -227,6 +204,7 @@ theorem exists_runsInTime_polynomial_of_runsInSpace_log (ntm : MultiTapeNTM k Bo (c : ℕ) : ∃ d, ∀ {input : List Bool} {t : ℕ}, ntm.RunsInSpace input (c * (Nat.log2 input.length + 1)) → ntm.RunsInTime input t → ntm.RunsInTime input (2 * (2 * (input.length + 1)) ^ d) := - ⟨_, fun hs ht => runsInTime_polynomial_of_runsInSpace_log hs ht⟩ + ⟨_, fun hs ht => + (runsInTime_of_runsInSpace hs ht).mono (two_pow_coreLengthBound_log_le k State c _)⟩ end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 94e33e71ef..c0b46a6744 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -216,20 +216,8 @@ polynomial in the input length. -/ private theorem rounds_le (k : ℕ) (State : Type) (c n : ℕ) : 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) ≤ 2 * 2 ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) * - (n + 1) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := by - set M := 8 + 2 * Nat.card (Option State) + 200 * k - set D := 2 * M * (c + 1) - have hexp : 2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1 ≤ - (Nat.log2 n + 1) * D + 1 := by - simp only [coreLengthBound, D] - rw [← show M = 8 + 2 * Nat.card (Option State) + 200 * k from rfl] - nlinarith - calc 2 ^ (2 * coreLengthBound k State n (c * (Nat.log2 n + 1)) + 1) - ≤ 2 ^ ((Nat.log2 n + 1) * D + 1) := Nat.pow_le_pow_right (by norm_num) hexp - _ = 2 * (2 ^ (Nat.log2 n + 1)) ^ D := by rw [pow_succ, pow_mul, mul_comm] - _ ≤ 2 * (2 * (n + 1)) ^ D := - Nat.mul_le_mul_left 2 (Nat.pow_le_pow_left (Nat.two_pow_log2_succ_le n) D) - _ = 2 * 2 ^ D * (n + 1) ^ D := by rw [mul_pow, mul_assoc] + (n + 1) ^ (2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)) := + (two_pow_coreLengthBound_log_le k State c n).trans_eq (by rw [mul_pow, ← mul_assoc]) open scoped Classical in /-- **Acceptance within logarithmic space is decided by breadth-first search in polynomial time.** diff --git a/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean b/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean new file mode 100644 index 0000000000..86b891820f --- /dev/null +++ b/Complexity/Foundations/LinearAlgebra/Matrix/CoinStep.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.Matrix.Mul +public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse +public import Mathlib.Data.Fintype.Pi +import Mathlib.Algebra.Ring.GeomSum +import Mathlib.Data.Fin.Tuple.Basic + +/-! +# Transition matrices of coin-driven maps + +A map `next : α → Bool → α` moves a state to one of two successors, selected by a coin. On a finite +set `s` of states closed under `next`, its *count matrix* `Matrix.coinStepMatrix next s` has as +entry `(x, y)` the number of coins that move `x` to `y`. Its powers count coin strings +(`Matrix.coinStepMatrix_pow_mulVec`): `(N ^ t *ᵥ f) x` is the sum of `f` over the endpoints of +the `2 ^ t` coin strings of length `t` replayed from `x`. Halving the entries gives the stochastic +matrix of the fair-coin random walk. + +Keeping only the rows of the *live* states gives `Matrix.liveCoinStepMatrix live next s`, which +counts coin strings along which every state before the last is live +(`Matrix.liveCoinStepMatrix_pow_mulVec`). When the other states are fixed by `next`, the walk +stops at the first state that is not live, and every coin string is counted by the time it stops +(`Matrix.coinStepMatrix_pow_mulVec_eq_sum`). When the live walks have bounded length, the live +matrix is nilpotent, and `1 - S` has the inverse `∑ i < n, S ^ i` +(`Matrix.inv_one_sub_eq_sum_pow`). + +## Main definitions + +* `Matrix.coinStepMatrix`: the count matrix of a coin-driven map on a finite set. +* `Matrix.liveCoinStepMatrix`: its rows at live states, zero rows elsewhere. + +## Main results + +* `Matrix.coinStepMatrix_pow_mulVec`: powers sum over coin strings. +* `Matrix.liveCoinStepMatrix_pow_mulVec`: powers of the live matrix sum over live coin strings. +* `Matrix.coinStepMatrix_pow_mulVec_eq_sum`: first-stop decomposition of the count matrix. +* `Matrix.liveCoinStepMatrix_pow_eq_zero`: bounded live walks make the live matrix nilpotent. +* `Matrix.inv_one_sub_eq_sum_pow`: the inverse of `1 - S` for nilpotent `S`. +-/ + +@[expose] public section + +namespace Matrix + +variable {α R : Type*} [DecidableEq α] + +section Semiring + +variable [CommSemiring R] (next : α → Bool → α) (s : Finset α) + +/-- **The count matrix of a coin-driven map** on a finite set `s`: the entry at `(x, y)` is the +number of coins `b` with `next x b = y`. -/ +def coinStepMatrix : Matrix s s R := + fun x y => ∑ b : Bool, if next x b = y then 1 else 0 + +variable (live : α → Prop) [DecidablePred live] + +/-- **The live count matrix**: the rows of `Matrix.coinStepMatrix` at states satisfying `live`, +and zero rows at the other states. -/ +def liveCoinStepMatrix : Matrix s s R := + fun x y => if live x then coinStepMatrix next s x y else 0 + +variable {next s live} + +/-- A row of the count matrix, applied to a vector, sums the two coin successors. -/ +theorem coinStepMatrix_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (g : s → R) (x : s) : + (coinStepMatrix next s *ᵥ g) x = ∑ b : Bool, g ⟨next x b, hs x x.2 b⟩ := by + simp only [mulVec, dotProduct, coinStepMatrix, Finset.sum_mul, ite_mul, one_mul, zero_mul] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun b _ => ?_ + rw [Finset.sum_eq_single ⟨next x b, hs x x.2 b⟩] + · simp + · intro y _ hy + simp only [show ¬ next x b = y from fun h => hy (Subtype.ext h.symm), ↓reduceIte] + · simp + +/-- A row of the live count matrix sums the two coin successors at a live state and vanishes +elsewhere. -/ +theorem liveCoinStepMatrix_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (g : s → R) (x : s) : + (liveCoinStepMatrix next s live *ᵥ g) x = + if live x then ∑ b : Bool, g ⟨next x b, hs x x.2 b⟩ else 0 := by + rw [← coinStepMatrix_mulVec hs] + simp only [mulVec, dotProduct, liveCoinStepMatrix] + split_ifs <;> simp + +/-- Sums over the coin strings of length `t + 1` split off the first coin. -/ +private theorem sum_fin_succ_bool {M : Type*} [AddCommMonoid M] (t : ℕ) + (g : (Fin (t + 1) → Bool) → M) : + ∑ w : Fin (t + 1) → Bool, g w = ∑ b : Bool, ∑ w : Fin t → Bool, g (Fin.cons b w) := by + rw [← Fintype.sum_prod_type', ← (Fin.consEquiv fun _ => Bool).sum_comp] + rfl + +/-- **Powers of the count matrix sum over coin strings**: `(N ^ t *ᵥ f) x` is the sum of `f` over +the states reached from `x` by the `2 ^ t` coin strings of length `t`. -/ +theorem coinStepMatrix_pow_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (f : α → R) (t : ℕ) + (x : s) : (coinStepMatrix next s ^ t *ᵥ fun y : s => f y) x = + ∑ w : Fin t → Bool, f ((List.ofFn w).foldl next x) := by + induction t generalizing f x with + | zero => simp + | succ t ih => + have hfun : (coinStepMatrix next s ^ t *ᵥ fun y : s => f y) = + fun y : s => ∑ w : Fin t → Bool, f ((List.ofFn w).foldl next y) := funext fun y => ih f y + rw [pow_succ', ← mulVec_mulVec, hfun, coinStepMatrix_mulVec hs, sum_fin_succ_bool] + simp [List.ofFn_succ] + +/-- **Powers of the live count matrix sum over live coin strings**: `(S ^ t *ᵥ f) x` is the sum +of `f` over the states reached from `x` by those coin strings of length `t` along which every +state before the last is live. -/ +theorem liveCoinStepMatrix_pow_mulVec (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) (f : α → R) (t : ℕ) + (x : s) : (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) x = + ∑ w : Fin t → Bool, if ∀ i : Fin t, live (((List.ofFn w).take i).foldl next x) then + f ((List.ofFn w).foldl next x) else 0 := by + classical + induction t generalizing f x with + | zero => simp + | succ t ih => + have hfun : (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) = + fun y : s => ∑ w : Fin t → Bool, if ∀ i : Fin t, + live (((List.ofFn w).take i).foldl next y) then f ((List.ofFn w).foldl next y) else 0 := + funext fun y => ih f y + rw [pow_succ', ← mulVec_mulVec, hfun, liveCoinStepMatrix_mulVec hs, sum_fin_succ_bool] + have hlive (b : Bool) (w : Fin t → Bool) : + (∀ i : Fin (t + 1), live (((List.ofFn (Fin.cons b w : Fin (t + 1) → Bool)).take i).foldl + next x)) ↔ live x ∧ ∀ i : Fin t, live (((List.ofFn w).take i).foldl next (next x b)) := by + rw [Fin.forall_fin_succ] + simp [List.ofFn_succ] + split_ifs with hx + · refine Finset.sum_congr rfl fun b _ => Finset.sum_congr rfl fun w _ => ?_ + simp only [hlive, hx, true_and] + simp [List.ofFn_succ] + · refine (Finset.sum_eq_zero fun b _ => Finset.sum_eq_zero fun w _ => ?_).symm + rw [ite_eq_right_iff, hlive] + exact fun h => absurd h.1 hx + +/-- **First-stop decomposition.** If the states that are not live are fixed by `next`, and `f` +vanishes at live states, then counting the coin strings of length `T` by `f` at their endpoint +is the same as counting, for each `t ≤ T`, the live coin strings of length `t` by `f`, each +weighted by the `2 ^ (T - t)` continuations after the walk has stopped. -/ +theorem coinStepMatrix_pow_mulVec_eq_sum (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) + (hfix : ∀ x, ¬ live x → ∀ b, next x b = x) {f : α → R} (hf : ∀ x, live x → f x = 0) + (T : ℕ) (x : s) : (coinStepMatrix next s ^ T *ᵥ fun y : s => f y) x = + ∑ t ∈ Finset.range (T + 1), + 2 ^ (T - t) * (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) x := by + induction T generalizing x with + | zero => simp + | succ T ih => + rw [pow_succ', ← mulVec_mulVec, coinStepMatrix_mulVec hs] + by_cases hx : live x + · rw [Finset.sum_range_succ', pow_zero, one_mulVec] + simp only [hf x hx, mul_zero, add_zero] + have hrow (t : ℕ) : (liveCoinStepMatrix next s live ^ (t + 1) *ᵥ fun y : s => f y) x = + ∑ b : Bool, (liveCoinStepMatrix next s live ^ t *ᵥ fun y : s => f y) + ⟨next x b, hs x x.2 b⟩ := by + rw [pow_succ', ← mulVec_mulVec, liveCoinStepMatrix_mulVec hs] + simp only [hx, ↓reduceIte] + simp only [hrow, Finset.mul_sum, Nat.add_sub_add_right] + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun b _ => ih ⟨next x b, hs x x.2 b⟩ + · have hnext (b : Bool) : (⟨next x b, hs x x.2 b⟩ : s) = x := Subtype.ext (hfix x hx b) + have hzero (t : ℕ) : + (liveCoinStepMatrix next s live ^ (t + 1) *ᵥ fun y : s => f y) x = 0 := by + rw [pow_succ', ← mulVec_mulVec, liveCoinStepMatrix_mulVec hs] + simp only [hx, ↓reduceIte] + simp only [hnext] + rw [Fintype.sum_bool, ih x, Finset.sum_range_succ', Finset.sum_range_succ'] + simp only [hzero, mul_zero, Finset.sum_const_zero, zero_add, pow_zero, one_mulVec, + Nat.sub_zero] + ring + +/-- **Bounded live walks make the live matrix nilpotent**: if along every coin string of length +`n` from a state of `s` some state before the last is not live, then `S ^ n = 0`. -/ +theorem liveCoinStepMatrix_pow_eq_zero (hs : ∀ x ∈ s, ∀ b, next x b ∈ s) {n : ℕ} + (h : ∀ x ∈ s, ∀ w : Fin n → Bool, ∃ i : Fin n, + ¬ live (((List.ofFn w).take i).foldl next x)) : + (liveCoinStepMatrix next s live : Matrix s s R) ^ n = 0 := by + ext x y + have hcol := liveCoinStepMatrix_pow_mulVec (R := R) (live := live) hs + (fun z => if z = y then 1 else 0) n x + have hvec : (fun z : s => if (z : α) = y then (1 : R) else 0) = Pi.single y 1 := by + funext z + simp only [Pi.single_apply, Subtype.ext_iff] + rw [hvec, mulVec_single_one, Finset.sum_eq_zero fun w _ => ?_] at hcol + · simpa using hcol + · obtain ⟨i, hi⟩ := h x x.2 w + exact ite_eq_right_iff.mpr fun hall => absurd (hall i) hi + +end Semiring + +/-- **Inverse of `1 - S` for nilpotent `S`**: if `S ^ n = 0`, then `1 - S` is invertible with +inverse the truncated geometric series `∑ i < n, S ^ i`. -/ +theorem inv_one_sub_eq_sum_pow {ι : Type*} [Fintype ι] [DecidableEq ι] [CommRing R] + {S : Matrix ι ι R} {n : ℕ} (h : S ^ n = 0) : + (1 - S)⁻¹ = ∑ i ∈ Finset.range n, S ^ i := + inv_eq_right_inv (by rw [mul_neg_geom_sum, h, sub_zero]) + +end Matrix diff --git a/ComplexityTests/CoinStepMatrix.lean b/ComplexityTests/CoinStepMatrix.lean new file mode 100644 index 0000000000..dda73a8f9b --- /dev/null +++ b/ComplexityTests/CoinStepMatrix.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.LinearAlgebra.Matrix.CoinStep + +/-! +# Tests for transition matrices of coin-driven maps +-/ + +namespace ComplexityTests.CoinStepMatrix + +open Matrix + +/-- From `0` the coin moves to `1` or `2`; the states `1` and `2` are fixed. -/ +private def next : Fin 3 → Bool → Fin 3 + | 0, b => if b then 1 else 2 + | x, _ => x + +private theorem next_mem (x : Fin 3) (_ : x ∈ (Finset.univ : Finset (Fin 3))) (b : Bool) : + next x b ∈ (Finset.univ : Finset (Fin 3)) := + Finset.mem_univ _ + +-- Half of the `8` coin strings of length three end in `1` from `0`: those starting with `true`. +example : (coinStepMatrix next Finset.univ ^ 3 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 4 := by + rw [coinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +/-- Only the state `0` is live, so the live matrix squares to zero. -/ +private theorem live_sq : (liveCoinStepMatrix next Finset.univ (· = 0) : Matrix _ _ ℚ) ^ 2 = 0 := + liveCoinStepMatrix_pow_eq_zero next_mem fun x _ w => by + refine ⟨1, ?_⟩ + fin_cases x <;> cases h : w 0 <;> simp [next, List.ofFn_succ, h] + +-- The walk from `0` stops after one step: one live coin string of length one ends in `1`, none +-- of length two, since the live condition fails at the second state. +example : (liveCoinStepMatrix next Finset.univ (· = 0) ^ 1 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 1 := by + rw [liveCoinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +example : (liveCoinStepMatrix next Finset.univ (· = 0) ^ 2 *ᵥ + fun y : (Finset.univ : Finset (Fin 3)) => if (y : Fin 3) = 1 then (1 : ℕ) else 0) + ⟨0, Finset.mem_univ _⟩ = 0 := by + rw [liveCoinStepMatrix_pow_mulVec next_mem (fun y => if y = 1 then 1 else 0)] + decide + +-- With `S ^ 2 = 0`, the inverse of `1 - S` is `1 + S`. +example : (1 - (liveCoinStepMatrix next Finset.univ (· = 0) : Matrix _ _ ℚ))⁻¹ = + 1 + liveCoinStepMatrix next Finset.univ (· = 0) := by + rw [inv_one_sub_eq_sum_pow live_sq, Finset.sum_range_succ, Finset.sum_range_one, pow_zero, + pow_one] + +end ComplexityTests.CoinStepMatrix diff --git a/ComplexityTests/RandomizedLogSpace.lean b/ComplexityTests/RandomizedLogSpace.lean index e5684761ad..c6b30b8a5e 100644 --- a/ComplexityTests/RandomizedLogSpace.lean +++ b/ComplexityTests/RandomizedLogSpace.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Christian Reitwiessner -/ import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix import Complexity.Computability.Complexity.Classes.LogSpace.USTCON /-! @@ -151,4 +152,51 @@ example (enc : ℕ ↪ List Bool) : ∃ (k : ℕ) (State : Type) (_ : Finite Sta end Amplification +section ConfigurationMatrix + +open Cslib Turing Matrix + +open scoped Classical in +-- On the reachable views of `coinFlip`, the configuration matrix counts the one accepting coin +-- string of length one, and its stochastic power gives probability `1/2` at every later clock. +example (input : List Bool) : ∃ (V : Finset (FiniteCfg 0 Bool Unit)) + (hinit : coinFlip.toNTM.initView input ∈ V), + (coinFlip.configMatrix ℕ V ^ 1 *ᵥ FiniteCfg.acceptVec ℕ V) ⟨_, hinit⟩ = 1 ∧ + (((2 : ℚ)⁻¹ • coinFlip.configMatrix ℚ V) ^ 5 *ᵥ FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ = + 1 / 2 := by + obtain ⟨V, hreach, hV, -⟩ := + coinFlip.exists_finset_reachable (MultiTapeNTM.runsInSpace_zero_tapes _ input 0) + have hinit : coinFlip.toNTM.initView input ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, ?_, ?_⟩ + · rw [← MultiTapePTM.acceptCoins_eq_configMatrix_pow_mulVec ℕ hV hinit, Nat.cast_id, + acceptCoins_coinFlip] + · have h5 := MultiTapePTM.acceptCoins_add coinFlip (runsInTime_coinFlip input) 4 + rw [← MultiTapePTM.acceptCoins_div_eq_configMatrix_pow_mulVec ℚ hV hinit, + show 5 = 1 + 4 from rfl, h5, acceptCoins_coinFlip] + norm_num + +open scoped Classical in +-- The same probability `1/2` as the entry of `(1 - S / 2)⁻¹ *ᵥ e`, and as the sum of the +-- substochastic powers up to the halting time `1`. +example (input : List Bool) : ∃ (V : Finset (FiniteCfg 0 Bool Unit)) + (hinit : coinFlip.toNTM.initView input ∈ V), + ((1 - (2 : ℚ)⁻¹ • coinFlip.liveConfigMatrix ℚ V)⁻¹ *ᵥ FiniteCfg.acceptVec ℚ V) + ⟨_, hinit⟩ = 1 / 2 ∧ + ∑ t ∈ Finset.range 2, (((2 : ℚ)⁻¹ • coinFlip.liveConfigMatrix ℚ V) ^ t *ᵥ + FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩ = 1 / 2 ∧ + coinFlip.liveConfigMatrix ℚ V ^ 2 = 0 := by + obtain ⟨V, hreach, hV, -⟩ := + coinFlip.exists_finset_reachable (MultiTapeNTM.runsInSpace_zero_tapes _ input 0) + have hinit : coinFlip.toNTM.initView input ∈ V := (hreach _).mpr .refl + refine ⟨V, hinit, ?_, ?_, ?_⟩ + · rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ (runsInTime_coinFlip input) hV + (fun finite hf => (hreach _).mp hf), acceptCoins_coinFlip] + norm_num + · rw [← MultiTapePTM.acceptCoins_div_eq_sum_liveConfigMatrix ℚ hV hinit 1, acceptCoins_coinFlip] + norm_num + · exact MultiTapePTM.liveConfigMatrix_pow_eq_zero ℚ (runsInTime_coinFlip input) hV + fun finite hf => (hreach _).mp hf + +end ConfigurationMatrix + end ComplexityTests.RandomizedLogSpace diff --git a/references.bib b/references.bib index ffd09ecfee..5e9ecd5ea3 100644 --- a/references.bib +++ b/references.bib @@ -729,6 +729,18 @@ @article{BorchertHemaspaandraRothe2000 url = {https://arxiv.org/abs/cs/9907041} } +@article{BorodinCookPippenger1983, + author = {Borodin, Allan and Cook, Stephen and Pippenger, Nicholas}, + title = {Parallel Computation for Well-Endowed Rings and Space-Bounded Probabilistic + Machines}, + journal = {Information and Control}, + volume = {58}, + number = {1--3}, + pages = {113--136}, + year = {1983}, + doi = {10.1016/S0019-9958(83)80060-6} +} + @book{BorweinErdelyi1995, author = {Borwein, Peter and Erd{\'e}lyi, Tam{\'a}s}, title = {Polynomials and Polynomial Inequalities}, @@ -2234,6 +2246,15 @@ @book{ Hopcroft2006 address = {USA} } +@techreport{Hoza2022, + author = {Hoza, William M.}, + title = {Recent Progress on Derandomizing Space-Bounded Computation}, + institution = {Electronic Colloquium on Computational Complexity}, + number = {TR22-121}, + year = {2022}, + url = {https://eccc.weizmann.ac.il/report/2022/121/} +} + @article{Huang2019, author = {Huang, Hao}, title = {Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture}, From 3fd12172dcb5d7826ad87f5516e6c3f3ad765bd4 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:43:22 +0000 Subject: [PATCH 2/4] fix(LogSpace): Hoza citation scope; export reachability and nilpotency for BPL MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Hoza Section 4.3 states BPSPACE(S) ⊆ DSPACE(S^2); the inverse picture is Section 3.2, and BPL ⊆ P is no longer attributed to it. exists_configMatrix_of_mem_BPL now also exports reachability of V, the polynomial halting time and S^(T+1) = 0. Co-Authored-By: Claude Opus 5.5 --- .../Randomized/ConfigurationMatrix.lean | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean index 7f786876f0..a81a7f8a1d 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationMatrix.lean @@ -39,10 +39,11 @@ The reachable views form such a set (`Turing.MultiTapePTM.exists_finset_reachabl under a logarithmic one. So a `BPL` language is decided by the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` for a polynomial-size matrix `S` (`Cslib.Complexity.exists_configMatrix_of_mem_BPL`). This is the Markov chain of a probabilistic -machine on its configurations [Gill][Gill1977], whose powers and inverse Borodin, Cook and -Pippenger compute in parallel to place probabilistic space `s` in `DSPACE(s²)` -[Borodin, Cook and Pippenger][BorodinCookPippenger1983]; for `BPL` this gives -`BPL ⊆ DSPACE(log² n)` and `BPL ⊆ P` [Hoza, Section 4.3][Hoza2022]. Those algorithms are not +machine on its configurations [Gill][Gill1977]. Borodin, Cook and Pippenger compute its powers +and inverse in parallel [Borodin, Cook and Pippenger][BorodinCookPippenger1983], which gives +`BPSPACE(S) ⊆ DSPACE(S²)` [Hoza, Section 4.3][Hoza2022]; the inverse of `1 - W` as the sum +`W⁰ + W¹ + …` of transition-matrix powers is the picture of [Hoza, Section 3.2][Hoza2022]. +Exact evaluation of the polynomial-size matrix also gives `BPL ⊆ P`. None of these algorithms is formalized here. The matrices are indexed by an arbitrary closed set of views rather than a set of @@ -342,15 +343,21 @@ variable {α : Type} {enc : α ↪ List Bool} {A : Set α} open scoped Classical in /-- **`BPL` through polynomial-size configuration matrices**: a `BPL` machine has, on every -encoded instance of length `n`, a closed set `V` of at most `2 * (2 * (n + 1)) ^ d` views, -containing the initial view, such that the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is -at least `2/3` on members and at most `1/3` on non-members, with `S` the live configuration -matrix on `V` and `e` the indicator of the accepting halted views. -/ +encoded instance of length `n`, a set `V` of at most `2 * (2 * (n + 1)) ^ d` views, all reachable +from the initial view and closed under coin steps, such that every branch halts within +`T = 2 * (2 * (n + 1)) ^ d` steps, the live configuration matrix `S` on `V` satisfies +`S ^ (T + 1) = 0`, and the entry at the initial view of `(1 - S / 2)⁻¹ *ᵥ e` is at least `2/3` on +members and at most `1/3` on non-members, with `e` the indicator of the accepting halted +views. -/ theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (M : MultiTapePTM k Bool State) (d : ℕ), ∀ a, ∃ (V : Finset (FiniteCfg k Bool State)) (hinit : M.toNTM.initView (enc a) ∈ V), V.card ≤ 2 * (2 * ((enc a).length + 1)) ^ d ∧ (∀ finite ∈ V, ∀ bit, M.viewCoinStep finite bit ∈ V) ∧ + (∀ finite ∈ V, + Relation.ReflTransGen M.toNTM.ViewStep (M.toNTM.initView (enc a)) finite) ∧ + M.toNTM.RunsInTime (enc a) (2 * (2 * ((enc a).length + 1)) ^ d) ∧ + M.liveConfigMatrix ℚ V ^ (2 * (2 * ((enc a).length + 1)) ^ d + 1) = 0 ∧ (a ∈ A → 2 / 3 ≤ ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ FiniteCfg.acceptVec ℚ V) ⟨_, hinit⟩) ∧ (a ∉ A → ((1 - (2 : ℚ)⁻¹ • M.liveConfigMatrix ℚ V)⁻¹ *ᵥ @@ -361,10 +368,14 @@ theorem exists_configMatrix_of_mem_BPL (h : A ∈ BPL enc) : obtain ⟨hs, t, ht, hmem, hnot⟩ := hM a obtain ⟨V, hreach, hV, hcard⟩ := M.exists_finset_reachable hs have hinit : M.toNTM.initView (enc a) ∈ V := (hreach _).mpr .refl - refine ⟨V, hinit, hcard.trans (MultiTapeNTM.two_pow_coreLengthBound_log_le k State c _), hV, - fun ha => ?_, fun ha => ?_⟩ - all_goals - rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV (fun finite hf => (hreach _).mp hf)] + have hpoly := MultiTapeNTM.two_pow_coreLengthBound_log_le k State c (enc a).length + have hreach' : ∀ finite ∈ V, + Relation.ReflTransGen M.toNTM.ViewStep (M.toNTM.initView (enc a)) finite := + fun finite hf => (hreach _).mp hf + have hT := (MultiTapeNTM.runsInTime_of_runsInSpace hs ht).mono hpoly + refine ⟨V, hinit, hcard.trans hpoly, hV, hreach', hT, + MultiTapePTM.liveConfigMatrix_pow_eq_zero ℚ hT hV hreach', fun ha => ?_, fun ha => ?_⟩ + all_goals rw [← MultiTapePTM.acceptCoins_div_eq_inv_mulVec ℚ ht hV hreach'] · have h : ((2 * 2 ^ t : ℕ) : ℚ) ≤ ((3 * M.acceptCoins (enc a) t : ℕ) : ℚ) := Nat.cast_le.mpr (hmem ha) push_cast at h From 975c93f6d2c3933396671ffc771dc9143d83719d Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 21:57:13 +0000 Subject: [PATCH 3/4] =?UTF-8?q?refactor(Machines):=20plain=20polynomial-ti?= =?UTF-8?q?me=20tape,=20configuration=20and=20NL=20=E2=8A=86=20P=20search?= =?UTF-8?q?=20rules=20(#862)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Plain ComputableInPolyTime rules for stack and bidirectional tapes, finite configurations (observations, fixed actions, initialization), list tail and emptiness, and the breadth-first search of Reachability (insertNew, expand, viewSucc), proved without the tidy calculus. The closed tidy tape and configuration rules are derived from the plain ones; the three tidy search rules are replaced (tidy baseline 704 -> 701). Co-Authored-By: Claude Opus 5.5 --- .../Complexity/LogSpace/Reachability.lean | 79 ++++---- .../Complexity/PolyTime/Configuration.lean | 173 +++++++++++++++--- .../MultiTape/Complexity/PolyTime/Tape.lean | 170 ++++++++++++++--- .../Turing/MultiTape/Complexity/Space.lean | 3 +- .../Internal/PolyTimeListPrimitives.lean | 16 ++ scripts/tidy_surface_baseline.json | 1 - 6 files changed, 342 insertions(+), 100 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 94e33e71ef..9ae13429e1 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -42,8 +42,8 @@ configuration graph, which has polynomially many vertices [Sipser, Section 8.4][ * `Turing.MultiTapeNTM.reflTransGen_viewSucc_iff`: the successor lists give the reachable views. * `Turing.MultiTapeNTM.searchAccepts_iff`: enough rounds decide acceptance. -* `Turing.MultiTapeNTM.computableTidilyInPolyTime_viewSucc`: the successors in polynomial time. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.expand`: a round in polynomial time. +* `Turing.MultiTapeNTM.computableInPolyTime_viewSucc`: the successors in polynomial time. +* `Turing.MultiTapeTM.ComputableInPolyTime.expand`: a round in polynomial time. * `Turing.MultiTapeNTM.exists_computableInPolyTime_searchAccepts`: under a logarithmic space bound, enough rounds of breadth-first search run in polynomial time. @@ -133,12 +133,12 @@ end Turing.MultiTapeNTM /-! ### Breadth-first search in polynomial time -/ -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime variable {α : Type} [DecidableEq α] {enc : α ↪ List Bool} /-- Appending an element unless it is already in the list is polynomial-time. -/ -theorem insertNew : ComputableTidilyInPolyTime +theorem insertNew : ComputableInPolyTime (fun p : List α × α => Cslib.Reachability.insertNew p.1 p.2) (encPair (encList enc) enc) (encList enc) := by have hmem (l : List α) (a : α) : decide (a ∈ l) = l.any fun b => decide (b = a) := by @@ -153,12 +153,12 @@ theorem insertNew : ComputableTidilyInPolyTime /-- **A round of breadth-first search is polynomial-time** when the successors are: the found elements and their successors are at most polynomially many and long. -/ -theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ enc (encList enc)) : - ComputableTidilyInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by - have hlist : ComputableTidilyInPolyTime (fun found : List α => found.flatMap succ) +theorem expand {succ : α → List α} (hsucc : ComputableInPolyTime succ enc (encList enc)) : + ComputableInPolyTime (Cslib.Reachability.expand succ) (encList enc) (encList enc) := by + have hlist : ComputableInPolyTime (fun found : List α => found.flatMap succ) (encList enc) (encList enc) := flatMapWithInput id' (hsucc.comp (snd _ _)) - have hstep : ComputableTidilyInPolyTime + have hstep : ComputableInPolyTime (fun p : (List α × List α) × α => Cslib.Reachability.insertNew p.1.2 p.2) (encPair (encPair (encList enc) (encList enc)) enc) (encList enc) := insertNew.comp (((snd _ _).comp (fst _ _)).prod (snd _ _)) @@ -176,7 +176,7 @@ theorem expand {succ : α → List α} (hsucc : ComputableTidilyInPolyTime succ length_frame] omega -end Turing.MultiTapeTM.ComputableTidilyInPolyTime +end Turing.MultiTapeTM.ComputableInPolyTime namespace Turing.MultiTapeNTM @@ -185,8 +185,8 @@ open MultiTapeTM variable {k : ℕ} {State : Type} [Finite State] {ntm : MultiTapeNTM k Bool State} /-- **The successors of a view are polynomial-time.** -/ -theorem computableTidilyInPolyTime_viewSucc : - ComputableTidilyInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by +theorem computableInPolyTime_viewSucc : + ComputableInPolyTime ntm.viewSucc encFiniteCfg (encList encFiniteCfg) := by classical let key (finite : FiniteCfg k Bool State) : Option State × Option Bool × (Fin k → Option Bool) := (finite.state, finite.inputSymbol, finite.workTapeSymbols) @@ -200,16 +200,16 @@ theorem computableTidilyInPolyTime_viewSucc : funext finite rfl rw [heq] - refine ComputableTidilyInPolyTime.finite_cases + refine ComputableInPolyTime.finite_cases (tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_ - · exact ComputableTidilyInPolyTime.finiteCfg_state.prod - (ComputableTidilyInPolyTime.finiteCfg_inputSymbol.prod - ComputableTidilyInPolyTime.finiteCfg_workTapeSymbols) + · exact ComputableInPolyTime.finiteCfg_state.prod + (ComputableInPolyTime.finiteCfg_inputSymbol.prod + ComputableInPolyTime.finiteCfg_workTapeSymbols) · rcases tag with ⟨_ | state, symbol, work⟩ - · exact ComputableTidilyInPolyTime.const [] - · exact ComputableTidilyInPolyTime.mapConst _ fun action _ => - ComputableInPolyTime.finiteCfg_summarizeOutput.tidy.comp - (ComputableTidilyInPolyTime.finiteCfg_step action) + · exact ComputableInPolyTime.const [] + · exact ComputableInPolyTime.mapConst _ fun action _ => + ComputableInPolyTime.finiteCfg_summarizeOutput.comp + (ComputableInPolyTime.finiteCfg_step action) /-- Under a logarithmic space bound, the number of rounds that decides acceptance is at most a polynomial in the input length. -/ @@ -244,20 +244,19 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List ComputableInPolyTime (fun a => ntm.searchAccepts (rounds a) (enc a)) enc encBool := by set D := 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1) set rounds : α → ℕ := fun a => 2 * 2 ^ D * ((enc a).length + 1) ^ D - refine ⟨rounds, fun a => rounds_le k State c _, - ComputableTidilyInPolyTime.computableInPolyTime ?_⟩ + refine ⟨rounds, fun a => rounds_le k State c _, ?_⟩ -- the number of rounds in unary - have hcount : ComputableTidilyInPolyTime rounds enc encUnary := - ComputableTidilyInPolyTime.unary_mul.comp ((ComputableTidilyInPolyTime.const _).prod - ((ComputableTidilyInPolyTime.unary_pow D).comp (ComputableTidilyInPolyTime.unary_add.comp - ((ComputableTidilyInPolyTime.encoding_length enc).prod - (ComputableTidilyInPolyTime.const 1))))) - have hinit : ComputableTidilyInPolyTime (fun a => [ntm.initView (enc a)]) enc + have hcount : ComputableInPolyTime rounds enc encUnary := + ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const _).prod + ((ComputableInPolyTime.unary_pow D).comp (ComputableInPolyTime.unary_add.comp + ((ComputableInPolyTime.encoding_length enc).prod + (ComputableInPolyTime.const 1))))) + have hinit : ComputableInPolyTime (fun a => [ntm.initView (enc a)]) enc (encList encFiniteCfg) := - ComputableTidilyInPolyTime.cons' (ComputableTidilyInPolyTime.finiteCfg_init - (ComputableTidilyInPolyTime.of_eq (encIn := enc) (encMid := encBits) (f := fun a => enc a) + ComputableInPolyTime.cons' (ComputableInPolyTime.finiteCfg_init + (ComputableInPolyTime.of_eq (encIn := enc) (encOut := encBits) (f := fun a => enc a) fun _ => rfl) ntm.q₀) - (ComputableTidilyInPolyTime.const []) + (ComputableInPolyTime.const []) -- the found views are polynomially many, each of linear length set bound : α → ℕ := fun a => rounds a * (2 * viewLengthBound k State (enc a).length (c * (Nat.log2 (enc a).length + 1)) + 1) @@ -282,17 +281,17 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List refine (length_encList_le encFiniteCfg _ fun finite hf => length_encFiniteCfg_le (hs a) (hreach finite hf)).trans ?_ exact Nat.mul_le_mul_right _ hlen - have hsearch := ComputableTidilyInPolyTime.iterate hcount hinit - (ComputableTidilyInPolyTime.expand computableTidilyInPolyTime_viewSucc) hbound hstates - have htest : ComputableTidilyInPolyTime + have hsearch := ComputableInPolyTime.iterate hcount hinit + (ComputableInPolyTime.expand computableInPolyTime_viewSucc) hbound hstates + have htest : ComputableInPolyTime (fun finite : FiniteCfg k Bool State => decide (finite.state = none) && decide (finite.output = [true])) encFiniteCfg encBool := - ComputableTidilyInPolyTime.bool_and.comp - (((ComputableTidilyInPolyTime.of_finite fun state : Option State => - decide (state = none)).comp ComputableTidilyInPolyTime.finiteCfg_state).prod - (ComputableTidilyInPolyTime.decide_eq' ComputableTidilyInPolyTime.finiteCfg_output - (ComputableTidilyInPolyTime.const [true]))) - exact ComputableTidilyInPolyTime.anyWithInput hsearch - (htest.comp (ComputableTidilyInPolyTime.snd _ _)) + ComputableInPolyTime.bool_and.comp + (((ComputableInPolyTime.of_finite fun state : Option State => + decide (state = none)).comp ComputableInPolyTime.finiteCfg_state).prod + (ComputableInPolyTime.decide_eq' ComputableInPolyTime.finiteCfg_output + (ComputableInPolyTime.const [true]))) + exact ComputableInPolyTime.anyWithInput hsearch + (htest.comp (ComputableInPolyTime.snd _ _)) end Turing.MultiTapeNTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean index 78a99271bf..74fd9275ff 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean @@ -12,21 +12,26 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Tape import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time finite configuration operations -Ordinary structure construction, observations, fixed native actions and reply installation are -certified through the tidy functional calculus. Copying the input, work tapes, accumulated output -and every channel is charged by their encodings. These rules implement the interpreter; clients -of its eventual oracle-substitution theorem need no configuration bookkeeping. +Ordinary structure construction, observations, fixed native actions and initialization are +certified in plain polynomial time (`Turing.MultiTapeTM.ComputableInPolyTime`), by composition of +pair, list, table and tape rules. The tidy forms of the closed rules are derived from the plain +ones; channel operations for oracle configurations remain in the tidy calculus. Copying the +input, work tapes, accumulated output and every channel is charged by their encodings. ## Main results -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteCfg_step`: execute a fixed native action. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_state`, `.finiteCfg_inputSymbol`, + `.finiteCfg_workTapeSymbols`, `.finiteCfg_output`: plain observations. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_step`: execute a fixed native action. +* `Turing.MultiTapeTM.ComputableInPolyTime.finiteCfg_init`: initialize finite storage. * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_step`, `.finiteConfig_receive`: local transitions and channel reset with a computed reply. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_init`: initialize finite storage. +* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.finiteConfig_init`: initialize oracle storage. ## References @@ -36,7 +41,7 @@ Adapts Computability/Probabilistic/Configuration.lean on the cslib `crypto` bran @[expose] public section -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime open Cslib.Turing MultiTapeMachine @@ -46,17 +51,17 @@ variable {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} @[fun_prop] theorem finiteCfg_mk {word : α → List Bool} {state : α → Option State} {position : ∀ a, Fin ((word a).length + 2)} {work : α → Fin k → BiTape Bool} - {output : α → List Bool} (hword : ComputableTidilyInPolyTime word input encBits) - (hstate : ComputableTidilyInPolyTime state input (encFinite (Option State))) - (hposition : ComputableTidilyInPolyTime (fun a => (position a).val) input encUnary) - (hwork : ComputableTidilyInPolyTime work input (encPi (encBiTape encBool))) - (houtput : ComputableTidilyInPolyTime output input encBits) : - ComputableTidilyInPolyTime (fun a => + {output : α → List Bool} (hword : ComputableInPolyTime word input encBits) + (hstate : ComputableInPolyTime state input (encFinite (Option State))) + (hposition : ComputableInPolyTime (fun a => (position a).val) input encUnary) + (hwork : ComputableInPolyTime work input (encPi (encBiTape encBool))) + (houtput : ComputableInPolyTime output input encBits) : + ComputableInPolyTime (fun a => (⟨word a, state a, position a, work a, output a⟩ : FiniteCfg k Bool State)) input encFiniteCfg := (hword.prod (hstate.prod (hposition.prod (hwork.prod houtput)))).of_enc_eq (fun _ => rfl) -private theorem finiteCfg_parts : ComputableTidilyInPolyTime +private theorem finiteCfg_parts : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => (cfg.input, cfg.state, cfg.inputPos.val, cfg.workTapes, cfg.output)) encFiniteCfg (encPair encBits (encPair (encFinite (Option State)) @@ -64,39 +69,39 @@ private theorem finiteCfg_parts : ComputableTidilyInPolyTime /-- Read the stored input word. -/ @[fun_prop] -theorem finiteCfg_input : ComputableTidilyInPolyTime (FiniteCfg.input (k := k) (State := State)) +theorem finiteCfg_input : ComputableInPolyTime (FiniteCfg.input (k := k) (State := State)) encFiniteCfg encBits := finiteCfg_parts.fst' /-- Read the finite control. -/ @[fun_prop] -theorem finiteCfg_state : ComputableTidilyInPolyTime (FiniteCfg.state (k := k) (State := State)) +theorem finiteCfg_state : ComputableInPolyTime (FiniteCfg.state (k := k) (State := State)) encFiniteCfg (encFinite (Option State)) := finiteCfg_parts.snd'.fst' /-- Read the input head's unary position. -/ @[fun_prop] -theorem finiteCfg_inputPos : ComputableTidilyInPolyTime +theorem finiteCfg_inputPos : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => cfg.inputPos.val) encFiniteCfg encUnary := finiteCfg_parts.snd'.snd'.fst' /-- Read the complete family of work tapes. -/ @[fun_prop] -theorem finiteCfg_workTapes : ComputableTidilyInPolyTime +theorem finiteCfg_workTapes : ComputableInPolyTime (FiniteCfg.workTapes (k := k) (State := State)) encFiniteCfg (encPi (encBiTape encBool)) := finiteCfg_parts.snd'.snd'.snd'.fst' /-- Read all accumulated output. -/ @[fun_prop] -theorem finiteCfg_output : ComputableTidilyInPolyTime (FiniteCfg.output (k := k) (State := State)) +theorem finiteCfg_output : ComputableInPolyTime (FiniteCfg.output (k := k) (State := State)) encFiniteCfg encBits := finiteCfg_parts.snd'.snd'.snd'.snd' /-- Observe the read-only input, including both blank boundary cells. -/ @[fun_prop] -theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime +theorem finiteCfg_inputSymbol : ComputableInPolyTime (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinEnum (Option Bool)) := by - have hlist : ComputableTidilyInPolyTime + have hlist : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => none :: cfg.input.map some) encFiniteCfg (encList (encFinEnum (Option Bool))) := by - have hsome : ComputableTidilyInPolyTime (some (α := Bool)) + have hsome : ComputableInPolyTime (some (α := Bool)) encBool (encFinEnum (Option Bool)) := of_finite _ exact (const none).cons' ((map hsome).comp (bitsToList.comp finiteCfg_input)) simpa only [Function.comp_def, List.getD_eq_getElem?_getD, @@ -105,14 +110,127 @@ theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime /-- Observe all work heads as a single fixed finite value. -/ @[fun_prop] -theorem finiteCfg_workTapeSymbols : ComputableTidilyInPolyTime +theorem finiteCfg_workTapeSymbols : ComputableInPolyTime (FiniteCfg.workTapeSymbols (k := k) (State := State)) encFiniteCfg (encFinEnum (Fin k → Option Bool)) := by - have hheads : ComputableTidilyInPolyTime + have hheads : ComputableInPolyTime (fun cfg : FiniteCfg k Bool State => fun tape => (cfg.workTapes tape).head) - encFiniteCfg (encPi (encOption encBool)) := by fun_prop + encFiniteCfg (encPi (encOption encBool)) := + pi fun tape => (biTape_head encBool).comp ((pi_apply _ tape).comp finiteCfg_workTapes) exact (of_finite id).comp hheads +/-- Clamped native input-head movement is efficient on the stored unary position. -/ +@[fun_prop] +theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a).length + 2)} + (hword : ComputableInPolyTime word input encBits) + (hposition : ComputableInPolyTime (fun a => (position a).val) input encUnary) + (move : SignType) : ComputableInPolyTime + (fun a => (Turing.moveInputPos (position a) move).val) input encUnary := by + cases move with + | neg => + apply (unary_sub.comp (hposition.prod (const 1))).of_enc_eq + intro a + apply congrArg encUnary + have h := val_moveInputPos_eq (position a) .neg + have hp := (position a).isLt + simp only [SignType.cast, Function.comp_def] at h ⊢ + lia + | zero => simpa using hposition + | pos => + -- `min x y = x - (x - y)` + have hnext := unary_add.comp (hposition.prod (const 1)) + have hlast := unary_add.comp ((length_bits.comp hword).prod (const 1)) + apply (unary_sub.comp (hnext.prod (unary_sub.comp (hnext.prod hlast)))).of_enc_eq + intro a + apply congrArg encUnary + have h := val_moveInputPos_eq (position a) .pos + simp only [SignType.cast, Function.comp_def] at h ⊢ + lia + +/-- Execute a fixed ordinary native action, including all retained storage. -/ +@[fun_prop] +theorem finiteCfg_step (action : Action k Bool State) : ComputableInPolyTime + (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := by + refine finiteCfg_mk finiteCfg_input (const _) + (moveInputPos finiteCfg_input finiteCfg_inputPos action.inputTape) + (pi fun tape => biTape_step (action.workTapes tape) + ((pi_apply _ tape).comp finiteCfg_workTapes)) + (bitsAppend finiteCfg_output (const _)) + +/-- Initialize with the native input-head convention and blank work tapes. -/ +@[fun_prop] +theorem finiteCfg_init {word : α → List Bool} + (hword : ComputableInPolyTime word input encBits) (state : State) : + ComputableInPolyTime (fun a => FiniteCfg.init (k := k) state (word a)) + input encFiniteCfg := by + apply finiteCfg_mk hword (const _) + · simpa using (const (encIn := input) (encOut := encUnary) 1) + · exact const _ + · exact const _ + +end Turing.MultiTapeTM.ComputableInPolyTime + +namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime + +open Cslib.Turing MultiTapeMachine + +variable {k : ℕ} {State α : Type} [Finite State] {input : α ↪ List Bool} + +/-- Assemble an ordinary configuration from its certified components. -/ +@[fun_prop] +theorem finiteCfg_mk {word : α → List Bool} {state : α → Option State} + {position : ∀ a, Fin ((word a).length + 2)} {work : α → Fin k → BiTape Bool} + {output : α → List Bool} (hword : ComputableTidilyInPolyTime word input encBits) + (hstate : ComputableTidilyInPolyTime state input (encFinite (Option State))) + (hposition : ComputableTidilyInPolyTime (fun a => (position a).val) input encUnary) + (hwork : ComputableTidilyInPolyTime work input (encPi (encBiTape encBool))) + (houtput : ComputableTidilyInPolyTime output input encBits) : + ComputableTidilyInPolyTime (fun a => + (⟨word a, state a, position a, work a, output a⟩ : FiniteCfg k Bool State)) + input encFiniteCfg := + (hword.prod (hstate.prod (hposition.prod (hwork.prod houtput)))).of_enc_eq (fun _ => rfl) + +/-- Read the stored input word. -/ +@[fun_prop] +theorem finiteCfg_input : ComputableTidilyInPolyTime (FiniteCfg.input (k := k) (State := State)) + encFiniteCfg encBits := ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_input + +/-- Read the finite control. -/ +@[fun_prop] +theorem finiteCfg_state : ComputableTidilyInPolyTime (FiniteCfg.state (k := k) (State := State)) + encFiniteCfg (encFinite (Option State)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_state + +/-- Read the input head's unary position. -/ +@[fun_prop] +theorem finiteCfg_inputPos : ComputableTidilyInPolyTime + (fun cfg : FiniteCfg k Bool State => cfg.inputPos.val) encFiniteCfg encUnary := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_inputPos + +/-- Read the complete family of work tapes. -/ +@[fun_prop] +theorem finiteCfg_workTapes : ComputableTidilyInPolyTime + (FiniteCfg.workTapes (k := k) (State := State)) encFiniteCfg (encPi (encBiTape encBool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_workTapes + +/-- Read all accumulated output. -/ +@[fun_prop] +theorem finiteCfg_output : ComputableTidilyInPolyTime (FiniteCfg.output (k := k) (State := State)) + encFiniteCfg encBits := ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_output + +/-- Observe the read-only input, including both blank boundary cells. -/ +@[fun_prop] +theorem finiteCfg_inputSymbol : ComputableTidilyInPolyTime + (FiniteCfg.inputSymbol (k := k) (State := State)) encFiniteCfg (encFinEnum (Option Bool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_inputSymbol + +/-- Observe all work heads as a single fixed finite value. -/ +@[fun_prop] +theorem finiteCfg_workTapeSymbols : ComputableTidilyInPolyTime + (FiniteCfg.workTapeSymbols (k := k) (State := State)) encFiniteCfg + (encFinEnum (Fin k → Option Bool)) := + ComputableInPolyTime.tidy ComputableInPolyTime.finiteCfg_workTapeSymbols + /-- Clamped native input-head movement is efficient on the stored unary position. -/ @[fun_prop] theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a).length + 2)} @@ -142,9 +260,8 @@ theorem moveInputPos {word : α → List Bool} {position : ∀ a, Fin ((word a). /-- Execute a fixed ordinary native action, including all retained storage. -/ @[fun_prop] theorem finiteCfg_step (action : Action k Bool State) : ComputableTidilyInPolyTime - (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := by - unfold FiniteCfg.step - fun_prop + (fun cfg : FiniteCfg k Bool State => cfg.step action) encFiniteCfg encFiniteCfg := + ComputableInPolyTime.tidy (ComputableInPolyTime.finiteCfg_step action) /-- Initialize with the native input-head convention and blank work tapes. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean index 0cdd9a3eab..d45709c25f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Tape.lean @@ -9,20 +9,22 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain /-! # Polynomial-time operations on finite tape storage -The operations of cslib's existing tapes are certified by composition of list, option and pair -operations. They charge the complete stored tapes and accept any symbol encoding, including -infinite or empty alphabets. Finite-control interpreters can use these rules without building -new tape machines. +The operations of cslib's existing tapes are certified in plain polynomial time +(`Turing.MultiTapeTM.ComputableInPolyTime`) by composition of list, option and pair operations; +the tidy forms of the closed operations are derived from them. They charge the complete stored +tapes and accept any symbol encoding, including infinite or empty alphabets. Finite-control +interpreters can use these rules without building new tape machines. ## Main results -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.stackTape_cons`: prepend a computed cell, +* `Turing.MultiTapeTM.ComputableInPolyTime.stackTape_cons`: prepend a computed cell, retaining the stack's omission of trailing blanks. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.biTape_moveLeft`, `.biTape_moveRight`, +* `Turing.MultiTapeTM.ComputableInPolyTime.biTape_moveLeft`, `.biTape_moveRight`, `.biTape_write`, `.biTape_step`: native tape operations with `fun_prop` certificates. * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.biTape_mk₁`: load a computed list. @@ -35,7 +37,7 @@ instead of fixed finite tags. @[expose] public section -namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime +namespace Turing.MultiTapeTM.ComputableInPolyTime open Cslib.Turing @@ -44,24 +46,140 @@ variable {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bo /-- Reading the stored list is a change of view of the same encoded bits. -/ @[fun_prop] theorem stackTape_toList (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := + ComputableInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := of_eq fun _ => rfl /-- Reading a stack head decodes the first cell, with a blank default. -/ @[fun_prop] theorem stackTape_head (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.head (encStackTape enc) (encOption enc) := by + ComputableInPolyTime StackTape.head (encStackTape enc) (encOption enc) := by apply ((headD (encA := encOption enc) none).comp (stackTape_toList enc)).of_enc_eq intro tape cases tape with | mk values h => cases values <;> rfl -/-- Removing a stack head is the certified list-tail operation. -/ +/-- Removing a stack head is the list-tail operation. -/ @[fun_prop] theorem stackTape_tail (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := + ComputableInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := ((tail (encA := encOption enc)).comp (stackTape_toList enc)).of_enc_eq (fun tape => by simp only [Function.comp_def, encStackTape_apply, StackTape.tail_toList]) +/-- Prepend a cell without requiring a default symbol or case analysis over the alphabet. -/ +@[fun_prop] +theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape Symbol} + (hsymbol : ComputableInPolyTime symbol input (encOption enc)) + (htape : ComputableInPolyTime tape input (encStackTape enc)) : + ComputableInPolyTime (fun a => StackTape.cons (symbol a) (tape a)) input + (encStackTape enc) := by + have hcells := (stackTape_toList enc).comp htape + have hcond : ComputableInPolyTime (fun a => (symbol a).isSome || !(tape a).toList.isEmpty) + input encBool := + bool_or.comp ((optionIsSome hsymbol).prod + (bool_not.comp ((listIsEmpty (encA := encOption enc)).comp hcells))) + have hlist : ComputableInPolyTime + (fun a => if (symbol a).isSome || !(tape a).toList.isEmpty + then symbol a :: (tape a).toList else []) input (encList (encOption enc)) := + hcond.ite (cons' hsymbol hcells) (const []) + exact hlist.of_enc_eq (fun a => by rw [encStackTape_apply, StackTape.cons_toList]) + +/-- Map symbols to occupied cells with the list map. -/ +@[fun_prop] +theorem stackTape_mapSome (enc : Symbol ↪ List Bool) : + ComputableInPolyTime StackTape.mapSome (encList enc) (encStackTape enc) := + (map (optionSome enc)).of_enc_eq (fun _ => rfl) + +private theorem biTape_parts (enc : Symbol ↪ List Bool) : + ComputableInPolyTime (fun tape : BiTape Symbol => (tape.head, tape.left, tape.right)) + (encBiTape enc) (encPair (encOption enc) (encPair (encStackTape enc) (encStackTape enc))) := + of_eq fun _ => rfl + +/-- Assemble a tape from its computed head and two sides. -/ +@[fun_prop] +theorem biTape_mk {head : α → Option Symbol} {left right : α → StackTape Symbol} + (hhead : ComputableInPolyTime head input (encOption enc)) + (hleft : ComputableInPolyTime left input (encStackTape enc)) + (hright : ComputableInPolyTime right input (encStackTape enc)) : + ComputableInPolyTime (fun a => BiTape.mk (head a) (left a) (right a)) input + (encBiTape enc) := + (hhead.prod (hleft.prod hright)).of_enc_eq (fun _ => rfl) + +/-- Read the current cell of a computed tape. -/ +@[fun_prop] +theorem biTape_head (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.head (encBiTape enc) (encOption enc) := + (biTape_parts enc).fst' + +/-- Extract the stored left side. -/ +@[fun_prop] +theorem biTape_left (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.left (encBiTape enc) (encStackTape enc) := + (biTape_parts enc).snd'.fst' + +/-- Extract the stored right side. -/ +@[fun_prop] +theorem biTape_right (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.right (encBiTape enc) (encStackTape enc) := + (biTape_parts enc).snd'.snd' + +/-- Move left by the stack operations. -/ +@[fun_prop] +theorem biTape_moveLeft (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := by + unfold BiTape.moveLeft + fun_prop + +/-- Move right by the stack operations. -/ +@[fun_prop] +theorem biTape_moveRight (enc : Symbol ↪ List Bool) : + ComputableInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := by + unfold BiTape.moveRight + fun_prop + +/-- Write a computed optional symbol, including blank erasure. -/ +@[fun_prop] +theorem biTape_write {tape : α → BiTape Symbol} {symbol : α → Option Symbol} + (htape : ComputableInPolyTime tape input (encBiTape enc)) + (hsymbol : ComputableInPolyTime symbol input (encOption enc)) : + ComputableInPolyTime (fun a => (tape a).write (symbol a)) input (encBiTape enc) := by + unfold BiTape.write + fun_prop + +/-- Execute a fixed native action, charging the full encoded tape. -/ +@[fun_prop] +theorem biTape_step (action : Option (Option Symbol) × SignType) + {tape : α → BiTape Symbol} + (htape : ComputableInPolyTime tape input (encBiTape enc)) : + ComputableInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := by + rcases action with ⟨write, move⟩ + cases write <;> cases move <;> + simp only [BiTape.step, Option.elim_none, Option.elim_some] <;> fun_prop + +end Turing.MultiTapeTM.ComputableInPolyTime + +namespace Turing.MultiTapeTM.ComputableTidilyInPolyTime + +open Cslib.Turing + +variable {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} + +/-- Reading the stored list is a change of view of the same encoded bits. -/ +@[fun_prop] +theorem stackTape_toList (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.toList (encStackTape enc) (encList (encOption enc)) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_toList enc) + +/-- Reading a stack head decodes the first cell, with a blank default. -/ +@[fun_prop] +theorem stackTape_head (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.head (encStackTape enc) (encOption enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_head enc) + +/-- Removing a stack head is the certified list-tail operation. -/ +@[fun_prop] +theorem stackTape_tail (enc : Symbol ↪ List Bool) : + ComputableTidilyInPolyTime StackTape.tail (encStackTape enc) (encStackTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_tail enc) + /-- Prepend a cell without requiring a default symbol or case analysis over the alphabet. -/ @[fun_prop] theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape Symbol} @@ -78,12 +196,7 @@ theorem stackTape_cons {symbol : α → Option Symbol} {tape : α → StackTape @[fun_prop] theorem stackTape_mapSome (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime StackTape.mapSome (encList enc) (encStackTape enc) := - (map (optionSome enc)).of_enc_eq (fun _ => rfl) - -private theorem biTape_parts (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime (fun tape : BiTape Symbol => (tape.head, tape.left, tape.right)) - (encBiTape enc) (encPair (encOption enc) (encPair (encStackTape enc) (encStackTape enc))) := - of_eq fun _ => rfl + ComputableInPolyTime.tidy (ComputableInPolyTime.stackTape_mapSome enc) /-- Assemble a tape from its computed head and two sides. -/ @[fun_prop] @@ -99,33 +212,31 @@ theorem biTape_mk {head : α → Option Symbol} {left right : α → StackTape S @[fun_prop] theorem biTape_head (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.head (encBiTape enc) (encOption enc) := - (biTape_parts enc).fst' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_head enc) /-- Extract the stored left side. -/ @[fun_prop] theorem biTape_left (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.left (encBiTape enc) (encStackTape enc) := - (biTape_parts enc).snd'.fst' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_left enc) /-- Extract the stored right side. -/ @[fun_prop] theorem biTape_right (enc : Symbol ↪ List Bool) : ComputableTidilyInPolyTime BiTape.right (encBiTape enc) (encStackTape enc) := - (biTape_parts enc).snd'.snd' + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_right enc) /-- Move left by the existing stack operations. -/ @[fun_prop] theorem biTape_moveLeft (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := by - unfold BiTape.moveLeft - fun_prop + ComputableTidilyInPolyTime BiTape.moveLeft (encBiTape enc) (encBiTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_moveLeft enc) /-- Move right by the existing stack operations. -/ @[fun_prop] theorem biTape_moveRight (enc : Symbol ↪ List Bool) : - ComputableTidilyInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := by - unfold BiTape.moveRight - fun_prop + ComputableTidilyInPolyTime BiTape.moveRight (encBiTape enc) (encBiTape enc) := + ComputableInPolyTime.tidy (ComputableInPolyTime.biTape_moveRight enc) /-- Write a computed optional symbol, including blank erasure. -/ @[fun_prop] @@ -141,10 +252,9 @@ theorem biTape_write {tape : α → BiTape Symbol} {symbol : α → Option Symbo theorem biTape_step (action : Option (Option Symbol) × SignType) {tape : α → BiTape Symbol} (htape : ComputableTidilyInPolyTime tape input (encBiTape enc)) : - ComputableTidilyInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := by - rcases action with ⟨write, move⟩ - cases write <;> cases move <;> - simp only [BiTape.step, Option.elim_none, Option.elim_some] <;> fun_prop + ComputableTidilyInPolyTime (fun a => (tape a).step action) input (encBiTape enc) := + (ComputableInPolyTime.tidy + (ComputableInPolyTime.biTape_step (enc := enc) action ComputableInPolyTime.id')).comp htape /-- Loading a list constructs a head and two stacks with no default symbol. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean index e18b157ae8..acd8e191dc 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space.lean @@ -108,7 +108,8 @@ theorem outputClass : theorem finiteCfg_summarizeOutput {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime (FiniteCfg.summarizeOutput (k := k) (State := State)) encFiniteCfg encFiniteCfg := - ComputableTidilyInPolyTime.finiteCfg_summarizeOutput.computableInPolyTime + finiteCfg_mk finiteCfg_input finiteCfg_state finiteCfg_inputPos finiteCfg_workTapes + (outputClass.comp finiteCfg_output) end MultiTapeTM.ComputableInPolyTime diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean index 1d7ca6914a..9249e237a3 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListPrimitives.lean @@ -209,6 +209,22 @@ theorem bitsIsEmpty : ComputableInPolyTime List.isEmpty encBits encBool := by exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, k, Q, hfinite, tm, fun word => htm word⟩ +/-- Drop the head of a list in any list encoding, reusing the encoding's linear-time machine. -/ +@[fun_prop] +theorem tail {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} + [ListEncoding encA encL] : ComputableInPolyTime (List.tail (α := α)) encL encL := by + obtain ⟨c, k, Q, hfinite, tm, htm⟩ := ListEncoding.tail (enc₁ := encA) (enc := encL) + exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, + k, Q, hfinite, tm, fun word => htm word⟩ + +/-- Test a list in any list encoding for emptiness, reusing the encoding's linear-time machine. -/ +@[fun_prop] +theorem listIsEmpty {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} + [ListEncoding encA encL] : ComputableInPolyTime (List.isEmpty (α := α)) encL encBool := by + obtain ⟨c, k, Q, hfinite, tm, htm⟩ := ListEncoding.isEmpty (enc₁ := encA) (enc := encL) + exact ⟨fun n => c * (n + 1), fun n => c * (n + 1), by fun_prop, by fun_prop, + k, Q, hfinite, tm, fun word => htm word⟩ + private theorem rangeStepCertificate : ComputableInPolyTime (fun p : RangeState × Bool => rangeStep p.1 p.2) (encPair rangeEncoding encBool) rangeEncoding := by diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 06f1c636d8..7a800c4596 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -21,7 +21,6 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Compiler.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 9, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, From 0843d45eeaf9665262adc20b6f5fb68195c0fdfb Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:08:44 +0000 Subject: [PATCH 4/4] =?UTF-8?q?feat(LogSpace):=20BPL=20=E2=8A=86=20P=20by?= =?UTF-8?q?=20exact=20evaluation=20of=20the=20configuration=20matrix=20(#4?= =?UTF-8?q?74)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Breadth-first search lists the reachable views; rounds of the count recursion on a table of binary counts evaluate the accepting coin strings at the polynomial clock exactly. Plain polynomial-time certificates only. Also exposes MultiTapeNTM.exists_computableInPolyTime_search and MultiTapeNTM.mem_search_iff. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Classes/LogSpace/Randomized/PolyTime.lean | 365 ++++++++++++++++++ .../Complexity/LogSpace/Reachability.lean | 53 ++- ComplexityTests/RandomizedLogSpace.lean | 24 ++ 4 files changed, 431 insertions(+), 12 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/LogSpace/Randomized/PolyTime.lean diff --git a/Complexity.lean b/Complexity.lean index dccd119200..2ca7488d41 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1004,6 +1004,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.PolyTime public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON public import Complexity.Computability.Complexity.Classes.MIP public import Complexity.Computability.Complexity.Classes.MIP.Defs diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/PolyTime.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/PolyTime.lean new file mode 100644 index 0000000000..368e4f14a5 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/PolyTime.lean @@ -0,0 +1,365 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix +public import Complexity.Computability.Complexity.Classes.P +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Reachability +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Configuration +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Space +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength + +/-! +# Randomized logarithmic space is within polynomial time + +The number of accepting coin strings of length `t` from a view satisfies a recursion over the +two coin successors (`Turing.MultiTapePTM.viewAcceptCount`), and it is the entry of the power of +the configuration matrix (`Turing.MultiTapePTM.configMatrix_pow_mulVec_acceptVec`). A +deterministic algorithm evaluates it exactly: breadth-first search lists the reachable views +(`Turing.MultiTapeNTM.exists_computableInPolyTime_search`), and `t` rounds update a table of +binary counts, one per view, by adding the counts of the two coin successors. Under a logarithmic +space bound there are polynomially many views, the polynomial clock bounds the number of rounds, +and every count of round `t` has at most `t + 1` bits, so the evaluation runs in polynomial time. +Comparing the count with `2 / 3` of the `2 ^ t` coin strings decides a `BPL` language, so +`BPL ⊆ P` (`Cslib.Complexity.BPL_subset_P`), and with `Cslib.Complexity.RL_subset_BPL` also +`RL ⊆ P`. This is a sequential exact evaluation of the configuration matrix, whose powers Borodin, +Cook and Pippenger evaluate in parallel [Borodin, Cook and Pippenger][BorodinCookPippenger1983]. + +The certificates use only the plain polynomial-time calculus. + +## Main definitions + +* `Turing.MultiTapePTM.viewAcceptCount`: the accepting coin strings of a given length from a view. + +## Main results + +* `Turing.MultiTapePTM.computableInPolyTime_viewCoinStep`: coin steps of views are + polynomial-time. +* `Turing.MultiTapePTM.configMatrix_pow_mulVec_acceptVec`: the count is an entry of the power of + the configuration matrix. +* `Turing.MultiTapePTM.acceptCoins_eq_viewAcceptCount`: the count from the initial view is the + number of accepting coin strings. +* `Cslib.Complexity.BPL_subset_P`, `Cslib.Complexity.RL_subset_P`: randomized logarithmic space is + within polynomial time. + +## References + +* [A. Borodin, S. Cook, N. Pippenger, *Parallel computation for well-endowed rings and + space-bounded probabilistic machines*][BorodinCookPippenger1983] +-/ + +@[expose] public section + +open Cslib.Turing + +namespace Turing.MultiTapePTM + +open MultiTapeTM Matrix + +variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) + +open scoped Classical in +/-- **The accepting coin strings from a view**: the number of coin strings of length `t` whose +replay from the view ends in a halted view with output `[true]`, by recursion over the two coin +successors. -/ +noncomputable def viewAcceptCount : ℕ → FiniteCfg k Bool State → ℕ + | 0, finite => if decide (finite.state = none) && decide (finite.output = [true]) then 1 else 0 + | t + 1, finite => viewAcceptCount t (machine.viewCoinStep finite false) + + viewAcceptCount t (machine.viewCoinStep finite true) + +variable {machine} + +/-- At most all coin strings are accepted. -/ +theorem viewAcceptCount_le (t : ℕ) (finite : FiniteCfg k Bool State) : + machine.viewAcceptCount t finite ≤ 2 ^ t := by + induction t generalizing finite with + | zero => + simp only [viewAcceptCount, pow_zero] + split_ifs <;> omega + | succ t ih => + simp only [viewAcceptCount, pow_succ] + have h₁ := ih (machine.viewCoinStep finite false) + have h₂ := ih (machine.viewCoinStep finite true) + omega + +open scoped Classical in +/-- **The count is an entry of the power of the configuration matrix** on any set of views +closed under coin steps. -/ +theorem configMatrix_pow_mulVec_acceptVec {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) (t : ℕ) (x : V) : + (machine.configMatrix ℕ V ^ t *ᵥ FiniteCfg.acceptVec ℕ V) x = + machine.viewAcceptCount t x := by + induction t generalizing x with + | zero => + simp only [pow_zero, one_mulVec, FiniteCfg.acceptVec, viewAcceptCount, Bool.and_eq_true, + decide_eq_true_eq] + | succ t ih => + rw [pow_succ', ← mulVec_mulVec, configMatrix, coinStepMatrix_mulVec hV, Fintype.sum_bool, + ← configMatrix, ih, ih, viewAcceptCount, add_comm] + +open scoped Classical in +/-- **The count from the initial view is the number of accepting coin strings.** -/ +theorem acceptCoins_eq_viewAcceptCount {input : List Bool} {V : Finset (FiniteCfg k Bool State)} + (hV : ∀ finite ∈ V, ∀ bit, machine.viewCoinStep finite bit ∈ V) + (hinit : machine.toNTM.initView input ∈ V) (t : ℕ) : + machine.acceptCoins input t = machine.viewAcceptCount t (machine.toNTM.initView input) := by + have h := acceptCoins_eq_configMatrix_pow_mulVec ℕ hV hinit t + rw [Nat.cast_id] at h + rw [h, configMatrix_pow_mulVec_acceptVec hV] + +variable [Finite State] + +/-- **Coin steps of views are polynomial-time.** -/ +theorem computableInPolyTime_viewCoinStep (machine : MultiTapePTM k Bool State) (bit : Bool) : + ComputableInPolyTime (machine.viewCoinStep · bit) encFiniteCfg encFiniteCfg := by + classical + let key (finite : FiniteCfg k Bool State) : Option State × Option Bool × (Fin k → Option Bool) := + (finite.state, finite.inputSymbol, finite.workTapeSymbols) + let branch (tag : Option State × Option Bool × (Fin k → Option Bool)) + (finite : FiniteCfg k Bool State) : FiniteCfg k Bool State := + match tag.1 with + | none => finite + | some state => + (finite.step ((machine.withCoin bit).toTM.tr state tag.2.1 tag.2.2)).summarizeOutput + have heq : (machine.viewCoinStep · bit) = fun finite => branch (key finite) finite := by + funext finite + rfl + rw [heq] + refine ComputableInPolyTime.finite_cases + (tagEncoding := encPair (encFinite _) (encPair (encFinEnum _) (encFinEnum _))) ?_ fun tag => ?_ + · exact ComputableInPolyTime.finiteCfg_state.prod + (ComputableInPolyTime.finiteCfg_inputSymbol.prod + ComputableInPolyTime.finiteCfg_workTapeSymbols) + · rcases tag with ⟨_ | state, symbol, work⟩ + · exact ComputableInPolyTime.id' + · exact ComputableInPolyTime.finiteCfg_summarizeOutput.comp + (ComputableInPolyTime.finiteCfg_step _) + +end Turing.MultiTapePTM + +/-! ### Evaluation of the counts on a table of views -/ + +namespace Cslib.Complexity + +open _root_.Turing _root_.Turing.MultiTapeTM + +variable {k : ℕ} {State : Type} + +open scoped Classical in +/-- The count stored for a view in a table of views and counts, `0` when it is absent. -/ +private noncomputable def lookupCount (table : List (FiniteCfg k Bool State × ℕ)) + (finite : FiniteCfg k Bool State) : ℕ := + ((table.filter fun entry => decide (entry.1 = finite)).map Prod.snd).headD 0 + +/-- One round of evaluation: each view's count becomes the sum of its coin successors' counts. -/ +private noncomputable def countRound (M : MultiTapePTM k Bool State) + (table : List (FiniteCfg k Bool State × ℕ)) : List (FiniteCfg k Bool State × ℕ) := + table.map fun entry => (entry.1, lookupCount table (M.viewCoinStep entry.1 false) + + lookupCount table (M.viewCoinStep entry.1 true)) + +/-- A table listing every view with its value returns that value for every listed view. -/ +private theorem lookupCount_map {views : List (FiniteCfg k Bool State)} + {value : FiniteCfg k Bool State → ℕ} {finite : FiniteCfg k Bool State} + (h : finite ∈ views) : + lookupCount (views.map fun view => (view, value view)) finite = value finite := by + classical + unfold lookupCount + set filtered := (views.map fun view => (view, value view)).filter + fun entry => decide (entry.1 = finite) + have hmem : (finite, value finite) ∈ filtered := + List.mem_filter.mpr ⟨List.mem_map.mpr ⟨finite, h, rfl⟩, by simp⟩ + obtain ⟨entry, rest, hcons⟩ := List.exists_cons_of_ne_nil (List.ne_nil_of_mem hmem) + have hentry : entry ∈ filtered := hcons ▸ List.mem_cons_self + obtain ⟨hentry, hfirst⟩ := List.mem_filter.mp hentry + obtain ⟨view, -, rfl⟩ := List.mem_map.mp hentry + have hview : view = finite := by simpa using hfirst + rw [hcons] + simp [hview] + +/-- **Rounds of evaluation compute the counts** on a list of views closed under coin steps. -/ +private theorem countRound_iterate (M : MultiTapePTM k Bool State) + {views : List (FiniteCfg k Bool State)} + (hclosed : ∀ finite ∈ views, ∀ bit, M.viewCoinStep finite bit ∈ views) (t : ℕ) : + (countRound M)^[t] (views.map fun view => (view, M.viewAcceptCount 0 view)) = + views.map fun view => (view, M.viewAcceptCount t view) := by + induction t with + | zero => rfl + | succ t ih => + rw [Function.iterate_succ_apply', ih, countRound, List.map_map] + refine List.map_congr_left fun view hview => ?_ + simp only [Function.comp_apply, lookupCount_map (hclosed view hview false), + lookupCount_map (hclosed view hview true), MultiTapePTM.viewAcceptCount] + +open scoped Classical in +/-- The table lookup is polynomial-time. -/ +private theorem computableInPolyTime_lookupCount [Finite State] : + ComputableInPolyTime (fun p : List (FiniteCfg k Bool State × ℕ) × FiniteCfg k Bool State => + lookupCount p.1 p.2) (encPair (encList (encPair encFiniteCfg encNat)) encFiniteCfg) + encNat := by + unfold lookupCount + have hfilter := ComputableInPolyTime.filterWithInput + (encA := encPair encFiniteCfg encNat) + (encIn := encPair (encList (encPair encFiniteCfg encNat)) encFiniteCfg) + (test := fun (p : List (FiniteCfg k Bool State × ℕ) × FiniteCfg k Bool State) + (entry : FiniteCfg k Bool State × ℕ) => decide (entry.1 = p.2)) + (ComputableInPolyTime.fst _ _) + (ComputableInPolyTime.decide_eq' ((ComputableInPolyTime.fst _ _).comp + (ComputableInPolyTime.snd _ _)) ((ComputableInPolyTime.snd _ _).comp + (ComputableInPolyTime.fst _ _))) + exact (ComputableInPolyTime.headD (encA := encNat) 0).comp + ((ComputableInPolyTime.map (ComputableInPolyTime.snd encFiniteCfg encNat)).comp hfilter) + +/-- A round of evaluation is polynomial-time. -/ +private theorem computableInPolyTime_countRound [Finite State] (M : MultiTapePTM k Bool State) : + ComputableInPolyTime (countRound M) (encList (encPair encFiniteCfg encNat)) + (encList (encPair encFiniteCfg encNat)) := by + have hview : ComputableInPolyTime + (fun p : List (FiniteCfg k Bool State × ℕ) × (FiniteCfg k Bool State × ℕ) => p.2.1) + (encPair (encList (encPair encFiniteCfg encNat)) (encPair encFiniteCfg encNat)) + encFiniteCfg := (ComputableInPolyTime.fst _ _).comp (ComputableInPolyTime.snd _ _) + have hlookup (bit : Bool) : ComputableInPolyTime + (fun p : List (FiniteCfg k Bool State × ℕ) × (FiniteCfg k Bool State × ℕ) => + lookupCount p.1 (M.viewCoinStep p.2.1 bit)) + (encPair (encList (encPair encFiniteCfg encNat)) (encPair encFiniteCfg encNat)) encNat := + computableInPolyTime_lookupCount.comp + ((ComputableInPolyTime.fst _ _).prod + ((M.computableInPolyTime_viewCoinStep bit).comp hview)) + exact ComputableInPolyTime.mapWithInput ComputableInPolyTime.id' + (hview.prod (ComputableInPolyTime.binary_add.comp ((hlookup false).prod (hlookup true)))) + +variable {α : Type} {enc : α ↪ List Bool} {A : Set α} + +open scoped Classical in +/-- **Randomized logarithmic space with two-sided error is within polynomial time**: breadth-first +search lists the polynomially many reachable views, and rounds of the count recursion over a +table of binary counts evaluate the number of accepting coin strings at the polynomial clock +exactly. -/ +theorem BPL_subset_P : BPL enc ⊆ P enc := by + intro A h + obtain ⟨k, State, hfin, M, c, d, hM⟩ := exists_polyClock_of_mem_BPL h + set T : α → ℕ := fun a => 2 * (2 * ((enc a).length + 1)) ^ d + obtain ⟨rounds, hrounds, hsearch⟩ := + MultiTapeNTM.exists_computableInPolyTime_search (ntm := M.toNTM) fun a => (hM a).1 + set views : α → List (FiniteCfg k Bool State) := fun a => + Cslib.Reachability.search M.toNTM.viewSucc (rounds a) (M.toNTM.initView (enc a)) + have hmem (a : α) (finite : FiniteCfg k Bool State) : finite ∈ views a ↔ + Relation.ReflTransGen M.toNTM.ViewStep (M.toNTM.initView (enc a)) finite := + MultiTapeNTM.mem_search_iff (hM a).1 (hrounds a) + have hclosed (a : α) : ∀ finite ∈ views a, ∀ bit, M.viewCoinStep finite bit ∈ views a := + fun finite hf bit => (hmem a _).mpr (((hmem a _).mp hf).tail + (MultiTapePTM.viewStep_toNTM_iff.mpr ⟨bit, rfl⟩)) + have hinitMem (a : α) : M.toNTM.initView (enc a) ∈ views a := (hmem a _).mpr .refl + -- the computed count at the clock is the number of accepting coin strings + set table : α → List (FiniteCfg k Bool State × ℕ) := fun a => + (countRound M)^[T a] ((views a).map fun view => (view, M.viewAcceptCount 0 view)) + have hvalue (a : α) : lookupCount (table a) (M.toNTM.initView (enc a)) = + M.acceptCoins (enc a) (T a) := by + simp only [table] + rw [countRound_iterate M (hclosed a), lookupCount_map (hinitMem a), + MultiTapePTM.acceptCoins_eq_viewAcceptCount (V := (views a).toFinset) + (fun finite hf bit => List.mem_toFinset.mpr (hclosed a finite + (List.mem_toFinset.mp hf) bit)) (List.mem_toFinset.mpr (hinitMem a))] + refine ⟨fun a => decide (2 * 2 ^ T a ≤ 3 * lookupCount (table a) (M.toNTM.initView (enc a))), + ?_, fun a => ?_⟩ + · -- certificates + have hT : ComputableInPolyTime T enc encUnary := + ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const 2).prod + ((ComputableInPolyTime.unary_pow d).comp (ComputableInPolyTime.unary_mul.comp + ((ComputableInPolyTime.const 2).prod (ComputableInPolyTime.unary_add.comp + ((ComputableInPolyTime.encoding_length enc).prod + (ComputableInPolyTime.const 1))))))) + have hinitView : ComputableInPolyTime (fun a => M.toNTM.initView (enc a)) enc encFiniteCfg := + ComputableInPolyTime.finiteCfg_init + (ComputableInPolyTime.of_eq (encIn := enc) (encOut := encBits) (f := fun a => enc a) + fun _ => rfl) M.toNTM.q₀ + have htest : ComputableInPolyTime + (fun finite : FiniteCfg k Bool State => + decide (finite.state = none) && decide (finite.output = [true])) encFiniteCfg encBool := + ComputableInPolyTime.bool_and.comp + (((ComputableInPolyTime.of_finite fun state : Option State => + decide (state = none)).comp ComputableInPolyTime.finiteCfg_state).prod + (ComputableInPolyTime.decide_eq' ComputableInPolyTime.finiteCfg_output + (ComputableInPolyTime.const [true]))) + have hcount0 : ComputableInPolyTime (M.viewAcceptCount 0) encFiniteCfg encNat := + htest.ite (ComputableInPolyTime.const 1) (ComputableInPolyTime.const 0) + have htable0 : ComputableInPolyTime + (fun a => (views a).map fun view => (view, M.viewAcceptCount 0 view)) enc + (encList (encPair encFiniteCfg encNat)) := + ComputableInPolyTime.mapWithInput hsearch + ((ComputableInPolyTime.snd _ _).prod (hcount0.comp (ComputableInPolyTime.snd _ _))) + -- every table has polynomially many entries of polynomial length + set K := 8 + 2 * Nat.card (Option State) + 200 * k + set D := 2 * K * (c + 1) + set viewBound : α → ℕ := fun a => + MultiTapeNTM.viewLengthBound k State (enc a).length (c * (Nat.log2 (enc a).length + 1)) + set bound : α → ℕ := fun a => + (2 * (2 * ((enc a).length + 1)) ^ D) * (2 * (2 * viewBound a + 1 + (T a + 1)) + 1) + have hviewBound : PolyBounded (fun a => (enc a).length) viewBound := by + refine .of_forall_le (2 * (10 + 2 * Nat.card (Option State) + 200 * k) * (c + 2) + 1) 1 + fun a => ?_ + have hlog := Nat.mul_le_mul_left ((10 + 2 * Nat.card (Option State) + 200 * k) * c) + (Nat.log2_le_self (enc a).length) + simp only [viewBound, MultiTapeNTM.viewLengthBound, pow_one] + generalize 10 + 2 * Nat.card (Option State) + 200 * k = B at * + nlinarith [Nat.zero_le (B * c), Nat.zero_le (B * (enc a).length), + Nat.zero_le (B * c * (enc a).length)] + have hbound : PolyBounded (fun a => (enc a).length) bound := by + refine (PolyBounded.of_forall_le (2 * 2 ^ D) D fun a => ?_).mul + ((((PolyBounded.const 2).mul ((((PolyBounded.const 2).mul hviewBound).add + (.const 1)).add (hT.polyBounded.add (.const 1)))).add (.const 1))) + rw [mul_pow, ← mul_assoc] + have hstates : ∀ a, ∀ i ≤ T a, (encList (encPair encFiniteCfg encNat) + ((countRound M)^[i] ((views a).map fun view => (view, M.viewAcceptCount 0 view)))).length + ≤ bound a := by + intro a i hi + rw [countRound_iterate M (hclosed a)] + have hreach (finite) (hf : finite ∈ views a) := + (hmem a finite).mp hf + have hlen : (views a).length ≤ 2 * (2 * ((enc a).length + 1)) ^ D := + (MultiTapeNTM.length_le_of_nodup_reachable (hM a).1 + (Cslib.Reachability.nodup_search _ _) hreach).trans + (MultiTapeNTM.two_pow_coreLengthBound_log_le k State c _) + refine (length_encList_le _ _ (b := 2 * viewBound a + 1 + (T a + 1)) ?_).trans ?_ + · intro entry hentry + obtain ⟨view, hview, rfl⟩ := List.mem_map.mp hentry + have hv := MultiTapeNTM.length_encFiniteCfg_le (hM a).1 (hreach view hview) + have hn : (encNat (M.viewAcceptCount i view)).length ≤ i + 1 := by + have := length_encNat_le_log2 (MultiTapePTM.viewAcceptCount_le (machine := M) i view) + rwa [Nat.log2_two_pow] at this + rw [length_encPair] + simp only [viewBound] + omega + · rw [List.length_map] + exact Nat.mul_le_mul_right _ hlen + have htable : ComputableInPolyTime table enc (encList (encPair encFiniteCfg encNat)) := + ComputableInPolyTime.iterate hT htable0 (computableInPolyTime_countRound M) hbound hstates + have hcount : ComputableInPolyTime + (fun a => lookupCount (table a) (M.toNTM.initView (enc a))) enc encNat := + computableInPolyTime_lookupCount.comp (htable.prod hinitView) + exact ComputableInPolyTime.binary_le' + (ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 2) + (ComputableInPolyTime.binary_two_pow.comp hT)) + (ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 3) hcount) + · change a ∈ A ↔ + decide (2 * 2 ^ T a ≤ 3 * lookupCount (table a) (M.toNTM.initView (enc a))) = true + rw [hvalue, decide_eq_true_iff] + obtain ⟨-, -, hmemA, hnotA⟩ := hM a + refine ⟨hmemA, fun hle => by_contra fun ha => ?_⟩ + have hle' := (hnotA ha).trans' (Nat.mul_le_mul_left 3 (le_refl _)) + have hpos := Nat.two_pow_pos (T a) + simp only [T] at hle hpos + omega + +/-- **Randomized logarithmic space with one-sided error is within polynomial time.** -/ +theorem RL_subset_P : RL enc ⊆ P enc := fun _ h => BPL_subset_P (RL_subset_BPL h) + +end Cslib.Complexity diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean index 21a22f5898..a8002748d3 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean @@ -41,9 +41,12 @@ configuration graph, which has polynomially many vertices [Sipser, Section 8.4][ ## Main results * `Turing.MultiTapeNTM.reflTransGen_viewSucc_iff`: the successor lists give the reachable views. +* `Turing.MultiTapeNTM.mem_search_iff`: enough rounds find exactly the reachable views. * `Turing.MultiTapeNTM.searchAccepts_iff`: enough rounds decide acceptance. * `Turing.MultiTapeNTM.computableInPolyTime_viewSucc`: the successors in polynomial time. * `Turing.MultiTapeTM.ComputableInPolyTime.expand`: a round in polynomial time. +* `Turing.MultiTapeNTM.exists_computableInPolyTime_search`: under a logarithmic space bound, + enough rounds of breadth-first search find their views in polynomial time. * `Turing.MultiTapeNTM.exists_computableInPolyTime_searchAccepts`: under a logarithmic space bound, enough rounds of breadth-first search run in polynomial time. @@ -113,6 +116,19 @@ theorem reflTransGen_viewSucc_iff {finite next : FiniteCfg k Bool State} : simp only [viewSucc, hs, List.mem_map, mem_actions] exact ⟨action, htr, rfl⟩ +open scoped Classical in +/-- **Enough rounds find every reachable view**: under a space bound `s`, breadth-first search +for at least `2 ^ (2 * coreLengthBound k State n s + 1)` rounds finds exactly the views reachable +from the initial view. -/ +theorem mem_search_iff {input : List Bool} {s rounds : ℕ} (hs : ntm.RunsInSpace input s) + (hrounds : 2 ^ (2 * coreLengthBound k State input.length s + 1) ≤ rounds) + {finite : FiniteCfg k Bool State} : + finite ∈ Cslib.Reachability.search ntm.viewSucc rounds (ntm.initView input) ↔ + Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite := by + rw [Cslib.Reachability.mem_search_iff (fun views hnodup hreach => + length_le_of_nodup_reachable hs hnodup fun f hf => + reflTransGen_viewSucc_iff.mp (hreach f hf)) hrounds, reflTransGen_viewSucc_iff] + /-- **Enough rounds decide acceptance**: under a space bound `s`, breadth-first search for at least `2 ^ (2 * coreLengthBound k State n s + 1)` rounds finds an accepting view exactly when the machine accepts. -/ @@ -122,10 +138,8 @@ theorem searchAccepts_iff {input : List Bool} {s rounds : ℕ} (hs : ntm.RunsInS classical have hmem (finite : FiniteCfg k Bool State) : finite ∈ Cslib.Reachability.search ntm.viewSucc rounds (ntm.initView input) ↔ - Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite := by - rw [Cslib.Reachability.mem_search_iff (fun views hnodup hreach => - length_le_of_nodup_reachable hs hnodup fun f hf => - reflTransGen_viewSucc_iff.mp (hreach f hf)) hrounds, reflTransGen_viewSucc_iff] + Relation.ReflTransGen ntm.ViewStep (ntm.initView input) finite := + mem_search_iff hs hrounds rw [accepts_iff_reflTransGen_viewStep, searchAccepts] simp only [List.any_eq_true, Bool.and_eq_true, decide_eq_true_eq, hmem] @@ -220,16 +234,17 @@ private theorem rounds_le (k : ℕ) (State : Type) (c n : ℕ) : (two_pow_coreLengthBound_log_le k State c n).trans_eq (by rw [mul_pow, ← mul_assoc]) open scoped Classical in -/-- **Acceptance within logarithmic space is decided by breadth-first search in polynomial time.** -If every computation prefix of `ntm` on every encoded instance `enc a` stays within space -`c * (Nat.log2 n + 1)`, then some polynomial number of rounds suffices for -`Turing.MultiTapeNTM.searchAccepts_iff`, and breadth-first search for that many rounds is -polynomial-time in the encoded instance. -/ -theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List Bool} {c : ℕ} +/-- **Breadth-first search within logarithmic space is polynomial-time.** If every computation +prefix of `ntm` on every encoded instance `enc a` stays within space `c * (Nat.log2 n + 1)`, then +for some polynomial number of rounds, at least the bound of `Turing.MultiTapeNTM.searchAccepts_iff`, +the list of views found by breadth-first search from the initial view is polynomial-time in the +encoded instance. -/ +theorem exists_computableInPolyTime_search {α : Type} {enc : α ↪ List Bool} {c : ℕ} (hs : ∀ a, ntm.RunsInSpace (enc a) (c * (Nat.log2 (enc a).length + 1))) : ∃ rounds : α → ℕ, (∀ a, 2 ^ (2 * coreLengthBound k State (enc a).length (c * (Nat.log2 (enc a).length + 1)) + 1) ≤ rounds a) ∧ - ComputableInPolyTime (fun a => ntm.searchAccepts (rounds a) (enc a)) enc encBool := by + ComputableInPolyTime (fun a => Cslib.Reachability.search ntm.viewSucc (rounds a) + (ntm.initView (enc a))) enc (encList encFiniteCfg) := by set D := 2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1) set rounds : α → ℕ := fun a => 2 * 2 ^ D * ((enc a).length + 1) ^ D refine ⟨rounds, fun a => rounds_le k State c _, ?_⟩ @@ -269,8 +284,22 @@ theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List refine (length_encList_le encFiniteCfg _ fun finite hf => length_encFiniteCfg_le (hs a) (hreach finite hf)).trans ?_ exact Nat.mul_le_mul_right _ hlen - have hsearch := ComputableInPolyTime.iterate hcount hinit + exact ComputableInPolyTime.iterate hcount hinit (ComputableInPolyTime.expand computableInPolyTime_viewSucc) hbound hstates + +open scoped Classical in +/-- **Acceptance within logarithmic space is decided by breadth-first search in polynomial time.** +If every computation prefix of `ntm` on every encoded instance `enc a` stays within space +`c * (Nat.log2 n + 1)`, then some polynomial number of rounds suffices for +`Turing.MultiTapeNTM.searchAccepts_iff`, and breadth-first search for that many rounds is +polynomial-time in the encoded instance. -/ +theorem exists_computableInPolyTime_searchAccepts {α : Type} {enc : α ↪ List Bool} {c : ℕ} + (hs : ∀ a, ntm.RunsInSpace (enc a) (c * (Nat.log2 (enc a).length + 1))) : + ∃ rounds : α → ℕ, (∀ a, 2 ^ (2 * coreLengthBound k State (enc a).length + (c * (Nat.log2 (enc a).length + 1)) + 1) ≤ rounds a) ∧ + ComputableInPolyTime (fun a => ntm.searchAccepts (rounds a) (enc a)) enc encBool := by + obtain ⟨rounds, hrounds, hsearch⟩ := exists_computableInPolyTime_search hs + refine ⟨rounds, hrounds, ?_⟩ have htest : ComputableInPolyTime (fun finite : FiniteCfg k Bool State => decide (finite.state = none) && decide (finite.output = [true])) encFiniteCfg encBool := diff --git a/ComplexityTests/RandomizedLogSpace.lean b/ComplexityTests/RandomizedLogSpace.lean index c6b30b8a5e..6720b40afb 100644 --- a/ComplexityTests/RandomizedLogSpace.lean +++ b/ComplexityTests/RandomizedLogSpace.lean @@ -5,6 +5,7 @@ Authors: Christian Reitwiessner -/ import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix +import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.PolyTime import Complexity.Computability.Complexity.Classes.LogSpace.USTCON /-! @@ -23,6 +24,9 @@ example : USTCON ∈ BPL encUSTCON := L_subset_BPL USTCON_mem_L -- Going through `RL` recovers `USTCON ∈ NL`. example : USTCON ∈ NL encUSTCON := RL_subset_NL (L_subset_RL USTCON_mem_L) +-- Going through `BPL` places `USTCON` in `P`. +example : USTCON ∈ P encUSTCON := BPL_subset_P (L_subset_BPL USTCON_mem_L) + section HaltingTime open Cslib.Turing Turing @@ -197,6 +201,26 @@ example (input : List Bool) : ∃ (V : Finset (FiniteCfg 0 Bool Unit)) · exact MultiTapePTM.liveConfigMatrix_pow_eq_zero ℚ (runsInTime_coinFlip input) hV fun finite hf => (hreach _).mp hf +-- The count recursion evaluated by the `BPL ⊆ P` algorithm gives the one accepting coin string +-- of `coinFlip`, and four times as many at clock three. +example (input : List Bool) : + coinFlip.viewAcceptCount 1 (coinFlip.toNTM.initView input) = 1 ∧ + coinFlip.viewAcceptCount 3 (coinFlip.toNTM.initView input) = 4 := by + obtain ⟨V, hreach, hV, -⟩ := + coinFlip.exists_finset_reachable (MultiTapeNTM.runsInSpace_zero_tapes _ input 0) + have hinit : coinFlip.toNTM.initView input ∈ V := (hreach _).mpr .refl + rw [← MultiTapePTM.acceptCoins_eq_viewAcceptCount hV hinit, + ← MultiTapePTM.acceptCoins_eq_viewAcceptCount hV hinit, + MultiTapePTM.acceptCoins_add coinFlip (runsInTime_coinFlip input) 2, acceptCoins_coinFlip] + exact ⟨rfl, rfl⟩ + +-- Every language accepted by the fair coin is decided in polynomial time. +example (enc : ℕ ↪ List Bool) : (Set.univ : Set ℕ) ∈ Cslib.Complexity.P enc := + Cslib.Complexity.RL_subset_P + ⟨0, Unit, inferInstance, coinFlip, 0, fun a => + ⟨MultiTapeNTM.runsInSpace_zero_tapes _ _ _, 1, runsInTime_coinFlip _, + fun _ => by rw [acceptCoins_coinFlip]; rfl, fun ha => absurd trivial ha⟩⟩ + end ConfigurationMatrix end ComplexityTests.RandomizedLogSpace