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
@[reducible, inline]
abbrev Cslib.Circuits.Boolean.BooleanFunction (n : ℕ) :
Type

Boolean functions on n inputs.

Equations
Instances For
    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
      @[instance_reducible]
      instance Cslib.Circuits.Boolean.instDecidableEqOp :
      DecidableEq Op
      Equations
      source
      def Cslib.Circuits.Boolean.instDecidableEqOp.decEq (x✝ x✝¹ : Op) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Circuits.Boolean.signature :
        Signature

        The De Morgan signature.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cslib.Circuits.Boolean.interpretation :
          Interpretation signature Bool

          The usual Boolean interpretation.

          Equations
          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 g o : ℕ} (c : Circuit Boolean.signature n g o) :
            c.FanInAtMost 2

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