Documentation

Complexitylib.Algebraic.LowerBound.KarchmerWigderson.Sharing.Extended.Defs

The De Morgan basis extended by XOR and EQUIV gates #

This file defines the circuit basis of Extended.signature: the De Morgan operations (Boolean constants, identity, NOT, binary AND and OR) together with binary XOR and EQUIV gates, its standard interpretation Extended.interpretation, and three cost models: Extended.deMorganCost counts the AND and OR gates, Extended.xorCost the XOR and EQUIV gates, and Extended.binaryCost all binary gates.

It also defines the four-leaf De Morgan formulas Formula.xorGadget z₁ z₂ and Formula.equivGadget z₁ z₂ computing z₁ ⊕ z₂ and z₁ ↔ z₂. When both variables are shared values (indices at least m), the gadgets have no input leaves below m; this is what lets an XOR or EQUIV gate of any fan-out be charged only two shared values in the Khrapchenko bound of Complexitylib.Algebraic.LowerBound.KarchmerWigderson.Sharing.Extended.

XOR and EQUIV gadgets #

source
def Algebraic.KW.Formula.xorGadget {N : ℕ} (z₁ z₂ : Fin N) :
Formula N

The De Morgan formula (z₁ ∧ ¬z₂) ∨ (¬z₁ ∧ z₂) computing z₁ ⊕ z₂ on two variables.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.KW.Formula.equivGadget {N : ℕ} (z₁ z₂ : Fin N) :
    Formula N

    The De Morgan formula (z₁ ∧ z₂) ∨ (¬z₁ ∧ ¬z₂) computing z₁ ↔ z₂ on two variables.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Algebraic.KW.Formula.eval_xorGadget {N : ℕ} (z₁ z₂ : Fin N) (x : Fin N → Bool) :
      (xorGadget z₁ z₂).eval x = (x z₁ ^^ x z₂)
      source
      @[simp]
      theorem Algebraic.KW.Formula.eval_equivGadget {N : ℕ} (z₁ z₂ : Fin N) (x : Fin N → Bool) :
      (equivGadget z₁ z₂).eval x = (x z₁ == x z₂)
      source
      theorem Algebraic.KW.Formula.inputLeaves_xorGadget_of_ge {N m : ℕ} {z₁ z₂ : Fin N} (h₁ : m ≤ ↑z₁) (h₂ : m ≤ ↑z₂) :
      (xorGadget z₁ z₂).inputLeaves m = 0

      When both variables z₁, z₂ are shared variables (≥ m), xorGadget z₁ z₂ contributes zero input leaves below m.

      source
      theorem Algebraic.KW.Formula.inputLeaves_equivGadget_of_ge {N m : ℕ} {z₁ z₂ : Fin N} (h₁ : m ≤ ↑z₁) (h₂ : m ≤ ↑z₂) :
      (equivGadget z₁ z₂).inputLeaves m = 0

      When both variables z₁, z₂ are shared variables (≥ m), equivGadget z₁ z₂ contributes zero input leaves below m.

      The extended basis #

      source
      inductive Algebraic.KW.Extended.Op :
      Type

      Operation symbols of the extended De Morgan basis with binary xor and equiv gates.

      Instances For
        source
        @[instance_reducible]
        instance Algebraic.KW.Extended.instDecidableEqOp :
        DecidableEq Op
        Equations
        source
        @[instance_reducible]
        instance Algebraic.KW.Extended.instFintypeOp :
        Fintype Op
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Algebraic.KW.Extended.arity :
        Op → ℕ

        Arity of an operation in the extended basis.

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

          Signature of the extended De Morgan + XOR/EQUIV basis.

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

            Standard Boolean interpretation of the extended basis.

            Equations
            Instances For
              source
              def Algebraic.KW.Extended.deMorganCost :
              OperationCost signature

              Cost model charging 1 for binary De Morgan gates (and, or) and 0 for all other gates.

              Equations
              Instances For
                source
                def Algebraic.KW.Extended.xorCost :
                OperationCost signature

                Cost model charging 1 for binary XOR/EQUIV gates (xor, equiv) and 0 for all other gates.

                Equations
                Instances For
                  source
                  def Algebraic.KW.Extended.binaryCost :
                  OperationCost signature

                  Cost model charging 1 for all binary gates (and, or, xor, equiv).

                  Equations
                  Instances For
                    source
                    def Algebraic.KW.Extended.isDeMorgan :
                    Op → Bool

                    Whether an operation is in the De Morgan fragment (false, true, id, not, and, or).

                    Equations
                    Instances For