De Morgan formulas

A De Morgan formula is a formula over the De Morgan signature, Formula Boolean.signature n, evaluated under Boolean.interpretation. Negations may appear anywhere. Pushing them to the leaves by De Morgan's laws does not change the leaf size, so lower bounds on the leaf size of these formulas are at least as strong as for formulas whose negations sit at the leaves Jukna, Chapter 6.

Main definitions

• Cslib.Circuits.Formula.const, Cslib.Circuits.Formula.not, Cslib.Circuits.Formula.and, Cslib.Circuits.Formula.or: De Morgan formulas built from constants and smaller formulas.
• Cslib.Circuits.Formula.xor: the exclusive or (F ∧ ¬G) ∨ (¬F ∧ G).
• Cslib.Circuits.Formula.orList, Cslib.Circuits.Formula.andList: the disjunction and the conjunction of a list of formulas as balanced trees of binary gates (Formula.balanced).
• Cslib.Circuits.Boolean.formulaDepth: the least depth of a De Morgan formula for a function, with negations and constants free.

Main results

• Cslib.Circuits.Formula.size_orList_add_one, Cslib.Circuits.Formula.depthWith_orList_le, Cslib.Circuits.Formula.size_andList_add_one, Cslib.Circuits.Formula.depthWith_andList_le: a balanced tree of k ≥ 1 formulas adds k - 1 nodes and ⌈log₂ k⌉ levels.
• Cslib.Circuits.Formula.exists_computes: every Boolean function has a De Morgan formula.
• Cslib.Circuits.Boolean.exists_computes_depthWith_eq_formulaDepth: some formula attains the formula depth.
• Cslib.Circuits.Boolean.arity_le_two: the De Morgan basis has fan-in at most two.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Formula.const {n : ℕ} (c : Bool) : Formula Boolean.signature n

The constant De Morgan formula.

def Cslib.Circuits.Formula.not {n : ℕ} (F : Formula Boolean.signature n) : Formula Boolean.signature n

The negation of a De Morgan formula.

def Cslib.Circuits.Formula.and {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The conjunction of two De Morgan formulas.

def Cslib.Circuits.Formula.or {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The disjunction of two De Morgan formulas.

def Cslib.Circuits.Formula.xor {n : ℕ} (F G : Formula Boolean.signature n) : Formula Boolean.signature n

The exclusive or of two De Morgan formulas, (F ∧ ¬G) ∨ (¬F ∧ G).

@[simp]

theorem Cslib.Circuits.Formula.eval_const {n : ℕ} (x : BitString n) (c : Bool) : (const c).eval Boolean.interpretation x = c

@[simp]

theorem Cslib.Circuits.Formula.eval_not {n : ℕ} (F : Formula Boolean.signature n) (x : BitString n) : F.not.eval Boolean.interpretation x = !F.eval Boolean.interpretation x

@[simp]

theorem Cslib.Circuits.Formula.eval_and {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.and G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x && G.eval Boolean.interpretation x)

@[simp]

theorem Cslib.Circuits.Formula.eval_or {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.or G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x || G.eval Boolean.interpretation x)

@[simp]

theorem Cslib.Circuits.Formula.eval_xor {n : ℕ} (F G : Formula Boolean.signature n) (x : BitString n) : (F.xor G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x ^^ G.eval Boolean.interpretation x)

@[simp]

theorem Cslib.Circuits.Formula.leafSize_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.leafSize = F.leafSize

@[simp]

theorem Cslib.Circuits.Formula.leafSize_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).leafSize = F.leafSize + G.leafSize

@[simp]

theorem Cslib.Circuits.Formula.leafSize_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).leafSize = F.leafSize + G.leafSize

@[simp]

theorem Cslib.Circuits.Formula.leafSize_xor {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).leafSize = 2 * F.leafSize + 2 * G.leafSize

@[simp]

theorem Cslib.Circuits.Formula.leafSize_const {n : ℕ} (c : Bool) : (const c).leafSize = 0

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_const {n : ℕ} (Y : Finset (Fin n)) (c : Bool) : leafSizeIn Y (const c) = 0

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_not {n : ℕ} (F : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y F.not = leafSizeIn Y F

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_and {n : ℕ} (F G : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y (F.and G) = leafSizeIn Y F + leafSizeIn Y G

@[simp]

theorem Cslib.Circuits.Formula.leafSizeIn_or {n : ℕ} (F G : Formula Boolean.signature n) (Y : Finset (Fin n)) : leafSizeIn Y (F.or G) = leafSizeIn Y F + leafSizeIn Y G

@[simp]

theorem Cslib.Circuits.Formula.size_const {n : ℕ} (c : Bool) : (const c).size = 1

A constant is one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.size = F.size + 1

A negation adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).size = F.size + G.size + 1

A conjunction adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).size = F.size + G.size + 1

