第13章 プログラムの論証 #3

13.7 コンパイラーの正しさ

忙しかったのでかなり間が空いてしまった。 今回は10.5節で出てきた関数を、10.5節とは違った形で（コンパイルして実行することで）評価する関数を定義して、その関数の振る舞いがもとの関数の振る舞いと一致することを証明する。

10.5節の関数の、仮想マシンを使わない定義はこれ（10.5節ではもともとの関数名は value だったが、eval に置き換えてある）。

data Expr = Val Int | Add Expr Expr
eval           :: Expr -> Int
eval (Val n)   =  n
eval (Add x y) =  eval x + eval y

10.5節では、「数式を処理する仮想マシンを定義することで、処理の順番を指示できる。」と述べたうえで、仮想マシンを使った eval 関数の定義に移っていった。この節でも同じような感じで数式を処理する仕組みを別途用意するのだけど、その方法が10.5節とは違っている。 10.5節では、加算レジスタ、評価レジスタ、そして命令のスタックを持った仮想マシンだった。そして、与えられた式を逐次仮想マシン命令に置き換えて評価していく、いわばインタープリタ的な動作として eval 関数を再定義した。

この節の仮想マシンは、加算・評価用のレジスタがスタックに置き換わっている感じ。加算もスタックに対して行うし、式の評価結果はスタックに残る。そして、与えられた数式はいったん命令スタックに置き換えて（コンパイルして）、それから仮想マシンを実行することで数式の値が評価される。

type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | Add

exec                       :: Code -> Stack -> Stack
exec [] s                  =  s
exec (PUSH n : c) s        =  exec c (n : s)
exec (ADD : c) (m : n : s) =  exec c (n + m : s)

comp           :: Expr -> Code
comp (Val n)   =  [Push n]
comp (Add x y) =  comp x ++ comp y ++ [ADD]

こうやって定義したコンパイル関数 comp と実行関数 exec の振る舞いが、もとの eval 関数の振る舞いと一致することを論証していく。すなわち、証明したい等式は以下だ。

exec (comp e) [] = [eval e]

ただし、上の形では証明が難しいので、スタックの状態を一般化した形で証明する。

exec (comp e) s = eval e : s

分配法則を使った証明

まずは、e = Val n の場合。

  左辺
= exec (comp (Val n)) s
= exec [PUSH n] s
= n : s

  右辺
= eval (Val n) : s
= n : s

次に、e = x および e = y のときに、以下が成り立つと仮定しておく。

exec (comp x) s = eval x : s
exec (comp y) s = eval y : s

上の仮定が成り立つときに、e = Add x y の場合は

  左辺
= exec (comp (Add x y)) s
= exec (comp x ++ comp y ++ [ADD]) s
= exec (comp x ++ (comp y ++ [ADD])) s
= exec (comp y ++ [ADD]) (exec (comp x) s) ★
= exec (comp y ++ [ADD]) (eval x : s)
= exec [ADD] (exec (comp y) (eval x : s)) ★
= exec [ADD] (eval y : eval x : s)
= exec [] ((eval x + eval y) : s)
= (eval x + eval y) : s

  右辺
= eval (Add x y) : s
= (eval x + eval y) : s

★はexecの分配法則を使って証明している。分配法則は、コードcとdを連結してから実行するのと、コードcの実行結果を使ってコードdを実行するのが同じ結果になることを表している。

exec (c ++ d) s = exec d (exec c s)

さて、分配法則を数学的帰納法で証明しよう。まずは、c = [] の場合。

  左辺
= exec ([] ++ d) s
= exec d s

  右辺
= exec d (exec [] s)
= exec d s

そして、c = x のときに、exec (x ++ d) s = exec d (exec x s) が成り立つと仮定しておき、さらに場合分けをする。

c = PUSH n : x の場合

  左辺
= exec ((PUSH n : x) ++ d) s
= exec (PUSH n : (x ++ d)) s
= exec (x ++ d) (n : s)
= exec d (exec x (n : s))

  右辺
= exec d (exec (PUSH n : x) s)
= exec d (exec x (n : s))

c = ADD : x の場合

この場合は、スタックsについて、s = m : n : s' であると考えてよい。これは、加算命令ADDが実行されるときには、スタックに少なくとも２つの数値が入っていることからきている（ADD命令を実行する exec の定義もそのようになっている）。

  左辺
= exec ((ADD : x) ++ d) s
= exec (ADD : (x ++ d)) (m : n : s')
= exec (x ++ d) (m + n : s')
= exec d (exec x (m + n : s'))

  右辺
= exec d (exec (ADD : x) s)
= exec d (exec (ADD : x) (m : n : s'))
= exec d (exec x (m + n : s'))

うへえ、長い……

分配法則の除去

13.6節で連結演算子を除去したのと同じような手法で、より簡潔に証明できる。

具体的には、以下の等式を満たす関数 comp' の定義を探す。

comp' e c = comp e ++ c

数学的帰納法に似た変形を使うと（教科書では省略してある。あとで練習問題に出そうだな）、comp'は以下のような定義になることがわかるらしい。

comp'             :: Expr -> Code -> Code
comp' (Val n) c   =  PUSH n : c
comp' (Add x y) c =  comp' x (comp' y (ADD : c))

で、この comp' の正しさは、以下の等式を証明することで論証される。

exec (comp' e c) s = exec c (eval e : s)

e = Val n の場合

  左辺
= exec (comp' (Val n) c) s
= exec (PUSH n : c) s
= exec c (n : s)

  右辺
= exec c (eval (Val n) : s)
= exec c (n : s)

e = x および e = y のときに、以下が成り立つと仮定しておく。

exec (comp' x c) s = exec c (eval x : s)
exec (comp' y c) s = exec c (eval y : s)

e = Add x y の場合

  左辺
= exec (comp' (Add x y) c) s
= exec (comp' x (comp' y (ADD : c))) s
= exec (comp' y (ADD : c)) (eval x : s)
= exec (ADD : c) (eval y : eval x : s)
= exec c ((eval x + eval y) : s)

  右辺
= exec c (eval (Add x y) : s)
= exec c ((eval x + eval y) : s)

おおー、短くなった！