ラムダ計算(lambda calculus)とは、何でも関数を用いて計算してしまう方法である。
概要
ラムダ計算とは、関数についての3つの操作だけであらゆる計算が可能、すなわちチューリング完全を実現できるという理論である。LISPをはじめとする関数型言語の理論的根拠となっている。1930年代にAlonzo Churchという数学者が提唱したが、最初に思いついたのはAlonzo Churchではないらしい。
ラムダ計算は以下の3つの操作からなる。きちんと説明しようとするとよくわからない記号だらけになるので、おおざっぱにだけ記載しておく。
- α変換: 関数に名前をつけて置き換えることができる。
- β変換: 関数には実際に代入して計算することができる。簡約ともいう。
- η変換: 2つの関数がすべての引数について同じ値を返すとき、2つの関数は同値であるとみなす。
η変換は何を当たり前のことを言っているんだと思うかもしれないが、たとえば1からnまでの整数の和を求めるのに、1から順番に数を足していく方法でも、等差数列の和の公式を使う方法でも、計算方法は違えど同値であるということである。
ラムダ式
上記操作においては、関数も数値と同じように引数にしたり戻り値にしたりできる、高階関数が前提となっている。このため、数値がx = 1というような書き方ができるように、関数も名前をつけて置き換えられる必要がある。
Alonzo Church自身は、たとえば f(x) = x2+ x + 1 のときに、関数 f 自体を f = λx.(x2+ x + 1) といった書き方をしており、これをラムダ式(lambda expression)と呼んだ。
プログラミングにおいては使用できる文字の制約などにより上記とは少し異なる記法を採用していることがほとんどだが、実質的には同じことなのでそれらもラムダ式と呼ばれている。
名前の由来
ラムダ式に用いられる記号 λ に由来するわけだが、この λ 自身の由来については2説あり、真偽についてはあまりはっきりしていない。
由来がある説
Rosserという人が1984年に以下のように報告している。
Russell と Whiteheadが、関数を抽象化するときの記号に「x̂(結合文字非対応環境用に書くと、âのaをxにしたもの)」を用いていた。Alonzo Churchは、この表記法にちなんで、「∧x」という記号を使用するようになった。その後印刷しやすいように「∧」の代わりに「λ」を使用するようになった(ちなみにλの大文字はΛ(≠∧)である)。
由来なんかない説
Alonzo Church自身は後年「とにかく記号が必要だったからたまたまλを選んだ」と語っており、この話を信じるなら特に由来はないということになる。一般には紙面で報告された「由来がある説」の方が信頼性が高いということになるが、紙面とはいえ他人がした報告である。一方こちらはAlonzo Church本人の言葉であり、そう聞いた人が1人だけというわけでなく2人いるということなので、こちらもそれなりに信憑性が高い。
- History of Lambda-calculus and Combinatory Logic: 上記の内容はこれの7ページあたりに書いてある。
- Why is lambda calculus named after that specific Greek letter? Why not “rho calculus”, for example?
- λの起源、2つの説: 後発記事だけにもう少し深く掘り下げているが2説あるというのは当記事と同じ。
関連項目
関連商品
- 1
- 0pt