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

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)

が成り立つ。