依存型

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

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

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

歴史

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

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

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

正式な定義

大まかに言えば、依存型はインデックス付き集合族の型に似ています。より正式には、型の集合体における型が与えられた場合、各項に型を割り当てる型の族が存在する可能性があります。この型はによって変化すると言います。 $A:{\mathcal {U}}$ ${\mathcal {U}}$ $B:A\to {\mathcal {U}}$ $a:A$ $B(a):{\mathcal {U}}$ $B(a)$ $a$

Π型

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

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

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

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

より具体的な例として、を 0 から 255 までの符号なし整数 (8 ビットまたは 1 バイトに収まるもの) の型とし、をとすると、はの積になります。 $A$ $B(a)=X_{a}$ $a:A$ ${\textstyle \prod _{x:A}B(x)}$ $X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}$

Σ型

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

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

より具体的な例として、を再び 0 から 255 までの符号なし整数の型とし、を再び256 のより任意のに対してと等しくすると、は合計になります。 $A$ $B(a)$ $X_{a}$ $X_{a}$ ${\textstyle \sum _{x:A}B(x)}$ $X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}$

存在量化としての例

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

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

$m\leq n\iff \exists {k}{\in }\mathbb {N} \,m+k=n.$

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

$\sum _{k:\mathbb {N} }m+k=n.$

つまり、がより小さいか等しいという命題の証明は、との差である負でない数と、等式の証明の両方を含むペアです。 $m$ $n$ $k$ $m$ $n$ $m+k=n$

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

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

第一階依存型理論

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

二次依存型理論

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

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

高階システムは、ラムダキューブの4つの抽象化形式すべてに拡張されます。すなわち、項から項、型から型、項から型、型から項への関数です。このシステムは構成計算に対応し、その導関数である帰納構成計算はRocqの基礎システムです。 $\lambda \Pi \omega$ $\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日アーカイブ - Wayback Machine	いいえ^[g]	純粋に機能的	いいえ	いいえ	いいえ	?	いいえ	?	?	?
スパーク	はい^[23]	命令形	はい^[24]	はい^[25]	はい^[26]	任意の用語^[h]	?	?	エイダとC ^[27]	はい^[28]
12	はい	論理プログラミング	?	はい	はい（オプション）	任意の（LF）用語	いいえ	いいえ	?	?

^ これはコア言語を指し、戦術（定理証明手順）やコード生成サブ言語を指すものではありません。
^ 宇宙制約などの意味的制約を受ける
^ リングソルバー^[6]
^ オプションのユニバース、オプションのユニバース多態性、およびオプションの明示的に指定されたユニバース
^ ユニバース、自動的に推論されるユニバース制約（Agdaのユニバース多態性とは異なる）、およびオプションのユニバース制約の明示的な印刷
^ ATSに置き換えられました
^ 最後のSage論文と最後のコードスナップショットはどちらも2006年のものである
^ 制限された用語にはStatic_Predicate、型キャスト内の任意の用語のAssertのようなチェックにはDynamic_Predicateを使用する

参照

参考文献

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

さらに読む

Martin-Löf, Per (1984). 直観主義型理論(PDF) . Bibliopolis.
ノードストローム、ベングト。ケント州ピーターソン。スミス、ヤン・M. (1990)。 Martin-Löf の型理論におけるプログラミング: 入門。オックスフォード大学出版局。ISBN 9780198538141。
Barendregt, H. (1992). 「型付きラムダ計算」 Abramsky, S.; Gabbay, D.; Maibaum, T. (編).コンピュータサイエンスにおける論理ハンドブック. Oxford Science Publications . doi :10.1017/CBO9781139032636. hdl : 2066/17231 .
ブランドル、ヘルムート（2022年）『構成の微積分』
マクブライド, コナー; マッキナ, ジェームズ (2004年1月). 「左からの視点」. Journal of Functional Programming . 14 (1): 69– 111. doi : 10.1017/s0956796803004829 . S2CID 6232997.
Altenkirch, Thorsten ; McBride, Conor ; McKinna, James (2006). 「依存型が重要な理由」(PDF) . Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13 . ISBN 1-59593-027-2。
ノレル、ウルフ（2007年9月）. 依存型理論に基づく実用的なプログラミング言語に向けて(PDF) (PhD). ヨーテボリ、スウェーデン：チャルマース工科大学コンピュータサイエンス・エンジニアリング学部. ISBN 978-91-7291-996-9。
Oury, Nicolas; Swierstra, Wouter (2008). 「円周率の力」(PDF) . ICFP '08: 第13回ACM SIGPLAN国際関数型プログラミング会議議事録. pp. 39– 50. doi :10.1145/1411204.1411213. ISBN 9781595939197. S2CID 16176901。
ノレル、ウルフ (2009)。「Agda での依存型プログラミング」(PDF)。コープマン、P.プラスマイヤー、R.スウィアストラ、D. (編)。高度な関数型プログラミング。 2008 年 AFP。コンピューターサイエンスの講義ノート。 Vol. 5832.スプリンガー。 pp. 230–266。土井:10.1007/978-3-642-04652-0_5。ISBN 978-3-642-04651-3。
Sitnikovski, Boro (2018). 『Idrisによる依存型入門』 Lean Publishing. ISBN 978-1723139413。
マクブライド, コナー; ノルドヴァル＝フォルスバーグ, フレドリック (2022). 「次元を考慮したプログラムのための型システム」(PDF) .計量と試験における高度な数学的・計算ツール XII . 応用科学のための数学の進歩. World Scientific. pp. 331– 345. doi :10.1142/9789811242380_0020. ISBN 9789811242380. S2CID 243831207。

