NuPRL 中的证明 (二) -- 我从来不写递归的
图文无关。 上一篇文章 LdBeth：NuPRL 中的证明–从一到CTT 上一篇讲了 CTT 中的一些类型。dependent function, dependent product, dependent record, universe 这些因为和 ITT 的沒什么区別，就默认读者已经会了。CTT 特色的 dependent intersection 和 dependent union 因为应用范围超出了基础，就先不讲了。 General Recursion considered K Also, in some other type systems, general recursion is not expressible, and such structural recursion operations must be built in. 在 Agda 中，众所周知是用写程序來证明的，tc 过了相当于证明过了。然而 NuPRL 因为 undecidable type checking 的性质，除了程序以外，证明还包括了 tc。 比如吧，在 Agda 里要证 $x\leq x!$ ，就要先写 ! (factorial) 的定义，写完了以后，在使用 factorial 的定义之前，还要做两件事: 给它一个能过 tc 的类型声明，并且证明 termination。...