誘導型

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

型理論では、定数とその型の項を作成する関数から新しい型を作成する機能がある場合、システムには誘導型があります。この機能は、プログラミング言語のデータ構造と同様の役割を果たし、型理論で数値関係ツリーなどの概念を追加できるようにします名前が示すように、誘導型は自己参照型にすることができますが、通常は構造的再帰を許可する方法でのみ使用できます。

標準的な例は、ペアノのエンコーディングを使用して自然数をエンコードすることです。

 帰納的 NAT   タイプ := 
   |  0   nat 
   |  S   nat-  >  nat 

ここで、自然数は定数「0」から、または関数「S」を別の自然数に適用することによって作成されます。「S」は、数値に1を加算することを表す後継関数です。したがって、「0」は0、「S 0」は1、「S(S 0)」は2、「S(S(S 0))」は3というようになります。

それらの導入以来、帰納法は、より多くの構造をエンコードするように拡張されましたが、それでも述語であり、構造の再帰をサポートしています。

消去

誘導型には通常、それらの特性を証明する関数が付属しています。したがって、「nat」には次のものが含まれる場合があります。

 nat_elim   forall  P   nat-  >  Prop  P  0  ->  forall  n  P  n-  >  P  S  n )) ->  forall  n  P  n ))。

これは、タイプ「nat」の構造再帰に期待される関数です。

実装

W型とM型

W型は直観主義型理論(ITT)において十分に根拠のある型です。[1]自然数、リスト、二分木、およびその他の「ツリー型」データ型を一般化します。Uを宇宙としますタイプA  :U従属ファミリB  :AUが与えられると、Wタイプを形成できます。 タイプAは、定義されている帰納型の(潜在的に無限の)コンストラクターの「ラベル」と考えることができますが、Bは、各コンストラクターの(潜在的に無限の)アリティを示します。Wタイプ(またはMタイプ)は、要素a  :Aでラベル付けされたノードを持ち、aでラベル付けされたノードB a -manyである、十分に根拠のある(または十分に根拠のない)ツリーとして理解することもできます。サブツリー。[2]各W型は、いわゆる多項式関手の始代数と同型です。

0、1、2などを住民1 1  :1、1 2、2 2 2など有限型とします自然数をW型と定義することができます。

f  :2Uは、 f 1 2)= 0(引数をとらないゼロのコンストラクターを表す)およびf(2 2)= 1(1つの引数をとる後継関数を表す)によって定義されます。

タイプA  :Uのリストを次のように定義できます。どこ

11は1唯一の住民ですの値空のリストのコンストラクターに対応しますが、別のリストの先頭に を追加するコンストラクターに対応します。

ジェネリックW型の要素のコンストラクタータイプがあります

このルールは、自然演繹の証明 のスタイルで書くこともできます。

Wタイプの除去規則は、木の構造的帰納法と同様に機能します。もし、プロパティが(タイプとしての提案の解釈の下で)いつでも特定のツリーのすべてのサブツリーを保持し、そのツリーも保持します。次に、すべてのツリーを保持します。

拡張型理論では、W型(またはM型)は、同型写像まで、多項式関手の始代数(または最終余代数)として定義できますこの場合、初期性(res。finality)のプロパティは、適切な帰納法の原則に直接対応します。[3]一価公理を用いた内包型理論では、この対応はホモトピー(命題的等式)まで成り立つ。[4] [5] [6]

MタイプはWタイプのデュアルであり、ストリームなどの共誘導(潜在的に無限)データ表します。[7] MタイプはWタイプから派生させることができます。[8]

相互帰納的定義

この手法により相互に依存する複数のタイプの定義が可能になります。たとえば、 Coqで相互に誘導する2つの型を使用して、自然数に2つのパリティ述語を定義します。

帰納的 偶数  nat-  >  Prop  := 
  |  zero_is_even   偶数 O 
  |  S_of_odd_is_even   forall  n nat  odd  n-  >  even  S  n ))
with  odd   nat-  >  Prop  := 
  |  S_of_even_is_odd   forall  n nat  even  n-  >  odd  S  n ))。

帰納法-再帰

帰納法-再帰はITTの限界の研究として始まりました。見つかったら、制限は新しい誘導型を定義できるルールに変わりました。これらのタイプは、両方が同時に定義されている限り、関数とタイプ上の関数に依存する可能性があります。

ユニバースタイプは、帰納法-再帰を使用して定義できます。

誘導-誘導

誘導-誘導により、タイプとタイプのファミリーを同時に定義できます。つまり、タイプAとタイプのファミリー

高誘導型

これはホモトピー型理論(HoTT)の現在の研究分野です。HoTTは、IDタイプ(同等性)がITTと異なります。より高い誘導型は、その型の要素を作成する定数と関数を使用して新しい型を定義するだけでなく、それらに関連するID型の新しいインスタンスも定義します。

簡単な例は、2つのコンストラクター(ベースポイント)で定義され た円タイプです。

ベース :サークル

とループ。

ループ :ベース=ベース

アイデンティティタイプの新しいコンストラクターの存在により、サークルはより帰納的なタイプになります。

も参照してください

  • 共誘導は、型理論において(効果的に)無限の構造を可能にします。

参考文献

  1. ^ Martin-Löf、Per(1984)。直観主義型理論 (PDF)サンビン、ジョバンニ。ナポリ:ビブリオポリス。ISBN 8870881059OCLC12731401 _
  2. ^ アーレンス、ベネディクト; カプリオッティ、パオロ; Spadotti、Régis(2015-04-12)。ホモトピー型理論における反基礎集合論Leibniz International Proceedings in Informatics(LIPIcs)。38. pp。17–30。arXiv1504.02949土井10.4230 /LIPIcs.TLCA.2015.17ISBN 9783939897873S2CID15020752 _
  3. ^ Dybjer、Peter(1997)。「Martin-Löfの型理論におけるウェルオーダーによって帰納的に定義された集合を表す」理論計算機科学176(1–2):329–335。土井10.1016 / s0304-3975(96)00145-4
  4. ^ Awodey、スティーブ; ガンビーノ、ニコラ; Sojakova、Kristina(2012-01-18)。「ホモトピー型理論における誘導型」。arXiv1201.3898 [ math.LO ]。
  5. ^ アーレンス、ベネディクト; カプリオッティ、パオロ; Spadotti、Régis(2015-04-12)。ホモトピー型理論における反基礎集合論Leibniz International Proceedings in Informatics(LIPIcs)。38. pp。17–30。arXiv1504.02949土井10.4230 /LIPIcs.TLCA.2015.17ISBN 9783939897873S2CID15020752 _
  6. ^ Awodey、スティーブ; ガンビーノ、ニコラ; Sojakova、Kristina(2015-04-21)。「ホモトピー-型理論における始代数」。arXiv1504.05531 [ math.LO ]。
  7. ^ van den Berg、Benno; マルキ、フェデリコデ(2007)。「カテゴリー内の根拠のない木」。純粋な応用論理の年報146(1):40–59。arXivmath / 0409158土井10.1016 /j.apal.2006.12.001S2CID360990_ 
  8. ^ アボット、マイケル; Altenkirch、Thorsten; ニール・ガニ(2005)「コンテナ:厳密に正の型を構築する」。理論計算機科学342(1):3–27。土井10.1016 /j.tcs.2005.06.002

外部リンク