Polynomial-Time and Strict Reductions Are FPT-Reductions

Lax496464.WH_A5_Bridges · concepts/Lax496464/WH_A5_Bridges.lean · lax-496464

proven

Loading review…

Natural Language Statement

Theorem

Most reductions in parameterized complexity are computable in polynomial time, and many are already proved in the archive in one of the following forms. Each yields an fpt-reduction.

Runs of a program. A program that halts with the correct output within a fixed-parameter bound $B$ at every word length from $B$ on, and writes numbers of at most $B$ bits, computes the function in fixed-parameter time. This is the form in which a program verified in the archive's IMP+ language arrives, run on the tape $x.length :: x$ .
Polynomial time on the word RAM. On the set of all words, polynomial time in the sense of $WH_A1_FptTime$ is $Lax759944.RamPolytime.RamPolytime$ . A polynomial-time reduction whose parameter is bounded by a computable function of the old one is an fpt-reduction.
Polynomial time on a Turing machine ( $Lax759944.TuringPolytime.TuringPolytime$ ), by the archive's equivalence of the two machine models.
The archive's strict fpt-reductions ( $Lax888481.ParameterizedComplexity.IsFptReduction$ , time $c\,g(k)\,(|x|+1)$ on the tape $x$ ), when $g$ and $h$ are computable and the output entries have fixed-parameter bit length; likewise the archive's strict fpt-algorithms.

Concept map

