查看“︁Loader 数”︁的源代码

'''Loader 数'''是 Ralph Loader 的 C 语言程序 '''Loader.c''' 的输出 <math>D^5(99)</math>，它在 2001 年的 [[Bignum Bakeoff]] 比赛（用不超过 512 字的代码生成尽可能大的有限整数）中获得第一名。

其中 D 函数的强度取决于 Huet-Coquand 构造演算（CoC）的证明论强度，其增长率达到了 <math>{\rm PTO}(Z_\omega)</math>。迄今为止，它仍然是最强的可计算函数之一。

=== 定义 ===
Loader.c 的源代码如下：<syntaxhighlight lang="c" line="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
</syntaxhighlight>此外，Loader 还给出了可读性更高的版本（我们使用中文注释）：<syntaxhighlight lang="c">
//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)))));
}
</syntaxhighlight>{{默认排序:相关问题}}
[[分类:记号]]