---
title: What Is an Algorithm?
module: Foundations
moduleNumber: 1
lessonNumber: 1
order: 101
summary: >
  An algorithm is a finite, mechanical recipe that transforms inputs into
  outputs. We define what counts as an algorithm, how we write one down, and
  the three things we always ask of it: is it correct, is it fast, and can we
  prove it.
topics: [Foundations, Correctness & Induction]
sources:
  - book: Erickson
    ref: "Ch. 0 — Introduction"
  - book: CLRS
    ref: "Ch. 1 — The Role of Algorithms"
  - book: Skiena
    ref: "§1.1–1.3 — Introduction to Algorithm Design"
practice:
  - title: 'Two Sum'
    slug: two-sum
    difficulty: Easy
  - title: 'Fizz Buzz'
    slug: fizz-buzz
    difficulty: Easy
  - title: 'Palindrome Number'
    slug: palindrome-number
    difficulty: Easy
  - title: 'Reverse Integer'
    slug: reverse-integer
    difficulty: Medium
---

You have already met dozens of algorithms without being told that's what
they were. [Merge sort](/algorithms/divide-and-conquer/mergesort),
[quicksort](/algorithms/divide-and-conquer/quicksort), binary search, linear
search, [breadth-first
search](/algorithms/graphs/representations-and-traversal); even the rote
procedures for multiplying ($374 \times 285$) or adding
($724 + 1366$) two integers by hand; even tidying a room by a fixed set of
rules. A simple working definition unites them:

> **Definition (Algorithm).** An algorithm is _a precise recipe of steps for solving a computational
> problem_, where a _computational problem_ is anything with
> a notion of an **input** and a corresponding **output**.

```py [fib.py] {2,3}
def fib(n: int) -> int:
  if n <= 1:
    return n
  return fib(n-1) + fib(n-2)

def fib2(n: int) -> int:
  M = [0, 1]
  for i in range(1, n):
    M.append(M[-1] + M[-2])
  return M[-1]
```

```hs [fib.hs]
fib :: Int -> Int
fib 0 = 0
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

fib2 :: Int -> Int
fib2 n
  | n <= 1    = n
  | otherwise = fib2 (n - 1) + fib2 (n - 2)
```

That definition is deliberately blunt. Erickson sharpens it the same way: an
algorithm is a procedure a _rock_ could follow, where every step is so
mechanical that no intelligence, intuition, or luck is required to carry it
out.[^erickson] CLRS frames it operationally: a "well-defined computational
procedure" that takes a value (or set of values) as input and produces a value
as output.[^clrs] Skiena adds the engineer's caveat: it must work _correctly on
every instance_, not merely on the examples we happen to test.[^skiena]

Pull those framings apart and you get a checklist. A procedure earns the name
_algorithm_ only if it is:

- **Finite.** It halts after finitely many steps on every valid input.
  "Repeat until it looks sorted" is not a step count you can bound.
- **Definite.** Every step is unambiguous: two executors starting from the same
  state and reading the same step do the same thing. "Pick a good pivot" fails
  this test until you say _which_ element.
- **Effective.** Each step is basic enough to actually carry out: compare two
  numbers, copy a cell, add. "Factor the integer" is a legal step only if you
  already hold an algorithm for factoring.
- **Anchored to a problem.** It consumes specified inputs and produces specified
  outputs. A procedure that produces nothing computes nothing.

The multiplication procedure you learned as a child passes all four; "season to
taste" fails definiteness, and a program that loops forever on one unlucky
input fails finiteness. Three demands run through everything that does pass,
and through this entire course:

- **Correctness.** The algorithm produces the right output on _every_ valid
  input. One counterexample is enough to sink it.
- **Efficiency.** It uses few resources (time, space) as the input grows.
- **Provability.** We can _argue_, rather than assert, that the first two hold.

## Communicating an algorithm

Having an algorithm in your head is not enough; you must convey it so that
someone else can run it, trust it, and predict its cost. In this course every
algorithm comes with **four deliverables**:

1. **High-level idea.** One or two sentences of plain English.
2. **Pseudocode.** The steps, precise enough to analyze.
3. **Proof of correctness.** An argument that it always returns the right
   answer.
4. **Complexity analysis.** How its running time (and sometimes space) grows
   with the input.

These four form a pipeline. The
**problem spec** fixes what counts as a correct answer; the **idea** and
**pseudocode** are two resolutions of the same method; the **proof** certifies
the pseudocode against the spec; and the **analysis** measures that same
pseudocode. Each deliverable feeds the next.

