型付きラムダ計算 - Wikipedia

型付きラムダ計算（かたつきラムダけいさん、英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ () というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究され

[Itisango]

「typed lambda calculus）とは、無名の関数の抽象表現にラムダ ({\displaystyle \lambda }\lambda ) というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの…」

[hiratara]

へえ。 > 依存型のあるラムダ計算は直観主義的型理論の基盤 > 全ての型の型 (Type : Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない