Complexity classes along special cases

Lax434175.ComplexityClasses · concepts/Lax434175/ComplexityClasses.lean · lax-434175

proven

Loading review…

Natural Language Statement

Theorem

The classes are those of the word RAM, for parameterized problems on words: a set of admissible words, the yes-instances among them, and a parameter.

P: one program decides the problem in polynomial time on its admissible words.
NP-hard: every language in NP, written as words of zeros and ones, reduces to the problem in polynomial time on admissible words.
FPT, W[t] and hardness for a class are those of the registered W-hierarchy (lax-496464).
XP: one program decides the problem within $(|x|+2)^{f(k)}$ instructions for a computable $f$ , where $|x|$ is the bit size of the word and $k$ its parameter.
para-NP-hard: the problem restricted to the words of parameter at most some $k$ is NP-hard.

A problem $A$ refines a problem $B$ if every admissible word of $A$ is one of $B$ , with the same answer and the same parameter.

Theorem. If $A$ refines $B$ , then $B$ in P, FPT or XP puts $A$ there, and $A$ NP-hard, para-NP-hard or hard for a class of parameterized problems makes $B$ so.

Theorem. For a coding of a family of scheduling problems with sound fields, the problem of a field-wise special case $s$ of $t$ refines that of $t$ , for every parameter of the kernel instance and every invariant parameter of a constraint field.

Concept map

