ついに最終章！
この最終章では、Haskellプログラミングを論証する方法を紹介する。まず等式推論の復習から始め、それがHaskellにどのように適用できるかを考える。そして、数学的帰納法という重要な技法を説明し、連結演算子を数学的帰納法に似た手法で除去できることを示す。最後に本章の締めくくりとして、簡単なコンパイラーの正しさを証明する。
13.1 等式推論
数学の復習。交換法則、結合法則、分配法則を使い、和の積を積の和に展開しても代数的に等しい。 公理から定理が導けるかを推論するのが等式推論。
13.2 Haskellでの論証
Haskellの等式推論。Haskellを論証するために数学を使う。関数定義を使い、左辺から右辺へ適用したり、右辺から左辺へ逆適用したりする。 ただし、Haskellの関数定義でパターンマッチを使っている場合、定義の順番に依存している。プログラムの論証を簡単にするには、順番に依存しないパターン（互いに素な、または重複なしのパターン）である必要がある。
これは順番に依存する。
isZero :: Int -> Bool isZero 0 = True isZero n = False
ガードを使い、互いに素なパターンにしておく。
isZero :: Int -> Bool isZero 0 = True isZero n | n /= 0 = False
13.3 簡単な例題
reverse 関数の定義。
reverse :: [a] -> [a] reverse [] = [] reverse (x:xs) = reverse xs ++ [x]
この定義と、リスト表記の定義と、結合演算子 ++ の定義を元に、任意の要素xに対し reverse [x] = [x]が成り立つことを証明する。
reverse [x] = reverse (x:[]) -- リスト表記の定義 = reverse [] ++ [x] -- reverseの定義 = [] ++ [x] -- reverseの定義 = [x] -- ++の定義
これを使うことで、プログラム中の式 reverse [x] を [x] と置き換えてもよいことがわかる。
続いて、パターンマッチを使ったプログラムの論証を場合分けで。
否定演算子の定義を使って、任意の真理値 b について二重否定を除去できることを証明したい。そこで、値が True の場合と False の場合の両方に分ける。
b = False の場合は以下のとおり。
not (not False) = not True = False
13.4 整数に対する数学的帰納法
再帰を使ったプログラムの論証を数学的帰納法で。（ただし、無限に再帰する値は扱わない）
data Nat = Zero | Succ Nat add :: Nat -> Nat -> Nat add Zero m = m add (Succ n) m = Succ (add n m)
という関数 add について、 add n Zero = nを証明する。
n = Zero の場合
add Zero Zero = Zero
n = x のときに add x Zero = x が成り立つと仮定して、 n = Succ x の場合
add (Succ x) Zero = Succ (add x Zero) = Succ x
<
自然数の加算に対する結合法則 add x (add y z) = add (add x y) z を証明する。
x = Zero の場合
|| 左辺 = add Zero (add y z) = add y z
右辺 = add (add Zero y) z = add y z ||<
x = n のときに add n (add y z) = add (add n y) z が成り立つと仮定して、 x = Succ n の場合
|| 左辺 = add (Succ n) (add y z) = Succ (add n (add y z)) = Succ (add (add n y) z)
右辺 = add (add (Succ n) y) z = add (Succ (add n y)) z = Succ (add (add n y) z) ||<
指定された要素をn個持つリストを生成するライブラリ関数 replicate の定義
replicate :: Int -> a -> [a] replicate 0 _ = [] replicate (n+1) c = c : replicate n c
をもとに、replicateが生成するリストの長さがnであること length (replicate n c) = n を証明する。
n = 0 の場合
length (replicate 0 c) = length [] = 0
n = x のときに length (replicate n c) = n が成り立つと仮定して、 n = x + 1 の場合
length (replicate (x+1) c) = length (c : replicate n c) = 1 + length (replicate n c) = 1 + n = n + 1
