Documentation

Cslib.Computability.Circuit.Boolean.Basic

Boolean circuits #

The De Morgan basis consists of binary AND and OR, unary NOT, and Boolean constants. Every gate has fan-in at most two, so these are the usual bounded fan-in Boolean circuits (Program.fanInAtMost_two). Circuit size counts every gate, including constants; designated output wires are free.

source
inductive Cslib.Circuits.Boolean.Op :
Type

Operations of the De Morgan basis, including constants.

  • const (value : Bool) : Op

    A Boolean constant.

  • not : Op

    Negation.

  • and : Op

    Binary conjunction.

  • or : Op

    Binary disjunction.

Instances For
    source
    def Cslib.Circuits.Boolean.instDecidableEqOp.decEq (x✝ x✝¹ : Op) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance Cslib.Circuits.Boolean.instDecidableEqOp :
      DecidableEq Op
      source
      @[instance_reducible]
      instance Cslib.Circuits.Boolean.instFintypeOp :
      Fintype Op
      source
      @[simp]
      theorem Cslib.Circuits.Boolean.Op.card :
      Fintype.card Op = 5

      The De Morgan basis has five operation symbols, counting its two constants.

      source
      @[reducible, inline]
      abbrev Cslib.Circuits.Boolean.signature :
      Signature

      The De Morgan signature.

      Instances For
        source
        def Cslib.Circuits.Boolean.interpretation :
        Interpretation signature Bool

        The usual Boolean interpretation.

        Instances For
          source
          theorem Cslib.Circuits.Program.fanInAtMost_two {n g : ℕ} (p : Program Boolean.signature n g) :
          p.FanInAtMost 2

          Every De Morgan program has fan-in at most two.

          source
          theorem Cslib.Circuits.Circuit.fanInAtMost_two {n o : ℕ} (c : Circuit Boolean.signature n o) :
          c.FanInAtMost 2

          Every De Morgan circuit has fan-in at most two.