A-normal form 再学習 その4 - Scheme VM
ここに書いてある内容は古いです。A正規形まとめをご参照ください。
A-reduction の定義は Evaluation Contexts の概念を参照する。Evaluation Contexts とは "hole" と称され[]で表現される項のことであり、特定の副項の場所に現れる。
hole の場所は、CEK semantics にしたがって次に evalute されるべき副次式(subexpression)を指し示す。
例えば (let (x M1) M2) という式の場合、Evaluation Contexts の定義に (let (x ε) M)があるので、次に簡約されるべき式は M1 でなければならない。
自信なしの訳。
変換例をなぞっていきましょう。
(+ (+ 2 2) (let (x 1) (f x)))
この式は Evaluation Contexts の (F V ... V ε M ... M) に該当し、εは (+ 2 2) になります。
(+ 2 2) が reduction されるときの Evaluation Contexts は (+ ... (let (x 1) (f x))) です。（ここがややこしい）
reduction されるべき (+ 2 2) は (F V1 ... Vn) に該当しますから、A-reductions の(A3)を適用します。
(let (t (+ 2 2)) (+ t (let (x 1) (f x))))
ここで t は「t は FV(ε) に含まれない」という条件があるので実装時は、他の変数名とはかぶらないものを使うことになります。
さてε[t] が次に reduction される候補です。
(+ t (let (x 1) (f x)))
の部分。t は変数ですから V (Values)として扱います。
この式は Evaluation Contexts の (F V ... V ε M ... M) に該当し、εは (let (x 1) (f x)) になります。
(let (x 1) (f x)) が reduction されるときの Evaluation Contexts は (+ t ...) です。
reduction されるべき (let ...) は (let (x M) N) に該当しますから(A1)を適用します。
(let (t (+ 2 2) (let (x 1) (+ t (f x)))))
となります。
次は (f x) です。A(3)を適用します。
(let (t2 (f x)) (let (t (+ 2 2) (let (x 1) (+ t t2)))))
できました。
実装
さてこれをコードに落とすことを考えます。Figure 9 に参考実装があるのですが Figure 7 と一致しない部分もあるともっぱらの噂なので慎重に。
基本的に Figure 9 のコード例が分かりやすい気がする。(normalize M k)の形式。
M が normalize するべき式、k が M が normalize された結果を受け取り、式に埋め込むための継続。（ここが本当に理解が難しい）
Figure 9 には
変換後コードサイズが指数関数的に大きくなってしまうことを防ぐために、条件分岐を取り囲む式の評価を2回してしまわないように工夫している。
と書かれていますが。
(a-normalize '(let (a (if 1 2 3)) (if (let (x 3) x) 4 5))) => (if 1 (let (a 2) (let (x 3) (if x 4 5))) (let (a 3) (let (x 3) (if x 4 5))))
のように分岐後のコードが重複するのを防ぐみたいです。
それと if の predicate 部の normalize が Figure 9 では間違っているような気がします。
[('if m1 m2 m3) (a-normalize-with-k m1 (lambda (normalized-m1) => [('if m1 m2 m3) (a-normalize-name m1 (lambda (normalized-m1)
だと思います。
問題は lambda の扱い。Figure 7 の簡約規則では lambda は Values と定義されていますから、変換の対象ではないとするのが正しそうです。
ところが Figure 9 のコードでは lambda の body を normalize しています。
確かに最適化のための中間コードとして採用するならば、lambda の body を normalize をしないと normalize の意味がないような気がします。
この件は id:sumii さんも
A正規形の元論文からして、Figure 7の簡約規則とFigure 9のコードが食い違っているような…（if文以外にも、λの中を正規化するかどうかも食い違っている気がする）
と指摘されています。（やっと理解が追いつきました）
ところで lambda の normalize はなぜ、lambda の外にしみださないようになっているのでしょうか。今のところ分かりません。
コード
Figure 9 ほぼそのままですが、Gauche で動くコードです。
(load "./lib/test.scm") ;;-------------------------------------------------------------------- ;; ;; A-normalization for Core Scheme. ;; ;; Based on A linear time A-normalization alogrithm, ;; in The Essence of Compiling with Continuations. ;; ;; (define (a-normalize m) (a-normalize-with-k m (lambda (x) x))) (define (a-normalize-with-k m k) (define (primitive-op? f) (eq? f '+)) (match m ;; normalization of lambda is not in Figure 7, but Figure 9. [('lambda params body) (k `(lambda ,params ,(a-normalize body)))] [('let (x m1) m2) (a-normalize-with-k m1 (lambda (normalized-m1) `(let (,x ,normalized-m1) ,(a-normalize-with-k m2 k))))] ;; [('if m1 m2 m3) ;; (a-normalize-with-k m1 (lambda (normalized-m1) ;; `(if ,normalized-m1 ;; ,(a-normalize-with-k m2 k) ;; ,(a-normalize-with-k m3 k))))] ;; To prevent possible exponential growth in code size, ;; the algorithm avoids duplicating the evaluation context enclosing a conditional expression. [('if m1 m2 m3) (a-normalize-name m1 (lambda (normalized-m1) (k `(if ,normalized-m1 ,(a-normalize m2) ,(a-normalize m3)))))] [(fn . m*) (if (primitive-op? fn) (a-normalize-name* m* (lambda (t*) (k `(,fn . ,t*))))) (a-normalize-name fn (lambda (t) (a-normalize-name* m* (lambda (t*) (k `(,t . ,t*))))))] [else (k m)])) (define (a-normalize-name m k) ;; ;; Values ;; constants or variables. (define (value? v) (not (pair? v))) (a-normalize-with-k m (lambda (n) (if (value? n) (k n) (let1 t (gensym) `(let (,t, n) ,(k t))))))) (define (a-normalize-name* m* k) (if (null? m*) (k '()) (a-normalize-name (car m*) (lambda (t) (a-normalize-name* (cdr m*) (lambda (t*) (k `(,t . ,t*)))))))) ;;-------------------------------------------------------------------- ;; ;; Tests ;; (a-normalize '(if (let (x 3) x) 4 5)) (eqt '(let (x 3) (if x 4 5)) (a-normalize '(if (let (x 3) x) 4 5))) (with-gensym (a-normalize '(+ (+ 2 2) (let (x 1) (f x))))) (eqt '(let (G7 (+ 2 2)) (let (x 1) (let (G8 (f x)) (+ G7 G8)))) ) (with-gensym (a-normalize '(+ (let (a 0) (+ a 3)) 2))) (eqt '(let (a 0) (let (G4 (+ a 3)) (+ G4 2))) (with-gensym (a-normalize '(+ (let (a 0) (+ a 3)) 2)))) (with-gensym (a-normalize '(let (a (let (b 3) (+ b 2))) (+ a 2)))) (eqt '(let (b 3) (let (a (+ b 2)) (+ a 2))) (with-gensym (a-normalize '(let (a (let (b 3) (+ b 2))) (+ a 2))))) (with-gensym (a-normalize '(lambda () (+ (+ 1 2) 3)))) (eqt '(lambda () (let (G4 (+ 1 2)) (+ G4 3))) (with-gensym (a-normalize '(lambda () (+ (+ 1 2) 3))))) (with-gensym (a-normalize '(if (+ 1 2) 3 3))) (eqt '(let (G2 (+ 1 2)) (if G2 3 3)) (with-gensym (a-normalize '(if (+ 1 2) 3 3)))) (test-end)
