A正規化されたIRをCEK抽象機械で実行

前回で定義した言語とそのA正規化されたIRをインタプリタで実行したい。

というわけでまたしてもMatt Mightのブログを参考にする：

matt.might.net

こちらのブログはCESKマシンの話だが、今のところ破壊的変更を言語機能として実装してないので、まずはCESKのステートSを抜いてCEK抽象機械での実行を目指す。

CEK抽象機械

CEK抽象機械というのは大雑把にいうとSECD抽象機械の仲間で、抽象機械の状態とその変遷関数を厳密に定義することで「プログラムの実行」をモデル化するもの。CEKという名前はこの抽象機械の状態を構成する三つの要素の頭文字（？）からきている。Control（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つである。

(control, environment, kontinuation)という状態を変遷関数stepに渡すとcontrolの形を元に条件分岐する。

controlが簡単な式であるなら直ちに評価する。結果が値ならkontinuationの先頭の継続をとってきて新しいcontrolに変換し、environmentに評価した値を追加した上で新しい状態(control', environment', kontinuation')を返す。結果が関数適用による新しい式と環境ならそのままそれを現在の継続と合わせて新しい状態(control', environment', kontinuation)として返す。結果が条件分岐による新しい式なら新しい状態(control', environment, kontinuation)として返す。などなど。

controlが複雑な式なら分解して、次に「実行するべき」式を新しいcontrolに、それ以外はkontinuationに追加する形で退避させておくことで新しい状態(control', environment', kontinuation')を返す。

余談だが以前作ったS式言語のインタプリタも、作った後にCEK機械の再実装であることがわかった：

zehnpaard.hatenablog.com

ある意味自然に導出されるようなインタプリタ形態なのかもしれない。

CEK抽象機械の詳細に関しては上記のMatt MightのブログやFelleisen他のSemantics Engineering with PLT Redexに詳しく載っている：

mitpress.mit.edu

特に後者ではラムダ計算を愚直に実行するインタプリタから効率・機能を求めてCEK、CESK抽象機械に段階的に発展していく経緯やSECD抽象機械との比較なども載っていて面白い。

CEKマシンの実装

cek.mlモジュールでCEK抽象機械を実装する。

まずは式を評価した結果となる値と、その値に変数を束縛する変数環境の二つを型として定義：

type val_ =
| Int of int
| Bool of bool
| Closure of Ast.t * env
and env = (string * val_) list

クロージャも値の一つで、クロージャは変数環境も持つ。なので値と変数環境は相互再帰的な型になる。

次は継続の型：

type kont =
| Letkont of string * env * Ast.t * kont
| Halt

A正規化したIRに特化したCEK抽象機械の特徴として、継続が非常に簡単になっている。「そのまま評価できない複雑な式」というのが必ずlet v = simple_exp in ...という形になっている、というA正規化形の性質を利用してLetkontという継続と、終端継続であるHaltのみを定義。

CEK抽象機械の状態は「実行中」の(control, environment, kontinuation)のタプルか、「評価結果」の値：

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

値を直接返す「アトミックな式」の評価関数：

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

値を継続に渡すためのヘルパ関数：

let apply_kont k v = match k with
| Halt -> Done v 
| Letkont(s,e,c,k) -> Running(c,(s,v)::e,k)

継続と値を受け取り、新たなCEK状態を返す。継続がHaltの場合は抽象機械が停止し、評価結果を返す。Letkontの場合には継続の仮引数s、継続の変数環境e、継続の式cそして残りの継続kが保持されている。受け取った値vをsと合わせて変数環境eを拡張し、その変数環境で式cを評価した結果の値を継続kに渡す、という新しいCEK状態を返す。

stepが抽象機械の動的な振る舞いの根本である変遷関数。

ASTノードに対してパターンマッチしているので各項目を個別に見ていく。

まずはアトミックな式から：

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

整数、真偽、関数、変数は直接eval_atomicで値に変換してからapply_kontで継続に渡している。

整数の和・比較：

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

+と<に関してはまず引数部分をアトミックな式として評価（もしアトミックでなければここでエラーになる）、引数が整数値であることを確認して（整数でなければまたしてもエラー）、和や比較結果を値として継続に渡している。

条件分岐：

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

条件分岐に関しては（厳密なA正規化かどうかは置いておいて）条件部分のみアトミックな式になっているはずなのでeval_atomicして結果がBoolであることを確かめ、その値によって次のcontrol式を選択して新しいCEK状態を返す。

let式：

| Ast.Let(s,e1,e2) -> Running(e1,e,Letkont(s,e,e2,k))

すでに述べたとおり、A正規化したIRだと継続を拡張する唯一のケースがlet式の評価。実際には何も評価せず、新しい継続を作った上で新しいCEK状態を返している。

関数適用：

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

関数部分、実引数部分すべてがアトミックな式であるはず。なのですべてに対してeval_atomicして、関数がクロージャ値であることを確認した上で(関数本体の式、仮引数・実引数で拡張されたクロージャの変数環境、元の継続)という新しいCEK状態を返す。

注意すべき点としてはすべてのeval_atomicが終わった時点で現在の変数環境は破棄されること。関数の本体部分の式はクロージャの変数環境で実行されるし、それ以降の評価ための環境は継続に保存されている。

これでstep関数は終わり。基本的に実行時エラーが多い。本来A正規化されたIRであれば通らないはずの条件分岐の部分なわけだが、IRの型がソース言語のASTと同一なのでこういった実行時チェックが必要になる。GADTなどで型としてA正規化を表現できればここら辺はスッキリしそう。

式を受け取り値を返すeval関数：

let eval c =
  let rec f = function
  | Running(c,e,k) -> f(step c e k)
  | Done v -> v
  in
  f (Running(c,[],Halt))

(実引数の式、空の環境、空の継続)というCEK状態を作成してstepを繰り返し適用し、状態が「停止」した時点で評価結果として値を返している。

val_型を文字列化するヘルパ関数も定義しておく：

let string_of_val = function
| Int n -> string_of_int n
| Bool b -> string_of_bool b
| Closure _ -> "closure"

使ってみる

main.mlを以下のように変更して使う：

let f s =
  Lexing.from_string s
  |> Parser.f Lexer.f
  |> Alpha.f
  |> Anormal.f

let () =
  let e = read_line() |> f in
  e |> L.Ast.to_string |> print_endline;
  e |> L.Cek.eval |> L.Cek.string_of_val |> print_endline;

これで受け取った式をまずA正規化してその式を出力、その後CEK抽象機械上でA正規化された式を実行してその結果を出力する。

試してみる：

(+ 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

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

今回のコード

（cek.mlとmain.ml以外は前回の記事のものを完全に流用）

gist.github.com