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.

• NoOneIsHere: Welcome to PPCG! Great post!
• John Tromp: 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.
• Peter Taylor: 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?
• Peter Taylor: 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.
• Peter Taylor: cheddarmonk.org/papers/laver.pdf is as much as I expect to get done this week, because I'm going to be travelling.

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;
 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)

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010

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

• Alex A.: 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.
• CalculatorFeline: You should probably include the exact code of length 234 bits in your post.
• PurkkaKoodari: 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.
• Alex A.: For compiled languages, we score the code written by the user--not the number of bytes in the generated binary.
• feersum: @AlexA. That's not necessary... any form of the code that can be understood by a compiler or interpreter is fine.

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.)

• Leaky Nun: What loop? Also, what does fi in the code mean?

Answer 4

Javascript, 53 bytes

for(M=0;!g(1,31);M-=~M)g=(x,y)=>y?g(g(x,y-1),x):x+1&M

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