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

最終章「プログラムの論証」続きです。まだ難しくはないです。

• 整数に対する数学的帰納法
  • 再帰と帰納法は類似。再帰による関数の論証には数学的帰納法を利用する
  • 有限の範囲だけを考える
  • まだ「あたりまえ」の範疇
• リストに対する数学的帰納法
  • [] (空リスト)を出発点にして cons 演算子で要素を追加していくことで全てのリストは構築できる
  • 「全てのリストについて○○」を証明するために数学的帰納法が使える
  • ステップが増えてきたので写経

reverse (reverse xs) = xs を証明する

xs = [] の時
reverse (reverse [])
=> reverse []
=> []

xs=ns の時 reverse (reverse ns) = ns が成り立つと仮定して。
reverse (reverse (n:ns))
=> reverse (reverse ns ++ [n])
=> reverse [n] ++ reverse (reverse ns) -- 分配則
=> [n] ++ reverse (reverse ns)    -- 前回証明した reverse [x] = [x]
=> [n] ++ ns
=> (n:ns)

故に任意のリスト xs について
reverse (reverse xs) = xs

reverse の分配則は別に証明します。

reverse (xs ++ ys) = reverse ys ++ reverse xs を証明する

xs = [] の時
reverse ([] ++ ys)
=> reverse ys
また
reverse ys ++ reverse []
=> reverse ys ++ []
=> reverse ys

xs = ns の時に以下が成り立つと仮定して
reverse (ns ++ ys) = reverse ys ++ reverse ns

xs=(n:ns) の時
reverse ((n:ns) ++ ys)
=> reverse (n:(ns ++ ys))
=> reverse (ns ++ ys) ++ [n]  -- reverse を1回適用(簡約)する
=> (reverse ys ++ reverse ns) ++ [n]
=> reverse ys ++ (reverse ns ++ [n])
=> reverse ys ++ (reverse (n:ns)) -- reverse を逆向きに適用

最後の関数の逆向きの適用は本書とはちょっと違うやりかたですが、「関数とその定義は相互に置き換え可能」と 13.2 に書いてあったのでやりかたとして間違ってはいないはずです。
まだ「あたりまえ」の範疇ですが、この調子でもっと自明でない複雑な命題も証明できそうだなという感覚は見えてきたところで今日はここまで。