Composition: alphabet reduction

The powering step of Dinur's proof of the PCP theorem amplifies the value of a constraint graph at the cost of an enormous, though constant, alphabet. Composition Dinur, Section 3.3 brings the alphabet back to a fixed one, losing a constant factor of the value that does not depend on the alphabet being reduced: that independence is what lets powering win.

Composition replaces every edge e of a constraint graph G over a finite alphabet α by the Hadamard assignment tester of its constraint (PCP.hadamardTester), on the labels in α themselves. The testers of all the edges share the tables of the vertices: the composed proof holds, for every vertex, a table that is supposedly the long code of its label, and for every edge, the linear and quadratic tables of its tester. The composed test (ConstraintGraph.composeTest) runs the tester of a uniformly random edge on the tables of the ends of that edge and on its own tables, and the composed constraint graph G.compose is the constraint graph of that test (LocalTest.toConstraintGraph). Its alphabet Bool × (HadamardTester.Query → Bool) has 2 ^ 18 symbols, whatever α is.

A labelling satisfying G gives the honest composed proof, which the composed test passes on every random string (ConstraintGraph.satisfiable_compose). Conversely, a labelling of the composed graph is decoded to a labelling of G by reading at every vertex the label whose long code is within relative distance 1/4 of its table (ConstraintGraph.decodeLabelling). If the decoded labelling violates an edge of G, the tester of that edge rejects with probability at least 1/28: otherwise its soundness would give labels satisfying the edge, with long codes within 1/4 of the tables of its ends, which the decoding must return. So the composed test rejects with probability at least 1/28 times the proportion of the edges of G that the decoded labelling violates, and since it makes 17 queries, the composed graph has value at least 1/476 times that of G (ConstraintGraph.le_unsatVal_compose). The number of edges is multiplied by a constant depending only on |α| (ConstraintGraph.card_edges_compose).

Main definitions

• Cslib.PCP.ConstraintGraph.decodeLabel: the label whose long code is close to a table.
• Cslib.PCP.ConstraintGraph.composeTest: the composed test of a constraint graph.
• Cslib.PCP.ConstraintGraph.compose: the composed constraint graph.
• Cslib.PCP.ConstraintGraph.composeProof: the honest composed proof of a labelling.
• Cslib.PCP.ConstraintGraph.decodeLabelling: the labelling decoded from a composed proof.

Main results

• Cslib.PCP.ConstraintGraph.satisfiable_compose, Cslib.PCP.ConstraintGraph.unsatVal_compose_le: completeness of composition.
• Cslib.PCP.ConstraintGraph.one_div_le_one_sub_acceptProb_of_not_satisfies: the tester of an edge violated by the decoded labelling rejects.
• Cslib.PCP.ConstraintGraph.unsatFrac_decodeLabelling_le, Cslib.PCP.ConstraintGraph.le_unsatVal_compose: soundness of composition.
• Cslib.PCP.ConstraintGraph.satisfiable_compose_iff: composition preserves satisfiability.
• Cslib.PCP.ConstraintGraph.card_edges_compose, Cslib.PCP.ConstraintGraph.card_vertices_compose, Cslib.PCP.ConstraintGraph.card_alphabet_compose: the size of the composed graph.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

noncomputable def Cslib.PCP.HadamardTester.assignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] : AssignmentTester α (α → Bool) (LinPos α ⊕ QuadPos α) (Rand α) Query Bool

The Hadamard tester as data for binary-constraint composition. Its distance-soundness theorem remains separate; composition needs only rejection on a violated decoded constraint.

theorem Cslib.PCP.HadamardTester.isComplete_assignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] : assignmentTester.IsComplete

The Hadamard construction has perfect completeness in the generic composition interface.

@[reducible, inline]

abbrev Cslib.PCP.ConstraintGraph.ComposePos (V : Type u_4) (E : Type u_5) (α : Type u_6) : Type (max (max u_6 u_5) u_4)

The positions of a composed proof, for vertices V, edges E and labels in α: the bit inl (v, r) of the table of the vertex v at r, and the bit inr (e, y) of the tables of the tester of the edge e at the position y of its linear or quadratic table.

@[instance_reducible]

instance Cslib.PCP.ConstraintGraph.instFintypeComposePosOfDecidableEq {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype V] [Fintype E] [Fintype α] [DecidableEq α] : Fintype (ComposePos V E α)

The positions of a composed proof are finitely many.

Decoding the long code

noncomputable def Cslib.PCP.ConstraintGraph.decodeLabel {α : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] (T : (α → Bool) → Bool) : α

The label decoded from a table T: the label whose long code is within relative distance 1/4 of T, if there is one (it is then unique, decodeLabel_eq), and an arbitrary label otherwise.

theorem Cslib.PCP.HadamardTester.sound_assignmentTester {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] : assignmentTester.Sound ConstraintGraph.decodeLabel (1 / 28)

A violated constraint on the uniquely decoded input tables is rejected with probability at least 1/28. This is the soundness contract required by generic composition.

The composed constraint graph

def Cslib.PCP.ConstraintGraph.testerPos {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) (e : E) : HadamardTester.Pos α → ComposePos V E α

Where the tester of the edge e reads in a composed proof: the table of its end b is the table of the vertex G.ends e b, and its linear and quadratic tables are those of e.

noncomputable def Cslib.PCP.ConstraintGraph.composeTest {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] : LocalTest (ComposePos V E α) (E × HadamardTester.Rand α) HadamardTester.Query Bool

The composed test Dinur, Section 3.3: on a uniformly random edge e, run the Hadamard assignment tester of the constraint of e on the tables of the ends of e and the tables of its tester.

