Karatsuba algorithm

DefinitionKaratsuba multiplication#✓fully proved

Karatsuba's algorithm on natural numbers \(x\) and \(y\), viewed as \(n\)-digit numbers in base \(B\), as a computation that returns a natural number together with a cost. If \(n \le 1\), it returns \(xy\) at cost \(1\). If \(n \ge 2\), let \(m = \lceil n/2 \rceil\), let \(a\) and \(b\) be the natural-number quotient and remainder of \(x\) by \(B^m\), and let \(c\) and \(d\) be those of \(y\) by \(B^m\). It runs itself with digit count \(m\) on the pairs \((a, c)\), \((b, d)\) and \((|a - b|, |c - d|)\), with results \(e\), \(f\) and \(g\), and returns \(B^{2m} e + B^m h + f\), where \(h = e + f - g\) (subtraction truncated at \(0\)) if \(b \le a\) holds exactly when \(d \le c\), and \(h = e + f + g\) otherwise. The cost of the call is \(n\) plus the costs of the three recursive calls.

Cslib.Algorithms.Lean.TimeM.karatsuba · 18 lines

def karatsuba (B : ℕ) (n x y : ℕ) : TimeM ℕ ℕ :=
  if n ≤ 1 then do
    ✓
    pure (x * y)
  else do
    let m := (n + 1) / 2
    let a := x / B ^ m
    let b := x % B ^ m
    let c := y / B ^ m
    let d := y % B ^ m
    let e ← karatsuba B m a c
    let f ← karatsuba B m b d
    let g ← karatsuba B m (Nat.dist a b) (Nat.dist c d)
    ✓[n]
    let mid := if (b ≤ a ↔ d ≤ c) then e + f - g else e + f + g
    pure (B ^ (2 * m) * e + B ^ m * mid + f)
termination_by n
decreasing_by all_goals omega

Used by 4

Used byCorrectness of Karatsuba multiplication · Cost of Karatsuba multiplication · Power-of-three bound on the cost of Karatsuba multiplication · The \(n^{\log_2 3}\) bound for Karatsuba multiplication

DefinitionKaratsuba cost recurrence#✓fully proved

The function \(T\) on natural numbers defined by \(T(n) = 1\) for \(n \le 1\) and \(T(n) = 3\,T(\lceil n/2 \rceil) + n\) for \(n \ge 2\).

It is the cost of Karatsuba multiplication on \(n\) digits: one unit for a product of single digits, and for \(n \ge 2\) three recursive calls on \(\lceil n/2 \rceil\) digits plus \(n\) units of linear digit work.

def karatsubaCost (n : ℕ) : ℕ :=
  if n ≤ 1 then 1 else 3 * karatsubaCost ((n + 1) / 2) + n
termination_by n
decreasing_by omega

Used by 6

Used byPower-of-three bound on the Karatsuba cost recurrence · The \(n^{\log_2 3}\) bound for the Karatsuba cost recurrence · Karatsuba cost at powers of two · Cost of Karatsuba multiplication · Power-of-three bound on the cost of Karatsuba multiplication · The \(n^{\log_2 3}\) bound for Karatsuba multiplication

11 fully proved

Correctness

TheoremKaratsuba's middle coefficient#✓fully proved

For all natural numbers \(a, b, c, d\), write \(P = |a - b| \cdot |c - d|\). If \(b \le a\) holds exactly when \(d \le c\), then \(ac + bd - P = ad + bc\), where the subtraction is truncated at \(0\); otherwise \(ac + bd + P = ad + bc\).

So the cross term \(ad + bc\) is recovered from the three products \(ac\), \(bd\) and \(P\).

theorem karatsuba_middle (a b c d : ℕ) :
    (if (b ≤ a ↔ d ≤ c) then a * c + b * d - Nat.dist a b * Nat.dist c d
      else a * c + b * d + Nat.dist a b * Nat.dist c d) = a * d + b * c

Used by 1

Used byCorrectness of Karatsuba multiplication

TheoremCorrectness of Karatsuba multiplication#✓fully proved

For all natural numbers \(B\), \(n\), \(x\) and \(y\), Karatsuba multiplication of \(x\) and \(y\) as \(n\)-digit numbers in base \(B\) returns \(xy\).

The inputs need not be below \(B^n\): the digit count only steers the recursion.

theorem karatsuba_ret (B n x y : ℕ) : (karatsuba B n x y).ret = x * y

