続きです

Scheme R7RSの形式意味論を見て行きます。

前回の続きとなります。
Scheme R7RSの形式意味論を読んでいく3 - nptclのブログ

【new】newの実装を考える

これ以降はnew関数が現れるため、メモリに関する説明が必要です。

newは新たにメモリ領域を確保する関数です。
関数の定義は次のようになります。

${\rm new} : {\rm S} \to {\rm L} + {{\tt error}}$
${\rm new} = {\rm 実装依存}$

「 ${\rm new} \: \sigma$ 」を実行したら、値を格納できる新しい場所が作成され、その位置 $\rm L$ が返却されます。

ただしメモリ割り当てに失敗する場合もあります。
そういうときは、 $\{{\tt error}\}$ というオブジェクトが返却されるそうです。
よって、new関数の戻り値は純粋な $\rm L$ ではありません。

new関数を使う時には、典型的な書き方があります。
${\rm new} \: \sigma \in {\rm L}$ で内容を確認し、もしエラーだったらwrong関数を呼び出すようにします。
例えば次のようになります。

${\rm new} \: \sigma \in {\rm L} \to {\rm 処理}, {\rm wrong} \: {\tt "out \: of \: memory"}$

new関数の内容を見て行きましょう。
仕様書にある説明は、次の一文だけです。

${\rm new} \: \sigma \in {\rm L}$ ならば $\sigma \: ({\rm new} \: \sigma \: | \: {\rm L}) \downarrow 2 = {\tt false}$

これは、新しく作成されたメモリの内容を表しています。
そもそも $\sigma$ が ${\rm E} \times {\rm T}$ を返却する関数なので、 newによって新規に作成されるものは $\langle {\rm E}, {\rm bool} \rangle$ という列になります。
その第二要素 $\rm T$ のブール値が、初期値はfalseだという意味です。
つまり、

$\langle {\rm undefined}, {\tt false} \rangle$

みたいな要素が作成されるのだと思います。

ここまでは何となく理解できます。
でも、そもそもfalseって何を意味することなの？
説明が全然ないから困るのです。

ここからは私が何となく思ったことを書きます。
合っているのかどうかは分かりません。
しかし無理やりにでも解釈しないと、後々の話を理解するのは不可能だと思います。
がんばってついてきて下さい。

まず第二要素のfalseは、確保されたけどまだ使われていない領域です。
この値がtrueにならない限り、 ${\rm new} \: \sigma$ は何回呼び出されても全く同じものを返却します。

実際に ${\rm new} \: \sigma$ が使われている所を見ると、何度も何度も ${\rm new} \: \sigma$ が呼び出されています。
一見すると、C言語で言うmalloc関数が何度も呼び出されているように見えます。
しかし多分違います。
${\rm new} \: \sigma$ が新たに違う要素を返却するには、すでに確保したされた列の第二要素がtrueになっていなければなりません。
その処理はupdate関数が行います。

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

実行内容は、メモリ $\sigma$ の位置 $\alpha$ にある内容を、 $\langle \epsilon, {\tt true} \rangle$ に書き換えるという意味です。
この操作を行った後で ${\rm new} \: \sigma$ を呼び出すと、全く違う位置が返却されるようになります。

上記の考え方が正しいと仮定して話を進めますが、残念ながら正しくない可能性もあります。
まず $\sigma$ の使い方が良くわからないのです。
変なふうに関数の引数に出てきたり、突然あらわれたりと、どういう扱われ方をしているのか全然わかりません。

もう少し詳しく $\sigma$ 見て行きましょう。

【new】 $\sigma$ の扱いを考える

$\sigma$ の扱いがあまりにもおかしいので、ちゃんと調べなければなりません。
まずはnewの使い方について見て行きましょう。

newは $\sigma$ に新しい要素を追加します。
引数の $\sigma$ に対して、破壊的に更新すると考えてもいいと思います。
新しい領域に値 $\epsilon$ を格納する方法が、 $\sigma [\epsilon / \alpha]$ という操作です。
ここで $\alpha$ というのは、 ${\rm new} \: \sigma \: | \: {\rm L}$ のことです。

$\sigma [\epsilon / \alpha]$ は破壊的ではありません。
$\sigma$ には全く手を付けずに、値が変更された新しい $\sigma_1$ が作成されます。
この考え方が非常に大事です。
もし複数の値を書き込みたいのであれば、元々の $\sigma$ ではなく、 $\sigma [\epsilon / \alpha]$ の方をたらいまわしにしなければなりません。

newには典型的な書き方がありますので、下記に示します。

