STG Version 2.5 の動作

準備

操作的意味論は，状態機械で定義されていて，遷移は評価ステップになっている．基本的な用語として，

アドレス

ヒープのアドレス．表現はなんでも良いが，通常の非負整数と思っておいてくれ．

値

以下の 2 種類:

• $\mathbf{Addr}\,a$ : アドレス
• $\mathbf{Int}\,n$ : プリミティブの整数

なお，プリミティブな値は増やそうと思えばいくらでも増やせるが，定義を書く上ではめんどいので，整数のみを扱う．

で使っていくのでよろしく．で，状態機械の状態は以下の要素の組として定義されている:

引数スタック ( $\mathit{as}$ )

値の列．関数の引数として使用されるやつらが入ってる．

返り値スタック ( $\mathit{rs}$ )

継続の列．これが tagless の所以なんだが，返り値スタックが使用されるのは case 式で， case はまず評価が終わった後の分岐 (パターンマッチ) を継続の形で返り値スタックに入れておき，評価値が返り値スタックの分岐から継続を選びそこを実行するみたいな感じになっている．実際の動きは，この後の操作的意味論を見ながら話す．

更新スタック ( $\mathit{us}$ )

サンクを評価する際に，現在のスタック情報を退避させておくためのフレームスタックで，退避させた引数スタックと返り値スタック，更新しているクロージャのアドレスの列が入っている．

ヒープ ( $h$ )

アドレスとクロージャの対応が入ってる．

グローバル環境 ( $\sigma$ )

トップレベルで束縛された変数とクロージャのアドレスの対応が入ってる．

命令

以下の 4 種類の命令:

• $\mathbf{Eval}\,e\,\rho$ : STG の式 $e$ を環境 $\rho$ で評価する．
• $\mathbf{Enter}\,a$ : アドレス $a$ にあるクロージャに，引数スタックに積まれてるものを引数として適用する．
• $\mathbf{ReturnCon}\,c\,\mathit{ws}$ : コンストラクタ $c$ とその適用された値 $ws$ から，返り値スタックにある継続を実行する．
• $\mathbf{ReturnInt}\,n$ : プリミティブ整数 $n$ から，返り値スタックにある継続を実行する．

なお， $\mathbf{ReturnInt}$ は $\mathbf{ReturnCon}$ のプリミティブ向け特殊版と考えれば良い．整数は引数無しのコンストラクタと大体同じ．

カッコ内に書いてあるのはメタ変数．以降はこの系統のメタ変数を使っていく．それから以下の補助関数を用意しておく:

この関数はまずローカルスコープで変数を探して，なかったらグローバルスコープで探し，その変数に対応するクロージャのアドレスを返す．では，実際の意味論を見ていく．

初期状態

まず， STG のプログラム

に対して初期状態は次のようになる:

最初はトップレベルの束縛の中に main 関数がある前提でそこから評価を始める．ここは本質じゃないので， $g_1$ とかから始めてもいい．トップレベルの束縛は， letrec 式に相当するので，自由変数の部分にトップレベルから取ってきたものをあてがって，ヒープに入れておく．

この状態から状態遷移を始めていく．

評価

まず， $\mathbf{Eval}$ 命令の遷移から見ていく．基本的に STG のそれぞれの式に対して，それに合う遷移をしていく．その定義は，以下のようになる:

let (rec) 式

