A正規形まとめ - Scheme VM を書く

A正規形についてまとめました。日本語の資料があまりに少ないのでまとめたのですが、正直理解できているか不安です。間違いを含んでいる可能性がある点にご注意ください。
間違いのご指摘やツッコミ大歓迎です。


あと念のため書いておきますが題材は、Schemeですが、A正規形自体はLispSchemeに特化した話ではなく、もっと一般的な話です。

A正規形の論文

The Essence of Compiling with Continuations - Flanagan, Sabry, Duba, Felleisen (ResearchIndex)という論文で解説されています。
この論文を読んで自分なりに理解できたことをここに書いています。

理解の前提

Scheme の let 式が分かっていないと理解が難しいかもしれません。

A正規形は何の役にたちますか?

コンパイラのコード生成時の中間表現として使われています。
中間言語として使われる理由としては

  • 最適化の際にコード変換しやすい
    • 計算の途中経過をくくり出すので最適化のチャンスが増える
    • 変換元と変換後のコードが等しいことが分かりやすい
    • 単純である
    • 種々の最適化アルゴリズムを適用しやすい
  • コンパイラが最終的な出力とするアセンブラの構造に近い形である
    • 元のソースコードよりは近いという意味。そっくりなわけではない。

などが挙げられます。

Core Scheme

A正規形への変換のモデルとして Core Scheme という言語が使われます。

;; Abstract syntax for Core Scheme

     M  ::=   V                      Values
         |    (let (x M) M)
         |    (if0 M M M)
         |    (M M ... M)
         |    (O M ... M)            Primitive Operations

     V  ::=  c                       Constants
         |   x                       Variables
         | (lambda x1 ... xn . M)

Scheme を少し単純化したものです。この Core Scheme で書かれたソースコードをA正規形に変換します。

A正規化

A正規形に変換することをA正規化と言います。A正規化を一言で説明するならば「計算の途中経過に変数を割り当てる」変換のことらしいです。
この説明はとても分かりやすいのですが、実際に変換用のコードを書こうとする場合は、きちんとルールを理解する必要があります。
A正規化は変換なので入力と出力があり、入力はターゲットとなるソースコード(今回の場合は Core Scheme)出力はA正規形の式になります。


A正規形になると、自由奔放だった Core Schemeソースコードが制限されたシンプルな形に変身します。
例えば let 式では (let (A B) C) の B の部分には「値」と「手続き呼び出し」と「演算子適用」しか許されなくなります。(let (x (if0 ...) ...)) や (let (x (let ...)) ...) いう形式は許されません。これらはA正規化されていない、もしくはA正規化の余地があるという状態です。

A正規化された Core Scheme で許される式の形は以下の通りです。

;; A-normalized Core Scheme

     M  ::=   V                             (return)
         |    (let (x V) M)                 (bind)
         |    (if0 V M M)                   (branch)
         |    (V V1 ... Vn)                 (tail call) 
         |    (let ((x (V V1 ... Vn))) M)   (call)
         |    (O V1 ... Vn)                 (prim-op)
         |    (let ((x (O V1 ... Vn))) M)   (prim-o	


このようにA正規化されると、許される式の形が限定されるので登場人物が減ることになります。そのため コード変換のときに考えなければいけないことが少なくなるというのも一つのメリットでしょうか。

さらに、(bind) (branch) などプリミティブな命令と見ることができる式だけになっているのも特徴的ですね。

A正規化のルール

A正規化のルールは以下のようになります。ルール自体は単純ですが、僕はこれを理解するのにとても時間がかかりました。(理解できたかも怪しい)
多分実例をまじえた方が理解が進むと思います。

A正規化の例

いくつか変換の例を挙げていきます。

(+ (+ 2 2) (let (x 1) (f x)))
(+ (+ 2 2) (let (x 1) (f x)))

を正規化してみましょう。

(+ (+ 2 2) (let (x 1) (f x)))

;;  (F V ... V E M ... M) に該当
;;  (A3)
;;  E = (+ [] (let (x 1) (f x)))
;;
;;  =>
;;

(let (t1 (+ 1 2)) (+ t1 (let (x 1) (f x))))

;;
;;  (A3)で E[t] と書いてあるから次は (+ t1 (let (x 1) (f x))) を正規化する
;;
;;  (F V ... V E M ... M) に該当
;;  (A1)
;;  E = (+ t1 [])
;;
;; =>
;;
(let (t1 (+ 1 2))
  (let (x 1)
    (+ t1 (f x))))

;;
;;  (A1)でE[N]と書いてあるから次は (+ t1 (f x))) を正規化する
;;
;;  (F V ... V E M ... M) に該当
;;  (A3)
;;  E = (+ t1 [])
;;
;;  =>
;;
;;  変換完了
;;  計算の途中経過に対して変数が割り当てられていますね
;;  途中経過に対する最適化のチャンスが生まれる
(let (t1 (+ 1 2))
  (let (x 1)
    (let (t2 (f x))
      (+ t1 t2))))
