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

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

Main results

• existsQuantify_eq_true — iff characterization via existential
• forallQuantify_eq_true — iff characterization via universal
• forallQuantify_eq_not_existsQuantify_not — De Morgan duality
• existsQuantify_mono — monotonicity under pointwise implication

def Complexity.existsQuantify {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

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

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

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

Equations

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

@[simp]

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

Characterization: existsQuantify f y = true iff some assignment x to the first k inputs makes f (x ++ y) = true.

@[simp]

theorem Complexity.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

Characterization: forallQuantify f y = true iff every assignment x to the first k inputs makes f (x ++ y) = true.

theorem Complexity.forallQuantify_eq_not_existsQuantify_not {k m : ℕ} (f : BitString (k + m) → Bool) (y : BitString m) : forallQuantify f y = !existsQuantify (fun (z : BitString (k + m)) => !f z) y

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

theorem Complexity.existsQuantify_eq_not_forallQuantify_not {k m : ℕ} (f : BitString (k + m) → Bool) (y : BitString m) : existsQuantify f y = !forallQuantify (fun (z : BitString (k + m)) => !f z) y

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

theorem Complexity.existsQuantify_mono {k m : ℕ} {f g : BitString (k + m) → Bool} (h : ∀ (z : BitString (k + m)), f z = true → g z = true) {y : BitString m} : existsQuantify f y = true → existsQuantify g y = true

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

theorem Complexity.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 Complexity.existsQuantify_const_true {k m : ℕ} : (existsQuantify fun (x : BitString (k + m)) => true) = fun (x : BitString m) => true

Constant true: existential quantification is always true.

@[simp]

theorem Complexity.existsQuantify_const_false {k m : ℕ} : (existsQuantify fun (x : BitString (k + m)) => false) = fun (x : BitString m) => false

Constant false: existential quantification is always false.

@[simp]

theorem Complexity.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 Complexity.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 Complexity.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

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

theorem Complexity.existsQuantify_succ {k m : ℕ} (f : BitString (k + 1 + m) → Bool) (y : BitString m) : existsQuantify f y = (existsQuantify (restrictFirst f false) y || existsQuantify (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))