関数のある言語の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))
多引数の関数
関数が複数の引数を取れるように拡張していく。(ちなみに再帰はできないのでまだチューリング完全ではない)
(追記:と思ったがまだ型検査を実装していないので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.map
やList.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_name
、normalize_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は(関数内のもの以外)全部外に出されているのがわかる。関数式の中は正規化されているが関数の外には出されない。