zick pages

R7RSのformal semanticsをOCamlで書いた

はじめに

ちょっと前にR5RSのformal semanticsをOCamlで書いた。 R7RSのformal semanticsはdynamic-windを除けばR5RSと対して変わらないという噂を 10年くらい前に聞いたような気がするので、 以前のOCamlのプログラムをR7RS用に書き直してみた。

ちなみに、書きたい部分しか書いてないので全体の仕様のうち ごくわずかな部分しか実装していない。このタイトルはほとんど詐欺だ。

R5RSとR7RSの違い

R5RSとR7RSをしっかり見比べればいいのだが、面倒なので、 R5RSに関してはおぼろげな記憶を頼りにR7RSだけ読みながら脳内でdiffをとった。

領域方程式

dynamic-windのために dynamic point (記号の上ではω ∈ P) というものが追加されている。 それから手続きがそのPを受け取るように変更されている。

F = L * (E* -> P -> K -> C)
P = (F * F * P) + {root}

Pの要素は「2つの手続きと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