依存型

コンピュータサイエンスと論理学において、依存型とは定義が値に依存する型のことです。これは型理論と型システムの重複する特徴です。直観主義型理論では、依存型は「すべての」や「存在する」といった論理の量化子を符号化するために使用されます。Agda 、ATS、Rocq（旧称Coq）、F*、Epigram、Idris、Leanなどの関数型プログラミング言語では、依存型はプログラマが実装可能な範囲をさらに限定する型を割り当てることを可能にするため、バグの削減に役立ちます 。

依存型の一般的な例としては、依存関数と依存ペアの2つがあります。依存関数の戻り値の型は、引数の1つの値（型だけでなく）に依存する場合があります。たとえば、正の整数を取る関数は長さ の配列を返すことがあります。この場合、配列の長さは配列の型の一部です。（これは、型を引数として含む多態性やジェネリックプログラミングとは異なることに注意してください。）依存ペアには2番目の値があり、その型は最初の値に依存します。配列の例で言えば、依存ペアは、配列とその長さを型安全にペアにするために使用できます。 n{\displaystyle n}n{\displaystyle n}

依存型は型システムの複雑さを増大させます。プログラム内の依存型の等価性を判定するには計算が必要になる場合があります。依存型に任意の値が許容される場合、型の等価性の判定には、任意の2つのプログラムが同じ結果を生成するかどうかの判定が含まれる可能性があります。したがって、型チェックの決定可能性は、与えられた型理論における等価性の意味論、つまり型理論が内包的か外延的かに依存する可能性があります。[ 1 ]

歴史

1934年、ハスケル・カリーは、型付きラムダ計算とその組み合わせ論理における型が、命題論理における公理と同じパターンに従っていることに気づきました。さらに、この論理におけるあらゆる証明に対して、プログラミング言語には対応する関数（項）が存在することを示しました。カリーの例の一つは、単純型付きラムダ計算と直観主義論理との対応でした。[ 2 ]

述語論理は命題論理の拡張であり、量指定子が追加されたものである。ハワードとデ・ブリュインは、ラムダ計算を拡張し、このより強力な論理に適合させ、「すべての場合」に対応する従属関数と、「存在する」に対応する従属ペアの型を作成した。[ 3 ]

このこととハワードの他の研究により、命題を型として扱うことはカリー・ハワード対応として知られています。

正式な定義

依存型理論において、依存型とは、値に応じて仕様が変化する型であり、インデックス付き集合族に類似したものとみなすことができます。を型のユニバースとし、を の型であると書きます。型 の項を と書きます。上の依存型族はと書き、族の各項に型 を割り当てることを意味します。したがって、およびが与えられた場合、式 は特定の値 に依存する型を表します。標準的な用語では、これは型が に応じて変化すると説明されます。 あなた{\displaystyle {\mathcal {U}}}あ:あなた{\displaystyle A:{\mathcal {U}}}あ{\displaystyle A}あなた{\displaystyle {\mathcal {U}}}1つの{\displaystyle a}あ{\displaystyle A}1つの:あ{\displaystyle a:A}あ{\displaystyle A}B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}1つの:あ{\displaystyle a:A}B（1つの）:あなた{\displaystyle B(a):{\mathcal {U}}}あ:あなた{\displaystyle A:{\mathcal {U}}}B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}B（1つの）{\displaystyle B(a)}1つの{\displaystyle a}B（1つの）{\displaystyle B(a)}1つの{\displaystyle a}

Π型

戻り値の型が引数によって変化する関数（つまり、固定の共線領域がない関数）は従属関数と呼ばれ、この関数の型は従属積型、π型（Π型）、または従属関数型と呼ばれます。[ 4 ]型の族から、項が項を取り、項を返す関数である従属関数の型を構築できます。この例では、従属関数の型は通常、またはと記述されます。 B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}∏×:あB（×）{\textstyle \prod _{x:A}B(x)}1つの:あ{\displaystyle a:A}B（1つの）{\displaystyle B(a)}∏×:あB（×）{\textstyle \prod _{x:A}B(x)}∏（×:あ）B（×）{\textstyle \prod {(x:A)}B(x)}

が定数関数である場合、対応する従属積型 は通常の関数型と等価である。つまり、が に依存しない場合、は と判断的に等しい。 B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}∏×:あB{\textstyle \prod _{x:A}B}あ→B{\displaystyle A\to B}B{\displaystyle B}×{\displaystyle x}

