ラムダ計算の公理とかはすっ飛ばして、ラムダ計算で実際にどうプログラムを組めるのかをまとめてみました。ラムダ計算による数値の扱い、条件分岐、論理式、ループ構造、そしてリスト構造の作り方について説明します。
ちなみに
β→はβ簡約、
λx.xはラムダ抽象、
M Nは、式の適用です。
=は、ここでは、同値を表す表現とします。
適宜applyの優先順位を表す為に括弧を用います。
例えば、λabc. x y zなど、ラムダ抽象は簡単のため、カリー化される前のた式として表します。(訂正 2016/05/02, λabc. x y z = λa.(λb.(λc. x y z))という意味です。)
1.チャーチ数
まず、最初は数値です。チャーチ数とは、ラムダ式で自然数を表現する方法です。ラムダ計算は、数値を扱うことができないように見えますが、ちゃんとした（？）数値計算を自身の計算体系のみで表現することができます。
まずは、数値の定義方法から紹介します。
0と1は、次のようにして定義します。
0 = λfx. x
1 = λfx. f x
ラムダ抽象の中で何回fがapplｙされるかで、数値を表します。2以降は、
2 = λfx. f (f x)
3 = λfx. f (f (f x))
4 = λfx. f (f (f (f x)))
n = λfx. f ( ... (f x) ...) (fがn個)
........
以上のようにして表現します。これだけだと表現しているだけですね。なぜ、このように表現するのか、必然性が無いと感じられるかも知れません。
しかし、これに数値計算方法を組み合わせると面白くなってきます。
加算は、次のように表します。
plus = λmnfx. m f (n f x)
なんとなくイメージがつかめると思います。mとnが足し合わせる値です。mの内側にnを突っ込むようなイメージです。元の数値表現に戻ることが確認できるかと思います。
こんな感じです。
意味 : 1+2
(plus 1 2)
β→ (λmnfx. m f (n f x)) (λfx. f x) (λfx. f (f x))
β→ (λnfx. (λfx. f x) f (n f x)) (λfx. f (f x))
β→ (λfx. (λfx. f x) f ((λfx. f (f x)) f x))
β→ (λfx. (λx. f x) ((λfx. f (f x)) f x))
β→ (λfx. f ((λfx. f (f x)) f x)))
β→ (λfx. f ((λx. f (f x)) x)))
=3となります。
乗算も簡単です。
mult = λmn. m (plus n) 0
ラムダ抽象mが囲っているそれぞれのfに対して、plus nを適用して展開させます。
最後に指数です。mのn乗とは次のように記述します。
exp = λmn. m (mult n) 1
乗算と同じ考え方で、指数も表現出来ました。
次に、定番なので、インクリメントを表す関数とデクリメントを表す関数を書いてみます。
インクリメントを表す関数succは、以下のように定義できます。succという名前はペアノの公理に由来します。
succ = λnfx. f(n f x)
デクリメントを表す関数predは、以下のように定義できます。ちょっと複雑ですね、理解に苦しみます。
pred = λnfx. n (λgh. h (g f)) (λy. x) (λy. y)
意味 : 2 - 1
pred 2
β→ (λnfx. n (λgh. h (g f)) (λy. x) (λy. y))(λfx. f (f x))
β→ (λfx. (λfx. f (f x)) (λgh. h (g f)) (λy. x) (λy. y))
β→ (λfx. (λx. (λgh. h (g f)) ((λgh. h (g f)) x)) (λy. x) (λy. y))
β→ (λfx. (λx. (λh. h (((λgh. h (g f)) x) f))) (λy. x) (λy. y)
β→ (λfx. (λh. h (((λgh. h (g f)) (λy. x)) f)) (λy. y))
β→ (λfx. (λy. y)(((λgh. h (g f)) (λy. x)) f))
β→ (λfx. (((λgh. h (g f)) (λy. x)) f))
β→ (λfx. ((λh. h ((λy. x) f)) f))
β→ (λfx. f ((λy. x) f))
β→ (λfx. f (x))
こんな感じでしょうか。括弧を調整しようとすると目がしょぼしょぼします。とりあえず、デクリメントの関数ができたので、これを使って減算ができます。
減算は次の様になります。
sub = λmn. n pred m
あっけないです。m-nを表す関数でした。λfx. f(...f(x)...)でネストしてるfをpredに置き換え、xをｍに置き換えています。これにより、predがn回mに対して適用される仕組みです。
注意 : この方法だと, sub 1 2 を簡約すると0になります. 上記の定義では, 負の数は扱えません.(2015/01/30追記, アンダースタンディング・コンピューテーションより.)
同様の仕組みで、加算も定義ができます。predのところをsuccに変えるだけです。
plus = λmn. n succ m
2.分岐構造
いわゆるif-else文をラムダ計算で表すことができます。次のように記述します。
true = λxy. x
false = λxy. y
if = λcxy. c x y
if は、一番目の式にtrue/falseを表す要素を受け取り、二番目にtrueだった場合の式を受け取り、三番目にfalseだった場合の式を受け取ります。trueは、2つ式を受け取り、受け取った式のうち、前の式を返します。逆にfalseは、後ろの式を返します。これでif-elseが成立しています。trueやfalseが適宜、ifに与えられた不要な式を切り捨てることでうまく表現することができるようになるのです。
if true A Bについて、次のように簡約されていきます。
(((λcxy. c x y) (λxy. x)) A B)
β→ (((λxy. (λxy. x) x y)) A B)
β→ (((λy. (λxy. x) A y)) B)
β→ ((λxy. x) A B)
β→ ((λy. A) B)
β→ A
正しくtrueの方が選択されていますね。
3.論理式
if-else についてやると今度は、notやandとかorについてもやってみたくなるが人情だと思います(?)。そこで、ラムダ計算でnot, and, orを表してみます。
not = λx. x false true
and = λxy. x y false
or = λxy. x true y
xor = λxy. x (not y) y
notは、if文と原理的には同じです。andは、第一引数がfalseならfalse、trueなら、第二引数の値を返します。orは、逆で、第一引数がtrueならtrue、falseなら、第二引数の値を返します。なかなか、うまく表現できています。xorは、and, not, orを使っても書けるので、特に必要無いような気もします。
4.数値判定
数値判定、具体的には、iszero?やequals?について判定するようなプログラムもかけちゃいます。数値表現とtrue/fasleができるようになったので、ここで紹介します。
まずは、与えられた数値が0かどうかを判定するiszero?から。
iszero? = λz. z (λx. false) true
iszero? 1
β→ (λz. z (λx. false) true) (λfx. f x)
β→ ((λfx. f x) (λx. false) true)
β→ ((λx. (λx. false) x) true)
β→ ((λx. false) true)
β→ false
こんな感じでfalseをちゃんと返してくれます。iszero? 0の場合は自明ですね。0は、二番目に与えられたラムダ式を返す式と考えれば良いので、二番目のラムダ式=trueが帰ってきます。
次に、あんまり扱われることのないequal?について実装してみたいと思います。その前に、mはn以上であるということを判定するgreater than equalについて実装する必要があります。名前は長いので、gte?にしましょう。
gte? = λmn. iszero? (sub n m)
より、equals?は、
equals? = λmn. and (gte? m n) (gte? n m)
だとわかります。
5.ループ構造
ラムダ計算における、代表的なループ構造は、Yコンビネータと呼ばれるものです。if式と比較して若干難しいかも知れませんが、気のせいです。
Y = λf. (λx. f (x x)) (λx. f (x x)))
このように定義されるのですが、これに何か値を渡して、β簡約すると面白いことが起きます。
(λf. (λx. f(x x)) (λx. f(x x))) A
β→ (λx. A(x x)) (λx. A(x x)))
β→ A((λx. A(x x)) (λx. A(x x))))
β→ A(A((λx. A(x x)) (λx. A(x x)))))
β→ A(A(A((λx. A(x x)) (λx. A(x x))))))
β→ A(A(A(A((λx. A(x x)) (λx. A(x x)))))))
一度目のβ簡約では、自由変数fを記号Aに置き換えただけです。しかし、二度目のβ簡約では、先頭のラムダ式のxを後続のラムダ式に置き換えると、何も変化させていないように見えるのですが、実はよく見ると元の形に戻っています。
(x x)のxを (λx. A(x x))に置き換えています。
上記のようにして、無限にAを適用出来るため、この形の式がループ構造として用いることができるのです。
上記の式ではβ簡約をいくら続けても止まりません。無限ループってやつですね。
一般にこのようなコンビネータを不動点コンビネータ(もしくは、フィックスなど)と呼びます。
上記の例以外にも次の式もまた、不動点コンビネータです。
Θ = (λxy. y(xxy)) (λxy. y(xxy))
このようにして、ラムダ計算では、ループを定義します。
ここで一瞬、普通の再帰呼び出しでもループを定義できるのでは？ と思うかもしれませんが、気のせいです。通常のプログラミング言語の再帰呼び出しの場合、自分自身の参照を呼び出し時にスコープが捉えています。しかし、ラムダ計算では、自分自身に付けられた名前が参照できるのは、それ自身が引数として与えられたラムダ抽象の内側だけです。したがって、ラムダ計算では直接的な再帰呼び出しを使うことができないのです。残念ですね。
例えば、以下の例で、
(λx. a b c ...) (λy. x y z ...)
右側のラムダ抽象で再帰呼び出しを行う場合、自分自身の名前を参照したいのですが、参照できるのは、左側のラムダ抽象だけです。こんな感じの違いがあります。
6.素朴なリスト構造
関数型プログラミングにリスト構造は必須です。というか、リスト構造があれば、他の構造はリスト構造でだいたい間に合います。唯一データ構造的に不可能なのは、ハッシュマップくらいでしょうか。
Lispでは、car/cdrとconsセルにお世話になっていますが、ラムダ計算においても、基本的にそのスタイルは変わっていません。consで、リストを作って、carとcdrでリストの要素にアクセスするだけです。
carは、与えられたリストの先頭の要素を取り出します。
cdrは、与えられたリストの後続の要素を取り出します。
consは、第一引数を第二引数で与えられたリストの先頭に付加します。
例えば、ls = (cons 1 (cons 2 '())で、ls = (1 2)のリストが生成されます。これに対して、(car ls) = 1であり、(cdr ls) = (2)です。Lispでcdrは基本的にリストを返しますし、ここでも2を要素に持つリストが帰ってきていますが、別に要素を返しても問題ありません。(注：イコールは同値関係を表しています。)
ラムダ計算で上記３つのオペレータを表現するわけですが、実に可愛いものです。
car = λx. x true
cdr = λx. x false
cons = λabf. f a b
これだけで、原理は、if-else式と似ていますね。consでリストの先頭要素と後続要素をエンクロージングして、最後に、carかcdrを与えて要素を取り出します。
例えば、次のconsとcdrを使うとこうなります。
意味 : (cdr (cons 1 2))
((λx. x false) ((λabf. f a b) 1 2))
β→ ((λx. x false) ((λbf. f 1 b) 2))
β→ ((λx. x false) (λf. f 1 2))
β→ ((λf. f 1 2) false)
β→ (false 1 2)
β→ 2
要素が取り出せていることが確認できるでしょうか。carの場合は、falseがtrueになるだけなので、根本的な違いはありません。
ところで、このリストには、まだnilが足りません。リストの終端を表してくれる大事な記号です。
この記号と、この記号を判定する関数を用意しましょう。
nil = false
isnil? = λx. x (λabc. false) true
こんなので本当にnilと判定してくれるのでしょうか……。とりあえず、isnil?に渡された値がnilであれば正確に判定してくれることは見ればわかります。
(isnil? (cons 1 nil))についてテストしてみましょう。
(isnil? (cons 1 nil))
β→ ((λx. x (λabc. false) true) (cons 1 nil))
β→ ((λx. x (λabc. false) true) ((λabf. f a b) 1 nil))
β→ ((λx. x (λabc. false) true) (λf. f 1 nil))
β→ ((λf. f 1 nil) (λabc. false) true)
β→ ((λabc. false) 1 nil true)
β→ false
若干β簡約の適用順序に一貫性がないような気がしますが、そこは、チャーチ・ロッサー性ってことで勘弁してもらいましょう。isnil?の真ん中にあるラムダ抽象のabcとは、それぞれリストの先頭(car部)、リストの後続(cdr部)、trueを取り除く為のものだったことがわかります。
これでリストの扱いも完璧になりました。
以上が ラムダ計算のざっくりとした使い方の解説でした。本当はリストの扱い方の別パターンも書きたかったのですが、それを書いていると書き終わりそうにないので、ココらへんで終わります。
ラムダ計算を試すのに専用の処理系(ラムダ計算のエミュレータみたいなもの)は、要りません。Scheme(Racket or Gauche)やその他レキシカルクロージャをサポートしている言語で、無名関数をラムダ関数に見立てれば、簡単にエミュレートできます。ただし、簡約のステップを表示させることはできませんが……
((間違いまたは適切な書き方でなかった為、訂正 2013/07/25) まず、ラムダ計算には、型付きと型なしの2種類あり、型付きのラムダ計算では、上記のような引き算や繰返し構造をそのまま表現することはできません。上記の説明は、型なしのラムダ計算を前提としています。従って、レキシカルクロージャをサポートしていても、型推論をする、HaskellやOCamlのような言語では、直接記述できるのは、加算と乗算など一部の計算だけです。ループに関しては、再帰型を定義することで実装可能になるようです。また、Clojure、SchemeやPythonのようなか動的型付け言語でも、再帰を扱う為には、不動点コンビネータの多相性を保証するようなテクニックが必要で、そのままラムダ式で直接記述できるわけではありません。)
参考文献