def karatsuba (B : ℕ) (n x y : ℕ) : TimeM ℕ ℕ :=
  if n ≤ 1 then do
    ✓
    pure (x * y)
  else do
    let m := (n + 1) / 2
    let a := x / B ^ m
    let b := x % B ^ m
    let c := y / B ^ m
    let d := y % B ^ m
    let e ← karatsuba B m a c
    let f ← karatsuba B m b d
  ⋯

CSLibExt/Algorithms/Lean/DivideAndConquer/Karatsuba.lean:59

Uses 2

Statement usesKaratsuba multiplication

Proof usesKaratsuba's middle coefficient

Operand sizes

TheoremSize bound for Karatsuba's recursive operands#✓fully proved

Let \(B \ge 1\) and \(n\) be natural numbers, let \(m = \lceil n/2 \rceil\), and let \(x < B^n\) be a natural number. Then the high part \(\lfloor x / B^m \rfloor\), the low part \(x \bmod B^m\), and their distance \(|\lfloor x / B^m \rfloor - x \bmod B^m|\) are all less than \(B^m\).

Applied to both inputs, all six recursive operands stay within the digit model, and the base case multiplies single digits.

theorem karatsuba_operands_lt {B n x : ℕ} (hB : 0 < B) (hx : x < B ^ n) :
    x / B ^ ((n + 1) / 2) < B ^ ((n + 1) / 2) ∧ x % B ^ ((n + 1) / 2) < B ^ ((n + 1) / 2) ∧
      Nat.dist (x / B ^ ((n + 1) / 2)) (x % B ^ ((n + 1) / 2)) < B ^ ((n + 1) / 2)

Cost

TheoremCost of Karatsuba multiplication#✓fully proved

For all natural numbers \(B\), \(n\), \(x\) and \(y\), the cost of Karatsuba multiplication of \(x\) and \(y\) as \(n\)-digit numbers in base \(B\) equals \(T(n)\), where \(T\) is the Karatsuba cost recurrence, \(T(n) = 1\) for \(n \le 1\) and \(T(n) = 3\,T(\lceil n/2 \rceil) + n\) for \(n \ge 2\).

In particular the cost depends only on the digit count \(n\), not on \(B\), \(x\) or \(y\).

theorem karatsuba_time (B n x y : ℕ) : (karatsuba B n x y).time = karatsubaCost n

def karatsuba (B : ℕ) (n x y : ℕ) : TimeM ℕ ℕ :=
  if n ≤ 1 then do
    ✓
    pure (x * y)
  else do
    let m := (n + 1) / 2
    let a := x / B ^ m
    let b := x % B ^ m
    let c := y / B ^ m
    let d := y % B ^ m
    let e ← karatsuba B m a c
    let f ← karatsuba B m b d
  ⋯

CSLibExt/Algorithms/Lean/DivideAndConquer/Karatsuba.lean:59

def karatsubaCost (n : ℕ) : ℕ :=
  if n ≤ 1 then 1 else 3 * karatsubaCost ((n + 1) / 2) + n
termination_by n
decreasing_by omega

CSLibExt/Algorithms/Lean/DivideAndConquer/Karatsuba.lean:80

Uses 2 · Used by 2

Statement usesKaratsuba multiplication · Karatsuba cost recurrence

Used byPower-of-three bound on the cost of Karatsuba multiplication · The \(n^{\log_2 3}\) bound for Karatsuba multiplication

TheoremKaratsuba cost at powers of two#✓fully proved

Let \(T\) be the Karatsuba cost recurrence, \(T(n) = 1\) for \(n \le 1\) and \(T(n) = 3\,T(\lceil n/2 \rceil) + n\) for \(n \ge 2\). For every natural number \(k\), \(T(2^k) + 2^{k+1} = 3^{k+1}\).

So at \(n = 2^k\) digits the cost is exactly \(3^{k+1} - 2^{k+1} = 3\, n^{\log_2 3} - 2n\).

theorem karatsubaCost_two_pow (k : ℕ) : karatsubaCost (2 ^ k) + 2 ^ (k + 1) = 3 ^ (k + 1)

Uses 1 · Used by 1

Statement usesKaratsuba cost recurrence

Used byPower-of-three bound on the Karatsuba cost recurrence

TheoremPower-of-three bound on the Karatsuba cost recurrence#✓fully proved

