Universal Property of fold

foldにはパッと見では分からない便利な特性を持っています.
その中でも(多分)かなり基本的な部類の性質を紹介します.


(注意1) 記事中でのfoldは全てfold-rightです.
(注意2) (o)は(.)です(点だと見づらいので)


一応foldの定義

fold f v []     = v
fold f v (x:xs) = f x (fold f v xs)

foldの特性

有限リストについて以下の二組の式

g []     = v
g (x:xs) = f x (g xs)

g = fold f v

の二つの式は同じ事を示しています.(片方が成り立てばもう片方も成り立つ)
これをfoldのUniversal Propertyといいます.

Universal Propertyを使った証明

リストの合計に1を足す関数の二つの異なる定義が等しいことを証明します.

((+) 1) o sum = fold (+) 1

リストの全要素を合計する関数sumの定義

sum [] = 0
sum (x:xs) = x + sum xs

universal propertyにより,以下のように展開できます.

 (((+) 1) o sum) []     = 1
 (((+) 1) o sum) (x:xs) = (+) x ((((+) 1) o sum) xs)

単に読みづらくなっただけに見えますが,
これを中置記法に変形して, さらに関数合成を展開すれば,...

 sum []     + 1 = 1
 sum (x:xs) + 1 = x + (sum xs + 1)

のように(非常に読み易く)変形出来ます.


ここで,それぞれの式の左辺を以下のように展開します.

sum [] + 1 => {sumの定義により} => 0 + 1 => 1
sum (x:xs) + 1
=> {sumの定義により} => (x + sum xs) + 1
=> x + (sum xs + 1)

よってそれぞれの等式が成り立つことが分かったので,

((+) 1) o sum = fold (+) 1

が証明できました (^^)b

何がすごいの?

universal properyを使うことによって,
再帰を含んだ関数(この例ではsum)を扱う際にも,明示的に再帰を持ち出す必要が無くなっています.
再帰はfoldの中に封じ込められています.(ここテストに出ます!)


参考