<!-- Generated from https://www.teclamairme.com/#group-T9 by readviews.py; never edited by hand. -->

# Glossary cards — Chapter ᚇ(D): The locomotive

*Teclam Áirme, the Mathematical Compendium — a copy for AI readers of https://www.teclamairme.com/#group-T9, as of 2026-09-30. Links are relative to https://www.teclamairme.com/fortheaireaders/.*

[Guide for AI readers](index.md) · [The chapter](ch09.md)

*Computability, complexity, and numerical analysis: lambda calculus, the halting problem, Busy Beaver, P and NP, and a rounding error that vanishes. Each card: its symbol, type, one-line headline, the longer note, the reference entries it cites and the cards it links to.*

### the letter Dair — `ᚇ` {#g-og-dair}

*Ogham letter*

Ogham letter name meaning ‘oak’, the highest of the trees in its first kenning.

Dair means ‘oak’, from the Indo-European root *doru-, and is one of the five names the medieval tradition read without glossing. The three Old Irish word-oghams, the Bríatharogaim ascribed to Morann mac Moín, to Mac ind Óc, and to Cú Chulainn, give ardam dosae, “highest tree”; grés soír, “handicraft of a craftsman”; and slechtam soíre, “most carved of craftsmanship.” The Auraicept keeps the first: “higher than bushes is an oak.” Modern tree lore and ogham divination descend from the medieval plant glosses by way of Robert Graves’s The White Goddess of 1948, which read the letter order as an ancient seasonal calendar of tree magic. Celtic scholarship rejects that reconstruction; the associations in circulation today are modern, not ancient.

