プログラミング Haskell 第13章 プログラムの論証 練習問題 その3

最終章「プログラムの論証」の練習問題です。

• 6. 13.5 の reverse (reverse xs) = xs の証明とここで提示された証明で 13.5 の証明のほうが良い理由を示せ、という難しい問題ですが、おそらくここで提示されている補助定理は 13.5 で利用されている補助定理から導ける粒度の大きい定理なので、小さい汎用性のある部品を使って証明するほうが良い、ということでしょうか。

• 7.

以下の定義が与えられているものとする
map f [] = []                    - (a1)
map f (x:xs) = f x : map f xs    - (a2)
(f . g) x = f (g x)              - (b)

map f (map g xs) = map (f . g) xs を示す

xs = [] の時
(左辺)
=> map f (map g [])
=> map f []         -- (a1) より
=> []               -- (a1) より

(右辺)
=> map (f . g) []
=> []               -- (a1) より

x = n:ns として
map f (map g ns) = map (f . g) ns が成り立つと仮定する

(左辺)
=> map f (map g (n:ns))
=> map f (g n : map g ns)         -- (a2) より
=> f (g n) : map f (map g ns)     -- (a2) より
=> f (g n) : map (f . g) ns       -- 仮定より
=> (f . g) n : map (f . g) ns     -- (b) より
=> map (f . g) (n:ns)             -- (a2) を逆向きに適用
= (右辺)

• 8.

以下の定義が与えられているものとする
take 0 _ = []                       - (a1)
take (n+1) [] = []                  - (a2)
take (n+1) (x:xs) = x : take n xs   - (a3)

drop 0 xs = xs                      - (b1)
drop (n+1) [] = []                  - (b2)
drop (n+1) (_:xs) = drop n xs       - (b3)

take n xs ++ drop n xs = xs を示す

n = 0 のとき

(左辺)
=> take 0 xs ++ drop 0 xs
=> [] ++ drop 0 xs              -- (a1) より
=> [] ++ xs                     -- (b1) より
=> xs                           -- ++ の定義より
= (右辺)

また xs = [] のとき
(左辺)
=> take n [] ++ drop n []
=> [] ++ drop n []              -- (a2) より
=> [] ++ []                     -- (b2) より
=> []                           -- ++ の定義より
= (右辺)

n = m + 1, xs = (y:ys) として
take m ys ++ drop m ys = ys が成り立つと仮定する

(左辺)
=> take (m+1) (y:ys) ++ drop (m+1) (y:ys)
=> (y : take m ys) ++ drop (m+1) (y:ys)    -- (a3)
=> (y : take m ys) ++ drop m ys            -- (b3)
=> y : (take m ys ++ drop m ys)            -- ++ の結合則より
=> y : ys                                  -- 仮定より
= (右辺)