Fine-grained hypotheses and reductions on short words

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

definition

Loading review…

Natural Language Statement

Definition

The hypotheses of fine-grained complexity, stated in the style of the exponential time hypothesis ( $Results.ETH$ ): on the word RAM of lax-808846, with short words, $\ell \ge c \log_2(|u| + M + 2)$ for the input $u$ with largest number $M$ , so that a program cannot pack many numbers into one word. Each is about an explicit problem on words. Problems with numbers have them polynomial in the input size, as the literature states these conjectures.

SETH: for every $\varepsilon > 0$ there is $k$ such that no program decides the satisfiability of formulas with clauses of at most $k$ literals over $n$ variables within $c\,2^{(1-\varepsilon)n}(|w|+1)^c$ instructions.
Orthogonal vectors: given $n$ and $d$ and two lists of $n$ vectors in $\{0,1\}^d$ , is some vector of the first list orthogonal to some of the second? For every $\varepsilon > 0$ there is $a$ such that with $d \le a \log_2 n$ no program decides it within $c\,n^{2-\varepsilon}$ .
3SUM: given $n$ integers of absolute value at most $n^3$ , do three of them (at different positions) sum to $0$ ? No program decides it within $c\,n^{2-\varepsilon}$ , for any $\varepsilon > 0$ .
APSP: given a complete directed graph on $n$ vertices with integer arc lengths of absolute value at most $n^3$ and no negative cycle, write the matrix of shortest distances; no program does so within $c\,n^{3-\varepsilon}$ .
Min-plus convolution: given two lists of $n$ integers of absolute value at most $n^3$ , write $c_k = \min_{i+j=k}(a_i + b_j)$ ; no program does so within $c\,n^{2-\varepsilon}$ .
$k$ -Clique: with $\omega$ the infimum of the exponents $e$ such that a program multiplies $n \times n$ matrices of integers of absolute value at most $n$ within $c\,n^e$ instructions, for every $k \ge 3$ and $\varepsilon > 0$ no program decides whether a graph on $n$ vertices has $k$ pairwise adjacent vertices within $c\,n^{(\omega/3-\varepsilon)k}$ .

Integers are written as sign and absolute value; vectors, lists and matrices entry by entry after their sizes; a graph as $n$ and its adjacency matrix.

A fine-grained reduction from a problem on words to another is one program that maps the words of the first to words of the second, keeps the answer, runs within $c\,(T(u) + 1)$ instructions on short words, and writes no number above $N(u)$ , so that the word length on the target side is known.

Concept map

