Число Лоудера

Число Лоудера — это выходные данные loader.c, программы на языке программирования C от Ральфа Лоудера^[1] который занял первое место в конкурсе Бигнум бейкофф, целью которого было написать программу на языке C (объёмом 512 символов или меньше), которая генерирует максимально возможный вывод на теоретической машине с бесконечной памятью.^[2]^[3] Объяснение неспециалистом идей, лежащих в основе loader.c, можно найти в последних двух видеороликах в этом плейлисте Youtube.

Ральф Лоудер объясняет в документе программы^[4], что программа реализует синтаксический анализатор, проверку типов, интерпретатор и поиск доказательств для Хьюэ-Коканда "исчисления конструкций" (CoC), особенно выразительного лямбда-исчисления, и Дэвид Моюз заявил ^[5], что программа диагонализуется поверх CoC, но фактических письменных доказательств их утверждений нет. Его выходные данные, ласково называемые числом Лоудера, определяются как $D^5(99)=D(D(D(D(D(99)))))$ , где $D(k)$ - совокупность всех возможных типизирующих суждений (утверждение что выражение имеет некоторый тип в некотором контексте), доказуемый приблизительно в пределах $\log (k)$ шагов вывода в исчислении конструкций (кодирование доказательств в виде двоичных чисел и выражений в виде опор электропередач). Сила доказательства и выразительность исчисления конструкций приводят к тому, что выходные данные $D(k)$ становятся очень большими для достаточно большого "k".

Дэвид Моюз заявил, что поведение $D(99)$ можно смоделировать, чтобы показать, что оно больше, чем $2 \uparrow\uparrow 30,419$ (где $\uparrow\uparrow$ - тетрация), и что $D^2(99)$ было бы намного больше, чем $f_{\varepsilon_{0} + \omega^{3}}(1000000)$ в быстрорастущей иерархии с использованием определения фундаментальных последовательностей Кантора, исходя из того, что число такого размера может быть выражено, опираясь на "Выразительность простых структур и структур второго порядка" от Fortune и др.^[6] Хотя нет доступных доказательств ни того, ни другого утверждения, если это правда, тогда $D^2(99)$ намного больше, чем выходные данные Marxen.c, которые ограничены сверху вышеупомянутым $f_{\varepsilon_{0} + \omega^{3}}(1000000)$ .

Конечный результат $D^5(99)$ - это число Лоудера, которое намного больше, чем $D^2(99)$ , но сравнить это с другими большими числами непросто.^{[note 1]} Функция Лоудера является вычислимой, поэтому $\Sigma(n) > D^5(99)$ для относительно небольшого "n", скажем, "n" = 2000, где $\Sigma(n)$ - это функция занятого бобра.

Код[]

#define R { return
#define P P (
#define L L (
#define T S (v, y, c,
#define C ),
#define X x)
#define F );}

