ラムダ計算

ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算という行為を「関数」の定義と適用だけで表現する計算模型（数理モデル）である。ラムダ算法とも言う。

1930年代に数学者のアロンゾ・チャーチとスティーヴン・コール・クリーネによって、「計算できるとはどういうことか」を厳密に定義するために考案された。当時はまだ電子計算機は実用化されておらず、ラムダ計算は純粋に理論的な数学的体系として発展した。関数を定義する際にギリシャ文字のラムダ（λ）を使う慣習からその名がある。

ラムダ計算は、変数と関数の抽象化、および関数の適用という基本的な操作のみから構成されるが、全ての計算可能関数を表現できるチューリング完全な計算体系である。ラムダ計算は、アラン・チューリングが考案したチューリングマシン（仮想的な機械のテープとヘッドの動きで計算を表現するモデル）と計算能力において等価である。チューリングマシンで計算可能な任意の関数はラムダ計算でも表現可能であり、逆にラムダ計算で表現可能な任意の関数はチューリングマシンでも計算可能である。この等価性はチャーチ＝チューリングのテーゼの重要な根拠の一つとなっている。チューリングマシンがハードウェア（機械）の観点から計算をモデル化するのに対し、ラムダ計算はソフトウェア（関数とその適用）の観点から計算をモデル化している。

ラムダ計算は、理論計算機科学や論理学の基礎理論として重要な位置を占めている。特にLISP、Haskell、MLといった関数型言語の理論的基盤となっており、Java（Java 8以降）、C#、Python、JavaScriptなど多くの主流プログラミング言語に導入されている「ラムダ式」（無名関数）の機能は、ラムダ計算の概念に基づいている。

本記事では、チャーチが提唱した元来の「型無しラムダ計算」（untyped lambda calculus）を中心に述べる。型無しラムダ計算は変数や式に型の制約を課さないため、表現力が高い反面、矛盾を含む式も記述可能である^[1]。その後、1940年代から論理的なパラドックスを回避し、またプログラムの整合性を保証するために、変数や関数に「型」の制約を加えた「型付きラムダ計算」（typed lambda calculus）という体系が発展した。型付きラムダ計算は直観主義論理との対応関係（カリー・ハワード対応）を持ち、プログラムの正当性検証や定理証明の理論的基盤となっている。型付きラムダ計算には単純型付きラムダ計算、System F、依存型を持つ体系など、多様な変種が存在する。

歴史

元々チャーチは、数学の基礎となり得るような完全な形式体系を構築しようとしていた。彼の体系がラッセルのパラドックスの類型に影響を受けやすい（例えば論理記号として含意 → を含むなら、λ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) となる。ここで、

(λf. f 3) (λx. x + 2) と (λx. x + 2) 3 と 3 + 2

の3つの表現はいずれも同値である。

ラムダ計算の形式的定義では、ラムダ抽象（関数の定義）は1つの変数のみを束縛する。複数の引数を取る関数は、1つの引数を受け取り別の関数を返す高階関数として表現される。この手法はカリー化と呼ばれる。例えば、関数 f(x, y) = x − y は λx. (λy. x − y) となる。この式は慣例で λxy. x − yと省略して書かれることが多い。以下の3つの式

(λxy. x − y) 7 2 と　(λy. 7 − y) 2 と 7 − 2

は全て同値となる。

ラムダ計算そのものには上で用いた整数や加算などの概念は組み込まれていないが、これらは特定のラムダ式として定義（エンコード）することで表現できる。

ラムダ式は自由変数（ λ によって束縛されていない変数）を含むこともできる。例えば、入力に関係なく常に y を返す関数を表す式 λx. y において、変数 y は自由変数である。このようなときに変数名の付け替えが必要になることがある。つまり、式 (λxy. y x) (λx. y) は λy. y (λx. y) ではなく、 λz.z (λx. y) と同値である。

定義

ここではラムダ計算の形式的な定義を述べる。まず、変数名として用いる記号（識別子、identifier）の可算無限集合 {a, b, c,…, x, y, z,…} を導入する。全てのラムダ式（ラムダ項）の集合の構文は、BNFを用いて以下のように帰納的に定義される。

<expr> ::= <identifier>
<expr> ::= (λ<identifier>. <expr>)
<expr> ::= (<expr> <expr>)

ここで <expr> はラムダ式（expression）を、<identifier> は変数名（識別子）を表すメタ記号である。

