Thinking Functionally with Haskell勉強メモ: 第6章問題2
Exercise F
第一部
任意の有限リストxs
について、以下の等式が成り立つことを証明せよ:
foldl f e xs = foldr (flip f) e (reverse xs)
帰納法で解く。
Case [] 左辺
foldl f e []
= {foldlの定義}
e
Case [] 右辺
foldr (flip f) e (reverse []) = {reverse [] = []} foldr (flip f) e [] = {foldrの定義} e
Case []は証明できた。
Case x:xs 左辺
foldl f e (x:xs) = {foldlの定義} foldl f (f e x) xs = {induction} foldr (flip f) (f e x) (reverse xs)
Case x:xs 右辺
foldr (flip f) e (reverse (x:xs)) = {reverse (x:xs) = reverse xs ++ [x]} foldr (flip f) e (reverse xs ++ [x]) = {foldr f e (xs++ys) = foldr f (foldr f e ys) xs} foldr (flip f) (foldr (flip f) e [x]) (reverse xs) = {foldrの定義} foldr (flip f) (flip f x (foldr (flip f) e [])) (reverse xs) = {foldrの定義} foldr (flip f) (flip f x e) (reverse xs) = {flipの定義} foldr (flip f) (f e x) (reverse xs)
これで{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}
が任意の有限リストxs
とys
で成り立つなら、Case x:xsも証明できた。
{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}
の帰納的証明:
Case [] 左辺
foldr f e ([]++ys) = {[]++xs=xs} foldr f e ys
Case [] 右辺
foldr f (foldr f e ys) []
= {foldrの定義}
foldr f e ys
Case []証明完了。
Case x:xs 左辺
foldr f e ((x:xs)++ys) = {(x:xs)++ys = x:(xs++ys)} foldr f e (x:(xs++ys)) = {foldrの定義} f x (foldr f e (xs++ys)) = {induction} f x (foldr f (foldr f e ys) xs)
Case x:xs 右辺
foldr f (foldr f e ys) (x:xs) = {foldrの定義} f x (foldr f (foldr f e ys) xs)
Case x:xs証明完了。
{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}
が任意の有限リストxs
とys
で成り立つ。
よってfoldl f e xs = foldr (flip f) e (reverse xs)
も任意の有限リストxs
で成り立つ。
第二部
任意の有限リストxs
について、以下の等式が成り立つことを証明せよ:
foldl (@) e xs = foldr (<>) e xs
ただし以下の条件が成り立つ:
(x <> y) @ z = x <> (y @ z) e @ x = x <> e
帰納法で証明する。
case [] 左辺
foldl (@) e [] = {foldlの定義} e
case [] 右辺
foldr (<>) e [] = {foldrの定義} e
case []証明完了(ほぼ自明)。
case x:xs 左辺
foldl (@) e (x:xs) = {foldlの定義} foldl (@) (e @ x) xs = {e @ x = x <> e} foldl (@) (x <> e) xs = {to be proven} x <> (foldl (@) e xs) = {induction} x <> (foldr (<>) e xs)
case x:xs 右辺
foldr (<>) e (x:xs) = {foldrの定義} x <> (foldr (<>) e xs)
Case x:xsはfoldl (@) (x <> e) xs = x <> (foldl (@) e xs)
が成り立つなら成り立つ。
foldl (@) (x <> e) xs = x <> (foldl (@) e xs)
の証明:
case [] 左辺
foldl (@) (x <> e) [] = {foldlの定義} x <> e
case [] 右辺
x <> (foldl (@) e []) = {foldlの定義} x <> e
case []証明完了。
case y:ys 左辺
foldl (@) (x <> e) (y:ys) = {foldlの定義} foldl (@) ((x <> e) @ y) ys = {(x <> y) @ z = x <> (y @ z)} foldl (@) (x <> (e @ y)) ys = {induction} x <> (foldl (@) (e @ y) ys)
case y:ys 右辺
x <> (foldl (@) e (y:ys)) = {foldlの定義} x <> (foldl (@) (e @ y) ys)
Case x:xs証明完了。
foldl (@) (x <> e) xs = x <> (foldl (@) e xs)
は成り立つ。
よってfoldl (@) e xs = foldr (<>) e xs
も成り立つ。
(ただ、この証明のこの部分はイマイチ自信がない・・・)
foldl (@) (x <> (e @ y)) ys = {induction} x <> (foldl (@) (e @ y) ys)
もうちょっと何が起きているのか考えて自分の中で納得する必要がある。
Exercise G
第一部
以下の条件が成り立つとして:
foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys
以下の等式が成り立つことを証明せよ:
foldl f e . concat = foldl (foldl f) e
帰納法:
Case []はfoldl
の定義から自明(両辺がe
になる)。
Case undefined 左辺
foldl f e (concat undefined) = {concatの定義} foldl f e undefined = {foldlの定義} undefined
Case undefined 右辺
foldl (fold f) e undefined
= {foldlの定義}
undefined
Case undefined証明完了。
Case xs:xss 左辺
foldl f e (concat xs:xss) = {concatの定義} foldl f e (xs ++ concat xss) = {foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys} foldl f (foldl f e xs) (concat xss) = {induction} foldl (foldl f) (foldl f e xs) xss
Case xs:xss 右辺
foldl (fold f) e (xs:xss) ={foldlの定義} foldl (foldl f) (foldl f e xs) xss
Case xs:xss証明完了。
よってfoldl f e . concat = foldl (foldl f) e
は成り立つ。
第二部
以下の条件が成り立つとして:
foldr f e (xs ++ ys) = foldr f (foldr f e ys) xs
以下の等式が成り立つことを証明せよ:
foldr f e . concat = foldr (flip (foldr f)) e
Case [] 左辺
foldr f e (concat []) = {concatの定義} foldr f e [] = {foldrの定義} e
Case [] 右辺
foldr (flip (foldr f)) e []
= {foldrの定義}
e
Case [] 証明完了。
Case undefined 左辺
foldr f e (concat undefined) = {concatの定義} foldr f e undefined = {foldrの定義} undefined
Case undefined 右辺
foldr (flip (foldr f)) e undefined
= {foldrの定義}
undefined
Case undefined証明完了。
Case xs:xss 左辺
foldr f e (concat xs:xss) = {concatの定義} foldr f e (xs ++ concat xss) = {foldr f e (xs ++ ys) = foldr f (foldr f e ys) xs} foldr f (foldr f e (concat xss)) xs
Case xs:xss 右辺
foldr (flip (foldr f)) e (xs:xss) = {foldrの定義} flip (foldr f) xs (foldr (flip (foldr f)) e xss) = {flipの定義} foldr f (foldr (flip (foldr f)) e xss) xs = {induction} foldr f (foldr f e (concat xss)) xs
Case xs:xss証明完了。
よってfoldr f e . concat = foldr (flip (foldr f)) e
は成り立つ。
Exercise H
sum (scanl (/) 1 [1..])
上の式によって表される数学的概念は(自然対数の底)である。
Exercise I
以下の等式から:
scanr f e = map (foldr f e) . tails
以下のscanr
の定義が導き出されることを証明せよ:
scanr f e [] = [e] scanr f e (x:xs) = f x (head ys) : ys where ys = scanr f e xs
Case []
map (foldr f e) (tails []) = {tailsの定義} map (foldr f e) [[]] = {mapの定義} (foldr f e []):map (foldr f e) [] = {mapの定義} (foldr f e []):[] = {foldrの定義} [e]
Case []証明完了。
Case undefined
map (foldr f e) (tails undefined) = {tailsの定義} map (foldr f e) undefined = {mapの定義} undefined
scanr
の定義では最初のパターンマッチでundefined
になる。
Case undefined証明完了。
Case 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)) = {scanr f e = map (foldr f e) . tails} (foldr f e (x:xs)) : (scanr f e xs) = {foldrの定義} (f x (foldr f e xs)) : (scanr f e xs) = {to be proven} (f x (head (scanr f e xs))) : (scanr f e xs) = {extract identical expressions as ys} (f x (head ys)) : ys where ys = scanr f e xs
Case x:xsはfoldr f e xs = head (scanr f e xs)
が成り立てば成り立つ。
foldr f e xs = head (scanr f e xs)
を帰納法で証明する。
Case []
head (scanr f e []) = {scanr f e = map (foldr f e) . tails} head (map (foldr f e) (tails [])) = {tailsの定義} head (map (foldr f e) [[]]) = {mapの定義} head ((foldr f e []) : map (foldr f e) []) = {headの定義} foldr f e []
Case [] 証明完了。
Case undefined
head (scanr f e undefined) = {scanr f e = map (foldr f e) . tails} head (map (foldr f e) (tails undefined)) = {tailsの定義} head (map (foldr f e) undefined) = {mapの定義} head undefined = {headの定義} undefined
foldr f e undefined
も定義から自明にundefined
。
Case undefined証明完了。
Case x:xs
head (scanr f e (x:xs)) = {scanr f e = map (foldr f e) . tails} head (map (foldr f e) (tails (x:xs))) = {tailsの定義} head (map (foldr f e) ((x:xs):(tails xs))) = {mapの定義} head ((foldr f e (x:xs)) : map (foldr f e) (tails xs)) = {headの定義} foldr f e (x:xs)
Case x:xs証明完了。
foldr f e xs = head (scanr f e xs)
は成り立つ。
よって
scanr f e = map (foldr f e) . tails
から
scanr f e [] = [e] scanr f e (x:xs) = f x (head ys) : ys where ys = scanr f e xs
が導き出される。