Probabilistically checkable proofs: definitions

PCP r q is the class of languages with a probabilistically checkable proof system: a polynomial-time verifier that, on an input of length n, flips r n coins, reads at most q n bits of a proof string, always accepts a correct proof of a member, and rejects every purported proof of a non-member with probability at least 1/2. This is the class PCP[r(n), q(n)] of Arora–Barak, Definition 11.5, and of https://en.wikipedia.org/wiki/PCP_(complexity): "the class of problems for which a probabilistically checkable proof of a solution can be given, such that the proof can be checked in polynomial time using r(n) bits of randomness and by reading q(n) bits of the proof, correct proofs are always accepted, and incorrect proofs are rejected with probability at least 1/2."

As in Complexitylib.Classes.Interactive, the verifier is machine-free: its two computations are a query-selection function in FP and a verdict language in P, both applied to encoded tuples. The verifier is non-adaptive — the positions it reads are a function of the input and the coins alone, not of earlier answers — which is the standard choice (Arora–Barak, Definition 11.5) and costs only a 2^q blow-up in query count against the adaptive variant.

Main definitions

• PCPVerifier — query positions as an FP-computable function of the encoded input and coins, and a verdict in P on the input, the coins, and the bits read
• PCPVerifier.Accepts, PCPVerifier.acceptEvent
• PCP — the class PCP[r(n), q(n)]

Main results

• PCP_mono — more coins or more queries only enlarge the class
• P_subset_PCP — the definition contains P for every r and q: the verifier reads nothing and ignores its coins
• Constructible — a resource bound that can be written out in unary

Conventions

The verifier uses exactly r n coins, never fewer: a verifier wanting fewer can ignore the surplus, so this loses nothing, and it keeps the coin count a parameter of the class rather than a field the verifier could smuggle non-uniform information into. The query count is an upper bound ≤ q n since the position list is produced by the FP function and carries no hidden information.

The proof is a finite string; a position beyond its end reads as false. This is no restriction, as the verifier's positions are polynomially many bits long, so a proof of length q n · 2 ^ r n suffices, matching the usual convention.

Completeness 1 and soundness 1/2 are hard-wired, following the PCP[r, q] convention rather than the 2/3–1/3 of Complexitylib.Classes.Randomized.

Verifiers

structure Complexity.PCPVerifier : Type

A (non-adaptive) PCP verifier: from the encoded input and coins it computes a list of proof positions in polynomial time, and from the input, the coins, and the bits found there it decides in polynomial time.

• positions : List Bool → List Bool → List ℕ

  The proof positions queried on input x with coins r.

• positions_mem : ∃ f ∈ FP, ∀ (x r : List Bool), f (pair x r) = DataEncode.bitstringEncode (self.positions x r)

  That computation is polynomial-time, as a function of pair x r producing the DataEncode bitstring of the position list.

• verdict : Language

  The verdict, on pair (pair x r) a where a lists the bits read.

• verdict_mem : self.verdict ∈ P

  That verdict is polynomial-time decidable.

def Complexity.PCPVerifier.answers (π : List Bool) (ps : List ℕ) : List Bool

The bits of the proof π at the listed positions; a position past the end of the proof reads as false.

Equations

• Complexity.PCPVerifier.answers π ps = List.map (fun (i : ℕ) => π.getD i false) ps

def Complexity.PCPVerifier.Accepts (V : PCPVerifier) (x π r : List Bool) : Prop

The verifier accepts input x and proof π with coins r.

Equations

• V.Accepts x π r = (Complexity.pair (Complexity.pair x r) (Complexity.PCPVerifier.answers π (V.positions x r)) ∈ V.verdict)

noncomputable def Complexity.PCPVerifier.acceptEvent (V : PCPVerifier) (t : ℕ) (x π : List Bool) : Finset (Fin t → Bool)

The coin strings of length t on which V accepts x with proof π.

Equations

• V.acceptEvent t x π = {r : Fin t → Bool | V.Accepts x π (Complexity.BitString.toList r)}

def Complexity.PCPVerifier.QueryBounded (V : PCPVerifier) (q : ℕ → ℕ) : Prop

The verifier reads at most q n bits of the proof on inputs of length n, whatever its coins.

Equations

• V.QueryBounded q = ∀ (x r : List Bool), (V.positions x r).length ≤ q x.length

The class

def Complexity.PCP (r q : ℕ → ℕ) : Set Language

PCP[r(n), q(n)]: languages with a polynomial-time verifier using r n random bits and reading at most q n bits of the proof, such that a member has a proof the verifier always accepts, while every proof of a non-member is rejected with probability at least 1/2.

Equations

• One or more equations did not get rendered due to their size.

Elementary properties

theorem Complexity.P_subset_PCP (r q : ℕ → ℕ) : P ⊆ PCP r q

P ⊆ PCP[r, q] for every r and q: the verifier never looks at the proof or its coins.

theorem Complexity.PCP_mono_queries {r q q' : ℕ → ℕ} (hq : ∀ (n : ℕ), q n ≤ q' n) : PCP r q ⊆ PCP r q'

More queries only enlarge the class.

Constructible bounds

def Complexity.Constructible (r : ℕ → ℕ) : Prop

A resource bound is constructible when it can be written out in unary in polynomial time.

Some such requirement is not optional. PCP r q constrains the verifier but says nothing about r, so without it the union below is not a complexity class at all: Complexitylib.Classes.PCP.Internal.BoundNotConstructible proves that for every set A ⊆ ℕ, computable or not, the language of inputs whose length lies in A satisfies the PCP conditions with r the indicator of A — a bound that is O(1), hence O(log n). That puts continuum-many languages in the union while NP is countable, so the unrestricted equation is false. Textbook statements of the theorem carry the same requirement tacitly, by taking the bounds to be constructible functions.

Equations

• Complexity.Constructible r = ((fun (x : List Bool) => List.replicate (r x.length) true) ∈ Complexity.FP)