Documentation

Complexitylib.Algebraic.Basis.DeMorgan

The De Morgan basis #

The basis contains Boolean constants, a structural identity gate, unary negation, and binary conjunction and disjunction. The circuit representation has free wire outputs; identity remains useful only when a proof explicitly materializes an output as a final program gate. binaryCost implements the standard gate-elimination cost model in which only the binary gates are charged. andCost and notCost count the AND gates and the NOT gates.

source
inductive Algebraic.DeMorgan.Op :
Type

Operation symbols in the De Morgan basis.

Instances For
    source
    @[instance_reducible]
    instance Algebraic.DeMorgan.instDecidableEqOp :
    DecidableEq Op
    Equations
    source
    @[instance_reducible]
    instance Algebraic.DeMorgan.instFintypeOp :
    Fintype Op

    The De Morgan basis has six operation symbols.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Algebraic.DeMorgan.arity :
    Op → ℕ

    Arity of an operation in the De Morgan basis.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_false :
      arity Op.false = 0
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_true :
      arity Op.true = 0
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_id :
      arity Op.id = 1
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_not :
      arity Op.not = 1
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_and :
      arity Op.and = 2
      source
      @[simp]
      theorem Algebraic.DeMorgan.arity_or :
      arity Op.or = 2
      source
      @[reducible, inline]
      abbrev Algebraic.DeMorgan.signature :
      Signature

      Signature of the De Morgan basis.

      Equations
      Instances For
        source
        def Algebraic.DeMorgan.interpretation (op : Op) :
        (Fin (arity op) → Bool) → Bool

        Standard Boolean interpretation of the De Morgan basis.

        Equations
        Instances For
          source
          def Algebraic.DeMorgan.binaryCost :
          OperationCost signature

          Cost model charging exactly the binary gates. This is the convention used by the gate-elimination lower bounds, not the mass-production manuscript.

          Equations
          Instances For
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_false :
            binaryCost Op.false = 0
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_true :
            binaryCost Op.true = 0
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_id :
            binaryCost Op.id = 0
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_not :
            binaryCost Op.not = 0
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_and :
            binaryCost Op.and = 1
            source
            @[simp]
            theorem Algebraic.DeMorgan.binaryCost_or :
            binaryCost Op.or = 1
            source
            def Algebraic.DeMorgan.standardCost :
            OperationCost signature

            The manuscript's standard circuit-size convention: constants and structural identities are free, while NOT, AND, and OR each cost one gate.

            Equations
            Instances For
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_false :
              standardCost Op.false = 0
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_true :
              standardCost Op.true = 0
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_id :
              standardCost Op.id = 0
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_not :
              standardCost Op.not = 1
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_and :
              standardCost Op.and = 1
              source
              @[simp]
              theorem Algebraic.DeMorgan.standardCost_or :
              standardCost Op.or = 1
              source
              def Algebraic.DeMorgan.andCost :
              OperationCost signature

              Charge AND gates and treat every other gate as free; the De Morgan analogue of AndOr.andCost.

              Equations
              Instances For
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_false :
                andCost Op.false = 0
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_true :
                andCost Op.true = 0
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_id :
                andCost Op.id = 0
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_not :
                andCost Op.not = 0
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_and :
                andCost Op.and = 1
                source
                @[simp]
                theorem Algebraic.DeMorgan.andCost_or :
                andCost Op.or = 0
                source
                def Algebraic.DeMorgan.notCost :
                OperationCost signature

                Charge NOT gates and treat every other gate as free, so that a circuit's cost is its number of negations.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_false :
                  notCost Op.false = 0
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_true :
                  notCost Op.true = 0
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_id :
                  notCost Op.id = 0
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_not :
                  notCost Op.not = 1
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_and :
                  notCost Op.and = 0
                  source
                  @[simp]
                  theorem Algebraic.DeMorgan.notCost_or :
                  notCost Op.or = 0