Arantium Maestum

プログラミング、囲碁、読書の話題

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}が任意の有限リストxsysで成り立つなら、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}が任意の有限リストxsysで成り立つ。

よって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..])

上の式によって表される数学的概念は{\sum_{n=0}^{\infty} \frac{1}{n!} = e}自然対数の底)である。

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

が導き出される。