Lambda 编码

在 $λ$ 演算中, $λ$ 编码是 Church 编码、Scott 编码和 Parigot 编码等借助 $λ$ 表达式表示复杂数据结构的手法的统称.

$λ$ 编码所需的类型论至少需要 F 系统或依值类型论的强度, 在无类型 $λ$ 演算中最为方便.

$λ$ 编码的表达能力极其强大, 虽然在计算机科学的研究中一般仅讨论它对自然数和一些有限集合的编码, 但它实际上可以通过 Leibniz 相等原则编码相等类型, 通过命题宇宙编码逻辑截断类型, 等等.

1基本思想

类型论中的类型一般由构造规则、消去规则和计算规则定义, 所谓 $λ$ 编码就是借助 $λ$ 表达式去 “实现” 出这些规则.

考虑自然数类型, 它的消去规则 $rec_{N} (a, b, n)$ 本质上就是将自然数 $n$ 转化为如下表达式:

$一共 n 个 b b (b (b (\dots (a))))$

那么, 直接将自然数 $n$ 定义为

$λa . λb . 一共 n 个 b b (b (b (\dots (a))))$

再使用函数应用去定义消去规则, 即可在不直接引入自然数类型的情况下使用自然数:

$rec_{N} rec_{N} : A \to (A \to A) \to N \to A (a, b, n) := n a b$

注意 $n$ 是自然数, 那么它按照上面的定义理应是一个二元函数, 因此我们可以直接将参数 $a, b$ 应用上去.

以上便是 Church 编码自然数的思路. 其它种类的编码稍有不同, 但大体思路都是一致的. 任何使用自然数的消去规则定义的操作都可以很容易地翻译到 Church 自然数, 例如加法和乘法:

$m + n m \times n := λa . λb . m b (n b a) := λa . λb . m (n b) a$

在 F 系统里, 我们可以赋予这种自然数以类型:

$N := \forall α . α \to (α \to α) \to α$

单位类型只有一个元素, 因此单独讨论它的实例不太有意义, 但如果限定到 F 系统中, 可以定义出这个类型:

$1 := \forall α . (α \to α)$

该类型在 F 系统中唯一可以写出的实例是 $λ x . x$ , 对应单位类型的构造规则.

在 Church 自然数中介绍的自然数极难定义减法. 特别的, 它很难定义自然数的前驱操作, 而减法依赖这个操作.

(..)

在 Martin-Löf 类型论、构造演算等大多数能表达相等类型的类型论中, 虽然可以轻易地定义自然数类型和 Church 编码的自然数之间的转换函数, 却不能证明这两个函数互逆, 这是因为这些类型论不能在内部证明参数性.

这个问题的最简单情况可以直接考虑单位类型中的编码. 为避免符号和自然数混淆, 记 $⊤_{λ} = \forall α . (α \to α)$ 、 $⊤$ 为标准的单位类型、如下函数为两者之间的转换函数, 它们直接忽略参数、返回目标类型的唯一实例:

$f : ⊤_{λ}_g : ⊤_\to ⊤ \mapsto ⋆ \to ⊤_{λ} \mapsto λ α . λ x . x$

两者互逆的命题如下:

$p q : Π_{a : ⊤} Id (f (g (a)), a) : Π_{a : ⊤_{λ}} Id (g (f (a)), a)$

其中 $p$ 非常容易证明, 但 $q$ 化简后会变成如下命题:

$q : Π_{a : ⊤_{λ}} Id (λ α . λ x . x, a)$

这个命题就是参数性的特殊情况, 需要非常特殊的类型论才能从类型论内部构造出来.

注 2.1. F 系统的参数性是元理论层面的定理, 它甚至不能表达相等类型, 从而无法证明如上命题. 但是我们可以认为上面的命题是 F 系统的元定理.

术语翻译

$λ$ 编码 • 英文 $λ$ -encoding