当需要判断两个 Term 是否在定义上相等 (definitionally equal) 时，可以使用转换检查 (conversion check)。 这是一个很符合直觉的过程：

1. 将两个 Term normalize 成 Normal Form (NF)
2. 比较两个 NF 的 Head 是否相等
3. 如果相等，那么递归地对两个 NF 的参数 (arguments) 进行此过程

但无论是处于工程角度上考虑，还是处于理论角度考虑， 将 Term normalize 成 NF 是十分昂贵的操作，甚至某些类型论并不总是保证 NF 的存在 {?}。 于是出现了一种更加 lossy 的方式：

1. 将两个 Term normalize 成 Weak Head Normal Form (WHNF)
2. 比较两个 WHNF 的 Head 是否相等
3. 如果相等，那么递归地对两个 WHNF 的参数 (arguments) 进行此过程

在上面的过程中，我们总是用到“比较”这个操作，这需要一些转换规则 (conversion rules) 来说明如何做这个比较。 这些规则可以通过不同的方法定义：基于语法的和基于类型的。

为保证符号的一致性：

符号	说明
$\Gamma \vdash u : A$	在语境 $\Gamma$ 下，Term $u$ 具有类型 $A$
$u \equiv v$	$u$ 和 $v$ 在定义上相等
$\Gamma\vdash u \equiv v : A$	在已知 $u$ 和 $v$ 在语境 $\Gamma$ 下都具有类型 $A$ 时，$u$ 和 $v$ 在定义上相等
$u[x \mapsto v]$	无需捕获 (capture-avoiding) 的替换 (substitution)，即将 $u$ 中的 $x$ 替换为 $v$

Untyped conversion

为了方便起见，先考虑基于语法的转换检查 (syntax-directed conversion，一些地方会翻译成语法制导 ，但我不喜欢这种翻译)。 一种方便的做法是从类型规则推导出转换规则：

成型规则 (formation-rule)

在 $\Sigma$ 类型的成型规则

$$\Gamma \vdash A \;\; \mathrm{type} \quad \Gamma, x : A \vdash B \;\; \mathrm{type} \over \Gamma \vdash \Sigma (x : A) \times B \;\; \mathrm{type}$$

的基础上进行一些“改写”，可以得到 $\Sigma$ 类型的转换规则

