Documentation

Complexitylib.Algebraic.Basis.DeMorgan.CSLib

Conversions to CSLib's Boolean basis #

CSLib counts constants, negations, conjunctions, and disjunctions as gates. Our De Morgan basis also has an identity operation and supports weighted costs. The realizations below preserve all outputs: importing a CSLib circuit preserves its gate count, while exporting a De Morgan circuit removes identity gates. Neither conversion identifies standardCost with CSLib size, since constants are free under standardCost.

source
def Algebraic.DeMorgan.fromBooleanOperation (op : Cslib.Circuits.Boolean.Op) :
Circuit signature (Cslib.Circuits.Boolean.signature.Arity op) 1

The one-gate circuit over this library's De Morgan basis simulating each operation of CSLib's De Morgan basis.

Equations
Instances For
    source
    @[simp]
    theorem Algebraic.DeMorgan.fromBooleanOperation_size (op : Cslib.Circuits.Boolean.Op) :
    (fromBooleanOperation op).size = 1

    Each CSLib De Morgan operation is simulated by exactly one gate of this library's De Morgan basis.

    source
    def Algebraic.DeMorgan.fromBoolean :
    Realization Cslib.Circuits.Boolean.signature signature Cslib.Circuits.Boolean.interpretation interpretation

    Realize CSLib's Boolean operations in the weighted De Morgan basis.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.DeMorgan.fromBoolean_size {n m : ℕ} (circuit : Circuit Cslib.Circuits.Boolean.signature n m) :
      (fromBoolean.compile circuit).size = circuit.size

      Importing a CSLib circuit preserves the number of internal gates.

      source
      theorem Algebraic.DeMorgan.fromBoolean_standardCost_le {n m : ℕ} (circuit : Circuit Cslib.Circuits.Boolean.signature n m) :
      (fromBoolean.compile circuit).cost standardCost ≤ circuit.size

      Weighted logical-gate cost is at most the imported CSLib gate count.

      source
      def Algebraic.DeMorgan.toBooleanGateCount :
      Op → ℕ

      The number of CSLib De Morgan gates simulating each operation of this library's De Morgan basis: none for the identity, one otherwise.

      Equations
      Instances For
        source
        def Algebraic.DeMorgan.toBooleanOperation (op : Op) :
        Circuit Cslib.Circuits.Boolean.signature (arity op) 1

        The CSLib De Morgan circuit simulating each operation of this library's De Morgan basis; the identity uses no gate.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.DeMorgan.toBooleanOperation_size (op : Op) :
          (toBooleanOperation op).size = toBooleanGateCount op

          The CSLib simulation of each operation uses toBooleanGateCount gates.

          source
          def Algebraic.DeMorgan.toBoolean :
          Realization signature Cslib.Circuits.Boolean.signature interpretation Cslib.Circuits.Boolean.interpretation

          Realize De Morgan operations in CSLib, using a free wire for identity.

          Equations
          Instances For
            source
            theorem Algebraic.DeMorgan.toBoolean_size_le {n m : ℕ} (circuit : Circuit signature n m) :
            (toBoolean.compile circuit).size ≤ circuit.size

            Removing identity gates never increases the internal gate count.

            source
            theorem Algebraic.DeMorgan.boolean_computes_iff {n : ℕ} (circuit : Circuit Cslib.Circuits.Boolean.signature n 1) (function : Cslib.BooleanFunction n) :
            (circuit.Computes Cslib.Circuits.Boolean.interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) ↔ circuit.ComputesWith Cslib.Circuits.Boolean.interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

            CSLib's Circuit.Computes and this library's Circuit.ComputesWith are the same predicate, so this holds by Iff.rfl. It is definitional and kept only for compatibility with code written against the earlier, scalar CSLib predicate.

            source
            theorem Algebraic.DeMorgan.fromBoolean_computes {n : ℕ} (circuit : Circuit Cslib.Circuits.Boolean.signature n 1) (function : Cslib.BooleanFunction n) :
            ((fromBoolean.compile circuit).ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) ↔ circuit.Computes Cslib.Circuits.Boolean.interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

            The imported De Morgan circuit computes function on its single output exactly when the CSLib circuit does.

            source
            theorem Algebraic.DeMorgan.toBoolean_computes {n : ℕ} (circuit : Circuit signature n 1) (function : ScalarFunction Bool n) :
            ((toBoolean.compile circuit).Computes Cslib.Circuits.Boolean.interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) ↔ circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

            The exported CSLib circuit computes function on its single output exactly when the De Morgan circuit does.