ラムダ計算した
Aizu Advent Calendar 2016(Qiita) 5日目です。
4日目はstringampさんのRubyを使ったWAVファイルのBPM解析 - Qiita
はじめに
ラムダ計算を調べた発端はこのブログ(5年前...)です。
記事中のfib関数はopen recursionと言って開いた再帰関数らしく、OOPの支援によって元の定義を変えずに簡単に拡張することができます。
ただこれをOOPの支援なしで元の定義を変えずに拡張するときはどうするのか、そのときに登場するのがラムダ計算のYコンビネータという不動点演算子と呼ばれるものです。
Yコンビネータは関数の再帰呼び出しを抽象化したもので、これで全ての再帰関数を表現できます。
ただ、この投稿ではラムダ式の基本とYコンビネータの紹介をするだけです。具体的な解決については上の記事内を参照してください。
ラムダ計算ってなに
こういうやつです↓
λx. x
これは「x を受け取って x を返す関数」です。このλx. xのことをラムダ式（ラムダ項）といいます。xという変数もラムダ式です。
次にこれ↓
λx. λf. f x
これは「x を受け取って、f を受け取って f に x を適用したものを返す関数、を返す関数」です。 ちなみにこれと同値です。
λx. λf. f x = λxf. f x
つまり、二つの引数を受け取る関数をカリー化したものが上のラムダ式です。 また、右辺は左辺のラムダ式を略記した形です。
ここで重要なのが、
- 関数には名前が付いていない。
- x や f はただの変数で、その名前は重要じゃない。
ということです。 なんのこっちゃわかりませんが、要するにメッチャ抽象的な関数をラムダ計算では扱います。
このラムダ計算を使うと、関数だけではなくプログラム上の論理式やif式、数値を表現することもできます。
ラムダ計算があって何が嬉しいかというと、
1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。(Wikipedia)
らしいです。
論理値
ラムダ式でtrue, false, if式はこのように定義できます。
true λtf. t false λtf. f if p then t else f (p には true か false が入る) λptf. p t f
式を見るだけどつまらないので、Haskellのコードで書いてみます。
true = \t f -> t false = \t f -> f if' p t f = p t f if' true 1 0 -- 1 if' false 1 0 -- 0
この計算の導出は、α変換、β簡約、η変換という三つのルールに従って行われています。
まず、if' true 1 0をラムダ式に直してみます。
(λptf. p t f) (λtf. t) O Z
便宜上、1をO、0をZとしています。
まず、引数をラムダ式内の変数に当てはめます。これがβ簡約です。
(λtf. (λtf. t) t f) O Z
すると、名前が同じで実体の違う変数 t と f が出てきました。ラムダ計算では上記の通り変数の名前は重要ではないのでそれぞれ名前を変えることができます。これがα変換です。
(λtf. (λxy. x) t f) O Z
次々にβ簡約をしていきます。
(λf. (λxy. x) O f) Z (λxy. x) O Z (λy. O) Z O
これで手動でラムダ計算ができました！
使わなかったη変換はこのような時に使います。
λx. f x
あるラムダ式fにxを適用するラムダ式ですが、よく考えるとこのラムダ式は f そのものと同値であることがわかります。
Z は任意のラムダ式 (λx. f x) Z f Z
この時λx. f xをfに変換することをη変換といいます。
数値
if式の例ではZ, Oと表記されていた数値ですが、これもラムダ式で表現することができます。 と言っても数字を直接扱うのではなく、関数を何回適用するかで表現します。
zero(Z) λsz. z one(O) λsz. s z two λsz. s (s z)
three以降は書くのが面倒ですね。数値n+1はsをnに一回適用することで得られることから、関数を一回適用するラムダ式を用意すればインクリメントの表現ができそうです。
succ λnsz. s (n s z) three λsz. succ two s z
数値は二つの引数を持つラムダ式なので、その分を埋める必要があります。
インクリメントもあればデクリメントもある。ということで、デクリメントはこちらです。
pred λnsz. n (λfg. g (f s)) (λx. z) (λx. x)
大変ですね。一つひとつ見てみましょう。 まずpredを三つの部分に分けて見てみます。
pred λnsz. n <flip> <const> <id> flip λfg. g (f s) const λx. z id λx. x
constは「何が適用されようがzを返す関数」、idは「何が適用されようがそのまま返す関数」と読めます。
キモはflipです。
flipは一体何をしているのでしょうか？
ラムダ式では数値は関数が何回適用されたかで表現するのでした。
nとn+1 s( s( s( s( s( ... s( z ) ... ) ) ) ) ) s( s( s( s( s( s( ... s( z ) ... ) ) ) ) ) )
ここで、twoにflipを渡してみます。flip中のsを一旦Sとおきます。
two λsz. s( s( z ) ) ) two flip ( λsz. s( s( z ) ) ) ( λfg. g ( f S ) ) ( λz. ( λfg. g ( f S ) ) ( ( λfg. g ( f S ) ) z ) ) --> (λz. <flip> (<flip> z)) λz. ( λfg. g ( f S ) ) ( λg. g ( z S ) ) λz. λg. g ( ( λg. g ( z S ) ) S ) λz. ( λh. h ( ( λg. g ( z S ) ) S ) ) λz. ( λh. h ( S ( z S ) ) ) λzh. h ( S ( z S ) )
これを見ると、s( s( z ) )だったものがs ( z ( s ) )になっていることがわかります。また、ここでzにあたるのはconstなのでさらにconstを適用してみましょう。const中のzを一旦Zとしておきます。
( λzh. h ( S ( z S ) ) ) ( λx. Z ) λh. h ( S ( λx. Z ) S ) λh. h ( S Z )
s ( s ( z ) )がs ( z )になりました！！
このままidも適用してみましょう。
( λh. h ( S Z ) ) (λx. x) ( λx. x ) ( S Z )
変換できるのはここまでですが、結果はこの時点でoneになることがわかります。
つまりflipはzとsを逆転させることでconstを適用した時にs ( z )をzに評価するようにしていた、ということになります。
再帰
ようやくYコンビネータです。
Y λf. f (λx. f ( x x ) ) (λx. f ( x x ) )
もう何を言ってるのかよくわかりません。とりあえず、Yコンビネータはこのような性質を持っています。
Y ( f ) = f ( Y ( f ) )
Yコンビネータを使って階乗を表してみると、このようになります。
<isZero> ... 引数がzeroならtrue,そうでなければfalseを返すラムダ式 <mul> ... λxy. x * yのような計算をするラムダ式 λn. <Y> (λfx. <if> (<isZero> x) <one> (<mul> ( f ( <pred> x ) ) x ) ) n
こうなると変換は大変なのでやりませんが、このように全て関数を使って再帰関数を表現することができました。
ちなみにHaskellで書いてみるとこのようになります。
-- そのまま書ける y f = f (y f) fac x = y (\f x -> if x == 0 then 1 else f (x - 1) * x) x
しかし、Yコンビネータを正格評価のプログラミング言語で実装すると無限再帰になってしまうので、それを解消するためのZコンビネータというものもあります。Zコンビネータは完全にYコンビネータの正格評価版です。
Z λf. ( λx. f ( λy. x x y ) ) ( λx. f ( λy. x x y ) )
// Scala def Z[A, B] = (f: (A => B) => A => B) => (x: A) => f(Z(f))(x)
おわりに
今回はラムダ計算そのものについて考えましたが、記事の初めに書いたように応用できると強いと思います。あと何より面白いので、本など漁ってみてはいかがでしょうか。僕はこの記事を投稿した後、漁ります。
6日目はmizuki_sonokoさんです！