$$\Gamma \vdash A \equiv A' \quad \Gamma, x : A \vdash B \equiv B'[x' \mapsto x] \over \Gamma \vdash \Sigma (x : A) \times B \equiv \Sigma (x' : A') \times B'$$

这个“改写”从直觉上看，好像就做了两件事：

1. 复制一份 $\Sigma$ 类型的成型规则并将其中的 $x$, $A$, $B$ 等都改写成带角标的格式
2. 将这两份规则根据语法构造合并

这其实是反映了比较两个 Term 的初衷：有 $\Sigma (x : A) \times B$ 和 $\Sigma (x' : A') \times B'$ 构造的两个 Term， 他们都是被类型检查器根据 $\Sigma$ 类型的成型规则产生的 Term，即类型检查器会做如下判断：

$$\Gamma \vdash A \;\; \mathrm{type} \quad \Gamma, x : A \vdash B \;\; \mathrm{type} \over \Gamma \vdash \Sigma (x : A) \times B \;\; \mathrm{type}$$

$$\Gamma \vdash A' \;\; \mathrm{type} \quad \Gamma, x' : A' \vdash B' \;\; \mathrm{type} \over \Gamma \vdash \Sigma (x' : A') \times B' \;\; \mathrm{type}$$

那么相应地，conversion check 只要比较其中的 $A$ 和 $A'$，$B$ 和 $B'$ 是否相等即可判断两个 $\Sigma$ Term 是否相等。

消去规则 (Elimination-rule)

再看 $\Sigma$ 类型的消去规则

$$\Gamma \vdash t : \Sigma (x : A) \times B \over \Gamma \vdash t.1 : A$$

$$\Gamma \vdash t : \Sigma (x : A) \times B \over \Gamma \vdash t.2 : B[x \mapsto t.1]$$

根据上面的方法，很简单就能写出投影 (Projection) 的转换规则*

$$\Gamma \vdash t \equiv t' \quad i = i' \over \Gamma \vdash t.i \equiv t'.i'$$

构造规则 (Introduction-rule)

至此为止，从类型规则中得到转换规则的过程看似十分顺利，但是问题马上就来了：考虑 $\Sigma$ 类型的构造规则，即我们可以通过如下规则构造 $\Sigma$ 类型的实例，一般称为元组 (Tuple)：

$$\Gamma \vdash a : A \quad \Gamma, a : A \vdash b : B[x \mapsto a] \over \Gamma \vdash (a, b) : \Sigma (x : A) \times B$$

按照上面的方法，可以得到

$$\Gamma \vdash a \equiv a' \quad \Gamma, a : A \vdash b \equiv b'[x \mapsto a] \over \Gamma \vdash (a, b) \equiv (a', b')$$

这有什么问题呢？现在让我们考虑 $\Sigma$ 类型的某个特殊例子，即0-元组类型，通常也被称为 Unit 类型， 写作 $\top$ 类型。 顾名思义，这是一个没有任何元素的元组类型，它的构造规则和对应的转换规则为：

$${} \over \Gamma \vdash () : \top$$

$${} \over \Gamma \vdash () \equiv ()$$

$\top$ 类型的转换规则表示：任何两个 $\top$ 类型的实例，都应该相等。 现在看来这套规则依然很美好，但是问题马上就要出现了。现在让我们引入中性 Term 这一概念。

中性 Term (Neutral Term)

中性 Term 是指无法化简 (irreducible) 的 Term。例如引用其他变量的 Term (称为 RefTerm) 是不可化简的，比如在下面的 Aya 代码中

def fst (r : Σ A B) : A => r.1

函数体中的 r 就是一个中性 Term，因为在函数的参数为给定前，无法知道 r 具有怎样的形式。 进一步地， 对中性 Term 的消去也都是中性 Term (例如上面代码中的 r.1)，因为无法知道被消去的 Term 的形式， 所以也无法知道其第一个元素的语法构造，因此无法化简。

但是 RefTerm 的转换规则却很平凡：只要引用的变量相同，那么两个 RefTerm 就相同

$$\mathrm{identity}(a) = \mathrm{identity}(a') \over \Gamma \vdash a \equiv a'$$

其中，$\mathrm{identity}$ 用于计算被引用的变量的唯一标识符 (可以视为一种 UUID)。

至此，上述由消去规则导出的转换规则也可以处理对中性 Term 的消去的转换检查了 (之前只能处理 elim(intro) 的情况)。

$\top$ 类型和中性 Term

当有两个中性 Term 的类型为 $\top$ 时，即 $\Gamma \vdash tt : \top$， 和 $\Gamma \vdash uu : \top$ 现在我们需要将 $tt$ 和 $uu$ 进行转换检查。因此，根据上文的内容，我们需要判断：

$$\mathrm{identity}(tt) = \mathrm{identity}(uu) \over \Gamma \vdash tt \equiv uu$$

显然，$tt$ 和 $uu$ 并不是同一个变量，因此该判断显然不成立，即结论为 $tt$ 和 $uu$ 在定义上不相等。 然而根据 $\top$ 类型的转换检查规则，所有 $\top$ 类型的实例都应该在定义上相等。 但根据刚刚写出的规则，这是无法完成的！

如果能知道它们的类型，那么就可以纠正这个错误，从而给出公正的判断。 但是该公式中没有任何地方可以告诉我们 $tt$ 和 $uu$ 的类型！唉！中性 Term！

所以，我们需要一些类型信息的帮助。

$\eta$-转换

另一个问题是，在进行转换检查之前，所有的 Term 已经被 normalize 成 WHNF。但如果 Term 本身是中性 Term，那么 normalize 的过程将会被卡住 ( stuck)， 无法得到“理想的 WHNF”。同时，由于类型信息的缺失，尽管类型检查器知道 $\Gamma\vdash t : \Sigma (x : A) \times B$， 也无法在转换检查中证明 WHNF $t$ 和 WHNF $(t.1, t.2)$ 相等 (这是 intro(elim)，也被称为 $\eta$-转换)。

但如果转换检查知道 $t$ 是一个 $\Sigma$ 类型，那么就可以正当地构造 $t.1$ 和 $t.2$， 并将它们分别和 $(t.1, t.2).1$ 和 $(t.1, t.2).2$ 进行比较，从而处理 $\eta$-转换。

Typed conversion

在基于语法的基础上，引入类型作为辅助信息，从而变成基于类型的转换检查 (type-directed conversion)。 这个思想本质上是将 $u \equiv v$ 变成了 $\Gamma\vdash u \equiv v : A$，这条新的规则表明三件事：

1. $\Gamma \vdash u : A$
2. $\Gamma \vdash v : A$
3. $u \equiv v$

现在用新的方法来定义转换检查，这次以 $\Pi$ 类型为例

$$\Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x : A \vdash B \equiv B'[x' \mapsto x] \; \mathrm{type} \over \Gamma \vdash \Pi (x : A) \rightarrow B \equiv \Pi (x' : A') \rightarrow B' \; \mathrm{type}$$

$$\Gamma \vdash f \equiv f' : \Pi (x : A) \rightarrow B \quad \Gamma \vdash a \equiv a' : A \over \Gamma \vdash f \; a \equiv f' \; a' : B[x \mapsto a]$$

而构造规则的转换检查 (即$\lambda$和元组的转换检查) 可以写成

$$\Gamma, (x : A) \vdash t[x \mapsto a] \equiv t'[x \mapsto a] : B[x \mapsto a] \over \Gamma \vdash \lambda x \Rightarrow t \equiv \lambda x' \Rightarrow t' : \Pi (x : A) \rightarrow B$$

$$\Gamma \vdash a \equiv a' : A \quad \Gamma, a : A \vdash b \equiv b'[x \mapsto a] : B[x \mapsto a] \over \Gamma \vdash (a, b) \equiv (a', b') : \Sigma (x : A) \times B$$

如果定义 RefTerm 的转换检查

$$\mathrm{identity}(a) = \mathrm{identity}(a') \quad \Gamma = \Gamma', a : A \over \Gamma \vdash a \equiv a' : A$$

其中 $\Gamma = \Gamma', a : A$ 表示 $a : A$ 在语境 $\Gamma$ 中。 并考虑 $\eta$-转换，又可以将$\lambda$和元组的转换检查写为

$$\Gamma, a : A \vdash f \; a \equiv f' \; a : B[x \mapsto a] \over \Gamma \vdash f \equiv f' : \Pi (x : A) \rightarrow B$$

$$\Gamma \vdash t.1 \equiv t'.1 : A \quad \Gamma \vdash t.2 \equiv t'.2 : B[x \mapsto t.1] \over \Gamma \vdash t \equiv t' : \Sigma (x : A) \times B$$

在这个框架下，处理 $\eta$-转换就变得更加方便。

Example: $\Sigma$ 类型的 $\eta$-转换

例如 $t \equiv (t.1, t.2)$， 在类型的辅助下可以写成 $\Gamma \vdash t \equiv (t.1, t.2) : \Sigma (x : A) \times B$。 套用上述公式将 $t'$ 替换成 $(t.1, t.2)$，得到

$$\Gamma \vdash t.1 \equiv (t.1, t.2).1 : A \quad \Gamma \vdash t.2 \equiv (t.1, t.2).2 : B[x \mapsto t.1] \over \Gamma \vdash t \equiv (t.1, t.2) : \Sigma (x : A) \times B$$

将其中的 $(t.1, t.2).1$ 和 $(t.1, t.2).2$ 都 normalize 成 WHNF 即可得到

$$\Gamma \vdash t.1 \equiv t.1 : A \quad \Gamma \vdash t.2 \equiv t.2 : B[x \mapsto t.1] \over \Gamma \vdash t \equiv (t.1, t.2) : \Sigma (x : A) \times B$$

显而易见这个转换是成立的。

Example: $\Pi$ 类型的 $\eta$-转换

同样地，也有 $\Gamma \vdash f \equiv (\lambda x \Rightarrow f \; x) : \Pi (x : A) \rightarrow B$， 套用上述公式将 $f'$ 替换成 $(\lambda x \Rightarrow f \; x)$，得到

$$\Gamma, a : A \vdash f \; a \equiv (\lambda x \Rightarrow f \; x) \; a : B[x \mapsto a] \over \Gamma \vdash f \equiv (\lambda x \Rightarrow f \; x) : \Pi (x : A) \rightarrow B$$

将其中的 $(\lambda x \Rightarrow f \; x) \; a$ normalize 成 WHNF 即可得到

$$\Gamma, a : A \vdash f \; a \equiv f \; a : B[x \mapsto a] \over \Gamma \vdash f \equiv (\lambda x \Rightarrow f \; x) : \Pi (x : A) \rightarrow B$$

显而易见这个转换也是成立的。

Bidirectional conversion

如果观察两种转换检查的方式，不难发现：

• 基于语法的转换检查可以产生类型信息。如转换检查函数应用 $f \; a$ 时，产生类型信息 $B[x \mapsto a]$。
• 基于类型的转换检查可以消耗类型信息。如转换检查$\Pi$类型的 $\eta-$规则时，消耗类型信息 $\Pi (x : A) \rightarrow B$

这与双向类型检查十分类似，其 synthesis/infer 阶段产生类型信息，其 inherit/check 阶段消耗类型信息。所以转换检查可以分为两个方向：

• 当比较中性 Term 时, 推导 (synthesis/infer) 它们的类型
• 当比较 WHNF 时, 使用推导出来的类型协助 $\eta-$转换

为了建立“双向”的直觉，需要定义新的符号：

• $\Gamma\vdash u \equiv v \Rightarrow A$ 表示对 $u$ 和 $v$ 进行基于语法的转换检查，并推导得出其在语境 $\Gamma$ 下都具有类型 $A$。
• $\Gamma\vdash u \equiv v \Leftarrow A$ 表示在已知 $u$ 和 $v$ 在语境 $\Gamma$ 下都具有类型 $A$ 的情况下，进行基于类型的转换检查。

RefTerm

$$\mathrm{identity}(a) = \mathrm{identity}(a') \quad \Gamma = \Gamma', a : A \over \Gamma \vdash a \equiv a' \Rightarrow A$$

成型规则

$$\Gamma \vdash A \equiv A' \Rightarrow \mathrm{type} \quad \Gamma, x : A \vdash B \equiv B'[x' \mapsto x] \Rightarrow \mathrm{type} \over \Gamma \vdash \Pi (x : A) \rightarrow B \equiv \Pi (x' : A') \rightarrow B' \Rightarrow \mathrm{type}$$

$$\Gamma \vdash A \equiv A' \Rightarrow \mathrm{type} \quad \Gamma, x : A \vdash B \equiv B'[x' \mapsto x] \Rightarrow \mathrm{type} \over \Gamma \vdash \Sigma (x : A) \times B \equiv \Sigma (x' : A') \times B' \Rightarrow \mathrm{type}$$

消除规则

$$\Gamma \vdash f \equiv f' \Rightarrow \Pi (x : A) \rightarrow B \quad \Gamma \vdash a \equiv a' \Leftarrow A \over \Gamma \vdash f \; a \equiv f' \; a' \Rightarrow B[x \mapsto a]$$

$$\Gamma \vdash t \equiv t' \Rightarrow \Sigma (\overline{x_j : A_j}) \times B \quad i = i' \over \Gamma \vdash t.i \equiv t'.i' \Rightarrow B[\overline{x_{i-1} \mapsto t.(i-1)}]$$

其中，$i = 1, 2, \cdots, j + 1$ 并且 $j = 1, 2, \cdots$。 符号 $\overline{u}$ 表示 $u$ 可以出现至少一次。

构造规则

$$\Gamma, a : A \vdash f \; a \equiv f' \; a \Leftarrow B[x \mapsto a] \over \Gamma \vdash f \equiv f' \Leftarrow \Pi (x : A) \rightarrow B$$

$$\Gamma \vdash t.1 \equiv t'.1 \Leftarrow A \quad \Gamma \vdash t.2 \equiv t'.2 \Leftarrow B[x \mapsto t.1] \over \Gamma \vdash t \equiv t' \Leftarrow \Sigma (x : A) \times B$$

Mode Switch

类似于双向类型检查，转换检查也可以在两个方向之间切换

$$\Gamma \vdash u \equiv v \Rightarrow A \over \Gamma \vdash u \equiv v \Leftarrow A$$

规律

不难发现，上面的双向转换规则可以由双向类型检查中的类型检查规则 (Type checking rule) 和类型推导规则 (Type inference rule) 导出 (How?)。

Reference

• Norell, U. (2007). Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology. Technical Report 33D.
• aya-prover/aya-dev:DefEq.java (opens new window)
• What are the upsides and downsides of typed vs untyped conversion (opens new window)