最初の2つの規則は関数の定義を表しており、3つめの規則は関数に引数を適用することを表している。規則2のことをラムダ抽象（英: lambda abstraction）といい、規則3のことを関数適用（英: application）という。関数適用は左結合であることと、ラムダ抽象はその後ろに続く全ての式を束縛することの2点をもってあいまいさが排除される場合は、括弧を省略してもよい。例えば、 ((λx. ((x x) x)) (λy. y)) はより簡単に (λx. x x x) λy. y と書ける。また、非形式的な説明で述べたようにMをラムダ式としたとき、λx. (λy. M)をλxy. Mと略記する。

ラムダ抽象によって束縛されていない変数を自由変数（英: free variable）という。式 λx. (x y) において、 y は自由変数である。ある変数の出現が自由出現であるかどうかは、より正確には以下のように帰納的に定義されている。

ラムダ式 V が変数のとき、 V は自由出現である。
ラムダ式 λV. E において、 E で自由出現している変数のうち V 以外のものが自由出現である。このとき、 E 中の変数 V はラムダに束縛されたという。
ラムダ式 (E E′) において、 E での自由出現と E′ での自由出現の和が自由出現である。

ラムダ式の集合の上での同値関係（ここでは == と書くことにする）は、直感的には、2つのラムダ式が同じ関数を表していることである。この同値関係は以下で述べるα-変換とβ-簡約によって定義される。第3の規則としてη-変換と呼ばれる規則が導入されることもある。

α-変換

アルファ変換の基本的なアイデアは、束縛変数の名前は重要ではない、ということにある。例えば、 λx. x と λy. y は同じ関数を表している。しかし、ことはそう単純ではない。ある束縛変数の名前を置換してもよいかどうかには、いくつかの規則が絡んでくる。例えば、ラムダ式 λx. λy. x 中の変数 x を y に置き換えると、 λy. λy. y となるが、これは最初の式とはまったく異なるものを表すことになる。そこでまず準備として、変数 V, W と式 E に対して、 E 中の V の全ての自由出現を W に置き換えたものを

E[V := W]

と書くことにする。この元で、アルファ変換は

λV. E →^α λW. E[V := W]

である。ただし、 E に W が自由出現しておらず、かつ V を置換することにより E 中で新たに W が束縛されることがないときに限る。この規則によれば、式 λx. (λx. x) x が λy. (λx. x) y に変換されることがわかる。

β-簡約

ベータ簡約（ベータ変換とも）の基本的なアイデアは、関数の適用である。ベータ簡約は以下の変換である。

((λV. E) E′) →^β E[V := E′]

ただし、 E′ の代入によって E′ 中の自由変数が新たに束縛されることがないときに限る。

関係 == は、上の2つの規則を含む最小の同値関係(同値閉包)である。

ベータ簡約は、（同値関係ではなく）左辺から右辺への一方的な変換であると見ることもできる。ベータ簡約の余地のないラムダ式、つまり、 ((λV. E) E′) の形(β-redex)をどこにも持っていないラムダ式を正規形（英: normal form）であるという。

η-変換

上に挙げた2つの規則の他に、第3の規則としてイータ変換が導入されることがある。イータ変換の基本的なアイデアは、関数の外延性である。ここでいう外延性とは、2つの関数が全ての引数に対して常に同じ値を返すようなとき、互いに同値であるとみなすという概念である。イータ変換は以下の変換である。

λV. E V →^η E

ただし、 E に V が自由出現しないときに限る。

この同値性は関数の外延性という概念によって以下のように示される。

もし全てのラムダ式 a に対して f a == g a であるならば、 a として f にも g にも自由出現しない変数 x をとることによって f x == g x であり、 λx. f x == λx. g x である。この等式にイータ変換をほどこすことによって f == g が得られる。これより、イータ変換を認めるならば関数の外延性が正当であることが示される。

逆に、関数の外延性を認めるとする。まず、全ての y に対してラムダ式 (λx. f x) y はベータ変換でき、 (λx. f x) y == f y となる。この同値関係は全ての y について成り立っているので、関数の外延性より λx. f x == f である。以上によって、関数の外延性を認めたときのイータ変換の正当性が示される。

計算論的性質

計算可能性とラムダ計算

自然数から自然数への関数 F: N → N が計算可能であるということは、全ての自然数の対 X, Y に対して F(X) = Y と f x == y が同値となるようなラムダ式 f が存在すること、と定義することができる。ここで、 x, y はそれぞれ X, Y に対応するチャーチ数によるラムダ式である。この定義は、計算可能性を定義する多くの方法のうちのひとつである。より詳しくは、チャーチ-チューリングの提唱の項を見よ。

チャーチ・ロッサー性

