高階の依存型付き多相ラムダ計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/29 03:08 UTC 版)
「依存型」の記事における「高階の依存型付き多相ラムダ計算」の解説
高階の λ Π ω {\displaystyle \lambda \Pi \omega } 型システムは λ Π 2 {\displaystyle \lambda \Pi 2} を、ラムダ・キューブの4つ全てのラムダ抽象の形式に拡張することで得られる。すなわち、項から項への関数、型から項への関数、項から型への関数、そして型から型への関数である。この型システムはCalculus of constructionsに対応する。Calculus of constructionsをさらに拡張するとCalculus of inductive constructions (en:Calculus of inductive constructions) が得られる。これは、Coqが用いている型システムである。
※この「高階の依存型付き多相ラムダ計算」の解説は、「依存型」の解説の一部です。
「高階の依存型付き多相ラムダ計算」を含む「依存型」の記事については、「依存型」の概要を参照ください。
ウィキペディア小見出し辞書の「高階の依存型付き多相ラムダ計算」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 高階の依存型付き多相ラムダ計算のページへのリンク
