R7RSの形式的意味論を読む

はじめに

Scheme の魅力のひとつとして「形式的意味論が定義されている」というのがあります。言語仕様書も無料で公開されていて誰でも読むことができます。言語処理系好きなら是非一度読んでみたいところです。しかし、この形式的意味論、とても読みにくい代物になっています。色々なものが記号の羅列で表されていて、各記号の説明も不十分で、更に解説がほとんどないのです。そこで、できるだけ日本語の解説を加え、R7RSの形式的意味論を読みやすくしてみようと思いました。(…が、書きあがってみるとなんかチラ裏な気もしつつ誰かの役に立つといいなぁという気持ちで公開します)

というわけで、R7RS の 7.2. Formal semantics を読んでいきます。

前準備

使われている記号について

まずは記号の話です。形式的意味論は記号だらけです。そういうものなので仕方ありません。

記号の一覧は p65 の右上にあります。が、概要しかかかれていません。慣れていないと読みにくいのですが、実際のところ特に難しいことはないので、具体例を挙げていけばすぐに理解できるでしょう。

sequence formation

$$\langle\cdots\rangle$$

いわゆる「列」です。具体例としては

$$
\langle\rangle\
\langle\alpha,\beta,\gamma\rangle\
\langle1,2,3,4\rangle
$$

などです。

列は要素の順序が区別されます。
つまり$\langle\alpha,\beta\rangle$ と $\langle\beta,\alpha\rangle$は異なります。
また、Schemeのlistとは異なり、pairの連鎖ではありません。列はあくまで順序を区別する要素の並びです。

kth member of the sequence(1-based)

$$s\downarrow k$$

$\downarrow$は列の要素を取りだす中置演算子です。$s\downarrow k$は$s$の$k$番目の要素を表します。例えば

$$
\langle\alpha,\beta,\gamma\rangle\downarrow1=\alpha\\
\langle\alpha,\beta,\gamma\rangle\downarrow2=\beta\\
\langle\alpha,\beta,\gamma\rangle\downarrow3=\gamma
$$

です。1はじまりなので気を付けましょう。

length of sequence s

$$＃s$$

＃は列$s$の長さを取り出す前置演算子です。

例えば、

$$
\begin{array}{rcl}
＃\langle\rangle&=&0\\
＃\langle\alpha\rangle&=&1\\
＃\langle\alpha,\beta\rangle&=&2\\
＃\langle\alpha,\beta,\gamma\rangle&=&3\\
\end{array}
$$

です。

concatenation of sequences s and t

$$s § t$$

$§$は中置演算子で、「$s § t$」は「列 $s$ と $t$ を連結したもの」を表します。

例えば、

$$
\begin{array}{rcl}
\langle\rangle§\langle\alpha\rangle&=&\langle\alpha\rangle\\
\langle\alpha\rangle§\langle\beta\rangle&=&\langle\alpha,\beta\rangle\\
\langle\alpha,\beta\rangle§\langle\gamma,\delta\rangle&=&\langle\alpha,\beta,\gamma,\delta\rangle\\
\end{array}
$$

です。

drop the first k members of sequence s

$$s\dagger k$$

$\dagger$ は中置演算子で、「$s\dagger k$」は「列$s$の最初の$k$個の要素を落としたもの」を表します。

例えば、

$$
\begin{array}{rcl}
\langle\alpha\rangle\dagger1&=&\langle\rangle\\
\langle\alpha,\beta\rangle\dagger1&=&\langle\beta\rangle\\
\langle\alpha,\beta,\gamma\rangle\dagger2&=&\langle\gamma\rangle\\
\langle\alpha,\beta,\gamma,\delta\rangle\dagger2&=&\langle\gamma,\delta\rangle\\
s\dagger0&=&s
\end{array}
$$

です。

McCarthy conditional "if t then a else b"

$$t \rightarrow a, b$$

$\rightarrow$ と $,$ は三項演算子で、「$t \rightarrow a, b$」は「$t$ が $true$ なら $a$、$t$ が $false$ なら $b$」を表します。

例えば

$$
\begin{array}{rcl}
true \rightarrow \alpha, \beta &=& \alpha\\
false \rightarrow \alpha, \beta &=& \beta
\end{array}
$$

です。

substitution "ρ with x for i"

$$\rho[x/i]$$

「$\rho[x/i]$」は「$i=j$のとき$\rho[x/i]j=x$、 $i\neq j$のとき$\rho[x/i]j=\rho j$」となる関数を表します。つまり $\rho[x/i] j = (i = j \rightarrow x, \rho j)$です。具体例については後述します。

injection of x into domain D

$$x\ \textrm{in}\ {\rm D}$$

いわゆるアップキャストです。$x$を${\rm D}$型として扱うことを明示します。

projection of x to domain D

$$ x\ |\ D$$

いわゆるダウンキャストです。$x$を${\rm D}$型として扱うことを明示します。ダウンキャストなので失敗することもありそうですが、形式的意味論中ではダウンキャスト失敗しないようになっている…のでしょうか？よくわかりません。(先行評価や必要呼びならダウンキャストは失敗しない。失敗するダウンキャストは簡約不能とすればどんな評価戦略でもよい。)

store と location と identifier について

R7RS には store, location, identifier という3種の変数っぽいものがでてきます。これを先に理解しておいた方が表示的意味論が読みやすいと思いますので、先に紹介しておきます。

これらはだいたい次のようになってます。

R7RS用語	集合の記号	元の記号	具体例
store	$\rm{S}$	$\sigma$	メモリ
location	$\rm{L}$	$\rho$	メモリアドレス
identifier	$\rm{Ide}$	$\rm{I}$	変数名

それぞれ見ていきましょう。

store

store は現実の計算機のメモリのことだと思ってよいと思います。

store の型は、${\rm S}={\rm L}\rightarrow({\rm E}\times{\rm T})$で、値は$\sigma$で表されます。${\rm L}$は location ですので、 store は location を引数に取り、expressed value と boolean の組を返す関数です。

具体例を書いてみましょう。storeは第一列がメモリアドレス(location)で、第二列がexpressed value と boolean の組になった表のようになっていると考えると良いと思います。

例えば

$$
\sigma=
\begin{array}{|cc|}
100 & \langle100, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}
$$

のような感じです。$100$番地に$\langle100,\mathit{true}\rangle$が入っていて、$104$番地に$\langle200,\mathit{true}\rangle$が入っていて…というような感じです。

この $\sigma$ は ${\rm L}$(location, メモリアドレス)を引数にとって値を返す関数でもあります。ですので

$$
\sigma\ 100=
\begin{array}{|cc|}
100 & \langle100, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}\ 100 = \langle 100, true\rangle
$$

や

$$
\sigma\ 104=
\begin{array}{|cc|}
100 & \langle100, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}\ 104 = \langle 200, true\rangle
$$

などとなります(なお、この表自体を関数のように扱う記法は私が考えたもので、一般的ではないと思います)。

