χ 语言和无类型 lambda 演算

在 Chalmers 的可计算性理论课上学了一个叫 χ 的语言，并在上面进行了许多可计算性的研究。

χ 语言中包含了如下运算：

• 变量（x）
• 构造（Cons(x, xs), C(x), D()）
• 递归（rec x = x）
• lambda 表达式（λx.x）
• 模式匹配（case x of { C(x) -> x }）
• 应用（f x）

其中的 变量、lambda 表达式 和 应用 在无类型 lambda 演算中显然是存在的，问题是如何在无类型 lambda 演算中实现 递归、构造 和 模式匹配。

递归

lambda 表达式中函数是没有名字的，无法直接进行递归调用。

为了解决这个问题，我们可以这样思考，以阶乘函数为例：

function factorial(n) {
    return n == 0 ? 1 : n * factorial(n - 1);
}

Instead of 调用 factorial，我们要求用户传入factorial这个函数：

function fact(f) {
    return (n) => n == 0 ? 1 : n * f(f)(n - 1);
}
const factorial = fact(fact);

这样，至少 factorial 中已经不包含对 factorial 这个函数的调用了。

我们再看几个例子：

function sum(f) {
    return (n) => {
        return n == 0 ? 1 : n + f(f)(n - 1);
    }
}
const factorial = sum(sum);

function fib(f) {
    return (n) => {
        if (n == 0) {
            return 0;
        } else if (n == 1) {
            return 1;
        } else {
            return f(f)(n-1) + f(f)(n-2)
        }
    }
}
const fibonacci = fib(fib);

可见，两个普遍的 pattern 是：

• 创建一个新的函数，这个函数接受一个函数 f ，返回一个和原来的递归函数实现相同，唯一的区别是把原本的函数名改成 f(f) 的新函数。
• 最终的函数是这个生成的函数应用到其自身的结果。

我们可以把这部分提取出来：

function selfApply(f) {
    return f(f);
}

const factorial = selfApply((f) => {
    return (n) => n == 0 ? 1 : n * selfApply(f)(n - 1);
});

继续把这里的业务逻辑抽象出来：

function selfApply(f) {
    return f(f);
}

function rec(h) {
    // since js is strict evaluated, we cannot use
    // selfApply(f => h(selfApply(f)));
    return selfApply(f => h((n) => selfApply(f)(n)));
}

const fact = rec((g) => {
    return (n) => n == 0 ? 1 : n * g(n - 1);
});

这里的 rec 就是大名鼎鼎的 Y 组合子，用 lambda 表达式写作：

$$ Y := \lambda h . (\lambda f . h\ (f\ f)) (\lambda f . h\ (f\ f)) $$

其中的 h 应当 “形如”¹ λg.λparam.exp。

构造 & case

如果你学过范畴论，可能你会知道什么是 泛性质，即某个东西的定义是由这个东西如何被使用定义的。

相似地，我们可以用接受一个 （“使用”这个构造 的 lambda 表达式） 的 lambda 表达式来定义构造，而 case 则体现为这个 lambda 表达式的应用。

例如：

const pair = (f) => (x, y) => f(x, y);

const true = (a) => (b) => a;
const false = (a) => (b) => b;

const zero = (f) => (x) => x;
const suc = (n) => (f) => (x) => f(n(f)(x));

这个手段称为邱奇编码²，基本上，如果你事先知道了一个 构造子和谁进行 matching，那么就一定可以将其编码到 lambda 表达式中。

注意必须能够知道要和哪些构造子一起 matching，才能将其编码。

或者说，你无法“事先”将构造子编码到 lambda 表达式中，并在任何情况下使用。

例如，C(x) 和 D(x) 在不知道他们如何被matching的情况下，完全无法区别。