构造演算中的递归答案

【问题标题】：Recursion in the calculus of construction构造演算中的递归
【发布时间】：2018-11-07 18:45:17
【问题描述】：

如何在（纯）calculus of constructions中定义递归函数？我在那里看不到任何定点组合器。

【问题讨论】：

【解决方案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

【讨论】：

如何递归调用严格较小的参数（根据有根据的关系）？
Coq 中的有根据的递归也是根据结构递归实现的（基于有根据的关系派生的“可访问性谓词”），因此应该应用相同的技术。我实际上并不确定 Coq 的固定点是否可以通过这种方式轻松编码，因为 Coq 的终止检查器所需的原始属性似乎相当重要：它不仅适用于直接子项（在取消一个构造函数之后），还适用于传递获得的那些，甚至查看嵌套的固定点。
那么CiC中Church编码自然数的归纳原理是如何定义的？ This answer 似乎说还需要其他东西，否则类型“太大”（=包含异国情调的奇怪元素）。
@larsr 您无法为 Church 编码类型的所有元素定义归纳原则，无论是在 CoC 还是在 CiC 中。拥有归纳原则是引入归纳类型的原因之一。