練習問題 4.5.8

scanr
の効率の良いプログラムが正しいことを説明せよ.



    scanr f e []
=       { scanr の仕様 }
    (map (foldr f e) . tails) []
=       { . の定義 }
    map (foldr f e) (tails [])
=       { tails の定義 }
    map (foldr f e) [[]]
=       { map の定義 }
    foldr f e [] : map (foldr f e) []
=       { map の定義 }
    foldr f e [] : []
=       { foldr の定義 }
    e : []
=       { リストのリテラル表記 }
    [e]

    scanr f e (x:xs)
=       { scanr の定義 }
    (map (foldr f e) . tails) (x:xs)
=       { . の定義 }
    map (foldr f e) (tails (x:xs))
=       { tails の定義 }
    map (foldr f e) ((x:xs) : tails xs)
=       { map の定義 }
    foldr f e (x:xs) : map (foldr f e) (tails xs)
=       { foldr の定義 }
    f x (foldr f e xs) : map (foldr f e) (tails xs)
=       { 任意の g について head (map g (tails xs)) = g xs であるから }
    f x (head (map (foldr f e) (tails xs))) : map (foldr f e) (tails xs)
=       { scanr の定義 }
    f x (head (scanr f e xs)) : scanr f e xs
=       { ys = scanr f e xs とする }
    f x (head ys) : ys
        where  ys = scanr f e xs