26 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax434175.Results
2
3	/-!
4	---
5	title: Fine-grained hypotheses and reductions on short words
6	type: definition
7	---
8	The hypotheses of fine-grained complexity, stated in the style of the
9	exponential time hypothesis (`Results.ETH`): on the word RAM of lax-808846, with
10	short words, $\ell \ge c \log_2(\|u\| + M + 2)$ for the input $u$ with largest
11	number $M$ , so that a program cannot pack many numbers into one word. Each is
12	about an explicit problem on words. Problems with numbers have them polynomial in
13	the input size, as the literature states these conjectures.
14
15	- SETH: for every $\varepsilon > 0$ there is $k$ such that no program decides
16	the satisfiability of formulas with clauses of at most $k$ literals over $n$
17	variables within $c\,2^{(1-\varepsilon)n}(\|w\|+1)^c$ instructions.
18	- Orthogonal vectors: given $n$ and $d$ and two lists of $n$ vectors in
19	$\{0,1\}^d$ , is some vector of the first list orthogonal to some of the
20	second? For every $\varepsilon > 0$ there is $a$ such that with $d \le a \log_2 n$
21	no program decides it within $c\,n^{2-\varepsilon}$ .
22	- 3SUM: given $n$ integers of absolute value at most $n^3$ , do three of them
23	(at different positions) sum to $0$ ? No program decides it within
24	$c\,n^{2-\varepsilon}$ , for any $\varepsilon > 0$ .
25	- APSP: given a complete directed graph on $n$ vertices with integer arc
26	lengths of absolute value at most $n^3$ and no negative cycle, write the
27	matrix of shortest distances; no program does so within $c\,n^{3-\varepsilon}$ .
28	- Min-plus convolution: given two lists of $n$ integers of absolute value
29	at most $n^3$ , write $c_k = \min_{i+j=k}(a_i + b_j)$ ; no program does so within
30	$c\,n^{2-\varepsilon}$ .
31	- $k$ -Clique: with $\omega$ the infimum of the exponents $e$ such that a
32	program multiplies $n \times n$ matrices of integers of absolute value at most
33	$n$ within $c\,n^e$ instructions, for every $k \ge 3$ and $\varepsilon > 0$ no
34	program decides whether a graph on $n$ vertices has $k$ pairwise adjacent
35	vertices within $c\,n^{(\omega/3-\varepsilon)k}$ .
36
37	Integers are written as sign and absolute value; vectors, lists and matrices
38	entry by entry after their sizes; a graph as $n$ and its adjacency matrix.
39
40	A fine-grained reduction from a problem on words to another is one program
41	that maps the words of the first to words of the second, keeps the answer, runs
42	within $c\,(T(u) + 1)$ instructions on short words, and writes no number above
43	$N(u)$ , so that the word length on the target side is known.
44	-/
45
46	namespace Lax434175.FineGrained
47	open Lax434175.Results Lax808846.Ram
48	open Classical
49
50	open Classical in
51	/-- One program decides the words of `dom` against `L` within `c (T w + 1)`
52	instructions at every short word length. -/
53	def DecidesIn (dom : Set (List ℕ)) (L : List ℕ → Prop) (T : List ℕ → ℝ) (p : Program) (c : ℕ) :
54	Prop :=
55	∀ w ∈ dom, ∀ ℓ, WordOk c w ℓ → ∃ t : ℕ, (t : ℝ) ≤ c * (T w + 1) ∧
56	RunsTo ℓ p (w.length :: w) (if L w then [1] else [0]) t
57
58	/-- One program writes `F w` for the words of `dom` within `c (T w + 1)`
59	instructions at every short word length. -/
60	def ComputesIn (dom : Set (List ℕ)) (F : List ℕ → List ℕ) (T : List ℕ → ℝ) (p : Program) (c : ℕ) :
61	Prop :=
62	∀ w ∈ dom, ∀ ℓ, WordOk c w ℓ → ∃ t : ℕ, (t : ℝ) ≤ c * (T w + 1) ∧ RunsTo ℓ p (w.length :: w) (F w) t
63
64	/-- An integer as sign and absolute value. -/
65	def int (z : ℤ) : List ℕ := [if z < 0 then 1 else 0, z.natAbs]
66
67	-- SETH
68
69	/-- The words of formulas on `n` variables with clauses of at most `k` literals. -/
70	def kCNF (k : ℕ) : Set (List ℕ) :=
71	{w \| ∃ n Φ, w = formulaWord n Φ ∧ ∀ C ∈ Φ, C.length ≤ k ∧ ∀ l ∈ C, l.index < n}
72
73	/-- The number of variables a formula word announces. -/
74	def vars (w : List ℕ) : ℕ := w.headD 0
75
76	/-- The strong exponential time hypothesis. -/
77	def SETH : Prop :=
78	∀ ε : ℝ, 0 < ε → ∃ k : ℕ, ∀ (p : Program) (c : ℕ),
79	¬ DecidesIn (kCNF k)
80	(fun w => ∃ n Φ, w = formulaWord n Φ ∧ Lax429075.CNF.Satisfiable Φ)
81	(fun w => (2 : ℝ) ^ ((1 - ε) * vars w) * (w.length + 1 : ℝ) ^ c) p c
82
83	-- Orthogonal vectors
84
85	/-- The word of an instance of orthogonal vectors. -/
86	def ovWord (n d : ℕ) (A B : Fin n → Fin d → Bool) : List ℕ :=
87	[n, d] ++ (List.ofFn fun i => List.ofFn fun k => if A i k then 1 else 0).flatten ++
88	(List.ofFn fun i => List.ofFn fun k => if B i k then 1 else 0).flatten
89
90	/-- The words of instances with `d ≤ a log₂ n`. -/
91	def OVWords (a : ℕ) : Set (List ℕ) :=
92	{w \| ∃ n d A B, w = ovWord n d A B ∧ d ≤ a * Nat.log 2 n}
93
94	/-- The orthogonal vectors hypothesis. -/
95	def OVH : Prop :=
96	∀ ε : ℝ, 0 < ε → ∃ a : ℕ, ∀ (p : Program) (c : ℕ),
97	¬ DecidesIn (OVWords a)
98	(fun w => ∃ n d A B, w = ovWord n d A B ∧ ∃ i j, ∀ k, A i k = false ∨ B j k = false)
99	(fun w => (w.headD 0 : ℝ) ^ (2 - ε)) p c
100
101	-- 3SUM
102
103	/-- The word of a list of integers. -/
104	def intsWord {n : ℕ} (a : Fin n → ℤ) : List ℕ := n :: (List.ofFn fun i => int (a i)).flatten
105
106	/-- The words of `n` integers of absolute value at most `n³`. -/
107	def SmallInts : Set (List ℕ) :=
108	{w \| ∃ (n : ℕ) (a : Fin n → ℤ), w = intsWord a ∧ ∀ i, (a i).natAbs ≤ n ^ 3}
109
110	/-- The 3SUM hypothesis. -/
111	def ThreeSumH : Prop :=
112	∀ ε : ℝ, 0 < ε → ∀ (p : Program) (c : ℕ),
113	¬ DecidesIn SmallInts
114	(fun w => ∃ (n : ℕ) (a : Fin n → ℤ), w = intsWord a ∧
115	∃ i j k, i ≠ j ∧ j ≠ k ∧ i ≠ k ∧ a i + a j + a k = 0)
116	(fun w => (w.headD 0 : ℝ) ^ (2 - ε)) p c
117
118	-- APSP
119
120	/-- The word of a complete directed graph with arc lengths. -/
121	def graphWord {n : ℕ} (len : Fin n → Fin n → ℤ) : List ℕ :=
122	n :: (List.ofFn fun i => (List.ofFn fun j => int (len i j)).flatten).flatten
123
124	/-- The length of a walk given by its list of vertices. -/
125	def walkLength {n : ℕ} (len : Fin n → Fin n → ℤ) : List (Fin n) → ℤ
126	\| a :: b :: rest => len a b + walkLength len (b :: rest)
127	\| _ => 0
128
129	/-- `δ` is the matrix of shortest distances: every walk from `i` to `j` is at
130	least `δ i j` long, and one has that length. -/
131	def Distances {n : ℕ} (len : Fin n → Fin n → ℤ) (δ : Fin n → Fin n → ℤ) : Prop :=
132	∀ i j, (∀ W : List (Fin n), W.head? = some i → W.getLast? = some j → δ i j ≤ walkLength len W) ∧
133	∃ W : List (Fin n), W.head? = some i ∧ W.getLast? = some j ∧ walkLength len W = δ i j
134
135	/-- No cycle has negative length. -/
136	def NoNegativeCycle {n : ℕ} (len : Fin n → Fin n → ℤ) : Prop :=
137	∀ W : List (Fin n), W.head? = W.getLast? → 0 ≤ walkLength len W
138
139	/-- The APSP hypothesis: no program writes the distance matrix within
140	`c n^{3-ε}`, for any function that writes it on the instances. -/
141	def APSPH : Prop :=
142	∀ ε : ℝ, 0 < ε → ∀ (p : Program) (c : ℕ) (F : List ℕ → List ℕ),
143	(∀ n (len : Fin n → Fin n → ℤ), NoNegativeCycle len → (∀ i j, (len i j).natAbs ≤ n ^ 3) →
144	∃ δ, Distances len δ ∧ F (graphWord len) = (List.ofFn fun i => (List.ofFn fun j =>
145	int (δ i j)).flatten).flatten) →
146	¬ ComputesIn {w \| ∃ (n : ℕ) (len : Fin n → Fin n → ℤ), w = graphWord len ∧ NoNegativeCycle len ∧
147	∀ i j, (len i j).natAbs ≤ n ^ 3} F (fun w => (w.headD 0 : ℝ) ^ (3 - ε)) p c
148
149	-- Min-plus convolution
150
151	/-- The word of two lists of `n` integers. -/
152	def pairWord {n : ℕ} (a b : Fin n → ℤ) : List ℕ :=
153	n :: (List.ofFn fun i => int (a i)).flatten ++ (List.ofFn fun i => int (b i)).flatten
154
155	/-- The min-plus convolution of two lists of `n ≥ 1` integers, entries `0` to `2n - 2`. -/
156	def minPlus {n : ℕ} (a b : Fin n → ℤ) (k : ℕ) : ℤ :=
157	((Finset.univ.filter fun p : Fin n × Fin n => p.1.val + p.2.val = k).image
158	fun p => a p.1 + b p.2).min.getD 0
159
160	/-- The min-plus convolution hypothesis. -/
161	def MinPlusH : Prop :=
162	∀ ε : ℝ, 0 < ε → ∀ (p : Program) (c : ℕ),
163	¬ ComputesIn {w \| ∃ (n : ℕ) (a b : Fin n → ℤ), w = pairWord a b ∧
164	∀ i, (a i).natAbs ≤ n ^ 3 ∧ (b i).natAbs ≤ n ^ 3}
165	(fun w => (List.ofFn fun k : Fin (2 * w.headD 0 - 1) => int (if h : ∃ (n : ℕ) (a b : Fin n → ℤ),
166	w = pairWord a b then minPlus h.choose_spec.choose h.choose_spec.choose_spec.choose k
167	else 0)).flatten)
168	(fun w => (w.headD 0 : ℝ) ^ (2 - ε)) p c
169
170	-- k-Clique
171
172	/-- The word of a square matrix of integers. -/
173	def matrixWord {n : ℕ} (A : Fin n → Fin n → ℤ) : List ℕ :=
174	n :: (List.ofFn fun i => (List.ofFn fun j => int (A i j)).flatten).flatten
175
176	/-- The exponents `e` of matrix multiplication: one program writes the product
177	of two `n × n` matrices with entries of absolute value at most `n` within
178	`c n^e` instructions. -/
179	def MultipliesIn (e : ℝ) : Prop :=
180	∃ (p : Program) (c : ℕ), ComputesIn
181	{w \| ∃ (n : ℕ) (A B : Fin n → Fin n → ℤ), w = matrixWord A ++ (matrixWord B).tail ∧
182	∀ i j, (A i j).natAbs ≤ n ∧ (B i j).natAbs ≤ n}
183	(fun w => if h : ∃ (n : ℕ) (A B : Fin n → Fin n → ℤ), w = matrixWord A ++ (matrixWord B).tail then
184	matrixWord fun i j => ∑ k, h.choose_spec.choose i k * h.choose_spec.choose_spec.choose k j
185	else [])
186	(fun w => (w.headD 0 : ℝ) ^ e) p c
187
188	/-- The exponent `ω` of matrix multiplication on the word RAM. -/
189	noncomputable def omega : ℝ := sInf {e \| MultipliesIn e}
190
191	/-- The word of a graph: `n` and its adjacency matrix. -/
192	def adjWord {n : ℕ} (G : Fin n → Fin n → Bool) : List ℕ :=
193	n :: (List.ofFn fun i => List.ofFn fun j => if G i j then 1 else 0).flatten
194
195	/-- The `k`-clique hypothesis. -/
196	def KCliqueH : Prop :=
197	∀ k : ℕ, 3 ≤ k → ∀ ε : ℝ, 0 < ε → ∀ (p : Program) (c : ℕ),
198	¬ DecidesIn {w \| ∃ (n : ℕ) (G : Fin n → Fin n → Bool), w = adjWord G ∧ ∀ i j, G i j = G j i}
199	(fun w => ∃ (n : ℕ) (G : Fin n → Fin n → Bool), w = adjWord G ∧
200	∃ S : Finset (Fin n), S.card = k ∧ ∀ i ∈ S, ∀ j ∈ S, i ≠ j → G i j = true)
201	(fun w => (w.headD 0 : ℝ) ^ ((omega / 3 - ε) * k)) p c
202
203	-- Reductions
204
205	/-- A fine-grained reduction: one program maps the words of `dom` to words of
206	`dom'`, keeps the answer, runs within `c (T u + 1)` instructions on short words,
207	and writes no number above `N u`. -/
208	def FineReduces (dom dom' : Set (List ℕ)) (L L' : List ℕ → Prop) (T : List ℕ → ℝ)
209	(N : List ℕ → ℕ) : Prop :=
210	∃ (f : List ℕ → List ℕ) (p : Program) (c : ℕ), ComputesIn dom f T p c ∧
211	∀ u ∈ dom, f u ∈ dom' ∧ (L u ↔ L' (f u)) ∧ maxEntry (f u) ≤ N u
212
213	end Lax434175.FineGrained
214

Builds on

Lax434175.Results

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

Fine-grained hypotheses and reductions on short words

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments