Nondeterministic Quantification of Boolean Functions

This module defines existential and universal quantification over inputs of Boolean functions, corresponding to nondeterministic computation.

Given f : BitString (k + m) → Bool, existential quantification over the first k variables produces g : BitString m → Bool defined by g(y) = true iff there exists an assignment x : BitString k such that f(x ++ y) = true. This models a nondeterministic circuit that guesses the first k input bits.

Main definitions

• existQuantify — existential quantification over first k inputs
• forallQuantify — universal quantification over first k inputs

Main results

• existQuantify_eq_true — iff characterization via existential
• forallQuantify_eq_true — iff characterization via universal
• forallQuantify_eq_not_existQuantify_not — De Morgan duality
• existQuantify_mono — monotonicity under pointwise implication

def CircuitComplexity.existQuantify {k m : ℕ} (f : BitString (k + m) → Bool) : BitString m → Bool

Existential quantification over the first k inputs of a Boolean function. Given f : BitString (k + m) → Bool, produces g : BitString m → Bool where g(y) = true iff ∃ x : BitString k, f(x ++ y) = true.

This models a nondeterministic circuit that guesses the first k inputs.

Equations

• CircuitComplexity.existQuantify f y = decide (∃ (x : CircuitComplexity.BitString k), f (Fin.append x y) = true)

def CircuitComplexity.forallQuantify {k m : ℕ} (f : BitString (k + m) → Bool) : BitString m → Bool

Universal quantification over the first k inputs of a Boolean function.

Equations

• CircuitComplexity.forallQuantify f y = decide (∀ (x : CircuitComplexity.BitString k), f (Fin.append x y) = true)

@[simp]

theorem CircuitComplexity.existQuantify_eq_true {k m : ℕ} {f : BitString (k + m) → Bool} {y : BitString m} : existQuantify f y = true ↔ ∃ (x : BitString k), f (Fin.append x y) = true

@[simp]

theorem CircuitComplexity.forallQuantify_eq_true {k m : ℕ} {f : BitString (k + m) → Bool} {y : BitString m} : forallQuantify f y = true ↔ ∀ (x : BitString k), f (Fin.append x y) = true

theorem CircuitComplexity.forallQuantify_eq_not_existQuantify_not {k m : ℕ} (f : BitString (k + m) → Bool) (y : BitString m) : forallQuantify f y = !existQuantify (fun (z : BitString (k + m)) => !f z) y

De Morgan duality: universal quantification equals negated existential of negation.

theorem CircuitComplexity.existQuantify_eq_not_forallQuantify_not {k m : ℕ} (f : BitString (k + m) → Bool) (y : BitString m) : existQuantify f y = !forallQuantify (fun (z : BitString (k + m)) => !f z) y

De Morgan duality: existential quantification equals negated universal of negation.

theorem CircuitComplexity.existQuantify_mono {k m : ℕ} {f g : BitString (k + m) → Bool} (h : ∀ (z : BitString (k + m)), f z = true → g z = true) {y : BitString m} : existQuantify f y = true → existQuantify g y = true

Monotonicity: if f implies g pointwise, existential quantification preserves this.

theorem CircuitComplexity.forallQuantify_mono {k m : ℕ} {f g : BitString (k + m) → Bool} (h : ∀ (z : BitString (k + m)), f z = true → g z = true) {y : BitString m} : forallQuantify f y = true → forallQuantify g y = true

Monotonicity for universal quantification.

@[simp]

theorem CircuitComplexity.existQuantify_const_true {k m : ℕ} : (existQuantify fun (x : BitString (k + m)) => true) = fun (x : BitString m) => true

Constant true: existential quantification is always true.

@[simp]

theorem CircuitComplexity.existQuantify_const_false {k m : ℕ} : (existQuantify fun (x : BitString (k + m)) => false) = fun (x : BitString m) => false

Constant false: existential quantification is always false.

@[simp]

theorem CircuitComplexity.forallQuantify_const_true {k m : ℕ} : (forallQuantify fun (x : BitString (k + m)) => true) = fun (x : BitString m) => true

Constant true: universal quantification is always true.

@[simp]

theorem CircuitComplexity.forallQuantify_const_false {k m : ℕ} : (forallQuantify fun (x : BitString (k + m)) => false) = fun (x : BitString m) => false

Constant false: universal quantification is always false.

def CircuitComplexity.restrictFirst {k m : ℕ} (f : BitString (k + 1 + m) → Bool) (b : Bool) : BitString (k + m) → Bool

Restrict a Boolean function by fixing its first input to a constant. Reduces the input size from (k + 1) + m to k + m.

Equations

• CircuitComplexity.restrictFirst f b z = f fun (i : Fin (k + 1 + m)) => if h : ↑i = 0 then b else z ⟨↑i - 1, ⋯⟩

theorem CircuitComplexity.existQuantify_succ {k m : ℕ} (f : BitString (k + 1 + m) → Bool) (y : BitString m) : existQuantify f y = (existQuantify (restrictFirst f false) y || existQuantify (restrictFirst f true) y)

Decomposition: quantifying over k + 1 variables factors as quantifying over k variables for each value of the first variable.

(∃ a ∈ {0,1}^{k+1}, f(a,y)) ↔ (∃ x ∈ {0,1}^k, f(0∷x,y)) ∨ (∃ x ∈ {0,1}^k, f(1∷x,y))