λ記法とは何か

プログラマの視点からはλ記法は無名関数を記述できる一種の魔法だ。さらに、無名関数で再帰的定義を可能にする Y コンビネーターのようなものが出てくると、ますます魔法の呪文感が強くなってくる。

しかし、λ計算の本質を考えると、それは、等価な記号列を作るための簡潔な規則でしかない。つまり、λ計算の本質とは、ある文字列からそれと等価な文字列を作るための記号の置き換えの規則に過ぎないのだ。おまけにその規則は3つしかない。つまりα-変換、β-簡約、η-変換の3つだ。λ計算はこれらの規則を使って、等価な文字列を次々に作って行くという意味しかない。

α-変換と言っても単なる変数名の付け替えだし、β-簡約は変数を値で置き換えることで、η-変換は関数 X の変数を表に出すか出さないか、つまり λx.X x = X という置き換え規則でしかない。

λ記法でプログラムが書けるように思えるのは、コンパイラやインタープリターが勝手に文字列を解釈して実行するからだ。λ計算自体は単なる記号の置き換えでしかない。Haskell や Scheme でラムダ記法で書いたプログラムが動いたり動かなかったりするのは、その記号列をそれらの処理系が意味論的に翻訳する時の問題で、ラムダ記法は本来は意味論とは無関係な統語論的な規則なのだ。

統語論的という意味は、その記号列にプログラムとしての意味があるかどうかは無関係に、記号の置き換えのルールに従って記号を置き換えて等価な記号列に変形していくということだ。

たとえば、つぎのような Y コンビネータには (x x) のような関数の自己適用があったりして呪文感が半端ないが、

Y = (λf . (λx . f (x x)) (λx . f (x x)))

Y を任意の関数 g に関数適用して不動点 Yg を作り出すことの証明は、単に変数を引数で置き換えたり、その逆をやったり、変数の名前を付け替えたりしているに過ぎない。

Y g
= (λf . (λx . f (x x)) (λx . f (x x))) g(Yの定義より)
= (λx . g (x x)) (λx . g (x x))(λfのβ簡約、主関数をgに適用)
= (λy . g (y y)) (λx . g (x x))(α変換、束縛変数の名前を変える)
= g ((λx . g (x x)) (λx . g (x x)))(λyのβ簡約、左の関数を右の関数に適用)
= g (Y g)(第2式より)

これは中学校のときに習った2次方程式 ax^2 + bx + c = 0 の一般解を求める時の操作と同じことをしているだけだ。

したがって、関数の自己適用 (x x) のようなものもその意味を考える必要はないのだ。自己適用のある関数 (x x) を更に自己適用する ((f (x x)) (f (x x))) という不可思議な呪文も、単に文字列として捉えれば、それを等価変換していくと Y g = g (Y g) という不動点にたどり着くだけのことだ。

このようにλ計算そのものは単に記号の置き換えだと考えると、そこにはなんの不思議な事もない。しかし、関数の自己適用とは何かなどと、(x x) の意味論まで考えてしまうと、迷宮に迷い込んでしまう。

このように、λ計算は記号列の統語論的な変換規則なのだと割り切ってしまうと、その意味が理解しやすくなる。

[PR]
by tnomura9 | 2017-11-13 06:36 | ラッセルのパラドックス | Comments(0)
<< Z - コンビネータ 万物は数である >>