一般にラムダ式の中にβ-変換できる部分式が複数ある場合、どこから評価を行うかによって評価の経過は複数存在する。それらの複数の経過からさらに評価することによって、同じラムダ式を得られる性質をチャーチ・ロッサー性、もしくは合流性と呼ぶ（チャーチ・ロッサーの定理）。また、あるラムダ式から一回のβ-簡約によって得られた二つのラムダ式が、同じラムダ式にβ-変換されるという性質は弱チャーチ・ロッサー性と呼ばれる。チャーチ・ロッサー性を持つ体系は弱チャーチ・ロッサー性も持つが、逆は必ずしもなりたたない。

チャーチ・ロッサー性は本稿で取り扱っている型無しラムダ計算の体系では成立することが知られている。しかしその他の体系、例えば型を付けて拡張されたラムダ計算の体系などに関しては、必ずしも成り立つとは限らない。

評価戦略

ラムダ式を簡約する際、複数の簡約可能な箇所（β-redex）が存在する場合、どの順序で簡約を行うかによって、計算の終了性や効率が異なる場合がある。代表的な評価戦略（リダクション戦略）として以下が挙げられる。

正規順序評価 (Normal-order reduction): 最も左外側にある β-redex を常に最初に簡約する戦略。「名前呼び出し」（call-by-name）の理論的基礎となる。; 正規順序評価には、もしそのラムダ式に正規形が存在するならば、必ず正規形に到達できる（簡約が停止する）という重要な性質がある。この性質により、停止可能な計算を確実に完了させることができる。プログラミング言語における遅延評価（lazy evaluation）の理論的基盤となっており、Haskellなどの言語で採用されている。; 例：(λx. λy. y) ((λz. z z)(λz. z z)) という式を考える。第二引数 (λz. z z)(λz. z z) は無限ループするが、正規順序評価では外側のλx から簡約するため、この引数は評価されず λy. y という正規形に到達する。一方、作用的順序評価では引数を先に評価しようとして無限ループに陥る。

作用的順序評価 (Applicative-order reduction): 最も左内側にある β-redex を常に最初に簡約する戦略。すなわち、関数の本体に適用する前に、引数を先に正規形になるまで簡約する。「値呼び出し」（call-by-value）の理論的基礎となる。; 多くのプログラミング言語（C言語、Java、ML、Schemeなど）で採用されている先行評価（eager evaluation）に相当する動作である。正規形が存在する場合でも、この戦略では引数の評価が無限ループに陥り、計算が停止しない場合がある。

停止性

β-変換は停止しない（無限ループに陥る）場合がある。例えば次の式を適用する場合には停止しない。

(λx. x x) (λx. x x) →^β (λx. x x) (λx. x x) →^β …

ある種のラムダ計算の体系では、任意のラムダ式に対してβ-変換の停止性が保証されていることがある。どのような順序でβ-変換を行ったとしてもβ-変換が停止する性質を強正規化性といい、β-変換の順序を上手く選んだ場合にβ-変換が停止する性質を弱正規化性という。チャーチ・ロッサー性を満たし、かつ停止性を持つラムダ計算の体系では、ラムダ式をどのような順序で評価しても必ず同じ結果になることがわかる。

強正規化的であり、かつ弱チャーチ・ロッサー性を持つラムダ計算の体系はチャーチ・ロッサー性を持つ（ニューマンの補題（英語版））。

型無しラムダ計算の体系では、ある式の停止性を判断する事は決定不能であることが証明されている。

同値性の決定不可能性

2つのラムダ式を入力とし、それらが同値であるかどうかを判定するアルゴリズムは存在しない。これは決定不可能性が示された歴史的に最初の問題である。ここで使われる「アルゴリズム」という言葉も、もちろんきちんと定義されなければならない。チャーチは自身の証明の中で帰納的関数をその定義に用いたが、現在ではこれは適切なその他のアルゴリズムの定義と等価であることが知られている。

チャーチの証明ではこの問題を、あたえられたラムダ式に正規形が存在するかどうかという問題に帰している。正規形とは、それ以上簡約のできない同値なラムダ式のことである。チャーチの証明ではまず、この問題が決定可能である、つまり、ラムダ式で表現可能であると仮定する。クリーネによる結果とゲーデル数のラムダ式表現を用いることによってチャーチは、対角線論法によりパラドキシカルなラムダ式 e を構成した。この e を、それ自身を表すゲーデル数に適用すると矛盾が導かれる。

詳しくいえば次のようである。まず $X$ を正規形の存在性を判定するラムダ式とする。 $A$ を2つのラムダ式のゲーデル数から、それらを適用してできるラムダ式を計算する関数を表すラムダ式、 $N$ を自然数からそれを表すラムダ式の表現のゲーデル数を求める関数を表すラムダ式とする。すなわち、

A\ulcorner x\urcorner \ulcorner y\urcorner \to ^{\beta }\ulcorner (xy)\urcorner

