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

とりあえず残りの問題だけ

13.9 練習問題

7. 以下の定義が与えられているとする。
   

   map f []     = []
   map f (x:xs) = f x : map f xs
   (f.g) x      = f (g x)
   

   map f (map g xs) = map (f.g) xsであることを、xsに対する数学的帰納法で証明せよ。
8. 以下の定義が与えられているとする。
   

   take 0 _          = []
   take (n+1) []     = []
   take (n+1) (x:xs) = x : take n xs
   
   drop 0 xs         = xs
   drop (n+1) []     = []
   drop (n+1) (_:xs) = drop n xs
   

   この定義と上記の++の定義を使って、take n xs ++ drop n xs = xsを証明せよ。 その際、0以上の整数nとリストxsに対して同時に数学的帰納法を用いよ。
   ヒント：関数 take と drop の定義は、それぞれ三つの場合分けがあることに注意。
9. 以下の型が与えられているとする。
   

   data Tree = Leaf Int | Node Tree Tree
   

   この木の葉の個数は、節の個数よりも、常に1多いことを数学的帰納法で示せ。
   ヒント：木の葉と節の個数を数える関数を定義するところから始めよ。
10. 等式 comp' e c = comp e ++ c が与えられたとき、数学的帰納法に似た手法をeに対して用いることで、関数 comp'の再帰的な定義を求めよ。