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
