An easy application of fusion law

Pearls of Functional Algorithm Design読書会で、Birdさんの"An easy application of fusion law of foldr"という１文に対して２時間ほど、どうやって融合法則を適用するか喧々諤々の議論が行われましたが、なんとなくuprefixesの定義が導き出せたような気がするので記念に。

filter (all up) . unravels
= {- definition of unravels -}
  filter (all up) . foldr (concatMap .prefixes) [[]]

Fusion law of foldr.
If f is strict, f a = b, and f (g x y) = h x (f y), then f . foldr g a = foldr h b
Let f = filter (all up), g = concatMap . prefixes, a = [[]].
Then b = f a = f [[]] = [[]]. (try it in ghci!)

f (g x y)
= {- definition of (.) -}
  (f . g x) y
= {- definition of f and g-}
  (filter (all up) . (concatMap . prefixes) x) y
= {- definition of (.) -}
  (filter (all up) . concatMap (prefixes x)) y
= {- definition of concatMap -}
  (filter (all up) . concat . map (prefixes x)) y
= {- filter-concat law, filter p . concat = concat . map (filter p). IFPH p.108 -}
  (concat . map (filter (all up)) . map (prefixes x)) y
= {- map i . map j = map (i . j). IFPH p.106 -}
  (concat . map (filter (all up) . prefixes x)) y
= {- definition of concatMap -}
  concatMap (filter (all up) . prefixes x) y

HFusion : A Fustion Tool for Haskell prgramsで紹介されている関数融合方法に従って、 (fliter (all up))と
(prefixes x)を融合して関数(f' x)を導く。
http://babel.ls.fi.upm.es/services/talks/HFusion.pdf

関数融合を行うには、filter (all up)とprefixes xの定義を書き出して、以下の2つのステップを行なう。
 1. prefixes xのデータ・コンストラクタ((:)と[])をfilter (all up)の対応する出力で置き換える。
 2. prefixes xの再帰呼び出しをf' xで置き換える。

filter (all up)の定義。
filter (all up) :: [[[a]]] -> [[[a]]]
filter (all up) [] = []
filter (all up) (xs:xss) = if (all up) xs then xs : filter (all up) xss else filter (all up) xss
prefixes xの定義。
prefixes :: a -> [[a]] -> [[[a]]]
prefixes x [] = [[[x]]] = [[x]] : []
prefixes x (xs:xss) = [(x:xs):xss] ++ map (xs :) (prefixes x xss)

f' xを導出。
f' x []
= {- prefixes x [] の定義[[[x]]]は、[[x]] : []なので、データ・コンスラクタ(:)と[]がある。filter (all up)の定義より、[]は[]に、(:)は if ~ then ~ else ~に置き換える。-}
  if (all up) [[x]] then [[x]] : filter (all up) [] else filter (all up) []
= {- (all up) [[x]]は、常にTrueなので -}
  [[x]] : filter (all up) []
= {- filter p [] = [] -}
  [[x]] : []
= [[[x]]]
f' x (xs::xss)
= {- 上と同様にデータ・コンスラクタを置換する。prefixes x (xs::xss)の定義では第1項目 [(x:xs):xss]にデータ・コンストラクタ(:)と[]がある。また、prefixes xの再帰呼び出しをf' xに置換する。-}
  (if (all up) ((x:xs):xss) then ((x:xs):xss) : filter (all up) [] else filter (all up) []) ++ map (xs :) (f' x xss)
= {- filter p [] = [] -}
  (if (all up) ((x:xs):xss) then ((x:xs):xss) : [] else []) ++ map (xs :) (f' x xss)
= {- 連結をifの中へ -}
  if (all up) ((x:xs):xss) then [((x:xs):xss)] ++ map (xs :) (f' x xss) else map (xs :) (f' x xss)

f' xの定義をまとめると。
f' :: a -> [[a]] -> [[[a]]]
f' x []       = [[[x]]]
f' x (xs:xss) = if (all up) ((x:xs):xss) then
                  [(x:xs):xss] ++ map (xs :) (f' x xss)
                else map (xs :) (f' x xss)

今、融合法則の条件を満すため、f (g x y) = h x (f y)となる関数hを見つけたい。
h x (f y) = f (g x y) = concatMap (f' x) y
なので、hはある関数h'に対して以下のような形であると推測できる。
h x (f y) = concatMap (h' x) (f y)
fが(filter (all up))であるので、(f y)は、yの要素の中で、(all up)を満すような要素からなるリストである。
(h' x)は、(all up)を満すような値(zs:zss)を取り、(f x)と同じ結果を出力する関数。
h' :: a -> [[a]] -> [[[a]]]
h' x [] = f' x [] = [[[x]]]
h' x (zs:zss)
= {- h' xはf xと同じ出力をするので。-}
  f' x (zs:zss)
= {- f' xの定義。-}
  if (all up) ((x:zs):zss) then [(x:zs):zss] ++ map (zs :) (f' x zss) else map (zs :) (f' x zss)
= {- (all up) (zs:zss) = Trueと、all upの定義より、(all up) ((x:zs):zss) = x <= head zs -}
  if x <= zs then [(x:zs):zss] ++ map (zs :) (f' x zss) else map (zs :) (f' x zss)

このh'が待望のuprefixes。

hの第2引数(f y)にある性質を仮定することがhを導き出すポイントのような気がする。 今回の場合、fが(filter all up)なのでhの第2引数は(all up)がTrueになるようなものしかとらない。 そのため、if文の条件が簡単にできた。