Hatena::Grouphaskell

猫とC#について書く代わりにHaskellとF#について書くmatarilloの日記 このページをアンテナに追加 RSSフィード

2012-08-07

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

16:45 | 第13章 プログラムの論証 #6 - 猫とC#について書く代わりにHaskellとF#について書くmatarilloの日記 のブックマークコメント

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

13.9 練習問題

  1. 以下の定義が与えられているとする。
    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に対する数学的帰納法で証明せよ。
  2. 以下の定義が与えられているとする。
    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に対して同時に数学的帰納法を用いよ。
    ヒント:関数 takedrop の定義は、それぞれ三つの場合分けがあることに注意。
  3. 以下の型が与えられているとする。
    data Tree = Leaf Int | Node Tree Tree
    
    この木の葉の個数は、節の個数よりも、常に1多いことを数学的帰納法で示せ。
    ヒント:木の葉と節の個数を数える関数を定義するところから始めよ。
  4. 等式 comp' e c = comp e ++ c が与えられたとき、数学的帰納法に似た手法をeに対して用いることで、関数 comp'再帰的な定義を求めよ。