練習問題 4.5.11

練習問題4.1.4で定義した

Liste a

型を考察しよう．この型上の畳み込み関数は以下のように定義できる．

folde    ::  (b -> a -> b) -> b -> Liste a -> b
folde f e Nil         = e
folde f e (Snoc xs x) = f (folde f e xs) x

folde

に割り当てられる型は

foldl

に割り当てられる型とほぼ同じである．違いは，

[a]

が

Liste a

になっているところだけである．実際，以下が成り立つ．

folde f e = foldl f e . convert

ここで，

convert :: Liste a -> [a]

である．関数

convert

を定義した上で，上の等式が成り立つことを帰納法で証明せよ．

convert              ::  Liste a -> [a]
convert Nil          =   []
convert (Snoc xs x)  =   convert xs ++ [x]

[] の場合：
    folde f e Nil
=       { folde の定義 }
    e
=       { foldl の定義 }
    foldl f e []
=       { convert の定義 }
    foldl f e (convert Nil)
=       { . の定義 }
    (foldl f e . convert) Nil

Snoc xs x の場合
    folde f e (Snoc xs x)
=       { folde の定義 }
    f (folde f e xs) x
=       { 帰納法の仮定 }
    f ((foldl f e . convert) xs) x
=       { . の定義 }
    f (foldl f e (convert xs)) x
=       { foldl の定義 }
    foldl f (f (foldl f e (convert xs)) x) []
=       { foldl の定義 }
    foldl f (foldl f e (convert xs)) (x:[])
=       { リストのリテラル表記 }
    foldl f (foldl f e (convert xs)) [x]
=       { (foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys) だから }
    foldl f e (convert xs ++ [x])
=       { convert の定義 }
    foldl f e (convert (Snoc xs x))
=       { . の定義 }
    (foldl f e . convert) (Snoc xs x)

主張：foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys の証明は練習問題4.6.4参照

IFPH — 練習問題 4.5.11

練習問題 4.5.11