$$
% caption: The four deliverables as a pipeline: the problem spec anchors everything; idea
%          and pseudocode refine the method; proof checks the pseudocode against the spec;
%          analysis measures the same pseudocode.
\begin{tikzpicture}[
    box/.style={draw, minimum height=8mm, inner sep=2.6mm, font=\small, align=center},
    lbl/.style={font=\footnotesize},
    >={Stealth[length=2.4mm]}]
  \definecolor{acc}{HTML}{2348F2}
  \useasboundingbox (-2.6,-2.5) rectangle (12.3,1.4);
  \node[box, fill=acc!15, draw=acc, very thick] (spec) at (0,0) {problem\\spec};
  \node[box] (idea) at (3.0,0) {high-level\\idea};
  \node[box] (code) at (6.1,0) {pseudo-\\code};
  \node[box] (ana) at (9.4,0) {complexit\/y\\analysis};
  \node[box, fill=acc!15] (proof) at (6.1,-2.0) {pro\/of of\\correctness};
  \draw[->, thick] (spec) -- (idea);
  \draw[->, thick] (idea) -- (code);
  \draw[->, thick] (code) -- (ana);
  \draw[->, thick] (code) -- (proof) node[midway, right, lbl] {certify};
  \draw[->, thick] (spec.south) .. controls +(0,-1.4) and +(-1.6,0) .. (proof.west)
    node[pos=0.62, below, lbl] {def\/ines correct};
  \node[lbl, above=0.5mm of idea] {\itshape what};
  \node[lbl, above=0.5mm of ana] {\itshape how fast};
\end{tikzpicture}
$$

We will build a complete example of all four below. First, two preliminaries:
what exactly the algorithm is _for_, and how we write it down.

## Specifying the problem

Before writing an algorithm we must agree on the **problem** it solves: the set
of legal inputs and, for each, the required output. A problem is a relation
between inputs and outputs; an _instance_ is one particular input. For sorting:

> **Input:** a sequence $\vector{a_1, a_2, \dots, a_n}$ of $n$ numbers.
> **Output:** a permutation $\vector{a'_1, a'_2, \dots, a'_n}$ of the input such
> that $a'_1 \le a'_2 \le \cdots \le a'_n$.

Notice what the specification _hides_: it says nothing about _how_ to reorder
the numbers, only _what_ the result must satisfy. Algorithm design rests on
that separation of **what** from **how**.

Our running example will be a smaller, more concrete problem:

> **Input:** an array $A[1..n]$ of numbers, with $n \ge 1$.
> **Output:** the maximum value $\max\set{A[1], \dots, A[n]}$.

It is simple enough that you can see the whole algorithm at once, yet rich
enough to demand all four deliverables, including a proof that is more subtle
than it first looks.

## Deliverable 1 — the high-level idea

Before any pseudocode, say what you intend to do in plain words. For
$\textsc{Find-Max}$:

> **Remark (High-level idea).** Keep track of the largest value $x$ seen so far.
> Sweep through the array left to right;
> whenever you meet an element bigger than $x$, update $x$ to it.
>
> When the sweep ends, $x$ is the maximum.

That sentence is the _whole_ algorithm. Everything that follows makes
it precise and proves it works.

## Deliverable 2 — the pseudocode

We describe algorithms in **pseudocode**: precise enough to analyze, free of the
syntactic noise of any real language. The high-level idea translates directly:

```algorithm
caption: $\textsc{Find-Max}(A)$ — return the largest element of $A[1..n]$
number: 1
$x \gets A[1]$ // largest value seen so far
for $i \gets 2$ to $n$ do
  if $A[i] > x$ then
    $x \gets A[i]$
return $x$
```

Two small but real design choices deserve attention. We seed $x$ with $A[1]$
rather than with $-\infty$ or $0$. This is why the specification insisted
$n \ge 1$, so that $A[1]$ exists and "the maximum" is well defined. The loop
starts at $i = 2$, since $A[1]$ has already been accounted for by the seed.

::impl{algo="find_max"}

As a second specimen of pseudocode, here is the classic insertion sort, which
sorts $A[1..n]$ in place by growing a sorted prefix one element at a time. We
will return to it when we study sorting; for now it shows what _nested_ loops
and an **in-place** rearrangement look like on the page.

```algorithm
caption: $\textsc{Insertion-Sort}(A)$ — sort $A[1..n]$ in increasing order
number: 2
for $j \gets 2$ to $n$ do
  $key \gets A[j]$
  $i \gets j - 1$ // insert into sorted prefix
  while $i > 0$ and $A[i] > key$ do
    $A[i + 1] \gets A[i]$
    $i \gets i - 1$
  $A[i + 1] \gets key$
return $A$
```

The outer loop walks a marker $j$ from left to right; everything _before_ $j$ is
already sorted. Each pass lifts $A[j]$ out as $key$, slides the larger
sorted-prefix elements one slot right, and drops $key$ into the gap that opens
up — exactly how you would tidy a hand of playing cards. The trace below shows
the sorted prefix (shaded) absorbing one new element per row.

$$
% caption: Insertion-Sort on $\langle 5,2,4,1\rangle$: each row is the array after one
%          pass of $j$; the shaded prefix is sorted, and the outlined cell is the $key$
%          just inserted.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=7mm, font=\small},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[lbl] at (-2.1,0) {start};
  \node[cell, fill=acc!15] (r0a) at (0,0) {5};
  \node[cell, right=0mm of r0a] (r0b) {2};
  \node[cell, right=0mm of r0b] (r0c) {4};
  \node[cell, right=0mm of r0c] (r0d) {1};
  \node[lbl] at (-2.1,-1.1) {$j=2$};
  \node[cell, fill=acc!15, very thick] (r1a) at (0,-1.1) {2};
  \node[cell, fill=acc!15, right=0mm of r1a] (r1b) {5};
  \node[cell, right=0mm of r1b] (r1c) {4};
  \node[cell, right=0mm of r1c] (r1d) {1};
  \node[lbl] at (-2.1,-2.2) {$j=3$};
  \node[cell, fill=acc!15] (r2a) at (0,-2.2) {2};
  \node[cell, fill=acc!15, very thick, right=0mm of r2a] (r2b) {4};
  \node[cell, fill=acc!15, right=0mm of r2b] (r2c) {5};
  \node[cell, right=0mm of r2c] (r2d) {1};
  \node[lbl] at (-2.1,-3.3) {$j=4$};
  \node[cell, fill=acc!15, very thick] (r3a) at (0,-3.3) {1};
  \node[cell, fill=acc!15, right=0mm of r3a] (r3b) {2};
  \node[cell, fill=acc!15, right=0mm of r3b] (r3c) {4};
  \node[cell, fill=acc!15, right=0mm of r3c] (r3d) {5};
  \node[lbl, right=4mm of r3d] {sorted};