$$\begin{array}{c} \langle \mathbf{Eval}\,\left(\begin{array}{lc} \text{\tt let} &x_1 = \mathit{vs}_1 \mathrel{\text{\tt \textbackslash}\pi_1} \mathit{xs}_1 \mathrel{\text{\tt ->}} e_1 \\ &\vdots \\ &x_n = \mathit{vs}_n \mathrel{\text{\tt \textbackslash}\pi_n} \mathit{xs}_n \mathrel{\text{\tt ->}} e_n \\ \text{\tt in}\,e \end{array}\right)\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{Eval}\,e\,\rho'\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h', \sigma ) \\ (\rho' = \rho\left[\begin{array}{c} x_1 \mapsto \mathbf{Addr}\,a_1 \\ \vdots \\ x_n \mapsto \mathbf{Addr}\,a_n \end{array}\right] , h' = h\left[\begin{array}{c} a_1 \mapsto \langle \mathit{vs}_1 \mathrel{\text{\tt \textbackslash}\pi_1} \mathit{xs}_1 \mathrel{\text{\tt ->}} e_1, \mathit{vals}(\langle \rho_{\mathit{rhs}}, []\rangle, \mathit{vs}_1)\rangle \\ \vdots \\ a_n \mapsto \langle \mathit{vs}_n \mathrel{\text{\tt \textbackslash}\pi_n} \mathit{xs}_n \mathrel{\text{\tt ->}} e_n, \mathit{vals}(\langle \rho_{\mathit{rhs}}, []\rangle, \mathit{vs}_n)\rangle \end{array}\right] , \rho_\mathit{rhs} = \rho ) \end{array}$$

letrec 式の場合は， $\rho_\mathit{rhs} = \rho'$ とする．この遷移は，単純に let で指定されたローカルのクロージャをヒープに確保し，そのアドレスを変数に結びつけるだけ． let と letrec の違いは作るクロージャでキャプチャするアドレスの違いで， let の場合は前の環境から， letrec の場合は今回確保したアドレスも含めてキャプチャする．

case 式

$$\langle \mathbf{Eval}\,(\text{\tt case}\,e\,\text{\tt of}\,\mathit{alts})\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{Eval}\,e\,\rho\rangle( \mathit{as}, \langle\mathit{alts}, \rho\rangle\mathbin{:}\mathit{rs}, \mathit{us}, h, \sigma )$$

この遷移では，分岐の継続を返り値スタックに積んだ後，対象の式の評価に移る．最終的に $\mathbf{ReturnCon}$ とか $\mathbf{ReturnInt}$ で帰ってきて，元の環境で継続に復帰する．

適用

$$\begin{array}{c} \langle \mathbf{Eval}\,(f\,\mathit{xs})\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{Enter}\,a\rangle( \mathit{as'}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ (\mathit{val}(\langle \rho, \sigma\rangle, f) = \mathbf{Addr}\,a, \mathit{as'} = \mathit{vals}(\langle \rho, \sigma\rangle, \mathit{xs}) \mathbin{++} \mathit{as}) \\ \\ \langle \mathbf{Eval}\,(v\,\{\})\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{ReturnInt}\,n\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ (\mathit{val}(\langle \rho, \sigma\rangle, v) = \mathbf{Int}\,n) \end{array}$$

変数への適用の場合 2 種類あって，クロージャへ引数を適用する場合とプリミティブ整数の評価の場合．クロージャの場合変数には $\mathbf{Addr}$ が結びついていて，プリミティブ整数の場合 $\mathbf{Int}$ が結びついてる．クロージャの場合，引数を引数スタックに積み込んで適用に移る．プリミティブ整数の場合，そのまま継続への復帰に遷移する．

コンストラクタ適用

$$\langle \mathbf{Eval}\,(c\,\mathit{xs})\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{ReturnCon}\,c\,\mathit{vals}(\langle \rho, \sigma\rangle, \mathit{xs})\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma )$$

コンストラクタへの適用は，単純に適用された変数から値を持ってきて，継続へ復帰するだけ．

プリミティブ

$$\begin{array}{c} \langle \mathbf{Eval}\,n\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{ReturnInt}\,n\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ \\ \langle \mathbf{Eval}\,(\oplus\,\{x_1, x_2\})\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle \mathbf{ReturnInt}\,(i_1 \oplus i_2)\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ (\mathit{vals}(\langle \rho, \sigma\rangle, \{x_1, x_2\}) = [\mathbf{Int}\,i_1, \mathbf{Int}\,i_2]) \end{array}$$

プリミティブ整数やプリミティブ演算は，そのまま継続へ復帰するだけ． STG では必ず評価は case 式でのみ行われるので，プリミティブ演算の引数にサンクは入ってこないことに注意．サンクを入れたい場合， case でサンクを潰した後それを束縛して渡してやる必要がある．

適用

次に， $\mathbf{Enter}$ 命令の遷移から見ていく． $\mathbf{Enter}$ 命令は，引数が充足してる場合は更新フラグを見て，いい感じに処理をする．その定義は，以下のようになる．

更新不要クロージャ

$$\begin{array}{c} \langle\mathbf{Enter}\,a\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Eval}\,e\,\rho\rangle( \mathit{as'}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ ( \mathit{ws}_a \mathbin{++} \mathit{as'} = \mathit{as} , |\mathit{ws}_a| = |\mathit{xs}| , \rho = [\mathit{vs} \mapsto \mathit{ws}_f, \mathit{xs} \mapsto \mathit{ws}_a] , h(a) = \langle\mathit{vs} \mathrel{\text{\tt \textbackslash n}} \mathit{xs} \mathrel{\text{\tt ->}} e, \mathit{ws}_f\rangle ) \end{array}$$

引数が充足してて更新不要なクロージャの場合，単なる関数適用を行う．環境はキャプチャしておいた自由変数と，引数の変数分を作って渡す．なお，論文中だとヒープからクロージャのアドレスを抜き去ってるように見えるんだが，大丈夫なんだろか．とりあえず，こっちでは修正しといた．ただ，表記法が定義されてないので，解釈違いかもしれん．

更新可能クロージャ

$$\begin{array}{c} \langle\mathbf{Enter}\,a\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h[a \mapsto \langle\mathit{vs} \mathrel{\text{\tt \textbackslash u}} \{\} \mathrel{\text{\tt ->}} e, \mathit{ws}_f\rangle], \sigma ) \Rightarrow \langle\mathbf{Eval}\,e\,\rho\rangle( [], [], \langle\mathit{as}, \mathit{rs}, a\rangle \mathbin{:} \mathit{us}, h, \sigma ) \\ (\rho = [\mathit{vs} \mapsto \mathit{ws}_f]) \end{array}$$

更新が必要なクロージャ，つまりサンクは，古いクロージャのアドレスをヒープから消し，更新スタックに情報を退避させて，評価を行う．ところで，この時もし古いクロージャのアドレスにアクセスして評価するような STG プログラムがあれば，そのアドレスを消してしまっていると問題が起きる．ただ，更新中に更新してるクロージャに再度アクセスがあるということは，つまり無限ループが発生してるってことでもある．これは論文中ではブラックホールと呼ばれていて，実際の実行マシンではこれを検出し，エラーを出すようにしてる．

部分適用

$$\begin{array}{c} \langle\mathbf{Enter}\,a\rangle( \mathit{as}, [], \langle \mathit{as}_u, \mathit{rs}_u, a_u\rangle\mathbin{:}\mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Enter}\,a\rangle( \mathit{as} \mathbin{++} \mathit{as}_u, \mathit{rs}_u, \mathit{us}, h', \sigma ) \\ \left(\begin{array}{c} h(a) = \langle \mathit{vs}\mathrel{\text{\tt \textbackslash n}}\mathit{xs}\mathrel{\text{\tt ->}} e, \mathit{ws}_f\rangle, |\mathit{as}| < |\mathit{xs}| \\ \mathit{xs}_1 \mathbin{++} \mathit{xs}_2 = \mathit{xs}, |\mathit{xs}_1| = |\mathit{as}|, h' = h[a_u \mapsto \langle (\mathit{vs} \mathbin{++} \mathit{xs}_1)\mathrel{\text{\tt \textbackslash n}}\mathit{xs}_2\mathrel{\text{\tt ->}} e, \mathit{ws}_f \mathbin{++} \mathit{as}\rangle] \end{array}\right) \end{array}$$

引数スタックの要素の数が，クロージャに必要な引数の数に満たない時は，クロージャへの適用は部分適用扱いになる．部分適用の場合，部分適用を表すサンクの評価中なはずなので，サンクの内容を既に分かっている部分はキャプチャして，本来の引数の数を受け取る関数を表すクロージャに更新する．そして，サンクに適用されたはずの引数を退避させた更新スタックから取り出してきて，もう一度適用をやり直す．

意味論上はこの規則で問題ないのだが，実装する時のことを考えると， $(\mathit{vs} \mathbin{++} \mathit{xs}_1)\mathrel{\text{\tt \textbackslash n}}\mathit{xs}_2\mathrel{\text{\tt ->}} e$ というクロージャを部分適用の際に作成するのはかなりめんどくさい．クロージャの中身はコンパイル時に通常生成されるわけだが，この場合動的に生成する必要が出てくる．または，全ての部分適用を想定して， $e$ 度に専用のクロージャコードをコンパイル時に生成するという方法も考えられる (普通はこちらが正攻法になる) ．ただ，もちろんそれはコンパイル時生成コードが大量に出てくるので避けたい．そこで，規則を以下のように変えることが考えられる:

$$\begin{array}{c} \langle\mathbf{Enter}\,a\rangle( \mathit{as}, [], \langle \mathit{as}_u, \mathit{rs}_u, a_u\rangle\mathbin{:}\mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Enter}\,a\rangle( \mathit{as} \mathbin{++} \mathit{as}_u, \mathit{rs}_u, \mathit{us}, h', \sigma ) \\ \left(\begin{array}{c} h(a) = \langle \mathit{vs}\mathrel{\text{\tt \textbackslash n}}\mathit{xs}\mathrel{\text{\tt ->}} e, \mathit{ws}_f\rangle, |\mathit{as}| < |\mathit{xs}| \\ \mathit{xs}_1 \mathbin{++} \mathit{xs}_2 = \mathit{xs}, |\mathit{xs}_1| = |\mathit{as}|, h' = h[a_u \mapsto \langle (f \mathbin{:} \mathit{xs}_1)\mathrel{\text{\tt \textbackslash n}}\text{\tt \{\}}\mathrel{\text{\tt ->}} f\,\mathit{xs}_1, \mathbf{Addr}\,a \mathbin{:} \mathit{as}\rangle], \text{\(f\) は fresh な変数} \end{array}\right) \end{array}$$

こうしておくと，部分適用用のクロージャを作っておくだけで，それを共有することができ，コード生成量もその手間も削減することができる．クロージャへのエントリが 1 回増えるが，そこら辺はより低レベルの最適化で消えることも期待できる．

継続への復帰

最後に， $\mathbf{ReturnCon}$ 命令 / $\mathbf{ReturnInt}$ 命令の遷移から見ていく．継続への復帰は，両命令でやってることは同じなので，まず $\mathbf{ReturnCon}$ 命令だけ見ていく．その定義は，以下のようになる．

マッチする場合

$$\begin{array}{c} \langle\mathbf{ReturnCon}\,c\,\mathit{ws}\rangle( \mathit{as}, \langle \mathit{alts}, \rho\rangle\mathbin{:}\mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Eval}\,e\,\rho[\mathit{vs} \mapsto \mathit{ws}]\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ (\mathit{alts} = \cdots\mathbin{;} c\,\mathit{vs}\mathrel{\text{\tt ->}}e\mathbin{;} \cdots) \end{array}$$

継続のパターンマッチの中に該当するコンストラクタに対する継続があるときは，その継続に復帰する．

デフォルトケースの場合

$$\begin{array}{c} \langle\mathbf{ReturnCon}\,c\,\mathit{ws}\rangle( \mathit{as}, \langle \mathit{alts}, \rho\rangle\mathbin{:}\mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Eval}\,e_d\,\rho\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h, \sigma ) \\ (\mathit{alts} = \left(\begin{array}{c} c_1\,\mathit{vs}_1\mathrel{\text{\tt ->}}e_1\mathbin{;} \\ \vdots \\ c_n\,\mathit{vs}_n\mathrel{\text{\tt ->}}e_n\mathbin{;} \\ \text{\tt default}\mathrel{\text{\tt ->}}e_d \end{array}\right), \forall 1 \leq i \leq n\ldotp c \neq c_i) \end{array}$$