N\ulcorner x\urcorner \to ^{\beta }\ulcorner \ulcorner x\urcorner \urcorner

が成り立つ。ここで $\ulcorner x\urcorner$ はラムダ式 $x$ のゲーデル数を表すラムダ式の表現である。いま、ラムダ式 $e$ を

e:=\lambda x.{\text{ if }}X(Ax(Nx)){\text{ then }}\Omega {\text{ else }}\lambda y.y

と定める。ここで $\Omega$ は正規形を持たないラムダ式 $(\lambda x.xx)(\lambda x.xx)$ である。自己適用 $e\ulcorner e\urcorner$ を計算すると次のようになる。

e\ulcorner e\urcorner

{\text{ if }}X(A\ulcorner e\urcorner (N\ulcorner e\urcorner )){\text{ then }}\Omega {\text{ else }}\lambda y.y

{\text{ if }}X(A\ulcorner e\urcorner \ulcorner \ulcorner e\urcorner \urcorner ){\text{ then }}\Omega {\text{ else }}\lambda y.y

{\text{ if }}X\ulcorner e\ulcorner e\urcorner \urcorner {\text{ then }}\Omega {\text{ else }}\lambda y.y

もし $e\ulcorner e\urcorner$ が正規形を持つならば、 $e\ulcorner e\urcorner$ は $\Omega$ にベータ簡約される。するとチャーチ・ロッサーの定理より、 $\Omega$ は $e\ulcorner e\urcorner$ と共通のラムダ式にベータ簡約できるから、 $\Omega$ は正規形を持つ。これは矛盾。したがって $e\ulcorner e\urcorner$ は正規形を持たない。すると $e\ulcorner e\urcorner$ は $\lambda x.x$ にベータ簡約されることになる。ラムダ式 $\lambda x.x$ は正規形であるので、やはり矛盾。したがって $X$ のようなラムダ式は存在しない。

数学的モデル

ラムダ計算は構文的な書き換え規則として定義されているが、これを数学的な集合と関数として解釈しようとすると困難が生じる。集合論において、集合 $D$ から $D$ への全ての関数の集合（関数空間）の濃度は、 $D$ の濃度より真に大きくなる（カントールの定理）。そのため、自分自身を引数として取れるような（ $D ≅ D \to D$ となるような）集合 $D$ は、自明なものを除いて通常の集合論の範囲では構成できない。

この問題は、1969年にデイナ・スコットによって、位相空間論に基づく「領域理論」を用いて解決された（スコット領域）。これによりラムダ計算は、単なる記号操作のルールとしてだけでなく、具体的な数学的対象としての意味（表示的意味論）を持つことが示された。

諸概念のラムダ式での表現

ラムダ計算は、チューリングマシンと同等の計算能力を持つチューリング完全な体系であり、計算可能な全ての関数を表現できる。しかし、基本的なラムダ計算の定義には、整数や真理値、データ構造といった具体的な概念は組み込まれていない。

これらの概念は、特定のラムダ式として「エンコード」（符号化）することで表現される。エンコーディングとは、ある数学的対象（例えば自然数）を、その性質を保つようなラムダ式の集合として定義することである。例えば自然数nのエンコーディングは、「ある関数をn回適用する」という操作を表すラムダ式として定義される。このようなエンコーディングが可能であることは、ラムダ計算の表現力の高さを示すとともに、計算の本質が「関数の適用」という単一の操作だけで捉えられることを示している。つまり、整数や真理値などのデータ型、およびそれらに対する操作は、全てラムダ抽象と関数適用の組み合わせとして定義できる。このようなエンコード手法は、ラムダ計算の表現力の高さを示すとともに、計算の本質が「関数」という概念だけで捉えられることを示している。

以下では、自然数、論理値、データ構造（対やリスト）、および再帰といった基本的な概念のラムダ式による表現を紹介する。これらの表現方法には複数の方式が存在するが、ここでは最も広く知られているアロンゾ・チャーチによるエンコード（チャーチ・エンコーディング）を中心に説明する。

自然数と算術

自然数をラムダ式で表現する方法はいくつか異なる手法が知られているが、その中でもっとも一般的なのはチャーチ数（英語版）（英: Church numerals）と呼ばれるもので、以下のように定義されている。

0 := λf x. x

1 := λf x. f x

2 := λf x. f (f x)

3 := λf x. f (f (f x))

以下同様である。直感的には、数 n はラムダ式では f という関数をもらってそれを n 回適用したものを返す関数である。つまり、チャーチ数は1引数関数を受け取り、1引数関数を返す高階関数である。（チャーチの提唱した元々のラムダ計算は、ラムダ式の引数が少なくとも一回は関数の本体に出現していなくてはならないことになっていた。そのため、その体系では上に挙げた 0 の定義は不可能である。）

