唯一性规则

在类型论中, 唯一性规则是指一类给出相等关系的推导规则, 这些规则描述某个类型的消去规则后接构造规则等于什么也不做. 例如对函数类型, 它便对应如下相等 (为了简便, 省略了语境和相继式的语法):$$\frac{f:A\to B}{f=(\lambda x.fx):A\to B}$$而对于二元的积类型, 则是$$\frac{t:A\times B}{t=⟨t.1,t.2⟩:A\times B}$$

唯一性规则又叫 $\mathbf{\eta }$ 规则, 给出的等式又叫 $\mathbf{\eta }$-相等.

唯一性规则的形式总是某变量 (较小) 等于某表达式 (较大) 的形式, 站在重写系统的视角下该规则有两种实现方式:

•	从小到大: 这叫做 $\eta$-展开, 展开后给出 $\eta$-长形式, 易于实现但容易增大表达式体积,
•	从大到小: 这叫做 $\eta$-规约, 这实现起来非常不自然, 但对于内存是更好的.

部分形成规则对应的唯一性规则极度复杂, 因此往往不采用.

归纳类型的唯一性规则

对于归纳类型, 其唯一性规则往往有多个版本, 在递归的情况下, 最一般的唯一性规则往往无法写出. 这里列举一些可能的唯一性规则, 并用自然数类型举例:

•	对易变换: $$\frac{x:\mathbb{N}⊢f:X}{x:\mathbb{N}⊢f={\mathrm{rec}}_{\mathbb{N}}(f[x:=0],\lambda n.f[x:=sn],x):X}$$该规则没有对应的 $\eta$-长形式, 意味着它可以无尽地展开, 而它的规约需要从消去规则中萃取出函数 $f$, 更加荒诞. 但该规则可以作为定理提供: $$(f:\mathbb{N}\to X)\to (m:\mathbb{N})\to {\mathrm{Id}}_X(fm,{\mathrm{rec}}_{\mathbb{N}}(f0,\lambda n.f(sn),m))$$可借助对 $m$ 归纳证明之.
•	自展开: $$\frac{n:\mathbb{N}}{n={\mathrm{rec}}_{\mathbb{N}}(0,s,n):\mathbb{N}}$$该规则更符合先消去再构造的基本规律, 但不太容易看出: 乍看之下消去规则 ${\mathrm{rec}}_{\mathbb{N}}$ 在外, 构造规则 $0,s$ 在内, 但它的正确阅读顺序是我们先对 $n$ 使用 ${\mathrm{rec}}_{\mathbb{N}}$ 消去, 再在分支处理上使用 $0,s$. 可借助对 $n$ 归纳证明之.
•	完整的唯一性规则: (...)

1相关概念

•	唯一性规则对应逻辑学中恒同规则是可容许规则的证明. 例如蕴涵的恒同规则可容许证明如下, 其中从上到下第一步是蕴涵的右规则 (可以类比为相继式演算版本的肯定前件), 第二步则是蕴涵的左规则: $$\frac{\frac{A⊢AB⊢B}{A\to B,A⊢B}}{A\to B⊢A\to B}$$带上证明对象便是: $$\frac{\frac{x:A⊢x:AB⊢B\text{(变量随后被代换掉, 忽略)}}{f:A\to B,x:A⊢fx:B}}{f:A\to B⊢f:A\to B}$$注意其中中间那一步在省略一些细节后形如 $x:A⊢fx:B$, 对应了唯一性规则.

•	与之对称的概念是计算规则.

术语翻译

唯一性规则 • 英文 uniqueness rule

$\eta$-长形式 • 英文 $\eta$-long form

对易变换 • 英文 commuting conversion

自展开 • 英文 identity expansion