13.9 練習問題
- 付録Aにある標準ライブラリの中から重複のあるパターンを使って定義されている関数を探せ。
いま手元に教科書がなくて、付録Aを確認できないので、今日はパス。
add n (Succ m) = Succ (add n m)であることをnに対する数学的帰納法で示せ。
n = Zeroの場合左辺 = add Zero (Succ m) = Succ m 右辺 = Succ (add Zero m) = Succ m
n = xのときにadd x (Succ m) = Succ (add x m)が成り立つと仮定して、n = Succ xの場合左辺 = add (Succ x) (Succ m) = Succ (add x (Succ m)) = Succ (Succ (add x m)) 右辺 = Succ (add (Succ x) m) = Succ (Succ (add x m))
- 練習問題2の性質と
add n Zero = nを使って、加算が交換法則add n m = add m nを満たすことを示せ。その際、nに対して数学的帰納法を用いよ。
n = Zeroの場合左辺 = add Zero m = m 右辺 = add m Zero = m
n = xのときにadd x m = add m xが成り立つと仮定して、n = Succ xの場合左辺 = add (Succ x) m = Succ (add x m) = Succ (add m x) 右辺 = add m (Succ x) = Succ (add m x)
- リストのすべての要素が、ある述語を満たすか調べるライブラリ関数
allの定義が以下のように与えられたとする。
all p [] = True all p (x:xs) = p x && all p xs関数replicateの正しさを証明したい。関数replicateが生成するリストのすべての要素が同じであることを示す式all (==x) (replicate n x)が満たされることを0以上の整数nに対する数学的帰納法を用いて証明せよ。
ヒント：この性質が常にTrueとなることを示せ。
n = 0の場合all (==x) (replicate 0 x) = all (==x) [] = True
n = mのときにall (==x) (replicate m x) = Trueが成り立つと仮定して、n = m + 1の場合all (==x) (replicate (m+1) x) = all (==x) (x : replicate m x) = (==x) x && all (==x) (replicate m x) = True && True = True
- 以下の定義が与えられているとする。
[] ++ ys = ys (x:xs) ++ ys = x:(xs ++ ys)以下の二つの性質をxsに対する数学的帰納法で証明せよ。
xs ++ [] = xs xs ++ (ys ++ zs) = (xs ++ ys) ++ zsヒント：関数addの証明と同じようにせよ。
xs = []の場合1の左辺 = [] ++ [] = [] = 1の右辺 2の左辺 = [] ++ (ys ++ zs) = ys ++ zs = ([] ++ ys) ++ zs = 2の右辺
xs = nsのときにns ++ [] = nsおよびns ++ (ys ++ zs) = (ns ++ ys) ++ zsが成り立つと仮定して、xs = n:nsの場合1の左辺 = (n:ns) ++ [] = n:(ns ++ []) = n:ns = 1の右辺 2の左辺 = (n:ns) ++ (ys ++ zs) = n:(ns ++ (ys ++ zs)) = n:((ns ++ ys) ++ zs) = (n:(ns ++ ys)) ++ zs = ((n:ns) ++ ys) ++ zs = 2の右辺
- 等式
reverse (reverse xs) = xsは、補助定理reverse (xs ++ [x]) = x:reverse xsのみを用いて証明できる。この補助定理自体は、xsに対する数学的帰納法で証明できる。13.5節で示した証明の方が優れているのはなぜか？
ちょっと何言ってるかわからないので、補助定理の証明にチャレンジ。
xs = []の場合左辺 = reverse ([] ++ [x]) = reverse [x] = [x] -- 13.3の性質 右辺 = x:reverse [] = x:[] = [x]
xs = nsのときにreverse (ns ++ [x]) = x:reverse nsが成り立つと仮定して、xs = n:nsの場合左辺 = reverse ((n:ns) ++ [x]) = reverse (n:(ns ++ [x])) -- xxの定義 = reverse (ns ++ [x]) ++ [n] -- reverseの定義 = (x:reverse ns) ++ [n] -- 仮定 = x:(reverse ns ++ [n]) -- xxの定義 右辺 = x:reverse (n:ns) = x:(reverse ns ++ [n]) -- reverseの定義
で、この補助定理を使うと
xs = []の場合左辺 = reverse (reverse []) = reverse [] = [] = 右辺
xs = nsのときにreverse (reverse ns) = nsが成り立つと仮定して、xs = ns ++ [n]の場合左辺 = reverse (reverse (ns ++ [n])) = reverse (n:reverse ns)) -- 補助定理 = reverse (reverse ns) ++ [n] -- reverseの定義 = ns ++ [n] -- 仮定 = 右辺
帰納法のところで、xs = n:ns じゃなく、xs = ns ++ [n] になってるあたりがイケてないってことかな？それぐらいしか理由は思いつかないけど。
追記
ちょっとネットでカンニングしたら、13.5節の分配法則は、この補助定理を一般化した形だから、そっちの方がいい、という回答が。
reverse (xs ++ ys) = reverse ys ++ reverse xs
において、ys = [x] としたのが今回の補助定理になる。確かにそうだ。
でも、13.5節の分配法則は、練習問題5で証明した ++の結合法則がないと証明できないし……面倒だよね。
