9

コンストラクターとは何か、およびその仕組みの原則を理解するのに苦労しています。

たとえば、Coq では、自然数を次のように定義するように教えられています。

Inductive nat : Type :=
   | O : nat
   | S : nat -> nat.

それはコンストラクターだと言われていますが、それSは正確にはどういう意味ですか?

私なら：

Check (S (S (S (S O)))).

4であり、タイプであることがわかりnatます。

これはどのように機能し、Coq はそれが を(S (S (S (S O))))表していることをどのように認識し4ますか?

これに対する答えは、Coq の非常に巧妙なバックグラウンド マジックだと思います。

4

2 に答える 2

7 
Inductive naturals : Type :=
   | Z : naturals
   | N : naturals -> naturals.

次のようなことを言っています。

  1. Z型の項ですnaturals

  2. eがタイプの項である場合naturals、N eはタイプの項ですnaturals。

  3. 適用ZまたはN自然を作成する唯一の 2 つの方法です。任意のナチュラルが与えられた場合、それが一方または他方から作成されたことがわかります。

  4. タイプのe1との2 つの項が等しいのは、それらが両方であるか、それぞれがであり、が等しい場合のみです。e2naturalsZN t1N t2t1t2

これらのルールが任意の誘導型定義にどのように一般化されるかを見ることができます。一般に、 type の任意の誘導型定義では、次のようになりtます。

  • 正しい型の引数にコンストラクターを適用すると、 type の項が生成されますt。
  • 型のすべての項は、型が定義されたときにt関連付けられたコンストラクターの 1 つを適用した結果です。t言い換えれば、タイプ の項が与えられたt場合、それは のコンストラクタの 1 つを適用した結果であると仮定できtます。
  • 型の 2 つの項tが等しいのは、それらが同じコンストラクタを同じ引数に適用した結果である場合のみです。

(補足: 型定義がZおよびの形状のコンストラクター用である場合、これらのプロパティは自然数に対するペアノの公理Nに多かれ少なかれ正確に対応します。これが、名前付きの型が Coq でこれらの形状のコンストラクターを使用して事前に定義されている理由です。自然数を表現する. このタイプは生の形を操作するのは非常にすぐに疲れてしまうので特別な扱いを受けるが, 特別な扱いは便宜上あるだけである.)nat

于 2011-02-23T12:18:50.910 に答える
0

型理論では、（型）コンストラクターは既存の型から新しい型を構築する方法にすぎません（http://en.wikipedia.org/wiki/Type_constructor）。

natの帰納的定義では、Sはコンストラクターです。これは（署名を見ると）natを受け取り、別のnatを生成するためです。

たとえば、natのペアの型コンストラクタは次のようになります。

Inductive pair : Type := P: nat->nat->pair.

Check P (S (O)) (S(S(O))).
于 2011-02-23T18:18:48.100 に答える