2013.11.09 Saturday
λ式のβ変換
この前また妻とふたりで人生ゲームをやった。株を一度に三枚変えるようにしたり、所持金の3桁変動マスは4桁変動にするなどのルールでやってみた。若干ゲームバランスが破綻してしまう感はあるが、スリルがあって面白い。
人生ゲームの攻略法について考察するのも面白そう。すでにやってる人いそうだが。
「計算論」の続き。ここからがλ計算本番という感じ。
λ計算のβ変換とはλ記法であらわされた関数の関数値を求める操作に相当するもの。
定義2.1.2に形式的な定義は書いてあるが、具体的な式で考えた方がわかりやすい。β変換を→で表すことにする。
まずはすごく簡単な例から。
(λx.x)y→y
これが定義2.1.2(1)だ。
問題は(2)の方だ。
M→Nならばλx.M→λx.N。どういうことだ。
(λx.x)y→y
だから例えば
λz.((λx.x)y)→λz.y
ということになる。あたり前な感じか。
次にM→NならばMP→NP。
(λx.x)y→y
だから
(λx.x)yz→yz
ふむふむ。M→NならばPM→PNも同様だ。自然な定義だな。
λ式に対してβ変換を繰り返して具体的な値を得たいのだが、β変換の組み合わせは無数にある。左から変換していってもいいし、右からしていってもいい。最終的な結果は一致するだろうか。
これが2.2節のテーマで、実はChurch-Rosserの定理によってこれは保証されている。有限のβ変換列でそれ以上変換できなくなった場合、そのλ式を正規形という。
すべてのλ式が正規形を持つことは保証されない。また、正規形を持つλ式でも変換の仕方によっては変換が無限に続く場合もある。ただし、この場合もうまく変換すれば正規形にもっていくことができる。
では確実に正規形を得る変換の方法はあるだろうか、という問いには正規化定理が答えてくれる。左から順に変換していけば、正規形を持つ場合は必ず正規形に到達する。
ここまででλ式の基本的な性質は大分わかってきた。
2.3節はとりあえずスルー。
2.4節はλ式なんか考えて何が楽しいのかについて書いてある。
結論を言えば帰納的関数(すなわち計算可能な関数)はλ式によって表現できることが証明される。
計算可能関数の結果を得るためにwhileプログラム(C言語等)を書いて実行してもいいのだが、λ式を書いて実行してもいいわけだ。この場合の計算過程はβ変換そのものだ。コードはλ式、β変換が実行過程。
手続型言語はwhileプログラム、LISPはλ計算を基礎にしていると言えよう。そりゃあ全然違うものになるわな。
人生ゲームの攻略法について考察するのも面白そう。すでにやってる人いそうだが。
「計算論」の続き。ここからがλ計算本番という感じ。
λ計算のβ変換とはλ記法であらわされた関数の関数値を求める操作に相当するもの。
定義2.1.2に形式的な定義は書いてあるが、具体的な式で考えた方がわかりやすい。β変換を→で表すことにする。
まずはすごく簡単な例から。
(λx.x)y→y
これが定義2.1.2(1)だ。
問題は(2)の方だ。
M→Nならばλx.M→λx.N。どういうことだ。
(λx.x)y→y
だから例えば
λz.((λx.x)y)→λz.y
ということになる。あたり前な感じか。
次にM→NならばMP→NP。
(λx.x)y→y
だから
(λx.x)yz→yz
ふむふむ。M→NならばPM→PNも同様だ。自然な定義だな。
λ式に対してβ変換を繰り返して具体的な値を得たいのだが、β変換の組み合わせは無数にある。左から変換していってもいいし、右からしていってもいい。最終的な結果は一致するだろうか。
これが2.2節のテーマで、実はChurch-Rosserの定理によってこれは保証されている。有限のβ変換列でそれ以上変換できなくなった場合、そのλ式を正規形という。
すべてのλ式が正規形を持つことは保証されない。また、正規形を持つλ式でも変換の仕方によっては変換が無限に続く場合もある。ただし、この場合もうまく変換すれば正規形にもっていくことができる。
では確実に正規形を得る変換の方法はあるだろうか、という問いには正規化定理が答えてくれる。左から順に変換していけば、正規形を持つ場合は必ず正規形に到達する。
ここまででλ式の基本的な性質は大分わかってきた。
2.3節はとりあえずスルー。
2.4節はλ式なんか考えて何が楽しいのかについて書いてある。
結論を言えば帰納的関数(すなわち計算可能な関数)はλ式によって表現できることが証明される。
計算可能関数の結果を得るためにwhileプログラム(C言語等)を書いて実行してもいいのだが、λ式を書いて実行してもいいわけだ。この場合の計算過程はβ変換そのものだ。コードはλ式、β変換が実行過程。
手続型言語はwhileプログラム、LISPはλ計算を基礎にしていると言えよう。そりゃあ全然違うものになるわな。