前回のCEK抽象機械を拡張して、ミュータブルな状態のある言語も自然に実行できるようにする。

CESK抽象機械

CEK抽象機械はControl（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つの要素を持つ。

CESK抽象機械はそこにStore（格納）を追加する。Storeは可変なメモリ領域を表す。

前回に続いて詳細についてはMatt Mightのブログ：

matt.might.net

あるいはFelleisen他の著作：

mitpress.mit.edu

を参照してほしい。

ちなみに今回のCESK拡張部分の実装に関してはMatt Mightのブログに厳密に準拠していない。コードやデザインに微妙なところがある責は私個人のものであることは断っておきたい。

型の変更

CEKをCESKに拡張するにあたってまず各種の型がどう定義されるかを見ていく。

値と環境：

type env = (string * int) list

type val_ =
| Int of int
| Bool of bool
| Closure of Ast.t * env

val_型には変更はないのだが、envが直接値を持つのではなく、変数の文字列とstoreのアドレスを指す整数のペアを持つようになる。ということでval_型と相互再帰する必要がなくなっている。

次にstore：

module Store = struct
  type t = {x:val_ array; mutable i:int}

  let n = 10000
  let init () = {x=Array.make n (Int 0); i=0}

  let get s = Array.get s.x
  let set s i v = Array.set s.x i v
  let add s v = Array.set s.x s.i v; s.i <- (s.i + 1); s.i-1
end

storeは「メモリ領域全体」を表すval_ arrayと「未使用のメモリ領域の先頭」を表す整数を持つレコードで表現される。

また、関連する関数がいくつかあるのでモジュール化。コンストラクタinit、特定アドレスの値を取得するget、特定アドレスに値を書き込むset、未使用のメモリ領域先頭に値を書き込むaddが定義されている。

getとsetはunitを、addは書き込み先のアドレスを返している。

最後に抽象機械の状態を表すcesk型：

type cesk = 
| Running of Ast.t * env * Store.t * kont
| Done of val_

cek型のRunning of Ast.t * env * kontにStore.tが追加されている。

アトミックな式の評価

アトミックな式を評価する際、CEKでは直接評価結果の値を返していた。CESKではまずstoreに書き込んでから、そのアドレスを返すかそのアドレスに入っている値を返すか使い分ける必要がある。

なのでeval_atomicとeval_store_atomicを分ける（前者は後者を呼び出している）：

let eval_store_atomic e env s = match e with
| A.Int n -> Store.add s (Int n)
| A.Bool b -> Store.add s (Bool b)
| A.Fn _ -> Store.add s (Closure(e,env))
| A.Var v -> List.assoc v env
| _ -> failwith "Evaluating non-atomic expression as atomic"

let eval_atomic e env s = Store.get s (eval_store_atomic e env s)

eval_store_atomicでは変数以外のアトミックな式は値をstoreに書き込んでからそのアドレスを返している。変数に関しては単に変数環境で対応するアドレスを探して返すだけ。この関数名は微妙だがあまりうまい名前が思いつかない・・・

eval_atomicではeval_store_atomicから返ってくるアドレスに入っている値をStore.getで取得して返す。

継続の実行

control部分の評価が終わって値を次の継続に渡すためのapply_kont関数：

let apply_kont k s i = match k with
| Halt -> Done (Store.get s i)
| Letkont(var,e,c,k) -> Running(c,(var,i)::e,s,k)

以前は値を直接次の継続に渡していたのだが、それを値が入っているstoreのアドレスを渡すように変更。

終端継続の場合はStore.get s iでそのアドレスから直接値を取り出す。（この記事を書いていて気づいたが、この部分に関してはDoneをDone of Store.t * iにして「最終状態の記憶領域と結果の値が入っているアドレス」にするべきだった。現在のデザインだと他のアドレスを参照しているような複雑な値を正しく返せない。）

Letkontの場合は変数環境に変数とアドレスのペアを追加した上で継続に格納されていた式を新しいcontrolとして実行。

状態遷移

状態遷移を表すstep関数については、前回の記事と同じように各パターンを個別に見ていく。

まずはcontrolにアトミックな式が来ている場合：

let step c e s k = match c with
| A.Int _ | A.Bool _ | A.Fn _ | A.Var _ -> apply_kont k s (eval_store_atomic c e s)

apply_kontに渡すのが値そのものではなく、store上のアドレスになっているのでeval_store_atomicしている。

和や比較：

| A.Add(e1,e2) -> (match eval_atomic e1 e s, eval_atomic e2 e s with
  | Int n, Int m -> apply_kont k s (Store.add s @@ Int(n+m))
  | _ -> failwith "Adding non-integer values")
| A.Lt(e1,e2) -> (match eval_atomic e1 e s, eval_atomic e2 e s with
  | Int n, Int m -> apply_kont k s (Store.add s @@ Bool(n<m))
  | _ -> failwith "Comparing non-integer values")

これらは保持しているアトミック（なはず）なサブ式を評価し、整数値であることを確認してから新しい値（整数値か真偽値）を継続に渡す、という処理の流れになっている。まずサブ式をeval_atomicで評価（内部でeval_store_atomicとStore.getを使っているので「store上のアドレスに格納されている値」を返すことがことが保証されている）、その値のタプルに対してパターンマッチして結果をStore.addでstoreに書き込み、そのアドレスをapply_kontに渡している。

条件分岐とlet式：

| A.If(cond,e1,e2) -> (match eval_atomic cond e s with
  | Bool b -> Running((if b then e1 else e2), e, s, k)
  | _ -> failwith "Conditional on non-boolean")
| A.Let(var,e1,e2) -> Running(e1,e,s,Letkont(var,e,e2,k))

ほぼ変更なし。各種関数やコンストラクタの引数にstoreが増えたくらい。

関数適用：

| A.Call(f,es) -> (match eval_atomic f e s with
  | Closure(A.Fn(ss,body),e') ->
    let vs = List.map (fun v -> eval_store_atomic v e s) es in
    Running(body, (List.combine ss vs)@e', s, k)
  | _ -> failwith "Non-function in operator position")

変数環境が(変数の文字列, 値)ではなく(変数の文字列, アドレス)になっているので、仮引数と実引数のタプルも同じく実引数はアドレスで表現する必要がある。なのでeval_atomicではなくeval_store_atomicをList.mapに渡している。

しかし、よく見たらlet vs = List.map (fun v -> eval_store_atomic v e s) esってOCamlコードの変数名がめちゃくちゃだな・・・　1文字変数はやめよう・・・

使ってみる

前回と同じ例：

(+ 1 2)
(+ 1 2)
3

(if (< 1 2) (+ 1 (+ 3 4)) 5)
(let [g0 (< 1 2)] (if g0 (let [g1 (+ 3 4)] (+ 1 g1)) 5))
8

前回と同じく、とりあえずこれらの入力ではうまくいっているようだ。

今後

今回は抽象機械は拡張したけど言語機能は変更しなかったのでありがたみが感じにくい。これからstoreが加わったことを利用しrefなどの機能を追加していく。

今回のコード

gist.github.com

Arantium Maestum

プログラミング、囲碁、読書の話題

CEK抽象機械をCESK抽象機械に拡張する