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

最終章「プログラムの論証」の中盤です。今日読んだところはこの章でやってきたプログラムの証明の実用的な活用方法が示されていて、すっきりしました。

• 13.6 連結を除去する
  • 前回までの reverse の定義には "++" によるリストの連結が利用されているので効率が悪い(O(N^2))
  • reverse' xs ys = reverse xs ++ ys を満たす関数を定義したい
• 関数を定義するために、欲しい関数が満たすべき等式から帰納法で検証してみる

基底部
reverse' [] ys
=> reverse [] ++ ys
=> [] ++ ys
=> ys

再帰部
reverse' (x:xs) ys
=> reverse (x:xs) ++ ys
=> (reverse xs ++ [x]) ++ ys
=> reverse xs ++ ([x] ++ ys)
=> reverse xs ++ (x:ys)
=> reverse' xs (x:ys)   -- reverse' の仕様の逆向きの適用

• • ここから reverse' の定義が自然と求まる

reverse' :: [a] -> [a] -> [a]
reverse' [] ys = ys
reverse' (x:xs) ys = reverse' xs (x:ys)

• • reverse' を用いて reverse を定義しなおすことができる

reverse xs = reverse' xs []

• • reverse' を用いる定義は蓄積変数(2つめの引数)に結果のリストを構築していくので元の ++ を使う定義よりも効率的

このように「こういう関数が欲しい」という時にプログラムの証明を利用して定義を探すことができるのですね。これはすごいですね!