The Decision Problems as Languages

Lax117284.Problems · concepts/Lax117284/Problems.lean · lax-117284

proven

Loading review…

Natural Language Statement

Definition

Instances as binary words, the representation against which classical complexity measures running time, and the two decision problems as languages of such words.

A natural number is written as its binary digits preceded by their number in unary, which makes the code self-delimiting. An instance is the number of clients, the number of days, and then, day by day and client by client, the processing time and the due date of that client's job on that day. An instance of $1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ appends the fairness parameter $k$ ; an instance of $1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ appends one parameter per client.

The language of the problem consists of the words encoding an instance and a parameter for which a fair schedule exists. Every complexity claim of the source concerns a class of instances — those with day-independent due dates, those whose fairness parameter is $m-1$ , those whose overall conflict graph has small treewidth — so the language is taken relative to such a class: a word belongs to it if it encodes an instance in the class, together with a parameter, that admits a fair schedule. A language is NP-hard if every language in NP reduces to it in polynomial time.

Concept map

6 concepts; 14 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Lax117284.Scheduling
2	import Lax429075.Reductions
3	import Mathlib.Data.List.FinRange
4	import Mathlib.Data.Nat.Bits
5
6	/-!
7	---
8	title: The Decision Problems as Languages
9	type: definition
10	---
11	Instances as binary words, the representation against which classical complexity measures
12	running time, and the two decision problems as languages of such words.
13
14	A natural number is written as its binary digits preceded by their number in unary, which
15	makes the code self-delimiting. An instance is the number of clients, the number of days,
16	and then, day by day and client by client, the processing time and the due date of that
17	client's job on that day. An instance of $1 \mid \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$
18	appends the fairness parameter $k$ ; an instance of
19	$1 \mid k_j, \mathrm{rep} \mid \min_j \sum_i Z_{i,j}$ appends one parameter per client.
20
21	The language of the problem consists of the words encoding an instance and a parameter for
22	which a fair schedule exists. Every complexity claim of the source concerns a class of
23	instances — those with day-independent due dates, those whose fairness parameter is $m-1$ ,
24	those whose overall conflict graph has small treewidth — so the language is taken relative
25	to such a class: a word belongs to it if it encodes an instance in the class, together with
26	a parameter, that admits a fair schedule. A language is NP-hard if every language in NP
27	reduces to it in polynomial time.
28
29	# Formalization Notes
30
31	Numbers are written in binary. Under a unary encoding the input would be exponentially
32	longer, a polynomial-time reduction correspondingly easier to achieve, and every hardness
33	claim weaker.
34
35	Restricting the class shrinks the language on both sides at once, so a reduction into it
36	witnesses hardness on the class: a word outside the class is not in the language, whatever
37	else it encodes, and a reduction must therefore produce instances of the class for the
38	yes-instances it is given. This is what is usually called para-NP-hardness when the class
39	is one on which a parameter is bounded by a constant — the conclusion being that no
40	algorithm runs in time $f(\tau)\cdot\mathrm{poly}(n)$ for any function $f$ unless
41	$\mathrm{P} = \mathrm{NP}$ .
42
43	The class is a predicate on the instance and the parameter rather than a bound on a
44	parameter function, so that a claim reads as the condition a reader checks the construction
45	against.
46	-/
47
48	namespace Lax117284.Problems
49
50	open Lax117284.Scheduling Lax434930.PolynomialTime
51	open Lax434930.NondeterministicPolynomialTime Lax429075.Reductions
52
53	/-- A natural number as a binary word: its digits, least significant first, preceded by
54	their number in unary. -/
55	def encodeNat (n : ℕ) : Word :=
56	List.replicate n.bits.length true ++ [false] ++ n.bits
57
58	/-- An instance as a binary word: the number of clients, the number of days, then the
59	processing time and the due date of every job. -/
60	def encodeInstance (I : Instance) : Word :=
61	encodeNat I.clients ++ encodeNat I.days ++
62	(List.finRange I.days).flatMap fun i =>
63	(List.finRange I.clients).flatMap fun j => encodeNat (I.p i j) ++ encodeNat (I.d i j)
64
65	/-- An instance of `1 \| rep \| min_j ∑_i Z_{i,j}`: an instance followed by the fairness
66	parameter. -/
67	def encodeUniform (I : Instance) (k : ℕ) : Word := encodeInstance I ++ encodeNat k
68
69	/-- An instance of `1 \| k_j, rep \| min_j ∑_i Z_{i,j}`: an instance followed by one
70	fairness parameter per client. -/
71	def encodePerClient (I : Instance) (k : Fin I.clients → ℕ) : Word :=
72	encodeInstance I ++ (List.finRange I.clients).flatMap fun j => encodeNat (k j)
73
74	/-- `1 \| rep \| min_j ∑_i Z_{i,j}` on the class `C`, as a language: the words encoding
75	an instance of `C` with a fairness parameter for which a fair schedule exists. -/
76	def Uniform (C : Instance → ℕ → Prop) : Language :=
77	{w \| ∃ (I : Instance) (k : ℕ), encodeUniform I k = w ∧ C I k ∧ I.HasKFairSchedule k}
78
79	/-- `1 \| k_j, rep \| min_j ∑_i Z_{i,j}` on the class `C`, as a language. -/
80	def PerClient (C : (I : Instance) → (Fin I.clients → ℕ) → Prop) : Language :=
81	{w \| ∃ (I : Instance) (k : Fin I.clients → ℕ),
82	encodePerClient I k = w ∧ C I k ∧ I.HasFairSchedule k}
83
84	/-- The class of all instances and parameters. -/
85	def any : Instance → ℕ → Prop := fun _ _ => True
86
87	/-- An instance with one client and no day, whose only client cannot be served at all. -/
88	def blocked : Instance where
89	clients := 1
90	days := 0
91	p := fun i => i.elim0
92	d := fun i => i.elim0
93	p_pos := fun i => i.elim0
94	p_le_d := fun i => i.elim0
95
96	/-- A word belonging to no language of this submission: the instance `blocked` with the
97	fairness parameter `1`. It is the image a reduction gives the words it must reject. -/
98	def rejected : Word := encodeUniform blocked 1
99
100	/-- A word belonging to no per-client language: the instance `blocked` with the fairness
101	parameter `1` for its only client. -/
102	def rejectedPerClient : Word := encodePerClient blocked fun _ => 1
103
104	/-- A word encodes at most one instance with at most one fairness parameter. -/
105	axiom encodeUniform_inj {I I' : Instance} {k k' : ℕ}
106	(h : encodeUniform I k = encodeUniform I' k') : I = I' ∧ k = k'
107
108	/-- **A word encodes at most one instance with at most one family of fairness
109	parameters.** -/
110	axiom encodePerClient_inj {I I' : Instance} {k : Fin I.clients → ℕ}
111	{k' : Fin I'.clients → ℕ} (h : encodePerClient I k = encodePerClient I' k') :
112	I = I' ∧ HEq k k'
113
114	/-- The rejected word lies in no version of the language. -/
115	axiom rejected_notMem (C : Instance → ℕ → Prop) : rejected ∉ Uniform C
116
117	/-- The rejected word of the per-client problem lies in no version of its language. -/
118	axiom rejectedPerClient_notMem (C : (I : Instance) → (Fin I.clients → ℕ) → Prop) :
119	rejectedPerClient ∉ PerClient C
120
121	/-- A language is NP-hard if every language in NP reduces to it in polynomial time. -/
122	def NPHard (L : Language) : Prop := ∀ A : Language, A ∈ NP → ManyOne A L
123
124	end Lax117284.Problems
125

Show ProofShow ProofShow ProofShow Proof

Formalization Notes

Numbers are written in binary. Under a unary encoding the input would be exponentially longer, a polynomial-time reduction correspondingly easier to achieve, and every hardness claim weaker.

Restricting the class shrinks the language on both sides at once, so a reduction into it witnesses hardness on the class: a word outside the class is not in the language, whatever else it encodes, and a reduction must therefore produce instances of the class for the yes-instances it is given. This is what is usually called para-NP-hardness when the class is one on which a parameter is bounded by a constant — the conclusion being that no algorithm runs in time $f(\tau)\cdot\mathrm{poly}(n)$ for any function $f$ unless $\mathrm{P} = \mathrm{NP}$ .

The class is a predicate on the instance and the parameter rather than a bound on a parameter function, so that a claim reads as the condition a reader checks the construction against.

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

The Decision Problems as Languages

Flags

Flag this concept

Natural Language Statement

Definition

1 `encodePerClient_inj` proven

2 `encodeUniform_inj` proven

3 `rejected_notMem` proven

4 `rejectedPerClient_notMem` proven

Lean source view on GitHub

Discussion

Settings

Your comments

The Decision Problems as Languages

Natural Language Statement

Definition

1 encodePerClient_inj proven

2 encodeUniform_inj proven

3 rejected_notMem proven

4 rejectedPerClient_notMem proven

Lean source view on GitHub

Discussion

1 `encodePerClient_inj` proven

2 `encodeUniform_inj` proven

3 `rejected_notMem` proven

4 `rejectedPerClient_notMem` proven