Loader 数
来自Googology Wiki
更多操作
Loader 数是 Ralph Loader 的 C 语言程序 Loader.c 的输出 ，它在 2001 年的 Bignum Bakeoff 比赛（用不超过 512 字的代码生成尽可能大的有限整数）中获得第一名。
其中 D 函数的强度取决于 Huet-Coquand 构造演算（CoC）的证明论强度，其增长率达到了 。迄今为止，它仍然是最强的可计算函数之一。
定义
Loader.c 的源代码[1]如下：
#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
此外，Loader 还给出了可读性更高的版本（我们使用中文注释）：
/*
* loader.c：中文易读版
*
* 这不是“枚举任意 C 程序并运行”，而是按构造演算的规则生成
* 有类型的表达式，并在生成过程中进行替换和 β 归约。
*
* 阅读顺序：
* Pair / Left / Right —— 把表达式树、上下文和记录编码为整数。
* Lift / Subst / Apply —— 调整变量编号、替换变量、计算函数应用。
* Derive —— 从比特流读取选择，按规则构造推导。
* main —— 把上一轮返回的大整数用作下一轮输入。
*
* 注意：这里沿用比赛的数学模型，int 被假定能容纳任意有限整数。
* typedef 本身并不会让现实中的 C int 变成大整数；本文件用于阅读，
* 不是可以直接用普通编译器算出 Loader 数的实现。
*
* 对照来源：
* https://djm.cc/bignum-results.txt （其中的原始 loader.c）
* https://djm.cc/bignum-rules-posted.txt （无限精度整数的比赛约定）
*/
/* 都是 int 的别名；不同名字只提示这个整数当前扮演什么角色。 */
typedef int Tree;
typedef int INT;
typedef int TREE;
typedef int BitStream;
/*
* lastRight：解包时的第二返回值。
* 执行 a = Left(p) 后，a 是左分量，lastRight 是右分量。
* 后续任何 Left / Right 都可能覆盖它，需保留时必须立即另存。
*
* accumulate：所有已完成 Derive 调用的返回记录组成的编码链表。
* 加入一条记录的方法是 Pair(新记录, 旧链表)，不是求和或取最大值。
* 递归调用、main 的五轮调用共用它；中间不清零。
*/
Tree lastRight = 0;
Tree accumulate = 0;
/* Subst 与 Apply 相互调用，因此先声明。 */
TREE Subst(INT vv, TREE yy, INT offset, TREE term);
TREE Apply(TREE yy, TREE xx);
/* ==================== 1. 用整数存放二叉树 ==================== */
/*
* Pair(a,b) = (2a+1) * 2^b。
* 对 a,b >= 0，它把两个非负整数唯一编码为一个正整数。
* 0 不属于 Pair 的值域，留作空上下文、空记录链表。
*
* 例如 Pair(3,2) = 7*4 = 28：
* 28 = 7*2^2，所以右分量是 2，左分量是 (7-1)/2 = 3。
*/
TREE Pair(TREE yy, TREE xx)
{
return (yy - ~yy) << xx; /* ~yy = -yy-1，故 yy-~yy = 2yy+1。 */
}
/*
* 取右分量：计算 xx 能连续除以 2 多少次，也就是其末尾有几个 0。
* 返回结果，并把同一个结果写入 lastRight。
* 前提是 xx > 0；Right(0) 不会终止，空链表不能直接解包。
*/
TREE Right(TREE xx)
{
return lastRight = (xx % 2) ? 0 : 1 + Right(xx / 2);
}
/*
* 取左分量，并顺便把右分量放进 lastRight。
* 若 xx = (2a+1)*2^b，则 (xx/2)>>b 恰好等于 a。
* 这里会重新调用 Right(xx)，不依赖上一次留下的 lastRight。
*/
TREE Left(TREE xx)
{
return (xx / 2) >> Right(xx);
}
/*
* 表达式的编码约定：
*
* Π x:A.B Pair(0, Pair(A,B)) 依赖函数类型
* λ x:A.b Pair(1, Pair(A,b)) 函数本身
* f a Pair(2, Pair(f,a)) 函数应用
* STAR Pair(3,0) = 7 记作 *
* BOX Pair(3,1) = 14 记作 □
* Var(n) Pair(4+2n,0) 整数值为 9+4n
*
* 注意：0 是 Π，1 才是 λ。
* 在 Π 和 λ 中，新变量只在第二个子项 B/b 内绑定，在 A 内不绑定。
*
* 变量不用名字，而用 De Bruijn 索引：
* Var(0) 指最近引入的变量；Var(1) 指再外一层的变量；以此类推。
* 例如 λx.λy.x 的主体 x 用 Var(1) 表示。
*
* 必须区分三个数：
* 变量索引 n；节点标签 4+2n；整个变量的编码 9+4n。
* 所以“索引增加 1”对应“标签增加 2”“完整编码增加 4”。
*
* 上下文记录当前可用的变量及其类型：
* 空上下文 Γ=∅：0
* 扩展为 Γ,x:A：Pair(A,Γ)，最近引入的类型放在链表头。
*
* 在合法表达式中，只有 STAR 和 BOX 满足 (term & 2) != 0。
* 以下用这一编码性质判断一个表达式是否为这两个 sort 之一。
*/
/* ==================== 2. 变量替换与计算 ==================== */
/*
* Lift(t)：在 t 外面新增一层变量时，把 t 的自由变量索引增加 1。
* 已被 t 内部的 λ/Π 绑定的变量不应改变。
*
* 实现方式：把 Var(0) 换成 Var(1)，其余自由变量也向外移一位。
* 4 是 Var(0) 的节点标签；
* 13 是 Var(1) 的完整编码；
* -4 使更外层变量的完整编码减去 -4，也就是增加 4。
* Subst 进入绑定体后会移动替换位置，因此不会误改内部绑定变量。
*/
#define Lift(xx) Subst(4, 13, -4, (xx))
/*
* Subst(vv, yy, offset, term)：在 term 中替换指定变量，并做 β 归约。
*
* vv ：目标变量的节点标签 4+2n（n>=0），不是直接写索引 n。
* yy ：替换进去的表达式。
* offset ：对目标之外、更外层变量的完整编码要减去多少。
* term ：被处理的表达式。
*
* 常见调用：
* Subst(4, a, 4, body)
* 把最内层变量换成 a，并删除这一层绑定；更外层索引减 1。
*
* Subst(4, 13, -4, t)
* 即 Lift(t)，效果是自由变量索引加 1。
*
* 正规化保证的前提：输入 yy、term 已是正规形，且替换结果可正规化。
* 不能把它当成对任意无类型 λ 项都能终止的通用正规化器。
*/
TREE Subst(INT vv, TREE yy, INT offset, TREE term)
{
Tree tag = Left(term);
Tree payload = lastRight;
if (tag > 2) {
/* STAR/BOX 的标签是 3，低于目标变量标签，不会被修改。 */
if (tag == vv)
return yy;
/* 更外层变量调整编号；更内层变量保持不变。 */
return term - (tag > vv ? offset : 0);
}
/* 以下三个构造的 payload 都是“两个子项的配对”。 */
Tree first = Left(payload);
Tree second = lastRight;
if (tag == 2) {
/* (f a)：先处理 f 和 a，再计算新产生的 β 可归约式。 */
Tree fn = Subst(vv, yy, offset, first);
Tree arg = Subst(vv, yy, offset, second);
return Apply(fn, arg);
}
/*
* tag==0：Π x:A.B；tag==1：λ x:A.b。
* 第一个子项 A 不在新变量的作用域内，直接替换。
* 第二个子项多了一层绑定：目标标签 +2，替换项也要 Lift，
* 防止 yy 原有的自由变量被这层绑定意外捕获。
*/
Tree newFirst = Subst(vv, yy, offset, first);
Tree liftedReplacement = Lift(yy);
Tree newSecond = Subst(vv + 2, liftedReplacement, offset, second);
return Pair(tag, Pair(newFirst, newSecond));
}
/*
* Apply(f,a)：形成函数应用，并在可计算时立即计算。
* f = λx:A.b → 返回 b[x:=a] 的正规形。
* f 不是 λ → 保留应用节点 (f a)。
* 与 Subst 一样，这里依赖输入已正规化、结果可正规化的前提。
*/
TREE Apply(TREE yy, TREE xx)
{
if (Left(yy) == 1) {
Tree body = Right(lastRight); /* λ 的 payload 是 Pair(A,body)。 */
return Subst(4, xx, 4, body);
}
return Pair(2, Pair(yy, xx));
}
/* ==================== 3. 从比特流读取选择 ==================== */
/*
* 把原来的 MAYBE 宏拆开：先除以 2，再读取新的最低位。
* 必须是这个顺序，不是先读取原来的最低位。
*
* 所有选择都是输入整数确定的，不是随机选择。
* 即使某条规则不能执行，有些位置仍必须读取一位；详见 Derive。
* 删除这些“没有产生动作的读位”也会改变后续推导。
*/
INT ReadBit(BitStream *stream)
{
*stream /= 2;
return *stream % 2;
}
/* ==================== 4. 按类型规则构造推导 ==================== */
/*
* 三个核心变量共同表示一个判断：
*
* context ⊢ term : type
*
* 即“在 context 列出的假设下，term 的类型是 type”。
* 比特流决定下一步尝试什么；规则的前提决定该步能否真的执行。
* term/type 在构造过程中保持正规形，因此需要比较类型时可以比较编码。
*
* 每次 Derive 返回时，将当时的四元组保存为：
* record = Pair(term, Pair(type, Pair(剩余比特流, context)))。
* 返回的是加入该 record 后的整个 accumulate，不是单独的 term。
*/
TREE Derive(BitStream xx)
{
Tree context = 0;
Tree term = 7;
Tree type = 14; /* 初始公理：∅ ⊢ * : □。 */
for (;;) {
/*
* 原来 while 条件逗号左边的动作：
* 先递归处理 xx-1，从而也覆盖较小的输入，并把记录加入累积器。
* 原版每次回到循环条件都会做这一步，不只在函数入口做一次。
*/
if (xx != 0)
Derive(xx - 1);
/* 原来 while 条件逗号右边的动作：读到 0 就结束本次推导。 */
if (!ReadBit(&xx))
break;
/*
* 构造另一份推导 Γ' ⊢ auxTerm : aux，供双前提规则使用。
* 子调用返回整个累积链表；最外层 Left 取出其最新记录。
*/
Tree record = Left(Derive(xx));
Tree auxTerm = Left(record);
Tree aux = Left(lastRight);
xx = Left(lastRight); /* 接着消费子推导未用完的比特。 */
Tree auxContext = lastRight;
/* ---------- A. 需要两份推导的规则 ---------- */
if (context == auxContext) {
/*
* 函数应用：
* Γ ⊢ f : Πx:A.B Γ ⊢ a : A
* --------------------------------
* Γ ⊢ f a : B[x:=a]
*
* 只有函数类型确为 Π，且参数类型匹配，才读取应用选择位。
*/
if (Left(type) == 0) {
Tree domain = Left(lastRight);
Tree codomain = lastRight;
if (domain == aux && ReadBit(&xx)) {
type = Subst(4, auxTerm, 4, codomain);
term = Apply(term, auxTerm);
}
}
/*
* 弱化：已知 Γ ⊢ A : s，s 为 * 或 □，允许增加假设 x:A。
* 原来的 term/type 仍有效，但自由变量编号都要 Lift。
*
* 这是独立的下一步，不是上面应用规则的 else 分支。
* 与原式 aux/2 & MAYBE(...) 一致：这里总要读取一位，
* 然后才决定是否执行弱化，即使 aux 不是 sort 也一样。
*/
INT chooseWeaken = ReadBit(&xx);
if ((aux & 2) && chooseWeaken) {
context = Pair(auxTerm, context);
term = Lift(term);
type = Lift(type);
}
}
/* ---------- B. 收起上下文中最近的一项 ---------- */
if (context && ReadBit(&xx)) {
Tree domain = Left(context);
Tree outerContext = lastRight;
/*
* 现在处于 Γ,x:A ⊢ term : type。
*
* type 为 * 或 □ 时，可以选择：
* 0：构造 Πx:A.term，类型仍为 type；
* 1：构造 λx:A.term，类型改为 Πx:A.type。
*
* type 不是 sort 时，不能做 Π 形成，强制选择 λ 引入。
* 但原版即使强制选择，也仍读取这个选择位，不能跳过。
* 原程序在这里放宽了 λ 引入：不另外检查新 Π 类型的可赋型性。
*/
INT choice = ReadBit(&xx);
INT isLambda = !(type & 2) || choice; /* 结果严格为 0 或 1。 */
if (isLambda)
type = Pair(0, Pair(domain, type));
term = Pair(isLambda, Pair(domain, term));
context = outerContext;
}
/* ---------- C. 引入一个新变量 ---------- */
/*
* 若 Γ ⊢ A : s，s 是 * 或 □，就可以得到 Γ,x:A ⊢ x : A。
* 新变量用 Var(0) 表示。A 进入扩展上下文后，其编码要 Lift。
*
* 这里也必须先读取一位，即使 type 不是 sort。
*/
INT chooseVariable = ReadBit(&xx);
if ((type & 2) && chooseVariable) {
context = Pair(term, context);
type = Lift(term);
term = 9; /* Var(0) = Pair(4,0)。 */
}
}
/* 每次 Derive 返回时记一条；不是每条规则执行完都额外记一条。 */
Tree record = Pair(term, Pair(type, Pair(xx, context)));
accumulate = Pair(record, accumulate);
return accumulate;
}
/* ==================== 5. 把结果重新作为输入 ==================== */
TREE main(void)
{
/*
* 从内到外调用五次，每次返回值成为下一次的比特流输入。
* accumulate 跨越五轮持续保留，因此 Derive 不是无状态的纯函数。
* 比赛把 main 的返回值当作结果；这里并没有打印十进制数字。
*/
return Derive(Derive(Derive(Derive(Derive(99)))));
}