\end{tikzpicture}
$$

## A picture of the idea

Here is $\textsc{Find-Max}$ mid-sweep on $A = \vector{3, 7, 2, 9, 5}$. The cursor
$i$ has just reached $A[4] = 9$; everything to its left has been scanned, and
$x$ holds the largest value among $A[1..3]$. Since $A[4] > x$, the **if** fires
and $x$ is updated to $9$.

$$
% caption: Find-Max mid-sweep over a five-cell array, updating $x$ at the cursor $i$.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=8mm, font=\small},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[cell] (a1) {3};
  \node[cell, right=0mm of a1] (a2) {7};
  \node[cell, right=0mm of a2] (a3) {2};
  \node[cell, right=0mm of a3, fill=acc!15, draw=acc, very thick] (a4) {9};
  \node[cell, right=0mm of a4] (a5) {5};
  \node[below=1pt of a1] {$1$};
  \node[below=1pt of a2] {$2$};
  \node[below=1pt of a3] {$3$};
  \node[below=1pt of a4] {$4$};
  \node[below=1pt of a5] {$5$};
  \draw[-{Stealth[]}, thick] ($(a4.north)+(0,7mm)$) -- ($(a4.north)+(0,2mm)$)
    node[above=6mm] {$i$};
  \draw[black] ($(a1.north west)+(0,1.5mm)$) -- ($(a1.north west)+(0,3mm)$)
    -- ($(a3.north east)+(0,3mm)$) -- ($(a3.north east)+(0,1.5mm)$);
  \node[font=\footnotesize, black, above] at ($(a2.north)+(0,3mm)$) {scanned: max is $x$};
  \node[draw, below=9mm of a2] (x) {$x = 7$};
  \draw[-{Stealth[]}, thick, red!75!black] (x.east) -- (a4.south west);
  \node[font=\footnotesize] at ($(a3.south)+(0,-17mm)$) {$A[i] > x$, so $x$ becomes~9};
\end{tikzpicture}
$$

The shaded cell is the element under the cursor; the region to its left
(positions $1$ through $i-1$) is the part already summarized by $x$.

::impl{algo="insertion_sort"}

## Deliverable 3 — proof of correctness

How do we _know_ $\textsc{Find-Max}$ works? Erickson's "a rock could run it"
intuition tells us the steps are mechanical, but it does **not** tell us the
answer is right. Correctness needs an _argument_.

It is tempting to argue by contradiction (_suppose $k$ is the true maximum but
$\textsc{Find-Max}$ returns something else_), but the clean way is to name what
the loop preserves and induct on it: **$x$ is only ever overwritten by a larger
value**, so $x$ never decreases and never holds anything that wasn't actually in
the array. Made precise, that is
a **loop invariant**: a statement true before and after every iteration.

> **Invariant.** At the start of the iteration with cursor $i$, the variable $x$
> equals $\max\set{A[1], \dots, A[i-1]}$.

We verify it with the three-part rubric that will recur throughout the course:

- **Initialization.** Before the first iteration $i = 2$, so we must check
  $x = \max\set{A[1]}$. The seed line set $x \gets A[1]$, and the maximum of a
  one-element set is that element. ✓
- **Maintenance.** Assume the invariant holds entering iteration $i$, i.e.
  $x = \max\set{A[1], \dots, A[i-1]}$. The body sets
  $x \gets \max\set{x, A[i]}$ (it overwrites $x$ exactly when $A[i] > x$, and
  leaves it otherwise). Hence after the body
  $x = \max\set{A[1], \dots, A[i-1], A[i]} = \max\set{A[1], \dots, A[i]}$, which
  is precisely the invariant for the next cursor value $i + 1$. ✓
- **Termination.** The loop ends once the cursor would exceed $n$, i.e. with the
  invariant established for $i - 1 = n$. So $x = \max\set{A[1], \dots, A[n]}$,
  and $\textsc{Find-Max}$ returns exactly the value the specification demands. ✓

Initialization, maintenance, termination: that triple drives correctness
proofs, and we will use it constantly.

> **Watch your indices.** A common slip is to muddle _which_ moment in time a
> claim about $i$ (or $x$) describes: the value _entering_ an iteration, or the
> value _after_ the update. State the invariant for one fixed moment (here, the
> _start_ of the iteration) and stick to it. Most "buggy proofs" of correct
> algorithms are really off-by-one confusions about state.

### The rubric on a harder loop: insertion sort

