Laver table computations and an algorithm that is not known to terminate in ZFC

Question

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.

Introduction

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.

Challenge

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.

Motivation

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
table:=function(n,x,y)
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.

Answer 1

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;
  dblmin1 = \n\f\x. n f (n f (f x)); -- map n to 2*n-1
  go2 = \mx. laver mx sweet mx (\_. mx) (go2 (dblmin1 mx));
in go2 one

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

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010

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

Answer 2

CJam (36 32 bytes)

1{2*31TW$,(+a{0X$j@(@jj}2j)W$=}g

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 A₄ 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 A₆ in milliseconds and overflows the stack testing A₇ - and I've actually deoptimised table in the interests of golfing.

Dissection

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

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

we can remove the first special case, giving

f(x,y) =
    y==1 ? x+1 :
    f(f(x,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

Answer 3

Pyth, 33 bytes

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

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