「Π型」という名前は、これらが型の直積として見ることができるという考え方に由来しています。Π型は、全称量指定子のモデルとしても理解できます。

例えば、実数のn組に対して と書くと、 は自然数nを与えるとサイズnの実数の組を返す関数の型になります。通常の関数空間は、範囲型が実際には入力に依存しない場合の特別なケースとして現れます。例えば は自然数から実数への関数の型であり、型付きラムダ計算では と書きます。 ベック⁡（R、n）{\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}∏n:北ベック⁡（R、n）{\textstyle \prod _{n:\mathbb {N} }\operatorname {Vec} (\mathbb {R} ,n)}∏n:北R{\textstyle \prod _{n:\mathbb {N} }{\mathbb {R} }}北→R{\displaystyle \mathbb {N} \to \mathbb {R} }

より具体的な例として、を 0 から 255 までの符号なし整数 (8 ビットまたは 1 バイトに収まるもの) の型とし、を とすると、は の積になります。 あ{\displaystyle A}B（1つの）＝X1つの{\displaystyle B(a)=X_{a}}1つの:あ{\displaystyle a:A}∏×:あB（×）{\textstyle \prod _{x:A}B(x)}X0×X1×X2×…×X253×X254×X255{\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}

Σ型

従属積型の双対は、従属ペア型、従属和型、シグマ型、または（紛らわしいですが）従属積型です 。[ 4 ]シグマ型は存在量化子としても理解できます。上記の例を続けると、型の宇宙に型と型の族がある場合、従属ペア型が存在します。（代替表記はΠ型と同様です。） あなた{\displaystyle {\mathcal {U}}}あ:あなた{\displaystyle A:{\mathcal {U}}}B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}∑×:あB（×）{\textstyle \sum _{x:A}B(x)}

従属ペア型は、第2項の型が第1項の値に依存する順序付きペアの概念を捉えたものである。もしならば、となり、 となる。もし が定数関数ならば、従属ペア型は積型、つまり通常の直積となる（と判断的に等しい）。[ 4 ]（1つの、b）:∑×:あB（×）、{\textstyle (a,b):\sum _{x:A}B(x),}1つの:あ{\displaystyle a:A}b:B（1つの）{\displaystyle b:B(a)}B{\displaystyle B}あ×B{\displaystyle A\times B}

より具体的な例として、 を再び 0 から 255 までの符号なし整数の型 とし、 を再び256 のより任意のに対して と等しくすると、 は合計 になります。 あ{\displaystyle A}B（1つの）{\displaystyle B(a)}X1つの{\displaystyle X_{a}}X1つの{\displaystyle X_{a}}∑×:あB（×）{\textstyle \sum _{x:A}B(x)}X0+X1+X2+…+X253+X254+X255{\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}

存在量化としての例

何らかの型 を とし、 とする。カリー・ハワード対応により、 はを とする論理述語として解釈できる。与えられた に対して、その型に が 存在するかどうかは、 がこの述語を満たすかどうかを示す。この対応は存在量化や従属対にも拡張できる。すなわち、命題は、その型に が 存在する場合にのみ真である。 あ:あなた{\displaystyle A:{\mathcal {U}}}B:あ→あなた{\displaystyle B:A\to {\mathcal {U}}}B{\displaystyle B}あ{\displaystyle A}1つの:あ{\displaystyle a:A}B（1つの）{\displaystyle B(a)}1つの{\displaystyle a}∃1つの∈あB（1つの）{\displaystyle \exists {a}{\in }A\,B(a)}∑1つの:あB（1つの）{\textstyle \sum _{a:A}B(a)}

例えば、が より小さいか等しいのは、となる別の自然数が存在する場合のみである。論理学では、この命題は存在量化によって次のように表現される。 メートル:北{\displaystyle m:\mathbb {N} }n:北{\displaystyle n:\mathbb {N} }け:北{\displaystyle k:\mathbb {N} }メートル+け＝n{\displaystyle m+k=n}

メートル≤n⟺∃け∈北メートル+け＝n。{\displaystyle m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.}

この命題は従属ペア型に対応します。

∑け:北メートル+け＝n。{\displaystyle \sum _{k:\mathbb {N} }m+k=n.}

つまり、が より小さいか等しいという命題の証明は、との差である負でない数 と、等式 の証明の両方を含むペアです。 メートル{\displaystyle m}n{\displaystyle n}け{\displaystyle k}メートル{\displaystyle m}n{\displaystyle n}メートル+け＝n{\displaystyle m+k=n}

