Isabelle Tutorial その8
3.3 Case Study: Compiling Expressions
今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項演算子も詳細は定めず、適当な演算子を持っているとします。
types 'v binop = "'v => 'v => 'v"
datatype ('a, 'v) expr = Cex 'v
| Vex 'a
| Bex "'v binop" "('a, 'v) expr" "('a, 'v) expr"
三つの構成子は定数、変数、二項演算子の適用を表わします。式をある環境の下で評価する関数は次のように定義できます。
primrec "value" :: "('a, 'v) expr => ('a => 'v) => 'v" where "value (Cex v) env = v" | "value (Vex a) env = env a" | "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
スタックマシーンは、定数をスタックに積む、アドレスが指す値をスタックに積む、スタックの上位二つの値を演算子に適用し結果をスタックに積む、という三つの命令があります。exprと同じように、アドレスと値の型は型パラメータとします。
datatype ('a, 'v) instr = Const 'v
| Load 'a
| Apply "'v binop"
スタックマシーンの実行は関数execでモデル化します。これは命令のリスト、記憶領域(式の評価の時の環境と同じように、アドレスから値への関数でモデル化します)、そして実行前のスタックを引数に取り、実行後のスタックを返します。
primrec exec :: "('a, 'v) instr list => ('a => 'v) => 'v list => 'v list" where
"exec [] s vs = vs" |
"exec (i#is) s vs =
(case i of Const v => exec is s (v#vs)
| Load a => exec is s ((s a)#vs)
| Apply f => exec is s ((f (hd vs) (hd (tl vs)))#(tl (tl vs))))"
関数は全て全域的なので、空リストに対するhdも定義されており、結果は不定です。よってexecも実行が終了することは保証されていますが、例えば空のスタックに対してApplyが実行されたときなど、結果が不定となる場合があります。
コンパイラは式から命令列への関数です。次のように定義できます。
primrec compile :: "('a, 'v) expr => ('a, 'v) instr list" where
"compile (Cex v) = [Const v]" |
"compile (Vex a) = [Load a]" |
"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
このコンパイラの正当性を証明します。これは、式の評価結果と、コンパイル後の命令列の実行結果が同じになることで確かめます。
theorem "exec (compile e) s [] = [value e s]"
ヒューリスティクスに従って一般化します。
theorem "ALL vs. exec (compile e) s vs = (value e s) # vs"
eに対する帰納法で証明しようとすると、二つの命令列の結合に関する補題が必要になることがわかります。
lemma exec_app[simp]: "ALL vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
これを証明しようとすると、命令に対する二つのcase式が残ります。よってcase式に対する場合分けルールを追加して証明します。
apply(induct_tac xs, simp, simp split: instr.split)
または次のメソッドでも証明できます。
apply(induct_tac xs, simp_all split: instr.split)