$\textsc{Find-Max}$'s invariant fit in one clause. Insertion sort (Algorithm 2)
needs two, and the second is the one beginners drop:

> **Invariant.** At the start of each iteration of the **for** loop (line 1),
> the prefix $A[1..j-1]$ consists of _exactly the elements originally in
> $A[1..j-1]$_, arranged in increasing order.

The phrase "exactly the elements originally in $A[1..j-1]$" is doing real work.
"The prefix is sorted" alone would not pin the algorithm down: a procedure
could make the prefix sorted by _destroying_ it (we will meet such a "sorter"
shortly), so the invariant must also record that elements are only ever
rearranged, never invented or lost. CLRS states the insertion-sort invariant in
exactly this two-clause form.[^clrs-inv]

Before the proof, look at what one pass actually does to the array. Lifting
$key$ out of its cell (line 2) leaves a hole; each pass of the **while** loop
(lines 4–6) slides one prefix element right into the hole, moving the hole one
step left; line 7 fills the final hole with $key$.

$$
% caption: Mid-pass snapshot of Insertion-Sort at $j = 5$, $key = 4$, on
%          $\langle 3,5,8,9,4,2 \rangle$. The while loop has slid $9$, then $8$, one slot
%          right, leaving the hole at position 3. Left of the hole the prefix is intact
%          and sorted; from the hole to position $j$, every element is $> key$; $A[6]$ has
%          not been looked at. The next test finds $A[2] = 5 > 4$, so the hole moves once
%          more before line 7 drops $key$ into it.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=7mm, font=\small},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[cell, fill=acc!15] (a1) at (0,0) {3};
  \node[cell, fill=acc!15, right=0mm of a1] (a2) {5};
  \node[cell, dashed, draw=black, right=0mm of a2] (a3) {};
  \node[cell, fill=acc!15, right=0mm of a3] (a4) {8};
  \node[cell, fill=acc!15, right=0mm of a4] (a5) {9};
  \node[cell, right=0mm of a5] (a6) {2};
  \draw[-{Stealth[]}, thick, acc] (a3.north) .. controls +(0,5mm) and +(0,5mm) .. (a4.north);
  \draw[-{Stealth[]}, thick, acc] (a4.north) .. controls +(0,5mm) and +(0,5mm) .. (a5.north);
  \node[lbl, acc] at ($(a4.north)+(0,8.5mm)$) {slid righ\/t};
  \draw[-{Stealth[]}, thick] ($(a2.north)+(0,6mm)$) -- ($(a2.north)+(0,1.5mm)$)
    node[above=5.5mm] {$i$};
  \draw[black] ($(a1.south west)+(0,-1.5mm)$) -- ($(a1.south west)+(0,-3mm)$)
    -- ($(a2.south east)+(0,-3mm)$) -- ($(a2.south east)+(0,-1.5mm)$);
  \node[lbl, black] at ($(a1.south east)+(0,-5mm)$) {still sorted};
  \draw[black] ($(a4.south west)+(0,-1.5mm)$) -- ($(a4.south west)+(0,-3mm)$)
    -- ($(a5.south east)+(0,-3mm)$) -- ($(a5.south east)+(0,-1.5mm)$);
  \node[lbl, black] at ($(a4.south east)+(0,-5mm)$) {eac\/h $>$ key};
  \node[lbl, black] at ($(a6.south)+(3mm,-5mm)$) {unseen};
  \node[draw] (k) at ($(a3.south)+(0,-13mm)$) {key = 4};
  \draw[-{Stealth[]}, thick, red!75!black] (k.north) -- (a3.south);
\end{tikzpicture}
$$

Now the three parts, argued against the line numbers of Algorithm 2.

- **Initialization.** Before the first iteration, $j = 2$, so the prefix is the
  single cell $A[1..1]$. Nothing has executed yet, so it still holds its
  original element, and a one-element array is trivially sorted. ✓
- **Maintenance.** Assume the invariant entering the iteration for some $j$:
  the prefix $A[1..j-1]$ is a sorted arrangement of the original first $j - 1$
  elements. Line 2 copies $A[j]$ into $key$, so we may treat cell $j$ as a
  hole. Each pass of the **while** loop (lines 4–6) fires only when
  $A[i] > key$; line 5 copies that element one slot right into the hole, and
  line 6 makes cell $i$ the new hole. Ignoring the hole, every shift leaves the
  prefix's elements intact and in the same relative order, so the region right
  of the hole (through cell $j$) stays sorted and consists entirely of elements
  $> key$. The loop exits in one of two ways: $i = 0$, so every prefix element
  was $> key$ and the hole is cell $1$; or $A[i] \le key$, so the hole sits
  just right of the rightmost element $\le key$. Either way, everything left of
  the hole is $\le key$ and sorted, everything right of it through cell $j$ is
  $> key$ and sorted, and line 7 drops $key$ into the hole. The result is
  $A[1..j]$ sorted, holding exactly the original elements of $A[1..j]$. That is
  the invariant with $j + 1$ in place of $j$. ✓
- **Termination.** The **for** loop exits when $j$ reaches $n + 1$. Plugging
  $j = n + 1$ into the invariant: $A[1..n]$ consists of exactly the elements
  originally in $A[1..n]$, in increasing order. That is word for word the
  sorting specification (a sorted _permutation_ of the input), and line 8
  returns it. ✓

