构造演算中的递归

Question

如何在(纯)calculus of constructions中定义递归函数？我在那里没有看到任何定点组合器。

Answer 1

CS stack exchange中的人也许能够提供更多见解，但这是一次尝试。

归纳数据类型在结构演算中定义为 Church encoding :数据类型是其折叠函数的类型。最基本的例子是自然数，其定义如下，使用类似 Coq 的表示法:

nat := forall (T : Type), T -> (T -> T) -> T

此编码产生两件事:(1) 用于构造自然数的术语 zero : nat 和 succ : nat -> nat，以及 (2) 运算符 nat_rec 用于编写递归函数。

zero : nat
zero T x f := x

succ : nat -> nat
succ n T x f := f (n T x f)

nat_rec : forall T, T -> (T -> T) -> nat -> T
nat_rec T x f n := n T x f

如果我们对项 x : T 和 f : T -> T 提出 F := nat_rec T x f，我们会看到以下方程有效:

F zero = x
F (succ n) = f (F n)

因此，nat_rec 允许我们通过指定基本情况的返回值 x 和要处理的函数 f 来定义递归函数递归调用的值。请注意，这不允许我们在自然数上定义任意递归函数，而只能定义那些对其参数的前驱执行递归调用的函数。允许任意递归将为部分函数打开大门，这将损害微积分的可靠性。

这个例子可以推广到其他归纳数据类型。例如，我们可以将自然数列表的类型定义为其右折叠函数的类型:

list_nat := forall T, T -> (nat -> T -> T) -> T