From d5e4481cd91d9c96efab6186e4f91cb3baab5845 Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 18:05:09 +0000 Subject: [PATCH] refactor(Complexity/Reduction): move polyTimeReducible_of_mem_P and oracle substitution to topic modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move polyTimeReducible_of_mem_P from the Berman-Hartmanis conjecture module to Reduction/Nontrivial.lean, and oracle substitution (P^{O1} ⊆ P^{O2} when O1 ∈ P^{O2}) from Reduction/Turing.lean to Classes/Oracle/Substitution.lean. Add _iff_manyOneReducibleBy bridges for the restricted one-one reducibilities in Reduction/Isomorphism.lean and derive their refl, trans, compl and projections from the ManyOneReducibleBy API. Part of #4737. Jetski worker session a924892d. --- CslibFrontier.lean | 2 + .../Complexity/Classes/Ladner/Density.lean | 2 +- .../Classes/Oracle/Substitution.lean | 192 ++++++++++++++++++ .../Complexity/Reduction/Isomorphism.lean | 97 +++++---- .../Reduction/Isomorphism/Conjecture.lean | 15 +- .../Complexity/Reduction/Nontrivial.lean | 44 ++++ .../Complexity/Reduction/Turing.lean | 154 +------------- 7 files changed, 298 insertions(+), 208 deletions(-) create mode 100644 CslibFrontier/Computability/Complexity/Classes/Oracle/Substitution.lean create mode 100644 CslibFrontier/Computability/Complexity/Reduction/Nontrivial.lean diff --git a/CslibFrontier.lean b/CslibFrontier.lean index 532bdc3f6b..84ae212708 100644 --- a/CslibFrontier.lean +++ b/CslibFrontier.lean @@ -2019,6 +2019,7 @@ public import CslibFrontier.Computability.Complexity.Classes.Oracle.PolyTime public import CslibFrontier.Computability.Complexity.Classes.Oracle.QueryBit public import CslibFrontier.Computability.Complexity.Classes.Oracle.SelfReduction public import CslibFrontier.Computability.Complexity.Classes.Oracle.Space +public import CslibFrontier.Computability.Complexity.Classes.Oracle.Substitution public import CslibFrontier.Computability.Complexity.Classes.Oracle.TQBF public import CslibFrontier.Computability.Complexity.Classes.Oracle.ThresholdSearch public import CslibFrontier.Computability.Complexity.Classes.Oracle.WitnessBit @@ -2635,6 +2636,7 @@ public import CslibFrontier.Computability.Complexity.Reduction.LogSpaceBoundedAu public import CslibFrontier.Computability.Complexity.Reduction.LogSpaceBoundedTruthTable public import CslibFrontier.Computability.Complexity.Reduction.LogSpaceTruthTable public import CslibFrontier.Computability.Complexity.Reduction.ManyOne +public import CslibFrontier.Computability.Complexity.Reduction.Nontrivial public import CslibFrontier.Computability.Complexity.Reduction.OneOne public import CslibFrontier.Computability.Complexity.Reduction.TruthTable public import CslibFrontier.Computability.Complexity.Reduction.TruthTableVariants diff --git a/CslibFrontier/Computability/Complexity/Classes/Ladner/Density.lean b/CslibFrontier/Computability/Complexity/Classes/Ladner/Density.lean index 4dcc6b3a5b..55035badc6 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Ladner/Density.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Ladner/Density.lean @@ -13,7 +13,7 @@ import CslibFrontier.Computability.Complexity.Classes.EXP.Decidable import CslibFrontier.Computability.Complexity.Classes.Immune import CslibFrontier.Computability.Complexity.Classes.Inclusions import CslibFrontier.Computability.Complexity.Classes.NP.Closure -import CslibFrontier.Computability.Complexity.Reduction.Isomorphism.Conjecture +import CslibFrontier.Computability.Complexity.Reduction.Nontrivial import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.BoundedSearch import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List diff --git a/CslibFrontier/Computability/Complexity/Classes/Oracle/Substitution.lean b/CslibFrontier/Computability/Complexity/Classes/Oracle/Substitution.lean new file mode 100644 index 0000000000..6241e63eb2 --- /dev/null +++ b/CslibFrontier/Computability/Complexity/Classes/Oracle/Substitution.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Computability.Complexity.Classes.Oracle.PolyTime +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Configuration +import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial.Automation +import CslibFrontier.Computability.Probabilistic.Oracle.Composition + +/-! +# Oracle substitution for polynomial-time oracle classes + +If an oracle language `O₁` belongs to `P^{O₂}`, a polynomial-time computation relative to `O₁` +becomes one relative to `O₂`: each query to `O₁` is answered by running the polynomial-time +`O₂`-oracle program deciding `O₁`. The simulation runs a finite oracle machine for the outer +computation and replaces each of its oracle steps by a call to the inner program; the outer clock +bounds both the number and the length of the queries, so the composite stays polynomial. + +The special case where `O₁` many-one reduces to `O₂` is +`Cslib.Complexity.PolyTimeReducible.PWithOracle_subset` in +`CslibFrontier.Computability.Complexity.Classes.Oracle.Monotone`, which also covers non-Boolean +outputs. + +## Main results + +* `Cslib.Complexity.ComputableInPolyTimeWithOracle.of_mem_PWithOracle`: a Boolean function + computable in polynomial time relative to `O₁ ∈ P^{O₂}` is computable in polynomial time + relative to `O₂`. +* `Cslib.Complexity.PWithOracle_subset_of_mem_PWithOracle`, + `Cslib.Complexity.NPWithOracle_subset_of_mem_PWithOracle`: if `O₁ ∈ P^{O₂}`, then + `P^{O₁} ⊆ P^{O₂}` and `NP^{O₁} ⊆ NP^{O₂}`. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α : Type} {encA : α ↪ List Bool} + +/-- One simulated instruction of a finite oracle machine `machine` when each query to its oracle is +answered by running the deterministic oracle program `prog`. -/ +private def oracleAnswerStep {k : ℕ} {Control : Type} + (machine : Turing.MultiTapePTM k Bool Control Unit) + (prog : List Bool → WordQueryComp Unit Bool) + (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : + WordQueryComp Unit (Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) := + if (machine.pendingQuery cfg).isSome then + (fun b => machine.receiveBit (cfg, b)) <$> prog (machine.pendingRequest cfg) + else + pure (machine.localStep cfg) + +private theorem interpret_oracleAnswerStep {k : ℕ} {Control : Type} + (machine : Turing.MultiTapePTM k Bool Control Unit) + (prog : List Bool → WordQueryComp Unit Bool) + (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : + OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg) = + if (machine.pendingQuery cfg).isSome then + (fun b => machine.receiveBit (cfg, b)) <$> + OracleComp.interpret ProbOracleComp.query (prog (machine.pendingRequest cfg)) + else + pure (machine.localStep cfg) := by + unfold oracleAnswerStep + split <;> simp [OracleComp.interpret_map] + +private theorem isOraclePPTOn_oracleAnswerStep {k : ℕ} {Control : Type} [Finite Control] + (machine : Turing.MultiTapePTM k Bool Control Unit) + {prog : List Bool → WordQueryComp Unit Bool} + (hprog : Probability.IsOraclePPTOn encBits encBool + (fun w => OracleComp.interpret ProbOracleComp.query (prog w))) : + Probability.IsOraclePPTOn encFiniteConfig encFiniteConfig + (fun cfg => + OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg)) := by + simp only [interpret_oracleAnswerStep] + exact Probability.IsOraclePPTOn.cond' + ((ComputableInPolyTime.of_finite Option.isSome).comp machine.pendingQuery_pt) + ((hprog.preprocess' machine.pendingRequest_pt).map_with' + (f := fun cfg b => machine.receiveBit (cfg, b)) machine.receiveBit_pt) + machine.localStep_pt.isOraclePPTOn + +private theorem spaceBound_of_mem_support_oracleAnswerStep {k : ℕ} {Control : Type} + (machine : Turing.MultiTapePTM k Bool Control Unit) + (prog : List Bool → WordQueryComp Unit Bool) + {inputSize steps : ℕ} + {cfg next : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit} + (hcfg : Turing.MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 1 cfg) + (hnext : next ∈ OracleComp.support + (OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg))) : + Turing.MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + 1) 1 next := by + rw [interpret_oracleAnswerStep] at hnext + split_ifs at hnext with hq + · obtain ⟨b, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hnext + have hstep := machine.spaceBound_answerStep (fun _ => b) hcfg + rw [machine.answerStep_bit (fun _ => b)] at hstep + simpa [hq] using hstep + · rw [OracleComp.eq_of_mem_supportWith_pure hnext] + have hstep := machine.spaceBound_answerStep (fun _ => false) hcfg + rw [machine.answerStep_bit (fun _ => false)] at hstep + simpa [hq] using hstep + +private theorem interpret_id_oracleAnswerStep {k : ℕ} {Control : Type} + (machine : Turing.MultiTapePTM k Bool Control Unit) + {prog : List Bool → WordQueryComp Unit Bool} {O : Set (List Bool)} {g : List Bool → Bool} + (hg : ∀ w, OracleComp.interpret (m := Id) (languageOracle O) (prog w) = g w) + (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : + OracleComp.interpret (m := Id) (languageOracle O) (oracleAnswerStep machine prog cfg) = + machine.answerStep (fun q => [g q.2]) cfg := by + rw [machine.answerStep_bit] + unfold oracleAnswerStep + split_ifs with hq + · rw [OracleComp.interpret_map, hg] + rfl + · rfl + +open Classical in +/-- **Oracle substitution for polynomial-time Boolean computations**: if an oracle language `O₁` +belongs to `P^{O₂}` and `f : α → Bool` is computable in polynomial time relative to `O₁`, then +`f` is computable in polynomial time relative to `O₂`. -/ +theorem ComputableInPolyTimeWithOracle.of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} {f : α → Bool} + (hO₁ : O₁ ∈ PWithOracle O₂ encBits) + (hf : ComputableInPolyTimeWithOracle O₁ f encA encBool) : + ComputableInPolyTimeWithOracle O₂ f encA encBool := by + obtain ⟨g, ⟨prog, hprog, hg⟩, hgO₁⟩ := hO₁ + have hg' : g = fun w => decide (w ∈ O₁) := funext fun w => + Bool.eq_iff_iff.mpr ⟨fun h => decide_eq_true ((hgO₁ w).mpr h), + fun h => (hgO₁ w).mp (of_decide_eq_true h)⟩ + subst hg' + obtain ⟨program, hcert, hprogram⟩ := hf + obtain ⟨k, m, machine, c, d, hrun⟩ := hcert.exists_fin_run_pure_false + obtain ⟨cf, hcf⟩ := length_encFiniteConfig_le (k := k) (State := Fin m) (Oracle := Unit) + have hcount : ComputableInPolyTime (fun a => c * ((encA a).length + 1) ^ d) encA + encUnary := + ((ComputableInPolyTime.unary_eval (Polynomial.C c * (Polynomial.X + 1) ^ d)).comp + (ComputableInPolyTime.encoding_length encA)).of_enc_eq fun a => by simp + have hinit : ComputableInPolyTime + (fun a => Turing.MultiTapeMachine.FiniteConfig.init (k := k) (Oracle := Unit) + machine.initial (encA a)) + encA encFiniteConfig := by + refine (((ComputableInPolyTime.of_eq fun _ => rfl : + ComputableInPolyTime encA encA encBits).prod + (ComputableInPolyTime.const (encOut := + encPair (encFinite (Option (Fin m))) + (encPair encUnary (encPair (encPi (Index := Fin k) (encBiTape encBool)) encBits))) + (some machine.initial, 1, fun _ => Cslib.Turing.BiTape.nil, []))).prod + (ComputableInPolyTime.const + (encOut := encPi (Index := Unit) (encPair encBits (encBiTape encBool))) + fun _ : Unit => ([], Cslib.Turing.BiTape.nil))).of_enc_eq fun a => ?_ + simp [Turing.MultiTapeMachine.FiniteConfig.init, Turing.FiniteCfg.init] + have hbound : PolyBounded (fun a => (encA a).length) + (fun a => cf * ((encA a).length + c * ((encA a).length + 1) ^ d + 1 + 1)) := by growth_poly + have hit := (Probability.IsOraclePPTOn.iterate_spec' hcount hinit + (isOraclePPTOn_oracleAnswerStep machine hprog) + (fun a i cfg => Turing.MultiTapeMachine.FiniteConfig.SpaceBound (encA a).length i 1 cfg) + (fun _ => Turing.MultiTapeMachine.FiniteConfig.spaceBound_init _ _ _) + (fun _ _ _ _ hinv _ hnext => + spaceBound_of_mem_support_oracleAnswerStep machine prog hinv hnext) + hbound + (fun _ _ _ hi hinv => (hcf _ _ _ _ hinv).trans (Nat.mul_le_mul_left cf (by omega)))).1 + refine ⟨fun a => (fun cfg => cfg.tapes.output.headD false) <$> + OracleComp.iterate (c * ((encA a).length + 1) ^ d) (oracleAnswerStep machine prog) + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a)), ?_, fun a => ?_⟩ + · simp only [OracleComp.interpret_map, OracleComp.interpret_iterate] + exact hit.map' (by fun_prop) + · rw [OracleComp.interpret_map, OracleComp.interpret_id_iterate] + simp only [interpret_id_oracleAnswerStep machine hg] + change ((machine.answerStep (languageOracle O₁))^[c * ((encA a).length + 1) ^ d] + (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))).tapes.output.headD + false = f a + rw [← machine.interpret_run_pure_false, hrun a (languageOracle O₁), ← hprogram a] + simp + +/-- If `O₁ ∈ P^{O₂}`, then `P^{O₁} ⊆ P^{O₂}`. -/ +theorem PWithOracle_subset_of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} + (hO₁ : O₁ ∈ PWithOracle O₂ encBits) (enc : α ↪ List Bool) : + PWithOracle O₁ enc ⊆ PWithOracle O₂ enc := + fun _ ⟨f, hf, hL⟩ => ⟨f, hf.of_mem_PWithOracle hO₁, hL⟩ + +/-- If `O₁ ∈ P^{O₂}`, then `NP^{O₁} ⊆ NP^{O₂}`. -/ +theorem NPWithOracle_subset_of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} + (hO₁ : O₁ ∈ PWithOracle O₂ encBits) (enc : α ↪ List Bool) : + NPWithOracle O₁ enc ⊆ NPWithOracle O₂ enc := + fun _ ⟨p, V, hV, hL⟩ => ⟨p, V, hV.of_mem_PWithOracle hO₁, hL⟩ + +end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/Reduction/Isomorphism.lean b/CslibFrontier/Computability/Complexity/Reduction/Isomorphism.lean index 80d9b27018..72bc0e2128 100644 --- a/CslibFrontier/Computability/Complexity/Reduction/Isomorphism.lean +++ b/CslibFrontier/Computability/Complexity/Reduction/Isomorphism.lean @@ -52,6 +52,10 @@ This module formalizes: `Cslib.Complexity.PolyTimeIsomorphic.refl`, `Cslib.Complexity.PolyTimeIsomorphic.symm`, `Cslib.Complexity.PolyTimeIsomorphic.trans`. +* The three one-one variants are instances of `Cslib.Complexity.ManyOneReducibleBy`: + `Cslib.Complexity.polyTimeInvertibleOneOneReducible_iff_manyOneReducibleBy`, + `Cslib.Complexity.polyTimeLengthIncreasingOneOneReducible_iff_manyOneReducibleBy`, + `Cslib.Complexity.polyTimeInvertibleLengthIncreasingOneOneReducible_iff_manyOneReducibleBy`. * Reflexivity and transitivity of `≤₁,ᵢ`; transitivity of `≤₁,ₗᵢ` and `≤₁,ᵢₗ`: `Cslib.Complexity.PolyTimeInvertibleOneOneReducible.refl`, `Cslib.Complexity.PolyTimeInvertibleOneOneReducible.trans`, @@ -189,31 +193,34 @@ def PolyTimeInvertibleOneOneReducible (encA : α ↪ List Bool) (encB : β ↪ L Function.LeftInverse g f) ∧ ∀ a, a ∈ A ↔ f a ∈ B +/-- Invertible one-one reducibility is many-one reducibility by the polynomial-time maps with a +polynomial-time left inverse. -/ +theorem polyTimeInvertibleOneOneReducible_iff_manyOneReducibleBy : + PolyTimeInvertibleOneOneReducible encA encB A B ↔ + ManyOneReducibleBy (fun f => ∃ g : β → α, ComputableInPolyTime f encA encB ∧ + ComputableInPolyTime g encB encA ∧ Function.LeftInverse g f) A B := + Iff.rfl + /-- The identity is a polynomial-time-invertible one-one reduction. -/ @[refl] theorem PolyTimeInvertibleOneOneReducible.refl (encA : α ↪ List Bool) (A : Set α) : PolyTimeInvertibleOneOneReducible encA encA A A := - ⟨id, ⟨id, ComputableInPolyTime.id', ComputableInPolyTime.id', fun _ => rfl⟩, fun _ => Iff.rfl⟩ + ManyOneReducibleBy.refl ⟨id, .id', .id', fun _ => rfl⟩ A /-- Polynomial-time-invertible one-one reductions compose. -/ @[trans] theorem PolyTimeInvertibleOneOneReducible.trans (hAB : PolyTimeInvertibleOneOneReducible encA encB A B) (hBC : PolyTimeInvertibleOneOneReducible encB encC B C) : - PolyTimeInvertibleOneOneReducible encA encC A C := by - obtain ⟨f₁, ⟨g₁, hf₁, hg₁, hleft₁⟩, h₁⟩ := hAB - obtain ⟨f₂, ⟨g₂, hf₂, hg₂, hleft₂⟩, h₂⟩ := hBC - refine ⟨f₂ ∘ f₁, ⟨g₁ ∘ g₂, hf₂.comp hf₁, hg₁.comp hg₂, fun a => ?_⟩, fun a => ?_⟩ - · dsimp - rw [hleft₂, hleft₁] - · rw [Function.comp_apply, ← h₂ (f₁ a), ← h₁ a] + PolyTimeInvertibleOneOneReducible encA encC A C := + ManyOneReducibleBy.trans (fun _ _ ⟨g₁, hf₁, hg₁, hleft₁⟩ ⟨g₂, hf₂, hg₂, hleft₂⟩ => + ⟨g₁ ∘ g₂, hf₂.comp hf₁, hg₁.comp hg₂, hleft₂.comp hleft₁⟩) hAB hBC /-- An invertible one-one reduction from `A` to `B` is one from `Aᶜ` to `Bᶜ`. -/ theorem PolyTimeInvertibleOneOneReducible.compl (h : PolyTimeInvertibleOneOneReducible encA encB A B) : - PolyTimeInvertibleOneOneReducible encA encB Aᶜ Bᶜ := by - obtain ⟨f, hf, hAB⟩ := h - exact ⟨f, hf, fun a => not_congr (hAB a)⟩ + PolyTimeInvertibleOneOneReducible encA encB Aᶜ Bᶜ := + ManyOneReducibleBy.compl h /-- A polynomial-time isomorphism is an invertible one-one reduction. -/ theorem PolyTimeIsomorphic.polyTimeInvertibleOneOneReducible @@ -225,9 +232,8 @@ theorem PolyTimeIsomorphic.polyTimeInvertibleOneOneReducible /-- An invertible one-one reduction is an injective one-one reduction. -/ theorem PolyTimeInvertibleOneOneReducible.polyTimeOneOneReducible (h : PolyTimeInvertibleOneOneReducible encA encB A B) : - PolyTimeOneOneReducible encA encB A B := by - obtain ⟨f, ⟨_, hf, _, hleft⟩, hAB⟩ := h - exact ⟨f, ⟨hf, hleft.injective⟩, hAB⟩ + PolyTimeOneOneReducible encA encB A B := + ManyOneReducibleBy.mono (fun _ ⟨_, hf, _, hleft⟩ => ⟨hf, hleft.injective⟩) h /-- An invertible one-one reduction is a many-one reduction. -/ theorem PolyTimeInvertibleOneOneReducible.polyTimeReducible @@ -259,31 +265,34 @@ def PolyTimeLengthIncreasingOneOneReducible (encA : α ↪ List Bool) (encB : β ∀ a, (encA a).length < (encB (f a)).length) ∧ ∀ a, a ∈ A ↔ f a ∈ B +/-- Length-increasing one-one reducibility is many-one reducibility by the injective, +length-increasing polynomial-time maps. -/ +theorem polyTimeLengthIncreasingOneOneReducible_iff_manyOneReducibleBy : + PolyTimeLengthIncreasingOneOneReducible encA encB A B ↔ + ManyOneReducibleBy (fun f => ComputableInPolyTime f encA encB ∧ Function.Injective f ∧ + ∀ a, (encA a).length < (encB (f a)).length) A B := + Iff.rfl + /-- Length-increasing one-one reductions compose. -/ @[trans] theorem PolyTimeLengthIncreasingOneOneReducible.trans (hAB : PolyTimeLengthIncreasingOneOneReducible encA encB A B) (hBC : PolyTimeLengthIncreasingOneOneReducible encB encC B C) : - PolyTimeLengthIncreasingOneOneReducible encA encC A C := by - obtain ⟨f₁, ⟨hf₁, hfi₁, hlen₁⟩, h₁⟩ := hAB - obtain ⟨f₂, ⟨hf₂, hfi₂, hlen₂⟩, h₂⟩ := hBC - refine ⟨f₂ ∘ f₁, ⟨hf₂.comp hf₁, hfi₂.comp hfi₁, fun a => ?_⟩, fun a => ?_⟩ - · exact (hlen₁ a).trans (hlen₂ (f₁ a)) - · rw [Function.comp_apply, ← h₂ (f₁ a), ← h₁ a] + PolyTimeLengthIncreasingOneOneReducible encA encC A C := + ManyOneReducibleBy.trans (fun f₁ _ ⟨hf₁, hfi₁, hlen₁⟩ ⟨hf₂, hfi₂, hlen₂⟩ => + ⟨hf₂.comp hf₁, hfi₂.comp hfi₁, fun a => (hlen₁ a).trans (hlen₂ (f₁ a))⟩) hAB hBC /-- A length-increasing one-one reduction from `A` to `B` is one from `Aᶜ` to `Bᶜ`. -/ theorem PolyTimeLengthIncreasingOneOneReducible.compl (h : PolyTimeLengthIncreasingOneOneReducible encA encB A B) : - PolyTimeLengthIncreasingOneOneReducible encA encB Aᶜ Bᶜ := by - obtain ⟨f, hf, hAB⟩ := h - exact ⟨f, hf, fun a => not_congr (hAB a)⟩ + PolyTimeLengthIncreasingOneOneReducible encA encB Aᶜ Bᶜ := + ManyOneReducibleBy.compl h /-- A length-increasing one-one reduction is an injective one-one reduction. -/ theorem PolyTimeLengthIncreasingOneOneReducible.polyTimeOneOneReducible (h : PolyTimeLengthIncreasingOneOneReducible encA encB A B) : - PolyTimeOneOneReducible encA encB A B := by - obtain ⟨f, ⟨hf, hfi, _⟩, hAB⟩ := h - exact ⟨f, ⟨hf, hfi⟩, hAB⟩ + PolyTimeOneOneReducible encA encB A B := + ManyOneReducibleBy.mono (fun _ ⟨hf, hfi, _⟩ => ⟨hf, hfi⟩) h /-- A length-increasing one-one reduction is a many-one reduction. -/ theorem PolyTimeLengthIncreasingOneOneReducible.polyTimeReducible @@ -318,40 +327,42 @@ def PolyTimeInvertibleLengthIncreasingOneOneReducible (encA : α ↪ List Bool) ∀ a, (encA a).length < (encB (f a)).length) ∧ ∀ a, a ∈ A ↔ f a ∈ B +/-- Invertible, length-increasing one-one reducibility is many-one reducibility by the +length-increasing polynomial-time maps with a polynomial-time left inverse. -/ +theorem polyTimeInvertibleLengthIncreasingOneOneReducible_iff_manyOneReducibleBy : + PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB A B ↔ + ManyOneReducibleBy (fun f => ∃ g : β → α, ComputableInPolyTime f encA encB ∧ + ComputableInPolyTime g encB encA ∧ Function.LeftInverse g f ∧ + ∀ a, (encA a).length < (encB (f a)).length) A B := + Iff.rfl + /-- Length-increasing, invertible one-one reductions compose. -/ @[trans] theorem PolyTimeInvertibleLengthIncreasingOneOneReducible.trans (hAB : PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB A B) (hBC : PolyTimeInvertibleLengthIncreasingOneOneReducible encB encC B C) : - PolyTimeInvertibleLengthIncreasingOneOneReducible encA encC A C := by - obtain ⟨f₁, ⟨g₁, hf₁, hg₁, hleft₁, hlen₁⟩, h₁⟩ := hAB - obtain ⟨f₂, ⟨g₂, hf₂, hg₂, hleft₂, hlen₂⟩, h₂⟩ := hBC - refine ⟨f₂ ∘ f₁, ⟨g₁ ∘ g₂, hf₂.comp hf₁, hg₁.comp hg₂, fun a => ?_, fun a => ?_⟩, fun a => ?_⟩ - · dsimp - rw [hleft₂, hleft₁] - · exact (hlen₁ a).trans (hlen₂ (f₁ a)) - · rw [Function.comp_apply, ← h₂ (f₁ a), ← h₁ a] + PolyTimeInvertibleLengthIncreasingOneOneReducible encA encC A C := + ManyOneReducibleBy.trans (fun f₁ _ ⟨g₁, hf₁, hg₁, hleft₁, hlen₁⟩ ⟨g₂, hf₂, hg₂, hleft₂, hlen₂⟩ => + ⟨g₁ ∘ g₂, hf₂.comp hf₁, hg₁.comp hg₂, hleft₂.comp hleft₁, + fun a => (hlen₁ a).trans (hlen₂ (f₁ a))⟩) hAB hBC /-- An invertible, length-increasing one-one reduction from `A` to `B` is one from `Aᶜ` to `Bᶜ`. -/ theorem PolyTimeInvertibleLengthIncreasingOneOneReducible.compl (h : PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB A B) : - PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB Aᶜ Bᶜ := by - obtain ⟨f, hf, hAB⟩ := h - exact ⟨f, hf, fun a => not_congr (hAB a)⟩ + PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB Aᶜ Bᶜ := + ManyOneReducibleBy.compl h /-- An invertible, length-increasing one-one reduction is an invertible one-one reduction. -/ theorem PolyTimeInvertibleLengthIncreasingOneOneReducible.polyTimeInvertibleOneOneReducible (h : PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB A B) : - PolyTimeInvertibleOneOneReducible encA encB A B := by - obtain ⟨f, ⟨g, hf, hg, hleft, _⟩, hAB⟩ := h - exact ⟨f, ⟨g, hf, hg, hleft⟩, hAB⟩ + PolyTimeInvertibleOneOneReducible encA encB A B := + ManyOneReducibleBy.mono (fun _ ⟨g, hf, hg, hleft, _⟩ => ⟨g, hf, hg, hleft⟩) h /-- An invertible, length-increasing one-one reduction is a length-increasing one-one reduction. -/ theorem PolyTimeInvertibleLengthIncreasingOneOneReducible.polyTimeLengthIncreasingOneOneReducible (h : PolyTimeInvertibleLengthIncreasingOneOneReducible encA encB A B) : - PolyTimeLengthIncreasingOneOneReducible encA encB A B := by - obtain ⟨f, ⟨_, hf, _, hleft, hlen⟩, hAB⟩ := h - exact ⟨f, ⟨hf, hleft.injective, hlen⟩, hAB⟩ + PolyTimeLengthIncreasingOneOneReducible encA encB A B := + ManyOneReducibleBy.mono (fun _ ⟨_, hf, _, hleft, hlen⟩ => ⟨hf, hleft.injective, hlen⟩) h /-- An invertible, length-increasing one-one reduction is an injective one-one reduction. -/ theorem PolyTimeInvertibleLengthIncreasingOneOneReducible.polyTimeOneOneReducible diff --git a/CslibFrontier/Computability/Complexity/Reduction/Isomorphism/Conjecture.lean b/CslibFrontier/Computability/Complexity/Reduction/Isomorphism/Conjecture.lean index b16e6224b5..20fd5e1c23 100644 --- a/CslibFrontier/Computability/Complexity/Reduction/Isomorphism/Conjecture.lean +++ b/CslibFrontier/Computability/Complexity/Reduction/Isomorphism/Conjecture.lean @@ -11,6 +11,7 @@ public import CslibFrontier.Init public import CslibFrontier.Computability.Complexity.Problems.SAT.Paddable import CslibFrontier.Computability.Complexity.CookLevin.Completeness import CslibFrontier.Computability.Complexity.Problems.SAT.PolyTime +import CslibFrontier.Computability.Complexity.Reduction.Nontrivial import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic /-! @@ -43,8 +44,6 @@ of arguments in the report. ## Main results -* `Cslib.Complexity.polyTimeReducible_of_mem_P`: every language in `P` reduces to every language - with a member and a nonmember. * `Cslib.Complexity.bermanHartmanisConjecture_iff_paddable`: the conjecture holds exactly when every `NP`-complete language of bit strings is paddable. * `Cslib.Complexity.BermanHartmanisConjecture.SAT_notMem_P`, @@ -73,18 +72,6 @@ so that clients can apply the hypothesis to particular languages. -/ ∀ A B : Set (List Bool), NPComplete encBits A → NPComplete encBits B → PolyTimeIsomorphic encBits encBits A B -/-- Every language in `P` reduces to every language with a member `b₁` and a nonmember `b₀`: -decide membership and output `b₁` or `b₀`. -/ -theorem polyTimeReducible_of_mem_P {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} - {A : Set α} {B : Set β} (hA : A ∈ P encA) {b₁ b₀ : β} (h₁ : b₁ ∈ B) (h₀ : b₀ ∉ B) : - PolyTimeReducible encA encB A B := by - obtain ⟨f, hf, hfA⟩ := hA - refine ⟨fun a => if f a then b₁ else b₀, hf.ite (.const b₁) (.const b₀), fun a => ?_⟩ - rw [hfA a] - cases hfa : f a - · simp only [hfa, Bool.false_eq_true, ↓reduceIte, h₀] - · simp only [hfa, ↓reduceIte, h₁] - /-- **The conjecture is paddability of every `NP`-complete language** of bit strings. The words that decode to satisfiable formulas form a paddable `NP`-complete language, and paddable `NP`-complete languages are isomorphic ([Berman and Hartmanis][BermanHartmanis1975], §III, diff --git a/CslibFrontier/Computability/Complexity/Reduction/Nontrivial.lean b/CslibFrontier/Computability/Complexity/Reduction/Nontrivial.lean new file mode 100644 index 0000000000..3f256e5685 --- /dev/null +++ b/CslibFrontier/Computability/Complexity/Reduction/Nontrivial.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.Computability.Complexity.Reduction + +/-! +# Reductions from `P` to nontrivial problems + +Every problem in `P` polynomial-time reduces to every problem with a member and a nonmember: +decide membership, then output the member or the nonmember. So `P` lies below every nontrivial +problem in the polynomial-time many-one order, and under `P = NP` every nontrivial problem is +`NP`-hard. + +## Main results + +* `Cslib.Complexity.polyTimeReducible_of_mem_P`: every problem in `P` reduces to every problem + with a member and a nonmember. +-/ + +public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +/-- Every problem in `P` reduces to every problem with a member `b₁` and a nonmember `b₀`: +decide membership and output `b₁` or `b₀`. -/ +theorem polyTimeReducible_of_mem_P {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} + {A : Set α} {B : Set β} (hA : A ∈ P encA) {b₁ b₀ : β} (h₁ : b₁ ∈ B) (h₀ : b₀ ∉ B) : + PolyTimeReducible encA encB A B := by + obtain ⟨f, hf, hfA⟩ := hA + refine ⟨fun a => if f a then b₁ else b₀, hf.ite (.const b₁) (.const b₀), fun a => ?_⟩ + rw [hfA a] + cases hfa : f a + · simp only [hfa, Bool.false_eq_true, ↓reduceIte, h₀] + · simp only [hfa, ↓reduceIte, h₁] + +end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/Reduction/Turing.lean b/CslibFrontier/Computability/Complexity/Reduction/Turing.lean index 72d8b8d58f..1ceae64f51 100644 --- a/CslibFrontier/Computability/Complexity/Reduction/Turing.lean +++ b/CslibFrontier/Computability/Complexity/Reduction/Turing.lean @@ -12,6 +12,7 @@ public import CslibFrontier.Computability.Complexity.Classes.Inclusions public import CslibFrontier.Computability.Complexity.Classes.Oracle.Closure public import CslibFrontier.Computability.Complexity.Classes.Oracle.Lowness public import CslibFrontier.Computability.Complexity.Classes.Oracle.PolyTime +public import CslibFrontier.Computability.Complexity.Classes.Oracle.Substitution public import CslibFrontier.Computability.Complexity.Classes.PP.Closure public import CslibFrontier.Computability.Complexity.Classes.Space public import CslibFrontier.Computability.Complexity.Reduction @@ -23,7 +24,6 @@ import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import CslibFrontier.Computability.Machines.Turing.MultiTape.Encodings.Length import CslibFrontier.Tactic.EncLen -import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynomial.Automation /-! # Polynomial-time Turing reductions and the Turing bridge @@ -66,12 +66,9 @@ oracle for `B` within polynomial time [Ladner, Lynch and Selman][LadnerLynchSelm bounded, positive, disjunctive, and conjunctive truth-table reductions are Turing reductions (`≤_tt, ≤_{k-tt}, ≤_btt, ≤_ptt, ≤_dtt, ≤_ctt ⇒ ≤_T`). * `Cslib.Complexity.PolyTimeTuringReducible.refl`: reflexivity. -* `Cslib.Complexity.ComputableInPolyTimeWithOracle.of_mem_PWithOracle`, - `Cslib.Complexity.PWithOracle_subset_of_mem_PWithOracle`, - `Cslib.Complexity.NPWithOracle_subset_of_mem_PWithOracle`: oracle substitution when the oracle - language itself belongs to `P^O`. * `Cslib.Complexity.PolyTimeTuringReducible.mem_PWithOracle`: `P^O` is closed under Turing - reductions to word languages. + reductions to word languages, by oracle substitution + (`Cslib.Complexity.PWithOracle_subset_of_mem_PWithOracle`). * `Cslib.Complexity.PolyTimeTuringReducible.trans`: transitivity of polynomial-time Turing reductions through word languages (`≤_T ∘ ≤_T ⇒ ≤_T`). * `Cslib.Complexity.PolyTimeReducible.trans_turing`: pre-composition with a many-one reduction @@ -307,150 +304,7 @@ theorem PolyTimeCTTReducible.polyTimeTuringReducible PolyTimeTuringReducible encA encB A B := h.polyTimeTruthTableReducible.polyTimeTuringReducible -/-! ### Oracle substitution and transitivity of Turing reductions -/ - -/-- One simulated instruction of a finite oracle machine `machine` when each query to its oracle is -answered by running the deterministic oracle program `prog`. -/ -private def oracleAnswerStep {k : ℕ} {Control : Type} - (machine : Turing.MultiTapePTM k Bool Control Unit) - (prog : List Bool → WordQueryComp Unit Bool) - (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : - WordQueryComp Unit (Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) := - if (machine.pendingQuery cfg).isSome then - (fun b => machine.receiveBit (cfg, b)) <$> prog (machine.pendingRequest cfg) - else - pure (machine.localStep cfg) - -private theorem interpret_oracleAnswerStep {k : ℕ} {Control : Type} - (machine : Turing.MultiTapePTM k Bool Control Unit) - (prog : List Bool → WordQueryComp Unit Bool) - (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : - OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg) = - if (machine.pendingQuery cfg).isSome then - (fun b => machine.receiveBit (cfg, b)) <$> - OracleComp.interpret ProbOracleComp.query (prog (machine.pendingRequest cfg)) - else - pure (machine.localStep cfg) := by - unfold oracleAnswerStep - split <;> simp [OracleComp.interpret_map] - -private theorem isOraclePPTOn_oracleAnswerStep {k : ℕ} {Control : Type} [Finite Control] - (machine : Turing.MultiTapePTM k Bool Control Unit) - {prog : List Bool → WordQueryComp Unit Bool} - (hprog : Probability.IsOraclePPTOn encBits encBool - (fun w => OracleComp.interpret ProbOracleComp.query (prog w))) : - Probability.IsOraclePPTOn encFiniteConfig encFiniteConfig - (fun cfg => - OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg)) := by - simp only [interpret_oracleAnswerStep] - exact Probability.IsOraclePPTOn.cond' - ((ComputableInPolyTime.of_finite Option.isSome).comp machine.pendingQuery_pt) - ((hprog.preprocess' machine.pendingRequest_pt).map_with' - (f := fun cfg b => machine.receiveBit (cfg, b)) machine.receiveBit_pt) - machine.localStep_pt.isOraclePPTOn - -private theorem spaceBound_of_mem_support_oracleAnswerStep {k : ℕ} {Control : Type} - (machine : Turing.MultiTapePTM k Bool Control Unit) - (prog : List Bool → WordQueryComp Unit Bool) - {inputSize steps : ℕ} - {cfg next : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit} - (hcfg : Turing.MultiTapeMachine.FiniteConfig.SpaceBound inputSize steps 1 cfg) - (hnext : next ∈ OracleComp.support - (OracleComp.interpret ProbOracleComp.query (oracleAnswerStep machine prog cfg))) : - Turing.MultiTapeMachine.FiniteConfig.SpaceBound inputSize (steps + 1) 1 next := by - rw [interpret_oracleAnswerStep] at hnext - split_ifs at hnext with hq - · obtain ⟨b, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hnext - have hstep := machine.spaceBound_answerStep (fun _ => b) hcfg - rw [machine.answerStep_bit (fun _ => b)] at hstep - simpa [hq] using hstep - · rw [OracleComp.eq_of_mem_supportWith_pure hnext] - have hstep := machine.spaceBound_answerStep (fun _ => false) hcfg - rw [machine.answerStep_bit (fun _ => false)] at hstep - simpa [hq] using hstep - -private theorem interpret_id_oracleAnswerStep {k : ℕ} {Control : Type} - (machine : Turing.MultiTapePTM k Bool Control Unit) - {prog : List Bool → WordQueryComp Unit Bool} {O : Set (List Bool)} {g : List Bool → Bool} - (hg : ∀ w, OracleComp.interpret (m := Id) (languageOracle O) (prog w) = g w) - (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) : - OracleComp.interpret (m := Id) (languageOracle O) (oracleAnswerStep machine prog cfg) = - machine.answerStep (fun q => [g q.2]) cfg := by - rw [machine.answerStep_bit] - unfold oracleAnswerStep - split_ifs with hq - · rw [OracleComp.interpret_map, hg] - rfl - · rfl - -open Classical in -/-- **Oracle substitution for polynomial-time Boolean computations**: if an oracle language `O₁` -belongs to `P^{O₂}` and `f : α → Bool` is computable in polynomial time relative to `O₁`, then -`f` is computable in polynomial time relative to `O₂`. -/ -theorem ComputableInPolyTimeWithOracle.of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} {f : α → Bool} - (hO₁ : O₁ ∈ PWithOracle O₂ encBits) - (hf : ComputableInPolyTimeWithOracle O₁ f encA encBool) : - ComputableInPolyTimeWithOracle O₂ f encA encBool := by - obtain ⟨g, ⟨prog, hprog, hg⟩, hgO₁⟩ := hO₁ - have hg' : g = fun w => decide (w ∈ O₁) := funext fun w => - Bool.eq_iff_iff.mpr ⟨fun h => decide_eq_true ((hgO₁ w).mpr h), - fun h => (hgO₁ w).mp (of_decide_eq_true h)⟩ - subst hg' - obtain ⟨program, hcert, hprogram⟩ := hf - obtain ⟨k, m, machine, c, d, hrun⟩ := hcert.exists_fin_run_pure_false - obtain ⟨cf, hcf⟩ := length_encFiniteConfig_le (k := k) (State := Fin m) (Oracle := Unit) - have hcount : ComputableInPolyTime (fun a => c * ((encA a).length + 1) ^ d) encA - encUnary := - ((ComputableInPolyTime.unary_eval (Polynomial.C c * (Polynomial.X + 1) ^ d)).comp - (ComputableInPolyTime.encoding_length encA)).of_enc_eq fun a => by simp - have hinit : ComputableInPolyTime - (fun a => Turing.MultiTapeMachine.FiniteConfig.init (k := k) (Oracle := Unit) - machine.initial (encA a)) - encA encFiniteConfig := by - refine (((ComputableInPolyTime.of_eq fun _ => rfl : - ComputableInPolyTime encA encA encBits).prod - (ComputableInPolyTime.const (encOut := - encPair (encFinite (Option (Fin m))) - (encPair encUnary (encPair (encPi (Index := Fin k) (encBiTape encBool)) encBits))) - (some machine.initial, 1, fun _ => Cslib.Turing.BiTape.nil, []))).prod - (ComputableInPolyTime.const - (encOut := encPi (Index := Unit) (encPair encBits (encBiTape encBool))) - fun _ : Unit => ([], Cslib.Turing.BiTape.nil))).of_enc_eq fun a => ?_ - simp [Turing.MultiTapeMachine.FiniteConfig.init, Turing.FiniteCfg.init] - have hbound : PolyBounded (fun a => (encA a).length) - (fun a => cf * ((encA a).length + c * ((encA a).length + 1) ^ d + 1 + 1)) := by growth_poly - have hit := (Probability.IsOraclePPTOn.iterate_spec' hcount hinit - (isOraclePPTOn_oracleAnswerStep machine hprog) - (fun a i cfg => Turing.MultiTapeMachine.FiniteConfig.SpaceBound (encA a).length i 1 cfg) - (fun _ => Turing.MultiTapeMachine.FiniteConfig.spaceBound_init _ _ _) - (fun _ _ _ _ hinv _ hnext => - spaceBound_of_mem_support_oracleAnswerStep machine prog hinv hnext) - hbound - (fun _ _ _ hi hinv => (hcf _ _ _ _ hinv).trans (Nat.mul_le_mul_left cf (by omega)))).1 - refine ⟨fun a => (fun cfg => cfg.tapes.output.headD false) <$> - OracleComp.iterate (c * ((encA a).length + 1) ^ d) (oracleAnswerStep machine prog) - (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a)), ?_, fun a => ?_⟩ - · simp only [OracleComp.interpret_map, OracleComp.interpret_iterate] - exact hit.map' (by fun_prop) - · rw [OracleComp.interpret_map, OracleComp.interpret_id_iterate] - simp only [interpret_id_oracleAnswerStep machine hg] - change ((machine.answerStep (languageOracle O₁))^[c * ((encA a).length + 1) ^ d] - (Turing.MultiTapeMachine.FiniteConfig.init machine.initial (encA a))).tapes.output.headD - false = f a - rw [← machine.interpret_run_pure_false, hrun a (languageOracle O₁), ← hprogram a] - simp - -/-- If `O₁ ∈ P^{O₂}`, then `P^{O₁} ⊆ P^{O₂}`. -/ -theorem PWithOracle_subset_of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} - (hO₁ : O₁ ∈ PWithOracle O₂ encBits) (enc : α ↪ List Bool) : - PWithOracle O₁ enc ⊆ PWithOracle O₂ enc := - fun _ ⟨f, hf, hL⟩ => ⟨f, hf.of_mem_PWithOracle hO₁, hL⟩ - -/-- If `O₁ ∈ P^{O₂}`, then `NP^{O₁} ⊆ NP^{O₂}`. -/ -theorem NPWithOracle_subset_of_mem_PWithOracle {O₁ O₂ : Set (List Bool)} - (hO₁ : O₁ ∈ PWithOracle O₂ encBits) (enc : α ↪ List Bool) : - NPWithOracle O₁ enc ⊆ NPWithOracle O₂ enc := - fun _ ⟨p, V, hV, hL⟩ => ⟨p, V, hV.of_mem_PWithOracle hO₁, hL⟩ +/-! ### Transitivity of Turing reductions -/ /-- **`P` relative to an oracle is closed under polynomial-time Turing reductions to word languages.** -/