eyedia

Ackermann

A function that grows faster than you can imagine, computed exactly and checked step by step.

ackermann.pl · 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
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.

What we tell Eyedia

ackermann([X, Y], A) :- B is Y+3, hyper(X, B, 2, C), A is C-3.

hyper(0, Y, _, A) :- A is Y+1.
hyper(1, Y, Z, A) :- A is Y+Z.
hyper(2, Y, Z, A) :- A is Y*Z.
hyper(3, Y, Z, A) :- A is Z^Y.
hyper(X, 0, _, 1) :- X > 3.
hyper(X, Y, Z, A) :- X > 3, Y > 0, B is Y-1, hyper(X, B, Z, C), D is X-1, hyper(D, C, Z, A).

true :+ ackermann([3, 4], _).
% … ten more questions like this

The first four levels are plain arithmetic (is means “compute”). The last line says: level X, Y times, is level X−1 applied to level X, Y−1 times.

What Eyedia 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. Eyedia’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: the tower 2^2^2 is 16, and 2¹⁶ is 65,536 — rule 7, twice over. Steps already proved for one answer are reused by 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

node bin/eyedia.js examples/ackermann.pl            # the answers
node bin/eyedia.js --proof examples/ackermann.pl    # with their proof

Or open it in the playground.

Add true :+ 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.

This site is open source. Improve this page.