第13章 プログラムの論証 #1

ついに最終章！

この最終章では、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