ラムダ計算とは何？わかりやすく解説 Weblio辞書

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

ラムダ計算

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/09/17 06:16 UTC 版)

この記事には参考文献や外部リンクの一覧が含まれていますが、脚注による参照が不十分であるため、情報源が依然不明確です。適切な位置に脚注を追加して、記事の信頼性向上にご協力ください。（2020年5月）

ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算模型のひとつで、計算の実行を関数への引数の評価（英語: evaluation）と適用（英語: application）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。

ラムダ計算は1つの変換規則（変数置換）と1つの関数定義規則のみを持つ、最小の（ユニバーサルな）プログラミング言語であるということもできる。ここでいう「ユニバーサルな」とは、全ての計算可能な関数が表現でき正しく評価されるという意味である。これは、ラムダ計算がチューリングマシンと等価な数理モデルであることを意味している。チューリングマシンがハードウェア的なモデル化であるのに対し、ラムダ計算はよりソフトウェア的なアプローチをとっている。

この記事ではチャーチが提唱した元来のいわゆる「型無しラムダ計算」について述べている。その後これを元にして「型付きラムダ計算」という体系も提唱されている。

歴史

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

最初の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 である。以上によって、関数の外延性を認めたときのイータ変換の正当性が示される。

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

上で述べたように、ラムダ計算は計算可能な全ての関数を表現することができる。また、上では 2 + 3 のような算術をラムダ式の一部として用いた。 2 + 3 などは計算可能であるから、もちろんラムダ計算による表現が可能である。もちろん、 2 + 3 以外にも計算可能な全ての関数の表現が可能である。ここではそれらのうちの主なものを紹介する。

自然数と算術

自然数をラムダ式で表現する方法はいくつか異なる手法が知られているが、その中でもっとも一般的なのはチャーチ数（英語版）（英: 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 に評価されることに注意せよ^[1]。

論理記号と述語

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 対として表現することによって実現できる。

再帰

「無名再帰」も参照

再帰とは自分自身を関数として使用することで、ラムダ計算では表面上は再帰操作は許されていないように見える。しかし少し工夫することによってラムダ計算でも再帰を実現できる。例として階乗を計算する関数 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 を用いることで全ての再帰的な関数をラムダ式で表現することができる。たとえば、自然数に対する除算、乗算や比較述語を再帰を用いてよりきれいに定義することができる。

計算可能性とラムダ計算

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

同値性の決定不可能性

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

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

詳しくいえば次のようである。まず $X$

ウィキペディア小見出し辞書

索引トップ用語の索引ランキング