一階の依存型理論
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/29 03:08 UTC 版)
一階の依存型を持つ λ Π {\displaystyle \lambda \Pi } 型システムは、単純型付きラムダ計算の関数型(矢印型)を依存積型に一般化することで得られる。これは論理学におけるLogical Framework LF (en:Logical framework#LF)に対応する。
※この「一階の依存型理論」の解説は、「依存型」の解説の一部です。
「一階の依存型理論」を含む「依存型」の記事については、「依存型」の概要を参照ください。
- 一階の依存型理論のページへのリンク