Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Atoms

Arithmetic atom projections #

Common list-level views of semantic arithmetic-circuit atoms. Keeping these projections independent of any particular Fusion witness lets dyadic, interaction-span, and future arithmetic specializations share the same notion of a multiplication occurrence and the same exact cost accounting.

source
def Algebraic.Fusion.Arithmetic.Atom.mulArguments? {C : Type u} {U : Type v} (atom : Atom (Arithmetic.signature C) U) :
Option (Fin 2 → U)

Retain the arguments of a multiplication atom and discard addition and constant atoms.

Equations
Instances For
    source
    def Algebraic.Fusion.Arithmetic.multiplicationArguments {C : Type u} {U : Type v} (atoms : List (Atom (Arithmetic.signature C) U)) :
    List (Fin 2 → U)

    Multiplication occurrences, in program order, contained in a list of evaluated arithmetic atoms. Equal semantic argument pairs remain distinct list entries.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.Fusion.Arithmetic.multiplicationArguments_cons_add {C : Type u} {U : Type v} (arguments : Fin 2 → U) (atoms : List (Atom (Arithmetic.signature C) U)) :
      multiplicationArguments ({ op := Arithmetic.Op.add, arguments := arguments } :: atoms) = multiplicationArguments atoms
      source
      @[simp]
      theorem Algebraic.Fusion.Arithmetic.multiplicationArguments_cons_mul {C : Type u} {U : Type v} (arguments : Fin 2 → U) (atoms : List (Atom (Arithmetic.signature C) U)) :
      multiplicationArguments ({ op := Arithmetic.Op.mul, arguments := arguments } :: atoms) = arguments :: multiplicationArguments atoms
      source
      @[simp]
      theorem Algebraic.Fusion.Arithmetic.multiplicationArguments_cons_constant {C : Type u} {U : Type v} (scalar : C) (arguments : Fin (Arithmetic.arity (Arithmetic.Op.constant scalar)) → U) (atoms : List (Atom (Arithmetic.signature C) U)) :
      multiplicationArguments ({ op := Arithmetic.Op.constant scalar, arguments := arguments } :: atoms) = multiplicationArguments atoms
      source
      theorem Algebraic.Fusion.Arithmetic.mem_multiplicationArguments {C : Type u} {U : Type v} (arguments : Fin 2 → U) (atoms : List (Atom (Arithmetic.signature C) U)) :
      arguments ∈ multiplicationArguments atoms ↔ { op := Arithmetic.Op.mul, arguments := arguments } ∈ atoms

      Membership in the multiplication-occurrence projection is exactly membership of the corresponding multiplication atom in the source list.

      source
      theorem Algebraic.Fusion.Arithmetic.multiplicationArguments_length {C : Type u} {U : Type v} (atoms : List (Atom (Arithmetic.signature C) U)) :
      (multiplicationArguments atoms).length = Atom.listCost atoms Arithmetic.multiplicationCost

      The number of retained multiplication occurrences is exactly their weighted atom cost.

      source
      def Algebraic.Fusion.Arithmetic.circuitMultiplicationArguments {C : Type u} {U : Type v} {n m : ℕ} [Add U] [Mul U] (constant : C → U) (input : Fin n → U) (circuit : Circuit (Arithmetic.signature C) n m) :
      List (Fin 2 → U)

      Multiplication occurrences of an arithmetic circuit evaluated on a particular semantic input.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algebraic.Fusion.Arithmetic.circuitMultiplicationArguments_length {C : Type u} {U : Type v} {n m : ℕ} [Add U] [Mul U] (constant : C → U) (input : Fin n → U) (circuit : Circuit (Arithmetic.signature C) n m) :
        (circuitMultiplicationArguments constant input circuit).length = circuit.cost Arithmetic.multiplicationCost

        The evaluated multiplication-occurrence list has exactly the circuit's multiplication cost, independently of semantic coincidences between gates.