自然数 (类型论)

自然数类型是自然数在类型论中的类比, 它在简单类型论和依值类型论里都可以定义, 但规则稍有不同.

1类型规则

沿用自然数的记号, 自然数类型记作 $\mathbb{N}$.

构造规则

以下规则模仿 Peano 公理和归纳法.

$$\Gamma ⊢0:\mathbb{N}\frac{\Gamma ⊢u:\mathbb{N}}{\Gamma ⊢s(u):\mathbb{N}}$$

不引起混淆的情况下, 可以将 $s(u)$ 写作 $su$.

注 1.1. 此处刻意避免了将后继操作定义为一个具有函数类型的操作符, 这是为了确保函数类型的典范形式只有它的构造规则. 在实际使用时, 可以使用 $\lambda x.s(x)$ 作为后继操作的函数形式.

常常使用 $1$ 表示 $s0$, $2$ 表示 $s(s0)$, 以此类推, 但 $1$ 也表示单位类型, 因此最好不要在两者同时出现的时候使用这种简写.

可以直接将 $\mathbb{N}$ 视为由如上两构造子生成的归纳类型并自动得到消去规则, 也可以单独给出消去规则.

消去规则

简单类型的消去规则:

$$\frac{\Gamma ⊢a:A\Gamma ⊢b:\mathbb{N}\to A\to A\Gamma ⊢u:\mathbb{N}}{\Gamma ⊢{\mathrm{rec}}_{\mathbb{N}}(a,b,u):A}$$

简单类型的计算规则:

$$\begin{gathered} {\mathrm{rec}}_{\mathbb{N}}(a,b,0)=a:A \\ {\mathrm{rec}}_{\mathbb{N}}(a,b,su)=b(u,{\mathrm{rec}}_{\mathbb{N}}(a,b,u)):A \end{gathered}$$

依值类型论中的消去规则需要用到宇宙:

$$\frac{\Gamma ⊢P:\mathbb{N}\to \mathcal{U}\Gamma ⊢a:P(0)\Gamma ⊢b:{\prod }_{n:\mathbb{N}}P(n)\to P(sn)\Gamma ⊢u:\mathbb{N}}{\Gamma ⊢{\mathrm{rec}}_{\mathbb{N}}(P,a,b,u):P(u)}$$

计算规则基本一致, 不再赘述.

自然数类型的唯一性规则十分复杂, 参见该词条.

2局限

加法

使用以上任意一种方式定义的 ${\mathrm{rec}}_{\mathbb{N}}$ 都不能定义出二元函数 $+:\mathbb{N}\to \mathbb{N}\to \mathbb{N}$ 使得对于任意 $\Gamma ⊢a:\mathbb{N}$ 同时满足如下两条计算规则:

$$\begin{array}{rl}\Gamma ⊢a+0& =0:\mathbb{N}\\ \Gamma ⊢0+a& =0:\mathbb{N}\end{array}$$

使用一些模式匹配的变种可以解决该问题.

3性质

定理 3.1. 对于任意 $n:\mathbb{N}$, 如下命题不成立: $$\mathrm{Id}(0,sn)$$换言之, 如下命题成立: $$\mathrm{Id}(0,sn)\to \varnothing$$

相关定义见相等类型、单位类型和空类型, 注意 $1$ 是单位类型而不是自然数 $s(0)$.

证明.

证明. 假设存在 $p:\mathrm{Id}(0,sn)$, 定义$$\begin{array}{rl}f& :\mathbb{N}\to \mathcal{U}\\ f& (n):={\mathrm{rec}}_{\mathbb{N}}(1,\lambda m.\lambda x.\varnothing ,n)\end{array}$$注意 $f(0)=1,f(sn)=\varnothing$. 根据相等类型的性质, 可以从 $p$ 得到 $q:\mathrm{Id}(f(0),f(sn))$, 即 $q:\mathrm{Id}(1,\varnothing )$. 再次根据相等类型的性质, 可以从 $q$ 推出如下函数存在: $$g:1\to \varnothing$$应用该函数即可得到空类型的实例 $g(\star ):\varnothing$.

$\square$

4范畴语义

$\mathbb{N}$ 可以定义为一种归纳类型, 它对应的自函子是:

$$F(X)=1+X$$

在这个视角下, ${\mathrm{rec}}_{\mathbb{N}}$ 就对应了这个始代数诱导的唯一态射, 如下图所示:

$$1\mathbb{N}\mathbb{N}AA0as{\mathrm{rec}}_{\mathbb{N}}{\mathrm{rec}}_{\mathbb{N}}b$$

上图也可以画成自环的形式:

不过一般不这么画, 因为此时 “图表交换” 的定义不明确. 以该交换图作为万有性质定义的对象 $\mathbb{N}$ 叫做自然数对象.