Oracle computations

This file defines PCPs and LPCPs in terms of oracle computations.

Main declarations

• PCP, LPCP: PCP and linear PCP language classes with query and randomness bounds.

instance instEncodableZModOfNeZero (q : ℕ) [NeZero q] : Encodable (ZMod q)

Equations

• instEncodableZModOfNeZero q = Encodable.ofEquiv (Fin q) ↑(ZMod.finEquiv q).symm

@[reducible, inline]

abbrev RunsInTime {ι α : Type} {spec : OracleSpec ι} (_oa : OracleComp spec α) (_n : ℕ) : Prop

RunsInTime oa n means oa halts in at most n steps.

Equations

• RunsInTime _oa _n = (true = true)

@[reducible, inline]

abbrev QueryBound {ι α : Type} {proofSpec : OracleSpec ι} (oa : OracleComp (unifSpec + proofSpec) α) (q r : ℕ) : Prop

QueryBound oa q r means oa makes at most q proof queries and at most r randomness queries.

Equations

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

@[reducible, inline]

abbrev RandOracle : OracleContext ℕ ProbComp

Equations

• RandOracle = { spec := unifSpec, impl := fun (n : unifSpec.Domain) => $ᵗFin (n + 1) }

@[reducible, inline]

abbrev ProofOracle {F : Type} {ℓ : ℕ} (π : Fin ℓ → F) : OracleContext (Fin ℓ) ProbComp

A proof is represented as a function π : [ℓ] → F. π(q) is the answer to query q.

Equations

• ProofOracle π = { spec := OracleSpec.ofFn fun (x : Fin ℓ) => F, impl := fun (q : (OracleSpec.ofFn fun (x : Fin ℓ) => F).Domain) => pure (π q) }

@[reducible, inline]

abbrev PCPOracleSpec (F : Type) (ℓ : ℕ) : OracleSpec (ℕ ⊕ Fin ℓ)

Equations

• PCPOracleSpec F ℓ = unifSpec + OracleSpec.ofFn fun (x : Fin ℓ) => F

@[reducible, inline]

abbrev PCPVerifier (α : Type) (size : α → ℕ) (F : Type) (ℓ : ℕ → ℕ) : Type

Equations

• PCPVerifier α size F ℓ = ((x : α) → OracleComp (PCPOracleSpec F (ℓ (size x))) Bool)

def PCP {α : Type} (size : α → ℕ) (ε_c ε_s : ENNReal) (F : Type) [Fintype F] [DecidableEq F] [Inhabited F] (ℓ q r : ℕ → ℕ) : Set (Set α)

Equations

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

@[reducible, inline]

abbrev LinProofOracle {F : Type} [Field F] {ℓ : ℕ} (π : Fin ℓ → F) : OracleContext (Fin ℓ → F) ProbComp

A linear-query proof: a query is a vector u, and the answer is the inner product ⟨π, u⟩.

Equations

• LinProofOracle π = { spec := OracleSpec.ofFn fun (x : Fin ℓ → F) => F, impl := fun (u : (OracleSpec.ofFn fun (x : Fin ℓ → F) => F).Domain) => pure (π ⬝ᵥ u) }

@[reducible, inline]

abbrev LPCPOracleSpec (F : Type) [Field F] (ℓ : ℕ) : OracleSpec (ℕ ⊕ (Fin ℓ → F))

Equations

• LPCPOracleSpec F ℓ = unifSpec + OracleSpec.ofFn fun (x : Fin ℓ → F) => F

@[reducible, inline]

abbrev LPCPVerifier (α : Type) (size : α → ℕ) (F : Type) [Field F] (ℓ : ℕ → ℕ) : Type

Equations

• LPCPVerifier α size F ℓ = ((x : α) → OracleComp (LPCPOracleSpec F (ℓ (size x))) Bool)

def LPCP {α : Type} (size : α → ℕ) (ε_c ε_s : ENNReal) (F : Type) [Field F] [Fintype F] [DecidableEq F] [Inhabited F] (ℓ q r : ℕ → ℕ) : Set (Set α)

Equations

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