Alternating formulas

An alternating formula of depth d over n variables is a formula in negation normal form whose unbounded fan-in AND and OR gates alternate along every path from the root, with d gates on each path and literals at the bottom (AltFormula n d): a literal (i, b) holds when bit i is b, as in Logic.PL.Literal. Its root operation is given when it is evaluated (AltFormula.eval), and its size counts the AND and OR gates; literals are free (AltFormula.size). This is the model of constant-depth circuits in which negations are free and only at the inputs. At depth two, alternating formulas are formulas in conjunctive or disjunctive normal form (AltFormula.eval_and_eq_cnf_eval, AltFormula.eval_or_eq_dnf_eval).

Substituting literals for the inputs costs nothing (AltFormula.mapInputs), and negating every input computes the negation with the dual root operation (AltFormula.eval_neg). Every function has alternating formulas of depth two of size 2 ^ n + 1 (AltFormula.exists_depth_two). An alternating formula of depth d is a circuit over the unbounded fan-in basis of AND/OR depth at most d, and of depth at most d + 1 counting negations, with at most n more gates, computing the negated inputs first (AltFormula.exists_circuit).

Main definitions

• Cslib.Circuits.Boolean.AltFormula: alternating formulas of a given depth.
• Cslib.Circuits.Boolean.AltFormula.eval, Cslib.Circuits.Boolean.AltFormula.size: their meaning, for a root operation, and their number of gates.

Main results

• Cslib.Circuits.Boolean.AltFormula.eval_and_eq_cnf_eval, Cslib.Circuits.Boolean.AltFormula.eval_or_eq_dnf_eval: depth two is conjunctive and disjunctive normal form.
• Cslib.Circuits.Boolean.AltFormula.exists_depth_two: normal forms as alternating formulas.
• Cslib.Circuits.Boolean.AltFormula.exists_circuit: alternating formulas as circuits over the unbounded fan-in basis.

inductive Cslib.Circuits.Boolean.AltOp : Type

The operation at the root of an alternating formula.

• and : AltOp

  Conjunction.

• or : AltOp

  Disjunction.

@[instance_reducible]

instance Cslib.Circuits.Boolean.instDecidableEqAltOp : DecidableEq AltOp

def Cslib.Circuits.Boolean.AltOp.dual : AltOp → AltOp

De Morgan duality swaps conjunction and disjunction.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.AltFormula (n : ℕ) : ℕ → Type

Alternating formulas of depth d over n variables: literals at depth zero, and a list of alternating formulas of depth d below each gate of depth d + 1. It is reducible, so that an alternating formula of depth two is a formula in conjunctive or disjunctive normal form.

def Cslib.Circuits.Boolean.AltFormula.size {n d : ℕ} : AltFormula n d → ℕ

The number of AND and OR gates; literals are free.

def Cslib.Circuits.Boolean.AltFormula.eval {n d : ℕ} : AltOp → AltFormula n d → BitString n → Bool

Evaluate an alternating formula with op at the root.

def Cslib.Circuits.Boolean.AltFormula.mapInputs {n m : ℕ} (ρ : Fin n → Logic.PL.Literal (Fin m)) {d : ℕ} : AltFormula n d → AltFormula m d

Substitute literals for the inputs. This changes no gates.

def Cslib.Circuits.Boolean.AltFormula.neg {n d : ℕ} (f : AltFormula n d) : AltFormula n d

Negate every input; with the dual root operation, this computes the negation (AltFormula.eval_neg).

@[simp]

theorem Cslib.Circuits.Boolean.AltFormula.size_mapInputs {n m d : ℕ} (ρ : Fin n → Logic.PL.Literal (Fin m)) (f : AltFormula n d) : (mapInputs ρ f).size = f.size

theorem Cslib.Circuits.Boolean.AltFormula.eval_mapInputs {n m d : ℕ} (ρ : Fin n → Logic.PL.Literal (Fin m)) (f : AltFormula n d) (op : AltOp) (x : BitString m) : eval op (mapInputs ρ f) x = eval op f fun (i : Fin n) => Logic.PL.Literal.eval x (ρ i)

@[simp]

theorem Cslib.Circuits.Boolean.AltFormula.size_neg {n d : ℕ} (f : AltFormula n d) : f.neg.size = f.size

