Googology Wiki
Advertisement
Googology Wiki

Loader's number is the output of loader.c, a C program by Ralph Loader[1] that came in first place for the Bignum Bakeoff contest, whose objective was to write a C program (in 512 characters or less) that generates the largest possible output on a theoretical machine with infinite memory.[2][3] A layman's explanation of the ideas behind loader.c can be found in the last two videos of this Youtube playlist on the Bignum Bakeoff contest.

Ralph Loader explains in the document of the program[3] that the program implements a parser, type-checker, interpreter and proof-search for the Huet-Coquand "Calculus of Constructions" (CoC), a particularly expressive lambda calculus, and David Moews stated[2] that the program diagonalizes over the CoC, but there is no actual written proof for their statements. Its output, affectionately nicknamed Loader's number, is defined as \(D^5(99)=D(D(D(D(D(99)))))\), where \(D(k)\) is an accumulation of all possible typing judgements (a statement that an expression has a some type under some context) provable within approximately \(\log(k)\) inference steps in the calculus of constructions (encoding proofs as binary numbers and expressions as power towers). The proof strength and expressiveness of the calculus of constructions makes the output of \(D(k)\) grow very large for sufficiently large k.

David Moews has stated that the behavior of \(D(99)\) can be simulated to show that it is larger than \(2↑↑30,419\) (where ↑↑ is tetration), and that \(D^2(99)\) would be much larger than \(f_{\varepsilon_0+\omega^3}(1,000,000)\) in the fast-growing hierarchy using Cantor's definition of fundamental sequences, on the basis that the number of this size can be expressed by building upon "The Expressiveness of Simple and Second-Order Type Structures" by Fortune et al..[2] Although there is no accessible proof of either claims, if this is true, then \(D^2(99)\) is much larger than the output of Marxen.c, which is upper bounded at the aforementioned \(f_{\varepsilon_0+\omega^3}(1,000,000)\).

The final output of \(D^5(99)\) is the Loader's number, which is much larger than \(D^2(99)\) but comparison to other large numbers is not easy.[note 1] Loader's function is computable, so \(\Sigma(n) > D^5(99)\) for relatively small n, say, n = 2000, where \(\Sigma(n)\) is the Busy beaver function.

Code

#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

See also

Footnotes

  1. There were unsourced descriptions in this article that the final output of \(D^5(99)\) is much larger than TREE(3), SCG(13), and, say, BH(100), and that it is overpowered by finite promise games and greedy clique sequences. However, the descriptions were not based on proof and therefore might be wrong.

Sources

Advertisement