外部リンク

依存型プログラミング 2008
依存型プログラミング 2010
依存型プログラミング 2011
Haskell Wikiの「依存型」
n ラボにおける依存型理論
n ラボの依存型
n ラボの依存製品タイプ
n ラボの従属和型
n ラボの依存製品
n ラボの従属合計

[5] これはコア言語を指し、戦術（定理証明手順）やコード生成サブ言語を指すものではありません。

[6] 宇宙制約などの意味的制約を受ける

[9] リングソルバー^[6]

[10] オプションのユニバース、オプションのユニバース多態性、およびオプションの明示的に指定されたユニバース

[17] ユニバース、自動的に推論されるユニバース制約（Agdaのユニバース多態性とは異なる）、およびオプションのユニバース制約の明示的な印刷

[19] ATSに置き換えられました

[29] 最後のSage論文と最後のコードスナップショットはどちらも2006年のものである

[34] 制限された用語にはStatic_Predicate、型キャスト内の任意の用語のAssertのようなチェックにはDynamic_Predicateを使用する

[extensional-1] ホフマン、マーティン（1995）、内包型理論における外延的概念（PDF）

[curry_howard-2] Sørensen, Morten Heine B.; Urzyczyn, Pawel (1998), Curry-Howard同型性に関する講義, CiteSeerX 10.1.1.17.7385

[dep_types_at_work-3] Bove, Ana; Dybjer, Peter (2008). 職場における依存型(PDF) (レポート). チャルマース工科大学.

[without-sugar-4] Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas (2010). "ΠΣ: 砂糖なしの依存型" (PDF) . Blume, Matthias; Kobayashi, Naoki; Vidal, Germán (編).関数型プログラミングと論理型プログラミング, 第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.

[7] 「Agda ダウンロードページ」。

[8] 「Agda リングソルバー」。

[agda-2.2.8-11] “Announce: Agda 2.2.8”. 2011年7月18日時点のオリジナルよりアーカイブ。2010年9月28日閲覧。

[12] 「Agda 2.6.0 変更ログ」。

[13] 「ATS2 ダウンロード」。

[14] 「ATS発明者Hongwei Xiからのメール」。

[15] Xi, Hongwei (2017年3月). 「応用型システム：定理証明による実践的プログラミングへのアプローチ」(PDF) . arXiv : 1703.08683 .

[16] 「Subversion リポジトリでの Coq の変更」。

[18] 「Coq 8.10 での SProp の導入」。

[20] ^ 「 GitHubでの F* の変更」。GitHub 。

[21] ^ 「 GitHub上のF* v0.9.5.0リリースノート」。GitHub 。

[22] 「Guru SVN」。

[guru-book-23] Aaron Stump (2009年4月6日). 「Verified Programming in Guru」(PDF) . 2009年12月29日時点のオリジナル(PDF)からアーカイブ。 2010年9月28日閲覧。

[hypjoin-paper-24] Petcher, Adam (2008年5月). 「操作型理論におけるグラウンド方程式を法とする結合可能性の決定」(PDF) (修士課程). ワシントン大学. 2010年10月14日閲覧。

[25] “Idris gitリポジトリ”. GitHub . 2022年5月17日.

[26] Brady, Edwin. 「Idris：依存型を持つ言語 — 拡張概要」（PDF） . CiteSeerX 10.1.1.150.9442 .

[idris-compare-27] Brady, Edwin. 「Idrisは他の依存型プログラミング言語と比べてどうなのか？」

[28] “Matita SVN”. 2006年5月8日時点のオリジナルよりアーカイブ。2010年9月29日閲覧。

[30] 「ALIRE を使用した SPARK のインストール」。

[31] 「§3.2.4 サブタイプ述語」Adaリファレンスマニュアル（2012年版）。

[32] 「5.11.6. SPARK Lemmaライブラリ」。SPARKユーザーズガイド（第25版）。

[33] 「5.2.8. 契約の終了」SPARKユーザーズガイド（第25版）。

[35] 「1.2. CCGの呼び出しと使用」。GNAT Pro共通コードジェネレータユーザーズガイド補足（第25.0版）。

[36] 「SPARK非対応コンパイラによるコンパイル」SPARKユーザーズガイド（第25.0版）。

v t e 数学の基礎における主要なトピック
数理論理学	ペアノの公理数学的帰納法正式なシステム公理体系ヒルベルトシステム自然演繹数学的証明モデル理論数学的構成主義様相論理数理論理学のトピック一覧
集合論	セット素朴集合論公理的集合論ツェルメロ集合論ツェルメロ・フランケル集合論構成的集合論記述的集合論決定性ラッセルのパラドックス集合論のトピックのリスト
型理論	還元公理単純な型理論依存型理論直観主義型理論ホモトピー型理論一価基底ジラールのパラドックス
カテゴリー理論	カテゴリトポス理論セットのカテゴリ高等圏理論 ∞群 ∞トポス理論数学的構造主義圏論用語集圏論のトピック一覧