プログラミング Haskell 第13章 プログラムの論証 その4

最終章「プログラムの論証」の後半です。「コンパイラーの正しさ」として少し長い例題が提示されているので写経しました。

• 加算を扱う式(Expr)をスタックマシンのコード(Code)に変換する関数 comp の正しさを検証
  • exec (comp e) [] = [eval e] を証明すればよい
  • 証明するために空リスト [] は任意のリスト s に拡張しておく
  • exec (comp e) s = (eval e):s
  • 証明のためにより一般化した式にしたほうがよいというのがおもしろい
• 連結演算子の除去(comp' の定義)
  • ついでに証明する時に暗に条件とする必要があったスタックアンダーフローが起きないことが自明になる
  • 効率的な関数定義は証明も簡潔？

手順は昨日までの reverse などの例と同じですがぐっと複雑さが増しています。数学的帰納法は実用的な関数実装のためのテクニックと言えると思います。

さてこれで 13章も練習問題を残すだけですが、付録のうち付録C「訳者による関数の解説」は本文中にでてきた例題の解説で参考になりそうなのでこれも読みます。そろそろ長かった「プログラミング Haskell」も終わりが見えてきたので次の本を何にするのか考えておかないといけませんね。