A function that grows faster than you can imagine, computed exactly and checked step by step.
ackermann.js · output · proof · check · try it in the playground
The question
Adding is repeated counting. Multiplying is repeated adding. Raising to a power is repeated multiplying. Keep going — repeated powers, then repeated that — and numbers explode.
The Ackermann function A(X, Y) climbs this ladder: X says which rung, Y how far to go. A(3, 4) is 125. A(4, 2) has 19,729 digits.
Can a computer get such numbers exactly right — and show how?
The ladder of operations
Mathematicians call the rungs hyperoperations. With base 2:
| Level | Operation | Example |
|---|---|---|
| 0 | successor (add one) | 7 + 1 |
| 1 | addition | 7 + 2 |
| 2 | multiplication | 7 × 2 |
| 3 | exponentiation (power) | 2⁷ = 128 |
| 4 | tetration (tower of powers) | 2^2^2^2 = 65,536 |
Each level above 3 is the level below, repeated. A(X, Y) shifts Y up by 3, applies level X with base 2, and subtracts 3 again.
What we tell eyecode
// A(X, Y): shift Y by 3, apply level X with base 2, and subtract 3 again.
implied_by(ackermann([X, Y], A), [is(B, add(Y, 3)), hyper(X, B, 2, C), is(A, sub(C, 3))])
// hyper(Level, Count, Base, Result)
implied_by(hyper(0, Y, _, A), is(A, add(Y, 1)))
implied_by(hyper(1, Y, Z, A), is(A, add(Y, Z)))
implied_by(hyper(2, Y, Z, A), is(A, mul(Y, Z)))
implied_by(hyper(3, Y, Z, A), is(A, pow(Z, Y)))
// Applied zero times, every level above 3 gives 1.
implied_by(hyper(X, 0, _, 1), gt(X, 3))
implied_by(
hyper(X, Y, Z, A),
[gt(X, 3), gt(Y, 0), is(B, sub(Y, 1)), hyper(X, B, Z, C), is(D, sub(X, 1)), hyper(D, C, Z, A)],
)
query(ackermann([3, 4], _))
// … ten more questions like this
The first four levels are plain arithmetic (is means “compute”; add,
mul and pow are addition, multiplication and power, and gt is
“greater than”). The last rule says: level X, Y times, is level X−1 applied to
level X, Y−1 times. Everything is a backward rule, worked out only when a
question asks for it.
What eyecode concludes
ackermann([0, 6], 7)
ackermann([2, 9], 21)
ackermann([3, 4], 125)
ackermann([3, 14], 131069)
ackermann([4, 1], 65533)
ackermann([4, 2], 2003529930406846464979072351560255750447825475569751419265016973710894…)
ackermann([5, 0], 65533)
7 of the 11 answers. The [4, 2] line goes on for 19,729 digits, ending
in …5587895905719156733. eyecode’s integers have no size limit, so nothing
is rounded.
Why: the proof in plain words
For A(3, 4) the proof says:
- 4 + 3 = 7 — a built-in calculation.
- 2⁷ = 128, so level 3 of 7 is 128 — rule 5.
- 128 − 3 = 125 — a built-in calculation.
- So A(3, 4) = 125 — rule 1, with X = 3, Y = 4.
A(4, 1) needs the repeating rule, rule 7: level 4 applied zero times is 1 (rule 6), then each application raises 2 to the previous result: 2, 4, 16, and finally 2¹⁶ = 65,536. The tower up to 16 was already proved for A(4, 0) = 13 and is reused: steps proved for one answer serve the next.
Checked, not just claimed
The checker read all 74 steps against the program:
- 33 steps matched exactly to the rule they cite;
- 41 calculations were recomputed by the checker itself and agreed — including the 19,729-digit power;
- no circular reasoning, and every step serves one of the 11 answers.
Verdict: checked. Nothing taken on trust.
Try it
eyecode examples/ackermann.js # the answers
eyecode --proof examples/ackermann.js # answers with their proof
Or open it in the playground.
Add query(ackermann([3, 5], _)) at the end and run again: a new answer
appears, ackermann([3, 5], 253).
Takeaway
Enormous numbers are no excuse for “trust me”. Every rung of the ladder is an ordinary rule, every sum and power is recomputed by an independent checker, and the answer is exact down to the last of its 19,729 digits.