ラムダ計算（ラムダけいさん、）は、計算模型のひとつで、計算の実行を関数への引数の評価（）と適用（）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。ラムダ計算は1つの変換規則（変数置換）と1つの関数定義規則のみを持つ、最小の（ユニバーサルな）プログラミング言語であるということもできる。ここでいう「ユニバーサルな」とは、全ての計算可能な関数が表現でき正しく評価されるという意味である。これは、ラムダ計算がチューリングマシンと等価な数理モデルであることを意味している。チューリングマシンがハードウェア的なモデル化であるのに対し、ラムダ計算はよりソフトウェア的なアプローチをとっている。この記事ではチャーチが提唱した元来のいわゆる「型無しラムダ計算」について述べている。その後これを元にして「型付きラムダ計算」という体系も提唱されている。元々チャーチは、数学の基礎となり得るような完全な形式体系を構築しようとしていた。彼の体系がラッセルのパラドックスの類型に影響を受けやすい（例えば論理記号として含意 → を含むなら、λx.(x→α) にYコンビネータを適用してカリーのパラドックスを再現できる）ということが判明した際に、彼はそこからラムダ計算を分離し、計算可能性理論の研究のために用い始めた。この研究からチャーチは一階述語論理の決定可能性問題を否定的に解くことに成功した。例えば、ある数に 2 を加える関数 "f" を考える。これは通常の書き方では "f"("x") = "x" + 2 と書くことができるだろう。この関数 "f" は、ラムダ計算の式（ラムダ式という）では λ"x". "x" + 2 と書かれる。変数 "x" の名前は重要ではなく、 λ"y". "y" + 2 と書いても同じである。同様に、この関数に 3 を適用した結果の数 "f"(3) は (λ"x". "x" + 2) 3 と書かれる。関数の適用は左結合である。つまり、 "f" "x" "y" = ("f" "x") "y" である。今度は、引数（関数の入力）に関数をとりそれに 3 を適用する関数を考えてみよう。これはラムダ式では λ"f". "f" 3 となる。この関数に、先ほど作った 2 を加える関数を適用すると、 (λ"f". "f" 3) (λ"x". "x" + 2) となる。ここで、の3つの表現はいずれも同値である。ラムダ計算では、関数の引数は常に1つである。引数を2つとる関数は、1つの引数をとり、1つの引数をとる関数を返す関数として表現される（カリー化）。例えば、関数 "f"("x

出典:wikipedia