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

13.5 リストに対する数学的帰納法

リストも再帰的にオブジェクトが構築される型なので、数学的帰納法で論証できる。

reverse (reverse xs) = xsの証明。

xs = [] の場合

  reverse (reverse [])
= reverse []
= []

xs = ns のときに reverse (reverse xs) = xs が成り立つと仮定して、 xs = n:ns の場合

  reverse (reverse (n:ns))
= reverse (reverse ns ++ [n]) ★1
= reverse [n] ++ reverse (reverse ns)
= [n] ++ reverse (reverse ns)
= [n] ++ ns
= n:ns

★1については、reverse 関数が ++ 演算子に対して分配法則を持っているという性質を使用する。

reverse (xs ++ ys) = reverse ys ++ reverse xs

xs = [] の場合

  左辺
= reverse ([] ++ ys)
= reverse ys

  右辺
= reverse ys ++ reverse []
= reverse ys ++ []
= reverse ys

xs = ns のときに reverse (xs ++ ys) = reverse ys ++ reverse xs が成り立つと仮定して、 xs = n:ns の場合

  左辺
= reverse ((n:ns) ++ ys)
= reverse (n:(ns ++ ys))
= reverse (ns ++ ys) ++ [n]
= (reverse ys ++ reverse ns) ++ [n] ★2
= revserse ys ++ (reverse ns ++ [n])

  右辺
= reverse ys ++ reverse (n:ns)
= reverse ys ++ (reverse ns ++ [n])

★2については、++ が結合法則を満たすという性質を使用する。（練習問題で証明する）

13.6 連結を除去する

連結演算子 ++ の効率は一番目の引数の長さに比例するので、reverse の効率は O(n²)。そこで reverse の定義から ++ を除去する。具体的には、以下の等式を満たす関数 reverse' の定義を探す。

reverse' xs ys = reverse xs ++ ys

（上記は等式であって、定義ではないことに注意。）

このような reverse' を、 ++ を使わずに定義することができれば、 reverse の定義を

reverse xs = reverse' xs []

に変えることで、 ++ を除去できるはず。

reverse' の定義は、上記の等式を元に数学的帰納法に似た変形を使うことで得られる。

xs = [] の場合

  reverse' [] ys
= reverse [] ++ ys
= [] ++ ys
= ys

xs = ns のときに reverse' xs ys = reverse xs ++ ys が成り立つと仮定して、 xs = n:ns の場合

  reverse' (n:ns) ys
= reverse (n:ns) ++ ys
= (reverse ns ++ [n]) ++ ys
= reverse ns ++ ([n] ++ ys)
= reverse ns ++ (n:ys)
= reverse' ns (n:ys)

すなわち、reverse' の定義は

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

この関数を使った reverse の定義は、効率が O(n)になる。

蓄積変数を使うよう関数 reverse を変更するには、単に reverse = foldl (\xs x -> x:xs) [] と定義すればよい。しかし、同様の振る舞いが数学的帰納法に似た手法で導けることを知っておくのも有益である。

続いて、木構造を扱う関数について、同様の導出で ++ を除去する。

data Tree = Leaf Int | Node Tree Tree
flatten            :: Tree -> [Int]
flatten (Leaf n)   =  [n]
flatten (Node l r) =  flatten l ++ flatten r

さっきのよりもさらに天下り的だが、以下の等式を満たす関数 flatten' の定義を探す。

flatten' t ns = flatten t ++ ns

もしこの関数が、++ を使わない形で定義できるのであれば、

  flatten t
= flatten t ++ []
= flatten' t []

という定義を使って、++ を除去できるはず。

t = Leaf n の場合

  flatten' (Leaf n) ns
= flatten (Leaf n) ++ ns
= [n] ++ ns
= n:ns

t = r および t = l のときに flatten' t ns = flatten t ++ ns が成り立つと仮定して、 t = Node l r の場合

  flatten' (Node l r) ns
= flatten (Node l r) ++ ns
= flatten l ++ flatten r ++ ns
= flatten l ++ (flatten r ++ ns)
= flatten l ++ (flatten' r ns)
= flatten' l (flatten' r ns)

すなわち、flatten の定義は

flatten   :: Tree -> [Int]
flatten t =  flatten' t []

flatten'               :: Tree -> [Int]
flatten' (Leaf n) ns   =  n:ns
flatten' (Node l r) ns =  flatten' l (flatten' r ns)