Arantium Maestum

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

関数のある言語のA正規化

前回の言語に関数定義・適用を追加する。

単一引数の関数

まずは変更を簡単にするために「単一引数の関数」を実装する。

関数自体の式であるFnと関数適用のCallをASTに追加:

type t =
...
| Fn of string * t
| Call of t * t

α変換は関数式に関しては(仮引数によって変数が導入されているので)genidで新しい変数を割り当てる必要がある:

let rec g env e = match e with
...
| A.Fn(s,e) ->
  let s' = genid s in
  A.Fn(s', g ((s,s')::env) e)
| A.Call(e1,e2) -> A.Call(g env e1, g env e2)

A正規化については関数式の中身も正規化する:

let rec normalize m k = match m with
...
| A.Fn(v,e) ->
  k (A.Fn(v,normalize e id))
| A.Call(e1,e2) ->
  normalize_name e1 (fun x ->
    normalize_name e2 (fun y ->
      k (A.Call(x,y))))
| _ -> k m
and normalize_name m k =
  normalize m (fun n ->
    if is_value(n) then k n
    else let g = gensym () in A.Let(g,n,k (A.Var g)))

単一引数の関数適用に関してはA正規化のロジックはAddとまったく同じになる(Addは二項演算で引数ふたつを正規化、関数適用は関数部分と引数の両方を正規化)。

使ってみるとこんな感じ(上の式が入力、下の式がA正規化したもの):

((let [x 5]
   (fn [y] (+ x (+ x y))))
   1)

(let [x.0 5]
  ((fn [y.1]
     (let [g0 (+ x.0 y.1)]
       (+ x.0 g0)))
     1))

単一引数のコードのgist

多引数の関数

関数が複数の引数を取れるように拡張していく。(ちなみに再帰はできないのでまだチューリング完全ではない)

(追記:と思ったがまだ型検査を実装していないのでYコンビネータが書ける。うっかりチューリング完全だった・・・)

AST:

type t =
...
| Fn of string list * t (* string * t から修正 *)
| Call of t * t list (* t * t から修正 *)

関数式は仮引数、関数適用は実引数をリストに変更している。

α変換:

let rec g env e = match e with
...
| A.Fn(ss,e) ->
  let ss' = List.map genid ss in
  A.Fn(ss', g ((List.combine ss ss') @ env) e)
| A.Call(e,es) -> A.Call(g env e, List.map (g env) es)

仮引数、実引数がリストになっているのに合わせてList.mapList.combineを使っている。後者は他の言語でよくzipと呼ばれている、リスト2つをタプルのリストに変更する関数。

A正規化は関数式には変更なし、関数適用だけ複雑になっている:

let rec normalize m k = match m with
...
| A.Fn(vs,e) ->
  k (A.Fn(vs,normalize e id))
| A.Call(e,es) ->
  normalize_name e (fun x ->
    normalize_names es (fun ys ->
      k (A.Call(x,ys))))
...
and normalize_name m k =
  normalize m (fun n ->
    if is_value(n) then k n
    else let g = gensym () in A.Let(g,n,k (A.Var g)))
and normalize_names ms k = match ms with
| [] -> k []
| m::ms ->
  normalize_name m (fun n ->
    normalize_names ms (fun ns -> k (n::ns)))

新しく作った相互再帰的なnormalize_names関数で実引数の式すべてに対して、必要とあればletで変数を割り当てながら正規化した形に変更する。ここで複雑なのはList.mapで「正規化した式のリスト」を作るだけでは不十分な点。正規化の過程で追加したletは関数適用の式の外に来る必要がある。normalize_name関数の中でのkの使い方で実現できている。

normalize_namesは名前が微妙だった(Scheme版だとnormalize-name*になっている)、というのはそもそもnormalize_nameが「名前を正規化」ではなくて「名前をつけて正規化」なので・・・ normalize_with_namenormalize_list_with_nameの方がいいかも。

使ってみるとこんな感じ(上の式が入力、下の式がA正規化したもの):

((let [x 5] (fn [y z] (+ x (+ y z))))
   (+ 1 (+ 2 3))
   (let [x 1] (+ x 4)))

(let [x.1 5]
  (let [g1 (+ 2 3)]
    (let [g2 (+ 1 g1)]
      (let [x.0 1]
        (let [g3 (+ x.0 4)]
          ((fn [y.2 z.3] (let [g0 (+ y.2 z.3)] (+ x.1 g0)))
             g2 g3))))))

関数適用の中のネストやletは(関数内のもの以外)全部外に出されているのがわかる。関数式の中は正規化されているが関数の外には出されない。

今回のコード(多引数バージョン)

gist.github.com