coq - 教会数字

Question

Poly 模块中有 4 个与教会数字相关的练习:

Definition cnat := forall X : Type, (X -> X) -> X -> X.

据我所知，cnat 是一个接受函数 f(x) 的函数，它是参数 x 并返回此参数的值:f(x)。

然后 0、1、2 和 3 有 4 个例子，用 Church 表示法表示。

但是如何解决呢？我知道我们必须再应用一次该功能。 cnat 返回的值将作为参数。但是如何编码呢？使用递归？

Definition succ (n : cnat) : cnat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

更新

我试过这个:

Definition succ (n : cnat) : cnat :=
match n with
| zero => one
| X f x => X f f(x) <- ?

Answer 1

请记住，Church 数字是两个参数的函数(如果您还计算类型，则为三个)。参数是函数 f 和起始值 x0。 Church 数字多次将 f 应用于 x0。 四个 f x0 将对应于 f (f (f (f x0))) 而 零 f x0 将忽略 f 并且只是 x0。

对于 n 的后继者，请记住 n 将为您应用任何函数 f n 次，因此，如果您的任务是创建一个函数，将一些 f 应用于一些 x0 n+1 次，只需将大部分工作留给教堂数字 n，给它你的 f 和 x0，然后再用一个 f 结束n 返回的结果。

您将不需要任何匹配，因为函数不是可以进行案例分析的归纳数据类型...