如何在(纯)构造演算中定义递归函数?我在那里看不到任何定点组合器。
问问题
217 次
1 回答
5
CS堆栈交换中的人们可能能够提供更多见解,但这里是一个尝试。
归纳数据类型是在具有Church 编码的构造演算中定义的:数据类型是其折叠函数的类型。最基本的例子是自然数,使用类似 Coq 的符号定义如下:
nat := forall (T : Type), T -> (T -> T) -> T
这种编码产生两件事:(1)用于构造自然数的项和(2)用于编写递归函数的运算zero : nat
符。succ : nat -> nat
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
如果我们对F := nat_rec T x f
术语x : T
和提出姿势f : T -> T
,我们会看到以下等式是有效的:
F zero = x
F (succ n) = f (F n)
因此,nat_rec
允许我们通过指定x
基本情况的返回值和f
处理递归调用值的函数来定义递归函数。请注意,这不允许我们在自然数上定义任意递归函数,而只能在其参数的前身上执行递归调用的那些函数。允许任意递归将为偏函数打开大门,这将损害微积分的可靠性。
这个例子可以推广到其他归纳数据类型。例如,我们可以将自然数列表的类型定义为它们的右折叠函数的类型:
list_nat := forall T, T -> (nat -> T -> T) -> T
于 2018-11-07T19:28:32.323 回答