コンストラクタにパターンマッチするものがなくて，デフォルトケースでの継続があるときは，その継続に復帰する．

デフォルトケースでの束縛

$$\begin{array}{c} \langle\mathbf{ReturnCon}\,c\,\mathit{ws}\rangle( \mathit{as}, \langle \mathit{alts}, \rho\rangle\mathbin{:}\mathit{rs}, \mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{Eval}\,e_d\,\rho'\rangle( \mathit{as}, \mathit{rs}, \mathit{us}, h', \sigma ) \\ \left(\begin{array}{c} \mathit{alts} = \left(\begin{array}{c} c_1\,\mathit{vs}_1\mathrel{\text{\tt ->}}e_1\mathbin{;} \\ \vdots \\ c_n\,\mathit{vs}_n\mathrel{\text{\tt ->}}e_n\mathbin{;} \\ v\mathrel{\text{\tt ->}}e_d \end{array}\right), \forall 1 \leq i \leq n\ldotp c \neq c_i \\ \rho' = \rho[v \mapsto \mathbf{Addr}\,a], h' = h[a \mapsto \langle \mathit{vs}\mathrel{\text{\tt \textbackslash n}}\{\}\mathrel{\text{\tt ->}}c\,\mathit{vs}, \mathit{ws}\rangle] \\ \text{\(\mathit{vs}\) は \(|\mathit{vs}| = |\mathit{ws}|\) を満たす fresh な変数列} \end{array}\right) \end{array}$$

束縛のないデフォルトケースと同じように，コンストラクタにパターンマッチするものがなくて，束縛が必要なデフォルトケースでの継続があった場合，その継続に復帰する．ただ，結果を束縛する必要があるので，コンストラクタ適用に相当するクロージャを生成して，それを束縛変数に結びつける．

更新スタックからの復帰

$$\begin{array}{c} \langle\mathbf{ReturnCon}\,c\,\mathit{ws}\rangle( [], [], \langle \mathit{as}_u, \mathit{rs}_u, a_u\rangle\mathbin{:}\mathit{us}, h, \sigma ) \Rightarrow \langle\mathbf{ReturnCon}\,c\,\mathit{ws}\rangle( \mathit{as}_u, \mathit{rs}_u, \mathit{us}, h', \sigma ) \\ (h' = h[a_u \mapsto \langle \mathit{vs}\mathrel{\text{\tt \textbackslash n}}\{\}\mathrel{\text{\tt ->}}c\,\mathit{vs}, \mathit{ws}\rangle], \text{\(\mathit{vs}\) は \(|\mathit{vs}| = |\mathit{ws}|\) を満たす fresh な変数列} ) \end{array}$$

そもそも返り値スタックを使い切ってしまった場合，更新スタックに要素があるなら，それはサンクを評価した結果出てきた評価値ということなので，サンクのあった部分に評価後の結果を表すクロージャを挿入して，元の評価に戻る．

$\mathbf{ReturnInt}$ の場合，デフォルトケースでの束縛時にヒープ割り当てを行わないで直接整数を束縛変数に結びつけるぐらいの違いしかない．

遷移例

では，意味論に則って，実際に STG のプログラムを動かしてみる．以下のプログラムを動かしてみる:

main = {} \u {} ->
  let nil = {} \n {} -> Nil {}
      mapid = {} \u {} -> map1 {id}
  in case 1# of
    v ->
      let l = {v, nil} \n {} -> Cons {v, nil}
      in mapid {l}

id = {} \n {x} -> x {}

map1 = {} \n {f, xs} ->
  letrec mf = {f, mf} \n {ys} ->
            case ys {} of
              Nil {}       -> Nil {}
              Cons {z, zs} ->
                let fz   = {f, z} \u {} -> f {z}
                    mfzs = {mf, zs} \u {} -> mf {zs}
                in Cons {fz, mfzs}
  in mf {xs}

このプログラムを意味論に沿って動かすと，次の動作をする:

ヒープはサンクを潰す時ぐらいしか整理してないので，参照がなくなったものは随時消す GC を実装すれば簡単に実行マシンは作れそう．