The maintenance step above quietly ran a second induction: the claim about
holes and shifted elements is itself an invariant of the _inner_ **while**
loop, checked once per shift. For nested loops that layering is the normal
shape of a correctness proof — an outer invariant whose maintenance step leans
on an inner one. Here the inner argument is short enough to inline; when it is
not, state the inner invariant explicitly and give it the same three-part
treatment.

### Aside: soundness and completeness

For algorithms that answer _yes/no_ rather than compute a value, the same rigor
takes a slightly different shape. Consider $\textsc{Linear-Search}(A, k)$, which
reports whether key $k$ occurs in $A$. Its correctness has **two independent
halves**, and they carry standard names worth adopting now — they recur across the
whole course, in search, decision procedures, verifiers, and the reductions of
[intractability](/algorithms/intractability/p-np-reductions):

- **Soundness** — _every_ `found` _answer is true._ The procedure never lies in
  the affirmative: when it says `found`, genuinely $k \in A$. Soundness rules out
  **false positives**.
- **Completeness** — _every true case is caught._ The procedure never misses: when
  $k \in A$, it really does say `found`. Completeness rules out **false
  negatives**.

The two are genuinely separate. An algorithm that _always_ answered `not found`
would be vacuously **sound** — it never makes a false claim of membership — yet
hopelessly **incomplete**; one that always answered `found` would be complete but
unsound. Correctness requires both guarantees at once.

> **Claim (Completeness).** If $k \in A$, then $\textsc{Linear-Search}$ returns
> `found`.

> **Claim (Soundness).** If $\textsc{Linear-Search}$ returns `found`, then
> $k \in A$ — equivalently (contrapositive), if $k \notin A$ it returns `not found`.

> **Proof.** _Completeness_ is direct: if $k$ sits at position $j$, the loop's
> $j$-th iteration tests $A[j] = k$ and returns `found`. _Soundness_ is cleaner in
> its **contrapositive** form. The logical identity is worth memorizing:
> $(p \Rightarrow q) \;\equiv\; (\lnot q \Rightarrow \lnot p).$
>
> So instead of proving soundness as "if $k \notin A$ then it returns `not found`,"
> we prove the equivalent "if it returns `found` then $k \in A$," which is
> immediate: the only way to return `found` is to have just tested $A[j] = k$ for
> some $j$, witnessing $k \in A$. Choosing the easier of two logically identical
> statements is a recurring move in correctness proofs. $\qed$