Cites: [2.15](ch02-refs.md#r-2.15), [2.16](ch02-refs.md#r-2.16), [2.17](ch02-refs.md#r-2.17), [2.19](ch02-refs.md#r-2.19)

### Church zero, decoded — `(λf.λx.x) S 0` {#g-church}

*Integer or rational*

The Church numeral for zero applies a function zero times, so applied to the successor and 0 it returns the number 0 itself: two beta reductions and a computation lands on zero.

Alonzo Church introduced the lambda calculus in 1932 and the Church numerals soon after, encoding the number n as a function that applies its argument n times: 0 is λf.λx.x, 1 is λf.λx.f x, and so on; Stephen Kleene later found how to λ-define the predecessor function. Decoding is standard: feed the numeral the successor function S and the ordinary number 0, and beta reduction hands back the ordinary number n. For zero that is two reductions, (λf.λx.x) S 0 → (λx.x) 0 → 0. The bare numeral is only an encoding; the decoding is a computation that halts holding the integer 0, hence the integer tag.

Cites: [9.1](ch09-refs.md#r-9.1), [9.19](ch09-refs.md#r-9.19)

See also: [the lambda calculus](ch09-cards.md#g-lambdacalc)

### the halting problem, as a bit — `[∃ a halting decider]` {#g-halting}

*Integer or rational*

Turing proved in 1936 that no program can decide, for every program, whether it halts, so the bracket is 0.

Alan Turing proved in his 1936 paper On Computable Numbers that no Turing machine can decide, for every machine and input, whether that machine halts; the proof builds a machine that consults the supposed decider about itself and does the opposite. The bracket contains the false statement that such a decider exists, so it is 0. Earlier in 1936, before Turing’s paper was received on 28 May, Church had published a proof, in the language of functions rather than machines, that no procedure decides the Entscheidungsproblem; Turing’s appendix shows that the two describe the same class. The bracket is an integer because a truth value is one.

Cites: [9.19](ch09-refs.md#r-9.19), [9.2](ch09-refs.md#r-9.2), [9.3](ch09-refs.md#r-9.3)

See also: [the Entscheidungsproblem](ch09-cards.md#g-entscheidung), [Turing machine](ch09-cards.md#g-turingm)

### the fifth Busy Beaver number — `BB(5)` {#g-bb5}

*Integer or rational*

47,176,870, proven in 2024 after decades of search; the largest Busy Beaver value actually known.

Tibor Radó defined the Busy Beaver function in 1962: BB(n) is the maximum number of steps an n-state, two-symbol Turing machine started on a blank tape can run before halting. BB(1) = 1, BB(2) = 6, BB(3) = 21, BB(4) = 107. The five-state champion running 47,176,870 steps was found by Heiner Marxen and Jürgen Buntrock in 1989, and it was proved to be the true BB(5) by the Busy Beaver Challenge collaboration on 2 July 2024, with a proof checked in the Coq (now Rocq) proof assistant. The function is uncomputable as a whole, because knowing it would decide the halting problem, but each known value is a plain integer, hence the tag.

Cites: [9.20](ch09-refs.md#r-9.20), [9.5](ch09-refs.md#r-9.5), [9.6](ch09-refs.md#r-9.6), [9.7](ch09-refs.md#r-9.7), [9.8](ch09-refs.md#r-9.8)

See also: [the Busy Beaver function](ch09-cards.md#g-busybeaver), [Rice’s theorem](ch09-cards.md#g-rice), [Turing machine](ch09-cards.md#g-turingm), [uncomputable](ch05-cards.md#g-uncomputable)

### Ackermann’s function at three and three — `A(3, 3)` {#g-ack}

*Integer or rational*

61, from the function that grows faster than any primitive recursion.

Wilhelm Ackermann published his function in 1928 as an example of something computable that is not primitive recursive, that is, not reachable by loops whose lengths are fixed in advance. In the common Péter form A(0, n) = n + 1, A(m, 0) = A(m − 1, 1), A(m, n) = A(m − 1, A(m, n − 1)), and A(3, 3) = 61; A(4, 2) has 19,729 digits and A(4, 3) cannot be written out in full. A(3, 3) is an ordinary integer, hence the tag.

Cites: [9.10](ch09-refs.md#r-9.10), [9.9](ch09-refs.md#r-9.9)

### the four smaller Busy Beaver numbers — `BB(1) + BB(2) + BB(3) + BB(4)` {#g-bbsmall}

*Integer or rational*

1 + 6 + 21 + 107 = 135: every Busy Beaver value below BB(5), each a plain count of steps.

BB(1) = 1 and BB(2) = 6 were settled in the early 1960s, BB(3) = 21 was proved by Lin and Radó in 1965, and BB(4) = 107 by Brady in 1983. Each is the longest a halting two-symbol Turing machine with that many states can run on a blank tape, and each is an ordinary integer once proved, which is why they sit in the denominator beside BB(5) while BB(6), still unknown, sits in Chapter ᚃ(F). Sum 135.

Cites: [9.19](ch09-refs.md#r-9.19), [9.5](ch09-refs.md#r-9.5), [9.6](ch09-refs.md#r-9.6)

See also: [the fifth Busy Beaver number](ch09-cards.md#g-bb5), [sixth Busy Beaver number](ch05-cards.md#g-bb6), [Turing machine](ch09-cards.md#g-turingm)

### the lambda calculus — `λx.M` {#g-lambdacalc}

*Function or operator*

Church’s 1932 model of computation: every term is a variable, a function λx.M, or one term applied to another, and its rule of computation is beta-reduction; it computes exactly what a Turing machine computes.

Alonzo Church introduced the lambda calculus in A set of postulates for the foundation of logic, published in 1932; it is a formal system built from abstraction and application, and beta-reduction, which applies a function to an argument, is its rule of computation. Numbers are encoded rather than built in: the Church numeral for n is a function that applies its argument n times, so zero is λf.λx.x, and Stephen Kleene found a λ-definition of the predecessor function. Untyped lambda calculus can simulate any Turing machine and a Turing machine can simulate it, which is why the three answers of the 1930s are one answer.

Cites: [9.1](ch09-refs.md#r-9.1), [9.3](ch09-refs.md#r-9.3)

See also: [the combinators](ch09-cards.md#g-ski), [Turing machine](ch09-cards.md#g-turingm)

### general recursion — `general recursive` {#g-genrec}

*Function or operator*

Herbrand and Gödel’s class of general recursive functions, set out in Gödel’s 1934 Princeton lectures on a suggestion of Jacques Herbrand; one of the decade’s three definitions of computable, and the same class as the other two.

Kurt Gödel, with Jacques Herbrand, formalized the definition of the class of general recursive functions, modifying his approach on Herbrand’s suggestion, and set the class out in his 1934 Princeton lectures. Church’s lambda-definable functions, these general recursive functions, and Turing’s machine-computable functions are extensionally the same class, which is what makes the Church–Turing thesis one thesis rather than three. The equivalence is a theorem about the three formal models; the further claim that this class is everything effectively calculable is not, because effective calculability has no agreed formal definition.

Cites: [9.3](ch09-refs.md#r-9.3)

See also: [the Church–Turing thesis](ch09-cards.md#g-churchturing)

### the Entscheidungsproblem — `Entscheidungsproblem` {#g-entscheidung}

*Function or operator*

Hilbert and Ackermann’s decision problem of 1928: is there an algorithm that says whether a given statement is valid in every structure? Church and Turing each showed in 1936 that there is none.

David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem in 1928: it asks for an algorithm that takes a statement and answers yes or no according to whether that statement is universally valid, meaning valid in every structure. In 1936 Alonzo Church and Alan Turing published independent papers showing that no general solution exists. Church’s was in print first; Turing’s was received on 28 May and printed on 30 November and 23 December, with an appendix showing that the lambda-definable and the machine-computable functions are the same class. Turing’s route to the answer, a machine that cannot decide whether another machine halts, is the one this chapter’s bracket records.

Cites: [9.21](ch09-refs.md#r-9.21), [9.3](ch09-refs.md#r-9.3)

See also: [the Answer](ch04-cards.md#g-fortytwo)

### the Busy Beaver function — `BB(n)` {#g-busybeaver}

*Function or operator*

Radó’s 1962 function: the most steps a halting n-state, two-symbol Turing machine can make from a blank tape. It eventually dominates every computable function, and no algorithm computes it.

Tibor Radó introduced the busy beaver game in 1962; in the step-count convention used throughout this book, BB(n) is the maximum number of steps a halting n-state, two-symbol Turing machine makes when started on the all-zero tape. The function is uncomputable and eventually dominates every computable function, because an exact computation of its values would decide halting for machines of bounded size. Individual values are ordinary integers once proved: BB(1) = 1, BB(2) = 6, BB(3) = 21 by Lin and Radó in 1965, and BB(4) = 107 by Brady in 1983; BB(5) = 47,176,870, whose champion machine Marxen and Buntrock found in 1989, was proved in 2024. BB(6) is still unknown, and sits in Chapter ᚃ(F). Uncomputability is a property of the function, not of any one of its values.

Cites: [9.5](ch09-refs.md#r-9.5), [9.6](ch09-refs.md#r-9.6), [9.7](ch09-refs.md#r-9.7), [9.8](ch09-refs.md#r-9.8)

See also: [the fifth Busy Beaver number](ch09-cards.md#g-bb5), [sixth Busy Beaver number](ch05-cards.md#g-bb6), [Turing machine](ch09-cards.md#g-turingm), [uncomputable](ch05-cards.md#g-uncomputable)

### Ackermann’s function — `A(m, n)` {#g-ackfn}

*Function or operator*

A recursive function, published by Wilhelm Ackermann in 1928 and now usually given in two-argument form, that is total and computable yet grows faster than any primitive recursive function.

In the common Péter form, A(0, n) = n + 1, A(m, 0) = A(m − 1, 1), and A(m, n) = A(m − 1, A(m, n − 1)). The function is total and computable, but it is not primitive recursive: no loop whose bound is fixed in advance can compute it, because it grows faster than any primitive recursive function. Ackermann published it in 1928 to separate the computable functions from the primitive recursive ones; A(3, 3) = 61 is the one value with a card of its own, and A(4, 2) already runs to 19,729 decimal digits.

Cites: [9.25](ch09-refs.md#r-9.25)

See also: [Ackermann’s function at three and three](ch09-cards.md#g-ack)

### the settled direction of P versus NP — `[P ⊆ NP]` {#g-pnpsub}

*Integer or rational*

Every problem that can be solved quickly can be checked quickly, so this bracket is 1; the other direction is the epilogue’s million-dollar bit.

P is the class of decision problems a deterministic machine solves in polynomial time, NP the class whose yes-answers a machine can verify in polynomial time given a certificate; the polynomial-time formulation is Cobham’s and Edmonds’, both from 1965. P ⊆ NP is immediate, since a solver is a verifier that ignores its certificate, so the bracket is 1. Whether NP ⊆ P is the P versus NP problem, whose bracket [P = NP] closes the book in the epilogue and can never sit in a denominator. Cook (1971) and Levin (1973) proved that satisfiability is NP-complete, and Karp gave a list of 21 NP-complete problems in 1972. A known truth value, hence the integer tag.

Cites: [9.11](ch09-refs.md#r-9.11), [9.12](ch09-refs.md#r-9.12)

See also: [the hardest problems in NP](ch28-cards.md#g-npcomplete), [the P versus NP question, as a bit](ch28-cards.md#g-pnp)

### a binary64 rounding zero — `fl_{64}(1+2^{−53})−1` {#g-float64zero}

*Integer or rational*

Exactly 0 under IEEE binary64 round-to-nearest, ties-to-even: the positive increment, half the gap between 1 and the next representable number, rounds away.

IEEE binary64 has 53 bits of significand precision. The next representable value above 1 is 1 + 2^{−52}, so 1 + 2^{−53} is exactly halfway. Under round-to-nearest, ties-to-even, the tie resolves to 1 because its final significand bit is even; subtracting 1 gives exactly 0. The rule and format are those standardized by IEEE 754. This is machine arithmetic, not an identity of the real numbers.

Cites: [9.13](ch09-refs.md#r-9.13), [9.14](ch09-refs.md#r-9.14)

See also: [IEEE 754](ch09-cards.md#g-ieee754), [the real numbers](ch01-cards.md#g-reals)

### machine epsilon of binary64 — `2^{−52}` {#g-eps64}

*Integer or rational*

About 2.2 × 10⁻¹⁶: the gap between 1 and the next double-precision number, the resolution of the double, one of the two most common floating-point formats in use.

IEEE binary64, the double type on most systems since the 1985 standard, carries 53 bits of significand precision, so the numbers just above 1 are spaced 2^{−52} ≈ 2.220446 × 10^{−16} apart. Half of that gap is the largest relative rounding error a single operation can make, and the numerator’s zero sits exactly on it. A rational number. (That 0.1 + 0.2 ≠ 0.3 on a computer has a different cause: 0.1 and 0.2 have no finite binary expansion, so they are stored rounded.)

Cites: [9.13](ch09-refs.md#r-9.13), [9.22](ch09-refs.md#r-9.22)

See also: [IEEE 754](ch09-cards.md#g-ieee754)

### Kolmogorov complexity — `K(x)` {#g-kolmogorov}

*Function or operator*

The length of the shortest program that prints x: Solomonoff 1960, Kolmogorov 1965, Chaitin 1966; not computable, by an argument modeled on Berry’s paradox.

The Kolmogorov complexity K(x) of a string is the length of the shortest program, in a fixed language, that outputs it; a string is random when no program is shorter than the string itself. Ray Solomonoff introduced the idea in 1960, Andrey Kolmogorov published it independently in 1965 and acknowledged Solomonoff’s priority when he learned of his work, and Gregory Chaitin’s paper followed in 1966. K is provably uncomputable, by a version of Berry’s paradox, and Chaitin’s Ω beside it is the halting probability of the same machine. A function, so a tool of the framework rather than a value.

Cites: [9.15](ch09-refs.md#r-9.15)

See also: [Berry’s paradox](ch01-cards.md#g-berry), [Chaitin’s constant](ch05-cards.md#g-omega), [uncomputable](ch05-cards.md#g-uncomputable)

### Turing machine — `TM` {#g-turingm}

*Function or operator*

Turing’s 1936 model of computation: a finite control, a tape, and a head that reads, writes, and moves; the Church–Turing thesis says everything computable is computable by one.

Alan Turing defined his machines in On Computable Numbers (1936): a finite set of states, an unbounded tape of cells, and a table saying, for each state and symbol, what to write, which way to move, and which state to enter. A universal machine can simulate any other from a description on its tape, which is the idea of the stored-program computer. Busy Beaver counts the steps of the most stubborn halting n-state machine; the halting bracket says no machine can predict them all. A model, hence the tool tag.

Cites: [9.3](ch09-refs.md#r-9.3), [9.4](ch09-refs.md#r-9.4)

See also: [the Church–Turing thesis](ch09-cards.md#g-churchturing)

### the Church–Turing thesis — `Church–Turing thesis` {#g-churchturing}

*Function or operator*

Every function a human could compute by a fixed procedure is computable by a Turing machine, equivalently by lambda calculus; a thesis, not a theorem, and never contradicted.

In 1936 Church’s lambda-definable functions, Herbrand and Gödel’s general recursive functions and Turing’s machine-computable functions were all shown to be the same class, and Church and Turing each proposed that this class is what computable means. The thesis cannot be proved, because effective procedure is an informal notion, and rigorous later models, including quantum Turing machines, have proved equivalent to it; only the theoretical models called hypercomputers go beyond it. It is the reason the halting bracket is a statement about all programs and not only Turing’s. A principle, hence the tool tag.

Cites: [9.3](ch09-refs.md#r-9.3)

See also: [general recursion](ch09-cards.md#g-genrec), [the lambda calculus](ch09-cards.md#g-lambdacalc), [Turing machine](ch09-cards.md#g-turingm)

### big-O notation — `O(n log n)` {#g-bigO}

*Function or operator*

How fast a cost grows with the size of the input, ignoring constants: the language complexity classes are written in.

Paul Bachmann proposed the notation in 1894 and Edmund Landau extended it in 1909; Knuth fixed Ω and Θ for the family in 1976. f = O(g) means f is eventually bounded by a constant times g. Sorting by comparisons costs Θ(n log n), multiplying two n-digit numbers costs O(n log n) by Harvey and van der Hoeven, announced in 2019 and published in 2021, and P is the class of problems solvable in O(n^k) for some k. Notation, hence the tool tag.

Cites: [9.11](ch09-refs.md#r-9.11)

### Rice’s theorem — `Rice’s theorem` {#g-rice}

*Function or operator*

Every non-trivial question about what a program computes is undecidable; the halting problem is only the first example.

Henry Gordon Rice proved in 1951 (published 1953) that for any property of the function a program computes, other than the trivial always-true and always-false ones, no algorithm can decide whether an arbitrary program has it. Does this program ever print 0, does it compute a total function, is it equivalent to that program: all undecidable. It turns the single halting bracket of the numerator into a whole class of zeros. A theorem, hence the tool tag.

Cites: [9.16](ch09-refs.md#r-9.16)

See also: [the halting problem, as a bit](ch09-cards.md#g-halting)

### the combinators — `S, K, I, Y` {#g-ski}

*Function or operator*

S, K, and I are the three building blocks from which every lambda term can be assembled; Y is the fixed-point combinator that gives recursion.

Moses Schönfinkel introduced combinatory logic in 1920, in a talk published in 1924, with S = λxyz.xz(yz) and K = λxy.x, from which I = SKK, and Haskell Curry rediscovered the combinators in 1927 and developed them in his 1930 thesis; every closed lambda term can be written with S and K alone. Curry’s fixed-point combinator Y = λf.(λx.f(xx))(λx.f(xx)) satisfies Y f = f(Y f), which is how a calculus with no loops or names still computes every recursive function, including the Church numerals’ arithmetic. Tools, hence the tag.

Cites: [9.17](ch09-refs.md#r-9.17)

### Gödel numbering — `⌜φ⌝` {#g-godelnum}

*Function or operator*

Encode every formula and proof as a natural number, so that arithmetic can talk about itself; the trick behind incompleteness and the universal machine.

Gödel’s 1931 proof assigns to each symbol, formula, and proof a natural number, using prime factorization so that the code can be decoded; the statement “this statement is unprovable” then becomes a statement about numbers. Turing’s universal machine of 1936 does the same for programs. The corner brackets ⌜φ⌝ are the standard notation for the number of the formula φ. A coding, hence the tool tag.

Cites: [9.18](ch09-refs.md#r-9.18), [9.24](ch09-refs.md#r-9.24), [9.4](ch09-refs.md#r-9.4)

### IEEE 754 — `binary64` {#g-ieee754}

*Function or operator*

The floating-point standard almost all modern computers follow, first published in 1985: its binary64 format keeps 53 bits of significand precision, and its default rounding is to the nearest representable number, ties to even.

The first IEEE standard for floating-point arithmetic, IEEE 754-1985, was published in 1985, and round to nearest, ties to even is its default rounding for binary formats. The binary64 format, the double type on most systems, carries 53 bits of significand precision with 52 of them explicitly stored, so the numbers just above 1 are spaced 2^{−52} ≈ 2.220446 × 10^{−16} apart. The tie rule is what makes this chapter’s numerator 0: 1 + 2^{−53} is exactly halfway to the next double, and of its two neighbors the one whose last significand bit is even is 1 itself. A decision made by a committee, not a theorem of arithmetic.

Cites: [9.13](ch09-refs.md#r-9.13), [9.14](ch09-refs.md#r-9.14), [9.22](ch09-refs.md#r-9.22)