Integer multiplication in time O(n log n)

DefinitionEncoding of pairs#✓fully proved

Given encodings \(e_A : A \to \Gamma_A^*\) and \(e_B : B \to \Gamma_B^*\) of types \(A\) and \(B\) as lists over alphabets \(\Gamma_A\) and \(\Gamma_B\), and a new symbol \(\bot\) in neither alphabet, a pair \((a, b)\) is encoded as a list over the alphabet \((\Gamma_A \cup \{\bot\}) \times (\Gamma_B \cup \{\bot\})\) by zipping: its length is the larger of the lengths of \(e_A(a)\) and \(e_B(b)\), and its \(i\)-th entry is the pair of the \(i\)-th entries of \(e_A(a)\) and \(e_B(b)\), where an entry missing from the shorter list is replaced by \(\bot\).

def encodeProd {α β αΓ βΓ : Type*} (ea : α → List αΓ) (eb : β → List βΓ) (x : α × β) :
    List (Option αΓ × Option βΓ) :=
  List.zipWithAll Prod.mk (ea x.1) (eb x.2)

Used by 1

Used byHarvey–van der Hoeven: integer multiplication in time \(O(n \log n)\)

DefinitionBinary encoding of natural numbers#✓fully proved

The binary encoding of a natural number \(n\) is the list of its base-\(2\) digits, least significant first, with the digit \(1\) written as the Boolean value true and the digit \(0\) as false. The list has no trailing zero digit, so \(0\) is encoded by the empty list.

Unlike the unary encoding, this encoding of \(n > 0\) has length \(\lfloor \log_2 n \rfloor + 1\), which is the size model of the bit-complexity bound \(O(n \log n)\) for integer multiplication; with the unary encoding that bound could not hold.

def encodeNatBinary (n : ℕ) : List Bool :=
  (Nat.digits 2 n).map (fun d => d == 1)

Sources

• Lean variant; this replaces the upstream unary encoding Computability.encodeNat.

Used by 1

Used byHarvey–van der Hoeven: integer multiplication in time \(O(n \log n)\)

TheoremHarvey–van der Hoeven: integer multiplication in time \(O(n \log n)\)#●ready to prove

There is a multi-stack Turing machine with finite alphabets and a function \(t : \mathbb{N} \to \mathbb{N}\) such that, for all natural numbers \(x\) and \(y\), the machine started on the encoding of the pair \((x, y)\) (the binary encodings of \(x\) and \(y\), zipped) halts within \(t(\ell)\) steps with the binary encoding of \(xy\), where \(\ell\) is the length of the input, and \(t(n) = O(n \log n)\) as \(n \to \infty\).

public theorem_wanted theorem_1_1 :
    ∃ T : TM2ComputableInTime (encodeProd encodeNatBinary encodeNatBinary) encodeNatBinary (fun (x, y) ↦ x * y),
      (fun n ↦ (T.time n : ℝ)) =O[Filter.atTop] (fun n ↦ n * log n)

Sources

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_integer_multiplication of the lean-eval benchmark.

Uses 2

Statement usesBinary encoding of natural numbers · Encoding of pairs

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.