Arithmetic Queries and Complex Multiplication

A simple example showing how to use FreeM.cost with variable/parametrized query costs.

ArithQuery α supports addition, subtraction, and multiplication, each with independently parametrized costs. Complex number multiplication provides a toy example where two algorithms (naive and Gauss's trick) trade multiplications for additions, and the optimal choice depends on the cost ratio.

inductive Cslib.Query.ArithQuery (α : Type) : Type → Type

Arithmetic queries: addition, subtraction, and multiplication.

• add {α : Type} (a b : α) : ArithQuery α α
• sub {α : Type} (a b : α) : ArithQuery α α
• mul {α : Type} (a b : α) : ArithQuery α α

@[reducible, inline]

abbrev Cslib.Query.ArithQuery.doAdd {α : Type} (a b : α) : FreeM (ArithQuery α) α

Lift ArithQuery.add a b into a FreeM that returns the sum.

Equations

• Cslib.Query.ArithQuery.doAdd a b = Cslib.FreeM.lift (Cslib.Query.ArithQuery.add a b)

@[reducible, inline]

abbrev Cslib.Query.ArithQuery.doSub {α : Type} (a b : α) : FreeM (ArithQuery α) α

Lift ArithQuery.sub a b into a FreeM that returns the difference.

Equations

• Cslib.Query.ArithQuery.doSub a b = Cslib.FreeM.lift (Cslib.Query.ArithQuery.sub a b)

@[reducible, inline]

abbrev Cslib.Query.ArithQuery.doMul {α : Type} (a b : α) : FreeM (ArithQuery α) α

Lift ArithQuery.mul a b into a FreeM that returns the product.

Equations

• Cslib.Query.ArithQuery.doMul a b = Cslib.FreeM.lift (Cslib.Query.ArithQuery.mul a b)

def Cslib.Query.ArithQuery.honest {α : Type} [Add α] [Sub α] [Mul α] {ι : Type} : ArithQuery α ι → ι

An honest oracle interprets arithmetic queries using the actual ring operations.

Equations

• (Cslib.Query.ArithQuery.add a b).honest = a + b
• (Cslib.Query.ArithQuery.sub a b).honest = a - b
• (Cslib.Query.ArithQuery.mul a b).honest = a * b

def Cslib.Query.ArithQuery.weight {α : Type} (c_add c_mul : ℕ) {ι : Type} : ArithQuery α ι → ℕ

Weighted cost model for arithmetic queries. Subtraction costs the same as addition (both are linear-time on bignums).

Equations

• Cslib.Query.ArithQuery.weight c_add c_mul (Cslib.Query.ArithQuery.add a b) = c_add
• Cslib.Query.ArithQuery.weight c_add c_mul (Cslib.Query.ArithQuery.sub a b) = c_add
• Cslib.Query.ArithQuery.weight c_add c_mul (Cslib.Query.ArithQuery.mul a b) = c_mul

def Cslib.Query.complexMulNaive {α : Type} (a b c d : α) : FreeM (ArithQuery α) (α × α)

Naive complex multiplication: (a + bi)(c + di) = (ac - bd) + (ad + bc)i. Uses 4 multiplications, 1 subtraction, 1 addition.

Equations

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

def Cslib.Query.complexMulGauss {α : Type} (a b c d : α) : FreeM (ArithQuery α) (α × α)

Gauss's trick for complex multiplication: computes (a+b)(c+d) to save one multiplication, at the cost of extra additions and subtractions. Uses 3 multiplications, 2 subtractions, 3 additions.

Equations

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