Loader's Number

Summary

View full site to see MathJax equation 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.[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 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.. 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 bound...