2005年06月13日

MinCaml読解ノート: K正規化

K正規化の意味

K正規化は、複雑な計算の途中結果全てを変数として定義する。 これによって複雑な式が一連の単純な式に分解され、プログラムは順序づけられた単純な計算の繰り返しに姿を変える。

K正規化後の型であるKNormal.tにもそれが表れている。

type t =
  | Add of Id.t * Id.t
  | Sub of Id.t * Id.t
  | ...
  | IfEq of Id.t * Id.t * t * t
  | IfLE of Id.t * Id.t * t * t
  | Let of (Id.t * Type.t) * t * t
  | LetRec of fundef * t
  | LetTuple of (Id.t * Type.t) list * Id.t * t

全ての演算や関数適用は、式KNormal.tではなく変数Id.tをオペランドにとるようになり、KNormal.tをとるのはlet類と条件分岐のみである。 つまり、KNormal.tによる表現はletをノードとするリストとなる。

「速攻MinCamlコンパイラ概説」にある例では、a+b+c-dは次のようになる。

let tmp1=a+b in
let tmp2=tmp1+c in
tmp2-d

※正確には、MinCamlのK正規化の実装では a+b+c-d

let tmp2 =
  let tmp1 = a+b in
  tmp1+c in
tmp2-d

に変換される。これは次のように図示できる。青い破線と数字は実行順を示す。

List of let by K-Normalization

データ構造としては完全な一次元ではないが、これは入れ子になったリストと見ることが出来る。計算とその順序の点では先の表現と等価である。 簡単な変形を施すと先の表現のような入れ子のないリストに出来、後のネストしたletの簡約フェーズではそれを行う。

K正規化の実装

kNormal.mlで定義される関数はfv, insert_let, g, f。このうちfvは当面使われない。fgを呼ぶだけのもので、K正規化の本体はKNormal.gである。

KNormal.gは型環境と式(Syntax.t)を取り、K正規化した式(KNormal.t)と型を返す。 最も基本的な単項演算の場合はこのようになる。

  | Syntax.Neg(e) ->
      insert_let (g env e)
	(fun x -> Neg(x), Type.Int)

insert_letはオペランドの式で変数を定義するLetノードを作り、演算ノードをそれに繋げる。ただし演算ノードはオペランドの変数名が不明では作れないので、insert_letに渡すのは演算ノードではなくそれを作るクロージャである。

insert_letでは受け取った式を調べ、単なる変数の場合はその変数をそのまま演算に渡し、letを作らない。この節約をしないと項の数だけ無駄にletが増える。

二項演算子はオペランドが2つあるのでinsert_letを重ねる。Letノードが2つ続き、その次にAddノードが来る形になる。

  | Syntax.Add(e1, e2) ->
      insert_let (g env e1)
	(fun x -> insert_let (g env e2)
	    (fun y -> Add(x, y), Type.Int))

この変換の結果は次のようになる。

Let [x] ---- Let [y] ---- Add(x,y)
|            |
(g env e1)   (g env e2)

その他、関数適用等の場合もこれと同様に出てくる式の数だけletを並べ最後にApp等のノードが来る形になる。

「ついで」の変換

「概説」にある通り、ブール値は整数の1と0に置換される。

KNormal.tでは比較・論理演算とif文を条件分岐 IfEqIfLE による表現に置き換える。

直接KNormal.IfEqKNormal.IfLE に変換できるのは、Syntax.If(Syntax.Eq(e1,e2), e3, e4)のようにif文の中に比較がある場合である

それ以外のif文の扱いが面白い。Syntax.tによる別の表現に言い換えた上で、もう一度KNormal.gにかけるのである。つまりLispでいうマクロのようにして実現している。

例えば、条件式が比較ではないif文Syntax.If(e1,e2,e3)は、Syntax.If(Syntax.Eq(e1, Syntax.Bool(false)), e3, e2)に言い換える。 また、単独で出現する比較は、その比較を行ってtrueまたはfalseを返すif文に態々変換されるという具合である。

OCamlメモ

fst: 'a * 'b -> 'a
二つの要素の組をとり、最初の要素を返す。早い話がLispのcar。 案の如くcdrに相当する二つ目の要素を返すものもあり、そちらはsndという。

この記事へのトラックバック
この記事へのコメント
コメントを書く
お名前: [必須入力]

メールアドレス:

ホームページアドレス:

コメント: [必須入力]

認証コード: [必須入力]


※画像の中の文字を半角で入力してください。

広告


この広告は60日以上更新がないブログに表示がされております。

以下のいずれかの方法で非表示にすることが可能です。

・記事の投稿、編集をおこなう
・マイブログの【設定】 > 【広告設定】 より、「60日間更新が無い場合」 の 「広告を表示しない」にチェックを入れて保存する。


×

この広告は1年以上新しい記事の投稿がないブログに表示されております。