Loader 数
来自Googology Wiki
更多操作
Loader 数是 Ralph Loader 的 C 语言程序 Loader.c 的输出 ，它在 2001 年的 Bignum Bakeoff 比赛（用不超过 512 字的代码生成尽可能大的有限整数）中获得第一名。
其中 D 函数的强度取决于 Huet-Coquand 构造演算（CoC）的证明论强度，其增长率达到了 。迄今为止，它仍然是最强的可计算函数之一。
定义
Loader.c 的源代码如下：
#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 还给出了可读性更高的版本（我们使用中文注释）：
//Tree、INT、TREE、BitStream 都被定义为 int，只是为了区分用途。
//把宏 DESCEND 直接展开为变量 xx，用于 while 里的递归控制。
typedef int Tree;
typedef int INT;
typedef int TREE;
typedef int BitStream;
#define DESCEND xx
// 全局临时变量：
// lastRight —— 用于在解码配对结构时暂存“另一半”值；
// accumulate —— 累积所有推导结果（每个结果是(term, type, 剩余比特流, context) 四元组的配对编码）。
Tree lastRight, accumulate;
// —— 基础编码：二元配对函数 ——
// 将两个非负整数 yy, xx 编码为一个整数，保证一一对应（双射）。
// 公式：Pair(yy,xx) = (yy − ~yy) << xx = (2*yy + 1) << xx
// 这样低位的连续零数目即为 xx，高位奇数部分即为 2*yy+1，方便快速解码。
TREE Pair (TREE yy, TREE xx)
{
return yy - ~yy << xx;
}
// —— 解码：取配对的第二个分量 ——
// 从编码值 xx 中恢复出原始的第二个参数（移位次数）。
// 逻辑：若 xx 为奇数，则移位次数为 0；否则不断除以 2 并累加，直到遇到奇数。
// 计算结果同时写入 lastRight。
TREE Right (TREE xx)
{
return lastRight = xx % 2 ? 0 : 1 + Right (xx / 2);
}
// —— 解码：取配对的第一个分量 ——
// 先将编码右移 1 位（去除最低位信息），再右移 Right(xx) 位，得到原始的 yy。
// 上一次调用 Right 时已经把移位计数存入 lastRight，因此这里可直接使用。
TREE Left (TREE xx)
{
return xx / 2 >> Right (xx);
}
// —— 宏：提升（Lift） ——
// 将所有自由变量的 De Bruijn 索引统一 +1，维护绑定层级。
// 通过 Subst(vv=4, yy=13, context=-4, term=xx) 实现。
#define Lift(xx) Subst (4, 13, -4, xx)
// —— 归一化替换（Subst） ——
// 在 term 中，将索引 vv 的变量替换为术语 yy，并对索引 > vv 的变量减去 context。
// 同时对 λ 抽象 (aux=0)、Π 构造 (aux=1) 和函数应用 (aux=2) 等节点进行递归归一化。
// 参数说明：
// vv : 要替换的变量索引
// yy : 用来替换的术语（已规范化）
// context : 替换后，所有更大索引变量需减去的偏移
// term : 待处理的术语编码
TREE Subst (INT vv, TREE yy, INT context, TREE term)
{
Tree aux = Left (term), // 当前节点类型：0=λ，1=Π，2=应用，>2=变量/常量
xx = lastRight; // 当前节点主体或子配对
// 按节点类型分支处理
if (aux == 2) {
// 应用节点：先递归替换，再用 Apply 做 β-归约或重构
return Apply (
Subst (vv, yy, context, Left (xx)),
Subst (vv, yy, context, Right (xx))
);
}
else if (aux > 2) {
// 变量或常量：
// 若 aux == vv，则替换为 yy；否则若 aux>vv，就减去偏移 context
return aux == vv
? yy
: term - (aux > vv ? context : 0);
}
else {
// 抽象节点：aux==0 为 λ，aux==1 为 Π
// 构造新配对 (aux, (子项1', 子项2'))
// 对右子树的 yy 先做 Lift 以调整绑定深度
return Pair (
aux,
Pair (
Subst (vv, yy, context, Left (xx)),
Subst (vv+2, Lift(yy), context, Right (xx))
)
);
}
}
// —— 函数应用归一化（Apply） ——
// 若 yy 的操作码 Left(yy)==1（λ 抽象），则对其主体做一次 β-归约：Subst(4, xx, 4, body)。
// 否则重构应用节点 Pair(2, Pair(yy, xx))。
TREE Apply (TREE yy, TREE xx)
{
return Left (yy) == 1
? Subst (4, xx, 4, Right (lastRight))
: Pair (2, Pair (yy, xx));
}
// —— 比特流测试宏 ——
// 把 xx 当作待消费的比特流，每用一次 xx/=2，测试被除后最低位是否为 1。
#define MAYBE (xx /= 2) % 2 &&
// —— 主推导过程（Derive） ——
// 将整数 xx 视作一条比特流，按照 Curry–Howard 同构/类型规则生成所有可能的 λ 术语并归一化。
// 输出的(term, type, 剩余比特流, context) 四元组不断累加到全局 accumulate 中。
// 算法概览：
// 1. 递归调用 Derive(xx-1)，保证对所有小于 xx 的比特串也进行推导，确保单调增长。
// 2. 在 while 循环中，依次用 MAYBE 消费一位比特，决定是否执行对应规则：
// - APPLY (函数应用 β-归约)
// - 弱化 (Weaken，将新假设压入上下文，并提升当前项/类型)
// - Π 构造 / λ 引入
// - 变量引入 (VAR(0))
// 3. 每次规则应用后，把当前 term/type/剩余比特流/context 打包配对累积。
TREE Derive (BitStream xx)
{
Tree aux, auxTerm;
Tree context = 0, // 初始空上下文
term = 7, // STAR 常量：Pair(3,0)=7
type = 14; // BOX 常量：Pair(3,1)=14
// while 条件中先递归 Derive(xx-1)，再根据下一位比特决定是否进入循环体
while (DESCEND && Derive (xx - 1), MAYBE (1)) {
// 1) 从子推导中获取一个新项 auxTerm 及其类型 aux
auxTerm = Left (Left (Derive (xx)));
aux = Left (lastRight);
xx = Left (lastRight); // 更新剩余比特流
// 2) 若当前上下文与子推导上下文相等，则可以尝试 APPLY 或 Weaken
if (context == lastRight) {
// — APPLY：当类型符合 Π(aux, -) 时，对 term 执行函数应用
if (Left (type) == 1 && Left (lastRight) == aux && MAYBE (1)) {
type = Subst (4, auxTerm, 4, lastRight);
term = Apply (term, auxTerm);
}
// — 弱化：若 auxType 是 STAR/BOX，可引入新假设
else if ((aux / 2) && MAYBE (1)) {
context = Pair (auxTerm, context);
term = Lift (term);
type = Lift (type);
}
}
// 3) Π 构造 或 λ 引入：当上下文非空时，可根据比特选择
if (context && MAYBE (1)) {
// LHS：若 type 不支持 Π 构造，则强制做 λ 引入，并相应先对 type 做 Π 构造
Tree isLambda = (~type & 2);
if (MAYBE (isLambda)) {
type = Pair (1, Pair (Left (context), type)); // Π(Left(context), type)
}
term = Pair (isLambda | 0, Pair (Left (context), term));
context = lastRight; // 弹出已用的上下文项
}
// 4) 变量引入：若 type 是 STAR/BOX，可引入 VAR(0)
if ((type / 2) && MAYBE (1)) {
context = Pair (term, context);
type = Lift (term);
term = Pair (4, 0); // VAR(0)
}
}
// 将当前四元组打包，并加到 accumulate
return accumulate = Pair (
Pair (term, Pair (type, Pair (xx, context))),
accumulate
);
}
// —— 主函数 ——
// 对初值 99 连续调用五次 Derive，以充分“填充” accumulate。
TREE main ()
{
return Derive (Derive (Derive (Derive (Derive (99)))));
}