Documentation

Complexitylib.Algebraic.Basis.Binary.Formula

Formulas over the full binary basis #

A formula is a tree whose leaves are input variables or constants and whose internal nodes apply one of the sixteen binary Boolean functions. Its size is its number of variable leaves, the standard leaf-size measure; constants are free, as they can be absorbed into the adjacent gate.

leavesIn Y counts the variable leaves whose index lies in a block Y. Over pairwise disjoint blocks these counts add up to at most the total leaf count (sum_leavesIn_le_leaves), and a formula with no leaf in Y does not depend on the coordinates in Y (eval_eq_of_leavesIn_eq_zero). These are the two facts Nechiporuk's argument uses.

source
inductive Algebraic.Binary.Formula (n : ℕ) :
Type

A formula over the full binary basis.

Instances For
    source
    def Algebraic.Binary.Formula.eval {n : ℕ} :
    Formula n → (Fin n → Bool) → Bool

    Evaluate a formula on an input.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.Binary.Formula.eval_var {n : ℕ} (index : Fin n) (input : Fin n → Bool) :
      (var index).eval input = input index
      source
      @[simp]
      theorem Algebraic.Binary.Formula.eval_const {n : ℕ} (value : Bool) (input : Fin n → Bool) :
      (const value).eval input = value
      source
      @[simp]
      theorem Algebraic.Binary.Formula.eval_gate {n : ℕ} (op : Op) (left right : Formula n) (input : Fin n → Bool) :
      (gate op left right).eval input = op (left.eval input) (right.eval input)
      source
      def Algebraic.Binary.Formula.leaves {n : ℕ} :
      Formula n → ℕ

      The number of variable leaves: the leaf size of the formula. Constant leaves count 0. This differs from Algebraic.KW.Formula.leaves, which also counts constant leaves (so there every formula has leaf size at least 1); the Nechiporuk and cutwidth bounds use this convention.

      Equations
      Instances For
        source
        def Algebraic.Binary.Formula.leavesIn {n : ℕ} (Y : Finset (Fin n)) :
        Formula n → ℕ

        The number of variable leaves whose index lies in Y.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.Binary.Formula.leavesIn_var {n : ℕ} (Y : Finset (Fin n)) (index : Fin n) :
          leavesIn Y (var index) = if index ∈ Y then 1 else 0
          source
          @[simp]
          theorem Algebraic.Binary.Formula.leavesIn_const {n : ℕ} (Y : Finset (Fin n)) (value : Bool) :
          leavesIn Y (const value) = 0
          source
          @[simp]
          theorem Algebraic.Binary.Formula.leavesIn_gate {n : ℕ} (Y : Finset (Fin n)) (op : Op) (left right : Formula n) :
          leavesIn Y (gate op left right) = leavesIn Y left + leavesIn Y right
          source
          def Algebraic.Binary.Formula.Computes {n : ℕ} (F : Formula n) (f : Cslib.BooleanFunction n) :
          Prop

          A formula computes f when it agrees with f on every input.

          Equations
          Instances For
            source
            theorem Algebraic.Binary.Formula.Computes.eval_eq {n : ℕ} {F : Formula n} {f : Cslib.BooleanFunction n} (h : F.Computes f) :
            F.eval = f
            source
            theorem Algebraic.Binary.Formula.leavesIn_le_leaves {n : ℕ} (Y : Finset (Fin n)) (F : Formula n) :
            leavesIn Y F ≤ F.leaves
            source
            theorem Algebraic.Binary.Formula.sum_leavesIn_le_leaves {n k : ℕ} (Y : Fin k → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin k) => Disjoint (Y i) (Y j)) (F : Formula n) :
            ∑ i : Fin k, leavesIn (Y i) F ≤ F.leaves

            Over pairwise disjoint blocks, the block leaf counts add up to at most the leaf size.

            source
            theorem Algebraic.Binary.Formula.eval_eq_of_leavesIn_eq_zero {n : ℕ} {Y : Finset (Fin n)} {x x' : Fin n → Bool} (agree : ∀ i ∉ Y, x i = x' i) (F : Formula n) :
            leavesIn Y F = 0 → F.eval x = F.eval x'

            A formula without leaves in Y ignores the coordinates in Y.