Nombre de Loader

Le Nombre de Loader est la sortie de loader.c, un programme C de Ralph Loader qui a remporté la première place du concours Bignum Bakeoff, dont l'objectif était d'écrire un programme C (en 512 caractères ou moins) qui génère la plus grande sortie possible sur une machine théorique à mémoire infinie.

The program diagonalizes over the Huet-Coquand calculus of constructions, a particularly expressive lambda calculus. Its output, affectionately nicknamed Loader's number, is defined as D⁵(99)=D(D(D(D(D(99))))), where D(k) is an accumulation of all possible expressions 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 shown that D(99) is larger than 2↑↑30419 (where ↑↑ is tétration), and that even D²(99) would be much larger than $f_{\varepsilon_{0} + \omega^{3}}(1000000)$ in the hiérarchie de croissance rapide, using Cantor's definition of fundamental sequences. D²(99) thus is obviously much larger than the output of Marxen.c, which is upper bounded at the aforementioned $f_{\varepsilon_{0} + \omega^{3}}(1000000)$.

The final output of D⁵(99) is much larger than TREE(3), SCG(13), and, say, BH(100). Loader's function is computable, so Σ(n) > D⁵(99) for relatively small n, say, n = 2000.

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