上のチャーチ数の定義のもとで、後続（後者）を計算する関数、すなわち n を受け取って n + 1 を返す関数を定義することができる。それは以下のようになる。

SUCC := λn f x. f (n f x)

また、加算は以下のように定義できる。

PLUS := λm n f x. m f (n f x)

または単にSUCCを用いて、以下のように定義してもよい。

PLUS := λm n. m SUCC n

PLUS は2つの自然数をとり1つの自然数を返す関数である。例えば、 PLUS 2 3 == 5 となることが計算によって確かめられる。また、乗算は以下のように定義される。

MULT := λm n. m (PLUS n) 0

この定義は、 m と n の乗算は、 0 に n を m回加えることと等しい、ということを利用して作られている。もう少し短く、以下のように定義することもできる。

MULT := λm n f. m (n f)

正の整数 n の先行（前者）を計算する関数 PRED n = n − 1 は簡単ではなく、

PRED := λn f x. n (λg h. h (g f)) (λu. x) (λu. u)

もしくは

PRED := λn. n (λg k. (g 1) (λu. PLUS (g k) 1) k) (λv. 0) 0

と定義される。上の部分式 (g 1) (λu. PLUS (g k) 1) k は、 g(1) がゼロとなるとき k に評価され、そうでないときは g(k) + 1 に評価される^[2]。

論理記号と述語

TRUE や FALSE といった真理値は慣習的に以下のように定義されることが多い。これらはチャーチ真理値（英語版）（英: Church booleans）とよばれている。

TRUE := λx y. x

FALSE := λx y. y

（この FALSE は前述のチャーチ数のゼロと同じ定義であることに注意せよ）

これらの真理値に対して論理記号を定義することができる。たとえば、以下のようなものがある。

AND := λp q. p q FALSE

OR := λp q. p TRUE q

NOT := λp. p FALSE TRUE

IFTHENELSE := λp x y. p x y

これらの記号を使った計算の例を挙げる。

AND TRUE FALSE

= (λp q. p q FALSE) TRUE FALSE →^β TRUE FALSE FALSE

= (λx y. x) FALSE FALSE →^β FALSE

以上より、 AND TRUE FALSE が FALSE と等しいことがわかる。

「述語」とは、真理値を返す関数のことである。計算論において最も基本的な述語は ISZERO で、これは引数がチャーチ数の 0であった場合には TRUE を、そうでなければ FALSE を返す関数であり、以下のように定義できる。

ISZERO := λn. n (λx. FALSE) TRUE

対

（2つ組の）順序対のデータ型は、 TRUE および FALSE を用いて定義することができる。これらはチャーチ対（英語版）（英: Church pairs）とよばれている。

CONS := λs b f. f s b

CAR := λp. p TRUE

CDR := λp. p FALSE

リンク型のリスト構造は、空リストのために特定の予約された値（例えば FALSE ）を用い、リストをその先頭要素と後続リストの CONS 対として表現することによって実現できる。

リストは、順序付けられた要素の列である。ラムダ計算においてリストを表現する手法は複数存在するが、いずれも空リスト（nil）、要素の追加（cons）、先頭要素の取得（head）、残りのリストの取得（tail）といった基本的な操作を定義できる必要がある。

代表的な表現手法として、畳み込み（fold）操作としてリストを定義する「チャーチ・エンコーディング」と、パターンマッチングの考え方に基づく「スコット・エンコーディング」がある。

チャーチ・リスト (Church lists)

自然数をチャーチ数としてエンコードしたのと同様の考え方で、リストもまた関数として表現される。チャーチ・リストにおけるリストとは、2つの引数（畳み込み関数

c

と初期値

n

）を受け取り、リストの各要素に対して

c

を順次適用した結果を返す関数である（これはリストに対する右畳み込み (right fold) 操作に相当する）。

定義は以下のようになる。

\operatorname {nil} \equiv \lambda cn.n

（空リストは初期値をそのまま返す）

\operatorname {cons} \equiv \lambda htcn.c\ h\ (t\ c\ n)

（先頭要素

h

に関数

c

を適用し、残りのリスト

t

の結果と結合する）

これを用いると、例えば要素

x,y,z

を持つリストは以下のように表現される。

\lambda cn.c\ x\ (c\ y\ (c\ z\ n))

この表現では、リストの要素数（length）や総和（sum）、写像（map）などの計算は非常に自然に行えるが、一方で「リストの末尾（tail）」を取得する関数の定義は（チャーチ数における前者の計算と同様に）複雑になり、計算コストが高くなる（