さて、$\sigma$は純粋な関数ですので、表自体を書き換えることはできません。その代わり、$\rho[x/i]$の記法で「一部だけ異なるが残りは全て同じ表」を表現します。例えば「$\rho$の$100$番地を$\langle400,true\rangle$に置き換えたメモリ」は以下の様な感じで表現できます。

$$
\sigma[\langle 400,true\rangle/100] =
\begin{array}{|cc|}
100 & \langle100, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}[\langle 400,true\rangle/100] =
\begin{array}{|cc|}
100 & \langle400, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}
$$

identifier と environment

表示的意味論中では、identifier と location(メモリアドレス) の対応表を使って、 identifier から location を得ます。この identifier と location の対応表を environment とよんでいて、$\rho$で表します。

たとえば

$$
\rho=
\begin{array}{|cc|}
\mathit{apple}&100\\
\mathit{banana}&104\\
\mathit{cherry}&108
\end{array}
$$

のようになっています。

$\mathit{apple}$は$100$番地、$\mathit{banana}$は$108$番地、$\mathit{cherry}$は$108$番地を表す identifier である、という感じです。

$\rho$ の型は ${\rm U}={\rm Ide}\rightarrow{\rm L}$です。ですので

$$
\rho\ \mathit{apple} =
\begin{array}{|cc|}
\mathit{apple}&100\\
\mathit{banana}&104\\
\mathit{cherry}&108
\end{array}\mathit{apple} = 100
$$

や

$$
\rho\ \mathit{banana} =
\begin{array}{|cc|}
\mathit{apple}&100\\
\mathit{banana}&104\\
\mathit{cherry}&108
\end{array}\mathit{banana} = 100
$$

等のようになります。

identifier の値

Scheme では識別子を評価すると識別子に束縛された値になります。
このとき裏で次のようなことが行われます。

1. environment を使って identifier を location に変換する
2. store を使って location を expressed value と boolean の対に変換する
3. expressed value と boolean の対の第一要素を取る

identifier ${\mathit banana}$ に束縛された値は environment $\rho$ と store $\sigma$ を使って次のように表せます。

$$
\begin{array}{cl}
& \sigma(\rho\ {\mathit banana}) \downarrow 1 \\
= & \sigma(\begin{array}{|cc|}
\mathit{apple}&100\\
\mathit{banana}&104\\
\mathit{cherry}&108
\end{array}\ \mathit{banana})\downarrow 1 \\
= & \sigma\ 104 \downarrow 1 \\
= & \begin{array}{|cc|}
100 & \langle100, \mathit{true} \rangle \\
104 & \langle200, \mathit{true} \rangle \\
108 & \langle300, \mathit{true} \rangle
\end{array}\ 104 \downarrow 1 \\
= & \langle200, true\rangle\downarrow 1 \\
= &200
\end{array}
$$

要するに、identifier の値を得るには、表を二回引くわけです。

dynamic-wind と dynamic point

R7RSの表示的意味論では dynamic-wind に必要な dynamic point という概念が出てきます。dynamic-wind を理解していればどうということはないのですが、あまり使うことのない手続きなので、先に紹介しておくことにします。(ただ、dynamic-wind の表示的意味論を理解できなくて良いのであれば、この節は無視してもかまいません。むしろ慣れてから読み返しても良いと思います。)

dynamic-wind は次のような手続きです。

(dynamic-wind before thunk after)

before, thunk, after いずれも引数0個の手続きで、
dynamic-wind は before, thunk, after の順に呼び出す手続きなのですが、
2点注目すべき点があります。

• thunk の中に飛び込むような継続を呼び出すと、飛び込む前に before を呼び出します。
• thunk の中から外に飛び出すような継続を呼び出すと、飛び出す前に after を呼び出します。

試してみましょう。

