Loader's number

Loader's number is the output of loader.c, a program by Ralph LoaderLoader's home page (It has a web archive.) 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.David Moews' comments on the program, as well as other entriesThe original program (prior to compression) 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 that the program implements a parser, type-checker, interpreter and proof-search for the Huet-Coquand "" (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 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.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. 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 ==
Upquark11111 elaborates the code.Upquark11111. User blog:Upquark11111/An Explanation of Loader's Number 2017-11-30.
#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
Ralph Loader also provided a human-readable version of the above code with the macros expanded and with more expressive variable names and comments.
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)))));
}
==Functions defined in Loader.c==
=== P(y,x) ===
It outputs a number that in binary would be represented as <binary representation of y>1000...0 where the number of 0s after the 1 is equal to x. Notice that you can deduce both x and y by looking at the value of P(x,y).
In loader.c the function is used to create a tree with y denoting the left subtree and x denoting the right subtree.
It's defined as y - ~y << x, which is just (2*y+1)*2^x.
The functions Z(x) and L(x) help extract the right and left subtrees from a tree x.
=== Z(x) ===
It's defined as follows:
# If x is odd, Z(x) = 0.
# If x is even, Z(x) = 1 + Z(x/2) where / hereafter is integral division.
Note that this is just the number of 0s at the end of the binary representation of x, which is exactly the way that the right subtree is encoded in x.
=== L(x) ===
It's defined as the integer part of division (x/2)/2^(Z(x)).
Note that this is just the number you get by removing the 0s at the end of x along with the 1 preceding the 0s, which is exactly the way the the left subtree is encoded in x. Since Z(x) stores the return value in a variable r, when calling Z(x) we get the left subtree as output and the right subtree is automatically stored in the variable r.
=== S(v,y,c,t) ===
It's defined as follows:
# If L(t) = 2, S(v, y, c, t) = A(S(v, y, c, L(x)), S(v, y, c, Z(x))).
# If L(t) > 2 and L(t) = v, S(v, y, c, t) = y.
# If L(t) > 2 and L(t) > v, S(v, y, c, t) = t-c.
# If L(t) > 2 and L(t) < v, S(v, y, c, t) = t.
# If L(t) < 2, S(v, y, c, t) = P(f, P(S(v, y, c, L(x)), S(v + 2, t2, c, Z(x)))) where t2 = S(4, 13, -4, y).
=== A(y,x) ===
It's defined as follows:
# If L(y) = 1, A(y,x) = S (4, x, 4, Z(Z(y))).
# Otherwise, A(y,x) = 5 << P(y, x) = P(2, P(y,x)).
=== D(x) ===
== Programs ==
Programs for calculating Loader's number, other than the original program.
* John Tromp, Binary Lambda Calculus code for a number exceeding Loader's, based on a slightly faster growing Derive function, of length 2236 bits (under 280 bytes).
==See also==
==Footnotes==
==Sources==
ja:ローダー数
Category:Bignum Bakeoff contestant
Category:Functions
Category:Numbers
Category:Computers
Category:Eponymous numbers
Category:Higher computable level
Category:Eponymous functions