O(n)

）という欠点がある。

スコット・エンコーディング (Scott encoding)

デイナ・スコットによって考案されたこの手法は、リストを「空リストの場合」と「要素がある場合（cons）」の分岐（case analysis）として表現する。

定義は以下のようになる。

\operatorname {nil} \equiv \lambda nc.n

（空リストの場合の処理

n

を選択する）

\operatorname {cons} \equiv \lambda htnc.c\ h\ t

（要素がある場合の処理

c

を選択し、それに先頭

h

と残り

t

を渡す）

この表現では、先頭要素（head）と残りのリスト（tail）の取得が極めて簡単かつ定数時間（

O(1)

）で行える。

\operatorname {head} \equiv \lambda l.l\ \operatorname {undefined} \ (\lambda ht.h)

\operatorname {tail} \equiv \lambda l.l\ \operatorname {undefined} \ (\lambda ht.t)

一方で、mapやfoldのような再帰的な操作を行う場合には、不動点コンビネータ（Yコンビネータ）を明示的に使用する必要がある。

対（ペア）による実装: 前節で定義した「対（cons）」を用いて、LISPのような連結リスト構造をそのまま模倣することも可能である。この場合、空リストを表すための特定の値を定義し（例えば $\operatorname {FALSE}$ ）、リストを「(要素, 次のリスト)」という対の入れ子構造で表現する。

再帰

→「無名再帰」も参照

再帰とは自分自身を関数として使用することで、ラムダ計算では表面上は再帰操作は許されていないように見える。しかし少し工夫することによってラムダ計算でも再帰を実現できる。例として階乗を計算する関数 f(n) を考えてみよう。この関数は再帰的に以下のように定義できる。

f(n) := 1, if n = 0; and n × f(n − 1), if n > 0

ラムダ計算では自分自身を含む関数は定義できない。この問題を解決するためにまず、 f を引数にとり n を引数にとる関数を返すg という関数を考える。

g := λf n. (1, if n = 0; and n × f(n − 1), if n > 0)

関数 g は 1 か n × f(n − 1) を返すような関数を返す。上述の ISZERO や算術、論理記号の定義を用いれば、この関数 g はラムダ式で定義することができる。

しかし、これでは g 自身はまだ再帰的ではない。 g を用いて再帰的な階乗関数を作り出すためには、 g に対して引数 f として渡されている関数が、ある性質を持つ必要がある。すなわち、この f を展開すると関数 g がある一つの引数を伴った形になり、さらにその g への引数は先ほどf として渡された関数に再びなる必要がある。

この性質は言い換えると、 f は g ( f )に展開される必要があるということだ。この g の呼び出しは先ほどの階乗関数に展開され、再帰の段階を一段降りる計算をしている。この展開において、関数 f が再度出現する。そして、この関数 f は再度 g ( f )に展開され、再帰が続いていく。この f = g ( f )となるような関数は、 g の不動点と呼ばれる。そして、この不動点は不動点コンビネータとして知られるものによってラムダ計算で表現することが出来る。この不動点コンビネータは Y と表される -- Yコンビネータ:

Y = λg. (λx. g (x x)) (λx. g (x x))

ラムダ計算では、 Y g は g の不動点となる。つまり、 g (Y g) == Y g となる。このもとで、 n の階乗を計算するには単に g (Y g) n を呼び出せばよい。ここで、 n は上述したチャーチ数である。

n = 5 として、評価の例を見てみよう。

(λn.(1, if n = 0; and n·((Y g)(n − 1)), if n > 0)) 5

1, if 5 = 0; and 5·(g(Y g)(5 − 1)), if 5 > 0

5·(g(Y g) 4)

5·(λn. (1, if n = 0; and n·((Y g)(n − 1)), if n > 0) 4)

5·(1, if 4 = 0; and 4·(g(Y g)(4 − 1)), if 4 > 0)

5·(4·(g(Y g) 3))

5·(4·(λ n. (1, if n = 0; and n·((Y g)(n− 1)), if n > 0) 3))

5·(4·(1, if 3 = 0; and 3·(g(Y g)(3 − 1)), if 3 > 0))

5·(4·(3·(g(Y g) 2)))

...

このように、アルゴリズムの構造が再帰的に評価される。再帰的に定義される関数は全て他の適当な関数の不動点となっているため、 Y を用いることで全ての再帰的な関数をラムダ式で表現することができる。たとえば、自然数に対する除算、乗算や比較述語を再帰を用いてよりきれいに定義することができる。

型付きラムダ計算とカリー＝ハワード同型対応

ラムダ計算に型を導入した体系（単純型付きラムダ計算など）は、証明論との間に密接な関係を持つことが知られている。