9 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Lax496464.WH_A2_FptReductions
2	import Lax759944.TuringPolytime
3
4	/-!
5	---
6	title: Polynomial-Time and Strict Reductions Are FPT-Reductions
7	type: theorem
8	---
9	Most reductions in parameterized complexity are computable in polynomial time, and many are
10	already proved in the archive in one of the following forms. Each yields an fpt-reduction.
11
12	1. Runs of a program. A program that halts with the correct output within a fixed-parameter
13	bound $B$ at every word length from $B$ on, and writes numbers of at most $B$ bits, computes the
14	function in fixed-parameter time. This is the form in which a program verified in the archive's
15	IMP+ language arrives, run on the tape `x.length :: x`.
16	2. Polynomial time on the word RAM. On the set of all words, polynomial time in the sense of
17	`WH_A1_FptTime` is `Lax759944.RamPolytime.RamPolytime`. A polynomial-time reduction whose parameter
18	is bounded by a computable function of the old one is an fpt-reduction.
19	3. Polynomial time on a Turing machine (`Lax759944.TuringPolytime.TuringPolytime`), by the
20	archive's equivalence of the two machine models.
21	4. The archive's strict fpt-reductions (`Lax888481.ParameterizedComplexity.IsFptReduction`,
22	time $c\,g(k)\,(\|x\|+1)$ on the tape $x$ ), when $g$ and $h$ are computable and the output entries
23	have fixed-parameter bit length; likewise the archive's strict fpt-algorithms.
24
25	# Formalization Notes
26
27	Output entries in the strict case. The strict definition bounds the running time but not the
28	size of the numbers written: a program that repeatedly squares a number writes, in $m$ steps, a
29	number of $2^m$ bits. Such an output cannot be read by a further reduction in fixed-parameter time.
30	The hypothesis `hout` excludes this; it holds for every reduction whose output numbers are
31	polynomially bounded in its input numbers.
32
33	Tapes. The strict notion gives the program the word $x$ , the polynomial-time notions the word
34	`x.length :: x`; a program for one tape is converted into one for the other with constant
35	overhead.
36	-/
37
38	namespace Lax496464.WH_A5_Bridges
39
40	open Lax808846.Ram Lax808846.RamComputes Lax759944.BinaryWordEncoding
41	open Lax759944.RamPolytime Lax759944.TuringPolytime
42	open Lax888481.ParameterizedComplexity (Problem Fits Decides)
43	open Lax496464.WH_A1_FptTime Lax496464.WH_A2_FptReductions
44
45	/-- On all words, polynomial time is the archive's polynomial time on the word RAM. -/
46	axiom polyTimeOn_univ_iff (F : List ℕ → List ℕ) : PolyTimeOn Set.univ F ↔ RamPolytime F
47
48	/-- From runs on the machine. A program that, on the tape `x.length :: x` of every word `x` of
49	`D`, halts with output `F x` within `B = f(κ x) · (\|x\| + 1)^d` steps at every word length `w ≥ B`,
50	writing only numbers below `2 ^ B`, computes `F` in fixed-parameter time. -/
51	axiom fptTimeOn_of_runsTo {D : Set (List ℕ)} {κ : List ℕ → ℕ} {F : List ℕ → List ℕ}
52	{p : Program} {f : ℕ → ℕ} {d : ℕ} (hf : Computable f)
53	(hrun : ∀ x ∈ D, ∀ w : ℕ, fptBound f d (κ x) (bitSize x) ≤ w →
54	∃ t ≤ fptBound f d (κ x) (bitSize x), RunsTo w p (x.length :: x) (F x) t)
55	(hout : ∀ x ∈ D, ∀ v ∈ F x, v < 2 ^ fptBound f d (κ x) (bitSize x)) :
56	FptTimeOn D κ F
57
58	/-- From runs on the machine, polynomial version: the same with the bound `c · (\|x\| + 1)^d`. -/
59	axiom polyTimeOn_of_runsTo {D : Set (List ℕ)} {F : List ℕ → List ℕ} {p : Program} {c d : ℕ}
60	(hrun : ∀ x ∈ D, ∀ w : ℕ, c * (bitSize x + 1) ^ d ≤ w →
61	∃ t ≤ c * (bitSize x + 1) ^ d, RunsTo w p (x.length :: x) (F x) t)
62	(hout : ∀ x ∈ D, ∀ v ∈ F x, v < 2 ^ (c * (bitSize x + 1) ^ d)) :
63	PolyTimeOn D F
64
65	/-- A polynomial-time computation on the word RAM is polynomial time on every set of inputs. -/
66	axiom polyTimeOn_of_ramPolytime {F : List ℕ → List ℕ} (D : Set (List ℕ)) :
67	RamPolytime F → PolyTimeOn D F
68
69	/-- A polynomial-time computation on a Turing machine is polynomial time on every set of inputs. -/
70	axiom polyTimeOn_of_turingPolytime {F : List ℕ → List ℕ} (D : Set (List ℕ)) :
71	TuringPolytime F → PolyTimeOn D F
72
73	/-- A polynomial-time reduction with a computably bounded parameter is an fpt-reduction. -/
74	axiom fptReduces_of_polyTime {P Q : Problem} {R : List ℕ → List ℕ} :
75	IsReduction P Q R → ParamBounded P Q R → PolyTimeOn P.Domain R → P ≤ᶠᵖᵗ Q
76
77	/-- A computation in the archive's strict linear fixed-parameter time, with a computable time factor
78	and outputs of fixed-parameter bit length, is a fixed-parameter computation. -/
79	axiom fptTimeOn_of_strict {D : Set (List ℕ)} {κ : List ℕ → ℕ} {F : List ℕ → List ℕ}
80	{prog : Program} {c : ℕ} {g : ℕ → ℕ} (hg : Computable g)
81	(htime : ∀ w : ℕ, ComputesInTime w prog {x \| x ∈ D ∧ Fits c w x ∧ Fits c w (F x)} F
82	fun x => c * g (κ x) * (x.length + 1))
83	(hout : ∃ (e : ℕ → ℕ) (d : ℕ), Computable e ∧
84	∀ x ∈ D, ∀ v ∈ F x, v < 2 ^ (e (κ x) * (bitSize x + 1) ^ d)) :
85	FptTimeOn D κ F
86
87	/-- A strict fpt-reduction of the archive with computable functions and outputs of
88	fixed-parameter bit length is an fpt-reduction. -/
89	axiom fptReduces_of_strict {P Q : Problem} {R : List ℕ → List ℕ} {prog : Program} {c : ℕ}
90	{g h : ℕ → ℕ} (hr : Lax888481.ParameterizedComplexity.IsFptReduction P Q R prog c g h)
91	(hg : Computable g) (hh : Computable h)
92	(hout : ∃ (e : ℕ → ℕ) (d : ℕ), Computable e ∧
93	∀ x ∈ P.Domain, ∀ v ∈ R x, v < 2 ^ (e (P.param x) * (bitSize x + 1) ^ d)) :
94	P ≤ᶠᵖᵗ Q
95
96	/-- A strict fpt-algorithm of the archive with a computable time factor puts a parameterized
97	problem into FPT. -/
98	axiom mem_FPT_of_decides {P : Problem} {prog : Program} {c : ℕ} {g : ℕ → ℕ}
99	(hP : IsParameterized P) (hg : Computable g) (hd : Decides P prog c g) : P ∈ FPT
100
101	end Lax496464.WH_A5_Bridges
102

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Formalization Notes

Output entries in the strict case. The strict definition bounds the running time but not the size of the numbers written: a program that repeatedly squares a number writes, in $m$ steps, a number of $2^m$ bits. Such an output cannot be read by a further reduction in fixed-parameter time. The hypothesis $hout$ excludes this; it holds for every reduction whose output numbers are polynomially bounded in its input numbers.

Tapes. The strict notion gives the program the word $x$ , the polynomial-time notions the word $x.length :: x$ ; a program for one tape is converted into one for the other with constant overhead.

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

Polynomial-Time and Strict Reductions Are FPT-Reductions

Flags

Flag this concept

Natural Language Statement

Theorem

1 `fptReduces_of_polyTime` proven

2 `fptReduces_of_strict` proven

3 `fptTimeOn_of_runsTo` proven

4 `fptTimeOn_of_strict` proven

5 `mem_FPT_of_decides` proven

6 `polyTimeOn_of_ramPolytime` proven

7 `polyTimeOn_of_runsTo` proven

8 `polyTimeOn_of_turingPolytime` proven

9 `polyTimeOn_univ_iff` proven

Lean source view on GitHub

Discussion

Settings