Documentation

Complexity.Computability.Circuit.Monotone.Formula

Monotone formulas #

A monotone formula is a formula over the monotone basis, Formula Monotone.signature n, evaluated under Monotone.interpretation: a tree of AND and OR gates of fan-in two whose leaves are inputs and Boolean constants (Monotone.const, Monotone.and, Monotone.or). Every function it computes is monotone (monotone_eval), and every monotone function has one: the disjunction, over the inputs z where the function is true, of the conjunction of the bits that are one in z (exists_computes_of_monotone). Unlike De Morgan formulas, monotone formulas thus compute only some Boolean functions, so the least depth of a monotone formula for f is extended-valued: eformulaDepth f, the least depth with constants free (Formula.minDepthWith for binaryCost), is ⊤ when no monotone formula computes f, that is, when f is not monotone (eformulaDepth_ne_top_iff). A monotone formula is a De Morgan formula (Formula.mapOp along toDeMorgan), so the De Morgan formula depth is at most the monotone one (formulaDepth_le_eformulaDepth).

Main definitions #

Main results #

References #

Constructors #

source
def Cslib.Circuits.Monotone.const {n : ℕ} (b : Bool) :
Formula signature n

The constant monotone formula.

Instances For
    source
    def Cslib.Circuits.Monotone.and {n : ℕ} (F G : Formula signature n) :
    Formula signature n

    The conjunction of two monotone formulas.

    Instances For
      source
      def Cslib.Circuits.Monotone.or {n : ℕ} (F G : Formula signature n) :
      Formula signature n

      The disjunction of two monotone formulas.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.eval_const {n : ℕ} (x : BitString n) (b : Bool) :
        (const b).eval interpretation x = b
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.eval_and {n : ℕ} (F G : Formula signature n) (x : BitString n) :
        (and F G).eval interpretation x = (F.eval interpretation x && G.eval interpretation x)
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.eval_or {n : ℕ} (F G : Formula signature n) (x : BitString n) :
        (or F G).eval interpretation x = (F.eval interpretation x || G.eval interpretation x)
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.depthWith_const {n : ℕ} (cost : Op → ℕ) (b : Bool) :
        Formula.depthWith cost (const b) = cost (Op.const b)
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.depthWith_and {n : ℕ} (F G : Formula signature n) (cost : Op → ℕ) :
        Formula.depthWith cost (and F G) = max (Formula.depthWith cost F) (Formula.depthWith cost G) + cost Op.and
        source
        @[simp]
        theorem Cslib.Circuits.Monotone.depthWith_or {n : ℕ} (F G : Formula signature n) (cost : Op → ℕ) :
        Formula.depthWith cost (or F G) = max (Formula.depthWith cost F) (Formula.depthWith cost G) + cost Op.or

        Monotone functions #

        source
        theorem Cslib.Circuits.Monotone.monotone_eval {n : ℕ} (F : Formula signature n) :
        Monotone (F.eval interpretation)

        Monotone formulas compute monotone functions.

        source
        theorem Cslib.Circuits.Monotone.exists_computes_of_monotone {n : ℕ} {f : BooleanFunction n} (hf : Monotone f) :
        ∃ (F : Formula signature n), F.Computes interpretation f

        Every monotone function has a monotone formula: the disjunction, over the inputs z where it is true, of the conjunction of the bits that are one in z.

        source
        theorem Cslib.Circuits.Monotone.exists_computes_iff_monotone {n : ℕ} {f : BooleanFunction n} :
        (∃ (F : Formula signature n), F.Computes interpretation f) ↔ Monotone f

        A Boolean function has a monotone formula exactly when it is monotone.

        Depth #

        source
        @[reducible, inline]
        noncomputable abbrev Cslib.Circuits.Monotone.eformulaDepth {n : ℕ} (f : BooleanFunction n) :
        ℕ∞

        The least depth of a monotone formula computing f, with constants free, or ⊤ if no monotone formula computes f: the least depth with costs binaryCost (Formula.minDepthWith), whose API applies to it.

        Instances For
          source
          theorem Cslib.Circuits.Monotone.eformulaDepth_ne_top_iff {n : ℕ} {f : BooleanFunction n} :
          eformulaDepth f ≠ ⊤ ↔ Monotone f

          The monotone formula depth of a function is finite exactly when the function is monotone.

          source
          theorem Cslib.Circuits.Monotone.formulaDepth_le_eformulaDepth {n : ℕ} (f : BooleanFunction n) :
          ↑(Boolean.formulaDepth f) ≤ eformulaDepth f

          A monotone formula is a De Morgan formula of the same depth, so De Morgan formulas are at most as deep as monotone ones.