Arithmetic circuit basis

The arithmetic basis has binary addition and multiplication together with a family of nullary constants. The constant symbols are parameterized independently of the semantic carrier, so the same syntax can be interpreted in a polynomial ring, an extension field, a quotient, or an abstract algebra.

No ring laws are built into the circuit syntax. interpretation only asks for addition and multiplication on the carrier and for a map assigning semantic values to constant symbols. Algebraic laws and homomorphism properties belong to the chosen interpretations.

inductive Algebraic.Arithmetic.Op (K : Type u) : Type u

Addition, multiplication, and a parameterized family of constants.

• add {K : Type u} : Op K
• mul {K : Type u} : Op K
• constant {K : Type u} (value : K) : Op K

@[instance_reducible]

instance Algebraic.Arithmetic.instDecidableEqOp {K✝ : Type u_1} [DecidableEq K✝] : DecidableEq (Op K✝)

Equations

• Algebraic.Arithmetic.instDecidableEqOp = Algebraic.Arithmetic.instDecidableEqOp.decEq

def Algebraic.Arithmetic.instDecidableEqOp.decEq {K✝ : Type u_1} [DecidableEq K✝] (x✝ x✝¹ : Op K✝) : Decidable (x✝ = x✝¹)

Equations

• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.add Algebraic.Arithmetic.Op.add = isTrue ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.add Algebraic.Arithmetic.Op.mul = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.add (Algebraic.Arithmetic.Op.constant value) = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.mul Algebraic.Arithmetic.Op.add = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.mul Algebraic.Arithmetic.Op.mul = isTrue ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq Algebraic.Arithmetic.Op.mul (Algebraic.Arithmetic.Op.constant value) = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq (Algebraic.Arithmetic.Op.constant value) Algebraic.Arithmetic.Op.add = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq (Algebraic.Arithmetic.Op.constant value) Algebraic.Arithmetic.Op.mul = isFalse ⋯
• Algebraic.Arithmetic.instDecidableEqOp.decEq (Algebraic.Arithmetic.Op.constant a) (Algebraic.Arithmetic.Op.constant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Algebraic.Arithmetic.opEquiv {K : Type u_1} : Op K ≃ Bool ⊕ K

Arithmetic operations are equivalent to two binary symbols plus the constant-symbol type.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Algebraic.Arithmetic.instFintypeOp {K : Type u_1} [Fintype K] : Fintype (Op K)

A finite constant alphabet gives a finite arithmetic signature.

Equations

• Algebraic.Arithmetic.instFintypeOp = Fintype.ofEquiv (Bool ⊕ K) Algebraic.Arithmetic.opEquiv.symm

def Algebraic.Arithmetic.arity {K : Type u_1} : Op K → ℕ

Arity of an arithmetic operation.

Equations

• Algebraic.Arithmetic.arity Algebraic.Arithmetic.Op.add = 2
• Algebraic.Arithmetic.arity Algebraic.Arithmetic.Op.mul = 2
• Algebraic.Arithmetic.arity (Algebraic.Arithmetic.Op.constant value) = 0

@[simp]

theorem Algebraic.Arithmetic.arity_add {K : Type u_1} : arity Op.add = 2

@[simp]

theorem Algebraic.Arithmetic.arity_mul {K : Type u_1} : arity Op.mul = 2

@[simp]

theorem Algebraic.Arithmetic.arity_constant {K : Type u_1} (value : K) : arity (Op.constant value) = 0

@[reducible, inline]

abbrev Algebraic.Arithmetic.signature (K : Type u) : Signature

Signature of arithmetic circuits with constants named by K.

Equations

• Algebraic.Arithmetic.signature K = { Op := Algebraic.Arithmetic.Op K, Arity := Algebraic.Arithmetic.arity }

def Algebraic.Arithmetic.interpretation {R : Type u_1} {K : Type u_2} [Add R] [Mul R] (constant : K → R) (op : Op K) : (Fin (arity op) → R) → R

Interpret arithmetic syntax in any carrier with addition and multiplication, using constant to interpret the nullary symbols.

Equations

• Algebraic.Arithmetic.interpretation constant Algebraic.Arithmetic.Op.add input = input (Fin.cast ⋯ 0) + input (Fin.cast ⋯ 1)
• Algebraic.Arithmetic.interpretation constant Algebraic.Arithmetic.Op.mul input = input (Fin.cast ⋯ 0) * input (Fin.cast ⋯ 1)
• Algebraic.Arithmetic.interpretation constant (Algebraic.Arithmetic.Op.constant value) x_2 = constant value

def Algebraic.Arithmetic.nativeInterpretation {K : Type u_1} [Add K] [Mul K] : Interpretation (signature K) K

Interpret constants by themselves in their native arithmetic carrier.

Equations

• Algebraic.Arithmetic.nativeInterpretation = Algebraic.Arithmetic.interpretation id

def Algebraic.Arithmetic.weightedCost {K : Type u_1} (addition multiplication : ℕ) : OperationCost (signature K)

Charge additions and multiplications independently; constants are free.

Equations

• Algebraic.Arithmetic.weightedCost addition multiplication Algebraic.Arithmetic.Op.add = addition
• Algebraic.Arithmetic.weightedCost addition multiplication Algebraic.Arithmetic.Op.mul = multiplication
• Algebraic.Arithmetic.weightedCost addition multiplication (Algebraic.Arithmetic.Op.constant value) = 0

def Algebraic.Arithmetic.gateCost {K : Type u_1} : OperationCost (signature K)

Standard arithmetic gate count: additions and multiplications cost one.

Equations

• Algebraic.Arithmetic.gateCost = Algebraic.Arithmetic.weightedCost 1 1

def Algebraic.Arithmetic.multiplicationCost {K : Type u_1} : OperationCost (signature K)

Multiplicative complexity: only multiplication gates are charged.

Equations

• Algebraic.Arithmetic.multiplicationCost = Algebraic.Arithmetic.weightedCost 0 1

def Algebraic.Arithmetic.additionCost {K : Type u_1} : OperationCost (signature K)

Additive complexity: only addition gates are charged.

Equations

• Algebraic.Arithmetic.additionCost = Algebraic.Arithmetic.weightedCost 1 0

@[simp]

theorem Algebraic.Arithmetic.weightedCost_add {K : Type u_1} (addition multiplication : ℕ) : weightedCost addition multiplication Op.add = addition

@[simp]

theorem Algebraic.Arithmetic.weightedCost_mul {K : Type u_1} (addition multiplication : ℕ) : weightedCost addition multiplication Op.mul = multiplication

@[simp]

theorem Algebraic.Arithmetic.weightedCost_constant {K : Type u_1} (addition multiplication : ℕ) (value : K) : weightedCost addition multiplication (Op.constant value) = 0

@[simp]

theorem Algebraic.Arithmetic.gateCost_add {K : Type u_1} : gateCost Op.add = 1

@[simp]

theorem Algebraic.Arithmetic.gateCost_mul {K : Type u_1} : gateCost Op.mul = 1

@[simp]

theorem Algebraic.Arithmetic.gateCost_constant {K : Type u_1} (value : K) : gateCost (Op.constant value) = 0

@[simp]

theorem Algebraic.Arithmetic.multiplicationCost_add {K : Type u_1} : multiplicationCost Op.add = 0

@[simp]

theorem Algebraic.Arithmetic.multiplicationCost_mul {K : Type u_1} : multiplicationCost Op.mul = 1

@[simp]

theorem Algebraic.Arithmetic.multiplicationCost_constant {K : Type u_1} (value : K) : multiplicationCost (Op.constant value) = 0

@[simp]

theorem Algebraic.Arithmetic.additionCost_add {K : Type u_1} : additionCost Op.add = 1

@[simp]

theorem Algebraic.Arithmetic.additionCost_mul {K : Type u_1} : additionCost Op.mul = 0

@[simp]

theorem Algebraic.Arithmetic.additionCost_constant {K : Type u_1} (value : K) : additionCost (Op.constant value) = 0