$$
% caption: Proving soundness by contrapositive: the hard claim about the whole array (top)
%          is logically identical to an easy one about a single line of code (bottom).
\begin{tikzpicture}[
    box/.style={draw, minimum height=9mm, inner sep=3mm, font=\small, align=center},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[box] (p1) at (0,0) {$k$ not in $A$};
  \node[box, right=24mm of p1] (q1) {returns\\ \texttt{not found}};
  \draw[-{Stealth[]}, thick] (p1) -- (q1) node[midway, above, lbl, align=center, fill=white, inner sep=1.5pt] {hard to\\prove\\directly};
  \node[box, fill=acc!15] (q2) at (0,-2.1) {returns\\ \texttt{found}};
  \node[box, fill=acc!15, right=24mm of q2] (p2) {$k$ in $A$};
  \draw[-{Stealth[]}, thick, red!75!black] (q2) -- (p2) node[midway, above, lbl] {immediate};
  \draw[black, thick] (4.15,-0.87) -- (4.65,-0.87);
  \draw[black, thick] (4.15,-0.99) -- (4.65,-0.99);
  \draw[black, thick] (4.15,-1.11) -- (4.65,-1.11);
  \node[lbl, black, right] at (4.75,-0.99) {equivalent};
\end{tikzpicture}
$$

::impl{algo="linear_search"}

### Both tools at once: binary search

Invariants are not only about prefixes growing left to right. When the array is
_sorted_, we can search it by repeatedly halving a window, and the invariant
describes where the answer can still hide rather than what has been built so
far.

> **Input:** a sorted array $A[1..n]$ and a key $k$.
> **Output:** `found` if $k$ occurs in $A$, else `not found`.

```algorithm
caption: $\textsc{Binary-Search}(A, k)$ — search sorted $A[1..n]$ for $k$
number: 3
$lo \gets 1$
$hi \gets n$
while $lo \le hi$ do
  $mid \gets \floor{(lo + hi) / 2}$
  if $A[mid] = k$ then return found
  else if $A[mid] < k$ then $lo \gets mid + 1$ // discard left half
  else $hi \gets mid - 1$ // discard right half
return not found
```

> **Invariant.** At the start of each test of the **while** condition (line 3),
> if $k$ occurs anywhere in $A[1..n]$, then $k$ occurs in the window
> $A[lo..hi]$.

The invariant is deliberately _conditional_. It does not claim $k$ is in the
window — $k$ may not be in the array at all — only that the cells outside the
window have been legitimately ruled out.

- **Initialization.** Lines 1–2 set $lo = 1$ and $hi = n$, so the window is the
  whole array and the claim is vacuous: if $k$ is in $A[1..n]$, it is in
  $A[1..n]$. ✓
- **Maintenance.** Suppose the invariant holds entering an iteration and line 5
  does not return, so $A[mid] \ne k$. If $A[mid] < k$ (line 6), sortedness
  gives $A[1] \le \cdots \le A[mid] < k$, so no cell at index $\le mid$ can
  hold $k$. If $k$ is in the array at all, the invariant places it in
  $A[lo..hi]$, and we just excluded $A[lo..mid]$, so it lies in
  $A[mid+1..hi]$ — exactly the new window after $lo \gets mid + 1$. The case
  $A[mid] > k$ (line 7) is symmetric. ✓
- **Termination.** Two duties here, and the first is easy to forget: the loop
  must actually _end_, and the exit state must imply the postcondition. For
  progress: $lo \le hi$ inside the loop forces $lo \le mid \le hi$, so line 6
  raises $lo$ by at least one and line 7 lowers $hi$ by at least one; the
  window length $hi - lo + 1$ strictly shrinks every iteration and the loop
  runs at most $\ceil{\lg n} + 1$ times. For the exit itself there are two
  doors. Through line 5, the algorithm just witnessed $A[mid] = k$, so `found`
  is **sound**. Through line 3 failing, $lo > hi$ and the window is empty; the
  invariant says that if $k$ were in the array it would be in that empty
  window, which is absurd, so $k \notin A$ and `not found` is correct — the
  algorithm is **complete**. ✓

The same vocabulary as $\textsc{Linear-Search}$, but here completeness is not a
one-line observation: it rests entirely on the invariant. Every discarded cell
was ruled out for a reason, and the invariant records those reasons.

$$
% caption: Binary-Search for $k = 11$ in $A = \langle 2,3,5,7,11,13,17 \rangle$. Each row
%          is one probe: the shaded window is $A[lo..hi]$, the thick cell is $A[mid]$, and
%          grayed cells have been ruled out by the invariant. Probes: $A[4] = 7 < 11$,
%          then $A[6] = 13 > 11$, then $A[5] = 11$ — found.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=7mm, font=\small},
    dead/.style={draw=black, text=black},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[lbl, anchor=east] at (-0.6,0) {lo = 1, hi = 7};
  \node[cell, fill=acc!8] (r1a) at (0,0) {2};
  \node[cell, fill=acc!8, right=0mm of r1a] (r1b) {3};
  \node[cell, fill=acc!8, right=0mm of r1b] (r1c) {5};
  \node[cell, fill=acc!8, draw=acc, very thick, right=0mm of r1c] (r1d) {7};
  \node[cell, fill=acc!8, right=0mm of r1d] (r1e) {11};
  \node[cell, fill=acc!8, right=0mm of r1e] (r1f) {13};
  \node[cell, fill=acc!8, right=0mm of r1f] (r1g) {17};
  \node[lbl, anchor=west] at ($(r1g.east)+(2mm,0)$) {7 $<$~11: go righ\/t};
  \node[lbl, anchor=east] at (-0.6,-1.1) {lo = 5, hi = 7};
  \node[cell, dead] (r2a) at (0,-1.1) {2};
  \node[cell, dead, right=0mm of r2a] (r2b) {3};
  \node[cell, dead, right=0mm of r2b] (r2c) {5};
  \node[cell, dead, right=0mm of r2c] (r2d) {7};
  \node[cell, fill=acc!8, right=0mm of r2d] (r2e) {11};
  \node[cell, fill=acc!8, draw=acc, very thick, right=0mm of r2e] (r2f) {13};
  \node[cell, fill=acc!8, right=0mm of r2f] (r2g) {17};
  \node[lbl, anchor=west] at ($(r2g.east)+(2mm,0)$) {13 $>$ 11: go left};
  \node[lbl, anchor=east] at (-0.6,-2.2) {lo = 5, hi = 5};
  \node[cell, dead] (r3a) at (0,-2.2) {2};
  \node[cell, dead, right=0mm of r3a] (r3b) {3};
  \node[cell, dead, right=0mm of r3b] (r3c) {5};
  \node[cell, dead, right=0mm of r3c] (r3d) {7};
  \node[cell, fill=acc!15, draw=acc, very thick, right=0mm of r3d] (r3e) {11};
  \node[cell, dead, right=0mm of r3e] (r3f) {13};
  \node[cell, dead, right=0mm of r3f] (r3g) {17};
  \node[lbl, acc, anchor=west] at ($(r3g.east)+(2mm,0)$) {11 = 11: found};
\end{tikzpicture}
$$

### How invariant proofs go wrong

An invariant proof has exactly three joints, and each one has a
characteristic failure. All three failures look like proofs until you press on
the right spot.[^skiena-pitfalls]

**False at initialization.** The seed $x \gets A[1]$ in $\textsc{Find-Max}$
looks fussier than the "neutral" seed $x \gets 0$, and the neutral seed is a
genuine bug. With $x = 0$, the invariant $x = \max\set{A[1], \dots, A[i-1]}$ is
already false entering $i = 2$ whenever $A[1] \ne 0$; and on an all-negative
array the **if** never fires, so the algorithm returns $0$ — a value that is
not even in the array. The failed initialization check is not pedantry; it
points at a real input that breaks the program.

