ラムダ計算とは
ラムダ記法を使って関数をいろいろといじる (?) ものです。関数型プログラミングなどのもとになっていて、チューリング完全です。
ラムダ記法とは
下のような感じで $\lambda$ <引数> . <式> と表します。
下の例を見てください ($普通の記法→ラムダ記法$ といった感じで書いています)
f(x) = y→ \lambda x.y
またカッコが多すぎると見づらいので
( \lambda x_1.( \lambda x_2.( \lambda x_3.(・・・(x_n.M)・・・))))→ \lambda x_1x_2x_3・・・x_n.M
((・・・((M_1M_2)M_3)・・・)M_n) → M_1M_2M_3・・・M_n
のように略すことができます。
例えば $f(x, y)= x+y→ \lambda xy.(x+y)$ といった具合です。
ラムダ計算
ラムダ式
ラムダ計算はラムダ式で表されるものを扱っていて、ラムダ式は次のように定義されています。
- 変数 ($x_0$, $x_1$ 等) はラムダ式です
- $( \lambda x.M)$ もラムダ式です (ただし、 $M$ はラムダ式、 $x$ は変数とする)
- $(MN)$ もラムダ式になっています。 (ただし $M$, $N$ はラムダ式)
ここでは、基本的に大文字 ( $L$, $M$, $N$ 等) はラムダ式 (もちろん変数もラムダ式なので、変数である可能性もあります。) を、小文字 ($x$, $y$, $z$ や $x_0$, $x_1$, $x_2$ 等)は変数を表すこととします。
これで何をするのか？
ラムダ式だけあっても、評価できないと意味がないので評価するための規則が2つあります。(η変換というのを含める場合もあり、そうすれば3種類となるが今回は扱わない。)
2つとは、α変換とβ変換のことです。
α変換
簡単に言えば、変数の名前を変えてもいいよってことです。それはそうですね。例えば、 $ \lambda xy.x $ を $ \lambda zy.z $ にしても意味は変わりません。もちろんかぶらないように変える必要があって、さっきの例では $ \lambda yy.y $ っていうわけには行きません。
β変換
ラムダ式の真髄みたいなとこです。 $( \lambda x.M)N$ は $L$ (ただし、 $L$ は $M$ のなかの $x$ を $N$ に変えたもの) に変えられるよっていうことです。ベータ変換は何度でもすることができます。ベータ変換を $ \underset{β}{→} $ で表します。
たとえば次のような感じです。
( \lambda x.x)z \underset{β}{→} z
( \lambda xy.x)z \underset{β}{→} ( \lambda x.( \lambda y.x))z \underset{β}{→} \lambda y.z
(( \lambda xy.yx)z_1)z_2 \underset{β}{→} ( \lambda y.yz_1)z_2 \underset{β}{→} z_2z_1
複数回のベータ変換は $ \underset{β}{↠} $ で表すことができます。
(( \lambda xy.yx)z_1)z_2 \underset{β}{↠} z_2z_1
といった感じです。
β変換できる部分をβ基と呼びます。たとえば $ \underline{( \lambda x.x)(( \lambda y.y) z)} $ と $ ( \lambda x.x)( \underline{( \lambda y.y)z)})$ のように (下線部分がβ基) β基が複数ある場合もあり、どちらで変換することもできます。β変換を繰り返しもうβ基がなくなった状態を正規形 (β-nf) と呼びます。すべてのラムダ式に正規形があるわけではなくあるものもないものもあります。
Church-Rosser の定理と、正規化定理
まず Church-Rosser の定理について説明します。なんか難しそうな名前ですが、話は簡単で、一つのラムダ式からβ変換を繰り返してできた別の2つのラムダ式は、β変換を繰り返せばまた合流することが可能であるということです。
言い換えれば任意のラムダ式 $K$ について $K \underset{β}{↠}M, K \underset{β}{↠}N $ が成り立つならば $M \underset{β}{↠}L, N \underset{β}{↠}L$ をみたすラムダ式 $L$ が存在するということです。
では、正規化定理を説明します。正規化定理とはあるラムダ式 $N$ が β-nf を持つとき、常に一番左にあるβ基をβ変換していけばβ基になるという定理です。
定理の証明等などは調べたら出てくると思うので、興味があったらぜひ調べてみてください。
ラムダ式の応用
ラムダ式で自然数や演算、条件分岐等についてやりたいと思います。
数
多分基本です。
$0$ : $ \lambda fx.x$
$1$ : $ \lambda fx.fx$
$2$ : $ \lambda fx.f(fx)$
$3$ : $ \lambda fx.f(f(fx))$
........
といった感じで続いていきます。
演算等
インクリメント (+1)
$ [suc] $ = $ \lambda nfx.f(nfx)$
インクリメントするには $ \lambda fx.f(fx)$ から $ \lambda fx.f(f(fx))$ とかえるように、$f( )$ を一つ増やせば良いです。とりあえず $ \lambda fx.f(fx)$ から $ f(fx)$ にするために $( \lambda fx.f(fx))fx$ します。 ( $( \lambda fx.f(fx))fx \underset{β}{↠}f(fx)$ ) それを $f()$ でつつんであげれば $ \lambda fx.f(f(fx))$ となり以上のことをやると $ [suc] $ のようになります。
足し算
$ [add] $ = $ \lambda mn. m [suc] n$
たとえば、 $2+3$ だと
[add] 2 3 \underset{β}{↠} 2[suc]3 \underset{β}{↠} \lambda fx.f(fx) [suc] 3 \underset{β}{↠} \lambda x.[suc]([suc]x)3
$ \lambda x. [suc] ( [suc] x) $ はxに2回インクリメントする関数となっています。このように $n[suc]$ は $n$ に $f$ が $n$ 個あり、それが $[suc]$ に変わるので $n$ 回インクリメントする関数ができるのだと考えられます。
\lambda x.[suc]([suc]x)3 \underset{β}{↠} 5
となり足し算に成功しました。
掛け算
$ [mul] = \lambda mn.m([add]n)0$
先ほどと同様にして $m([add]n)$ が、 $m$ 回 $n$ を加える関数となり、 $0$ に $n$ を $m$ 回足すので $m*n$ が求められる。
デクリメント (-1)
$ [PRE] = \lambda nfx.n(λgh.h(gf))(λu.x)(λu.u)$
僕は馬鹿だったので何をやっているのかはわからなかったですが、これでうまく行くそうです。
True or False
$ [TRUE] = λxy.x$
$ [FALSE] = λxy.y$
IF
$ [条件][trueの場合の処理][falseの場合の処理] $
[TRUE]と[FALSE]の定義より自明です。
AND と OR
$ [AND] = λxy.xy[FALSE]$
$ [OR] = λxy.x[TRUE]y$
$ [NOT] = λp.p[FALSE][TRUE]$
試せば解ると思います。
おわりに
お読みいただきありがとうございます。部誌に書くのは初めてなのであまり個人的な考察などはかけず、いろいろとまとめただけって感じになってしまったので、来年はもう少し自分の考察等も入れたいなと思います。多分 @Linuxmetel で Qiita の方にも投稿するのでよかったら LGTM 等もお願いします。
参考文献
- Wikipedia 日本語版 「ラムダ計算」
- 計算論 ー計算可能性とラムダ計算ー ISBN 4-7649-0184-6