1

CPDTを読んでいますが、理解できない例が 1 つあります。

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 について何か根本的なことを誤解していますか? そのラムダの重要性は何ですか?

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

その最初の引数は、Pが与えられるとnat、を返すaSetです。次に、セットの要素と、からの要素があると仮定しP Oたセットの要素を指定します。最後に、すべてのタイプの要素が返されます。これは、すべてのユーザーに対してタイプの要素を作成できることを意味します。入力として渡します（Oを渡すと、指定したものが返されます。それ以外の場合は、3番目の引数を繰り返し適用して結果を作成します）。P (S n)P nforall n, P nP nnP O

さて、あなたを混乱させているそのラムダは、P私が話していることです。それは与えられ、natそれから「リターンタイプ」を構築します。nat_rec特に、リターンタイプを、つまりforall n : nat, P n、のタイプにしようとしていplus_recますnat -> nat -> nat。Pこれは、すべてのnについて、が次のようにインスタンス化することで実行できますP n = nat -> nat。これは、ラムダ項を使用して取得したものfun _ : nat => nat -> natです。

この用語は入力を無視しますnat（タイプが最初に受け取るnat_recものに依存するものを構築するのに十分一般的ですが、最初の引数に部分的に適用されるタイプは実際にはその引数の値に依存しないため）。次に、それはただ戻ります（これは、1つのオペランドへの加算の部分適用のタイプです。合計を返す前に、まだaを期待しています）。natplus_recnat -> natnatnat

ここで、nat_recその面白いラムダ用語に部分的に適用されているものを見ると、タイプは次のとおりです。

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)

今、これは間違いなく混乱するはずです。

与える必要のある最初の引数は、plustoの部分適用のタイプと考える必要がありますO。2番目のオペランドを受け取り、2つの合計を返します。

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

2番目の引数には(n : nat)、関数r : nat -> nat、別の、が与えられm : nat、finalを返す必要がありますnat。それは束の中で最も混乱しています。道徳的にrはP n、つまり、「入力にnを追加する方法を知っている関数」という目標が与えられています。道徳的にも、最後は、「入力に（S n）を追加する方法を知っている関数」である(nat -> nat)必要があります。P (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 に答える