ラムダキューブのシステム

ヘンク・バレンドレトは、型システムを3つの軸に沿って分類する手段として、ラムダキューブを開発しました。立方体の図の8つの角はそれぞれ1つの型システムに対応し、最も表現力の低い角には単純型ラムダ計算、最も表現力の高い角には構成計算が配置されています。立方体の3つの軸は、単純型ラムダ計算の3つの異なる拡張、すなわち依存型の追加、ポリモーフィズムの追加、そして高次の型構築子（例えば、型から型への関数）の追加に対応しています。ラムダキューブは、純粋型システムによってさらに一般化されます。

第一階依存型理論

論理フレームワークLFに対応する純粋な第 1 階従属型のシステムは、単純型ラムダ計算の関数空間型を従属積型に一般化することによって得られます。 λΠ{\displaystyle \lambda \Pi }

二次依存型理論

二階従属型の体系は、型構成子に対する量化を許容することによって得られる。この理論では、従属積演算子は、単純型ラムダ計算の演算子とシステムFの結合子の両方を包含する。 λΠ2{\displaystyle \lambda \Pi 2}λΠ{\displaystyle \lambda \Pi }→{\displaystyle \to}た{\displaystyle \forall }

高階依存型多態ラムダ計算

高階システムは、ラムダキューブの4つの抽象化形式すべてに拡張されます。すなわち、項から項、型から型、項から型、型から項への関数です。このシステムは構成計算に対応し、その導関数である帰納構成計算はRocqの基礎システムです。 λΠω{\displaystyle \lambda \Pi \omega }λΠ2{\displaystyle \lambda \Pi 2}

同時プログラミング言語とロジック

カリー・ハワード対応は、任意の複雑な数学的特性を表現する型を構築できることを意味します。ユーザーが、ある型が存在する（つまり、その型の値が存在する）という構成的証明を提供できれば、コンパイラはその証明を検証し、構築を実行することで値を計算する実行可能なコンピュータコードに変換できます。この証明検証機能により、依存型言語は証明支援系と密接に関連しています。コード生成機能は、機械的に検証された数学的証明から直接コードを導出するため、 形式的なプログラム検証と証明付きコードへの強力なアプローチを提供します。

依存型を持つ言語の比較

言語積極的に開発パラダイム[ a ]戦術証明用語終了チェック種類は[ b ]に依存する宇宙証明の無関係性プログラム抽出抽出により無関係な用語が消去される
アグダはい[ 5 ]純粋に機能的少ない/限られている[ c ]はいはい（オプション）任意の用語はい（任意）[ d ]証明無関係な議論[ 7 ]証明無関係な命題[ 8 ]Haskell、JavaScriptはい[ 7 ]
ATSはい[ 9 ]機能的/命令的いいえ[ 10 ]はいはい静的用語[ 11 ]?はいはいはい
カイエンいいえ純粋に機能的いいえはいいいえ任意の用語いいえいいえ??
ガリーナ（ロク（旧称コック））はい[ 12 ]純粋に機能的はいはいはい任意の用語はい[ e ]はい[ 13 ]Haskell、Scheme、OCamlはい
依存型MLいいえ[ f ]??はい?自然数????
クソ*はい[ 14 ]機能的かつ命令的はい[ 15 ]はいはい（オプション）純粋な用語はいはいOCaml、F#、Cはい
グルいいえ[ 16 ]純粋に機能的な[ 17 ]結合[ 18 ]はい[ 17 ]はい任意の用語いいえはいキャラウェイはい
イドリスはい[ 19 ]純粋に機能的な[ 20 ]はい[ 21 ]はいはい（オプション）任意の用語はいいいえはいはい[ 21 ]
傾くはい純粋に機能的はいはいはい任意の用語はいはいはいはい
マティタはい[ 22 ]純粋に機能的はいはいはい任意の用語はいはいOCamlはい
ニューPRLはい純粋に機能的はいはいはい任意の用語はい?はい?
PVSはい?はい???????
Sage 2020年11月9日アーカイブat the Wayback Machineいいえ[ g ]純粋に機能的いいえいいえいいえ?いいえ???
スパークはい[ 23 ]命令形はい[ 24 ]はい[ 25 ]はい[ 26 ]任意の用語[ h ]??エイダとC [ 27 ]はい[ 28 ]
12はい論理プログラミング?はいはい（オプション）任意の（LF）用語いいえいいえ??
  1. ^これはコア言語を指し、戦術（定理証明手順）やコード生成サブ言語を指すものではありません。
  2. ^宇宙制約などの意味的制約を受ける
  3. ^リングソルバー[ 6 ]
  4. ^オプションのユニバース、オプションのユニバース多態性、およびオプションの明示的に指定されたユニバース
  5. ^ユニバース、自動的に推論されるユニバース制約（Agdaのユニバース多態性とは異なる）、およびオプションのユニバース制約の明示的な印刷
  6. ^ ATSに置き換えられました
  7. ^最後のSage論文と最後のコードスナップショットはどちらも2006年のものである
  8. ^制限された用語にはStatic_Predicate、型キャスト内の任意の用語のAssertのようなチェックにはDynamic_Predicateを使用する