21 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	import Lax434930.NondeterministicPolynomialTime
2	import Lax496464.WH_B4_Hierarchies
3	import Lax434175.WordProblems
4
5	/-!
6	---
7	title: Complexity classes along special cases
8	type: theorem
9	---
10	The classes are those of the word RAM, for parameterized problems on words: a
11	set of admissible words, the yes-instances among them, and a parameter.
12
13	- P: one program decides the problem in polynomial time on its
14	admissible words.
15	- NP-hard: every language in NP, written as words of zeros and ones,
16	reduces to the problem in polynomial time on admissible words.
17	- FPT, W[t] and hardness for a class are those of the registered
18	W-hierarchy (lax-496464).
19	- XP: one program decides the problem within $(\|x\|+2)^{f(k)}$
20	instructions for a computable $f$ , where $\|x\|$ is the bit size of the word
21	and $k$ its parameter.
22	- para-NP-hard: the problem restricted to the words of parameter at most
23	some $k$ is NP-hard.
24
25	A problem $A$ refines a problem $B$ if every admissible word of $A$ is one of
26	$B$ , with the same answer and the same parameter.
27
28	Theorem. If $A$ refines $B$ , then $B$ in P, FPT or XP puts $A$ there,
29	and $A$ NP-hard, para-NP-hard or hard for a class of parameterized problems
30	makes $B$ so.
31
32	Theorem. For a coding of a family of scheduling problems with sound
33	fields, the problem of a field-wise special case $s$ of $t$ refines that of
34	$t$ , for every parameter of the kernel instance and every invariant parameter
35	of a constraint field.
36	-/
37
38	namespace Lax434175.ComplexityClasses
39	open Lax434175.Kernels Lax434175.Modules Lax434175.Assembly
40	open Lax434175.Parameters Lax434175.WordProblems
41	open Lax808846.Ram Lax759944.BinaryWordEncoding Lax759944.RamPolytime
42	open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime
43	open Lax496464.WH_A1_FptTime Lax496464.WH_A2_FptReductions
44	open Lax888481.ParameterizedComplexity (Problem)
45
46	/-- The answer a deciding program writes. -/
47	noncomputable def answer (P : Problem) (x : List ℕ) : List ℕ :=
48	open Classical in if P.Yes x then [1] else [0]
49
50	/-- `P` is in P. -/
51	def InP (P : Problem) : Prop := PolyTimeOn P.Domain (answer P)
52
53	/-- `P` reduces to `Q` in polynomial time on the admissible words of `P`. -/
54	def PolyReduces (P Q : Problem) : Prop := ∃ R, IsReduction P Q R ∧ PolyTimeOn P.Domain R
55
56	/-- A language of bit strings as a problem on words of zeros and ones. -/
57	def ofLanguage (A : Language) : Problem where
58	Domain := {x \| ∀ v ∈ x, v < 2}
59	Yes x := x.map (fun v => decide (v = 1)) ∈ A
60	param _ := 0
61
62	/-- `P` is NP-hard. -/
63	def NPHard (P : Problem) : Prop := ∀ A ∈ NP, PolyReduces (ofLanguage A) P
64
65	/-- On every admissible word, one program computes `F` within
66	`(bitSize x + 2) ^ f (κ x)` instructions, for a computable `f`. -/
67	def XPTimeOn (D : Set (List ℕ)) (κ : List ℕ → ℕ) (F : List ℕ → List ℕ) : Prop :=
68	∃ (p : Program) (f : ℕ → ℕ), Computable f ∧ ∀ x ∈ D,
69	FitsInWords ((bitSize x + 2) ^ f (κ x)) ((x.length :: x) ++ F x) ∧
70	∀ w : ℕ, (bitSize x + 2) ^ f (κ x) ≤ w →
71	∃ t ≤ (bitSize x + 2) ^ f (κ x), RunsTo w p (x.length :: x) (F x) t
72
73	/-- XP. -/
74	def XP : Set Problem := {P \| IsParameterized P ∧ XPTimeOn P.Domain P.param (answer P)}
75
76	/-- The words of parameter at most `k`. -/
77	def slice (P : Problem) (k : ℕ) : Problem where
78	Domain := {x \| x ∈ P.Domain ∧ P.param x ≤ k}
79	Yes := P.Yes
80	param := P.param
81
82	/-- `P` is para-NP-hard. -/
83	def ParaNPHard (P : Problem) : Prop := ∃ k, NPHard (slice P k)
84
85	/-- `A` refines `B`. -/
86	structure Refines (A B : Problem) : Prop where
87	domain : A.Domain ⊆ B.Domain
88	yes : ∀ x ∈ A.Domain, (A.Yes x ↔ B.Yes x)
89	param : ∀ x ∈ A.Domain, A.param x = B.param x
90
91	variable {A B : Problem}
92
93	axiom inP_of_refines : Refines A B → InP B → InP A
94	axiom fpt_of_refines : Refines A B → B ∈ FPT → A ∈ FPT
95	axiom xp_of_refines : Refines A B → B ∈ XP → A ∈ XP
96	axiom npHard_of_refines : Refines A B → NPHard A → NPHard B
97	axiom paraNPHard_of_refines : Refines A B → ParaNPHard A → ParaNPHard B
98	axiom hard_of_refines (𝒞 : Set Problem) : Refines A B → Hard 𝒞 A → Hard 𝒞 B
99
100	variable {K : Kernel} {F : Family K}
101
102	axiom refines_of_le_kernel (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
103	(κ : K.Inst → ℕ) :
104	Refines (wordProblem C s (ofKernel F κ s)) (wordProblem C t (ofKernel F κ t))
105
106	axiom refines_of_le_field (C : Coding F) (hF : F.Sound) {s t : Spec F} (h : s.le t)
107	(i : F.ModuleName) (κ : FieldParameter (F.module i)) (hκ : κ.Invariant) :
108	Refines (wordProblem C s (ofField F i κ s)) (wordProblem C t (ofField F i κ t))
109
110	end Lax434175.ComplexityClasses
111

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Complexity classes along special cases

Flags

Flag this concept

Natural Language Statement

Theorem

1 `fpt_of_refines` proven

2 `hard_of_refines` proven

3 `inP_of_refines` proven

4 `npHard_of_refines` proven

5 `paraNPHard_of_refines` proven

6 `refines_of_le_field` proven

7 `refines_of_le_kernel` proven

8 `xp_of_refines` proven

Lean source view on GitHub

Discussion

Settings