手作業でプログラム運算

• 関数プログラミング入門 Haskellで学ぶ原理と技法, Richard Bird(著) / 山下伸夫(訳), 2012

 p368の練習問題12.1.3

zipp . pair (map f, map g) = map (pair (f, g))という法則は両辺を同じ結果に単純化することで証明できるか. 証明はzipp . unzip . map (pair (f, g))という式を2つの本質的に異なる方法(1つはzipp . unzip = idという法則を使い, もう1つはunzipの定義を使うことで単純化することで可能になる. 詳細を示せ.

 プログラム運算を実感するために, 上記の問題をやってみたいと思います. zippは, カリー化されてないzip関数.
 各関数の定義.

pair (f, g) x = (f x, g x)
zipp = uncurry zip
uncurry f xy = f (fst xy) (snd xy)
unzip = pair (map fst, map snd)

 早速, 変換を始めてみると,

zipp . unzip . map (pair (f, g))
{- zipp . unzip = idより -}
= map (pair (f, g))
= 右辺

{- unzipの定義から, -}
zipp . unzip . map (pair (f, g))
= zipp . pair (map fst, map snd) . map (pair (f, g))  --(1)

{- ここで, -}
pair (map fst, map snd) . map (pair (f, g))
{- pair (f, g) . h = pair (f . h, g . h) だから -}
= pair (map fst . (map (pair (f, g))), map snd . (map (pair (f, g))))
{- map分配則(map f . map g = map (f . g))から -}
= pair (map (fst . (pair (f, g))), map (snd . (pair (f, g))))
{- fst . pair (f, g) = fなどから -}
= pair (map f, map g)

{- なので, -}
zipp . unzip . map (pair (f, g))
= zipp . pair (map f, map g)
= 左辺

 左辺の変換は, ポイントフリーだとわかりにくいので, リストxsを使って考えると,

pair (map fst, map snd) (map (pair (f, g)) xs)
= (map fst (map (pair (f, g)) xs), (map snd (map (pair (f, g)) xs))
{- point freeで書き直すと -}
= (map fst . map (pair (f, g)) xs), ((map snd . map (pair (f, g)) xs))
{- map分配則から -}
= (map (fst . pair (f, g)) xs), map (snd . pair (f ,g)) xs)
{- fst .pair (f ,g) = f などから -
= (map f xs, map g xs)
= pair (map f, map g) xs

{- のように変形できるので, -}
unzip . map (pair (f, g))
= pair (map f, map g)

と考えることも可能.

というわけで, zipp . pair (map f, map g) = map (pair (f, g))が成立.

まとめると,

zipp . pair (map f, map g)
{- fst . pair (f, g) = fなどから -}
= zipp . pair (map (fst . (pair (f, g))), map (snd . (pair (f, g))))
{- map分配則(map f . map g = map (f . g))から -}
= zipp . pair (map fst . (map (pair (f, g))), map snd . (map (pair (f, g))))
{- pair (f, g) . h = pair (f . h, g . h) だから -}
= zipp . pair (map fst, map snd) . map (pair (f, g))
{- unzipの定義から-}
= zipp . unzip . map (pair (f, g))
{- zipp . unzip = idより -}
= map (pair (f, g))

2014/12/11, 間違っていたので一部修正.