(let (x (let (y 0) y)) x)
(let (x (let (y 0) y)) x)

;;  (let (x E) M) に該当。
;;  (A1)
;;    E = (let (x []) x)
;;    [] に y の正規形(結局は y)が入る
;;
;;  =>
;;

(let (y 0)
  (let (x y)
    x))
(car (let (a '(1 2)) a))
(car (let (a '(1 2)) a))

;;  (F V ... V E M ... M) に該当
;;  (A1)
;;  E = (car [])
;;  [] に y の正規形が入る
;;
;;  =>
;;
(let (a '(1 2)) (car a))
(let1 (a 3) (+ (+ 1 2) 3))
(let1 (a 3) (+ (+ 1 2) 3))

;;  (let (x E) M) に該当
;;  (A1)
;;  E = []
;;
;;  =>
;;
(let1 (a 3) (+ (+ 1 2) 3))

;;  次に正規化するのは(+ (+ 1 2) 3)
;;
;;  (F V ... V E M ... M) に該当
;;  (A3)
;;  E = (+ [] 3)
;;
;;  =>
;;
(let (a 3)
  (let (t1 (+ 1 2))
    (+ t1 3)))
(lambda () (+ (1 2) 3))

論文のA正規化ルールでは lambda は Values として扱われている。しかし実際問題 lambda の中の正規化をしないと手続きの最適化ができない。
こういうルールいかがでしょう。

;;  Evaluation Contexts: を追加
(lambda (V ... V) E M ... M)

;; The A-reductions:
E[(lambda (V ... V) M)] -> (lambda (V ... V) E[N])

このルールで行くと

(lambda () (+ (1 2) 3))

;;  (A3)
;;  E = (lambda () [])
;;
;;  =>
;;
(lambda () (let (t1 (+ 1 2)) (+ t1 3)))

となります。

A正規化の後は?

コードをA正規形にしたあとは、Beta簡約、インライン展開、不要定義削除などの最適化を行います。
例えば上で変換例に挙げた式は以下のように定数 0 に最適化されます。

(let (x (let (y 0) y))
  x)

;;  =(A正規化)=>

(let (y 0)
  (let (x y)
    x))

;;  =(Beta簡約)=>

(let (y 0)
  (let (x 0)
    0))

;; =(不要定義削除)=>
0

Beta簡約や不要定義削除についてはまた今度。

関連用語

関連用語は以下の通り。A も normal も検索時にノイズが多すぎるのが難点です。
A-reductionとα(alpha)-reductionは違うものです。

A正規形に変換すること

A正規化、A-normalization、A-reduction

A正規形の別名

A-normal form、let normal form、Administrative normal form

コード

Figure 9にあるコードを Gaucheで動くようにしたものです。以前何回かコードを貼りましたが最新版です。
quote を value にするなどの改善をしてあります。

;;--------------------------------------------------------------------
;;
;; 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)))))]
    [('quote a)
     (k m)]
    [(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)
    (if (pair? v)
        (or (eq? (car v) 'quote) (eq? (car v) 'let1) (eq? (car v) 'if))
        #t))
  (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*))))))))