条件分岐のある言語のA正規化
前回に続いてA正規化の話。前回のミニマルな言語にブール型とifによる条件分岐を加える。実は条件分岐の正しいA正規化に関しては曖昧性があるようなので、後半はその話。
言語拡張
ASTに以下を追加：
type t = ... | Bool of bool ... | Lt of t * t ... | If of t * t * t
Ltは「未満」。(if (< x 5) 5 x))のような形で使う。
α変換は簡単：
let rec g env e = match e with ... | A.Bool _ -> e ... | A.Lt(e1,e2) -> A.Lt(g env e1, g env e2) ... | A.If(e1,e2,e3) -> A.If(g env e1, g env e2, g env e3)
今回導入したASTノードはどれも新しい変数を導入するものではないので、子ノードに対して再帰的にα変換を適用していくだけ。
A正規化
A正規化するのも（実装は）簡単である。
まず比較演算子やブール値に関しては：
let rec normalize m k = match m with ... | A.Lt(e1,e2) -> normalize_name e1 (fun x -> normalize_name e2 (fun y -> k (A.Lt(x,y)))) | _ -> k m
AddやIntとほぼ同じ処理をすることになる。
新しいのはIfに対する処理で：
let rec normalize m k = match m with ... | A.If(e1,e2,e3) -> normalize_name e1 (fun x -> k (A.If(x, normalize e2 id, normalize e3 id))) ... 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)))
ifの条件式だけはネストした式になっている場合、新しいletでif式の前に条件を計算する形に直す。ifの結果式２つに関してはそれぞれA正規化はするが、if式の外に処理を出したりすることはしない。
これで以下のようなソースと正規化のコードになる：
(if (let [x 5] (< x 10))
(+ 1 (+ 2 3))
(let [y 4] (+ (+ y y) y)))
(let [x.1 5]
(let [g0 (< x.1 10)]
(if g0
(let [g2 (+ 2 3)] (+ 1 g2))
(let [y.0 4]
(let [g1 (+ y.0 y.0)] (+ g1 y.0))))))
A正規化の定義に関する疑義
ただし、このやり方で本当に「正しいA正規化」ができているのか、というと疑義が出る。
問題となるのは：
(let [x (if (< 3 4) 5 6)] (+ x x))
のようなletの束縛される方の式がifであるケース。
今回の実装だと：
(let [g0 (< 3 4)]
(let [x.0 (if g0 5 6)]
(+ x.0 x.0)))
のようにifがletで束縛されたままの形で正規化される。
上記の（MinCamlの作者でもある）住井先生のブログ記事を読んでいたら：
厳密なA正規形（とCPS）だと、let x = (if y then 式1 else 式2) in ...も許されないので
というフレーズを見つけて気になった。
The following grammar describes a minimal A-Normal form, adapted from Flanagan et al.'s The Essence of Compiling with Continuations:
<aexp> ::= NUMBER | STRING | VAR | BOOLEAN | PRIMOP
| (lambda (VAR ...) <exp>)
<cexp> ::= (<aexp> <aexp> ...)
| (if <aexp> <exp> <exp>)
<exp> ::= (let ([VAR <cexp>]) <exp>)
| <cexp>
| <aexp>
と書いており、明確にletで束縛する式はifを含んでもいいようになっている。
住井先生の記事でも
厳密なA正規形では、let式の=の右辺にif式が出てくるのも駄目なはずですが、これはわりと曖昧な場合が多い気がします。A正規形の元論文からして、Figure 7の簡約規則とFigure 9のコードが食い違っているような…
と書いてある通り、The Essence of Compiling with Continuationsを読むとページ７では
M ::= V (let (x V) M) (if0 V M M) (V V_1 .. V_n) (let (x (V V_1 .. V_n)) M) (O V_1 .. V_n) (let (x (O V_1 .. V_n)) M) V ::= c | x | (lambda x...x_n.M)
とあって、letで束縛される式はアトミックな値かアトミックな値に対する関数・演算子の適用だけ、となっているのにページ１１に載っている実際に正規化するためのアルゴリズムはMatt Mightの
(define (normalize-term M) (normalize M (λ (x) x)))
(define (normalize M k)
(match M
[`(λ ,params ,body)
(k `(λ ,params ,(normalize-term body)))]
[`(let ([,x ,M1]) ,M2)
(normalize M1 (λ (N1)
`(let ([,x ,N1])
,(normalize M2 k))))]
[`(if ,M1 ,M2 ,M3)
(normalize-name M1 (λ (t)
(k `(if ,t ,(normalize-term M2)
,(normalize-term M3)))))]
[`(,Fn . ,M*)
(normalize-name Fn (λ (t)
(normalize-name* M* (λ (t*)
(k `(,t . ,t*))))))]
[(? Value?) (k M)]))
(define (normalize-name M k)
(normalize M (λ (N)
(if (Value? N) (k N)
(let ([t (gensym)])
`(let ([,t ,N]) ,(k t)))))))
とほぼ同一のものになっている（SchemeとRacketの構文の差などに起因する小さな違いはある）。
そもそもページ７では関数内を正規化する話がまったく出てこないので、そのA正規化定義では不十分そうだ。
しかしA正規化でletの束縛される式にifが出てはいけない、という話はCompiling with Continuations, Continuedでも
Consider the term
let z = (λx.if x then a else b) c in M
This is in ANF, but β-reduction produces
let z = (if c then a else b) in M,
which is not in normal form because it contains a let-bound conditional expression.
という感じで出てくる。A正規化の定義というのは諸説あるようだ。
