Matpic
mathematics, in pictures
Concept

Termination

The property of a procedure guaranteed to stop, usually because some whole-number quantity strictly decreases at every step. Proving it usually means exhibiting the decreasing quantity, which is the same move as an argument by descent.

Named by 12 essays across 6 fields — each of them below, with the objects they name alongside it.

Euclid's algorithm on a 34 by 13 rectangle. The rectangle is tiled by peeling off the largest square that fits, again and again, until nothing is left.

The oldest algorithm, drawn as a tiling

Euclid's method for finding a greatest common divisor is usually presented as a loop. It is also a way of tiling a rectangle with squares, and the tiling explains why it works.

geometry · Euclidean algorithm φ as a continued fraction. The nested fraction, one quotient per step, descending to the right.

A fraction that never closes

Euclid's algorithm throws away everything except the number of squares it peeled at each step. Those counts are a second name for the number it started from — one that terminates exactly when the ratio is a ratio.

number · Euclidean algorithm The Collatz orbit of 27. Halve an even number, triple an odd one and add one; the sequence plotted on a logarithmic scale.

The question nobody can answer

Halve it if it is even, triple it and add one if it is odd. Every number anyone has tried comes down to one. Nobody can prove they all do, and the reason is not that the problem is hard to state.

dynamics · Collatz The Goodstein sequence from 4, with the ordinal beside each term. A table of the Goodstein sequence with each term's hereditary representation and the ordinal obtained by replacing the base with omega.

A sequence that explodes and still stops

Goodstein's sequence starting at 4 climbs past any number you care to name and reaches zero after about ten to the hundred and twenty million steps. The proof that it stops is a second sequence, running alongside it, that goes down.

logic · Ordinals The fast-growing hierarchy at its first few ordinals. A table of the fast-growing hierarchy: one row per ordinal index, one column per argument, with the cells too large to evaluate marked as such.

An ordinal as a growth rate

Index a family of functions by the ordinals, each one iterating the last, and the index becomes a measure of how fast a function grows. The point where the index leaves what arithmetic can prove is exactly where the Goodstein sequence became unprovable.

logic · Ordinals A landscape nobody is looking at, and every move goes downhill on it. The 8 states of a congestion game with 3 participants and two resources, ordered by Rosenthal's potential, with every improving unilateral move drawn as an arrow. Every arrow points downward.

The landscape nobody is looking at

Letting participants move one at a time to whatever is currently better can cycle forever, and on a network of congestible roads it cannot. The reason is a single number attached to each state that falls by exactly what the mover saves.

applied · Equilibrium Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

The instance that has to be guessed

Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

logic · Proof systems 6 vertices folded to 4, and a graph that decides. The graph built from 3 generator words, folded until no vertex has two edges of one label leaving it. Reading a word from the base vertex decides membership, and 6 words are tested.

Folding a graph until it decides

A subgroup of a free group usually arrives as a list of words, and almost nothing about it is readable from the list. Draw the words as loops, merge every pair of edges with the same label leaving one point, and what is left is a machine that decides membership by reading.

topology · Covering spaces An area of starting points from which z³ − 2z + 2 is never solved. The complex plane coloured by which root of z³ − 2z + 2 Newton's method reaches from each starting point, with the points that reach no root left uncoloured.

An area that never finishes

Newton's method's famous failure is a boundary, and a boundary has no area — a random start misses it with probability one. The real failure is different in kind: a polynomial with small whole-number coefficients whose method has a region of starting points, with area, from which it provably never terminates.

dynamics · Newton basins Four proofs about numbers, and what they compute. λn f x. n (λy. f y) (f x) computes n + 1; λn f x. n (λy. f (f y)) x computes 2n; λn f x. n (λy. n (λz. f z) y) x computes n²; λn f x. n (λy. x) (f x) computes 1 at 0, else 0.

What a proof about numbers can compute

The proofs of (o → o) → o → o without detours are the whole numbers, one for each count of how often the assumption is used. A proof of the implication from that formula to itself therefore takes a number and returns one, and removing its detours computes the answer. Enumerating all 14,659 such proofs up to size 16 finds 299 different functions — sums, products, squares, cubes, tests on zero — and not one of them subtracts. The predecessor, n − 1, is not among them, and a single line about polynomials says it never will be.

logic · Proof systems Raising the input's type, and what becomes computable. N[o]: 299 functions, 0 not extended polynomials; N[o → o]: 163 functions, 42 not extended polynomials; N[(o → o) → o]: 128 functions, 46 not extended polynomials; N[o → o → o]: 72 functions, 33 not extended polynomials.

One type up

A numeral is an iterator, and the formula it proves fixes what it may iterate. At the lowest type it can only repeat the successor, and every function it computes is a polynomial — no predecessor. Let the same numeral iterate a function on functions and 2ⁿ appears; let it iterate a function that takes a function and returns a value, and the predecessor appears at size 15; let it iterate a pair of values, and the predecessor, halving and parity all arrive at size 16. The trick is Kleene's, from 1932, and an exhaustive search finds it without being told.

logic · Proof systems Ackermann's function as one polymorphic term. A : N → N → N; A(0,0)=1 in 6 steps, A(0,1)=2 in 6 steps, A(0,2)=3 in 6 steps, A(0,3)=4 in 6 steps, A(0,4)=5 in 6 steps, A(0,5)=6 in 6 steps, A(1,0)=2 in 10 steps, A(1,1)=3 in 13 steps, A(1,2)=4 in 16 steps, A(1,3)=5 in 19 steps, A(1,4)=6 in 22 steps, A(1,5)=7 in 25 steps, A(2,0)=3 in 17 steps, A(2,1)=5 in 33 steps, A(2,2)=7 in 55 steps, A(2,3)=9 in 83 steps, A(2,4)=11 in 117 steps, A(2,5)=13 in 157 steps, A(3,0)=5 in 37 steps, A(3,1)=13 in 191 steps, A(3,2)=29 in 881 steps, A(3,3)=61 in 3795 steps, A(3,4)=125 in 15765 steps.

One type for every use

In the simply typed calculus a numeral must be told in advance what kind of thing it will iterate, and with input and output of one type it computes only polynomials with tests. Let a single type stand for every type — a numeral is then a term of type ∀X. (X → X) → X → X, used at whatever type each occasion needs — and the same few symbols compute subtraction, exponentials and Ackermann's function, which grows faster than anything built from primitive recursion. Every run still finishes, and the proof that it does lies just beyond the reach of second-order arithmetic.

logic · Proof systems

Named alongside it

The objects these essays reach for when they reach for this one.

Proof systemComputationIterationNormal formRecursionContinued fractionsDecision procedureFibonacciGreatest common divisorGraphIncommensurabilityIndependence

All concepts