$$
% caption: A broken seed. Initializing $x \gets 0$ falsifies the invariant before the loop
%          even starts: on $A = \langle -3, -7, -2 \rangle$ no element beats $0$, the
%          **if** never fires, and Find-Max returns $0$, which does not occur in $A$. The
%          correct seed $x \gets A[1]$ makes initialization checkable — and true.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=8mm, font=\small},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[cell] (a1) at (0,0) {-3};
  \node[cell, right=0mm of a1] (a2) {-7};
  \node[cell, right=0mm of a2] (a3) {-2};
  \draw[black] ($(a1.north west)+(0,1.5mm)$) -- ($(a1.north west)+(0,3mm)$)
    -- ($(a3.north east)+(0,3mm)$) -- ($(a3.north east)+(0,1.5mm)$);
  \node[lbl, black, above] at ($(a2.north)+(0,3mm)$) {no element beats 0};
  \node[draw=red!75!black, below=7mm of a2] (x) {x = 0};
  \node[lbl, red!75!black, anchor=west] at ($(x.east)+(2.5mm,0)$) {returned, but not in the array};
\end{tikzpicture}
$$

**Too weak to imply the postcondition.** Take insertion sort and drop the
permutation clause, keeping only "$A[1..j-1]$ is sorted." Now consider this
impostor, which replaces lines 2–7 of Algorithm 2 with a single assignment:

```algorithm
caption: $\textsc{Copy-Left}(A)$ — a "sorter" with a perfect (weak) invariant
number: 4
for $j \gets 2$ to $n$ do
  $A[j] \gets A[j - 1]$
return $A$
```

The weak invariant sails through all three checks: a one-cell prefix is sorted
(initialization); appending a copy of the last element keeps a sorted prefix
sorted (maintenance); at $j = n + 1$ the whole array is sorted (termination).
Every step is airtight, and the program is garbage — on $\vector{5, 2, 4, 1}$
it "sorts" to $\vector{5, 5, 5, 5}$. Nothing in the proof was wrong; the
_invariant_ proved a true statement that fails to imply the specification,
which demanded a sorted **permutation** of the input. When the termination step
ends with anything short of the postcondition, word for word, the invariant
needs strengthening.

**Off-by-one at the exit.** The termination step must use the _exact negation_
of the loop guard, evaluated at the _actual_ exit value of the counter.
$\textsc{Find-Max}$'s loop ends with $i = n + 1$, not $i = n$; plugging the
wrong value into the invariant "proves" only $x = \max\set{A[1], \dots,
A[n-1]}$, which leaves $A[n]$ unaccounted for. The same slip in
$\textsc{Binary-Search}$ is a live bug rather than a weak conclusion: change
line 3 to **while** $lo < hi$ and, on a one-element array with $A[1] = k$, the
loop body never runs and line 8 answers `not found`. The invariant itself
survives untouched — what breaks is the exit analysis, because $lo < hi$
failing gives $lo \ge hi$, a window that may still hold one _unexamined_ cell,
and the "window is empty" step of the termination argument is simply false.

> **Takeaway.** Read the three checks as three different questions. Initialization:
> _is the invariant true before anything runs?_ Maintenance: _does one pass
> preserve it?_ Termination: _does the guard's negation, plus the invariant,
> spell out the postcondition?_ A proof that never states which question it is
> answering is usually answering none of them.

## Deliverable 4 — complexity, in brief

The fourth deliverable asks _how many steps_ the algorithm takes as a function of
the input size $n$. For $\textsc{Find-Max}$, the seed and the final return cost a
constant; the loop runs $n - 1$ times, doing a comparison and at most one
assignment each pass. If each line costs some machine-dependent constant
$c_1, c_2, \dots$, the total is

$$
c_1 + (n-1)(c_2 + c_3) + c_4 \;=\; O(n),
$$

a **linear** running time: double the array and you roughly double the work. The
point of the $O(\cdot)$ is that it throws away the machine-specific constants and
keeps only the growth rate.

That insertion sort, by contrast, is not always so cheap is why "fast"
needs care. On an array already in reverse order, every new element sifts past
_all_ its predecessors, costing $1 + 2 + \cdots + (n-1) = \floor{n(n-1)/2}$
comparisons, which is **quadratic** in $n$. On an already-sorted array it does
only $n - 1$ comparisons, which is linear: the same algorithm, wildly different
costs.

$$
% caption: Why the same Insertion-Sort costs so differently: a reverse-sorted input forces
%          every new element past its whole prefix, while a sorted input shifts nothing.
\begin{tikzpicture}[
    cell/.style={draw, minimum size=6.5mm, font=\small},
    lbl/.style={font=\footnotesize},
    every node/.style={font=\small}]
  \definecolor{acc}{HTML}{2348F2}
  \node[lbl, anchor=west] at (-3.7,0.7) {worst case (descending)};
  \node[cell, fill=acc!15] (w1) at (-3.7,0) {2};
  \node[cell, fill=acc!15, right=0mm of w1] (w2) {3};
  \node[cell, fill=acc!15, right=0mm of w2] (w3) {4};
  \node[cell, fill=acc!15, draw=acc, very thick, right=0mm of w3] (w4) {1};
  \draw[-{Stealth[]}, thick, red!75!black] (w4.south) .. controls +(0,-8mm) and +(0,-8mm) .. (w1.south)
    node[midway, below, lbl] {sifts past 3};
  \node[lbl, anchor=west] at (1.5,0.7) {best case (already sorted)};
  \node[cell, fill=acc!15] (b1) at (1.5,0) {1};
  \node[cell, fill=acc!15, right=0mm of b1] (b2) {2};
  \node[cell, fill=acc!15, right=0mm of b2] (b3) {3};
  \node[cell, fill=acc!15, draw=acc, very thick, right=0mm of b3] (b4) {4};
  \node[lbl, acc, below=8mm of b4] (stay) {stays put};
  \draw[-{Stealth[]}, thick, acc] (stay) -- (b4.south);
