ラムダ計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/09/17 06:16 UTC 版)
ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算模型のひとつで、計算の実行を関数への引数の評価（英語: evaluation）と適用（英語: application）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。
- ^ “チャーチ数とpred関数”. kimiyuki.net. 2018年10月6日閲覧。
ラムダ計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/25 04:07 UTC 版)
カリー＝ハワード対応はIPCと直和と直積を持つ単純型付きラムダ計算との間に拡張できる。
※この「ラムダ計算」の解説は、「直観主義論理」の解説の一部です。
「ラムダ計算」を含む「直観主義論理」の記事については、「直観主義論理」の概要を参照ください。
ラムダ計算
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/09 06:43 UTC 版)
計算を1つの初期ラムダ式（入力を分離したい場合は2つのラムダ式）と有限個のラムダ項で表す。各ラムダ項は前のラムダ項にβ簡約を適用したものである。
※この「ラムダ計算」の解説は、「計算理論」の解説の一部です。
「ラムダ計算」を含む「計算理論」の記事については、「計算理論」の概要を参照ください。
ラムダ計算と同じ種類の言葉
- ラムダ計算のページへのリンク