Let \(T\) be the Karatsuba cost recurrence, \(T(n) = 1\) for \(n \le 1\) and \(T(n) = 3\,T(\lceil n/2 \rceil) + n\) for \(n \ge 2\), and let \(\ell(n)\) be the least natural number \(k\) with \(n \le 2^k\) (so \(\ell(n) = \lceil \log_2 n \rceil\) for \(n \ge 1\)). For every natural number \(n\), \(T(n) \le 3^{\ell(n) + 1}\).

The proof pads \(n\) up to the next power of two.

theorem karatsubaCost_le (n : ℕ) : karatsubaCost n ≤ 3 ^ (Nat.clog 2 n + 1)

Uses 2 · Used by 2

Statement usesKaratsuba cost recurrence

Proof usesKaratsuba cost at powers of two

Used byThe \(n^{\log_2 3}\) bound for the Karatsuba cost recurrence · Power-of-three bound on the cost of Karatsuba multiplication

TheoremPower-of-three bound on the cost of Karatsuba multiplication#✓fully proved

Let \(\ell(n)\) be the least natural number \(k\) with \(n \le 2^k\) (so \(\ell(n) = \lceil \log_2 n \rceil\) for \(n \ge 1\)). For all natural numbers \(B\), \(n\), \(x\) and \(y\), the cost of Karatsuba multiplication of \(x\) and \(y\) as \(n\)-digit numbers in base \(B\) is at most \(3^{\ell(n) + 1}\).

theorem karatsuba_time_le (B n x y : ℕ) :
    (karatsuba B n x y).time ≤ 3 ^ (Nat.clog 2 n + 1)

def karatsuba (B : ℕ) (n x y : ℕ) : TimeM ℕ ℕ :=
  if n ≤ 1 then do
    ✓
    pure (x * y)
  else do
    let m := (n + 1) / 2
    let a := x / B ^ m
    let b := x % B ^ m
    let c := y / B ^ m
    let d := y % B ^ m
    let e ← karatsuba B m a c
    let f ← karatsuba B m b d
  ⋯

CSLibExt/Algorithms/Lean/DivideAndConquer/Karatsuba.lean:59

Uses 4

Statement usesKaratsuba multiplication

Proof usesKaratsuba cost recurrence · Power-of-three bound on the Karatsuba cost recurrence · Cost of Karatsuba multiplication

TheoremThe \(n^{\log_2 3}\) bound for the Karatsuba cost recurrence#✓fully proved

Let \(T\) be the Karatsuba cost recurrence, \(T(n) = 1\) for \(n \le 1\) and \(T(n) = 3\,T(\lceil n/2 \rceil) + n\) for \(n \ge 2\). For every natural number \(n \ge 1\), \(T(n) \le 9\, n^{\log_2 3}\).

theorem karatsubaCost_le_rpow {n : ℕ} (hn : 1 ≤ n) :
    (karatsubaCost n : ℝ) ≤ 9 * (n : ℝ) ^ Real.logb 2 3

Uses 2 · Used by 1

Statement usesKaratsuba cost recurrence

Proof usesPower-of-three bound on the Karatsuba cost recurrence

Used byThe \(n^{\log_2 3}\) bound for Karatsuba multiplication

TheoremThe \(n^{\log_2 3}\) bound for Karatsuba multiplication#✓fully proved

For all natural numbers \(B\), \(x\), \(y\) and \(n \ge 1\), the cost of Karatsuba multiplication of \(x\) and \(y\) as \(n\)-digit numbers in base \(B\) is at most \(9\, n^{\log_2 3}\).

theorem karatsuba_time_le_rpow (B : ℕ) {n : ℕ} (hn : 1 ≤ n) (x y : ℕ) :
    ((karatsuba B n x y).time : ℝ) ≤ 9 * (n : ℝ) ^ Real.logb 2 3

def karatsuba (B : ℕ) (n x y : ℕ) : TimeM ℕ ℕ :=
  if n ≤ 1 then do
    ✓
    pure (x * y)
  else do
    let m := (n + 1) / 2
    let a := x / B ^ m
    let b := x % B ^ m
    let c := y / B ^ m
    let d := y % B ^ m
    let e ← karatsuba B m a c
    let f ← karatsuba B m b d
  ⋯

CSLibExt/Algorithms/Lean/DivideAndConquer/Karatsuba.lean:59

Uses 4

Statement usesKaratsuba multiplication

Proof usesKaratsuba cost recurrence · The \(n^{\log_2 3}\) bound for the Karatsuba cost recurrence · Cost of Karatsuba multiplication

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.