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

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に対する数学的帰納法で証明せよ。

xs = []の場合

  左辺
= map f (map g [])
= map f []
= []

右辺
= map (f.g) []
= []

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

  左辺
= map f (map g (n:ns))
= map f (g n : map g ns)
= f (g n) : map f (map g ns)
= (f.g) n : map (f.g) ns

右辺
= map (f.g) (n:ns)
= (f.g) n : map (f.g) ns

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 の定義は、それぞれ三つの場合分けがあることに注意。

n = 0の場合

  左辺
= take 0 xs ++ drop 0 xs
= [] ++ xs
= xs
= 右辺

n > 0, xs = []の場合

  左辺
= take n [] ++ drop n []
= [] ++ []
= []
= 右辺

n = m, xs = ysで式が成り立つと仮定して、n = m+1, xs = y:ysの場合

  左辺
= take (m+1) (y:ys) ++ drop (m+1) (y:ys)
= (y: take m ys) ++ (drop m ys)
= y : (take m ys ++ drop m ys)
= y:ys
= 右辺

9. 以下の型が与えられているとする。
   

   data Tree = Leaf Int | Node Tree Tree
   

   この木の葉の個数は、節の個数よりも、常に1多いことを数学的帰納法で示せ。
   ヒント：木の葉と節の個数を数える関数を定義するところから始めよ。

ヒント通り、木の葉と節の個数を数える関数を定義する。

countLeaf :: Tree -> Int
countLeaf Leaf _   = 1
countLeaf Node l r = countLeaf l + countLeaf r

countNode :: Tree -> Int
countNode Leaf _ = 0
countNode Node l r = 1 + countNode l + countNode r

その上で、countLeaf t = countNode t + 1が常に成り立つことをを証明する。

t = Leaf nの場合

  左辺
= countLeaf Leaf n
= 1

右辺
= countNode Leaf n + 1
= 0 + 1
= 1

t = l および t = r で式が成り立つと仮定して t = Node l r の場合

  左辺
= countLeaf Node l r
= countLeaf l + countLeaf r
= (countNode l + 1) + (countNode r + 1)
= 2 + countNode l + countNode r

右辺
= countNode Node l r + 1
= 1 + countNode l + countNode r + 1
= 2 + countNode l + countNode r

10. 等式 comp' e c = comp e ++ c が与えられたとき、数学的帰納法に似た手法をeに対して用いることで、関数 comp'の再帰的な定義を求めよ。

compの定義を再掲しておく。

comp           :: Expr -> Code
comp (Val n)   =  [Push n]
comp (Add x y) =  comp x ++ comp y ++ [ADD]

e = Val nの場合

  comp' (Val n) c
= [Push n] ++ c
= Push n : c

e = x および e = y で comp' e c = comp e ++ c が成り立つと仮定して e = Add x y の場合

  comp' (Add x y) c
= comp x ++ comp y ++ [ADD] ++ c
= comp' x (comp y ++ [ADD] ++ c)
= comp' x (comp' y (ADD : c))

まとめると

comp'             :: Expr -> Code -> Code
comp' (Val n) c   =  Push n : c
comp' (Add x y) c =  comp' x (comp' y (ADD : c))

ついに終わった……