理学部紹介冊子
ラムダ計算
ラムダ計算は，計算を抽象化した体系であり，さまざまなプログラミング言語の基礎として利用されている。
ラムダ計算の特徴として，関数を形式的に扱うことができるという点が挙げられる。一般に，数学の議論に登場する数式は厳密な記法であると信じられがちだが，実際は必ずしもそうではない。とくに，数式における関数の表現は曖昧であることが多い。たとえば，よく目にする「f（x）」という表現がある。これは，xの部分に後で何かを受け取る関数を意味しているのか，すでにあるそのような関数に値xを渡した計算結果を意味しているのか，定かではない。どちらを意味するのかは，通常，文脈によって決定される。このことは，専門家同士が議論をする上ではあまり問題にならないが，分野の違う人々が議論する場合に大きな妨げとなることがある。ラムダ計算では，関数そのものと関数が返す値とは表記上厳密に区別されるので，ラムダ計算の記法を使えば，そのような問題は起こらない。
また，ラムダ計算において関数を定義することと，プログラムを書くことはよく似ている。実際，関数型プログラミング言語とよばれるラムダ計算を基礎として実装されたプログラミング言語では，プログラムを書くことは，関数を定義することとほぼ同義である。
もともと，ラムダ計算に型は存在しなかったが，プログラミング言語としての側面が強くなるに連れて，型が考慮されるようになる。関数型プログラミング言語に限らず，型は高度なプログラミングに有効な概念である。たとえば，JavaやMLといったプログラミング言語では，型の整合性がないプログラムはコンパイルできず，コンパイルできたプログラムは実行時にある種のエラーが起こらないことが保証されている。ラムダ計算と型についての研究は，現在でも活発に行われている。
ところで，ラムダ計算のラムダとは，勿論ギリシャ文字の「λ」のことである。計算機科学の分野では，このようにギリシャ文字の名前がついた計算体系が数多く提案されており，中でも，ラムダ計算に次いでよく利用されているのがパイ計算である。パイ計算は，おもに通信や平行計算のモデルとして利用されている。情報理工学系研究科コンピュータ科学専攻の萩谷研究室では，ラムダ計算やパイ計算の理念にあるように，計算というものの本質を抽象化し形式的に扱うことを研究の大きなテーマとしている。