\end{tikzpicture}
$$

Defining $O$, $\Omega$, and $\Theta$ precisely, and measuring this growth
independently of the machine, is the subject of
[asymptotic analysis](/algorithms/foundations/asymptotic-analysis) in the next
lesson.

## Further frontiers

The four deliverables are a working discipline, but each has grown into a field
of its own. The "precise, mechanical procedure" we relied on informally has an
exact meaning: a function is _computable_ if some Turing machine computes it, and
the **Church–Turing thesis** holds that every reasonable model of computation —
Turing machines, the lambda calculus, the RAM of the next lesson — computes
exactly the same class of functions. Turing's 1936 construction also produced the
first problem that _no_ algorithm can solve, the **halting problem**: there is no
procedure that decides, for an arbitrary program and input, whether the program
eventually stops.[^turing] So "write an algorithm for it" is not always a request
that can be met, a boundary worth knowing before spending a week on a problem that
is provably undecidable.

The proof-of-correctness deliverable, done here by hand, can be machine-checked.
Interactive proof assistants such as Coq and Isabelle let one state an algorithm's
specification and its invariants formally and have the computer verify every step;
the **CompCert** C compiler and the **seL4** operating-system kernel are large
systems proved correct this way, insertion sort's loop invariant scaled up to
tens of thousands of lines.[^formal-verification] And the high-level-idea
deliverable is where the standard design paradigms live — divide-and-conquer,
greedy, dynamic programming, and the rest — each a reusable pattern for the "idea"
step, and each the subject of a later module. Skiena frames the whole design
manual around recognizing which paradigm a new problem fits.[^skiena-paradigms]

## Takeaways

- An algorithm is _a precise recipe of steps for solving a computational
  problem_: a finite, mechanical, input-to-output procedure that must be
  **correct on every instance**.
- Every algorithm comes with **four deliverables**: high-level idea, pseudocode,
  proof of correctness, and complexity analysis. $\textsc{Find-Max}$ shows all
  four at full size.
- Specify the **problem** (legal inputs → required outputs) before the
  **method**. That is also what tells you to seed $x \gets A[1]$ and require
  $n \ge 1$.
- Pseudocode is for humans to reason about; a **loop invariant** ("$x$ only ever
  grows, to a value actually in the array") turns "it looks right" into a proof
  by **initialization, maintenance, termination**. State _which_ moment your
  invariant describes.
- Invariants must be **strong enough to imply the postcondition**: insertion
  sort's invariant needs the permutation clause, not just "the prefix is
  sorted" — $\textsc{Copy-Left}$ satisfies the weak version while destroying
  the input.
- The termination step has two duties: show the loop **ends** (a quantity that
  strictly shrinks), then combine the invariant with the **exact negation of
  the guard** at the counter's real exit value. Off-by-ones live here.
- For yes/no algorithms, prove each direction separately, and use the
  **contrapositive** $(p \Rightarrow q) \equiv (\lnot q \Rightarrow \lnot p)$ to
  pick the easier statement. $\textsc{Binary-Search}$ needs both: `found` is
  witnessed directly; `not found` is forced by the invariant.
- Correctness and efficiency are separate questions: an algorithm can win one
  and lose the other.

[^erickson]: **Erickson**, _Algorithms_, Ch. 0 — Introduction: an algorithm as a procedure mechanical enough that "a rock could follow it."
[^clrs]: **CLRS**, Ch. 1 — The Role of Algorithms (§1.1): the operational "well-defined computational procedure" framing.
[^skiena]: **Skiena**, _The Algorithm Design Manual_, §1.1–1.3 — Introduction to Algorithm Design: an algorithm must be correct on _every_ instance.
[^clrs-inv]: **CLRS**, §2.1 — Insertion sort: the loop invariant is stated with both clauses, "the elements originally in $A[1..j-1]$" and "in sorted order."
[^skiena-pitfalls]: **Skiena**, §1.3 — Reasoning about Correctness: on how plausible-looking correctness arguments fail, and why counterexamples and induction are the tools that expose them.
[^turing]: Turing, A. M. (1936). "On computable numbers, with an application to the Entscheidungsproblem." _Proc. London Mathematical Society_ s2-42 — Turing machines, the Church–Turing thesis, and the undecidability of the halting problem.
[^formal-verification]: Leroy, X. (2009). "Formal verification of a realistic compiler." _Communications of the ACM_ 52(7) — the CompCert verified C compiler; Klein, G. et al. (2009). "seL4: formal verification of an OS kernel." _Proc. SOSP_.
[^skiena-paradigms]: **Skiena**, _The Algorithm Design Manual_, §1.1 and Part I — organizing algorithm design around a small set of reusable paradigms (divide-and-conquer, greedy, dynamic programming, and others).