ラムダ計算
(lambda calculus から転送)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2026/02/05 04:00 UTC 版)
|
この記事には参考文献や外部リンクの一覧が含まれていますが、脚注による参照が不十分であるため、情報源が依然不明確です。
|
ラムダ計算（ラムダけいさん、英語: 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 を、それ自身を表すゲーデル数に適用すると矛盾が導かれる。
詳しくいえば次のようである。まず 
- lambda calculusのページへのリンク