$(\lambda \sigma \: . \: {\rm body})$
$\quad {\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: \epsilon \: \sigma$

この処理は、まずupdate関数が新しい領域に値 $\epsilon$ を割り当てています。
update関数の戻り値は、新しい $\sigma$ なので、をlambda式の引数に渡してbodyを実行しています。
つまり、古い $\sigma$ と新しい $\sigma$ を、lambda式を使って繋ぎ変えているのです。

問題があり、new関数はエラーチェックが必要です。
そこで次のような書き方をします。

$\lambda \sigma \: . \: {\rm new} \: \sigma \in {\rm L} \to$
$\quad {\rm body}$
$\quad ({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: \epsilon \: \sigma),$
$\quad {\rm wrong} \; {\tt "out \: of \: memory"} \: \sigma$

この書き方は、本当に意味が分かりません。
前に説明した「lambda式とマッカーシーの条件」を思い出して下さい。
つまり、次のように書き直すことができます。

${\rm new} \: \sigma \in {\rm L} \to$
$\quad \lambda \sigma \: . \: {\rm body} \: ({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: \epsilon \: \sigma),$
$\quad \lambda \sigma \: . \: {\rm wrong} \; {\tt "out \: of \: memory"} \: \sigma$

この考え方は合っていると思います。
しかし説明がつかないところもあります。
下記の例を見てください。

この例だと、 ${\rm new} \: \sigma \in {\rm L}$ の次にupdateが実行されるので、 lambda式内の $\langle {\rm new} \: \sigma \: | \: {\rm L}, \cdots \rangle$ のnewは、別の内容が新規で作成されるのでは？

何か解釈が間違っているかもしれません。
でも、そう言うものだと考えて無視しましょう。
なぜならもっと大きな問題があるからです。

いちばんおかしな部分を説明します。
上記のように苦労して $\sigma$ をネストしても、結局は $\sigma$ が無視されてしまっています。
そもそも $\sigma$ ってどこから出てきたんだ？と思いませんか。
$\sigma$ は $\rho$ とは違っていて、 $\cal E$ の引数には存在しません。
しかし、例えば ${\cal E} [\![{\rm I}]\!]$ なんかではメモリから値を取り出さなければいけません。
その取り出している処理はhold関数なのですが、すでに話題に出した通り、hold関数の中では $\sigma$ が突然出てきています。
そう言う部分はいっぱいあります。
たぶんですが、初めは $\sigma$ をたらいまわししていて、途中からやっぱりやめるわ、と言って $\sigma$ を削除しようとしたものの、そんなに簡単に削除できなくてめちゃくちゃになったのでは？

よくわからないので、もう $\sigma$ について考えるのをやめます。
無視していいと思います。
一応言っておきますが、私は素人ですので、何か間違っているとは思います。
でもこの辺の解釈に何日もかけてますので、これ以上は時間の無駄です。
Schemeの形式意味論は、メモリ関係やローカル変数などの扱いを確認するのではなく、実行時に値と継続の関係がどうなっているのかだけに注目したほうがいいでしょう。

【new】エラーのないnew関数

ごめんなさい。
前の説明であったように、 $\sigma$ あたりの説明はやめます。
そうなると、new関数のエラーと、updateのタイミングなど、シビアな部分にいちいちお付き合いする必要が無くなります。
自分が使いやすい、新しいnew関数を定義します。

通常のnew関数は、エラーの場合を考慮しています。
でも正直いらないのでは？
というのもLispのシステムは、newにエラーが生じた時点でほぼ続行不可能な状況なので、 abortしてしまう以外やりようがないのです。
Schemeではありませんが、Common Lispのsbclもclispもabortします。
私が作ったnptに至っては、Lispを諦めてC言語上で異常時の対応ができるようになっています。

Schemeの仕様書では、wrong関数に返却があります。
たぶんエラーが生じた後でも続けることができるようになっているのだと思います。
そんなのやめましょう。
エラーが生じたらabortする新しい関数wrong*を定義します。

${\rm wrong*} : {\rm X} \to \: ?$

内容は実装依存です。
こうすることで、new関数もかなり使いやすくなります。
newとupdateを同時にこなす、new*関数を定義します。

${\rm new*} : {\rm E} \to {\rm L}$
${\rm new*} = \lambda \epsilon \: . \: {\rm new} \: \sigma \in {\rm L} \to$
$\qquad \qquad \qquad (\lambda \alpha \: . \: {\rm prog2} \: ({\rm update} \: \alpha \epsilon \sigma) \: \alpha) ({\rm new} \: \sigma \: | \: {\rm L}),$
$\qquad \qquad \qquad {\rm wrong*} \: {\tt "out \: of \: memory"}$
${\rm prog2} = \lambda x y \: . \: y$

$\sigma$ の扱いが完全に不明のため、グローバル変数として使うことにしました。
戻り値の確認が無くなったため、非常に使いやすい関数になったと思います。
newの返却は「 ${\rm L} + {\tt \{error}\}$ 」なので、返却値はから $\rm L$ だけを取り出すには「 ${\rm new} \: \sigma \: | \: {\rm L}$ 」みたいな書き方をする必要がありましたが、 new*は $\rm L$ だけなのでそのまま使うことができます。

new*の例として、cons関数を定義すると次のようになります。

${\rm cons} = {\rm twoarg} (\lambda \epsilon_1 \epsilon_2 \omega \kappa \: . \: {\rm send} (\langle {\rm new*} \: \epsilon_1, {\rm new*} \: \epsilon_2, {\tt true} \rangle \: {\rm in} \: {\rm E}) \kappa)$

もとの内容と比べて見ると、ずいぶんすっきりしたと思います。

${\cal E} [\![({\tt lambda} \; ({\rm I^}) \; {\rm \Gamma^} \: {\rm E_0})]\!]$

定義を示します。

${\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!] =$
$\quad \lambda \rho \omega \kappa \: . \: \lambda \sigma \: . \:$
$\qquad {\rm new} \: \sigma \in {\rm L} \to$
$\qquad \quad {\rm send} (\langle {\rm new} \: \sigma \: | \: {\rm L},$
$\qquad \qquad \quad \:\: \lambda \epsilon^* \omega' \kappa' \: . \: \#\epsilon^* = \#{\rm I^*} \to$
$\qquad \qquad \:\: \qquad {\rm tievals} (\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \qquad \qquad \qquad \qquad \qquad \:\: ({\rm extends} \: \rho \: {\rm I^*} \: \alpha^*))$
$\qquad \qquad \qquad \qquad \quad \:\: \epsilon^*,$
$\qquad \qquad \:\: \qquad {\rm wrong} \: {\tt "wrong \: number \: of \: arguments"} \rangle$
$\qquad \qquad \quad \:\: {\rm in} \: {\rm E})$
$\qquad \qquad \quad \kappa$
$\qquad \qquad \quad ({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: {\tt unspecified} \: \sigma),$
$\qquad \quad {\rm wrong} \: {\tt "out \: of \: memory"} \: \sigma$

まずは「エラーのないnew関数」であるnew*を使うように書き直します。

${\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!] =$
$\quad \lambda \rho \omega \kappa \: . \: {\rm send} \: (\langle {\rm new*} \: {\tt unspecified},$
$\qquad \qquad \qquad \quad \lambda \epsilon^* \omega' \kappa' \: . \: \#\epsilon^* = \#{\rm I^*} \to$
$\qquad \qquad \qquad \qquad {\rm tievals} (\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad ({\rm extends} \: \rho \: {\rm I^*} \: \alpha^*))$
$\qquad \qquad \qquad \qquad \qquad \quad \epsilon^*,$
$\qquad \qquad \qquad \quad \quad {\rm wrong} \: {\tt "wrong \: number \: of \: arguments"} \rangle \: {\rm in} \: {\rm E})$
$\qquad \qquad \qquad \kappa$

ずいぶんとすっきりした形になりました。
説明をする前に、内部で使用されているtievals関数を見て行きます。

${\rm tievals} : ({\rm L^*} \to {\rm C}) \to {\rm E^*} \to {\rm C}$
${\rm tievals} =$
$\quad \lambda \psi \epsilon^* \sigma \: . \: \#\epsilon^* = 0 \to \psi \langle \rangle \sigma,$
$\qquad {\rm new} \: \sigma \in {\rm L} \to {\rm tievals} \: (\lambda \alpha^* \: . \: \psi \: (\langle {\rm new} \: \sigma \: | \: {\rm L} \rangle \: \S \: \alpha^*))$
$\qquad \qquad \qquad \qquad \qquad \quad (\epsilon^* \dagger 1)$
$\qquad \qquad \qquad \qquad \qquad \quad ({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: (\epsilon^* \downarrow 1) \: \sigma),$
$\qquad \qquad \qquad \qquad {\rm wrong} \: {\tt "out \: of \: memory"} \: \sigma$

こちらもまずはnew*で書き直します。

${\rm tievals} = \lambda \psi \epsilon^* \: . \: \#\epsilon^* = 0 \to \psi \langle \rangle,$
$\qquad {\rm tievals} \: (\lambda \alpha^* \: . \: \psi \: (\langle {\rm new*} \: (\epsilon^* \downarrow 1) \rangle \: \S \: \alpha^*)) \: (\epsilon^* \dagger 1)$

これはこれで合っているのですが、 $\lambda \alpha^*$ のクロージャーに $\epsilon^*$ 全体の値が保存されそうなので、ちょっと書き方を変えます。

${\rm tievals} = \lambda \psi \epsilon^* \: . \: \#\epsilon^* = 0 \to \psi \langle \rangle,$
$\qquad (\lambda \epsilon_1 \epsilon_2 \: . \: {\rm tievals} \: (\lambda \alpha^* \: . \: \psi \: (\langle {\rm new*} \: \epsilon_1) \rangle \: \S \: \alpha^*)) \: \epsilon_2)$
$\qquad \quad (\epsilon^* \downarrow 1) \: (\epsilon^* \dagger 1)$

tievalsは再帰呼出を使い、 $\epsilon^*$ の全ての要素にnew*を使い列を値を格納します。
入力は $\rm E$ の配列ですが、関数 $\psi$ に渡る前まではnew*の列なので $\rm L$ の配列です。
新しく得られた列に対して、関数 $\psi$ を実行して $\rm C$ が返却されます。
つまり、入力

$\langle \epsilon_1, \epsilon_2, \epsilon_3 \rangle$

が、new*によって

$\langle \alpha_1, \alpha_2, \alpha_3 \rangle$

になって、最後に

$\psi \langle \alpha_1, \alpha_2, \alpha_3 \rangle$

が実行されます。
これも典型的な再帰呼出なので、 Schemeで書くと例えばこんな感じになります。

(define (new x)
  (* x 10))  ;; ★確認のため10倍する

(define (tievals psi eps)
  (if (null? eps)
    (psi ())
    (let ((e1 (car eps))   ;; eps ↓ 1
          (e2 (cdr eps)))  ;; eps † 1
      (tievals
        (lambda (alpha)
          (psi (cons (new e1) alpha)))  ;; <new* e1> § α*
        e2))))

(tievals
  (lambda (x) (list '< x '>))
  '(10 20 30)))
-> (< (100 200 300) >)

それでは続けてextends関数の説明をします。

${\rm extends} : {\rm U} \to {\rm Ide^*} \to {\rm L^*} \to {\rm U}$
${\rm extends} = \lambda \rho {\rm I^*} \alpha^* \: . \: \#{\rm I^*} = 0 \to \rho,$
$\qquad \qquad \qquad {\rm extends} \, (\rho [ (\alpha^* \downarrow 1) / ({\rm I^*} \downarrow 1)]) \: ({\rm I^*} \dagger 1) \: (\alpha^* \dagger 1)$

この関数は、変数の列 $\rm I^*$ と、位置の列 $\rm L^*$ を受け取り、変数に対応する場所に位置を書き込んでいく関数です。
再帰関数なので、先頭にある要素からひとつずつ処理をして、残りの処理は自分自身に任せています。

それでは $\cal E$ に戻りましょう。
sendの部分を見ると、次のようになると思います。

${\rm send} \, (\langle {\rm new} \: {\tt unspecified}, \cdots \rangle \: {\rm in} \: {\rm E}) \: \kappa$

「 $\langle \cdots \rangle \: {\rm in} \: {\rm E}$ 」の意味が分からないのですけど、列に対して無理やり $\rm E$ を作ってよ、と言っているのだと思います。
sendの第一引数は $\rm E$ なので、これは問題ないと思います。
では $\cdots$ を見て行きます。

$\lambda \epsilon^* \omega' \kappa' \: . \: \#\epsilon^* = \#{\rm I^*} \to$
$\quad {\rm tievals} (\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \qquad \qquad \quad ({\rm extends} \: \rho \: {\rm I^*} \: \alpha^*))$
$\qquad \qquad \epsilon^*,$
$\quad {\rm wrong} \: {\tt "wrong \: number \: of \: arguments"}$

この式 $\lambda \epsilon^* \omega' \kappa'$ とは、引数の列、dynamic-points、継続を引数に取る関数であり、典型的なSchemeの関数を表しています。

内容は、まず継続から受け取った $\epsilon^*$ の列長さと、 lambda式の引数の列 $\rm I^*$ の長さを比べ、もし違っていたら、それは関数呼び出しの間違いなのでエラーになります。

これは単純に

(define (aaa x y z)  ;; I*の列
  ...)

みたいな関数があったとして、

(aaa 10 20 30 40)  ;; ε*の列

で呼び出した場合、引数 $\epsilon^*$ の長さが4なのに、 $\rm I^*$ の長さが3で合ってないじゃん。
ということになります。
長さチェックをクリアしたら、ようやくtievals関数の呼び出しです。
第一引数はどういう意味なのでしょうか。

$\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \quad ({\rm extends} \: \rho \: {\rm I^*} \: \alpha^*))$

lambda式が2つありますが、内側の方はただ単に extendsの戻り値を変数 $\rho'$ に代入しているだけです。
$({\rm extends} \; \rho {\rm I^*} \alpha^*)$ は、 $\rho$ を用いて、引数の変数に値を束縛していきます。
例えば、

${\rm I^*} = \langle x, y, z \rangle$
$\alpha^* = \langle 10, 20, 30 \rangle$

だった場合、 $\rho$ の変数表に $x$ は $10$ , $y$ は $20$ , $z$ は $30$ とメモリに書き込みます。
それがすんだら次は下記を実行します。

${\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa')$

なにやら複雑そうに見えますが、 lambdaのbody部を順番に実行して行っているようです。
まずは $\cal C$ の定義を見てみましょう。

${\cal C} [\![\,]\!] = \lambda \rho \omega \theta \: . \: \theta$
${\cal C} [\![\Gamma_0 \: \Gamma^*]\!] = \lambda \rho \omega \theta \: . \: {\cal E} [\![\Gamma_0]\!] \rho \omega (\lambda \epsilon^* \: . \: {\cal C} [\![\Gamma^*]\!] \rho \omega \theta)$

もはや見慣れてしまった再帰関数の実行です。
最初に形式意味論の式を見たときは本当に意味不明だったけど、そろそろ慣れてきたのが驚きです。

まず ${\cal C} [\![\,]\!]$ ですが、ただ単に継続 $\theta$ を返却するだけです。
次に ${\cal C} [\![\Gamma_0 \: \Gamma^*]\!]$ は、まず ${\cal E} [\![\Gamma_0]\!]$ を普通に実行します。
ただし、継続を次のように置き換えています。

$\lambda \epsilon^* \: . \: {\cal C} [\![\Gamma^*]\!] \rho \omega \theta$

これは単純に残りの $\Gamma^*$ をひたすら実行するだけのようです。
なお引数の $\epsilon^*$ は、継続の引数なので、つまりは戻り値です。
上記の式では $\epsilon^*$ は無視されていますので、戻り値が捨てられているということです。

話を戻します。

${\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa')$

何かこれおかしくないですか。
まず $\cal C$ を実行するには、事前に3つの引数が必要になります。
つまり $({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa')$ を先に実行する必要があります。

実行する順番が変です。
本来であれば $\Gamma^*$ を全部実行してから $\rm E_0$ が実行されるはずです。
しかし今の状態だと、例えば、

(lambda ()
  (aaa)
  (bbb)
  (ccc))

という関数を実行した際、まずは真っ先に(ccc)が実行されることになります。
しかも(ccc)の実行が終わったら、(aaa)と(bbb)が実行されるのではなく、 (ccc)の実行結果がそのまま継続に渡されるので、 (aaa)と(bbb)は全てが終わった後に実行されます。
あってるのかな。
ちょっと自信ない。
何か勘違いしている可能性が高いですが話を進めます。

無理やり書き直すならこうなると思います。

$(\lambda \theta_{\tt ignore} \: . \: {\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa') \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' \theta_{\tt dummy}$

この式は、まず真っ先に $\Gamma^*$ が実行されます。
ただし $\cal C$ は引数にコマンドの継続が必要なので、適当な継続 $\theta_{\tt dummy}$ を渡しました。
あらかじめ用意しておいてください。
用意できないなら $\theta_{\tt dummy} = \lambda \sigma \: . \: {\tt undefined}$ で全然問題ありません。
引数に渡した継続はどうせ無視されます。
$\cal C$ の返却値は $\lambda$ の引数に渡されますが、すぐに $\cal E$ を実行するので $\theta_{\tt ignore}$ は捨てられます。
たぶんこれでうまく行くはず。

${\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!]$ の実行をまとめます。
まずはローカル変数を作り、継続から変数と値を割り当てます。
そのあとbody部を実行し、最後の式を返却値として継続に渡します。
以上です。

${\cal E} [\![({\tt lambda} \; ({\rm I^} \: . \: {\rm I}) \; {\rm \Gamma^} \: {\rm E_0})]\!]$

定義を示します。

${\cal E} [\![({\tt lambda} \; ({\rm I^*} \: . \: {\rm I}) \; {\rm \Gamma^*} \: {\rm E_0})]\!] =$
$\quad \lambda \rho \omega \kappa \: . \: \lambda \sigma \: . \:$
$\qquad {\rm new} \: \sigma \in {\rm L} \to$
$\qquad \quad {\rm send} (\langle {\rm new} \: \sigma \: | \: {\rm L},$
$\qquad \qquad \quad \:\: \lambda \epsilon^* \omega' \kappa' \: . \: \#\epsilon^* \ge \#{\rm I^*} \to$
$\qquad \qquad \qquad \quad {\rm tievalsrest}$
$\qquad \qquad \qquad \qquad (\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \qquad \qquad \qquad \;\;\; ({\rm extends} \: \rho \: ({\rm I^*} \: \S \: \langle {\rm I} \rangle) \: \alpha^*))$
$\qquad \qquad \qquad \qquad \epsilon^*$
$\qquad \qquad \qquad \qquad (\#{\rm I^*}),$
$\qquad \qquad \qquad \quad {\rm wrong} \: {\tt "\: Too \: few \: arguments"} \rangle \: {\rm in} \: {\rm E})$
$\qquad \qquad \quad \kappa$
$\qquad \qquad \quad ({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \: {\tt unspecified} \: \sigma),$
$\qquad \quad {\rm wrong} \: {\tt "out \: of \: memory"} \: \sigma$

「エラーのないnew関数」で書き直します。

${\cal E} [\![({\tt lambda} \; ({\rm I^*} \: . \: {\rm I}) \; {\rm \Gamma^*} \: {\rm E_0})]\!] =$
$\quad \lambda \rho \omega \kappa \: . \: {\rm send} \: (\langle {\rm new*} \: {\tt unspecified},$
$\qquad \qquad \qquad \quad \lambda \epsilon^* \omega' \kappa' \: . \: \#\epsilon^* \ge \#{\rm I^*} \to$
$\qquad \qquad \qquad \qquad {\rm tievalsrest}$
$\qquad \qquad \qquad \qquad \quad (\lambda \alpha^* \: . \: (\lambda \rho' \: . \: {\cal C}[\![\Gamma^*]\!] \rho' \omega' ({\cal E}[\![{\rm E_0}]\!] \rho' \omega' \kappa'))$
$\qquad \qquad \qquad \qquad \qquad \quad \;\;\; ({\rm extends} \: \rho \: ({\rm I^*} \: \S \: \langle {\rm I} \rangle) \: \alpha^*))$
$\qquad \qquad \qquad \qquad \quad \epsilon^*$
$\qquad \qquad \qquad \qquad \quad (\#{\rm I^*}),$
$\qquad \qquad \qquad \quad {\rm wrong} \: {\tt "\: Too \: few \: arguments"} \rangle \: {\rm in} \: {\rm E})$
$\qquad \qquad \qquad \kappa$

前に解説した ${\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!]$ とほぼ同じです。
違う部分は下記の通り。

引数の個数チェックが $\ge$ に
tieval関数ではなく、tievalrest関数の呼び出しに

引数の個数チェックについては分かると思います。
等しいのではなく、継続の値の方が多い分には問題ありません。

tievalsrest関数は説明する必要があります。

${\rm tievalsrest} : ({\rm L^*} \to {\rm C}) \to {\rm E^*} \to {\rm N} \to {\rm C}$
${\rm tievalsrest} =$
$\quad \lambda \psi \epsilon^* \nu \: . \: {\rm list} \: ({\rm dropfirst} \: \epsilon^* \nu)$
$\qquad \qquad \qquad ({\rm single} (\lambda \epsilon \: . \: {\rm tievals} \: \psi ( ({\rm takefirst} \: \epsilon^* \nu) \: \S \: \langle \epsilon \rangle) ) )$

説明してない関数が3つも出てきます。

dropfirst
takefirst
list

まずは先にこれらの関数を説明して行きます。

${\rm dropfirst} = \lambda l n \: . \: n = 0 \to l, {\rm dropfirst} \: (l \dagger 1) \: (n - 1)$
${\rm takefirst} = \lambda l n \: . \: n = 0 \to \langle \rangle, \langle l \downarrow 1 \rangle \: \S \: ({\rm takefirst} \: (l \dagger 1) \: (n - 1))$

dropfirstは列の最初から $n$ 番目までが削除された列を返却します。
takefirstは列の $n$ 番目より先の列を返却します。

例を見るとすぐわかると思います。

${\rm dropfirst} \: \langle a, b, c, d, e, f \rangle \: 4 \to \langle e, f \rangle$
${\rm takefirst} \: \langle a, b, c, d, e, f \rangle \: 4 \to \langle a, b, c, d \rangle$

あと、dropfirstは $(l \downarrow n)$ と同じです。
なぜ同じものを関数として作ったのかというと、おそらくはtakefirstと合わせたかったのでしょう。

それではlistの定義を示します。

${\rm list} : {\rm E^*} \to {\rm P} \to {\rm K} \to {\rm C}$
${\rm list} = \lambda \epsilon^* \omega \kappa \: . \: \#\epsilon^* = 0 \to {\rm send} \: {\tt null} \: \kappa,$
$\qquad \qquad \qquad \qquad {\rm list} \: (\epsilon^* \dagger 1) \: ({\rm single} \: (\lambda \epsilon \: . \: {\rm cons} \langle \epsilon^* \downarrow 1, \epsilon \rangle \: \kappa))$

この関数にも問題があり、引数の数が一致してません。
しかしいつも通り「暗黙のlambda式」のパターンではなく、宣言の数は3つで合っているのですが、関数呼び出しが全部2つになっています。
よくよく見てみると、引数の $\omega$ が使われていないので、 list関数は引数を2個に出来そうです。
書き換えるのは少々手間がかかるので、まずはlist関数の意味を説明して話を進めます。

list関数の目的は、列をリストに変えることです。
引数 $\epsilon^*$ は列であり、再帰呼出によってリストを作り、それを継続 $\kappa$ に渡して実行します。
もう少し説明しますが、列とは形式意味論だけで使われている $\langle 10, 20, 30 \rangle$ のよう値です。
一方リストとは、Schemeで使われるペアの集合です。
ペアとは、コンスとも呼ばれており、car, cdrの二つの値を取るオブジェクトです。
ペアを(car . cdr)と表すとき、 10, 20, 30,の値を持つリストは (10 . (20 . (30 . ())))と表すことができます。
ペアを作る処理はcons関数であり、 list関数内で呼び出されています。

それではtievalsrestに戻りますが、この関数は引数を3つ受け取ります。
第一引数 $\psi$ は、tievalsの時と同様、最終的に呼び出される関数です。
第二引数 $\epsilon^*$ は、関数呼び出しの引数の列です。
第三引数 $\nu$ は、lambda式で必須の引数の個数です。
例えば

(lambda (x y . z)
  ...)

の場合、必須の引数はxとyなので、 $\nu$ は2です。
仮にこの関数が次の引数で呼び出された場合、

$\epsilon^* = \langle 10, 20, 30, 40, 50 \rangle$

tievalsrest関数内でdropfirstが列を削除するので、次のようにlist関数が実行されます。

${\rm list} \: \langle 30, 40, 50 \rangle ({\rm single} \: \cdots)$

list関数は(30 40 50)というリストを作成した後、継続内で次の文を実行します。

${\rm tievals} \: \psi ( ({\rm takefirst} \: \epsilon^* \nu) \: \S \: \langle \epsilon \rangle))$

ここで、

$\epsilon^* = \langle 10, 20, 30, 40, 50 \rangle$
$\nu = 2$
$\epsilon = (30 \: 40 \: 50)$
$({\rm takefirst} \: \epsilon^* \nu) = \langle 10, 20 \rangle$

なので、

${\rm tievals} \: \psi \langle 10, 20, (30 \: 40 \: 50) \rangle$

という文が実行されます。
なお、 $\langle \cdots \rangle$ は列であり、 $( \cdots )$ はリストです。

あとは今作成した列にあうように、extends関数でcdr部の変数を加えれば、前に説明した ${\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!]$ と同じになります。
分かりづらい所は、リストを作るときにちゃんコンスで作っているということでしょうか。

最後にlist関数を書き換えます。
list関数はtievalsrest関数でしか呼び出されていないようなので、引数の $\omega$ を消してしまいましょう。

${\rm list} : {\rm E^*} \to {\rm K} \to {\rm C}$
${\rm list} = \lambda \epsilon^* \kappa \: . \: \#\epsilon^* = 0 \to {\rm send} \: {\tt null} \: \kappa,$
$\qquad \qquad \qquad \qquad {\rm list} \: (\epsilon^* \dagger 1) \: ({\rm single} \: (\lambda \epsilon \: . \: {\rm cons} \langle \epsilon^* \downarrow 1, \epsilon \rangle \: {\tt \{root\}} \: \kappa))$

あわせてcons関数も書き換えたかったのですが、 cons関数内のtwoargを修正するのは手間だったので、それならダミーの値を渡してしまおうということで $\tt \{root\}$ を渡しています。
この値は $\omega \in {\rm P}$ の説明で出てくるものです。

以前紹介した、書き換えを行ったcons関数を再掲します。

${\cal E} [\![({\tt lambda} \;\; {\rm I} \;\; {\rm \Gamma^*} \: {\rm E_0})]\!]$

定義を示します。

${\cal E} [\![({\tt lambda} \;\; {\rm I} \;\; {\rm \Gamma^*} \: {\rm E_0})]\!] = {\cal E} [\![({\tt lambda} \;\; (. \: {\rm I}) \;\; {\rm \Gamma^*} \: {\rm E_0})]\!]$

うーん。
いいんじゃない？

${\cal E} [\![({\tt if} \; {\rm E_0} \; {\rm E_1} \; {\rm E_2})]\!]$

定義を示します。

${\cal E} [\![({\tt if} \; {\rm E_0} \; {\rm E_1} \; {\rm E_2})]\!] =$
$\qquad \lambda \rho \omega \kappa \: . \: {\cal E} [\![ {\rm E_0} ]\!] \rho \omega ({\rm single} \: (\lambda \epsilon \: . \: {\rm truish} \: \epsilon \to {\cal E} [\![ {\rm E_1} ]\!] \rho \omega \kappa, {\cal E} [\![ {\rm E_2} ]\!] \rho \omega \kappa))$

非常に分かりやすい文です。
まずは $\rm E_0$ を実行し、返却値を継続に渡します。
継続では返却値を元に、 $\rm E_1$ か $\rm E_2$ かの実行を選択します。
truish関数の定義を見てみましょう。

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

要するに、false以外が真ということです。

${\cal E} [\![({\tt if} \; {\rm E_0} \; {\rm E_1})]\!]$

定義を示します。

${\cal E} [\![({\tt if} \; {\rm E_0} \; {\rm E_1})]\!] =$
$\qquad \lambda \rho \omega \kappa \: . \: {\cal E} [\![ {\rm E_0} ]\!] \rho \omega ({\rm single} \: (\lambda \epsilon \: . \: {\rm truish} \: \epsilon \to {\cal E} [\![ {\rm E_1} ]\!] \rho \omega \kappa, {\rm send} \: {\tt unspecified} \: \kappa))$

こちらも難しくないです。
else項が省略されたら、unspecifiedを返却してくださいとのこと。
注釈があり「別にunspecifiedにこだわらず、何を返却しても良いよ、でもundefinedだけはやめてね。」だそうです。

${\cal E} [\![({\tt set!} \; {\rm I} \; {\rm E})]\!]$

定義を示します。

${\cal E} [\![({\tt set!} \; {\rm I} \; {\rm E})]\!] =$
$\quad \lambda \rho \omega \kappa \: . \: {\cal E} [\![ {\rm E} ]\!] \rho \omega ({\rm single} \: (\lambda \epsilon \: . \: {\rm assign} \: ({\rm lookup} \: \rho {\rm I})$
$\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad \:\: \epsilon$
$\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad \:\: ({\rm send} \: {\tt unspecified} \: \kappa)))$

まずはassignを見てみましょう。

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

引数の数があっていませんので、暗黙のlambda式として書き直します。

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

この意味は少しわかりづらいです。
まずはupdate関数で位置 $\alpha$ に値 $\epsilon$ を代入します。
そのあと、lambda式が実行され、 $\theta$ がそのまま返却されます。

それではset!文に戻ります。
まずは $\cal E$ によって $\rm E$ が評価され、継続 $\kappa$ に結果が渡されます。
継続内ではlookup関数により、変数 $\rm I$ の位置が求められます。
そしてsend関数により、set!式の継続 $\kappa$ にunspecifiedが渡されてます。
その後、assign関数により値の代入処理を行います。

これって本当にあってる？
assign関数が実行するまえに、send関数で継続 $\kappa$ を実行していませんか？
本来だと継続 $\kappa$ を実行する前にassignで割り当てなければならないはず。
間違ってるように思えるんだがどうなんだろう。
この手の問題は、lambda式のbody部にもありました。

私が勘違いしている可能性が高いですが、書き直してみます。

${\rm assign*} : {\rm L} \to {\rm E} \to {\rm K} \to {\rm C}$
${\rm assign*} = \lambda \alpha \epsilon \kappa \: . \: \lambda \sigma \: . \:$
$\qquad {\rm send} \: {\tt unspecified} \: \kappa$
$\qquad ({\rm update} \: \alpha \epsilon \sigma)$