时间戳

首页 > 解决方案 > 构造演算中的递归

recursion - 构造演算中的递归

问题描述

如何在（纯）构造演算中定义递归函数？我在那里看不到任何定点组合器。

标签： recursionfunctional-programmingcoqlambda-calculustyped-lambda-calculus

解决方案

CS堆栈交换中的人们可能能够提供更多见解，但这里是一个尝试。

归纳数据类型是在具有Church 编码的构造演算中定义的：数据类型是其折叠函数的类型。最基本的例子是自然数，使用类似 Coq 的符号定义如下：

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

这种编码产生两件事：（1）用于构造自然数的项和（2）用于编写递归函数的运算zero : nat符。succ : nat -> natnat_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

推荐阅读