The Laver tables provide examples of programs which have not been shown to terminate in the standard axiomatic system of mathematics ZFC but which do terminate when one assumes very large cardinal axioms.


The classical Laver tables An are the unique finite algebras with underlying set {1,...,2n} and an operation * that satisfies the identity x * (y * z)=(x * y) * (x * z) and where x*1=x+1 for x<2n and where 2n*1=1.

More information about the classical Laver tables can be found in the book Braids and Self-Distributivity by Patrick Dehornoy.


What is the shortest code (in bytes) that calculates 1*32 in the classical Laver tables and terminates precisely when it finds an n with 1*32<2n? In other words, the program terminates if and only if it finds an n with 1*32<2n but otherwise it runs forever.


A rank-into-rank cardinal (also called an I3-cardinal) is an extremely large level of infinity and if one assumes the existence of a rank-into-rank cardinal, then one is able to prove more theorems than if one does not assume the existence of a rank-into-rank cardinal. If there exists a rank-into-rank cardinal, then there is some classical Laver table An where 1*32<2n. However, there is no known proof that 1*32<2n in ZFC. Furthermore, it is known that the least n where 1*32<2n is greater than Ack(9,Ack(8,Ack(8,254)))(which is an extremely large number since the Ackermann function Ack is a fast growing function). Therefore, any such program will last for an extremely long amount of time.

I want to see how short of a program can be written so that we do not know if the program terminates using the standard axiomatic system ZFC but where we do know that the program eventually terminates in a much stronger axiomatic system, namely ZFC+I3. This question was inspired by Scott Aaronson's recent post in which Aaronson and Adam Yedidia have constructed a Turing machine with under 8000 states such that ZFC cannot prove that the Turing machine does not terminate but is known not to terminate when one assumes large cardinal hypotheses.

How the classical Laver tables are computed

When computing Laver tables it is usually convenient to use the fact that in the algebra An, we have 2n * x=x for all x in An.

The following code calculates the classical Laver table An

# table(n,x,y) returns x*y in An
if x=2^n then return y;
elif y=1 then return x+1;
else return table(n,table(n,x,y-1),x+1); fi; end;

For example, the input table(4,1,2) will return 12.

The code for table(n,x,y) is rather inefficient and it can only compute in the Laver table A4 in a reasonable amount of time. Fortunately, there are much faster algorithms for computing the classical Laver tables than the ones given above.

  • 2
    \$\begingroup\$ Welcome to PPCG! Great post! \$\endgroup\$ May 9, 2016 at 2:56
  • 1
    \$\begingroup\$ According to Wikipedia, Ack(9,Ack(8,Ack(8,254))) is a lower bound on n for which the period exceeds 16. For that, we can check 1*16 rather than 1*32. I will amend my program accordingly. \$\endgroup\$
    – John Tromp
    May 10, 2016 at 20:59
  • 1
    \$\begingroup\$ I've started writing up a Turing machine to do this, and I think I've spotted an out-by-factor-of-two error. Didn't Dougherty prove that Ack(9,Ack(8,Ack(8,254))) is a lower bound for the first table in which the first row has period 32, i.e. where 1*16 < 2^n? \$\endgroup\$ May 26, 2016 at 22:36
  • 1
    \$\begingroup\$ If you have a 20-state 2-symbol machine for Ackermann then please give me a link, because I can probably steal some ideas from it. I have 44 states to compute table(n,x,y), and I think it'll take between 25 and 30 states to set up the constants and the outer loop. The only direct TM representation I can find on esolangs.org is esolangs.org/wiki/ScripTur and it's not really that golfy. \$\endgroup\$ May 27, 2016 at 22:09
  • 1
    \$\begingroup\$ cheddarmonk.org/papers/laver.pdf is as much as I expect to get done this week, because I'm going to be travelling. \$\endgroup\$ May 31, 2016 at 21:51

4 Answers 4


Binary Lambda Calculus, 215 bits (27 bytes)

\io. let
  zero = \f\x. x;
  one = \x. x;
  two = \f\x. f (f x);
  sixteen = (\x. x x x) two;
  pred = \n\f\x. n (\g\h. h (g f)) (\h. x) (\x. x);
  laver = \mx.
    let laver = \b\a. a (\_. mx (b (laver (pred a))) zero) b
    in laver;
  sweet = sixteen;
  dblp1 = \n\f\x. n f (n f (f x)); -- map n to 2*n+1
  go2 = \mx. laver mx sweet mx (\_. mx) (go2 (dblp1 mx));
