教会数字

Question

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

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

据我所知，cnat 是一个接受函数 f(x) 的函数，它是参数 x，returns 它是这个参数的值：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

As far as I understand cnat is a function that takes a function f(x), it's argument x and returns it's value for this argument: f(x).

请注意 cnat 本身不是函数。相反，cnat 是所有此类函数的类型。另请注意，cnat 的元素也将 X 作为参数。牢记 cnat 的定义会有所帮助。

Definition succ (n: cnat): cnat.
Proof.
  unfold cnat in *. (* This changes `cnat` with its definition everywhere *)
  intros X f x.

之后，我们的目标就是X，我们有n : forall X : Type, (X -> X) -> X -> X、X、f和x作为前提。

如果我们将 n 应用于 X、f 和 x（如 n X f x），我们将得到 [=14= 的元素]，但这并不是我们想要的，因为最终结果将再次是 n。相反，我们需要在某处应用 f 额外时间。你能看到哪里吗？有两种可能。

Answer 2

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

对于 n 的后继者，请记住 n 将为您应用任何函数 f 次 n 次，因此如果您的任务是创建函数应用一些 f 在一些 x0 n+1 次，只需将大部分工作留给教会数字 n，通过给它你的 f 和 x0，然后对 n.

返回的结果再次应用 f 结束

您将不需要任何 match，因为函数不是可以根据大小写分析的归纳数据类型...

Answer 3

您可以通过以下方式为 succ 编写 Definition：

Definition succ (n : cnat) : cnat :=
    fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

教会数字

Church numerals

coq

logical-foundations