Arithmetization of quantified Boolean formulas with linearization

A quantified Boolean formula is arithmetized over a commutative ring by reading true as 1, false as 0, negation as 1 - a, conjunction as a * b, disjunction as 1 - (1 - a) * (1 - b), ∀ x as the product and ∃ x as the arithmetized disjunction of the values at x = 0 and x = 1 Lund, Fortnow, Karloff and Nisan, Shamir. Each quantifier can double the degree of the result in the other variables, so Shen's linearization operator L x, with value (1 - x) * a + x * b from the values a and b at x = 0 and x = 1, is applied after every quantifier: it does not change the value on 0-1 points and makes the result affine in x Shen, Arora and Barak, Section 8.3.

Cslib.Logic.PL.ArithQBF is the syntax of formulas with the two quantifiers and linearization as operators binding a variable (Cslib.Logic.PL.ArithQBF.Operator). Its value at a point r : V → R is Cslib.Logic.PL.ArithQBF.eval. Fixing every variable but x gives a univariate polynomial (Cslib.Logic.PL.ArithQBF.restrict), of degree at most the syntactic bound Cslib.Logic.PL.ArithQBF.degBound x (Cslib.Logic.PL.ArithQBF.natDegree_restrict_le). These are the polynomials a prover sends in the interactive proof for quantified Boolean formulas, and Cslib.Logic.PL.ArithQBF.roundDegree, the sum over the operators of the degree of their body in the bound variable, is the numerator of its soundness error.

On 0-1 points an arithmetic formula has the value of the quantified Boolean formula obtained by dropping its linearizations (Cslib.Logic.PL.ArithQBF.eval_boolean). The arithmetization Cslib.Logic.PL.QBF.arithmetize xs φ linearizes every variable of the list xs after every quantifier, so it has the value of φ on 0-1 points (Cslib.Logic.PL.QBF.eval_arithmetize). When xs contains every variable of φ, all degrees are at most the size of φ (Cslib.Logic.PL.QBF.degBound_arithmetize_le) and the sum of the round degrees is at most (2 * |xs| + 1) * size φ ^ 2 (Cslib.Logic.PL.QBF.roundDegree_arithmetize_le). For a verifier reading the same number of coefficients in every round, the arithmetization has at most (|xs| + 1) * size φ operators (Cslib.Logic.PL.QBF.ops_arithmetize_le), and, when xs contains every variable of φ, the body of each has degree at most 2 * size φ in its variable (Cslib.Logic.PL.QBF.maxRoundDegree_arithmetize_le). Values and restrictions depend only on the variables of a formula (Cslib.Logic.PL.ArithQBF.eval_congr, Cslib.Logic.PL.ArithQBF.restrict_congr). Shen linearizes only the free variables of each quantified subformula; linearizing a fixed list of variables is simpler to compute and costs only polynomially many more rounds.

Main definitions

• Cslib.Logic.PL.ArithQBF: arithmetic formulas with the operators ∃, ∀ and L.
• Cslib.Logic.PL.ArithQBF.eval, Cslib.Logic.PL.ArithQBF.restrict: values and univariate restrictions.
• Cslib.Logic.PL.ArithQBF.degBound, Cslib.Logic.PL.ArithQBF.roundDegree: syntactic degree bounds.
• Cslib.Logic.PL.ArithQBF.ops, Cslib.Logic.PL.ArithQBF.maxRoundDegree: the number of operators and the largest degree of their bodies.
• Cslib.Logic.PL.ArithQBF.vars: the variables of an arithmetic formula.
• Cslib.Logic.PL.ArithQBF.toQBF: the formula without its linearizations.
• Cslib.Logic.PL.QBF.arithmetize: the arithmetization with linearization.

Main results

• Cslib.Logic.PL.ArithQBF.eval_restrict, Cslib.Logic.PL.ArithQBF.natDegree_restrict_le: the restriction to a variable is a polynomial of degree at most degBound.
• Cslib.Logic.PL.ArithQBF.eval_boolean: on 0-1 points the value is that of the formula without its linearizations.
• Cslib.Logic.PL.QBF.eval_arithmetize, Cslib.Logic.PL.QBF.eval_arithmetize_zero: the arithmetization is faithful on 0-1 points, and a closed formula has value 1 or 0 at the origin.
• Cslib.Logic.PL.QBF.degBound_arithmetize_le, Cslib.Logic.PL.QBF.roundDegree_arithmetize_le, Cslib.Logic.PL.QBF.ops_arithmetize_le, Cslib.Logic.PL.QBF.maxRoundDegree_arithmetize_le: polynomial bounds.
• Cslib.Logic.PL.ArithQBF.eval_congr, Cslib.Logic.PL.ArithQBF.restrict_congr: dependence on the variables only.

