Documentation

Complexity.Computability.Circuit.Boolean.BinaryCost

Counting the binary gates of De Morgan circuits #

The size of a De Morgan circuit counts every gate. The usual measure for lower bounds charges only the AND and OR gates and lets negations and constants be free Jukna, Section 1.2. It is the cost of a program for binaryCost, and it is at most the size (Program.cost_binaryCost_le).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.Op.IsBinary (op : Op) :
Prop

The binary operations of the De Morgan basis, AND and OR.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Circuits.Boolean.instDecidablePredOpIsBinary :
    DecidablePred Op.IsBinary
    source
    theorem Cslib.Circuits.Boolean.Op.isBinary_iff {op : Op} :
    op.IsBinary ↔ op = and ∨ op = or
    source
    theorem Cslib.Circuits.Boolean.Op.isBinary_and :
    and.IsBinary
    source
    theorem Cslib.Circuits.Boolean.Op.isBinary_or :
    or.IsBinary
    source
    theorem Cslib.Circuits.Boolean.Op.IsBinary.val_lt_two {op : Op} (h : op.IsBinary) (s : Fin (signature.Arity op)) :
    ↑s < 2

    The arguments of a binary operation are numbered 0 and 1.

    source
    theorem Cslib.Circuits.Boolean.Op.IsBinary.eq_or_eq {op : Op} (h : op.IsBinary) {s t : Fin (signature.Arity op)} (hst : s ≠ t) (u : Fin (signature.Arity op)) :
    u = s ∨ u = t

    Two different arguments of a binary operation are all of its arguments.

    source
    def Cslib.Circuits.Boolean.binaryCost :
    Op → ℕ

    The cost function charging one for each AND and OR gate and nothing for negations and constants. Its counterparts for the other bases are Monotone.binaryCost, its restriction to the monotone basis (Monotone.binaryCost_toDeMorgan), and Unbounded.andOrCost, which also charges the constants of the unbounded fan-in basis, its AND and OR gates of no arguments.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.binaryCost_and :
      binaryCost Op.and = 1
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.binaryCost_or :
      binaryCost Op.or = 1
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.binaryCost_not :
      binaryCost Op.not = 0
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.binaryCost_const (b : Bool) :
      binaryCost (Op.const b) = 0
      source
      theorem Cslib.Circuits.Boolean.binaryCost_le_one (op : Op) :
      binaryCost op ≤ 1
      source
      theorem Cslib.Circuits.Boolean.binaryCost_eq_ite (op : Op) :
      binaryCost op = if op.IsBinary then 1 else 0
      source
      theorem Cslib.Circuits.Program.cost_binaryCost_le {n g : ℕ} (p : Program Boolean.signature n g) :
      p.cost Boolean.binaryCost ≤ g

      The number of binary gates of a program is at most its number of gates.