2

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

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

据我了解，cnat 是一个接受函数 f(x) 的函数，它是参数 x 并返回它的这个参数的值：f(x)。

然后有 0、1、2 和 3 的 4 个示例以教会符号表示。

但是如何解决这个问题？我知道我们必须再次应用该功能。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) <- ?
4

3 回答 3

2

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

对于 的继任者n，请记住，它将为您n应用任何函数时间，因此，如果您的任务是创建一个函数，在某些时间应用一些函数，只需将大部分工作留给教堂数字，给它您的and ，然后对返回的结果再应用一次.fnfx0 n+1nfx0fn

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

于 2019-02-18T11:25:18.453 回答
1

据我了解，cnat 是一个接受函数 f(x) 的函数，它是参数 x 并返回它的这个参数的值：f(x)。

请注意，cnat它本身不是一个函数。相反，cnat是所有此类函数的类型。还要注意cnattake的元素也可以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和作为前提。fx

如果我们应用n,X和(as ) f，我们会得到 的元素，但这并不是我们想要的，因为最终结果会再次出现。相反，我们需要在某处应用额外的时间。你能看到在哪里吗？有两种可能性。xn X f xXnf

于 2019-02-16T22:00:45.057 回答
1

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

Definition succ (n : cnat) : cnat :=
    fun (X : Type) (f : X -> X) (x : X) => f (n X f x).
于 2019-02-26T19:47:05.113 回答