References

• C. Lund, L. Fortnow, H. Karloff, N. Nisan, Algebraic methods for interactive proof systems
• A. Shamir, IP = PSPACE
• A. Shen, IP = SPACE: simplified proof
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Arithmetic formulas

inductive Cslib.Logic.PL.ArithQBF.Connective : Type

The binary connectives of arithmetic formulas.

• and : Connective

  Conjunction, arithmetized as a * b.

• or : Connective

  Disjunction, arithmetized as 1 - (1 - a) * (1 - b).

@[instance_reducible]

instance Cslib.Logic.PL.ArithQBF.instDecidableEqConnective : DecidableEq Connective

inductive Cslib.Logic.PL.ArithQBF.Operator : Type

The operators of arithmetic formulas, each binding a variable.

• ex : Operator

  Existential quantification, the arithmetized disjunction of the values at 0 and 1.

• all : Operator

  Universal quantification, the product of the values at 0 and 1.

• lin : Operator

  Linearization: (1 - x) * a + x * b for the values a and b at 0 and 1.

@[instance_reducible]

instance Cslib.Logic.PL.ArithQBF.instDecidableEqOperator : DecidableEq Operator

inductive Cslib.Logic.PL.ArithQBF (V : Type u_1) : Type u_1

Arithmetic formulas: quantified Boolean formulas over variables of type V whose operators binding a variable are the two quantifiers and Shen's linearization Shen.

• var {V : Type u_1} (v : V) : ArithQBF V

  The variable v.

• top {V : Type u_1} : ArithQBF V

  The constant 1.

• bot {V : Type u_1} : ArithQBF V

  The constant 0.

• not {V : Type u_1} (e : ArithQBF V) : ArithQBF V

  Negation, 1 - a.

• bin {V : Type u_1} (o : Connective) (e₁ e₂ : ArithQBF V) : ArithQBF V

  A binary connective.

• op {V : Type u_1} (o : Operator) (v : V) (e : ArithQBF V) : ArithQBF V

  An operator binding the variable v.

@[instance_reducible]

instance Cslib.Logic.PL.instDecidableEqArithQBF {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (ArithQBF V✝)

def Cslib.Logic.PL.instDecidableEqArithQBF.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : ArithQBF V✝) : Decidable (x✝ = x✝¹)

Values

def Cslib.Logic.PL.ArithQBF.Connective.apply {R : Type u_2} [CommRing R] : Connective → R → R → R

The value of a connective on the values a and b of its two arguments.

def Cslib.Logic.PL.ArithQBF.Operator.apply {R : Type u_2} [CommRing R] : Operator → R → R → R → R

The value of an operator binding x, on the value t of x and the values a and b of its body at x = 0 and x = 1.

theorem Cslib.Logic.PL.ArithQBF.Connective.map_apply {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) (o : Connective) (a b : R) : f (o.apply a b) = o.apply (f a) (f b)

theorem Cslib.Logic.PL.ArithQBF.Operator.map_apply {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) (o : Operator) (t a b : R) : f (o.apply t a b) = o.apply (f t) (f a) (f b)

def Cslib.Logic.PL.ArithQBF.eval {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) : ArithQBF V → R