noncomputable def Cslib.PCP.ConstraintGraph.compose {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] : ConstraintGraph (ComposePos V E α ⊕ E × HadamardTester.Rand α) ((E × HadamardTester.Rand α) × HadamardTester.Query) (Bool × (HadamardTester.Query → Bool))

The composed constraint graph Dinur, Section 3.3: the constraint graph of the composed test, over the alphabet Bool × (HadamardTester.Query → Bool), which does not depend on α.

Completeness

noncomputable def Cslib.PCP.ConstraintGraph.composeProof {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] (σ : V → α) : ComposePos V E α → Bool

The honest composed proof of a labelling σ of G: the long code of the label of every vertex as its table, and the honest proof of the labels of its ends as the tables of the tester of every edge.

theorem Cslib.PCP.ConstraintGraph.composeProof_comp_testerPos {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] (σ : V → α) (e : E) : G.composeProof σ ∘ G.testerPos e = HadamardTester.honestProof fun (b : Fin 2) => σ (G.ends e b)

The tester of the edge e reads in the honest composed proof the honest proof of the labels of the ends of e.

theorem Cslib.PCP.ConstraintGraph.passes_composeTest_composeProof {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] {σ : V → α} {e : E} (he : G.Satisfies σ e) (ω : HadamardTester.Rand α) : G.composeTest.Passes (G.composeProof σ) (e, ω)

The composed test passes the honest composed proof of σ on every random string of the edges satisfied by σ.

theorem Cslib.PCP.ConstraintGraph.satisfiable_compose {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] (h : G.Satisfiable) : G.compose.Satisfiable

Completeness of composition Dinur, Lemma 3.6: if G is satisfiable, so is the composed graph.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_compose_labellingOf_le {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Fintype E] (σ : V → α) (γ : Bool) : G.compose.unsatFrac (G.composeTest.labellingOf (G.composeProof σ) γ) ≤ G.unsatFrac σ

The labelling of the composed graph by the honest composed proof of σ violates at most the proportion of the edges of G that σ violates.

theorem Cslib.PCP.ConstraintGraph.unsatVal_compose_le {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Fintype E] [Nonempty α] : G.compose.unsatVal ≤ G.unsatVal

Completeness of composition, quantitatively: composition does not increase the value.

Soundness

noncomputable def Cslib.PCP.ConstraintGraph.decodeLabelling {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] (π : ComposePos V E α → Bool) (v : V) : α

The labelling of G decoded from a composed proof π: every vertex gets the label decoded from its table.

theorem Cslib.PCP.ConstraintGraph.one_div_le_one_sub_acceptProb_of_not_satisfies {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] {π : ComposePos V E α → Bool} {e : E} (he : ¬G.Satisfies (decodeLabelling π) e) : 1 / 28 ≤ 1 - (hadamardTester (G.rel e)).acceptProb (π ∘ G.testerPos e)

A violated edge makes its tester reject: if the labelling decoded from a composed proof π violates the edge e, the tester of e rejects π with probability at least 1/28.

theorem Cslib.PCP.ConstraintGraph.unsatFrac_decodeLabelling_le {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] [Fintype E] (A : ComposePos V E α ⊕ E × HadamardTester.Rand α → Bool × (HadamardTester.Query → Bool)) : G.unsatFrac (decodeLabelling (LocalTest.proofOf A)) ≤ 476 * G.compose.unsatFrac A

Soundness of composition, for a labelling: every labelling A of the composed graph violates a proportion of the edges at least 1/476 times the proportion of the edges of G violated by the labelling decoded from it.

theorem Cslib.PCP.ConstraintGraph.le_unsatVal_compose {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] [Fintype E] : G.unsatVal / 476 ≤ G.compose.unsatVal

Soundness of composition Dinur, Lemma 3.6: composition divides the value of a constraint graph by at most 476, whatever its alphabet.

theorem Cslib.PCP.ConstraintGraph.satisfiable_compose_iff {V : Type u_1} {E : Type u_2} {α : Type u_3} (G : ConstraintGraph V E α) [Fintype α] [DecidableEq α] [Nonempty α] [Finite E] : G.compose.Satisfiable ↔ G.Satisfiable

Composition preserves satisfiability.

Size

theorem Cslib.PCP.ConstraintGraph.card_edges_compose {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype E] : Fintype.card ((E × HadamardTester.Rand α) × HadamardTester.Query) = 17 * 2 ^ (20 * Fintype.card α ^ 2 + 15 * Fintype.card α + 3) * Fintype.card E

The size of the composed graph: every edge of G gives 17 · 2 ^ (20 k² + 15 k + 3) edges, where k = |α|, a constant depending only on the alphabet.

theorem Cslib.PCP.ConstraintGraph.card_vertices_compose {V : Type u_1} {E : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Fintype V] [Fintype E] : Fintype.card (ComposePos V E α ⊕ E × HadamardTester.Rand α) = 2 ^ Fintype.card α * Fintype.card V + (2 ^ (2 * Fintype.card α) + 2 ^ (4 * Fintype.card α ^ 2) + 2 ^ (20 * Fintype.card α ^ 2 + 15 * Fintype.card α + 3)) * Fintype.card E

The composed graph has a vertex for each position of the table of every vertex of G, and for each position of the tables of the tester of every edge and each random string of that tester.

theorem Cslib.PCP.ConstraintGraph.card_alphabet_compose : Fintype.card (Bool × (HadamardTester.Query → Bool)) = 2 ^ 18

The alphabet of the composed graph has 2 ^ 18 symbols.