图文无关。
上一篇文章 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。
而在 NuPRL 中，写完一个定义后，类型声明和 termination proof 都是不需要的。我是不是说过 NuPRL 沒有 pattern match？那 factorial 要怎么定义呢
$\textbf{Rec}\ x! == \texttt{if}\ x=0 \rightarrow 1\ \texttt{else}\ x(x-1)!\ \texttt{fi}$
啥玩意，x 为负数的时候岂不是 non termination 了么？沒错，extrinsic type theory 就是可以为所欲为，这样的定义并不会造成什么问題。而 $\forall x :\mathbb{N}. x! \in \mathbb{N}$ 可以做为一个单独的定理证明。
又比如
mu : (ℕ → Bool) → ℕ -- Kleene's paradigmatic unbounded search function
mu f with f zero
... | true = 0
... | false = suc (mu (λ x → f (suc x)))
这样在 Agda 明显不能过 termination check 的定义，也全然大丈夫。
Recursive Type considered K
吶，没有 ADT 咋定义 List 吶
那啥，我好像沒提 inl inr 什么的，那就提一下吧。因为 Sum type 是 primitive，所以还有一个对应的的 data destructor 叫 InjCase。
$\textbf{Thm}\ \forall z : A+B.z = InjCase(z;u.inl(u);v.inr(v))$
所以在 $\mathbb{B} == Unit+Unit,\ \cdot \in Unit$ 下， $true == inl(\cdot),\ false == inr(\cdot),\ \texttt{if}\ b\ \rightarrow t\ \texttt{else}\ f\ \texttt{fi} == InjCase(b ; t; f)$
借助用来定义 recursive type 的 primitive， $List (A) == rec(X.Unit+(A\times X)),\ nil = inl(\cdot),\ Cons(a,b)==inr(
还有个 destructor
$\texttt{case}\ s: nil \rightarrow e; Cons(x,y) \rightarrow f(x,y) == InjCase(s;e;x,y.f(x,y))$
忘了提了，不过很显然
$\forall a : A, b : B.
This is (not) Y Kombinator
上面的定义用到了 recursion，对于了解 untyped lambda 的读者定然知道 Y combinator。
NuPRL 的 recursion 并非做成了 primitive，而是用 Y 定义的。
上面 factorial 的定义实质上是
$x! == Y(\lambda fx. \texttt{if}\ x=0 \rightarrow 1\ \texttt{else}\ f(x(x-1))\ \texttt{fi}, x)$