# 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
```

より効率のいい定義を求めよ。

##### `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]
```

```map sum (y ++ map (x:) y) = h 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

```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)
```

#### 補足証明

##### `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)
```

が成り立つ。