続・R5RSの形式的意味論
R5RSの形式的意味論ですが、ほとんど分かりました。
とりあえず概略を書いておきます。
プログラムは次の形で評価される。
E[[E]]ρκσ
Eは式、環境、次に評価する式、ストアを受け取り式の意味を返す意味関数
Eは式の集合の要素(つまり式)、
ρは環境(識別子(変数)を受け取りロケーション(アドレス)を返す関数)
σはストア(ロケーションを受け取り評価済みの値を返す関数)
κは次に評価する式(継続)
(κの初期値はλε*ρ.ε*)
式が複数の部分式に分けられるときは一箇所のみを評価し、
残りの箇所を評価するために継続渡し形式(CPS)が用いられる(κに適当なものを入れる)。
注意すべき点は同じ文字をフォントだけ変えて全く別のものとして扱っているということです。
はっきりいって慣れるまでかなり紛らわしいです。
あと、ほとんどの式はρとκを受け取ることによって評価され、直接σを受け取りません。
(例えば、 E[[K]] = λρκ.send(K[[K]])κ のような形をしています。)
変数の参照、書き換えなど一部の操作はσを受け取ってから評価が始まり、
以降の式には(変数を書き換えた場合は)新しいσを渡します。
それから、どうでもいいこととしては、継続渡し形式を使ってるため、call/cc自体はすごく簡単だとか。
とまあ、自分では分かったつもりなんですが、
言葉にして説明するって難しいですね。