Algorithms, correctness and efficiency

Lens

MotivationH

Twenty questions

Think of a whole number between $1$ and $1\,000\,000$ . I will find it by asking questions that you answer only "yes" or "no" — and I promise to need at most twenty.

The trick: always ask about the middle. "Is it more than $500\,000$ ?" Whatever you answer, half of the possibilities are gone. After one question $500\,000$ remain, after two $250\,000$ , and in general after $k$ questions at most $\lceil 10^6 / 2^k \rceil$ . Since $2^{20} = 1\,048\,576$ is more than a million, after twenty questions only one possibility is left. Asking "Is it $1$ ? Is it $2$ ? Is it $3$ ?…" could take a million questions.

Both are algorithms — precise recipes that a person or a machine can follow without thinking. Both are correct. One is fifty thousand times faster. The same contrast appears whenever a phone searches your contacts, a library catalogue finds a book, a teacher in Nairobi sorts six hundred exam scripts into alphabetical order, or a bank in São Paulo checks a payment against a list of millions of accounts.

This lesson asks three questions about every algorithm: Does it stop? Does it give the right answer? How long does it take? — and answers them with proofs, not just tests.

IntuitionH

Why testing is not enough

You could check an algorithm by running it on many examples. That is useful — and it is how bugs are often found — but it cannot show that the algorithm works on the inputs you did not try. Binary search is famous for this: it is short and simple, yet Jon Bentley, citing Donald Knuth, pointed out in Programming Pearls that although the first binary search was published in 1946, the first version that works correctly for every list length did not appear in print until 1962. And in 2006 Joshua Bloch reported that the binary search in Java's standard library, used for nearly a decade, failed on lists of more than about a billion entries.

DefinitionsH

Definitions

Definition— algorithm and specification

An algorithm is a finite list of precise instructions that transforms an input into an output. Its specification says which inputs are allowed and what the output must satisfy. For example: input a list $a_0 \le a_1 \le \dots \le a_{n-1}$ of numbers in increasing order and a number $t$ ; output an index $i$ with $a_i = t$ , or "absent" if there is none.

Definition— correctness

An algorithm is correct if, for every allowed input, it terminates (stops after finitely many steps) and its output satisfies the specification.

Definition— loop invariant

A loop invariant is a statement about the variables of a loop that holds before the first pass through the loop and is preserved by every pass (if it holds before a pass, it holds after). It then holds whenever the loop stops — by induction on the number of passes.

Definition— termination measure

A termination measure (or variant) is a whole number, computed from the variables, that is never negative and strictly decreases with every pass. Since a decreasing sequence of natural numbers cannot go on forever, the loop must stop.

Definition— running time

The running time of an algorithm is the number of basic steps it takes (here: comparisons), as a function of the size $n$ of the input. The worst-case running time $T(n)$ is the largest number of steps over all inputs of size $n$ .

We usually care about how $T(n)$ grows, not its exact value. We write $T(n) = O(g(n))$ , "big-O of $g$ ", if there are constants $C$ and $N$ with $T(n) \le C\,g(n)$ for all $n \ge N$ . So $3n^2 + 5n + 7 = O(n^2)$ : for large $n$ the $n^2$ term dominates and constant factors are ignored.

Worked examplesH

Four algorithms

Example— Linear search

Check the entries one by one.

def linear_search(a, t):
    for i in range(len(a)):
        if a[i] == t:
            return i
    return None          # t is absent

On $a = [4, 9, 2, 7]$ and $t = 2$ it compares $t$ with $4$ , $9$ , $2$ and returns index $2$ after three comparisons. If $t$ is absent it makes $n$ comparisons. It works on any list, sorted or not.

Example— Binary search

For a sorted list, compare $t$ with the middle entry and discard the half that cannot contain it.

def binary_search(a, t):
    lo, hi = 0, len(a) - 1
    while lo <= hi:                 # the range a[lo..hi] is not empty
        mid = (lo + hi) // 2        # the middle (rounded down)
        if a[mid] == t:
            return mid
        elif a[mid] < t:
            lo = mid + 1            # t can only be to the right of mid
        else:
            hi = mid - 1            # t can only be to the left of mid
    return None

We count each probe of $a_{mid}$ as one comparison with three possible outcomes — equal, smaller or larger — even though the code tests two conditions.

Trace on $a = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29]$ (indices $0$ – $9$ ) with $t = 23$ : $\;mid = 4$ , $a_4 = 11 < 23$ , so $lo = 5$ ; $\;mid = 7$ , $a_7 = 19 < 23$ , so $lo = 8$ ; $\;mid = 8$ , $a_8 = 23$ : found, after three comparisons. With $t = 4$ : $mid = 4$ ( $11 > 4$ , $hi = 3$ ), $mid = 1$ ( $3 < 4$ , $lo = 2$ ), $mid = 2$ ( $5 > 4$ , $hi = 1$ ); now $lo > hi$ , so $4$ is absent — again three comparisons.

Example— Insertion sort

Sort like a hand of cards: take each new entry and slide it left past the larger entries before it.

def insertion_sort(a):
    for i in range(1, len(a)):
        x = a[i]
        j = i - 1
        while j >= 0 and a[j] > x:
            a[j + 1] = a[j]         # shift the larger entry right
            j -= 1
        a[j + 1] = x                # drop x into the gap

On $[5, 2, 4, 1]$ : insert $2$ → $[2, 5, 4, 1]$ ; insert $4$ → $[2, 4, 5, 1]$ ; insert $1$ → $[1, 2, 4, 5]$ .

Example— Euclid's algorithm

To find $\gcd(a, b)$ : while $b \ne 0$ , replace $(a, b)$ by $(b, \; a \bmod b)$ ; then the answer is $a$ .