theorem Cslib.Circuits.Boolean.AltFormula.eval_neg {n d : ℕ} (f : AltFormula n d) (op : AltOp) (x : BitString n) : eval op.dual f.neg x = !eval op f x

De Morgan's law: negating every input and dualizing the root operation negates the value.

theorem Cslib.Circuits.Boolean.AltFormula.eval_and_eq_cnf_eval {n : ℕ} (f : AltFormula n 2) (x : BitString n) : eval AltOp.and f x = Logic.PL.CNF.eval x f

An alternating formula of depth two with a conjunction at the root is a formula in conjunctive normal form.

theorem Cslib.Circuits.Boolean.AltFormula.eval_or_eq_dnf_eval {n : ℕ} (f : AltFormula n 2) (x : BitString n) : eval AltOp.or f x = Logic.PL.DNF.eval x f

An alternating formula of depth two with a disjunction at the root is a formula in disjunctive normal form.

Building alternating formulas

noncomputable def Cslib.Circuits.Boolean.AltFormula.gate {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n d) : AltFormula n (d + 1)

One gate over a finite family of alternating formulas.

theorem Cslib.Circuits.Boolean.AltFormula.size_gate {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n d) : (gate fs).size = 1 + ∑ i : ι, (fs i).size

theorem Cslib.Circuits.Boolean.AltFormula.eval_gate_and {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n d) (x : BitString n) : eval AltOp.and (gate fs) x = true ↔ ∀ (i : ι), eval AltOp.or (fs i) x = true

theorem Cslib.Circuits.Boolean.AltFormula.eval_gate_or {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n d) (x : BitString n) : eval AltOp.or (gate fs) x = true ↔ ∃ (i : ι), eval AltOp.and (fs i) x = true

noncomputable def Cslib.Circuits.Boolean.AltFormula.merge {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n (d + 1)) : AltFormula n (d + 1)

Merge the roots of a finite family of alternating formulas into one, without adding a gate layer.

theorem Cslib.Circuits.Boolean.AltFormula.eval_merge_and {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n (d + 1)) (x : BitString n) : eval AltOp.and (merge fs) x = true ↔ ∀ (i : ι), eval AltOp.and (fs i) x = true

theorem Cslib.Circuits.Boolean.AltFormula.eval_merge_or {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n (d + 1)) (x : BitString n) : eval AltOp.or (merge fs) x = true ↔ ∃ (i : ι), eval AltOp.or (fs i) x = true

theorem Cslib.Circuits.Boolean.AltFormula.size_merge_le {n d : ℕ} {ι : Type u_1} [Fintype ι] (fs : ι → AltFormula n (d + 1)) : (merge fs).size ≤ 1 + ∑ i : ι, (fs i).size

def Cslib.Circuits.Boolean.AltFormula.constant (n d : ℕ) (op : AltOp) (b : Bool) : AltFormula n (d + 2)

A constant, as an alternating formula of any depth at least two.

theorem Cslib.Circuits.Boolean.AltFormula.eval_constant (n d : ℕ) (op : AltOp) (b : Bool) (x : BitString n) : eval op (constant n d op b) x = b

theorem Cslib.Circuits.Boolean.AltFormula.size_constant_le (n d : ℕ) (op : AltOp) (b : Bool) : (constant n d op b).size ≤ 2

noncomputable def Cslib.Circuits.Boolean.AltFormula.excludingClause {n : ℕ} (y : BitString n) : AltFormula n 1

The clause excluding exactly the input y.

theorem Cslib.Circuits.Boolean.AltFormula.eval_excludingClause {n : ℕ} (y x : BitString n) : eval AltOp.or (excludingClause y) x = true ↔ x ≠ y

theorem Cslib.Circuits.Boolean.AltFormula.size_excludingClause {n : ℕ} (y : BitString n) : (excludingClause y).size = 1

noncomputable def Cslib.Circuits.Boolean.AltFormula.cnf {n : ℕ} (f : BitString n → Bool) : AltFormula n 2

The formula in conjunctive normal form excluding every false input of f.

theorem Cslib.Circuits.Boolean.AltFormula.eval_cnf {n : ℕ} (f : BitString n → Bool) (x : BitString n) : eval AltOp.and (cnf f) x = f x