参照

参考文献

  1. ^ホフマン、マーティン（1995）、内包型理論における外延的概念（PDF）
  2. ^ Sørensen, Morten Heine B.; Urzyczyn, Pawel (1998), Curry-Howard同型性に関する講義, CiteSeerX 10.1.1.17.7385 
  3. ^ Bove, Ana; Dybjer, Peter (2008).職場における依存型(PDF) (レポート). チャルマース工科大学.
  4. ^ a b c Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: 砂糖を使わない依存型" (PDF) . Blume, Matthias; Kobayashi, Naoki; Vidal, Germán (eds.).関数型プログラミングと論理型プログラミング, 第10回国際シンポジウム, FLOPS 2010, 仙台, 日本, 2010年4月19日～21日. Proceedings . Lecture Notes in Computer Science. Vol. 6009. Springer. pp.  40– 55. doi : 10.1007/978-3-642-12251-4_5 .
  5. ^ 「Agda ダウンロード ページ」。
  6. ^ 「アグダリングソルバー」。
  7. ^ a b “Announce: Agda 2.2.8” . 2011年7月18日時点のオリジナルよりアーカイブ。2010年9月28日閲覧。
  8. ^ 「Agda 2.6.0 変更ログ」。
  9. ^ 「ATS2 ダウンロード」。
  10. ^ 「ATS発明者Hongwei Xiからのメール」。
  11. ^ Xi, Hongwei (2017年3月). 「応用型システム：定理証明による実践的プログラミングへのアプローチ」(PDF) . arXiv : 1703.08683 .
  12. ^ 「Subversion リポジトリでの Coq の変更」。
  13. ^ 「Coq 8.10 での SProp の導入」。
  14. ^ 「 GitHubでの F* の変更」。GitHub 。
  15. ^ 「 GitHub上の F* v0.9.5.0 リリースノート」。GitHub 。
  16. ^ 「Guru SVN」。
  17. ^ a b Aaron Stump (2009年4月6日). 「Verified Programming in Guru」(PDF) . 2009年12月29日時点のオリジナル(PDF)からアーカイブ。 2010年9月28日閲覧。
  18. ^ Petcher, Adam (2008年5月). 「操作型理論におけるグラウンド方程式を法とする結合可能性の決定」 (PDF) (修士課程). ワシントン大学. 2010年10月14日閲覧。
  19. ^ 「Idris gitリポジトリ」 . GitHub . 2022年5月17日.
  20. ^ Brady, Edwin. 「Idris：依存型を持つ言語 — 拡張概要」（PDF） . CiteSeerX 10.1.1.150.9442 . 
  21. ^ a b Brady, Edwin. 「Idrisは他の依存型プログラミング言語と比べてどうなのか？」
  22. ^ “Matita SVN” . 2006年5月8日時点のオリジナルよりアーカイブ。2010年9月29日閲覧。
  23. ^ 「ALIRE を使用した SPARK のインストール」。
  24. ^ 「§3.2.4 サブタイプ述語」 Adaリファレンスマニュアル（2012年版）。
  25. ^ 「5.11.6. SPARK Lemmaライブラリ」。SPARKユーザーズガイド（第25版）。
  26. ^ 「5.2.8. 契約の終了」 SPARKユーザーズガイド（第25版）。
  27. ^ 「1.2. CCGの呼び出しと使用」。GNAT Pro共通コードジェネレータユーザーズガイド補足（25.0版）。
  28. ^ 「SPARK非対応コンパイラを使用したコンパイル」。SPARKユーザーズガイド（第25.0版）。

さらに読む

「 https://en.wikipedia.org/w/index.php?title=Dependent_type&oldid=1330547407#Comparison_of_languages_with_dependent_types」より取得