ちょっと前にR5RSのformal semanticsをOCamlで書いた。 R7RSのformal semanticsはdynamic-windを除けばR5RSと対して変わらないという噂を 10年くらい前に聞いたような気がするので、 以前のOCamlのプログラムをR7RS用に書き直してみた。
ちなみに、書きたい部分しか書いてないので全体の仕様のうち ごくわずかな部分しか実装していない。このタイトルはほとんど詐欺だ。
R5RSとR7RSをしっかり見比べればいいのだが、面倒なので、 R5RSに関してはおぼろげな記憶を頼りにR7RSだけ読みながら脳内でdiffをとった。
dynamic-windのために dynamic point (記号の上ではω ∈ P) というものが追加されている。 それから手続きがそのPを受け取るように変更されている。
F = L * (E* -> P -> K -> C)
P = (F * F * P) + {root}
Pの要素は「２つの手続きとPの3つ組」もしくは「定数root」のいずれかとなる。 このrootは「dynamic-windが一度も呼ばれていない状態」を表し、 3つ組は「dynamic-windの中に入るときに呼ばれる手続き、 出るときに呼ばれる手続き、一つ前の状態」を表す。 一つ前の状態というのが若干わかりにくいが、 dynamic-windが入れ子で呼ばれたときのためのものだ。 これによりdynamic pointはリスト構造をなすため、 大域脱出するときは順番に「出るときに呼ばれる手続き」を呼び出したり、 再突入するときにも順番に「入るときに呼ばれる手続き」 を呼び出したりすることができる。
Fの要素は継続が正しくdynamic pointを記憶できるように、 これを受け取るようになっている。
これをOCamlに直訳するのは相変わらず簡単だ。
type tyF = tyL * (tyEl -> tyP -> tyK -> tyC)
...
and tyP =
PRoot
| PE of (tyF * tyF * tyP)
R5RSの意味関数ℰはExp -> U -> K -> Cという型で、
式、環境、継続、内部記憶を受け取ったが、R7RSでは
Exp -> U -> P -> K -> Cとなっており、
dynamic pointも受け取るようになっている。
ただ、ℰ自身はこれといって面白いことはしない。
ただdynamic pointを市中引き回しの刑に処すだけだ。
引き回されたdynamic pointはdynamic-windとcall/ccの中でだけ使われる。
さて、問題のdynamic-windなのだが、意外と単純だ。
3つの手続きe1, e2, e3を受け取って、順番に呼ぶのだが、
2つ目の手続きを呼ぶときはdynamic point ω をそのまま使うのではなく、
(e1, e2, ω)の3つ組を使う。
イメージとしてはスタックに必要な情報を乗せる感じだ。
複雑なのはcall/ccの方だ。これだけで補助関数の25%くらいの紙面を使っている。 基本方針としては「現在のdynamic point」を使って 「出るときに呼び出す手続き」を順番に呼び出し、 「継続が記憶しているdynamic point」を使って 「入るときに呼び出す手続き」を順番に呼び出す。 ただし、すべての手続きを呼び出せばいいというものではない。
(dynamic-wind ;; [1]
...
(dynamic-wind ;; [2]
...
(dynamic-wind ;; [3]
...)))
このような入れ子があったとき、[3]から[2]の外側に大域脱出したときは、 [3]と[2]の「出るときに呼び出す手続き」を呼ぶ必要があるが、 [1]の手続きを呼んではいけない。 再突入に関しても同様の話がある。 さらには継続を使ってスタックが「枝分かれ」するようなケースもあり、 この場合は色々と楽しくなってくる。
要するに、スタックを巻き戻したり再構築する範囲でだけ、 必要な手続きを呼ぶ必要があり、範囲外の手続きを呼んではいけない。 R7RSのformal semanticsではこれを実現するために 集合を使ったちょっとビックリする式が書いてあるので、 興味がある方はぜひとも読んでほしい。 ビックリするもののOCamlに直訳するのは意外と簡単にできる。
せっかくコードを書いたのだから実行したいのだが、 dynamic-windの複雑な例を試すためには set!やdisplayなど副作用を用意しないといけない。 これが面倒だったのでせっかく作ったdynamic-windを試していない。 OCamlの型チェックが通っただけで満足してしまった。
型といえば、R7RSではcar-internalという補助関数の定義が間違っている。型からは 「carはdynamic pointを受け取るがcar-internalはdynamic pointを受け取らない」 という意図を感じるのだが、実際の式はdynamic pointを受け取っている。 呼び出す側はdynamic pointを付けていないので明らかにおかしい。
car-internal: E -> K -> C
car-internal = λεωκ.hold(ε|Ep↓1)κ
call-with-valuesの定義が間違っていたところでそこまで気にならないが、 carの定義が間違っているとさすがにどうかと思ってしまう。
2022-08-13