Changes: Loader's number

Revision as of 10:25, 9 September 2021

Warning: This article includes so many unsourced description. The reader should be careful that the contents might include many fakes.

Loader's number is the output of loader.c, a C program by Ralph Loader 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.^[1]^[2] It is among the largest computable numbers ever devised.^{[citation needed]} 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.

The program diagonalizes over the Huet-Coquand calculus of constructions, a particularly expressive lambda calculus.^{[citation needed]} 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 shown that \(D(99)\) is larger than \(2↑↑30,419\) (where ↑↑ is tetration),^{[citation needed]} and that even \(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.^{[citation needed]} \(D^2(99)\) thus is obviously 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 much larger than TREE(3), SCG(13), and, say, BH(100).^{[citation needed]} It is overpowered by finite promise games and greedy clique sequences^{[citation needed]}. Loader's function is computable, so \(\Sigma(n) > D^5(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

External links

Loader's home page^{[dead link]} (It has a web archive.)

Sources

↑ David Moews' comments on the program, as well as other entries
↑ The original program (prior to compression)

Footnotes

[1] David Moews' comments on the program, as well as other entries

[2] The original program (prior to compression)

[1]

[2]

@@ Line 3: / Line 3: @@
 '''Loader's number''' is the output of '''loader.c''', a {{w|C (programming language)|C}} program by Ralph Loader 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.<ref>[http://djm.cc/bignum-results.txt David Moews' comments on the program, as well as other entries]</ref><ref>[https://github.com/rcls/busy The original program] (prior to compression)</ref> It is among the largest computable numbers ever devised.{{citation needed}} A layman's explanation of the ideas behind loader.c can be found in the last two videos of [https://www.youtube.com/playlist?list=PL-R4p-BRL8NR8THgjx_DW9c92VHTtjZEY this Youtube playlist] on the Bignum Bakeoff contest.
-The program diagonalizes over the Huet-Coquand calculus of constructions, a particularly expressive lambda calculus.{{citation needed}} 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 expressions provable<ref group="note">Here, the provability of an expression does not make sense, and hence the intention of the explanation is ambiguous.</ref> 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''.
+The program diagonalizes over the Huet-Coquand calculus of constructions, a particularly expressive lambda calculus.{{citation needed}} 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 shown that \(D(99)\) is larger than \(2↑↑30,419\) (where ↑↑ is [[tetration]]),{{citation needed}} and that even \(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.{{citation needed}} \(D^2(99)\) thus is obviously much larger than the output of [[Marxen.c]], which is upper bounded at the aforementioned \(f_{\varepsilon_0+\omega^3}(1,000,000)\).