カリー・ハワード対応（Curry-Howard correspondence / Curry-Howard isomorphism）は、型付きラムダ計算と直観主義論理の間に存在する深い構造的対応関係を指す。この対応関係は以下のように要約される。

型は命題に対応する
プログラム（ラムダ項）は証明に対応する
型付け可能性（あるプログラムに型が付けられること）は証明可能性（ある命題が証明できること）に対応する

具体的には、

型 $A \to B$ （A型の引数を取りB型を返す関数の型）は、論理式 $A \Rightarrow B$ （「AならばB」という含意）に対応する
関数抽象（ $λx:A.M$ ）は、仮定Aの下で結論Bを導く含意導入規則に対応する
関数適用（ $M N$ ）は、推論規則におけるモーダスポネンス（前件肯定、含意除去）に対応する
直積型（ $A \times B$ ）は論理積（ $A \land B$ ）に、直和型（ $A + B$ ）は論理和（ $A \lor B$ ）に対応する

形式的検証と定理証明

型付きラムダ計算とカリー・ハワード対応の発見は、ソフトウェアの正当性を数学的に保証する技術（形式的検証）や、数学の定理をコンピュータ上で証明するシステム（定理証明支援系）の発展をもたらした。これらシステムの多く（Coq、Agda、Leanなど）は、内部言語として強力な型システムを持つラムダ計算（Calculus of constructions（英語版）など）を採用している。

システムF（多相ラムダ計算）

単純型付きラムダ計算を拡張した体系として、ジャン＝イヴ・ジラールとジョン・C・レイノルズ（英語版）が独立に発見した「System F」（二階ラムダ計算）がある。

単純型付きラムダ計算では、例えば「引数をそのまま返す関数（恒等関数）」であっても、整数用（int -> int）と真理値用（bool -> bool）で個別に定義する必要があった。 System Fでは、型そのものを変数（型変数）として扱い、型について抽象化を行うことができる。これにより、「あらゆる型 $\alpha$ について、型 $\alpha$ の引数を取りその値を返す関数」という、多相的な恒等関数が定義可能になる。

実装技術

ラムダ計算を計算機上で実装する際、変数名の衝突を避けるための α-変換の実装は煩雑かつコストがかかる処理となる。この問題を回避する手法として、オランダの数学者ニコラース・ホーバート・ド・ブランによって考案された「ド・ブラン・インデックス（de Bruijn index）」がある。

ド・ブラン・インデックスでは、変数を名前ではなく「その変数を束縛している λ が、内側から数えて何番目にあるか」という相対的な自然数のインデックスで表現する。例えば、 λx. (λy. x y) という式は、 λ (λ 2 1) と表現される（ここで '2' は2つ外側の λ を指し、 '1' は直近の λ を指す）。この表記法を用いることで、α-変換（変数名の付け替え）が不要となり、2つのラムダ項が同値であるかの判定（α-同値性）が単なる項の構造比較だけで行えるようになる。

ラムダ計算とプログラミング言語

ピーター・ランディン（英語版）は1965年に発表したA Correspondence between ALGOL 60 and Church's Lambda-notationにおいて、ラムダ計算が手続的な抽象化と手続き（サブプログラム）の適用のしくみを提供しているがために、多くのプログラミング言語がラムダ計算にその基礎を置いているとみることができるとしている。

ラムダ計算をコンピュータ上に実装するには、関数を第一級オブジェクトとして取り扱う必要があり、これはスタック・ベースのプログラミング言語においては問題となってくる。これはFunarg問題として知られている。

ラムダ計算と最も密接な関係をもつプログラミング言語は関数型言語と呼ばれる諸言語である。初期のLISP（LISP 1.5など）は関数の定義にラムダ記法を採用したが、その変数の扱いは「動的スコープ」（dynamic scope）であり、本来のラムダ計算が定義する「静的スコープ」（lexical scope / static scope）とは異なる動作をしていた。静的スコープでは、変数は定義された場所（字句的な位置）によって束縛先が決まるのに対し、動的スコープでは実行時の呼び出し順序によって束縛先が決まる。これは、ジョン・マッカーシーがLISPの実装において、当時の計算機の制約や実装の簡便性を優先したためである。マッカーシー自身はラムダ計算の理論を理解していたが、実用的な理由から静的スコープの実装を見送った。

この不一致により、初期のLISPでは関数を引数として渡す際などに予期せぬ変数の衝突（Funarg問題）が発生した^[3]。後にScheme（1975年）がガイ・スティールとジェラルド・ジェイ・サスマンによって開発され、ラムダ計算のモデルに忠実な静的スコープを採用したことで、ラムダ計算はプログラミング言語の理論的基盤として定着した。現在では、HaskellやMLなど多くの関数型言語がラムダ計算を基礎としている。