(252, 198) \to (198, 54) \to (54, 36) \to (36, 18) \to (18, 0), \qquad \text{so } \gcd(252, 198) = 18.

See divisibility and Euclid's algorithm for its background.

ProofH

Correctness and running time, proved

Theorem— Theorem 1 (linear search)

Linear search is correct, and it makes at most $n$ comparisons on a list of length $n$ , exactly $n$ when $t$ is absent.

Proof

Invariant: at the start of the pass with index $i$ , $t$ is not among $a_0, \dots, a_{i-1}$ . This holds for $i = 0$ (there is nothing to check), and a pass that does not return has found $a_i \ne t$ , so the invariant holds for $i + 1$ . If the loop returns $i$ , then $a_i = t$ , which is correct. Otherwise the loop runs to the end, and the invariant with $i = n$ says $t$ is absent — correct again. There is one comparison per pass and at most $n$ passes; if $t$ is absent, all $n$ passes happen.

∎

Theorem— Theorem 2 (binary search is correct)

If $a_0 \le a_1 \le \dots \le a_{n-1}$ , binary search terminates, and it returns an index $i$ with $a_i = t$ if $t$ occurs in the list, and "absent" otherwise.

Proof

Invariant: if $t$ occurs in the list, then it occurs at some index in the range $lo, \dots, hi$ .

Initially $lo = 0$ , $hi = n - 1$ : the range is the whole list. ✓
Each pass preserves it. If $a_{mid} = t$ we return a correct answer. If $a_{mid} < t$ , then for every $i \le mid$ we have $a_i \le a_{mid} < t$ because the list is sorted; so $t$ is not at any index up to $mid$ , and if it occurs at all it occurs in $mid + 1, \dots, hi$ — the new range. The case $a_{mid} > t$ is symmetric.
Termination. The measure $hi - lo + 1$ (the size of the range) is a natural number while the loop runs, and each pass removes at least the index $mid$ , so it strictly decreases.
At the end, if nothing was returned, $lo > hi$ : the range is empty. By the invariant, $t$ does not occur, so "absent" is correct.

∎

Theorem— Theorem 3 (binary search is fast)

Binary search on a sorted list of $n \ge 1$ entries makes at most $\lfloor \log_2 n \rfloor + 1$ comparisons. For $n = 1\,000\,000$ that is $20$ .

Proof

Let $m = hi - lo + 1$ be the size of the range. The middle index $mid = \lfloor (lo + hi)/2 \rfloor$ splits off a left part of size $mid - lo = \lfloor (m-1)/2 \rfloor$ and a right part of size $hi - mid = \lceil (m-1)/2 \rceil = \lfloor m/2 \rfloor$ . So after one comparison the new size is at most $\lfloor m/2 \rfloor$ .

Claim: if $m < 2^k$ , at most $k$ comparisons remain. By induction on $k$ . If $k = 0$ then $m = 0$ : the range is empty and the loop stops. If $m < 2^{k+1}$ , one comparison leaves a range of size at most $\lfloor m/2 \rfloor < 2^k$ , after which at most $k$ comparisons remain: $k + 1$ in all.

Finally, $n < 2^{\lfloor \log_2 n \rfloor + 1}$ by definition of $\lfloor \log_2 n \rfloor$ (the largest $j$ with $2^j \le n$ ), so the claim with $k = \lfloor \log_2 n \rfloor + 1$ gives the bound. Since $2^{19} = 524\,288 \le 1\,000\,000 < 2^{20}$ , $\lfloor \log_2 10^6 \rfloor + 1 = 20$ .

∎

The bound is the best possible: if $t$ is larger than every entry, the search always goes right and the size goes $n \to \lfloor n/2 \rfloor \to \lfloor n/4 \rfloor \to \dots$ , which takes exactly $\lfloor \log_2 n \rfloor + 1$ steps to reach $0$ .

