運算の楽しみ
この記事はHaskell Advent Calendar 2016に参加したものです．
プログラム運算
関数プログラミングでは，プログラムは関数として定義します．（この関数は，もちろん計算可能な関数でなければならないという制限はあるものの，数学の対象として扱える関数です．）
単純明瞭な関数定義は，正しいことが明白ではあり，プログラムの仕様として機能します．（すなわち，関数プログラミングにおいてプログラムは実行可能な仕様ということになります．）
しかし，単純明瞭な関数定義は効率が悪いのが通常で，そのままでは実用に供することができません．これを等式論証の手法を用いて，意味を変えずに，複雑ではあるけれど効率の良い定義を導出するのが，プログラム運算（program calculation）です．
最大切片和（maximum segment sum）問題
これは有名な問題で，与えられた整数列のすべての切片の和のうち最大のものを求めよ，というものです．
切片（segment）は，連続部分列（contiguous subsequence）ともいいます．
mssの仕様
まず，仕様をそのまま実装してみましょう．
関数名をmssとしましょう．
mssは整数のリストから整数への関数なので，型シグネチャは
code:haskell
mss :: Int -> Int
となります．
与えられた整数列の切片をすべて生成する関数をsegs，与えられたリストの要素の総和を求める関数をsum，与えられたリストの最大要素を求める関数をmaximumとすると，mssの仕様mss0は以下のように定義できます．
code:haskell
mss0 :: Int -> Int
mss0 = maximum . map sum . segs
mss0の漸近的時間計算量
maximum，sum，segsの3つの関数がきちんと仕様を満していれば，mss0の仕様記述は正しいことは明らかでしょう．では，3つの関数を定義を見ましょう．
code:haskell
maximum :: Int -> Int
maximum = foldr max minBound
maximumはData.Listモジュールからエクスポートされており，少し定義は異なります．（さらに，もう少し多相的に定義されています．）しかし，仕様としても，漸近的時間計算量（入力リストの長さを$ nとすると$ O(n)になる）としても，本質的には上のものと同じです．
code:haskell
sum :: Int -> Int
sum = foldl (+) 0
sumはPreludeモジュールからエクスポートされています．こちらもIntのリスト上の関数としては，仕様としても，漸近的時間計算量（入力リストの長さを$ nとすると$ O(n)になる）としても，本質的には上のものと同じです．
code:haskell
segs :: a -> a
segs = concatMap inits . tails
initsとtailsはともにData.Listモジュールからエクスポートされている関数で，指定されたリストの先頭部分リストのリストと末尾部分リストのリストを生成する関数です．たとえば，inits "abc"は["","a","ab","abc"]であり，tails "abc"は["abc","bc","c",""]です．したがって，segsは，指定したリストの長さを$ nとすると$ O(n)の長さの切片を，$ O(n^2)個生成するので，
mss0の漸近的時間計算量は$ O(n^3)ということになる．
運算によって$ O(n^2)の定義を導出する
code:proof
maximum . map sum . segs
= { segsの定義 }
maximum . map sum . concatMap inits . tails
= { concatMapの仕様 }
maximum . map sum . concat . map inits . tails
= { map-concat則 }
maximum . concat . map (map sum) . map inits . tails
= { mapのファンクタ則 }
maximum . concat . map (map sum . inits) . tails
= { sumの定義 }
maximum . concat . map (map (foldl (+) 0) . inits) . tails
= { scanlの仕様 }
maximum . concat . map (scanl (+) 0) . tails
scanl f eはfが定数時間のとき，入力のリストの長さに比例する定義になっていれば，これで$ O(n^2)の定義が導出できたことになります．
scanl f eの入力リストの長さに比例する時間計算量になる定義は以下のように運算すると求められます．
code:proof
入力が [] 場合
scanl f e []
= { scanlの仕様 }
(map (foldl f e) . inits) []
= { 関数合成の定義 }
map (foldl f e) (inits [])
= { initsの定義 }
map (foldl f e) [[]]
= { mapの定義 }
foldl f e [] : map (fold f e) []
= { mapの定義 }
[foldl f e []]
= { foldlの定義 }
e
入力が x:xs の場合
scanl f e (x:xs)
= { scanlの仕様 }
(map (foldl f e) . inits) (x:xs)
= { 関数合成の定義 }
map (foldl f e) (inits (x:xs))
= { initsの定義 }
map (foldl f e) ([] : map (x:) (inits xs))
= { mapの定義 }
foldl f e [] : map (foldl f e) (map (x:) (inits xs))
= { foldlの定義 }
e : map (foldl f e) (map (x:) (inits xs))
= { 関数合成の定義 }
e : (map (foldl f e) . map (x:)) (inits xs)
= { foldl f e . (x:) = foldl f (f e x) であるから }
e : map (foldl f (f e x)) (inits xs)
= { scanlの仕様 }
e : scanl f (f e x) xs
というわけで，scanlの効率のよい定義は以下のようになります．
code:haskell
scanl :: (a -> a -> a) -> a -> a -> a
scanl f e [] = e
scanl f e (x:xs) = e : scanl f (f e x) xs
運算によって$ O(n)の定義を導出する
code:proof
maximum . concat . map (scanl (+) 0) . tails
= { 簿記の法則（maximum . concat = maximum . map maximum） }
maximum . map maximum . map (scanl (+) 0) . tails
= { mapのファンクタ則 }
maximum . map (maximum . scanl (+) 0) . tails
= { maximumの定義 }
maximum . map (foldr max minBound . scanl (+) 0) . tails
= { {Int,max,minBound,(+),0}の5つ組は半環をなすので，半環融合則により，x # y = 0 max (x+y)とすると }
maximum . map (foldr (#) 0) . tails
= { scanrの仕様 }
maximum . scanr (#) 0
scanr f eはfが定数時間のとき，入力のリストの長さに比例する定義になっていれば（こちらもscanrの仕様から運算で導出できます），これで$ O(n)の定義が導出できたことになります．
追記(2017-01-05)
最終的に得られた効率のよいプログラムが正しい（仕様を満す）プログラムであることが、運算によって保証されているということが肝心です。
#元qiita