1

我正在阅读CPDT并且有一个我不理解的示例：

Definition plus_rec : nat -> nat -> nat :=
  nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)).

除了fun _ : nat => nat -> nat. 我根本不明白这有什么意义，这个函数似乎返回了一个没有值的类型。

我是否误解了关于 Coq 的一些基本内容？那个 lambda 的意义是什么？

4

1 回答 1

4

让我们来看看nat_rec：

nat_rec :
  forall P : nat -> Set,
  P O ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n

它的第一个参数是 a P，给定 a nat，返回 a Set。然后你将给出集合P O的一个元素，P (S n)假设你有一个来自的元素P n，最后给你一个类型forall n, P n的元素，这意味着它可以P n为每个n你构造一个类型的元素作为输入传入（如果传递 O，它将返回P O您提供的值，否则它将通过重复应用第三个参数来构建您的结果）。

现在，让你感到困惑的是P我一直在谈论的那个 lambda。它被赋予一个nat并从中构建“返回类型”。特别是我们试图有返回类型nat_rec，即forall n : nat, P n是类型plus_rec，即nat -> nat -> nat。这可以通过P对所有 n,进行实例化来完成P n = nat -> nat。这是我们使用 lambda-term 获得的fun _ : nat => nat -> nat。

该术语忽略了输入nat（因为nat_rec对于构建其类型取决于nat它们接收的第一个参数的事物来说足够通用，但plus_rec部分应用于任何第一个参数的类型实际上并不依赖于该参数的值）。然后它只是返回nat -> nat（这是对一个操作数进行部分加法的类型：我们仍然期望 anat才能返回 sum nat）。

现在，如果你看一下nat_rec部分应用于那个有趣的 lambda 项，类型是：

nat_rec (fun _ : nat => nat -> nat) :
  (fun _ : nat => nat -> nat) O ->
  (forall n : nat, (fun _ : nat => nat -> nat) n -> (fun _ : nat => nat -> nat) (S n)) ->
  forall n : nat, (fun _ : nat => nat -> nat) n

（我刚刚回答P了(fun _ : nat => nat -> nat)。现在，这简化为：

nat_rec (fun _ : nat => nat -> nat) :
  (nat -> nat) ->
  (forall n : nat, (nat -> nat) -> (nat -> nat)) ->
  forall n : nat, (nat -> nat)

现在这肯定会令人困惑。

您应该将需要提供的第一个参数视为 to 的部分应用的plus类型O。它接收第二个操作数，并返回两者之和：

(fun m => m) (* morally, O + m *)

第二个参数是一个(n : nat)，一个函数r : nat -> nat，另一个m : nat，并且需要返回一个final nat。它是这群人中最令人困惑的。从道德上讲，r是 a P n，也就是说，给定我们的目标，“一个知道如何将 n 添加到其输入的函数”。再次从道德上讲，最后一个(nat -> nat)应该是 a P (S n)，即“知道如何将 (S n) 添加到其输入的函数”。特别是，我们将此输入命名为m。您应该能够说服自己结果应该是：

(fun _ r m => S (r m))
(* ignore n, use r (which is the "+ n" function) on m, to get (n + m), and add 1 to get (n + 1) + m *)

有了这一切，我们设法构建了函数plus。

请注意，这是一种非常容易出错的定义方式plus_rec，特别是因为您必须非常努力地记住什么是什么，否则您将不会定义您想要的函数，因为打字真的很松散（看看我们如何忽略n最的时间）。事实上，在同一函数的早期草案中存在一个错误，该函数进行了类型检查。

我相信这表明一切都在地毯下，但不要认为这是你应该定义 plus_rec 的一般方式。

最后，这很难解释，我很确定我的答案不会很清楚。随意发表评论，我将编辑答案以使事情更干净。

于 2013-01-21T05:04:13.470 回答