Theorem— Theorem 4 (Euclid's algorithm)

For natural numbers $a, b$ , Euclid's algorithm terminates and returns $\gcd(a, b)$ .

Proof

Invariant: the gcd of the current pair equals $\gcd$ of the original pair. Write $a = qb + r$ with $r = a \bmod b$ . Any common divisor of $a$ and $b$ divides $r = a - qb$ ; any common divisor of $b$ and $r$ divides $a = qb + r$ . So the pairs $(a, b)$ and $(b, r)$ have the same common divisors, hence the same greatest one: $\gcd(a, b) = \gcd(b, a \bmod b)$ . Termination: the measure is the second number, which strictly decreases since $0 \le a \bmod b < b$ . At the end $b = 0$ , and $\gcd(a, 0) = a$ is the answer.

∎

Theorem— Theorem 5 (insertion sort)

Insertion sort rearranges any list of $n$ entries into increasing order, using at most $1 + 2 + \dots + (n-1) = \frac{n(n-1)}{2}$ comparisons.

Proof

Invariant: at the start of pass $i$ , the first $i$ entries are the original first $i$ entries, in increasing order. Pass $i$ shifts the entries of that sorted block that are larger than $x = a_i$ one place right and puts $x$ into the gap, so afterwards the first $i + 1$ entries are sorted. At the end ( $i = n$ ) the whole list is sorted, and since entries are only moved, never created or lost, it is a rearrangement of the input. Pass $i$ compares $x$ with at most the $i$ entries before it, so the total is at most $1 + 2 + \dots + (n - 1) = n(n-1)/2$ (Gauss's formula, proved in proof techniques). A list in decreasing order needs every one of these comparisons.

∎

Insertion sort is $O(n^2)$ . Can one do much better? Merge sort splits the list in half, sorts each half (by the same method), and merges the two sorted halves with at most $n - 1$ comparisons. For $n = 2^k$ its worst case $C(n)$ satisfies $C(1) = 0$ and $C(n) \le 2\,C(n/2) + n - 1$ , and induction on $k$ gives $C(2^k) \le k\,2^k - 2^k + 1$ , that is, $C(n) \le n \log_2 n - n + 1$ . So merge sort is $O(n \log n)$ . Could a cleverer method do better still? Here is the surprising answer.

Theorem— Theorem 6 (a limit for every sorting method)

Any sorting method that learns about the input only by comparing two entries at a time needs, in the worst case, at least $\log_2(n!)$ comparisons to sort $n$ different entries. Moreover $\log_2(n!) \ge \frac{n}{2} \log_2 \frac{n}{2}$ , so the number of comparisons grows at least like $n \log_2 n$ .

Proof

Picture the method as a decision tree: the first comparison is the root; its two answers lead to two subtrees, the next comparisons; each leaf is a point where the method stops and announces the sorted order. The worst-case number of comparisons is the height $h$ of the tree, the length of its longest path.

A tree of height $h$ has at most $2^h$ leaves. By induction: a single leaf has height $0$ and $2^0 = 1$ leaf; a tree whose root has subtrees of heights at most $h - 1$ has at most $2^{h-1} + 2^{h-1} = 2^h$ leaves.
A correct method needs at least $n!$ leaves. The $n$ entries can arrive in $n!$ different orders, and each order requires a different rearrangement to sort it. Two different orders cannot end at the same leaf, because the leaf announces one rearrangement.

So $n! \le 2^h$ , that is, $h \ge \log_2(n!)$ . For the estimate, at least $n/2$ of the factors of $n! = 1 \cdot 2 \cdots n$ (those from $\lceil n/2 \rceil$ to $n$ ) are each at least $n/2$ , and the rest are at least $1$ , so $n! \ge (n/2)^{n/2}$ and $\log_2(n!) \ge \frac{n}{2}\log_2 \frac{n}{2}$ .

∎

For $n = 5$ : $5! = 120 > 64 = 2^6$ , so every method needs 7 comparisons in the worst case on five items. Merge sort is therefore within a constant factor of the best possible. (The theorem says nothing about methods that do not work by comparisons, such as sorting exam scripts into 26 piles by first letter — those can beat $n \log n$ in special situations.)

ExplanationH

Growth rates, and why faster computers do not save us

Suppose a computer performs a billion ( $10^9$ ) basic steps per second. Here is how long algorithms with different running times take on inputs of size $n$ :

$n$	$\log_2 n$	$n$	$n \log_2 n$	$n^2$	$2^n$
$10$	instant	instant	instant	instant	$1$ microsecond
$1000$	instant	$1$ microsecond	$10$ microseconds	$1$ millisecond	longer than the age of the universe
$10^6$	instant	$1$ millisecond	$20$ milliseconds	$17$ minutes	—
$10^9$	instant	$1$ second	$30$ seconds	$32$ years	—

How running times grow

Move the sliders and trace along the curves to read off values.

log₂ n
n
n log₂ n
n²

Trace along xx = 1

log₂ n: y = 0
n: y = 1
n log₂ n: y = 0
n²: y = 1

A faster computer helps far less than a better algorithm. If a new machine is $1000$ times faster, then in the same time:

a linear-time algorithm ( $n$ steps) can handle $1000$ times as much data;
a quadratic algorithm ( $n^2$ steps) only $\sqrt{1000} \approx 31.6$ times as much, because $(31.6\,n)^2 \approx 1000\,n^2$ ;
an exponential algorithm ( $2^n$ steps) only about $10$ more items, because $2^{n + 10} = 1024 \cdot 2^n$ .

Formal mathematicsF

Correctness checked by Lean

In Lean, loops are written as recursive functions: each recursive call is one pass of the loop, and Lean only accepts the definition if it can see a termination measure that decreases. Here is linear search, its correctness, and its comparison count:

linearSearchLean 4Formally verified

/-- **Linear search**: is `t` in the list? Compare `t` with each entry in turn. -/
def linearSearch (t : ℕ) : List ℕ → Bool
  | [] => false
  | x :: xs => x == t || linearSearch t xs

Axioms used: No axiomsformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

linearSearch_correctLean 4Proved here from basic factsFormally verified

/-- **Linear search is correct**: it answers `true` exactly when `t` is in the list. Proof by
induction on the list (the loop invariant "`t` is not among the entries already checked"). -/
theorem linearSearch_correct (t : ℕ) (xs : List ℕ) : linearSearch t xs = true ↔ t ∈ xs := by
  induction xs with
  | nil => simp [linearSearch]
  | cons x xs ih => simp [linearSearch, ih, @eq_comm _ x t]

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

linearComparisonsLean 4Formally verified

/-- The number of comparisons linear search makes: it stops at the first match. -/
def linearComparisons (t : ℕ) : List ℕ → ℕ
  | [] => 0
  | x :: xs => if x = t then 1 else 1 + linearComparisons t xs

Axioms used: No axiomsformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

linearComparisons_leLean 4Proved here from basic factsFormally verified

/-- Linear search makes **at most `n` comparisons** on a list of length `n`. -/
theorem linearComparisons_le (t : ℕ) (xs : List ℕ) : linearComparisons t xs ≤ xs.length := by
  induction xs with
  | nil => simp [linearComparisons]
  | cons x xs ih =>
    simp only [linearComparisons, List.length_cons]
    split_ifs <;> omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

linearComparisons_absentLean 4Proved here from basic factsFormally verified

/-- …and **exactly `n`** when `t` is absent: the worst case really happens. -/
theorem linearComparisons_absent (t : ℕ) (xs : List ℕ) (h : t ∉ xs) :
    linearComparisons t xs = xs.length := by
  induction xs with
  | nil => simp [linearComparisons]
  | cons x xs ih =>
    have hx : x ≠ t := fun hxt => h (hxt ▸ List.mem_cons_self)
    have hxs : t ∉ xs := fun ht => h (List.mem_cons_of_mem x ht)
    simp [linearComparisons, hx, ih hxs]
    omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

For binary search we formalise the closely related "first yes" form, which finds the first point where a monotone yes/no test becomes true — the form behind "twenty questions", and behind finding the first entry $\ge t$ in a sorted list. The invariant and the halving argument are those of Theorems 2 and 3; note the termination_by hi - lo, Lean's version of our termination measure.

bsearchLean 4Formally verified

/-- **Binary search for the first "yes".** `p` is a yes/no test on `lo, …, hi`. Probe the
middle `m = ⌊(lo + hi)/2⌋`: if `p m` is true, the first "yes" is at most `m`, so continue with
`lo, …, m`; otherwise it is after `m`, so continue with `m + 1, …, hi`. Stop when `lo = hi`.
Lean accepts the definition because `hi - lo` strictly decreases at each call. -/
def bsearch (p : ℕ → Bool) (lo hi : ℕ) : ℕ :=
  if lo < hi then
    if p ((lo + hi) / 2) then bsearch p lo ((lo + hi) / 2)
    else bsearch p ((lo + hi) / 2 + 1) hi
  else lo
termination_by hi - lo
decreasing_by all_goals omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

bsearch_correctLean 4Proved here from basic factsFormally verified

/-- **Binary search is correct.** Suppose `p` is monotone (once true, it stays true). The
**loop invariant** is:
* `lo ≤ hi`,
* `p hi` is true (there is a "yes" at the right end), and
* `p k` is false for every `k < lo` (everything left of `lo` is a "no").
It holds initially by hypothesis, and each probe preserves it: if `p m` is true we move `hi`
down to `m`; if `p m` is false then, by monotonicity, so is every `k ≤ m`, and we move `lo`
up to `m + 1`. When the loop stops, `lo = hi`, and the invariant says exactly that `lo` is
the first "yes". The proof is a strong induction on the size `hi - lo` (the **termination
measure**). -/
theorem bsearch_correct (p : ℕ → Bool) (hmono : ∀ a b, a ≤ b → p a = true → p b = true) :
    ∀ lo hi, lo ≤ hi → p hi = true → (∀ k, k < lo → p k = false) →
      p (bsearch p lo hi) = true ∧ ∀ k, k < bsearch p lo hi → p k = false := by
  intro lo hi
  induction h : hi - lo using Nat.strong_induction_on generalizing lo hi with
  | _ n ih =>
    intro hle hhi hlo
    rw [bsearch]
    split_ifs with hlt hp
    · -- `p m` true: continue on `lo, …, m`; the invariant holds with `hi := m`.
      exact ih ((lo + hi) / 2 - lo) (by omega) lo ((lo + hi) / 2) rfl (by omega) hp hlo
    · -- `p m` false: continue on `m + 1, …, hi`; everything up to `m` is a "no".
      refine ih (hi - ((lo + hi) / 2 + 1)) (by omega) ((lo + hi) / 2 + 1) hi rfl (by omega) hhi ?_
      intro k hk
      cases hpk : p k with
      | false => rfl
      | true => exact absurd (hmono k ((lo + hi) / 2) (by omega) hpk) hp
    · -- `lo = hi`: the invariant says `lo` is the first "yes".
      have hEq : lo = hi := by omega
      subst hEq
      exact ⟨hhi, hlo⟩

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

bsearchStepsLean 4Formally verified

/-- The number of probes `bsearch` makes on `lo, …, hi` (same recursion, counting `1` per
probe). -/
def bsearchSteps (p : ℕ → Bool) (lo hi : ℕ) : ℕ :=
  if lo < hi then
    1 + if p ((lo + hi) / 2) then bsearchSteps p lo ((lo + hi) / 2)
        else bsearchSteps p ((lo + hi) / 2 + 1) hi
  else 0
termination_by hi - lo
decreasing_by all_goals omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

bsearchSteps_leLean 4Proved here from basic factsFormally verified

/-- **Halving bound.** If the range has fewer than `2^k` points beyond `lo` (that is,
`hi - lo < 2^k`), binary search makes at most `k` probes. Each probe leaves a range of size at
most `⌊(hi - lo)/2⌋ < 2^(k-1)`; induction on `k`. -/
theorem bsearchSteps_le (p : ℕ → Bool) :
    ∀ k lo hi, hi - lo < 2 ^ k → bsearchSteps p lo hi ≤ k := by
  intro k
  induction k with
  | zero =>
    intro lo hi h
    have hlt : ¬ lo < hi := by simp at h; omega
    rw [bsearchSteps]
    simp [hlt]
  | succ k ih =>
    intro lo hi h
    rw [Nat.pow_succ] at h
    rw [bsearchSteps]
    split_ifs with hlt hp
    · have := ih lo ((lo + hi) / 2) (by omega)
      omega
    · have := ih ((lo + hi) / 2 + 1) hi (by omega)
      omega
    · omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

bsearchSteps_le_logLean 4Proved here from basic factsFormally verified

/-- **Binary search makes at most `⌊log₂ n⌋ + 1` probes** on a range of size `n = hi - lo`.
Since `n < 2^(⌊log₂ n⌋ + 1)` (`Nat.lt_pow_succ_log_self`), this is `bsearchSteps_le`. -/
theorem bsearchSteps_le_log (p : ℕ → Bool) (lo hi : ℕ) :
    bsearchSteps p lo hi ≤ Nat.log 2 (hi - lo) + 1 :=
  bsearchSteps_le p _ lo hi (Nat.lt_pow_succ_log_self Nat.one_lt_two _)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

Euclid's algorithm, with its invariant:

euclidLean 4Formally verified

/-- **Euclid's algorithm**: replace `(a, b)` by `(b, a mod b)` until `b = 0`; answer `a`. It
terminates because the second number strictly decreases (`a mod b < b`). -/
def euclid (a b : ℕ) : ℕ :=
  if b = 0 then a else euclid b (a % b)
termination_by b
decreasing_by exact Nat.mod_lt a (by omega)

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

euclid_eq_gcdLean 4Proved here from basic factsFormally verified

/-- **Euclid's algorithm is correct**: `euclid a b = gcd(a, b)`. The loop invariant is that
the gcd of the current pair never changes: `gcd(a, b) = gcd(b, a mod b)` (from `Nat.gcd_rec`
and `Nat.gcd_comm`), and at the end `gcd(a, 0) = a`. Strong induction on `b`. -/
theorem euclid_eq_gcd (a b : ℕ) : euclid a b = Nat.gcd a b := by
  induction b using Nat.strong_induction_on generalizing a with
  | _ b ih =>
    rw [euclid]
    split_ifs with hb
    · subst hb
      exact (Nat.gcd_zero_right a).symm
    · rw [ih (a % b) (Nat.mod_lt a (Nat.pos_of_ne_zero hb)) b]
      -- invariant: gcd(b, a mod b) = gcd(a mod b, b) = gcd(b, a) = gcd(a, b)
      rw [Nat.gcd_comm b (a % b), ← Nat.gcd_rec b a, Nat.gcd_comm b a]

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

For sorting, Mathlib already proves that its insertion sort meets the specification, and we prove the decision-tree lower bound:

insertionSort_sortedLean 4Applies a library theoremFormally verified

/-- Insertion sort returns a **sorted** list: Mathlib's `List.pairwise_insertionSort` (sorted
means every earlier entry is `≤` every later one). -/
theorem insertionSort_sorted (l : List ℕ) :
    (l.insertionSort (· ≤ ·)).Pairwise (· ≤ ·) :=
  List.pairwise_insertionSort _ l

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

insertionSort_permLean 4Applies a library theoremFormally verified

/-- …which is a **rearrangement** of the input (`~` means "permutation of"):
Mathlib's `List.perm_insertionSort`. Together: insertion sort meets its specification. -/
theorem insertionSort_perm (l : List ℕ) : (l.insertionSort (· ≤ ·)).Perm l :=
  List.perm_insertionSort _ l

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

DecisionTreeLean 4Formally verified

/-- A **binary decision tree**: each internal node is one yes/no comparison with two
subtrees for the two answers; each leaf is a final answer. -/
inductive DecisionTree where
  | leaf : DecisionTree
  | node : DecisionTree → DecisionTree → DecisionTree

Axioms used: No axiomsformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

leavesLean 4Formally verified

/-- The number of leaves (possible final answers). -/
def DecisionTree.leaves : DecisionTree → ℕ
  | leaf => 1
  | node l r => l.leaves + r.leaves

Axioms used: No axiomsformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

heightLean 4Formally verified

/-- The height: the largest number of comparisons on any path from the root to a leaf, i.e.
the worst-case number of comparisons. -/
def DecisionTree.height : DecisionTree → ℕ
  | leaf => 0
  | node l r => max l.height r.height + 1

Axioms used: No axiomsformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

leaves_le_two_pow_heightLean 4Proved here from basic factsFormally verified

/-- **A decision tree of height `h` has at most `2^h` leaves.** Each comparison at most
doubles the number of reachable outcomes: by induction,
`leaves ≤ 2^(height l) + 2^(height r) ≤ 2 · 2^(max) = 2^(max + 1)`. -/
theorem leaves_le_two_pow_height : ∀ t : DecisionTree, t.leaves ≤ 2 ^ t.height
  | .leaf => by simp [DecisionTree.leaves, DecisionTree.height]
  | .node l r => by
    have hl := leaves_le_two_pow_height l
    have hr := leaves_le_two_pow_height r
    have hl' : 2 ^ l.height ≤ 2 ^ max l.height r.height :=
      Nat.pow_le_pow_right Nat.two_pos (le_max_left _ _)
    have hr' : 2 ^ r.height ≤ 2 ^ max l.height r.height :=
      Nat.pow_le_pow_right Nat.two_pos (le_max_right _ _)
    simp only [DecisionTree.leaves, DecisionTree.height, Nat.pow_succ]
    omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

sorting_lower_boundLean 4Proved here from basic factsFormally verified

/-- **Lower bound for comparison sorting.** A decision tree that sorts `n` distinct items must
be able to give `n!` different answers (one for each order of the input), so it has at least
`n!` leaves. Then `n! ≤ 2^height`: in the worst case it makes at least `log₂ n!`
comparisons. -/
theorem sorting_lower_bound (n : ℕ) (t : DecisionTree) (h : n.factorial ≤ t.leaves) :
    n.factorial ≤ 2 ^ t.height :=
  h.trans (leaves_le_two_pow_height t)

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

five_items_need_sevenLean 4Proved here from basic factsFormally verified

/-- **Sorting 5 items needs 7 comparisons** in the worst case: `5! = 120 > 64 = 2^6`, so a
tree with at least 120 leaves has height at least 7. (Seven comparisons also suffice, by a
clever method; that part is not formalised here.) -/
theorem five_items_need_seven (t : DecisionTree) (h : Nat.factorial 5 ≤ t.leaves) :
    7 ≤ t.height := by
  have h2 := sorting_lower_bound 5 t h
  by_contra hlt
  have h6 : 2 ^ t.height ≤ 2 ^ 6 := Nat.pow_le_pow_right Nat.two_pos (by omega)
  have h120 : Nat.factorial 5 = 120 := rfl
  omega

Axioms used: propext, Quot.soundformal/Lumenary/AlgorithmsAndEfficiency.leanTry it in the Lean web editor

ComputationC

Counting comparisons

Linear and binary search: counting the comparisonsPythonExhaustive finite checkExact computationComputationally tested

"""Linear search versus binary search: counting comparisons.

Binary search on a sorted list probes the middle entry and throws away half
of what is left. We count probes exactly: for every list size n up to 200
and every possible target (present or absent) the largest number of probes
is found by running the search, and compared with floor(log2 n) + 1. Then we
race the two searches on huge sorted lists (stored as a rule a[i] = 2i, so
nothing is allocated) and show why a faster computer does not rescue a slow
algorithm. Exhaustive-finite for the sizes tested; the lesson proves the
bound for every n.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import math
import textwrap

def linear_search(key, n, target):
    """Scan a[0], a[1], ...; return (index or None, comparisons made).

    ``key(i)`` gives the entry a[i] of a list of length ``n``.
    """
    for i in range(n):
        if key(i) == target:
            return i, i + 1
    return None, n

def binary_search(key, n, target):
    """Search a sorted list a[0] <= ... <= a[n-1]; return (index or None, probes).

    Invariant: if the target is in the list, its index is in lo..hi.
    Each probe compares the target with the middle entry a[mid].
    """
    lo, hi = 0, n - 1
    probes = 0
    while lo <= hi:
        mid = (lo + hi) // 2
        probes += 1
        value = key(mid)
        if value == target:
            return mid, probes
        if value < target:
            lo = mid + 1
        else:
            hi = mid - 1
    return None, probes

def evens(i):
    """The sorted list 0, 2, 4, ... given as a rule."""
    return 2 * i

def worst_binary_probes(n):
    """Largest number of probes over every target -1, 0, 1, ..., 2n - 1."""
    return max(binary_search(evens, n, t)[1] for t in range(-1, 2 * n))

def log2_floor(n):
    """floor(log2 n) for n >= 1, computed exactly with integers."""
    return n.bit_length() - 1

def main():
    agree = all(worst_binary_probes(n) == log2_floor(n) + 1
                for n in range(1, 201))
    print("Binary search, every target, every size n = 1..200:")
    print(f"  worst case = floor(log2 n) + 1 probes for every n: {agree}")
    for n in (7, 8, 100, 128):
        print(f"  n = {n:>3}: worst {worst_binary_probes(n)} probes")
    print()
    print(f"{'list size n':>18}  {'linear (worst)':>18}  {'binary (worst)':>14}")
    for k in (1, 2, 3, 6, 9, 12):
        n = 10 ** k
        probes = binary_search(evens, n, 2 * n)[1]  # target beyond the end
        if n <= 1000:
            lin = f"{linear_search(evens, n, -1)[1]:,}"  # absent: run it
        else:
            lin = f"{n:,}*"
        print(f"{n:>18,}  {lin:>18}  {probes:>14}")
    print("* not run: an absent target forces linear search to check all n")
    print()
    speedup = 1000
    print(f"A computer {speedup} times faster, in the same time, handles:")
    print(f"  linear-time algorithm:    {speedup} times as much data")
    print(f"  quadratic-time algorithm: {math.sqrt(speedup):.1f} times as much data")
    print(f"  2^n-time algorithm:       only {math.log2(speedup):.1f} more items")
    print()
    print(textwrap.fill(
        "Epistemic status: exhaustive-finite and exact. The worst case of "
        "binary search was found by running every target for every n up to "
        "200; the large-n rows are exact counts from real runs. That the worst "
        "case is floor(log2 n) + 1 for every n is the lesson's theorem, proved "
        "by halving (and formalised in Lean); the runs only illustrate it.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Counting comparisons in insertion sort and merge sortPythonExhaustive finite checkExperimental evidenceComputationally tested

"""How many comparisons does sorting take? Insertion sort, merge sort, and a floor.

We count the comparisons made by insertion sort and merge sort. On every
ordering of n = 1..7 items we find each method's worst case exactly and set
it beside the lower bound ceil(log2 n!) that no comparison sort can beat.
Then we sort seeded random lists of 100 and 1000 numbers and compare the
counts with n(n - 1)/4 (insertion sort's average) and log2 n!.
Exhaustive-finite for n <= 7, a seeded experiment for the large lists.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import permutations
import math
import random
import textwrap

def insertion_sort(items):
    """Return (sorted copy, number of comparisons) using insertion sort.

    Invariant: before step i, the first i entries are sorted.
    """
    a = list(items)
    comparisons = 0
    for i in range(1, len(a)):
        x = a[i]
        j = i - 1
        while j >= 0:
            comparisons += 1
            if a[j] <= x:
                break
            a[j + 1] = a[j]
            j -= 1
        a[j + 1] = x
    return a, comparisons

def merge_sort(items):
    """Return (sorted copy, number of comparisons) using merge sort."""
    a = list(items)
    if len(a) <= 1:
        return a, 0
    mid = len(a) // 2
    left, c1 = merge_sort(a[:mid])
    right, c2 = merge_sort(a[mid:])
    merged, comparisons = [], c1 + c2
    i = j = 0
    while i < len(left) and j < len(right):
        comparisons += 1
        if left[i] <= right[j]:
            merged.append(left[i])
            i += 1
        else:
            merged.append(right[j])
            j += 1
    merged.extend(left[i:])
    merged.extend(right[j:])
    return merged, comparisons

def lower_bound(n):
    """ceil(log2 n!): the fewest worst-case comparisons any method can need."""
    return (math.factorial(n) - 1).bit_length()

def worst_case(sort, n):
    """Largest comparison count of ``sort`` over all n! orderings of 0..n-1."""
    return max(sort(p)[1] for p in permutations(range(n)))

def main():
    print(" n   n!   insertion   merge   lower bound ceil(log2 n!)")
    for n in range(1, 8):
        ins, mer = worst_case(insertion_sort, n), worst_case(merge_sort, n)
        print(f"{n:>2} {math.factorial(n):>4}   {ins:>9}   {mer:>5}   {lower_bound(n):>5}")
    print("Insertion sort's worst case is n(n - 1)/2 (a reversed list).")
    print()
    rng = random.Random(2024)
    print("Seeded random lists (one run each):")
    print("    n   insertion   n(n-1)/4    merge   log2(n!)")
    for n in (100, 1000):
        data = [rng.random() for _ in range(n)]
        s1, ins = insertion_sort(data)
        s2, mer = merge_sort(data)
        assert s1 == s2 == sorted(data)
        bound = math.lgamma(n + 1) / math.log(2)
        print(f"{n:>5}   {ins:>9,}   {n * (n - 1) / 4:>8,.0f}   {mer:>6,}"
              f"   {bound:>8,.0f}")
    print()
    print(textwrap.fill(
        "Epistemic status: the table for n <= 7 is exhaustive and exact - every "
        "ordering was sorted. The random rows are a seeded experiment: one "
        "input each, so they show typical behaviour, not a theorem. The lower "
        "bound log2(n!) is the lesson's decision-tree theorem; insertion "
        "sort's n(n - 1)/2 worst case and merge sort's n log2 n growth are "
        "proved or sketched there.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The small- $n$ table is exhaustive: every input was tried, so those worst cases are certain. Merge sort sits close to the lower bound; insertion sort pulls away quickly. The random lists are a seeded experiment — one input each — showing typical behaviour: insertion sort makes about $n^2/4$ comparisons on a random list, merge sort about $n \log_2 n$ .

Explore

Explore: Euclid's algorithm as cutting squares

Euclid's algorithm has a beautiful picture: from an $a \times b$ rectangle, cut the largest possible squares; then do the same to the leftover strip. Each round of cutting is one step $(a, b) \to (b, a \bmod b)$ , and the side of the last square is the gcd. Try consecutive Fibonacci numbers such as $21$ and $13$ , which make Euclid work hardest.

Euclid's algorithm: cutting squares

Each round of squares is one step of the algorithm.

Width21Height13

21 × 13

Step 1 of 7

A 21 by 13 rectangle. Press “Next step” to cut off the biggest squares that fit.

Exercises

1. Algorithms, correctness and efficiency

Warm-upHuman

What is the largest number of comparisons binary search can make on a sorted list of $1000$ entries?

2. Algorithms, correctness and efficiency

Warm-upHuman

How many comparisons does insertion sort make, in the worst case, to sort a list of $10$ entries?

3. Algorithms, correctness and efficiency

CoreHuman

This loop adds up a list $a$ of length $n$ :

s = 0
for i in range(n):      # i = 0, 1, ..., n - 1
    s = s + a[i]

Which statement is a loop invariant that holds at the start of each pass (before $a_i$ is added) and proves that $s$ is the total at the end?

Choose one

s = a_0 + a_1 + \dots + a_{i-1}

s = a_0 + a_1 + \dots + a_i

s \ge 0

s = a_0 + a_1 + \dots + a_{n-1}

4. Algorithms, correctness and efficiency

CoreHuman

A classmate's sorting function passed $1000$ random tests on lists of up to $50$ numbers. Which statement is correct?

Choose one

This is evidence that the function works, but it does not prove it works on every list.It is now proved correct for all lists of length at most

50

.It is proved correct, since

1000

is a large number of tests.The tests are useless; only proofs matter.

5. Algorithms, correctness and efficiency

CoreHuman

An algorithm takes $n^2$ steps on inputs of size $n$ . A new computer is $100$ times faster. In the time the old computer needed for size $n$ , the new one can handle size $k \cdot n$ . What is $k$ ?

6. Algorithms, correctness and efficiency

CoreHuman

In the correctness proof of binary search, suppose $a_{mid} < t$ . Why may we discard the indices $lo, \dots, mid$ ?

Choose one

The list is sorted, so

a_i \le a_{mid} < t

for every

i \le mid

: none of these entries equals

t

.Because

mid

is the middle, so

t

is equally likely to be in either half.Because we have already compared

t

with all of

a_{lo}, \dots, a_{mid}

.Because

lo \le mid \le hi

7. Algorithms, correctness and efficiency

CoreFormal

Let r := bsearch p lo hi. Which Lean proposition says that r is the first point where the test p gives true?

Choose one

p r = true ∧ ∀ k, k < r → p k = falsep r = true∃ k, p k = true∀ k, k < r → p k = true

8. Algorithms, correctness and efficiency

CoreComputational

Write binary_search(a, t) for a sorted list a. Return a pair (index, probes): an index i with a[i] == t (or -1 if t is absent), and the number of times you compared t with an entry of the list. The tests check correctness on many lists and that probes never exceeds $\lfloor \log_2 n \rfloor + 1$ , which is len(a).bit_length() in Python.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

9. Algorithms, correctness and efficiency

StretchHuman

Using the decision-tree argument (Theorem 6), what is the smallest number of comparisons that any comparison-based method could need, in the worst case, to sort $5$ different numbers?

10. Algorithms, correctness and efficiency

StretchHuman

Run Euclid's algorithm on $(89, 55)$ . How many divisions with remainder does it perform before reaching a pair whose second number is $0$ ? (Count every step $(a, b) \to (b, a \bmod b)$ .)

Common misconceptionsH

Common misconceptions

Misconception

"It passed all my tests, so it is correct." Tests examine finitely many inputs; correctness is about all of them. Java's binary search passed its tests for years before failing on lists of a billion entries. Tests find bugs; proofs (with a loop invariant and a termination measure) show there are none — relative to the specification.

Misconception

"Faster computers make efficiency irrelevant." A thousandfold speed-up lets a quadratic algorithm handle only about $32$ times more data, and an exponential one only $10$ more items. Meanwhile data keeps growing. Algorithmic improvements — from $n^2$ to $n \log n$ — routinely matter more than decades of hardware progress.

Misconception

"Binary search works on any list." It relies on sortedness in the invariant step ("every entry left of $mid$ is at most $a_{mid}$ "). On an unsorted list it can miss an entry that is present.

Misconception

" $O(n \log n)$ is always faster than $O(n^2)$ ." Big-O ignores constant factors and small inputs. For short lists insertion sort often beats merge sort in practice, which is why real sorting libraries switch to insertion sort for small pieces. Big-O describes growth, for large $n$ .

Misconception

"An algorithm that always gives the right answer when it stops is correct." That is only partial correctness. A full proof also needs termination: a loop that never ends never gives a wrong answer — and never gives any answer.

ViewpointsH

The same ideas, seen by others

Number theory— The worst case of Euclid

How many steps can Euclid's algorithm take? The slowest inputs are consecutive Fibonacci numbers: $(89, 55) \to (55, 34) \to (34, 21) \to \cdots \to (2, 1) \to (1, 0)$ uses nine divisions, and at each step the quotient is $1$ , the smallest possible. Gabriel Lamé proved in 1844 that the number of division steps is never more than five times the number of decimal digits of the smaller number — the first analysis of an algorithm's running time. So Euclid is fast: $O(\log b)$ steps.

Combinatorics— Counting orders and leaves

The lower bound of Theorem 6 is pure counting: $n!$ orders, at most $2^h$ leaves. The sharper estimate comes from Stirling's formula, $\log_2(n!) = n \log_2 n - n \log_2 e + O(\log n)$ , so about $n \log_2 n - 1.44\,n$ comparisons are unavoidable. For small $n$ the exact minimum is known only for limited ranges, and finding it is a hard combinatorial search: for $n = 12$ the answer ( $30$ , one more than $\lceil \log_2 12! \rceil = 29$ ) was settled by computer only in the 1960s.

Analysis— Asymptotics

Comparing $n \log n$ with $n^2$ is a question about limits: $\frac{n \log n}{n^2} = \frac{\log n}{n} \to 0$ , so eventually $n \log n$ is tiny compared with $n^2$ , whatever the constants. Estimating $\log(n!) = \sum_{k=1}^{n} \log k$ by the integral $\int_1^n \log x \, dx = n \log n - n + 1$ is the analyst's route to Stirling's formula, and the same comparison of sums with integrals measures many other algorithms. See sequences and series.

Algebra— Fast powers from associativity

To compute $a^{1000}$ you need not multiply $999$ times. Square repeatedly — $a^2, a^4, a^8, \dots, a^{512}$ — and multiply the powers for the binary digits of $1000 = 512 + 256 + 128 + 64 + 32 + 8$ : $9$ squarings and $5$ further multiplications, $14$ in all — $O(\log n)$ in general. The method works in any structure with an associative operation (numbers mod $m$ , matrices, compositions of functions), because associativity guarantees that regrouping the factors does not change the answer — see Composition. It is the reason modern cryptography can raise numbers to enormous powers in milliseconds.

Logic— What can and cannot be decided

Could a program check, for every program, whether it terminates? Alan Turing proved in 1936 that no algorithm can do this (the halting problem). So there is no general machine for proving algorithms correct: each proof needs an idea, such as an invariant or a measure. Robert Floyd (1967) and Tony Hoare (1969) turned loop invariants into a logic of programs — Hoare logic — and proof assistants like Lean check such proofs mechanically. See computability and First steps in Lean.

Probability— The average case

If the target is in the list and every position is equally likely, linear search makes on average $\frac{1 + 2 + \dots + n}{n} = \frac{n + 1}{2}$ comparisons — half the worst case, but still linear. On a random ordering, insertion sort's comparisons are close to the number of inversions (pairs in the wrong order), whose average is $\frac{n(n-1)}{4}$ , since each of the $\binom{n}{2}$ pairs is out of order with probability $\frac12$ . Randomness can also be a tool: quicksort with randomly chosen pivots makes about $2n \ln n \approx 1.39\, n \log_2 n$ comparisons on average, for every input.

History & global context

History and global context

Euclid's algorithm appears in Euclid's Elements (Book VII, around 300 BCE), and is one of the oldest algorithms still in daily use. The Chinese Nine Chapters on the Mathematical Art reduces fractions by repeated subtraction, the same idea; Āryabhaṭa's kuṭṭaka (India, 499) extends it to solve equations $ax + by = c$ .
The word algorithm comes from the name of Muḥammad ibn Mūsā al-Khwārizmī, who worked in Baghdad's House of Wisdom in the 9th century; Latin translations of his book on Hindu–Arabic numerals began "Dixit Algorizmi".
Ada Lovelace's notes (1843) on Charles Babbage's Analytical Engine include a detailed method for computing Bernoulli numbers on the machine, often called the first published computer program.
In 1936 Alan Turing and Alonzo Church gave precise definitions of "algorithm" and showed that some problems have none. John von Neumann described merge sort in 1945; binary search was described by John Mauchly in 1946.
Robert Floyd (1967) and Tony Hoare (1969) introduced invariant-based proofs of programs; Donald Knuth's The Art of Computer Programming (from 1968) made the analysis of algorithms a mathematical subject.

Twenty questions

Why testing is not enough

Definitions

Four algorithms

Correctness and running time, proved

Growth rates, and why faster computers do not save us

Correctness checked by Lean

Counting comparisons

Explore: Euclid's algorithm as cutting squares

Exercises

Common misconceptions

The same ideas, seen by others

History and global context

Further reading