Te tabele Laver przykłady programów, które nie zostały pokazane, aby zakończyć się w standardowym systemie aksjomatyczną matematyki ZFC , ale które nie kończą, gdy zakłada bardzo duże aksjomaty kardynalnych.

Wprowadzenie

Klasyczne tabele Laver są unikalne skończone algebry z bazowego zestawu i operacja , która spełnia tożsamość i gdzie dla i gdzie .An{1,...,2n}*x * (y * z)=(x * y) * (x * z)x*1=x+1x<2n2n*1=1

Więcej informacji na temat klasycznych stołów Laver można znaleźć w książce Warkocze i autodystrybucja autorstwa Patricka Dehornoya.

Wyzwanie

Jaki jest najkrótszy kod (w bajtach), który oblicza się 1*32w klasycznych tabelach Lavera i kończy się dokładnie, gdy znajdzie znak nz ? Innymi słowy, program kończy się wtedy i tylko wtedy, gdy znajdzie się jednak inaczej działa zawsze.1*32<2nn1*32<2n

Motywacja

Szeregowych do rangi kardynał (zwane również I3-kardynał) jest bardzo duży poziom nieskończoność i jeśli ktoś zakłada istnienie kardynała szeregowych do rangi, a następnie z nich jest w stanie udowodnić kolejne twierdzenia, niż gdyby ktoś nie założyć istnienie kardynała szeregowego. Jeśli istnieje kardynał rangi, to istnieje jakiś klasyczny stół Laver, gdzie . Jednak nie ma znanego dowodu na to, że w ZFC. Ponadto wiadomo, że najmniej gdzie jest większe niż (co jest wyjątkowo dużą liczbą, ponieważ funkcja Ackermanna jest funkcją szybko rosnącą). Dlatego każdy taki program będzie trwał bardzo długo.An1*32<2n1*32<2nn1*32<2nAck(9,Ack(8,Ack(8,254)))Ack

Chcę zobaczyć, jak krótki jest program, abyśmy nie wiedzieli, czy program kończy się przy użyciu standardowego systemu aksomatycznego ZFC, ale gdzie wiemy, że program ostatecznie kończy się w znacznie silniejszym systemie aksomatycznym, a mianowicie ZFC + I3. Pytanie to zostało zainspirowane najnowszym postem Scotta Aaronsona, w którym Aaronson i Adam Yedidia skonstruowali maszynę Turinga z mniej niż 8000 stanów, tak że ZFC nie może udowodnić, że maszyna Turinga się nie kończy, ale wiadomo, że nie kończy się, gdy przyjmuje się duże hipotezy kardynalne.

Jak obliczane są klasyczne tabele Lavera

Przy obliczaniu tabele Laver zwykle jest wygodny w użyciu, że w algebrze , mamy dla wszystkich w .An2n * x=xxAn

Poniższy kod oblicza klasyczną tabelę Lavera An

# tabela (n, x, y) zwraca x * y w A n
tabela: = funkcja (n, x, y)
jeśli x = 2 ^ n, to zwróć y;
elif y = 1, a następnie zwraca x + 1;
w przeciwnym razie zwraca tabelę (n, tabela (n, x, y-1), x + 1); fi; koniec;

Na przykład dane wejściowe table(4,1,2)zostaną zwrócone 12.

Kod dla table(n,x,y)jest raczej nieefektywny i może obliczyć tylko w tabeli Laver w rozsądnym czasie. Na szczęście istnieją znacznie szybsze algorytmy obliczania klasycznych tabel Lavera niż te podane powyżej.A4

Binary Lambda Calculus, 215 bitów (27 bajtów)

\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

kompiluje się do (przy użyciu oprogramowania na https://github.com/tromp/AIT )

000101000110100000010101010100011010000000010110000101111110011110010111
110111100000010101111100000011001110111100011000100000101100100010110101
00000011100111010100011001011101100000010111101100101111011001110100010

To rozwiązanie wynika głównie z https://github.com/int-e

CJam ( 36 32 bajty)

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

W praktyce powoduje to dość szybki błąd, ponieważ przepełnia stos wywołań, ale na teoretycznej nielimitowanej maszynie jest to poprawne i rozumiem, że to założenie tego pytania.

Kod dla table(n,x,y)jest raczej nieefektywny i można go obliczyć tylko w tabeli Lavera A ₄ w rozsądnym czasie.

nie jest właściwie poprawne, jeśli buforujemy obliczone wartości, aby uniknąć ich ponownego obliczenia. Takie podejście zastosowałem, używając joperatora (zapamiętywania) . Testuje A ₆ w milisekundach i przepełnia stos A ₇ - a tak naprawdę zostałem zoptymalizowany table w interesie gry w golfa.

Sekcja

Jeśli założymy, że nrozumiemy to z kontekstu, zamiast

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

możemy usunąć pierwszy specjalny przypadek, dając

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

i nadal działa, ponieważ

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

i dla każdego innego y,

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

więc przez indukcję otrzymujemy f(2^n, y) = y.

W przypadku CJam wygodniej jest odwrócić kolejność parametrów. I zamiast używać zakresu 1 .. 2^n, używam zakresu 0 .. 2^n - 1, zmniejszając każdą wartość, więc implementuję funkcję rekurencyjną

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 bajty

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

Wypróbuj online! (Oczywiście część testowa nie jest tutaj uwzględniona.)