theorem Cslib.Circuits.Boolean.AltFormula.size_cnf_le {n : ℕ} (f : BitString n → Bool) : (cnf f).size ≤ 2 ^ n + 1

theorem Cslib.Circuits.Boolean.AltFormula.exists_depth_two {n : ℕ} (f : BitString n → Bool) (op : AltOp) : ∃ (g : AltFormula n 2), g.size ≤ 2 ^ n + 1 ∧ ∀ (x : BitString n), eval op g x = f x

Normal forms: every Boolean function has alternating formulas of depth two, with either root operation, of size at most 2 ^ n + 1.

Alternating formulas as circuits

def Cslib.Circuits.Boolean.AltFormula.toFormula {n d : ℕ} : AltOp → AltFormula n d → Formula Unbounded.signature (n + n)

An alternating formula as a formula over the unbounded fan-in basis, on the positive inputs 0, …, n - 1 followed by the negated inputs n, …, 2 n - 1.

def Cslib.Circuits.Boolean.AltFormula.literals {n : ℕ} (x : BitString n) : BitString (n + n)

The positive inputs followed by the negated inputs.

theorem Cslib.Circuits.Boolean.AltFormula.eval_toFormula {n d : ℕ} (op : AltOp) (f : AltFormula n d) (x : BitString n) : (toFormula op f).eval Unbounded.interpretation (literals x) = eval op f x

theorem Cslib.Circuits.Boolean.AltFormula.size_toFormula {n d : ℕ} (op : AltOp) (f : AltFormula n d) : (toFormula op f).size = f.size

theorem Cslib.Circuits.Boolean.AltFormula.depth_toFormula_le {n d : ℕ} (op : AltOp) (f : AltFormula n d) : (toFormula op f).depth ≤ d

theorem Cslib.Circuits.Boolean.AltFormula.depthWith_toFormula_le {n d : ℕ} (op : AltOp) (f : AltFormula n d) : Formula.depthWith Unbounded.andOrCost (toFormula op f) ≤ d

def Cslib.Circuits.Boolean.AltFormula.literalsCircuit (n : ℕ) : Circuit Unbounded.signature n (n + n)

The circuit computing the positive and the negated inputs, with one negation gate per input.

theorem Cslib.Circuits.Boolean.AltFormula.eval_literalsCircuit {n : ℕ} (x : BitString n) : (literalsCircuit n).eval Unbounded.interpretation x = literals x

theorem Cslib.Circuits.Boolean.AltFormula.size_literalsCircuit (n : ℕ) : (literalsCircuit n).size = n

def Cslib.Circuits.Boolean.AltFormula.deMorganLiteralsCircuit (n : ℕ) : Circuit signature n (n + n)

The circuit computing the positive and the negated inputs over the De Morgan basis, with one negation gate per input.

theorem Cslib.Circuits.Boolean.AltFormula.eval_deMorganLiteralsCircuit {n : ℕ} (x : BitString n) : (deMorganLiteralsCircuit n).eval interpretation x = literals x

theorem Cslib.Circuits.Boolean.AltFormula.size_deMorganLiteralsCircuit (n : ℕ) : (deMorganLiteralsCircuit n).size = n

theorem Cslib.Circuits.Boolean.AltFormula.depth_literalsCircuit_le (n : ℕ) : (literalsCircuit n).depth ≤ 1

theorem Cslib.Circuits.Boolean.AltFormula.depthWith_literalsCircuit (n : ℕ) : Circuit.depthWith Unbounded.andOrCost (literalsCircuit n) = 0

Negations are free in the AND/OR depth, so the literals have AND/OR depth zero.

theorem Cslib.Circuits.Boolean.AltFormula.exists_circuit {n d : ℕ} (op : AltOp) (f : AltFormula n d) : ∃ (c : Circuit Unbounded.signature n 1), c.Computes Unbounded.interpretation (single (eval op f)) ∧ Circuit.depthWith Unbounded.andOrCost c ≤ d ∧ c.depth ≤ d + 1 ∧ c.size = f.size + n

Alternating formulas are circuits: an alternating formula of depth d computing f with root op is a circuit over the unbounded fan-in basis of AND/OR depth at most d, and of depth at most d + 1 counting negations, with at most n more gates, negating every input first.