Las tablas de Laver proporcionan ejemplos de programas que no se ha demostrado que terminen en el sistema axiomático estándar de matemática ZFC, pero que terminan cuando se asumen axiomas cardinales muy grandes.

Introducción

Las tablas Laver clásicas son las álgebras finitas únicos con el conjunto subyacente y una operación que satisface la identidad y donde para y donde .An{1,...,2n}*x * (y * z)=(x * y) * (x * z)x*1=x+1x<2n2n*1=1

Se puede encontrar más información sobre las tablas clásicas de Laver en el libro Braids and Self-Distributivity de Patrick Dehornoy.

Desafío

¿Cuál es el código más corto (en bytes) que se calcula 1*32en las tablas clásicas de Laver y termina precisamente cuando encuentra un ncon ? En otras palabras, el programa termina si y solo si encuentra un con pero de lo contrario se ejecuta para siempre.1*32<2nn1*32<2n

Motivación

Un cardenal de rango dentro de rango (también llamado cardenal I3) es un nivel extremadamente grande de infinito y si uno asume la existencia de un cardenal de rango dentro de rango, entonces puede probar más teoremas que si no lo hace Supongamos la existencia de un cardenal de rango en rango. Si existe un cardenal de rango en rango, entonces hay alguna tabla clásica de Laver donde . Sin embargo, no hay pruebas conocidas de que en ZFC. Además, se sabe que el menor donde es mayor que (que es un número extremadamente grande ya que la función de Ackermann es una función de rápido crecimiento). Por lo tanto, cualquier programa de este tipo durará mucho tiempo.An1*32<2n1*32<2nn1*32<2nAck(9,Ack(8,Ack(8,254)))Ack

Quiero ver qué tan corto se puede escribir un programa para que no sepamos si el programa termina usando el sistema axiomático estándar ZFC, pero si sabemos que el programa finalmente termina en un sistema axiomático mucho más fuerte, a saber, ZFC + I3. Esta pregunta se inspiró en la reciente publicación de Scott Aaronson en la que Aaronson y Adam Yedidia han construido una máquina de Turing con menos de 8000 estados, de modo que ZFC no puede probar que la máquina de Turing no termina pero se sabe que no termina cuando se asumen grandes hipótesis cardinales.

Cómo se calculan las tablas clásicas de Laver

Cuando se calculan las tablas Laver lo general es conveniente utilizar el hecho de que en el álgebra , tenemos para todos en .An2n * x=xxAn

El siguiente código calcula la tabla clásica de Laver An

# table (n, x, y) devuelve x * y en A n
tabla: = función (n, x, y)
si x = 2 ^ n entonces devuelve y;
elif y = 1 luego devuelve x + 1;
else return table (n, tabla (n, x, y-1), x + 1); fi; final;

Por ejemplo, la entrada table(4,1,2)volverá 12.

El código para table(n,x,y)es bastante ineficiente y solo puede calcular en la tabla Laver en un período de tiempo razonable. Afortunadamente, existen algoritmos mucho más rápidos para computar las tablas clásicas de Laver que los que se dan arriba.A4

Cálculo binario de Lambda, 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

compila a (utilizando software en https://github.com/tromp/AIT )

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010

Esta solución se debe principalmente a https://github.com/int-e

CJam ( 36 32 bytes)

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

En la práctica, esto se corrige rápidamente porque desborda la pila de llamadas, pero en una máquina teórica ilimitada es correcto, y entiendo que esa es la suposición de esta pregunta.

El código para table(n,x,y)es bastante ineficiente y solo puede calcular en la tabla Laver A ₄ en un período de tiempo razonable.

en realidad no es correcto si almacenamos en caché los valores calculados para evitar volver a calcularlos. Ese es el enfoque que he tomado, utilizando el joperador (memorización) . Prueba A ₆ en milisegundos y desborda la pila probando A ₇ , y en realidad me he desmotivado table en interés del golf.

Disección

Si suponemos que nse entiende desde el contexto, en lugar de

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

podemos quitar el primer caso especial, dando

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

y todavía funciona porque

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

y para cualquier otro y,

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

entonces por inducción obtenemos f(2^n, y) = y.

Para CJam resulta más conveniente invertir el orden de los parámetros. Y en lugar de usar el rango 1 .. 2^n, estoy usando el rango 0 .. 2^n - 1al disminuir cada valor, por lo que la función recursiva que estoy implementando es

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

Pruébalo en línea! (Obviamente, la parte de prueba no está incluida aquí).