関数を第一級オブジェクトとして扱えるのは関数型言語だけというわけではない。Pascal、C、C++などの命令型言語でも、関数ポインタや関数オブジェクトを用いることで、関数を他の関数の引数として渡すことが可能であった。

さらに、2000年代以降の多くの主要なプログラミング言語においては、ラムダ計算に由来する無名関数（ラムダ式）の記法や機能が標準的に取り入れられている。C#（デリゲートおよびラムダ式）、C++（C++11以降）、Java（Java 8以降）、JavaScript（アロー関数）、Pythonなどがその例である。これらの言語では、無名関数を生成し、変数に代入したり、高階関数の引数として渡したりすることが容易に行えるようになっている。

例えば、引数 x を受け取りその二乗を返すラムダ式 λx. x * x は、JavaScriptでは x => x * x、Pythonでは lambda x: x * x のように記述され、これは第一級オブジェクトとして扱われる。

並行性

ラムダ計算のチャーチ・ロッサー性は、評価（β-簡約）をどの順序で行っても、さらには同時に（並行に）行ってもよいことを意味している。（より詳しくいえば、ラムダ計算は参照透過である。）このため、ラムダ計算を用いて種々の非決定的評価戦略をモデル化することができる。並列性や並行性をモデル化するためのより強力な手法として、Communicating Sequential Processes（CSP）、w:calculus of communicating systems（CCS）、パイ計算、アンビエント計算などのプロセス計算がある。

コンビネータ論理との関係

ラムダ計算と密接に関連する計算体系として、モーゼス・シェーンフィンケルとハスケル・カリーによって発展した「コンビネータ論理」がある。ラムダ計算が変数と抽象化（λ）を用いるのに対し、コンビネータ論理は変数を一切使用せず、いくつかの基本的な関数（コンビネータ）の組み合わせだけで全ての計算可能な関数を表現する。

特に有名なのは S と K という2つのコンビネータを用いた SKIコンビネータ計算である。

$K x y = x$ （定数関数を作る）
$S x y z = x z (y z)$ （引数を分配する）

任意のラムダ式は、これら S と K （および恒等関数 I）の組み合わせに変換することができ（ブラケット抽象）、逆にコンビネータの式はラムダ計算のサブセットと見なすことができる。この事実は、計算というプロセスから「変数」という概念を完全に排除できることを示唆しており、理論的な興味深さだけでなく、関数型言語の実装（グラフ簡約など）にも応用されている。

言語学への応用

ラムダ計算は計算機科学のみならず、言語学（特に形式意味論）の分野でも重要な役割を果たしている。 1970年代、論理学者のリチャード・モンタギューは、自然言語の意味を論理学的に記述する手法（モンタギュー文法）を提唱した。彼は、文の構成要素（名詞句や動詞など）が持つ意味をラムダ式として表現し、それらの関数適用によって文全体の意味が構成されることを示した。

例えば、他動詞 "loves"（愛する）は、目的語 x と主語 y を取り、命題 loves(y, x) を返す関数として、以下のようにモデル化されることがある。

\lambda x.\lambda y.loves(y,x)

このように、ラムダ計算は「言葉の意味」を厳密に計算可能な形式で捉えるための標準的なツールとして、自然言語処理や人工知能の分野でも参照されている。

参考資料

計算論計算可能性とラムダ計算コンピュータサイエンス大学講座高橋正子 (著) 近代科学社 ISBN 4764901846 (1991)
ハロルド・エイブルソン、ジェラルド・ジェイ・サスマン、ジュリー・サスマン共著『計算機プログラムの構造と解釈　第二版』和田英一訳、ピアソンエデュケーション、2000、ISBN 4-8947-1163-X

この記事は2008年11月1日以前にFree On-line Dictionary of Computingから取得した項目の資料を元に、GFDL バージョン1.3以降の「RELICENSING」(再ライセンス) 条件に基づいて組み込まれている。

脚注

^ 例えば、自己適用 (λx. x x)(λx. x x) のような式は型付き体系では許されないが、型無しラムダ計算では記述可能である。
^ “チャーチ数とpred関数”. kimiyuki.net. 2018年10月6日閲覧。
^ Funarg問題は「関数的引数問題」（functional argument problem）の略で、動的スコープを持つ言語で関数を第一級オブジェクトとして扱う際に生じる意味論上の問題を指す

典拠管理データベース
国立図書館	ドイツアメリカフランス BnF data ラトビアイスラエル
その他	IdRef Yale LUX

歴史