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

### Exercise A

```mult :: Nat -> Nat -> Nat
mult Zero y = Zero
mult (Succ x) y = mult x y + y
```

`mult (x+y) z = mult x z + mult y z`を証明せよ：

case 0 左辺

```mult (x+0) z

= {x+0 = x}
mult x z
```

case 0 右辺

```mult x z + mult 0 z

= {mult Zero y = Zero}
mult x z + 0

= {x+0 = x}
mult x z
```

case y+1 左辺

```mult (x+(y+1)) z

= {x+(y+1) = (x+y)+1}
mult ((x+y)+1) z

= {mult (Succ x) y = mult x y + y }
mult (x+y) z + z
```

case y+1 右辺

```mult x z + mult (y+1) z

= {mult (Succ x) y = mult x y + y }
mult x z + (mult y z + z)

= {x + (y + z) = (x + y) + z}
(mult x z + mult y z) + z

= {induction}
mult (x+y) z + z
```

# Exercise B

```reverse (xs ++ ys) = reverse ys ++ reverse xs
```

の証明：

Case [] 左辺

```reverse ([] ++ ys)

= { [] ++ xs = xs}
reverse ys
```

Case [] 右辺

```reverse ys ++ reverse []

= { reverse [] = [] }
reverse ys ++ []

= {[] ++ xs = xs}
reverse ys
```

Case (x:xs) 左辺

```reverse ((x:xs) ++ ys)

= {(x:xs) ++ ys = x:(xs++ys)}
reverse (x:(xs++ys))

= {reverse x:xs = reverse xs ++ [x] }
reverse (xs++ys) ++ [x]
```

Case (x:xs) 右辺

```reverse ys ++ reverse (x:xs)

= { reverse (x:xs) = reverse xs ++ [x] }
reverse ys ++ (reverse xs ++ [x])

= {xs ++ (ys ++ zs) = (xs ++ ys) ++ zs }
(reverse ys ++ reverse xs) ++ [x]

= {induction}
reverse (xs++ys) ++ [x]
```

Exercise C

```head . map f = f . head
```

の証明。

Case undefined 左辺

```head (map f undefined)
= undefined
```

Case undefined 右辺

```f (head undefined)
= f undefined
```

Case [] 左辺

```head (map f [])
= undefined
```

Case [] 右辺

```f (head [])
= f undefined
```

Case (x:xs) 左辺

```head (map f (x:xs))
= head ((f x) : map f xs)
= f x
```

Case (x:xs) 右辺

```f (head (x:xs))
= f x
```

`f`がstrictであることが条件(== `f undefined = undefined`）。

# Exercise D

### `cp`を`foldr`で定義せよ：

```cp = foldr f [[]]
where f xs xss = [y:ys | y <- xs, ys <- xss]
```

### `length . cp`をfusion lawを使って`foldr`で定義せよ：

```length . cp = length . foldr f [[]]
where f xs xss = [y:ys | y <- xs, ys <- yss]
```

fusion lawの三条件を使うと：

```length undefined = undefined  -- 成り立つ
length [[]]       = 1

length [y:ys | y <- xs, ys <- xss] = h xs (length xss)
length xs * length xss = h xs (length xss)

h x y = length x * y
```

なので

```length cp = foldr ((*) . length) 1
```

### `map length`を`foldr`で定義せよ：

```map length = foldr ((:) . length) []
```

### `product . map length`をfusion lawを使って`foldr`で定義せよ：

```product . map length = product . foldr ((:) . length) []
```

fusion lawの三条件

```product undefined       = undefined
product []              = 1
product (length x : xs) = h x (product xs)
length x * product xs   = h x (product xs)
h x y                   = length x * y
```

なので

```product . map length = foldr ((*) . length) 1
```

### `length . cp`と`product . map length`の同値性：

```product . map length = foldr ((*) . length) 1
length cp            = foldr ((*) . length) 1
```

# Exercise E

The first two arguments of `foldr` are replacements for the constructors

`(:) :: a -> [a] -> [a]` `[] :: [a]`

of lists. A fold function can be defined for any data type: just give replacements for the constructors of the data type.

とあるが、いまいち何を言っているのかわかりにくかった。そもそももともと何処にあったconstructorをreplaceしているというのだろう？

```data Nat = Zero | data Succ Nat
```

のための`fold`を定義せよ：

```foldN :: (a -> a) -> a -> Nat -> a
foldN f e Zero = e
foldN f e (Succ n) = f (foldN f e n)
```

`data NEList = One a | Cons a (NEList a)`

のための`fold`を定義せよ：

```foldNEList :: (a -> b -> b) -> (a -> b) -> [a] -> b
foldNEList f g [x] = g x
foldNEList f g (x:xs) = f x (foldNEList f g xs)
```

この定義と比較すると、Preludeの`foldr1`

```foldr1 :: (a -> a -> a) -> [a] -> a
foldr1 f = foldNEList f id
```

となっていることがわかり、表現力が低くなっている。