The value of an arithmetic formula at the point r. An operator binding v combines the values of its body with v set to 0 and to 1, and, for linearization, the value r v.

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_var {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (v : V) : eval r (var v) = r v

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_top {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) : eval r top = 1

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_bot {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) : eval r bot = 0

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_not {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (e : ArithQBF V) : eval r e.not = 1 - eval r e

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_bin {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (e₁ e₂ : ArithQBF V) (o : Connective) : eval r (bin o e₁ e₂) = o.apply (eval r e₁) (eval r e₂)

@[simp]

theorem Cslib.Logic.PL.ArithQBF.eval_op {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (v : V) (e : ArithQBF V) (o : Operator) : eval r (op o v e) = o.apply (r v) (eval (Function.update r v 0) e) (eval (Function.update r v 1) e)

Univariate restrictions and their degrees

noncomputable def Cslib.Logic.PL.ArithQBF.restrict {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (x : V) : ArithQBF V → Polynomial R

The univariate polynomial obtained from an arithmetic formula by fixing every variable but x to its value in r (Cslib.Logic.PL.ArithQBF.eval_restrict).

theorem Cslib.Logic.PL.ArithQBF.eval_restrict {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (e : ArithQBF V) (x : V) (z : R) : Polynomial.eval z (restrict r x e) = eval (Function.update r x z) e

The restriction of a formula to x at r, evaluated at z, is the value of the formula at r with x set to z.

def Cslib.Logic.PL.ArithQBF.Operator.degMul : Operator → ℕ

The factor by which an operator binding another variable can multiply the degree in x.

def Cslib.Logic.PL.ArithQBF.degBound {V : Type u_1} [DecidableEq V] (x : V) : ArithQBF V → ℕ

A syntactic bound on the degree of an arithmetic formula in the variable x (Cslib.Logic.PL.ArithQBF.natDegree_restrict_le).

theorem Cslib.Logic.PL.ArithQBF.Connective.natDegree_apply_le {R : Type u_2} [CommRing R] (o : Connective) (p q : Polynomial R) : (o.apply p q).natDegree ≤ p.natDegree + q.natDegree

theorem Cslib.Logic.PL.ArithQBF.Operator.natDegree_apply_le {R : Type u_2} [CommRing R] (o : Operator) (t : R) {p q : Polynomial R} {d : ℕ} (hp : p.natDegree ≤ d) (hq : q.natDegree ≤ d) : (o.apply (Polynomial.C t) p q).natDegree ≤ o.degMul * d

theorem Cslib.Logic.PL.ArithQBF.Operator.natDegree_apply_X_le {R : Type u_2} [CommRing R] (o : Operator) (a b : R) : (o.apply Polynomial.X (Polynomial.C a) (Polynomial.C b)).natDegree ≤ 1

theorem Cslib.Logic.PL.ArithQBF.natDegree_restrict_le {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (r : V → R) (e : ArithQBF V) (x : V) : (restrict r x e).natDegree ≤ degBound x e

The restriction of a formula to x has degree at most degBound x.

def Cslib.Logic.PL.ArithQBF.roundDegree {V : Type u_1} [DecidableEq V] : ArithQBF V → ℕ

The sum, over the operators of a formula, of the degree of their body in the variable they bind: the number of roots that can fool the verifier in the interactive proof.

def Cslib.Logic.PL.ArithQBF.ops {V : Type u_1} : ArithQBF V → ℕ

The number of operators of a formula: the number of rounds of the interactive proof that draw a random element.

def Cslib.Logic.PL.ArithQBF.maxRoundDegree {V : Type u_1} [DecidableEq V] : ArithQBF V → ℕ

The largest degree, over the operators of a formula, of their body in the variable they bind. A prover sending polynomials of this degree can be honest in every round.

theorem Cslib.Logic.PL.ArithQBF.roundDegree_le_ops_mul {V : Type u_1} [DecidableEq V] (e : ArithQBF V) : e.roundDegree ≤ e.ops * e.maxRoundDegree

The round degrees sum to at most the number of rounds times the largest round degree.

Variables

def Cslib.Logic.PL.ArithQBF.vars {V : Type u_1} : ArithQBF V → List V

The variables of an arithmetic formula, free or bound, with multiplicity, in prefix order.

theorem Cslib.Logic.PL.ArithQBF.eval_congr {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (e : ArithQBF V) {r r' : V → R} (h : ∀ w ∈ e.vars, r w = r' w) : eval r e = eval r' e

The value of a formula depends only on the values of its variables.

theorem Cslib.Logic.PL.ArithQBF.restrict_congr {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (e : ArithQBF V) {r r' : V → R} (x : V) (h : ∀ w ∈ e.vars, r w = r' w) : restrict r x e = restrict r' x e

The restriction of a formula to a variable depends only on the values of its variables.

Values on 0-1 points

def Cslib.Logic.PL.ArithQBF.toQBF {V : Type u_1} : ArithQBF V → QBF V

The quantified Boolean formula obtained by dropping the linearizations.

theorem Cslib.Logic.PL.ArithQBF.eval_boolean {V : Type u_1} {R : Type u_2} [CommRing R] [DecidableEq V] (e : ArithQBF V) (σ : V → Bool) : eval (fun (w : V) => if σ w = true then 1 else 0) e = if QBF.eval σ e.toQBF = true then 1 else 0

Faithfulness on 0-1 points. At the point given by a truth assignment, an arithmetic formula has value 1 or 0 according to the truth value of the formula without its linearizations.

Linearization

def Cslib.Logic.PL.ArithQBF.lins {V : Type u_1} (xs : List V) (e : ArithQBF V) : ArithQBF V

Linearization of each variable of a list, the first one outermost.

@[simp]

theorem Cslib.Logic.PL.ArithQBF.lins_nil {V : Type u_1} (e : ArithQBF V) : lins [] e = e

@[simp]

theorem Cslib.Logic.PL.ArithQBF.lins_cons {V : Type u_1} (e : ArithQBF V) (x : V) (xs : List V) : lins (x :: xs) e = op Operator.lin x (lins xs e)

@[simp]

theorem Cslib.Logic.PL.ArithQBF.toQBF_lins {V : Type u_1} (e : ArithQBF V) (xs : List V) : (lins xs e).toQBF = e.toQBF

@[simp]

theorem Cslib.Logic.PL.ArithQBF.ops_lins {V : Type u_1} (e : ArithQBF V) (xs : List V) : (lins xs e).ops = xs.length + e.ops

Arithmetization

def Cslib.Logic.PL.QBF.arithmetize {V : Type u_1} (xs : List V) : QBF V → ArithQBF V

Arithmetization with linearization Shen: the arithmetic formula of φ that linearizes every variable of xs after every quantifier.

@[simp]

theorem Cslib.Logic.PL.QBF.toQBF_arithmetize {V : Type u_1} (xs : List V) (φ : QBF V) : (arithmetize xs φ).toQBF = φ

theorem Cslib.Logic.PL.QBF.eval_arithmetize {V : Type u_1} {R : Type u_2} [DecidableEq V] [CommRing R] (xs : List V) (φ : QBF V) (σ : V → Bool) : ArithQBF.eval (fun (v : V) => if σ v = true then 1 else 0) (arithmetize xs φ) = if eval σ φ = true then 1 else 0

The arithmetization is faithful on 0-1 points.

theorem Cslib.Logic.PL.QBF.eval_arithmetize_zero {V : Type u_1} {R : Type u_2} [DecidableEq V] [CommRing R] (xs : List V) {φ : QBF V} (hφ : φ.Closed) (σ : V → Bool) : ArithQBF.eval 0 (arithmetize xs φ) = if eval σ φ = true then 1 else 0

A closed formula's arithmetization has value 1 or 0 at the origin, according to its truth value.

theorem Cslib.Logic.PL.QBF.degBound_arithmetize_eq_zero {V : Type u_1} [DecidableEq V] {xs : List V} {x : V} (hx : x ∉ xs) {φ : QBF V} (hφ : x ∉ φ.vars) : ArithQBF.degBound x (arithmetize xs φ) = 0

A variable that does not occur in φ nor in xs does not occur in the arithmetization.

theorem Cslib.Logic.PL.QBF.degBound_arithmetize_le {V : Type u_1} [DecidableEq V] {xs : List V} {φ : QBF V} (hxs : ∀ v ∈ φ.vars, v ∈ xs) (x : V) : ArithQBF.degBound x (arithmetize xs φ) ≤ φ.size

Degrees stay small. When xs contains every variable of φ, the arithmetization has degree at most the size of φ in every variable.

theorem Cslib.Logic.PL.QBF.roundDegree_arithmetize_le {V : Type u_1} [DecidableEq V] {xs : List V} {φ : QBF V} (hxs : ∀ v ∈ φ.vars, v ∈ xs) : (arithmetize xs φ).roundDegree ≤ (2 * xs.length + 1) * φ.size ^ 2

The round degrees are polynomial. When xs contains every variable of φ, the sum of the round degrees of the arithmetization is at most (2 * |xs| + 1) * size φ ^ 2.

theorem Cslib.Logic.PL.QBF.mem_vars_arithmetize {V : Type u_1} {xs : List V} {φ : QBF V} {w : V} (h : w ∈ (arithmetize xs φ).vars) : w ∈ φ.vars ∨ w ∈ xs

Every variable of the arithmetization is a variable of φ or of xs.

theorem Cslib.Logic.PL.QBF.ops_arithmetize_le {V : Type u_1} (xs : List V) (φ : QBF V) : (arithmetize xs φ).ops ≤ (xs.length + 1) * φ.size

The arithmetization has at most (|xs| + 1) * size φ operators.

theorem Cslib.Logic.PL.QBF.maxRoundDegree_arithmetize_le {V : Type u_1} [DecidableEq V] {xs : List V} {φ : QBF V} (hxs : ∀ v ∈ φ.vars, v ∈ xs) : (arithmetize xs φ).maxRoundDegree ≤ 2 * φ.size

Every round is of small degree. When xs contains every variable of φ, the body of every operator of the arithmetization has degree at most 2 * size φ in its variable.