A disjunction adds one operation node.

@[simp]

theorem Cslib.Circuits.Formula.size_xor {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).size = 2 * F.size + 2 * G.size + 5

Exclusive or uses two copies of each argument and five operation nodes.

@[simp]

theorem Cslib.Circuits.Formula.depth_const {n : ℕ} (c : Bool) : (const c).depth = 1

A constant has depth one.

@[simp]

theorem Cslib.Circuits.Formula.depth_not {n : ℕ} (F : Formula Boolean.signature n) : F.not.depth = F.depth + 1

A negation is one deeper than its argument.

@[simp]

theorem Cslib.Circuits.Formula.depth_and {n : ℕ} (F G : Formula Boolean.signature n) : (F.and G).depth = max F.depth G.depth + 1

A conjunction is one deeper than the deeper conjunct.

@[simp]

theorem Cslib.Circuits.Formula.depth_or {n : ℕ} (F G : Formula Boolean.signature n) : (F.or G).depth = max F.depth G.depth + 1

A disjunction is one deeper than the deeper disjunct.

theorem Cslib.Circuits.Formula.depth_xor_le {n : ℕ} (F G : Formula Boolean.signature n) : (F.xor G).depth ≤ max F.depth G.depth + 3

Exclusive or adds at most three levels beyond its deeper argument.

@[simp]

theorem Cslib.Circuits.Formula.depthWith_const {n : ℕ} (cost : Boolean.Op → ℕ) (c : Bool) : depthWith cost (const c) = cost (Boolean.Op.const c)

@[simp]

