(泥縄とかそういう突っ込みはいらない)
ラムダ計算入門のPDFが分かりやすかったのでこれを元に入門編を勉強。
とりあえずラムダ計算の定義。
e(λ式) ::= x (変数)
| λx.e (λ抽象)
| e1e2 (関数適用)
この辺は余裕。Schemeで変数を定義するときにlet式を使うが、let式もlambdaに変換できる。
(SICPで出たが復習)
(let ((x 1)) <body>) -> ((lambda (x) <body>) 1)
λ式に対して関数適用をするといった感じ？
β簡約
いくつかやり方があるらしい。とりあえず資料にあったのは、R-Beta、R-App1、R-App2とR-Absの4つ。
R-Beta: -------------------------- (λx.e1)e2 -> [e2/x]e1 例: (λx.x)y -> y (λx.λy.x)z -> λy.z[e2/x]e1はe1の変数xにe2を代入したという意味。
R-App1:
e1 -> e1'
-----------------
e1e2 -> e1'e2
例:
(λa.b)cd -> bd
λ式は左結合なので、(λa.b)cdは実際は((λa.b)c)dとなる。R-Betaで(λa.b)cが[c/a]bになって、このbに対してdを適用するということ。じゃあ、正確には[c/a]bdじゃないのだろうかと、ちと疑問。
R-App2:
e2 -> e2'
-----------------
e1e2 -> e1e2'
例:
a((λx.x)b) -> ab
R-App2はR-App1のe2版。つまり引数に対してβ簡約をするということ。例は資料になかったので自分で考えた。間違い指摘大歓迎！！
R-Abs:
e -> e'
-------------------
λx.e -> λx.e'
例:
λx.(λy.y)x -> λx.x
λ抽象に対しての簡約。実行時に関数を評価するMLでは必要ないらしい。でも、簡約=最適化だとすればコンパイル時に評価しなくてもいいので、簡約はしておきたいなぁ。ということでこれも必要としておこう。α変換
変数名を一意に変換すること。こんな感じ(まんま資料から)。
(λx.λy.xy)y -α変換-> (λx.λy'.xy')y -β簡約-> λy'.yy'
最初の式のyと適用されるyは異なる変数だが同名がつけられている。このまま簡約すると式の意味が変わるので変数名を変えようというだけの話。
仰々しい名前が着いてるけど、変数名の衝突を防ぐだけ・・・
とりあえず、入門の入門としてはこれくらいにする。
1時間の勉強内容としてはこんなもんだろう・・・
最終的にはSabry&WadlerのCPS変換の実装をSchemeでできるまでには習得したい・・・