Thinking Functionally with Haskell勉強メモ: 第６章問題１

Exercise A

自然数が以下のとおりに定義されている：

mult :: Nat -> Nat -> Nat
mult Zero y = Zero
mult (Succ x) y = mult x y + y

mult (x+y) z = mult x z + mult y zを証明せよ：

case 0 左辺

mult (x+0) z

= {x+0 = x}
mult x z

case 0 右辺

mult x z + mult 0 z

= {mult Zero y = Zero}
mult x z + 0

= {x+0 = x}
mult x z

case y+1 左辺

mult (x+(y+1)) z

= {x+(y+1) = (x+y)+1}
mult ((x+y)+1) z

= {mult (Succ x) y = mult x y + y }
mult (x+y) z + z

case y+1 右辺

mult x z + mult (y+1) z

= {mult (Succ x) y = mult x y + y }
mult x z + (mult y z + z)

= {x + (y + z) = (x + y) + z}
(mult x z + mult y z) + z

= {induction}
mult (x+y) z + z

Exercise B

reverse (xs ++ ys) = reverse ys ++ reverse xs

の証明：

Case [] 左辺

reverse ([] ++ ys)

= { [] ++ xs = xs}
reverse ys

Case [] 右辺

reverse ys ++ reverse []

= { reverse [] = [] }
reverse ys ++ []

= {[] ++ xs = xs}
reverse ys

Case (x:xs) 左辺

reverse ((x:xs) ++ ys)

= {(x:xs) ++ ys = x:(xs++ys)}
reverse (x:(xs++ys))

= {reverse x:xs = reverse xs ++ [x] }
reverse (xs++ys) ++ [x]

Case (x:xs) 右辺

reverse ys ++ reverse (x:xs)

= { reverse (x:xs) = reverse xs ++ [x] }
reverse ys ++ (reverse xs ++ [x])

= {xs ++ (ys ++ zs) = (xs ++ ys) ++ zs }
(reverse ys ++ reverse xs) ++ [x]

= {induction}
reverse (xs++ys) ++ [x]

Exercise C

head . map f = f . head

の証明。

Case undefined 左辺

head (map f undefined)
= head undefined
= undefined

Case undefined 右辺

f (head undefined)
= f undefined

Case [] 左辺

head (map f [])
= head []
= undefined

Case [] 右辺

f (head [])
= f undefined

Case (x:xs) 左辺

head (map f (x:xs))
= head ((f x) : map f xs)
= f x

Case (x:xs) 右辺

f (head (x:xs))
= f x

fがstrictであることが条件(== f undefined = undefined）。

Exercise D

cpをfoldrで定義せよ：

cp = foldr f [[]]
     where f xs xss = [y:ys | y <- xs, ys <- xss]

length . cpをfusion lawを使ってfoldrで定義せよ：

length . cp = length . foldr f [[]]
              where f xs xss = [y:ys | y <- xs, ys <- yss]

fusion lawの三条件を使うと：

length undefined = undefined  -- 成り立つ
length [[]]       = 1

length [y:ys | y <- xs, ys <- xss] = h xs (length xss)
length xs * length xss = h xs (length xss)

h x y = length x * y

なので

length cp = foldr ((*) . length) 1

map lengthをfoldrで定義せよ：

map length = foldr ((:) . length) []

product . map lengthをfusion lawを使ってfoldrで定義せよ：

product . map length = product . foldr ((:) . length) []

fusion lawの三条件：

product undefined       = undefined
product []              = 1
product (length x : xs) = h x (product xs)
length x * product xs   = h x (product xs)
h x y                   = length x * y

なので

product . map length = foldr ((*) . length) 1

length . cpとproduct . map lengthの同値性：

product . map length = foldr ((*) . length) 1
length cp            = foldr ((*) . length) 1

Exercise E

The first two arguments of foldr are replacements for the constructors

(:) :: a -> [a] -> [a] [] :: [a]

of lists. A fold function can be defined for any data type: just give replacements for the constructors of the data type.

とあるが、いまいち何を言っているのかわかりにくかった。そもそももともと何処にあったconstructorをreplaceしているというのだろう？

data Nat = Zero | data Succ Nat

のためのfoldを定義せよ：

foldN :: (a -> a) -> a -> Nat -> a
foldN f e Zero = e
foldN f e (Succ n) = f (foldN f e n)

自然数０に何らかの要素eを対応付け、１にf(e)を、２にf(f(e))を・・・　としている。

data NEList = One a | Cons a (NEList a)

のためのfoldを定義せよ：

foldNEList :: (a -> b -> b) -> (a -> b) -> [a] -> b
foldNEList f g [x] = g x
foldNEList f g (x:xs) = f x (foldNEList f g xs)

この定義と比較すると、Preludeのfoldr1は

foldr1 :: (a -> a -> a) -> [a] -> a
foldr1 f = foldNEList f id

となっていることがわかり、表現力が低くなっている。