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

13.9 練習問題

  1. 付録Aにある標準ライブラリの中から重複のあるパターンを使って定義されている関数を探せ。

いま手元に教科書がなくて、付録Aを確認できないので、今日はパス。

  1. 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))
  1. 練習問題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)
  1. リストのすべての要素が、ある述語を満たすか調べるライブラリ関数 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
  1. 以下の定義が与えられているとする。
    [] ++ 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の右辺
  1. 等式 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で証明した ++の結合法則がないと証明できないし……面倒だよね。