in: Pages with dead links, Bignum Bakeoff contestant, Functions, and 5 more

English

Loader's number

View full site to see MathJax equation

Loader's number 是 loader.c 的输出结果，这是一个由 Ralph Loader 编写的 C 程序，该程序在 Bignum Bakeoff 竞赛中获得第一名。该竞赛的目标是用 C 语言（在 512 个字符或更少的情况下）编写一个程序，在具有无限内存的理论机器上生成尽可能大的输出。[1] [2][3] 关于 loader.c 背后的想法的通俗解释可以在 这个 Youtube 播放列表 的最后两个视频中找到，该播放列表是关于 Bignum Bakeoff 竞赛的。

Ralph Loader 在程序的文档[3]中解释说，该程序实现了一个解析器、类型检查器、解释器以及 Huet-Coquand "Calculus of Constructions" (CoC) 的证明搜索，CoC 是一种特别富有表现力的 lambda 演算。David Moews 表示[2]该程序对 CoC 进行了对角化处理，但是没有实际的书面证明来支持他们的陈述。它的输出，被亲切地昵称为 Loader's number，定义为 \(D^5(99)=D(D(D(D(D(99)))))\)，其中 \(D(k)\) 是所有可能的类型判断（声明一个表达式在某个上下文中具有某种类型）的累积，这些类型判断可以在构造演算中大约 \(\log(k)\) 个推理步骤内证明（将证明编码为二进制数，并将表达式编码为幂塔）。构造演算的证明强度和表达能力使得 \(D(k)\) 的输出对于足够大的 k 增长非常大。

David Moews 已经声明，可以模拟 \(D(99)\) 的行为以表明它大于 \(2↑↑30,419\)（其中 ↑↑ 是 tetration），并且 \(D^2(99)\) 将远大于 fast-growing hierarchy 中使用 Cantor 的基本序列定义的 \(f_{\varepsilon_0+\omega^3}(1,000,000)\)，这是基于 Fortune 等人建立在 "The Expressiveness of Simple and Second-Order Type Structures" 的基础上的。[2] 虽然没有可访问的证据来证明这些说法，但如果这是真的，那么 \(D^2(99)\) 远大于 Marxen.c 的输出，该输出的上界是前面提到的 \(f_{\varepsilon_0+\omega^3}(1,000,000)\)。

\(D^5(99)\) 的最终输出是 Loader's number，它远大于 \(D^2(99)\)，但与其他大数的比较并不容易。[note 1] Loader's function 是 computable 的，所以对于相对较小的 n ，比如 n = 2000，有 \(\Sigma(n) > D^5(99)\)，其中 \(\Sigma(n)\) 是 Busy beaver function。

Contents

Code[]

Upquark11111 详细阐述了代码。[4]

