Documentation

Complexity.Computability.Circuit.Monotone.Basic

Monotone circuits #

The monotone basis has the Boolean constants, binary conjunction and binary disjunction: the De Morgan basis (Cslib.Circuits.Boolean.signature) without negation. Each of its operations is monotone (interpretation_mono), and so is every function computed by a monotone circuit. The depth of monotone formulas charges AND and OR gates and lets constants be free (binaryCost), as for De Morgan formulas, and the monotone basis maps into the De Morgan basis (toDeMorgan) keeping meanings and these costs (binaryCost_toDeMorgan).

Main definitions #

Main results #

References #

source
inductive Cslib.Circuits.Monotone.Op :
Type

Operations of the monotone basis.

  • const (b : Bool) : Op

    A Boolean constant.

  • and : Op

    Binary conjunction.

  • or : Op

    Binary disjunction.

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

      Finite enumeration of the monotone basis operations Op.

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

      The monotone signature: constants, binary conjunction and binary disjunction.

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

        The Boolean interpretation of the monotone basis.

        Instances For
          source
          @[simp]
          theorem Cslib.Circuits.Monotone.interpretation_const (b : Bool) (x : Fin 0 → Bool) :
          interpretation (Op.const b) x = b

          Under interpretation, .const b evaluates to b.

          source
          @[simp]
          theorem Cslib.Circuits.Monotone.interpretation_and (x : Fin 2 → Bool) :
          interpretation Op.and x = (x 0 && x 1)

          Under interpretation, .and evaluates to x 0 && x 1.

          source
          @[simp]
          theorem Cslib.Circuits.Monotone.interpretation_or (x : Fin 2 → Bool) :
          interpretation Op.or x = (x 0 || x 1)

          Under interpretation, .or evaluates to x 0 || x 1.

          source
          theorem Cslib.Circuits.Monotone.interpretation_mono (op : Op) {x y : Fin (signature.Arity op) → Bool} (h : ∀ (i : Fin (signature.Arity op)), x i ≤ y i) :
          interpretation op x ≤ interpretation op y

          The operations of the monotone basis are monotone.

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

          The cost function charging one for each AND and OR gate and nothing for constants, the monotone counterpart of Boolean.binaryCost (binaryCost_toDeMorgan).

          Instances For
            source
            @[simp]
            theorem Cslib.Circuits.Monotone.binaryCost_and :
            binaryCost Op.and = 1

            An AND gate costs one level.

            source
            @[simp]
            theorem Cslib.Circuits.Monotone.binaryCost_or :
            binaryCost Op.or = 1

            An OR gate costs one level.

            source
            @[simp]
            theorem Cslib.Circuits.Monotone.binaryCost_const (b : Bool) :
            binaryCost (Op.const b) = 0

            Constants are free.

            source
            def Cslib.Circuits.Monotone.andCost :
            Op → ℕ

            Count AND gates, with constants and OR gates free.

            Instances For
              source
              @[simp]
              theorem Cslib.Circuits.Monotone.andCost_and :
              andCost Op.and = 1

              An AND gate has andCost equal to 1.

              source
              @[simp]
              theorem Cslib.Circuits.Monotone.andCost_or :
              andCost Op.or = 0

              An OR gate has andCost equal to 0.

              source
              @[simp]
              theorem Cslib.Circuits.Monotone.andCost_const (b : Bool) :
              andCost (Op.const b) = 0

              A constant gate has andCost equal to 0.

              The monotone basis inside the De Morgan basis #

              source
              def Cslib.Circuits.Monotone.toDeMorgan :
              signature.Hom Boolean.signature

              The monotone basis is the De Morgan basis without negation.

              Instances For
                source
                @[simp]
                theorem Cslib.Circuits.Monotone.toDeMorgan_const (b : Bool) :
                toDeMorgan (Op.const b) = Boolean.Op.const b

                toDeMorgan maps .const b to .const b.

                source
                @[simp]
                theorem Cslib.Circuits.Monotone.toDeMorgan_and :
                toDeMorgan Op.and = Boolean.Op.and

                toDeMorgan maps .and to .and.

                source
                @[simp]
                theorem Cslib.Circuits.Monotone.toDeMorgan_or :
                toDeMorgan Op.or = Boolean.Op.or

                toDeMorgan maps .or to .or.

                source
                instance Cslib.Circuits.Monotone.instPreservesBoolToDeMorganInterpretationInterpretation :
                toDeMorgan.Preserves interpretation Boolean.interpretation

                The monotone operations mean what their De Morgan images mean.

                source
                @[simp]
                theorem Cslib.Circuits.Monotone.binaryCost_toDeMorgan (op : Op) :
                Boolean.binaryCost (toDeMorgan op) = binaryCost op

                The De Morgan image of an operation costs what it costs in the monotone basis.

                source
                theorem Cslib.Circuits.Monotone.toDeMorgan_injective :
                Function.Injective ⇑toDeMorgan

                The monotone operations embed injectively into the De Morgan basis.