型付きラムダ計算

ウィキペディア

型付きラムダ計算

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/08/07 06:18 UTC 版)

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