Thinking Functionally with Haskell勉強メモ: 第6章問題3
Exercise J
Maximum Subsequence Sumが以下のように定義されている:
mss :: [Int] -> Int mss = maximum . map sum . subseqs subseqs :: [a] -> [[a]] subseqs [] = [[]] subseqs (x:xs) = xss ++ map (x:) xss where xss = subseqs xs
より効率のいい定義を求めよ。
現状では各要素ごとにsubsequenceの数が倍になるので、計算量O(2**n)。
subseqs
のfoldr
化
以下の等式が成り立つことを証明する:
subseqs = foldr f [[]] where f x y = y ++ map (x:) y
Case []はfoldr
の定義から自明。
Case x:xs
foldr f [[]] (x:xs) = {foldrの定義} f x (foldr f [[]] xs) = {induction} f x (subseq xs) = {fの定義} (subseq xs) ++ map (x:) (subseq xs) = {重複パターンをxssに束縛} xss ++ map (x:) xss where xss = subseq xs
証明完了。
mss
の定義は
mss :: [Int] -> Int mss = maximum . map sum . foldr f [[]] where f x y = y ++ map (x:) y
fusion law 1
map sum . foldr f [[]]
にfusion lawを適用する。
fusion lawの条件:
f . foldr g a = foldr h b {s.t.} f undefined = undefined f a = b f (g x y) = h x (f y)
まず第一、第二条件:
map sum undefined = undefined -- mapの定義から map sum [[]] = sum [] : [] = [0]
第一条件は満たしていることがわかる。第二条件からfusion lawの結果はfoldr h [0]
になるとわかる。
第三条件からh
を特定する:
map sum (y ++ map (x:) y) = h x (map sum y)
左辺をx
とmap sum y
の組み合わせに変換したい:
map sum (y ++ map (x:) y) = (map f (xs ++ ys) = map f xs ++ map f ys) map sum y ++ map sum (map (x:) y) = {functor law of map} map sum y ++ map (sum . (x:)) y = {sum . (x:) = (x+) . sum -- (to be proven)} map sum y ++ map ((x+) . sum) y = {functor law of map} map sum y ++ map (x+) (map sum y)
(to be provenな部分は最後にまとめて証明していく)
fusion law第三条件からh x y = y ++ map (x+) y
が導き出された。
mss
の定義は
mss :: [Int] -> Int mss = maximum . foldr f [0] where f x y = y ++ map (x+) y
fusion law 2
再度fusion lawを適用してみる。
第一、第二条件
maximum undefined = undefined maximum [0] = 0
どちらもmaximum
の定義から。
第三条件:
maximum (y ++ map (x+) y) = h x (maximum y) maximum (y ++ map (x+) y) = {maximum = foldr1 max} foldr1 max (y ++ map (x+) y) = {foldr1 max (xs ++ ys) = max (foldr1 max xs) (foldr1 max ys) -- (to be proven)} max (foldr1 max y) (foldr1 max (map (x+) y)) = {foldr1 (<>) . map (x@) = (x@) . foldr1 (<>) iff (@) distributes over (<>)} max (foldr1 max y) (x + (foldr1 max y)) = {maximum = foldr1 max} max (maximum y) (x + maximum y)
後述するが
foldr1 max (xs ++ ys) = max (foldr1 max xs) (foldr1 max ys)
はxs != []
、ys != []
が条件。
このケースでは、
foldr f [0] where f x y = y ++ map (x+) y
の部分で使われるのでxs != []
、ys != []
が成り立つ。(xs = y
、ys = map (x+) y
でy
は[0]
かそこに要素を加えたもの)
fusion law第三条件からh x y = max y (x + y)
が導き出された。
mss
の定義は
mss :: [Int] -> Int mss = foldr f 0 where f x y = max y (x + y)
最終的には計算量O(n)になった。
問題を読んで直観的に「最善でO(n)だな」とはわかっていたのだが、元の定義からO(n)への道筋がまったく見えなかったのに半ば機械的に式変換していっただけでそこまで最適化されたのは感動した。
補足証明
sum . (x:) = (x+) . sum
sum (x:xs) = {sum = foldr (+) 0} foldr (+) 0 (x:xs) = {foldrの定義} x + (foldr (+) 0 xs) = {sum = foldr (+) 0} x + sum xs
foldr1 max (xs ++ ys) = max (foldr1 max xs) (foldr1 max ys)
この等式はどちらかのリストが[]
の場合成り立たない。右辺がundefined
になってしまう。
ベースケースはCase [x]。
Case [x] 左辺
foldr1 max ([x] ++ ys) = {[x] ++ ys = x:ys} foldr1 max (x:ys) = {foldr1の定義} max x (foldr1 max ys)
Case [x] 右辺
max (foldr1 max [x]) (foldr1 max ys) = {foldr1 max [x] = x} max x (foldr1 max ys)
Case [x]証明完了。
Case x:xs 左辺
foldr1 max ((x:xs) ++ ys) = {(x:xs) ++ ys = x:(xs ++ ys)} foldr1 max (x : (xs ++ ys)) = (foldr1の定義} max x (foldr1 max (xs ++ ys)) = {induction} max x (max (foldr1 max xs) (foldr1 max ys))
Case x:xs 右辺
max (foldr1 max (x:xs)) (foldr1 max ys) = {foldr1の定義} max (max x (foldr1 max xs)) (foldr1 max ys) = {(a `max` b) `max` c = a `max` (b `max` c)} max x (max (foldr1 max xs) (foldr1 max ys))
Case x:xs証明完了。
よってxs != [], ys != []
の場合:
foldr1 max (xs ++ ys) = max (foldr1 max xs) (foldr1 max ys)
が成り立つ。