int r, a;
P y, X
   R y - ~y << x;
}
Z (X
   R r = x % 2 ? 0 : 1 + Z (x / 2 F
L X
   R x / 2 >> Z (x F
#define U = S(4,13,-4,
T  t)
{
   int
      f = L t C         
      x = r;
   R
         f - 2 ?
         f > 2 ?
         f - v ? t - (f > v) * c : y :
         P f, P T  L X  C 
                          S (v+2, t  U y C  c, Z (X )))
         :
         A (T  L X  C 
                T  Z (X ) F
}
A (y, X
   R L y) - 1
      ? 5 << P y, X 
      : S (4, x, 4, Z (r) F
#define B (x /= 2) % 2 && (
D (X 
{
   int
      f,
      d,
      c = 0,
      t = 7,
      u = 14;
   while (x && D (x - 1 C  B 1))
      d = L L D (X ) C
         f = L r C
         x = L r C
         c - r || (
            L u) || L r) - f ||
            B u = S (4, d, 4, r C 
                   t = A (t, d) C
            f / 2 & B  c = P d, c C 
                              t  U t C 
                              u  U u) )
             C
         c && B
            t = P
               ~u & 2 | B
                  u = 1 << P L c C  u) C 
               P L c C  t) C
            c = r  C
         u / 2 & B 
            c = P t, c C 
            u  U t C 
            t = 9 );
   R a = P P t, P u, P x, c)) C 
                                a F
}
main ()
   R D (D (D (D (D (99)))) F

Ральф Лоудер также предоставил удобочитаемую версию приведённого выше кода с расширенными макросами и более выразительными именами переменных и комментариями.

typedef int Tree;
typedef int INT;
typedef int TREE;
typedef int BitStream;
#define DESCEND xx

Tree lastRight, accumulate;

// A bijective pairing.
TREE Pair (TREE yy, TREE xx)
{
   // x - ~x = x - (-1 - x) = 2 * x + 1
   return yy - ~yy << xx;
}

// The second component of a pair.
TREE Right (TREE xx)
{
   return lastRight = xx % 2 ? 0 : 1 + Right (xx / 2);
}

// The first component.  Note that we leave the other component in lastRight.
TREE Left (TREE xx)
{
   return xx / 2 >> Right (xx);
}

// Encoding
// PI(A,B) = Pair(0,Pair(A,B))
// LAMBDA(A,B) = Pair(1,Pair(A,B))
// APPLY(A,B) = Pair(2,Pair(A,B))
// STAR = Pair(3,0) = 7
// BOX = Pair(3,1) = 14
// VAR(n) = Pair(4+2n,0) = 9 + 4n [n >= 0]
// The empty context is 0, and the context Gamma,A is Pair (A,Gamma).
// STAR and BOX are the only terms x with (x&2)!=0

// Increment the index of each variable in xx.  Uses Subst.
// Making this a macro means that we can absorb an "=" and a "(" into the macro.
#define Lift(xx) Subst (4, 13, -4, xx)

// Substitute yy for vv in term, and normalise.  Variables > yy get adjusted by
// -context.  [The precise normalisation is: if yy and term are normal, and the
// substitution has a normal form, then the normal form is returned.]
TREE Subst (INT vv, TREE yy, INT context, TREE term)
{
   Tree
      aux = Left (term),        // The operation of term.
      xx = lastRight;           // The body of term.

   {
      return
         aux - 2 ?
         aux > 2 ?
         // Variable or Star or Box.
         aux - vv ? term - (aux > vv) * context : yy :
         // aux = 0 or aux = 1: lambda or pi.  The stray 'term =' below is
         // harmless, but allows us to push the '=' into the Lift macro.
         Pair (aux, Pair (Subst (vv, yy, context, Left (xx)),
                          Subst (vv+2, term = Lift (yy), context, Right (xx))))
         :
         // Application.  Use Apply.
         Apply (Subst (vv, yy, context, Left (xx)),
                Subst (vv, yy, context, Right (xx)));
   }
}

// Apply yy to xx and normalise.  [Precisely, if yy and xx are normal, and
// yy(xx) is normalisable, Apply(yy,xx) returns the normal form of yy(xx).
TREE Apply (TREE yy, TREE xx)
{
   return Left (yy) - 1
      // 5 << x == Pair(2,x)
      ? 5 << Pair (yy, xx)
      : Subst (4, xx, 4, Right (lastRight));
}

// We use xx as a bit stream.  The MAYBE macro tests the next bit for us.
#define MAYBE (xx /= 2) % 2 &&

// Derive parses a bit stream into terms of CoC and normalises everything.  The
// outputs are accumulated into the variable yy.  We also recurse, so as to
// cover all the BitStreams which are < xx.
TREE Derive (BitStream xx)
{
   Tree
      aux,
      auxTerm,
      // The axiom.
      context = 0,
      term = 7,
      type = 14;

   // Inside the while condition is the main recursion that makes us monotone.
   // It doesn't need to be inside the while, but that allows us to compress the
   // "),".  It also means we get called more often, which makes "accumulate"
   // bigger...
   while (DESCEND && Derive (xx - 1), MAYBE (1))

      // Get another term.
      auxTerm = Left (Left (Derive (xx))),
         // And get its type.
         aux = Left (lastRight),

         // And get the left-over bit-stream.  This leaves the context from
         // the sub-derivation in lastRight.
         xx = Left (lastRight),

         // Rules that depend on two antecedents...  The two contexts (one is in
         // lastRight) must be the same.
         context - lastRight || (
            // APPLY.  type must be PI(aux,-).
            Left (type) || Left (lastRight) - aux ||
            MAYBE (type = Subst (4, auxTerm, 4, lastRight),
                   term = Apply (term, auxTerm)),

            // Weakening.  auxType must be STAR or BOX.  The / 2 & MAYBE
            // combines MAYBE with testing the correct bit of auxType.  It is
            // safe to do this immediately after an APPLY above, because APPLY
            // does not change contexts.
            aux / 2 & MAYBE ( context = Pair (auxTerm, context),
                              term = Lift (term),
                              type = Lift (type) )

            ),

         context && MAYBE (
            // If we get here, we are either going to do PI formation or LAMBDA
            // introduction.  PI formation requires type to be STAR or BOX.  We
            // allow LAMBDA introduction whenever the context is non-empty.
            // This extension is a conservative extension of CoC.
            term = Pair (
               // Because of the && in MAYBE, this subexpression returns a
               // boolean 1 if we're doing LAMBDA introduction, 0 if we're
               // doing PI formation.  The ~type&2| ensures that we do LAMBDA
               // introduction if type is not the Star or Box needed to do PI
               // formation.
               ~type & 2 | MAYBE (
                  // If we're doing lambda introduction on term, then we also
                  // need to do a PI formation on type.  This is always
                  // non-zero.  1 << x = Pair(0,x).
                  type = 1 << Pair (Left (context), type)),
               Pair (Left (context), term)),

            // Remove the context item we just used.
            context = lastRight ),

         // If type is STAR or BOX then we allow variable introduction.
         type / 2 & MAYBE (
            context = Pair (term, context),
            type = Lift (term),
            term = 9 );     // Pair (4, 0)
   {
      // Pair term, type, context, and xx together, and chuck it all onto
      // accumulate.
      return accumulate = Pair (Pair (term, Pair (type, Pair (xx, context))),
                                accumulate);
   }
}

TREE main ()
{
   return Derive (Derive (Derive (Derive (Derive (99)))));
}

Функции, определенные в Loader.c[]

P(y,x)[]

P выводит число, которое в двоичном формате было бы представлено как <двоичное представление y>1000...0, где число 0 после 1 равно x. Обратите внимание, что вы можете вывести как x, так и y, посмотрев на значение P(x,y).

В loader.c функция используется для создания дерева, где y обозначает левое поддерево, а x - правое поддерево.

Он определяется как y - ~y << x, что равно всего лишь (2*y+1)*2^x.

Функции Z(x) и L(x) помогают извлекать левое и правое поддеревья из дерева x.

Z(x)[]

Это определяется следующим образом:

Если x нечётное, то Z(x) = 0.
Если x чётно, то Z (x) = 1 + Z (x / 2), где / далее - целочисленное деление.

Обратите внимание, что это всего лишь число 0 в конце двоичного представления x, которое точно так же кодируется в x правое поддерево.

L(x)[]

Это определяется как целая часть деления (x/2)/2^(Z(x)).

Обратите внимание, что это всего лишь число, которое вы получаете, удаляя 0 в конце x вместе с 1, предшествующим 0, что в точности соответствует способу кодирования левого поддерева в x. Поскольку Z(x) сохраняет возвращаемое значение в переменной r, при вызове Z(x) мы получаем левое поддерево в качестве выходных данных, а правое поддерево автоматически сохраняется в переменной r.

S(v,y,c,t)[]

Это определяется следующим образом:

Если L(t) = 2, S(v, y, c, t) = A(S(v, y, c, L(x)), S(v, y, c, Z(x))).
Если L(t) > 2 и L(t) = v, S(v, y, c, t) = y.
Если L(t) > 2 и L(t) > v, S(v, y, c, t) = t-c.
Если L(t) > 2 и L(t) < v, S(v, y, c, t) = t.
Если L(t) < 2, S(v, y, c, t) = P(f, P(S(v, y, c, L(x)), S(v + 2, t2, c, Z(x)))) где t2 = S(4, 13, -4, y).

A(y,x)[]

Это определяется следующим образом:

Если L(y) = 1, A(y,x) = 5 << P(y, x) = 5*2^P(y,x).
В противном случае A(y,x) = S (4, x, 4, Z (r)).

D(x)[]

Сноски[]

↑ В этой статье были неопубликованные описания того, что конечный результат $D^5(99)$ намного больше, чем TREE(3), SCG(13) и, скажем, BH(100), и что он подавлен игрой с конечным обещанием и последовательностью жадных кликов. Однако описания не были основаны на доказательствах и поэтому могли быть ошибочными.

Примечания[]

↑ домашняя страница Лоудера (На ней есть веб-архив.)
↑ Комментарии Дэвида Моюза к программе, а также другие записи
↑ Оригинальная программа (перед сжатием)
↑ Оригинальная программа (перед сжатием)
↑ Комментарии Дэвида Моюза к программе, а также другие записи
↑ Комментарии Дэвида Моюза к программе, а также другие записи

[7] В этой статье были неопубликованные описания того, что конечный результат $D^5(99)$ намного больше, чем TREE(3), SCG(13) и, скажем, BH(100), и что он подавлен игрой с конечным обещанием и последовательностью жадных кликов. Однако описания не были основаны на доказательствах и поэтому могли быть ошибочными.

[1] домашняя страница Лоудера (На ней есть веб-архив.)

[2] Комментарии Дэвида Моюза к программе, а также другие записи

[3] Оригинальная программа (перед сжатием)

[4] Оригинальная программа (перед сжатием)

[5] Комментарии Дэвида Моюза к программе, а также другие записи

[6] Комментарии Дэвида Моюза к программе, а также другие записи

[1]

[2]

[3]

[4]

[5]

[6]

[note 1]