<< ラムダ計算 | top | 「ライブ・ア・ライブ」クリアした >>

スポンサーサイト

一定期間更新がないため広告を表示しています

スポンサードリンク | - | | - | - |

λ式のβ変換

この前また妻とふたりで人生ゲームをやった。株を一度に三枚変えるようにしたり、所持金の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はλ計算を基礎にしていると言えよう。そりゃあ全然違うものになるわな。
 
ジャジャガッチ | LISP | 22:29 | comments(0) | trackbacks(0) |

スポンサーサイト

スポンサードリンク | - | 22:29 | - | - |
Comment









Trackback
URL:

07
--
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
--
>>
<<
--
PR
RECOMMEND
RECENT COMMENT
MOBILE
qrcode
OTHERS
Since 2013/09/17
LATEST ENTRY
CATEGORY
ARCHIVE
LINKS
PROFILE
SEARCH