Monotone Boolean formulas -- definitions

This file defines a typed formula tree containing variables, conjunctions, and disjunctions only. Constants and negations are deliberately absent: this is the standard syntax used by the Karchmer--Wigderson correspondence.

inductive Complexity.MonotoneFormula (N : ℕ) : Type

A monotone Boolean formula over exactly N input variables.

• var {N : ℕ} (index : Fin N) : MonotoneFormula N

  An input variable.

• conj {N : ℕ} (left right : MonotoneFormula N) : MonotoneFormula N

  Conjunction.

• disj {N : ℕ} (left right : MonotoneFormula N) : MonotoneFormula N

  Disjunction.

@[implicit_reducible]

instance Complexity.instReprMonotoneFormula {N✝ : ℕ} : Repr (MonotoneFormula N✝)

Equations

• Complexity.instReprMonotoneFormula = { reprPrec := Complexity.instReprMonotoneFormula.repr }

def Complexity.instReprMonotoneFormula.repr {N✝ : ℕ} : MonotoneFormula N✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Complexity.instDecidableEqMonotoneFormula {N✝ : ℕ} : DecidableEq (MonotoneFormula N✝)

Equations

• Complexity.instDecidableEqMonotoneFormula = Complexity.instDecidableEqMonotoneFormula.decEq

def Complexity.instDecidableEqMonotoneFormula.decEq {N✝ : ℕ} (x✝ x✝¹ : MonotoneFormula N✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.instDecidableEqMonotoneFormula.decEq (Complexity.MonotoneFormula.var a) (Complexity.MonotoneFormula.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (Complexity.MonotoneFormula.var index) (left.conj right) = isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (Complexity.MonotoneFormula.var index) (left.disj right) = isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (left.conj right) (Complexity.MonotoneFormula.var index) = isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (left.conj right) (left_1.disj right_1) = isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (left.disj right) (Complexity.MonotoneFormula.var index) = isFalse ⋯
• Complexity.instDecidableEqMonotoneFormula.decEq (left.disj right) (left_1.conj right_1) = isFalse ⋯

def Complexity.MonotoneFormula.eval {N : ℕ} (input : BitString N) : MonotoneFormula N → Bool

Evaluate a monotone formula.

Equations

• Complexity.MonotoneFormula.eval input (Complexity.MonotoneFormula.var index) = input index
• Complexity.MonotoneFormula.eval input (left.conj right) = (Complexity.MonotoneFormula.eval input left && Complexity.MonotoneFormula.eval input right)
• Complexity.MonotoneFormula.eval input (left.disj right) = (Complexity.MonotoneFormula.eval input left || Complexity.MonotoneFormula.eval input right)

def Complexity.MonotoneFormula.size {N : ℕ} : MonotoneFormula N → ℕ

Total tree-node count.

Equations

• (Complexity.MonotoneFormula.var index).size = 1
• (left.conj right).size = left.size + right.size + 1
• (left.disj right).size = left.size + right.size + 1

def Complexity.MonotoneFormula.leaves {N : ℕ} : MonotoneFormula N → ℕ

Number of variable leaves, counting repeated occurrences.

Equations

• (Complexity.MonotoneFormula.var index).leaves = 1
• (left.conj right).leaves = left.leaves + right.leaves
• (left.disj right).leaves = left.leaves + right.leaves

def Complexity.MonotoneFormula.depth {N : ℕ} : MonotoneFormula N → ℕ

Longest root-to-leaf path, with variables at depth zero.

Equations

• (Complexity.MonotoneFormula.var index).depth = 0
• (left.conj right).depth = max left.depth right.depth + 1
• (left.disj right).depth = max left.depth right.depth + 1

def Complexity.MonotoneFormula.vars {N : ℕ} : MonotoneFormula N → Finset (Fin N)

The set of variables occurring in the formula.

Equations

• (Complexity.MonotoneFormula.var index).vars = {index}
• (left.conj right).vars = left.vars ∪ right.vars
• (left.disj right).vars = left.vars ∪ right.vars

def Complexity.MonotoneFormula.Computes {N : ℕ} (formula : MonotoneFormula N) (function : BitString N → Bool) : Prop

Whether a formula computes a given single-output Boolean function.

Equations

• formula.Computes function = ∀ (input : Complexity.BitString N), Complexity.MonotoneFormula.eval input formula = function input

def Complexity.MonotoneFormula.toBoolFormula {N : ℕ} : MonotoneFormula N → BoolFormula

Erase finite-index proofs and view a monotone formula as a general BoolFormula.

Equations

• (Complexity.MonotoneFormula.var index).toBoolFormula = Complexity.BoolFormula.var ↑index
• (left.conj right).toBoolFormula = left.toBoolFormula.conj right.toBoolFormula
• (left.disj right).toBoolFormula = left.toBoolFormula.disj right.toBoolFormula

def Complexity.BitString.PointwiseLE {N : ℕ} (x y : BitString N) : Prop

Pointwise Boolean order, written as the implication x_i = 1 → y_i = 1 at every coordinate.

Equations

• x.PointwiseLE y = ∀ (index : Fin N), x index = true → y index = true

def Complexity.IsMonotoneBoolFun {N : ℕ} (function : BitString N → Bool) : Prop

A single-output Boolean function is monotone in the pointwise Boolean order.

Equations

• Complexity.IsMonotoneBoolFun function = ∀ ⦃x y : Complexity.BitString N⦄, x.PointwiseLE y → function x = true → function y = true