in go2 one

compiles to (using software at https://github.com/tromp/AIT)


This solution is mostly due to https://github.com/int-e

  • 2
    \$\begingroup\$ I'm not sure how you got your score but by default submissions should be scored according to the number of bytes in the code. I count 375 bytes for this submission. You should also include the language name and optionally a link to an interpreter for the language. \$\endgroup\$
    – Alex A.
    May 9, 2016 at 2:42
  • \$\begingroup\$ You should probably include the exact code of length 234 bits in your post. \$\endgroup\$ May 9, 2016 at 4:32
  • 2
    \$\begingroup\$ The encoding can be found on Wikipedia. There's also a link to this interpreter (not tested). These should be checked, though, and the binary encoding should also be in the post. \$\endgroup\$ May 9, 2016 at 5:46
  • 1
    \$\begingroup\$ For compiled languages, we score the code written by the user--not the number of bytes in the generated binary. \$\endgroup\$
    – Alex A.
    May 9, 2016 at 20:31
  • 8
    \$\begingroup\$ @AlexA. That's not necessary... any form of the code that can be understood by a compiler or interpreter is fine. \$\endgroup\$
    – feersum
    May 10, 2016 at 3:57

CJam (36 32 bytes)


In practice, this errors out quite quickly because it overflows the call stack, but on a theoretical unlimited machine it is correct, and I understand that to be the assumption of this question.

The code for table(n,x,y) is rather inefficient and it can only compute in the Laver table A4 in a reasonable amount of time.

is not actually correct if we cache computed values to avoid recomputing them. That's the approach I've taken, using the j (memoisation) operator. It tests A6 in milliseconds and overflows the stack testing A7 - and I've actually deoptimised table in the interests of golfing.


If we assume that n is understood from the context, instead of

f(x,y) =
    x==2^n ? y :
    y==1 ? x+1 :

we can remove the first special case, giving

f(x,y) =
    y==1 ? x+1 :

and it still works because

f(2^n, 1) = 2^n + 1 = 1

and for any other y,

f(2^n, y) = f(f(2^n, y-1), 1) = f(2^n, y-1) + 1

so by induction we get f(2^n, y) = y.

For CJam it turns out to be more convenient to reverse the order of the parameters. And rather than using the range 1 .. 2^n I'm using the range 0 .. 2^n - 1 by decrementing each value, so the recursive function I'm implementing is

g(y,x) =
    y==0 ? x+1
         : g(x+1, g(y-1, x))

1           e# Initial value of 2^n
{           e# do-while loop
  2*        e#   Double 2^n (i.e. increment n)
  31T       e#   table(n,1,32) is g(31,0) so push 31 0
  W$,(+a    e#   Set up a lookup table for g(0,x) = x+1 % 2^n
  {         e#   Memoisation function body: stack is 2^n ... y x
    0X$j    e#     Compute g(0,x) = x+1 % 2^n
            e#     Stack is 2^n ... y x (x+1%2^n)
    @(      e#     Bring y to top, decrement (guaranteed not to underflow)
            e#     Stack is 2^n ... x (x+1%2^n) (y-1%2^n)
    @jj     e#     Rotate and apply memoised function twice: g(x+1,g(y-1,x))
  2j        e#   Memoise two-parameter function
            e#   Stack: 2^n g(31,0)
  )W$=      e#   Test whether g(31,0)+1 is 2^n
}g          e# Loop while true

Pyth, 33 bytes

.N?qT^2NY?tY:N:NTtYhThT<:T1 32^2T

Try it online! (Obviously the testing part is not included here.)

  • \$\begingroup\$ What loop? Also, what does fi in the code mean? \$\endgroup\$
    – Leaky Nun
    May 10, 2016 at 2:57

Javascript, 53 bytes


Define g(x,y)=x*(y+1) on \$F_{2^n}\$, aka. \$2^n\$ is written as 0


This site is temporarily in read-only mode and not accepting new answers.

Not the answer you're looking for? Browse other questions tagged .