;;; 「msgを表示して改行する0引数手続き」を作成する手続き
(define cont1 #f)
(dynamic-wind
  (lambda () (display "before0\n"))
  (lambda ()
    (display "enter thunk1\n")
    (call/cc (lambda (cc) (set! cont1 cc))) ;; *1
    (display "leave thunk1\n"))
  (lambda () (display "after0\n")))

出力は

before0
enter thunk1
leave thunk1
after0

となります。

ここで

(cont1)

を評価すると、出力は

before0
leave thunk1
after0

となります。*1まで帰ったのに、 before0 が表示されています。また、"enter thunk1" は表示されない点にも注意しましょう。before は thunk に入る前に呼ばれる手続きで、after は thunk から出るときに呼ばれる手続きなのです。

さて、面倒なのは次のようなケースです。読みにくいコードで申し訳ないのですが、次のように動作します。

1. thunk1 を実行
2. thunk2 から thunk1 の中(label A)へ飛ぶ
3. thunk1 から thunk2 の中(label B)へ飛ぶ
4. thunk2 から通常の脱出

(define cont1 #f)
(define cont2 #f)
(dynamic-wind
  (lambda () (display "before0\n"))
  (lambda ()
    (dynamic-wind
      (lambda () (display "before1\n"))
      (lambda () ;; thunk1
        (display "enter thunk1\n")
        (call/cc (lambda (cc) (set! cont1 cc)))
        ;; label A
        (if cont2 (cont2)) ;; goto B in case the 2nd time
        (display "leave thunk1\n"))
      (lambda () (display "after1\n")))
    (dynamic-wind
      (lambda () (display "before2\n"))
      (lambda () ;; thunk2
        (display "enter thunk2\n")
        (call/cc (lambda (cc)
                   (set! cont2 cc)
                   (cont1))) ;; goto A
        ;; label B
        (display "leave thunk2\n"))
      (lambda () (display "after2\n"))))
  (lambda () (display "after0\n")))

これを実行すると次のように表示されます。

before0
before1
enter thunk1
leave thunk1
after1
before2
enter thunk2
after2
before1
after1
before2
leave thunk2
after2
after0

注目すべき点は before0 と after0 が一回ずつしか表示されていない点です。dynamic-wind がネストしていた場合、何が何でも before と after を呼べばよいというものではありません。thunk1 と thunk2 とでは外側の dynamic-wind を共有しているため、 thunk1 と thunk2 の間でのジャンプでは、外側の before と after は呼ばれないのです。

これを記述するための概念が dynamic point です。

dynamic point の型は

$$
{\mathrm P} = ({\mathrm F}\times{\mathrm F}\times{\mathrm P})+{root}
$$

です。

ノードひとつに関数($\mathrm{F}$)が二つある木構造になっています。これを使って何をするか、大体想像がつくと思います。

実際のところどう定義されているかは、表示的意味論を読むことにしましょう。

continuation

表示的意味論には2種類の continuation が存在します。command continuation と expression continuation です。この二つは何なのかというと、いわゆる「continuation」を二つに分けて整理したものです。

command continuation は $\theta$ で表され、型は $\mathrm{C} = \mathrm{S} \rightarrow \mathrm{A}$ です。

expression continuation は $\kappa$ で表され、型は $\mathrm{K} = \mathrm{E}^* \rightarrow \mathrm{C}$ です。

expression continuation の型には command continuation が含まれていますので、結局のところ expression continuation は、$\mathrm{K} = \mathrm{E}^* \rightarrow \mathrm{S} \rightarrow \mathrm{A}$です。

要するに expression continuation は「式の列とメモリを受け取り answer を返す関数」で、command continuation は「メモリを受け取り answer を返す関数」です。

では answer とは何かというと……R7RSのどこにも書かれていません。
恐らくこれはプログラムの終了状態を表す処理系毎に勝手に定義される値だと思います。

expression の評価

Scheme の expression の評価は、関数 $\mathcal E$ として定義されています。ある意味 Scheme 表示的意味論の主役ともいえる関数です。

$\mathcal E$ の型は $\mathrm{Exp} \rightarrow \mathrm{U} \rightarrow \mathrm{P} \rightarrow \mathrm{K} \rightarrow \mathrm{C}$ です。自然言語で書くと、$mathcal E$ は expression と environment と dynamic point と expression continuation を受け取り、command continuation を返す関数です。

つまりこれがどういうことかというと、 Scheme で「expression の評価」とされていたものは、「裏でこっそり environment と dynamic point と expression continuation を引数として引きずりまわしていました」 ということです。

本編

前準備としてはこれぐらいで良いと思います。というわけで本編を読んでいきましょう。

7.2.1 Abstract Syntax

まずは注釈付きで全体を引用します。

$$
\begin{array}{lclcll}
{\rm K} & \in & {\rm Con} & & & \text{quote式を含む定数}\\
{\rm I} & \in & {\rm Ide} & & & \text{identifier(variable)}\\
{\rm E} & \in & {\rm Exp} & & & \text{expression}\\
{\rm \Gamma} & \in & {\rm Com} & = & {\rm Exp} & \text{command}
\end{array}
$$

$$
\begin{array}{lcll}
{\rm Exp} & \longrightarrow & {\rm K} & \textrm{定数(constant)}\\
& | & {\rm I} & \textrm{識別子(identifier)}\\
& | & {\tt (E_0\hspace{1ex}E^*)} & \text{手続き呼び出し}\\
& | & {\tt (lambda\hspace{1ex}({\rm I^*})\hspace{1ex}{\rm \Gamma^*\hspace{1ex}E_0})} &\textrm{rest引数の無い{\tt lambda}式}\\
& | & {\tt (lambda\hspace{1ex}({\rm I^*}.\ {\rm I})\hspace{1ex}{\rm \Gamma^*\hspace{1ex}E_0})} & \textrm{rest引数の有る{\tt lambda}式}\\
& | & {\tt (lambda\hspace{1ex}{\rm I\hspace{1.5ex}\Gamma^*\ E_0})}&\textrm{restだけの{\tt lambda}式}\\
& | & {\tt (if\hspace{1ex}{\rm E_0\hspace{1ex}E_1\hspace{1ex}E_2})} & \text{else節のある{\tt if}式} \\
& | & {\tt (if\hspace{1ex}{\rm E_0\hspace{1ex}E_1})} & \text{else節のない{\tt if}式} \\
& | & {\tt (set!\hspace{1ex}{\rm I\hspace{1ex}E})} & \text{{\tt set!}式}
\end{array}
$$

記号に圧倒されそうになりますが、結局のところ次のことを言っています。

「式」は次の６つのうちどれかである
- 定数(constant)
- 識別子(identifier)
- 手続き呼び出し
- lambda 式
- if 式
- set! 式

じっくり読めば大したことは言っていません。じっくり読みましょう。

まず最初の部分ですが、これは単に記号の使い方を定義しているだけです。

$$
\begin{array}{lclcll}
{\rm K} & \in & {\rm Con} & & & \text{quote式を含む定数}\\
{\rm I} & \in & {\rm Ide} & & & \text{identifier(variable)}\\
{\rm E} & \in & {\rm Exp} & & & \text{expression}\\
{\rm \Gamma} & \in & {\rm Com} & = & {\rm Exp} & \text{command}
\end{array}
$$

たいしたことは言ってません。定数を表すときは$K$を使いますよ、定数の集合を表すときは$\rm{Con}$を使いますよ、と言っているだけです。

ところで command なるものがでてきてますね。${\rm \Gamma} \in {\rm Com} = {\rm Exp}$ とありますので、${\rm Com}$(command)と${\rm Exp}$(expression)は同じものです。${\rm E} \in {\rm Exp}$ ですので ${\rm \Gamma}$ も ${\rm E}$ も ${\rm Exp}$ です。

では ${\rm \Gamma}$ と ${\rm E}$ の違いは何かというと、「${\rm \Gamma}$の評価値は継続に渡されず、${\rm E}$の評価値は継続に渡される」ということです。なぜ ${\rm \Gamma}$ と ${\rm E}$ を区別しているかというと、${\rm \Gamma}$ と ${\rm E}$ の評価の意味論が異なるからです。先を読むとわかるのですが、それぞれに異なった意味が定義されています。expression を形式的に扱おうとすると、これらは区別せざるを得ないんですね。

次にこの部分です。

$$
\begin{array}{lcll}
{\rm Exp} &\longrightarrow& {\rm K} & \textrm{定数(constant)}\\
& | & {\rm I} & \textrm{識別子(identifier)}\\
& | & {\tt (E_0\hspace{1ex}E^*)} & \text{手続き呼び出し}\\
& | & {\tt (lambda\hspace{1ex}({\rm I^*})\hspace{1ex}{\rm \Gamma^*\hspace{1ex}E_0})} &\text{rest引数の無いlambda式}\\
& | & {\tt (lambda\hspace{1ex}({\rm I^*}.\ {\rm I})\hspace{1ex}{\rm \Gamma^*\hspace{1ex}E_0})} & \text{rest引数の有るlambda}\\
& | & {\tt (lambda\hspace{1ex}{\rm I\hspace{1.5ex}\Gamma^*\ E_0})}&\text{restだけのlambda式}\\
& | & {\tt (if\hspace{1ex}{\rm E_0\hspace{1ex}E_1\hspace{1ex}E_2})} & \text{else節のあるif式}\\
& | & {\tt (if\hspace{1ex}{\rm E_0\hspace{1ex}E_1})} & \text{else節のないif式}\\
& | & {\tt (set!\hspace{1ex}{\rm I\hspace{1ex}E})} & \text{set!式}
\end{array}
$$

これも記号に圧倒されそうですが、ひとつひとつ見ていけば大したことは言っていません。

まず一行目は「$\rm{K}$(定数)は式である」です。特に難しいことはありません。

二行目は「$\rm{I}$(identifier)は式である」です。特に難しいことはありません。

三行目は「$(\rm{E}_0\ \rm{E}^*)$ は式である」です。$^*$は0個以上の繰り返しを意味しますので、$(\rm{E}_0)$ や $(\rm{E}_0\ \rm{E}_1)$ や $(\rm{E}_0\ \rm{E}_1\ \rm{E}_2)$ 等は式です。これらは Scheme の手続き呼び出しですね。というわけで、三行目では「手続き呼び出しは式です」と言っています。

四・五・六行目は「lambda式は式である」と言っています。量に圧倒されそうですが、lambda式を3種類に分けて記述しているだけです。また、$\Gamma$に騙されそうですが、$\Gamma$ は $\rm{E}$ と同じなのでした。ここを押さえておけば$(\rm{lambda}\ ()\ \rm{E_0})$ や $(\rm{lambda}\ (\rm{I})\ \rm{E_0}\ \rm{E_1})$ や $(\rm{lambda}\ (\rm{I_0}\ .\ \rm{I_1})\ \rm{E_0}\ {E_1})$ や$(\rm{lambda}\ \rm{I_0}\ \rm{E_0})$ 等の見慣れたlambda式のことを言っているのがわかると思います。

七・八行目はif式ですね。もう大丈夫だと思います。

九行目はset!式です。

というわけで、結局のところ、 Abstract Syntax では「定数(constant)・識別子(identifier)・手続き呼び出し・lambda式・if式・set!式」だけを対象にしますよ、と言っているのです。

7.2.2 Domain equations

7.2.2 はどの記号を何に使うか決めているだけです。必要な時に都度参照してください。ざっと眺めて先に進みましょう。印刷して壁に貼っておくなりサブディスプレイに表示しておくなりでも良いと思います。

7.2.3 Semantic functions の概要

7.2.3がR7RSの形式的意味論の本丸です。ソースコードがどんな意味を持つのかここで定義しています。ここが読めればR7RSの形式的意味論を読めると言ってよいでしょう。

…が、細かく中身を追うには 7.2.4 の関数が必要です。本節では概要にとどめ、次に7.2.4を読み、その後7.2.3の詳細に戻ることにしましょう。

それでは概要です。

𝓚

$\mathcal{K}$は定数の semantic function です。

$\mathcal{K}$の定義は省略と書かれていますが、実際の定義は以下のようになると思います。

$$
\begin{array}{lcl}
\mathcal{K}[\hspace{-1pt}[{\tt ＃t}]\hspace{-1pt}]&=&true\\
\mathcal{K}[\hspace{-1pt}[{\tt ＃f}]\hspace{-1pt}]&=&false\\
\mathcal{K}[\hspace{-1pt}[\langle number\rangle]\hspace{-1pt}]&=&number_to_constant\ \langle number\rangle\\
\mathcal{K}[\hspace{-1pt}[{\tt '}\langle datum\rangle]\hspace{-1pt}]&=&quoted_datum_to_constant\ \langle datum\rangle\\
&\vdots&
\end{array}
$$

これがリテラルの種類分続きます。7.2に書かれているとおり、特に面白くない上に複雑になります。省略もやむなしでしょう。$number_to_constant$や$quoted_datum_to_constant$にあたるλ項も複雑かつ大量な割に言語仕様として書く意味は薄いと思います。

𝓔概要

表示的意味論の主人公です。

$\mathcal E$は「式を評価して継続に渡す関数」を定義しています。
$\rho$と$\omega$と継続$\kappa$があったとき、

$$
\mathcal E[\hspace{-1pt}[{({\tt if}\ {\tt ＃t}\ 0\ 1)}]\hspace{-1pt}]\rho\omega\kappa = \kappa\langle0\rangle\rho
$$

や、

$$
\mathcal E[\hspace{-1pt}[{({\tt car}\ {\tt '(1\ 2)})}]\hspace{-1pt}]\rho\omega\kappa = \kappa\langle1\rangle\rho
$$

等が言えるようになります。

詳細は後回しにします。下請け関数の意味がわからないと読めませんから、そちらを先に読みましょう。

𝓔*概要

これも詳細は後回しにしますが、$\mathcal E^*$ は引数評価用の補助関数です。

𝓒概要

これも詳細は後回しにしますが、$\mathcal C$ は command 評価用の補助関数です。

$({\tt lambda\ ()}\ \Gamma_0\ \Gamma_1\ \mathrm{E}_0)$ を呼び出したとき$\Gamma_0$ と $\Gamma_1$ の評価された値を捨てる、などためにあります。

7.2.4 Auxiliary functions

Semantic functions をさらっとなめたので、Auxiliary functions(補助関数)を読みます。Scheme の意味論はこれらを使って定義されていますので、こちらを先に理解しないと本体を読めないと思います。

前から順に読んでいきましょう。

lookup

$lookup:{\rm U} \rightarrow {\rm Ide} \rightarrow {\rm L}$
$lookup = \lambda\rho{\rm I}.\rho{\rm I}$

$lookup$ は identifier からアドレスを引く関数と考えると良いと思います。

$lookup$ は引数をふたつとる関数です。第一引数$\rho$は identifier からアドレスへの変換表で、第二引数${\rm I}$は identifier です。$lookup$ は $\rho$ の中から ${\rm I}$ に束縛された値を返す探し(lookup)、見つかった値を返します。

定義より、 $lookup\ \rho{\rm I}$ と $\rho{\rm I}$ は同じです。$\rho{\rm I}$ と書かずに $lookup\ \rho{\rm I}$ と書くのは「ここでは変数からアドレスへの変換をしていますよ」ということを明示するためではないかと思います。

extends

$extends: \mathrm{U} \rightarrow \mathrm{Ide^*} \rightarrow \mathrm{L^*} \rightarrow \mathrm{U}$
$extends = \lambda\rho\mathrm{I^*}\alpha^*\ . ＃\mathrm{I}^* = 0 \rightarrow \rho, extends(\rho[\alpha^*\downarrow1)/(\mathrm{I}^*\downarrow1)] (\mathrm{I}^*†1)(\alpha^*†1)$

$extends$ は identifier からアドレスへの変換表に、新たな項目を追加する関数です。
identifier の shadow も実現できます。

これも記号に圧倒されそうになりますが、微妙な違いを無視してScheme風に書くとこんな感じです。

;;; rho: identifier から location への変換表(list形式)
;;; i* : identifier の list
;;; a* : location の list
;;; i* と a* の長さは同じでなければならない。
;;; upsert! は変換表(rho)に項目が存在しなければその項目を insert した新しい変換表を返し、
;;; 項目が存在すればその項目を update した新しい変換表を返す手続き。
(define (extends rho i* a*)
  (if (null? rho)
      '()
      (extends (upsert! rho (car i*) (car i*))
               (cdr i*)
               (cdr a*))))

よくある再帰 map の変種です。
じっくり記号を読めば、たいしたことはしていないのがわかると思います。

wrong

関数 $wrong$ は実装依存です。

文字列を引数に取りますが、実装依存なので、引数の意味も実装依存です。

形式的意味論の中では「これはエラーだよ」ということを表すために使われていて、引数の文字列は「これはこんなエラーだよ」ということを表す文字列です。

引数はエラーの集合(${\rm X}$)の元であると定義されていますが、使われ方を見る限り、${\rm X}$の正体は文字列です。

send

$send:{\rm E}\rightarrow {\rm K}\rightarrow {\rm C}$
$send=\lambda\epsilon\kappa\ .\ \kappa\langle \epsilon\rangle$

値と値継続を引数にとり、コマンド継続を返す関数です(…としか言いようがない…)。

single

${\mathit single}:({\rm E}\rightarrow{\rm C})\rightarrow{\rm K}$
${\mathit single}=\lambda\psi\epsilon^*\ .\ ＃\epsilon^*=1\rightarrow\psi(\epsilon^*\downarrow 1),wrong\ \textrm{``wrong number of return values''}$

$single$は「第二引数の列が長さ1以外であればエラー、長さ1であればその列の要素を第一引数に適用する関数」です。

この関数は具体例を見るのがわかりやすいと思います。

${\mathit single}\ \psi\langle\rangle = wrong\ \textrm{''wrong number of return values''}$
${\mathit single}\ \psi\langle \epsilon_1\rangle = \psi\epsilon_1$
${\mathit single}\ \psi\langle \epsilon_1\epsilon_2\rangle = wrong\ \textrm{''wrong number of return values''}$
${\mathit single}\ \psi\langle \epsilon_1\epsilon_2\epsilon_3\rangle = wrong\ \textrm{''wrong number of return values''}$

一応型についてを説明しますと、${\mathit single}$ は『「値(${\rm E}$)を引数にとってコマンド継続を返す関数」を引数にとって「値の列(${\rm E}^*$)を引数にとってコマンド継続を返す関数(=expression continuation(${\rm K}$)」を返す関数』です。${\rm K}={\rm E}^*\rightarrow{\rm C}$であることを思い出すと、型を$({\rm E}\rightarrow{\rm C})\rightarrow({\rm E}^*\rightarrow{\rm C})$と読み替えられて、理解しやすくなると思います。

new

$\mathit{new}:{\rm S}\rightarrow({\rm L}+{\mathit{error}})$

要するにメモリ割当関数です。

この関数の振る舞いは実装依存ですが、7.2の地の文で「もし $\mathit{new}\ \sigma\in{\rm L}$ ならば、$\sigma(\mathit{new}\ \sigma\ |\ {\rm L})\downarrow 2=\mathit{false}$ である」という縛りがつけられています。つまり、成功すると、 $\langle\epsilon, false\rangle$を返し、失敗すると$error$を返す関数です。($\epsilon$の値は実装依存)

hold

$hold:{\rm L}\rightarrow{\rm K}\rightarrow{\rm C}$
$hold=\lambda\alpha\kappa\sigma\ .\ send(\sigma\alpha\downarrow1)\kappa\sigma$

少し乱暴に言うと、メモリに格納された値をexpression continuationに渡し、command continuationを返す関数です。

location は $\langle\epsilon,\mathrm{T}\rangle$ という形をしています。$hold$ はこの $\epsilon$ を取り出して、この$\epsilon$の先にある値を取り出し、値継続$\kappa$に$send$し、command continuationを返す関数です。

assign

$assign:{\rm L}\rightarrow{\rm E}\rightarrow{\rm C}\rightarrow{\rm C}$
$assign=\lambda\alpha\epsilon\theta\sigma\ .\ \theta(update\ \alpha\epsilon\sigma)$

$update$(後述)して command continuation を返します。
continuation を明示したset!と考えて良いと思います。

update

$update:{\rm L}\rightarrow{\rm E}\rightarrow{\rm S}\rightarrow{\rm S}$
$update=\lambda\alpha\epsilon\sigma\ .\ \sigma[\langle\epsilon,true\rangle/\alpha]$

location・値・storeを受け取り、location の値が書き換わった新しいstoreを返します。わからない場合は、本記事「store と location と identifier について」を読んで下さい。ほぼあれのままです。

tievals

$tivals:(\mathrm{L}^*\rightarrow\mathrm{C})\rightarrow\mathrm{E}^*\rightarrow\mathrm{C}$
$tivals=\lambda\psi\epsilon^*\sigma\ .\ ＃\epsilon^*=0\rightarrow\psi\langle\rangle\sigma,new\ \sigma\in\mathrm{L}\rightarrow tievals(\lambda\alpha^*\ .\ \psi(\langle new\ \sigma|\mathrm{L}\rangle§\alpha^*))(\epsilon^*†1)(update(new\ \sigma|\mathrm{L})(\epsilon^*\downarrow1)\sigma),wrong\ \text{``out of memory''}\sigma$

lambda の引数リストを束縛する関数です。

$new\ \sigma$ でメモリを確保し、そこに$update$ で $\epsilon^*$の値を詰め込みます。あとはよくある再帰関数です。

tievalsrest

$tivalsrest:(\mathrm{L}^*\rightarrow\mathrm{C})\rightarrow\mathrm{E}^*\rightarrow\mathrm{N}\rightarrow\mathrm{C}$
$tivalsrest=\lambda\psi\epsilon^*\nu\ .\ list(dripfirst\ \epsilon^*\nu)(single(\lambda\epsilon\ .\ tievals\ \psi((takefirst\ \epsilon^*\nu)§\langle\epsilon\rangle)))$

lambda のrest引数の処理をする関数です。

列の$\nu$ 個目以降を list にして $\epsilon$ に格納し、あとは $tivals$ に投げています。

dropfirst

$\mathit{dropfisrt}=\lambda l n\ . n=0\rightarrow l,\mathit{dropfirst}(l\dagger1)(n-1)$

列$l$の先頭$n$個を除去した列を返します。よくある再帰関数です。(ただの$l†n$との違いはなんだろう？)

takefirst

$\mathit{takefirst}=\lambda l n\ .\ n=0\rightarrow\langle\rangle,\langle l\downarrow1\rangle§(\mathit{takefirst}(l\dagger 1)(n-1))$

列$l$の先頭$n$個の要素からなる列を返します。よくある再帰関数です。

trueish

$\mathit{truish}:{\rm E}\rightarrow{\rm T}$
$\mathit{truish}=\lambda\epsilon\ .\ \epsilon=\mathit{false}\rightarrow\mathit{false},\mathit{true}$

引数が$\mathit{false}$なら$\mathit{false}$を、そうでなければ$\mathit{true}$を返す関数です。

Schemeの条件判定は＃fのみが偽でその他の値はすべて真なので、$\mathit{truish}$のような関数があると便利です。

permute / unpermute

引数の評価順序は未規定ですよ、ということを表すための実装依存の関数です。

applicate

$\mathit{applicate}:{\rm E}\rightarrow{\rm E}^*\rightarrow{\rm P}\rightarrow{\rm K}\rightarrow{\rm C}$
$\mathit{applicate}=\lambda\epsilon\epsilon^*\omega\kappa\ .\ \epsilon\in{\rm F}\rightarrow(\epsilon|{\rm F}\downarrow2)\epsilon^*\omega\kappa,\mathit{wrong}\ \textrm{''bad procedure''}$

第一引数が手続きでなかったら$\mathit{wrong}\ \textrm{''bad procedure''}$へと評価され、手続きであったら手続きの適用をする関数です。

onearg

エラー処理を無視すれば $onearg = \lambda\zeta\epsilon^*\omega\kappa\ .\ \zeta(\epsilon^*\downarrow1)\omega\kappa$ です。$\epsilon^*$の長さが1でないときはエラーとなります。

twoarg

エラー処理を無視すれば $twoarg = \lambda\zeta\epsilon^*\omega\kappa .\ \zeta(\epsilon^*\downarrow1)(\epsilon^*\downarrow2)\omega\kappa$ です。$\epsilon^*$の長さが2でないときはエラーとなります。

threearg

エラー処理を無視すれば $threearg = \lambda\zeta\epsilon^*\omega\kappa .\ \zeta(\epsilon^*\downarrow1)(\epsilon^*\downarrow)(\epsilon^*\downarrow3)\omega\kappa$ です。$\epsilon^*$の長さが3でないときはエラーとなります。

list, cons, less, add, car, cdr, setcar, eqv, apply

Scheme にほぼ同じ手続きがあるので、説明は省略します。ヘルパ関数も省略します。CPS形式になっていることだけ気を付ければ、ほぼそのまま読めると思います。

cwcc

$cwcc:\mathrm{E}^*\rightarrow\mathrm{P}\rightarrow\mathrm{K}\rightarrow\mathrm{C}$
$cwcc=onearg(\lambda\epsilon\omega\kappa\ .\ \epsilon\in\mathrm{F}\rightarrow(\lambda\sigma\ .\ new\ \sigma\in\mathrm{L}\rightarrow applicate\ \epsilon\langle\langle new\ \sigma|\mathrm{L},\lambda\epsilon^*\omega'\kappa'\ .\ travel\ \omega'\omega(\kappa\epsilon^*)\rangle\mathrm{in}\ \mathrm{E}\rangle\omega\kappa(update(new\ \sigma|\mathrm{L}) unspecified\ \sigma),wrong\ \text{''out of memory''}\ \sigma), wrong\ \text{''bad procedure argument''})$

call-with-current-continuation です。

エラー処理の部分でごちゃっとしていますが、キモになっているのは$\langle new\ \sigma|\mathrm{L},\lambda\epsilon^*\omega'\kappa'\ .\ travel\ \omega'\omega(\kappa\epsilon^*)\rangle$の部分です。これが call-with-current-continuation に渡される手続きに渡される手続き、つまり、いわゆる継続です。この関数部分が呼び出されると、$travel$ で dynamic-wind の処理を行った後、 $\kappa'$(expression continuation) を捨てて、$\kappa$を新たな expression continuation として処理を続行します。

travel

$travel: \mathrm{P} \rightarrow \mathrm{P} \rightarrow \mathrm{C} \rightarrow \mathrm{C}$
$travel = \lambda \omega_1 \omega_2\ .\ travelpath((pathup\ \omega_1(commonancest\ \omega_1 \omega_2)) § (pathdown\ (commonancest\ \omega_1 \omega_2)\omega_2))$

継続を呼び出したときに $dynamic-wind$ で登録された手続きを呼び出すための関数です。

英単語でなんとなく推測できてしまう思うのですが、ふたつの dynamic point(木構造のノード)を結ぶ最短経路を取得し、木の浅い方向に行く経路では脱出用の手続きを、木の深い方向に行く経路では再入用の関数を、引数なしで呼び出す関数です。

pointdepth

$pointdepth:\mathrm{P}\rightarrow\mathrm{N}$
$pointdepth=\lambda\omega\ .\ \omega = root \rightarrow 0, 1 + (pointdepth\ (\omega\ |\ (\mathrm{F}\times\mathrm{F}\times\mathrm{P}\downarrow 3))$

dynamic point(木構造のノード)の深さを返す関数です。よくある再帰関数です。

ancestors

$ancestors:\mathrm{P}\rightarrow\mathrm{P}$

$ancestors=\lambda\omega\ .\ \omega = root \rightarrow {\omega}, {\omega}\ \cup\ (ancestors\ (\omega\ |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow3))$

dynamic point(木構造のノード) の ancestor の集合を返す関数です。これもよくある再帰関数です。

commonancest

$commonancest:\mathrm{P}\rightarrow\mathrm{P}\rightarrow\mathrm{P}$
$commonancest=\omega_1\omega_2\ .\ \text{the only element of}\ {\omega'\ |\omega' \in (ancestors\ \omega_1)\cap(ancestors \omega_2), pointdepth\ \omega' \geq pointdepth \omega''\ \forall\omega'' \in (ancestors\ \omega1)\cap(ancestors\ \omega_2)}$

ふたつの dynamic point の共通の ancestor のうち、最も深い位置にあるものを返す関数です。

英文の "the only element of" は記号で書くと煩雑になるから自然言語で書いているのでしょうか？集合の元を取り出すことと、元が唯一であることを、自然言語で書いています。

pathup

$pathup:\mathrm{P}\rightarrow\mathrm{P}\rightarrow(\mathrm{P}\times\mathrm{F})^*$
$pathup=\lambda\omega_1\omega_2\ .\ \omega_1 = \omega_2\rightarrow\langle\rangle,\langle(\omega_1,\omega_1 |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow2\rangle§(pathup(\omega_1\ |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow 3)\omega_2)$

dynamic point $\omega_1$ と $\omega_2$ の間にある脱出用の手続きを全て列挙する関数です。$\omega_2$ は $\omega_1$ の先祖でなければなりません。$\omega_1$自身に登録された脱出用の関数は返り値に含まれますが、 $\omega_2$ 自身に登録された脱出用の関数は返り値に含まれません。また、列の要素の順序は葉に近い方からの順序になっています。

$\omega_1 |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow2$ が $\omega_1$の脱出手続きを表していて、$\omega_1|(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow 3$ が$\omega_1$の親ノードを表しています。

pathdown

$pathdown:\mathrm{P}\rightarrow\mathrm{P}\rightarrow(\mathrm{P}\times\mathrm{F})^*$
$pathdown=\lambda\omega_1\omega_2\ .\ \omega_1 = \omega_2\rightarrow\langle\rangle,(pathdown\ \omega_1(\omega_2\ |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow 3))§\langle(\omega_2,\omega_2 |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow1\rangle$

$pathup$の逆で、再入用の手続きを列挙する関数です。
列の要素の順序は根に近い方からの順序になっています。

また、$\omega_2 |(\mathrm{F}\times\mathrm{F}\times\mathrm{P})\downarrow1$ が $\omega_2$の再入手続きを表しています。

travelpath

$travelpath:(\mathrm{P}\times\mathrm{F})^*\rightarrow\mathrm{C}\rightarrow\mathrm{C}$
$travelpath=\lambda\pi^*\theta\ .\ ＃\pi^*=0\rightarrow\theta,((\pi^*\downarrow1)\downarrow2)\langle\rangle((\pi^*\downarrow1)\downarrow1)(\lambda\epsilon^*\ .\ travelpath(\pi^*†1)\theta)$

手続きの列の要素を引数なしで順に呼び出す関数です。pathup や pathdown で列挙された手続きを呼び出すのに使われます。

dynamicwind

$dynamicwind:\mathrm{E}^*\rightarrow\mathrm{P}\rightarrow\mathrm{K}\rightarrow\mathrm{C}$
$dynamicwind=threearg(\lambda\epsilon_1\epsilon_2\epsilon_3\omega\kappa\ .\ (\epsilon_1\in\mathrm{F}\land\mathrm\epsilon_2\in\mathrm{F}\land\epsilon_3\in\mathrm{F})\rightarrow applicate\ \epsilon_1\langle\rangle\omega(\lambda\zeta^*\ .\ applicate\ \epsilon_2\langle\rangle((\epsilon_1|\mathrm{F},\epsilon_3|\mathrm{F},\omega)\ \mathrm{in}\ \mathrm{P})(\lambda\epsilon^*\ .\ applicate\ \epsilon_3\langle\rangle\omega(\lambda\zeta^*\ .\ \kappa\epsilon^*))), wrong\ \text{''bad procedure argument''})$

名前通り dynamic-wind です。

長さ3の手続きの列を受け取り、それを順に呼び出すのですが、2番目の手続きは新たな dynamic point を作成してそれを引数にして呼び出しています。$(\epsilon_1|\mathrm{F},\epsilon_3|\mathrm{F},\omega)\ \mathrm{in}\ \mathrm{P}$ の部分が新しく作られた dynamic point です。

values

$values:\mathrm{E}^*\rightarrow\mathrm{P}\rightarrow\mathrm{K}\rightarrow\mathrm{C}$
$values = \lambda\epsilon^*\omega\kappa\ .\ \kappa\epsilon^*$

Scheme の手続きのvaluesの意味論だと思います。どこからも使われていません。dynamic pointを無視して継続に多値を渡すだけですね。

cwv

$cwv:\mathrm{E}^*\rightarrow\mathrm{P}\rightarrow\mathrm{K}\rightarrow\mathrm{C}$
$cwv=twoarg(\lambda\epsilon_1\epsilon_2\omega\kappa\ .\ applicate\ \epsilon_1\langle\rangle\omega(\lambda\epsilon^*\ .\ applicate\ \epsilon_2\epsilon^*\omega))$

Scheme の call-with-values の意味論です。

$\epsilon_1$ を呼び出した結果の多値は $\epsilon^*$ に束縛されるのですが、それをそのまま $\epsilon_2$ の引数として呼び出しています。

再度𝓔, 𝓔^*, 𝓒

さて、下請け関数の説明が終わりましたので、後回しにしていた主人公こと $\mathcal E$です。

下請け関数から順に行きます。

𝓒

$\mathcal{C}[\hspace{-1pt}[]\hspace{-1pt}]=\lambda\rho\omega\theta\ .\ \theta$
$\mathcal{C}[\hspace{-1pt}[\Gamma_0\ \Gamma^*]\hspace{-1pt}]=\lambda\rho\omega\theta\ .\ \mathcal{E}[\hspace{-1pt}[\Gamma_0]\hspace{-1pt}]\rho\omega(\lambda\epsilon^*\ .\ \mathcal{C}[\hspace{-1pt}[\Gamma^*]\hspace{-1pt}]\rho\omega\theta)$

$\mathcal{C}[\hspace{-1pt}[\Gamma_0\ \Gamma_1\ \Gamma_2 \cdots]\hspace{-1pt}]$ のような形があったら、まず$\Gamma_0$を評価し、評価した結果を捨てて、$\mathcal{C}[\hspace{-1pt}[\Gamma_1\ \Gamma_2 \cdots]\hspace{-1pt}]$を評価するよ、と言っています。

最終的に $\mathcal{C}[\hspace{-1pt}[]\hspace{-1pt}]$ の形になったところで停止し、コマンド継続を返します。

𝓔^*

$\mathcal{E}^*[\hspace{-1pt}[]\hspace{-1pt}]=\lambda\rho\omega\kappa\ .\ \kappa\langle\rangle$
$\mathcal{E}^*[\hspace{-1pt}[\mathrm{E_0}\ \mathrm{E}^*]\hspace{-1pt}]=\lambda\rho\omega\kappa\ .\ \mathcal{E}[\hspace{-1pt}[\mathrm{E_0}]\hspace{-1pt}]\rho\omega(single(\lambda\epsilon_0\ .\ \mathcal{E}^*[\hspace{-1pt}[\mathrm{E}^*]\hspace{-1pt}]\rho\omega(\lambda\epsilon^*\ .\ \kappa(\langle\epsilon_0\rangle§\epsilon^*))))$

引数評価用の$\mathcal E$の補助関数です。

エラー処理などを無視すると、大雑把には、 $\mathcal{E}^*[\hspace{-1pt}[\mathrm{E_0}\ \mathrm{E_1}\ \mathrm{E_2} \cdots]\hspace{-1pt}]$ のような形と$\lambda\rho\omega\kappa\ .\ \kappa\langle\mathcal{E}[\hspace{-1pt}[\mathrm{E_0}]\hspace{-1pt}]\downarrow 1, \mathcal{E}[\hspace{-1pt}[\mathrm{E_1}]\hspace{-1pt}]\downarrow 1, \mathcal{E}[\hspace{-1pt}[\mathrm{E_2}]\hspace{-1pt}]\downarrow 1, \cdots\rangle$ のような形とが同じになります。

𝓔〚I〛

$\mathcal{E}[\hspace{-1pt}[{\tt I}]\hspace{-1pt}]=\lambda\rho\omega\kappa\ .\ hold(lookup\ \rho\ I)(single(\lambda\epsilon\ .\ \epsilon=undefined\rightarrow wrong \ \text{''undefined variable''}, send\ \epsilon\kappa$

identifier 評価の意味論です。

$lookup$ と $hold$ で identifier $\mathrm{I}$ に対応する値を取り出し、その値を$send$で expression continuation に渡し、 command continuation を返します。

𝓔〚(E₀ E^*)〛

$\mathcal{E}[\hspace{-1pt}[{\tt I}]\hspace{-1pt}]=\lambda\rho\omega\kappa\ .\ \mathcal{E}^*(permute(\langle\mathrm{E}_0\rangle§\mathrm{E}^*))\rho\omega(\lambda\epsilon^*\ .\ ((\lambda\epsilon^*\ .\ applicate(\epsilon^*\downarrow1)(\epsilon^*†1)\omega\kappa)(unpermute\ \epsilon^*)))$

手続き呼び出しの意味論です。

$\mathcal{E}^*(permute(\langle\mathrm{E}_0\rangle§\mathrm{E}^*))$ の部分で手続きと引数をすべて順不同で評価し、$unpermute$の部分でまた元の順序に戻します(言語仕様上引数の評価順序が規定されていないことを表しています)。

$applicate(\epsilon^*\downarrow1)(\epsilon^*†1)$の部分で評価された引数を評価された手続きに渡しています。

𝓔〚(lambda (I*) Γ* E₀)〛

$\mathcal{E}[\hspace{-1pt}[\mathrm{(lambda (I^*)\Gamma^*\ E_0)}]\hspace{-1pt}] = \lambda\rho\omega\kappa\ .\ \lambda\sigma\ .\ new\ \sigma\in\mathrm{L}\rightarrow send(\langle new\ \sigma|\mathrm{L}, \lambda\epsilon^*\omega'\kappa'\ .\ ＃\epsilon^*=＃\mathrm{I}^*\rightarrow tievals(\lambda\alpha^*\ .\ (\lambda\rho'\ .\ \mathcal{C}[\hspace{-1pt}[\Gamma^*]\hspace{-1pt}]\rho'\omega'(\mathcal{E}[\hspace{-1pt}[\mathrm{E}_0]\hspace{-1pt}]\rho'\omega'\kappa'))(extends\ \rho\mathrm{I}^*\alpha^*))\epsilon^*,$ $wrong\ \text{''wrong number of arguments''}\rangle\ \mathrm{in}\ \mathrm{E})\kappa(update\ (new\ \sigma|\mathrm{L})\ unspecified\ \sigma),wrong\ \text{''out of memory''}\ \sigma$

固定数引数の手続きを定義する semantic function です。手続きを定義し、それを値継続に渡し、コマンド継続を返します。

$tievals(\cdots (extends\ \rho\ \mathrm{I}^*\ alpha^*))$ の部分がidentifier を実引数に束縛する部分です。

$(\lambda\rho'\ .\ \mathcal{C}[\hspace{-1pt}[\Gamma^*]\hspace{-1pt}]\rho'\omega'(\mathcal{E}[\hspace{-1pt}[\mathrm{E}_0]\hspace{-1pt}]\rho'\omega'\kappa'))$ の部分が定義される関数本体です。

𝓔〚(lambda (I . I) Γ E₀)〛

rest引数付き手続き定義の semantic function です。
固定数引数の手続きを定義する semantic function とほぼ同じなので詳細は省略します。
$tievals$ の代わりに $tievalsrest$ になっている点や引数の数の比較に$\geq$を使っている点などが異なります。

𝓔〚(lambda I Γ^* E₀)〛

$\mathcal{E}[\hspace{-1pt}[\mathrm{(lambda\ I\ \Gamma^*\ E_0)}]\hspace{-1pt}] = \mathcal{E}[\hspace{-1pt}[\mathrm{(lambda\ (.\ I)\ \Gamma^*\ E_0)}]\hspace{-1pt}]$

rest引数のみの手続きを定義する semantic function です。

S式をこんな風に扱っていいのかと言いたくなる定義ですが、なんというか、まあ、これはこれで理にかなっています。
rest引数付き手続き定義の semantic function に落とし込んでいるわけですね。

どうでもいい余談ですが、(. X) と X は等しい、ということにしておくとS式パーサを書くのがほんの少し簡単になります。

𝓔〚(if E₀ E₁ E₂〛

$\mathcal{E}[\hspace{-1pt}[\mathrm{(if\ E_0\ E_1\ E_2)}]\hspace{-1pt}] = \lambda\rho\omega\kappa\ .\ \mathcal{E}[\hspace{-1pt}[\mathrm{E_0}]\hspace{-1pt}]\rho\omega(single(\lambda\epsilon\ .\ trueish\ \epsilon\rightarrow\mathcal{E}[\hspace{-1pt}[\mathrm{E_1}]\hspace{-1pt}]\rho\omega\kappa,\mathcal{E}[\hspace{-1pt}[\mathrm{E_2}]\hspace{-1pt}]\rho\omega\kappa))$

ほぼそのままかと思います。
見どころは $truish$ で $false$ 以外を全て $true$ に変換しているあたりでしょうか。

𝓔〚(if E₀ E₁〛

$\mathcal{E}[\hspace{-1pt}[\mathrm{(if\ E_0\ E_1\ E_2)}]\hspace{-1pt}] = \lambda\rho\omega\kappa\ .\ \mathcal{E}[\hspace{-1pt}[\mathrm{E_0}]\hspace{-1pt}]\rho\omega(single(\lambda\epsilon\ .\ trueish\ \epsilon\rightarrow\mathcal{E}[\hspace{-1pt}[\mathrm{E_1}]\hspace{-1pt}]\rho\omega\kappa,send\ unspecified\ \kappa))$

else節が $send\ unspecified\ \kappa$になっている以外は3引数ifと同じです。

𝓔〚(set! I E)〛

$\mathcal{E}[\hspace{-1pt}[\mathrm{(set!\ I\ E)}]\hspace{-1pt}] = \lambda\rho\omega\kappa\ .\ \mathcal{E}[\hspace{-1pt}[\mathrm{E}]\hspace{-1pt}]\rho\omega(single(\lambda\epsilon\ .\ assign(lookup\ \rho\ \mathrm{I})\ \epsilon\ (send\ unspecified\ \kappa))$

$assing(lookup\ \rho\ \mathrm{I})$ で $\mathrm{I}$ の束縛を変更し、 value continuation に$unspecified$ を渡します。

さいごに

これで一通り読み終わりました。

Scheme で「expression の評価」とされていたものは、「裏でこっそり environment と dynamic point と expression continuation を引数として引きずりまわしていました」ということがわかれば大体良いのではないでしょうか。

この記事を見て下さった方の中でも、途中で疲れて(あきれて？)ここまで飛ばしてくる人の方や、何かよくわからんかったという方も多いと思います。実のところ、書けば書くほど全てが当たり前に思えてきてしまって、何を解説すべきで何を省略すべきかわからなくなってしまいました。おそらくこの記事自体もひどく読みにくい代物になっていると思います。Scheme の表示的意味論を理解しようと思ったら、この文章を真剣に追いかけるのではなく、自分で解説文書を書いてみるとか、実際に手を動かして式を評価してみるとかすると良いのではないでしょうか。きっとすべてが当たり前に思えてくると思います(放り投げ)。