#define R { return
#define P P (
#define L L (
#define T S (v, y, c,
#define C ),
#define X x)
#define F );}
intr,a;
Py,X
Ry-~y<<x;
}
Z(X
Rr=x%2?0:1+Z(x/2F
LX
Rx/2>>Z(xF
#define U = S(4,13,-4,
Tt)
{
int
f=LtC
x=r;
R
f-2?
f>2?
f-v?t-(f>v)*c:y:
Pf,PTLXC
S(v+2,tUyCc,Z(X)))
:
A(TLXC
TZ(X)F
}
A(y,X
RLy)-1
?5<<Py,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-1CB1))
d=LLD(X)C
f=LrC
x=LrC
c-r||(
Lu)||Lr)-f||
Bu=S(4,d,4,rC
t=A(t,d)C
f/2&Bc=Pd,cC
tUtC
uUu))
C
c&&B
t=P
~u&2|B
u=1<<PLcCu)C
PLcCt)C
c=rC
u/2&B
c=Pt,cC
uUtC
t=9);
Ra=PPt,Pu,Px,c))C
aF
}
main()
RD(D(D(D(D(99))))F

Ralph Loader 还提供了上述代码的可读版本，其中宏已展开，并具有更具表现力的变量名称和注释。

typedefintTree;
typedefintINT;
typedefintTREE;
typedefintBitStream;
#define DESCEND xx
TreelastRight,accumulate;
// A bijective pairing.
TREEPair(TREEyy,TREExx)
{
// x - ~x = x - (-1 - x) = 2 * x + 1
returnyy-~yy<<xx;
}
// The second component of a pair.
TREERight(TREExx)
{
returnlastRight=xx%2?0:1+Right(xx/2);
}
// The first component. Note that we leave the other component in lastRight.
TREELeft(TREExx)
{
returnxx/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.]
TREESubst(INTvv,TREEyy,INTcontext,TREEterm)
{
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).
TREEApply(TREEyy,TREExx)
{
returnLeft(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.
TREEDerive(BitStreamxx)
{
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.
returnaccumulate=Pair(Pair(term,Pair(type,Pair(xx,context))),
accumulate);
}
}
TREEmain()
{
returnDerive(Derive(Derive(Derive(Derive(99)))));
}

Functions defined in Loader.c[]

P(y,x)[]

它输出一个数字，该数字在二进制中表示为 <y 的二进制表示>1000...0，其中 1 之后的 0 的数量等于 x。请注意，您可以通过查看 P(x,y) 的值来推断出 x 和 y。

在 loader.c 中，该函数用于创建一个树，其中 y 表示左子树，x 表示右子树。

它被定义为 y - ~y << x，它只是 (2*y+1)*2^x。

函数 Z(x) 和 L(x) 帮助从树 x 中提取左右子树。

Z(x)[]

它定义如下：

  1. 如果 x 是奇数，则 Z(x) = 0。
  2. 如果 x 是偶数，则 Z(x) = 1 + Z(x/2)，其中 / 在此后是整数除法。

请注意，这只是 x 的二进制表示末尾的 0 的数量，这正是右子树在 x 中编码的方式。

L(x)[]

它被定义为除法 (x/2)/2^(Z(x)) 的整数部分。

请注意，这只是通过删除 x 末尾的 0 以及 0 前面的 1 而得到的数字，这正是左子树在 x 中编码的方式。由于 Z(x) 将返回值存储在变量 r 中，因此在调用 Z(x) 时，我们得到左子树作为输出，而右子树自动存储在变量 r 中。

S(v,y,c,t)[]

它定义如下：

  1. 如果 L(t) = 2, S(v, y, c, t) = A(S(v, y, c, L(x)), S(v, y, c, Z(x))).
  2. 如果 L(t) > 2 并且 L(t) = v, S(v, y, c, t) = y.
  3. 如果 L(t) > 2 并且 L(t) > v, S(v, y, c, t) = t-c.
  4. 如果 L(t) > 2 并且 L(t) < v, S(v, y, c, t) = t.
  5. 如果 L(t) < 2, S(v, y, c, t) = P(f, P(S(v, y, c, L(x)), S(v + 2, t2, c, Z(x)))) 其中 t2 = S(4, 13, -4, y).

A(y,x)[]

它定义如下：

  1. 如果 L(y) = 1, A(y,x) = S (4, x, 4, Z(Z(y))).
  2. 否则, A(y,x) = 5 << P(y, x) = P(2, P(y,x)).

D(x)[]

它真的很令人困惑，但证明的是 D(0) = 8 646 911 284 551 352 321 并且 D(3) 可以使计算机崩溃。

Programs[]

用于计算 Loader's number 的程序，除了原始程序。

See also[]

computers 中的大数 Main article: Numbers in computer arithmetic 127 · 128 · 256 · 32767 · 32768 · 65536 · 2147483647 · 4294967296 · 9007199254740991 · 9223372036854775807 · FRACTRAN catalogue numbersBignum Bakeoff contestants: pete-3.c · pete-9.c · pete-8.c · harper.c · ioannis.c · chan-2.c · chan-3.c · pete-4.c · chan.c · pete-5.c · pete-6.c · pete-7.c · marxen.c · loader.c****Channel systems: lossy channel system · priority channel systemConcepts: Recursion

Footnotes[]

  1. ↑ 本文中有未提供来源的描述，说 \(D^5(99)\) 的最终输出远大于 TREE(3), SCG(13), 和比如说 BH(100)，而且它被 finite promise games 和 greedy clique sequences 所超越。但是，这些描述没有基于证据，因此可能是错误的。

Sources[]

  1. ↑ Loader's home page[dead link] (它有 a web archive.)
  2. ↑ 2.0 2.1 2.2 David Moews' comments on the program, as well as other entries
  3. ↑ 3.0 3.1 The original program (prior to compression)
  4. ↑ Upquark11111. User blog:Upquark11111/An Explanation of Loader's Number 2017-11-30.