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

プログラミングHaskell

ついに最終章「プログラムの論証」に入ります。この章は長いです。内容も難しそうなので最初は少しずつ進めていきます。

• 等式推論 - 代数的性質(交換法則、結合法則など)の話
  • x*(y+z) と x*y + x*z は同等だけど演算回数は違う
  • ちょっとどこが論点なのか掴みかねますがここは Haskell とは直接関係ない話の導入らしい
• Haskell での論証
  • 関数とその定義は同等なので置き換え可能(簡約もできるし逆もできる)
  • 引数のパターンマッチの時は順番が影響することがあるので、順番に依存しないようにガードを使った書き方にして考える
• reverse の例

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

この定義から任意の x に対して reverse [x] = [x] なので reverse [x] と [x] はどこでも置き換え可能。

• not の例

not :: Bool -> Bool
not True -> False
not False -> True

• • 場合分けを用いて等式推論
  • not (not b) = b が b が True の時とFalse の時の場合分けをして示せる

なんだかあたりまえすぎてどこが重要なとろこかよくわかりませんが、基本が大事そうなにおいがしますので徐々に進みます。