今から６０年程前、プリンストン大学の若手論理学者Ａ．チャーチが、関数の新しい表記法を提案しました。ラムダ記法と呼ばれるその表記法では、例えば二乗を計算する関数は λx.x^2 と表します。従来の"f(x)"という書き方は、それが関数を表すのか、関数のxにおける値を表すのかが曖昧なので、ラムダ記法では、関数fのxにおける値をfxで示し、xにおける値がf(x)となる関数fをλx.f(x)と表すのです。
"f(x)"という表記法の欠陥は、高校の数学までではほとんど表面化しませんが、大学に入ってから定義域や値域が関数の集合になるような高階関数（オペレータとか作用素とも呼びます）を扱いだすとすぐわかります。作用素などというとひどく特殊なもののようですが、関数f(x)にその導関数f'(x)を対応させる微分演算子Ｄがその代表例です．例えば、D(f(g(x)))=f'(g(x))g'(x) はよく知られたchain ruleですが、f'(g(x)) をＤを使って D(f(g(x)))と表現してもいいですか？ もしそうすると左辺の式と区別できなくなってしまいますし、考えてみれば左辺が何を意味しているのかも曖昧だったのです。
チャーチがλ記法を導入したのは関数の概念をベースにして数学全体を基礎付けようという試みからでした。しかし、彼が提案した公理系は弟子達にその非整合性を突かれ、またラムダ計算で扱える関数のクラスが結局再帰的(recursive)関数のクラスと一致することが分かってしまうとチャーチたちはこの体系に興味を失ってしまったようです。ところが、最近になってラムダ計算がまた脚光を浴びています。“プログラムは関数である”という立場から、ソフトウェア・サイエンスを基礎付ける動きが本格化してきたからです。
まず、BASICやPASCALなどの言語で書かれた普通のプログラムを考えると、計算機はそれらを直接理解して思い通りの関数として働いてくれるわけではありません。人間が書いたプログラムは計算機にとって分かりやすい別のプログラムに翻訳されて、あるいは翻訳されながら実行されます。その翻訳のためのソフトウェア機構はコンパイラとかインタプリタとか呼ばれますが、われわれの言葉でいえば関数族から関数族への関数になります。しかし、コンパイラもそれ自身一種の高級なプログラムですから、それを解釈する別の機構が必要です。その機構は、関数族から関数族への関数をもらって関数の値を出すような関数になります。こうして眺めてゆくと、ソフトウェアの世界は関数族の層が幾重にも重なった複雑な構造であることが見えてきます。
このようなソフトウェアの複雑な構造の中で生じる問題の多くが、実は上で述べた関数の代入の問題と深く関連しているのです。例えば、オペレーティング・システムのバージョンアップで、使い慣れたアプリケーション・プログラムが動かなくなったり、異常な動きをしたりで困った経験をお持ちの方は多いでしょう。ソフトウェアというのは、その名の通り、柔軟に変化していくことが使命でしょうが、現状では階層間の関係が複雑すぎて、各層の機能を自由に改良することができません。また、実際にプログラムを組まれた経験のある方なら、この手の問題が単一のプログラムの中にも様々なレベルで存在することを知っていらっしゃるはずです。プログラムの各構成要素の役割が他の構成要素との関係で決まり、その関係があまりクリアーでないことが問題なのです。この辺りの問題を一掃するのが、ラムダ計算をベースにした関数型プログラミングの参照透明性(referential transparency)という概念です。関数型プログラミングの内容については、この小文の範囲を越えるので、興味ある方は文献［４］などを参照してください。
Ｂ. ラムダ計算の体系
ラムダ計算の体系といってもいろいろあるのですが、ここでは数学や論理の概念の定義（δ規則）を含まない最も原始的な体系を紹介します。しかし、実はこの極めて単純な体系の中にもかなり豊かな（計算のメカニズムを扱うには十分な）数学の世界があることをあとで示します。
まずラムダ計算の対象となるλ項を次のように帰納的に定義します。
定義１ (1) 変数x, y, ... はλ項である。
(2) M, Nがλ項のとき、 (MN)もλ項である。
(3) Mがλ項、xが変数のとき、(λx.M)はλ項である。
(MN)は、MのNへの関数適用と呼びます。これは、通常の記法でのM(N)（関数MのNでの値）を意味しているのですが、NをMに代入するのではなく、MをNに適用するという考え方の違いが重要です。もう一つ特筆すべき点は、(MN)が任意のλ項M, Nに対して定義されていること、つまり定義域の概念がないことです。これは驚異的な特長ですが、このために新しい概念を導入して理論を拡大することが困難になっており、最近では定義域の概念を加えた"型付きラムダ計算"の研究も盛んになっています。また、(λx.M)はxでの値がMとなるような関数を表し、Mのxによるλ抽象と呼ばれます。
ラムダ計算が扱う対象は、こうして定義されたλ項だけです。ただ、この定義のままではカッコが多すぎてカッコ悪いため、適当にカッコを省略したり、次のような略記法を用います。例えば、λxyz.M は(λx.(λy.(λz.M))) 、KLMNは(((KL)M)N)の省略形とします。直観的には、λxyz.Mという書き方はMが３変数関数f(x,y,z)であることを意味しており、(λx.(λy.(λz.M)))の方は、xの値を定めると、yの値に1変数関数λz.Mを対応させる関数が得られると解釈できます。つまり、多変数の関数が１変数の高階関数として表現できたわけで、このような表現法を論理学者カリーの名をとってカリー化と呼んでいます。
ラムダ計算は、λ項を変形して行くだけの極めて単純なシステムです。しかも、われわれの体系には変換規則がたった一つしかなく、その規則（β変換）も変数に関する条件を除けばほとんど自明なものです。ここでは多少厳密さを犠牲にし、なるべく簡単に変数条件等について説明しておきましょう。まず、λ項Mが(λx.N)の形の部分項を含むとき、この部分項における変数xのoccurrence（出現）はすべて束縛されているといいます。そして、(λx.N)における変数xのすべてのoccurrenceをこの部分項に含まれない別の変数で置き換えること、つまり束縛変数の交換（厳密にはα変換という）はあえて形式化しないで適当に行なうものとします。例えば、λx.fx と λy.fy とは交換自由です。一方、λ項Mにおける変数xのあるoccurrenceが(λx.N)の形のどの部分項にも入らないならそれは自由であるといいます。そして、β変換の定義に必要な表現M[x:=N] は、Mに含まれるxの自由なoccurrenceをすべてNで置き換えてできるλ項を表すものとします。このとき、Nの自由変数が置き換え後のM[x:=N] において束縛されてはならないというのが、最初に言いたかった条件です。今後は話を簡単にするため、この変数条件は束縛変数の変更（α変換）によって自動的に満たされていると仮定しておきます。
定義２ β変換とは、(λx.M) Nの形をしたλ項（β基）を M[x:=N]に変換する操作である。λ項Lに含まれる１つのβ基をβ変換してλ項Mが得られるとき、L→M と書く。また、β変換を０回以上有限回繰り返して、LからNが得られるとき、L→→N と書くことにします。
変換の具体例を見てみましょう。
(λxyz.xz(yz)) (λxy.x)
→ λyz.(λxy.x)z(yz)
→ λyz.(λy.z)(yz)
→ λyz.z
従って、(λxyz.xz(yz)) (λxy.x) →→λyz.z です。この例では、変換途中に現われるλ項はどれもちょうど一つのβ基を持ち、最後のλ項はβ基を持たないことに注意してください。従って、変換の道筋はただ１通りでこれ以外もこれ以上もありません。
M→→N で、かつN がβ基を持たないときに、Mは正規形Nを持つといいます。上の例では、λ項(λxyz.xz(yz)) (λxy.x)が唯一つの正規形λyz.zを持つことが示されました。しかし、一般には複数のβ基を持つλ項（例：(λx.x) ((λx.x) x)）や、β変換が有限で終わらないもの（例：(λx.xxx) (λx.xxx)）もたくさんあるので、与えられたλ項が正規形を持つか否かや、またどんな正規形を持つかということは全く明らかではありません。そこで、この変換プロセスの構造を研究することがラムダ計算の主要課題の一つで、次に述べる２つの定理はその代表的な成果です。
定理１（チャーチ・ロッサーの定理） L→→M かつ L→→N ならば、M→→K かつN→→K となるβ項Kが存在する。
この系として、一つのラムダ項が複数の正規形を持つことはないのがわかります。
定理２ ラムダ項が正規形を持つか否かを判定するアルゴリズムはない。（つまり、正規形をもつラムダ項のゲーデル数の集合はrecursiveでない。）
これは歴史上最初に示された非決定問題の形式として有名です。
Ｃ. ラムダ計算の中の世界
では、ラムダ計算に内在する数学の世界の面白さを少し見てみましょう。まず、自然数を次のようなλ項で定義します：
0 = λfx.x
1 = λfx.fx
2 = λfx.f(fx)
3 = λfx.f(f(fx))
ただし、これは新しいλ項を定義しているのではなく、例えばλfx.f(fx)を"2"と考える、あるいはλfx.f(fx)の省略形として2を用いるということです。もしも新しいλ項として2を導入し、それはλfx.f(fx)と互いに変換可能であるとしたら、それまで持っていた体系の性質まで変えてしまう危険性があるのです。また、この自然数の定義は一見奇妙ですが、哲学者ウィトゲンシュタインの命題「数とは操作のベキである」（『論理哲学論考』6.021）と符合しており、なかなか意味深長です。しかし、その真価はこれから述べる演算の定義の簡単さにあるでしょう。
まず、足し算plusを次のように定義します：
plus = λabfx.af(bfx)
これでうまくいくか、一つ簡単な計算をしてみましょう。
plus 1 2 = (λabfx.af(bfx)) (λfx.fx) (λfx.f(fx))
→ (λbfx.(λfx.fx)f(bfx)) (λfx.f(fx))
→ (λbfx.(λx.fx)(bfx)) (λfx.f(fx))
→ (λbfx.f(bfx)) (λfx.f(fx))
→ λfx.f((λfx.f(fx))fx)
→ λfx.f((λx.f(fx))x)
→ λfx.f(f(fx)) = 3.
さて面白いことに、掛け算timesや累乗expは足し算より簡単にできます：
times = λabf.a(bf), exp = λab.ba
例えば、times 2 3 →→ 6, exp 2 3 →→ 8 などを計算していただくと仕組みがわかるはずです。
ここまで来ると、λ項で表現できる関数の集合が一体どんなものか興味が涌いてきませんか？ 荒っぽい言い方ですが、それは計算機が計算できる関数の集合と一致することが知られています。“計算できる”という概念の源はゲーデルの不完全性定理の証明にあるのですが、チャーチはそれをラムダ計算の言葉で形式化し、ほぼ同じ頃チューリングは電子計算機のプロトタイプともいえるチューリング機械で表現しました。計算可能な関数がすべてこれらの形式で表現できると言う主張はチャーチ・チューリングの提唱と呼ばれています。
ここまでは自然数の話でしたが、実数だってちゃんと定義できます。例えば、
pi 0 = 3, pi 1 = 1 pi 2 = 4, pi 3 = 1, ...
を満たすλ項piの存在は、円周率πを計算するアルゴリズムがあることとチャーチ・チューリングの提唱から言えます。このλ項piを実数πと考えればいいわけですし、他の実数についても同様です。さらに、実数の演算や連続関数の概念などもうまく組み入れて、どんどん数学の世界を展開してゆくと一体どうなるでしょうか？ 多分、再帰的数学(recursive mathematics)と呼ばれて盛んに研究されている世界に近くなることは想像できますが、正確な解答は知りません。
最後になりましたが、ラムダ計算の本当の面白さはこの小文の先にあります。ラムダ計算のモデルの話（スコット理論）、型付きラムダ計算と論理の関係（カリー・ハワードの対応）、関数型プログラミングとその実現技術、etc. これらはどうか次の本を参考にしてください。
[1] 井田哲男、計算モデルの基礎理論、岩波書店 1991.
[2] 高橋正子、計算論、近代科学社 1991.
[3] Hindley & Seldin, Introduction to Combinators and λ-calculus, Cambridge Univ. Press 1986.
[4] Field & Harrison, Functional Programming, Addison-Wesley 1988.