theorem Cslib.Circuits.Formula.depthWith_not {n : ℕ} (F : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost F.not = depthWith cost F + cost Boolean.Op.not

@[simp]

theorem Cslib.Circuits.Formula.depthWith_and {n : ℕ} (F G : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost (F.and G) = max (depthWith cost F) (depthWith cost G) + cost Boolean.Op.and

@[simp]

theorem Cslib.Circuits.Formula.depthWith_or {n : ℕ} (F G : Formula Boolean.signature n) (cost : Boolean.Op → ℕ) : depthWith cost (F.or G) = max (depthWith cost F) (depthWith cost G) + cost Boolean.Op.or

@[simp]

theorem Cslib.Circuits.Formula.gate₂_and {n : ℕ} (F G : Formula Boolean.signature n) : gate₂ Boolean.Op.and ⋯ F G = F.and G

A conjunction is the binary node of .and.

@[simp]

theorem Cslib.Circuits.Formula.gate₂_or {n : ℕ} (F G : Formula Boolean.signature n) : gate₂ Boolean.Op.or ⋯ F G = F.or G

A disjunction is the binary node of .or.

def Cslib.Circuits.Formula.orList {n : ℕ} (l : List (Formula Boolean.signature n)) : Formula Boolean.signature n

The disjunction of a list of De Morgan formulas, as a balanced tree (Formula.balanced); the constant false for no formulas.

def Cslib.Circuits.Formula.andList {n : ℕ} (l : List (Formula Boolean.signature n)) : Formula Boolean.signature n

The conjunction of a list of De Morgan formulas, as a balanced tree (Formula.balanced); the constant true for no formulas.

@[simp]

theorem Cslib.Circuits.Formula.eval_orList {n : ℕ} (x : BitString n) (l : List (Formula Boolean.signature n)) : (orList l).eval Boolean.interpretation x = l.any fun (F : Formula Boolean.signature n) => F.eval Boolean.interpretation x

@[simp]

theorem Cslib.Circuits.Formula.eval_andList {n : ℕ} (x : BitString n) (l : List (Formula Boolean.signature n)) : (andList l).eval Boolean.interpretation x = l.all fun (F : Formula Boolean.signature n) => F.eval Boolean.interpretation x

@[simp]

theorem Cslib.Circuits.Formula.orList_nil {n : ℕ} : orList [] = const false

The disjunction of no formulas is the constant false.

@[simp]

theorem Cslib.Circuits.Formula.orList_singleton {n : ℕ} (F : Formula Boolean.signature n) : orList [F] = F

The disjunction of one formula is that formula.

@[simp]

theorem Cslib.Circuits.Formula.andList_nil {n : ℕ} : andList [] = const true

The conjunction of no formulas is the constant true.

@[simp]

theorem Cslib.Circuits.Formula.andList_singleton {n : ℕ} (F : Formula Boolean.signature n) : andList [F] = F

The conjunction of one formula is that formula.

theorem Cslib.Circuits.Formula.size_orList_add_one {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : l ≠ []) : (orList l).size + 1 = (List.map size l).sum + l.length

A balanced disjunction of k ≥ 1 formulas has k - 1 operation nodes besides theirs.

theorem Cslib.Circuits.Formula.size_andList_add_one {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : l ≠ []) : (andList l).size + 1 = (List.map size l).sum + l.length

A balanced conjunction of k ≥ 1 formulas has k - 1 operation nodes besides theirs.

theorem Cslib.Circuits.Formula.depthWith_orList_le {n : ℕ} {cost : Boolean.Op → ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith cost F ≤ d) (hnil : l = [] → cost (Boolean.Op.const false) ≤ d) : depthWith cost (orList l) ≤ d + cost Boolean.Op.or * Nat.clog 2 l.length

A balanced disjunction is deeper than its disjuncts by ⌈log₂⌉ of their number times the cost of a disjunction; the disjunction of no formulas is a constant.

theorem Cslib.Circuits.Formula.depthWith_andList_le {n : ℕ} {cost : Boolean.Op → ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith cost F ≤ d) (hnil : l = [] → cost (Boolean.Op.const true) ≤ d) : depthWith cost (andList l) ≤ d + cost Boolean.Op.and * Nat.clog 2 l.length

A balanced conjunction is deeper than its conjuncts by ⌈log₂⌉ of their number times the cost of a conjunction; the conjunction of no formulas is a constant.

theorem Cslib.Circuits.Formula.depthWith_binaryCost_orList_le {n : ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith Boolean.binaryCost F ≤ d) : depthWith Boolean.binaryCost (orList l) ≤ d + Nat.clog 2 l.length

With negations and constants free, a balanced disjunction is deeper than its disjuncts by ⌈log₂⌉ of their number.

theorem Cslib.Circuits.Formula.depthWith_binaryCost_andList_le {n : ℕ} {l : List (Formula Boolean.signature n)} {d : ℕ} (hl : ∀ F ∈ l, depthWith Boolean.binaryCost F ≤ d) : depthWith Boolean.binaryCost (andList l) ≤ d + Nat.clog 2 l.length

With negations and constants free, a balanced conjunction is deeper than its conjuncts by ⌈log₂⌉ of their number.

def Cslib.Circuits.Formula.literal {n : ℕ} (z : BitString n) (i : Fin n) : Formula Boolean.signature n

The literal of bit i that is true at z.

@[simp]

theorem Cslib.Circuits.Formula.eval_literal {n : ℕ} (x z : BitString n) (i : Fin n) : (literal z i).eval Boolean.interpretation x = (x i == z i)

@[simp]

theorem Cslib.Circuits.Formula.depthWith_literal {n : ℕ} (z : BitString n) (i : Fin n) : depthWith Boolean.binaryCost (literal z i) = 0

theorem Cslib.Circuits.Formula.exists_computes {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula Boolean.signature n), F.Computes Boolean.interpretation f

Every Boolean function has a De Morgan formula: its disjunctive normal form.

theorem Cslib.Circuits.Boolean.arity_le_two (op : Op) : signature.Arity op ≤ 2

The De Morgan basis has fan-in at most two.

noncomputable def Cslib.Circuits.Boolean.formulaDepth {n : ℕ} (f : BooleanFunction n) : ℕ

The least depth of a De Morgan formula computing f, with negations and constants free: the least depth with costs binaryCost (Formula.minDepthWith), which is finite because every function has a formula (Formula.exists_computes).

@[simp]

theorem Cslib.Circuits.Boolean.natCast_formulaDepth {n : ℕ} (f : BooleanFunction n) : ↑(formulaDepth f) = Formula.minDepthWith interpretation binaryCost f

The formula depth is the least depth with costs binaryCost.

theorem Cslib.Circuits.Boolean.formulaDepth_le {n : ℕ} {f : BooleanFunction n} {F : Formula signature n} (hF : F.Computes interpretation f) : formulaDepth f ≤ Formula.depthWith binaryCost F

The formula depth is at most the depth of every formula computing the function.

theorem Cslib.Circuits.Boolean.exists_computes_depthWith_eq_formulaDepth {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula signature n), F.Computes interpretation f ∧ Formula.depthWith binaryCost F = formulaDepth f

Some formula attains the formula depth.