圏論勉強会第７回

(T,in)がF始代数ならば
(|in|)=1T(反射則)
またh∘f=g∘F(h)　①が成り立つならば
h∘(|f|)=(|g|)　　　②　(融合則)

sum∘filter(even)を一つのfoldrで表せ。

まず
p(a,as)=　　cons(a,as)　(even(a)=trueの時)
　　　　　{　as　(それ以外)
とするとfilter(even)=(|[nil,p]|)となります。
　　このfilter(even)=(|[nil,p]|)が②の(|f|)に対応する

 よってsum∘[nil,p]=[c,g]∘(11+1A×sum)　③　を満たすc,gを見つければ融合則が使えます。
　　　①に対応する式が③　　　また、[nil,p]が①のfに対応している。　sumはｈに対応。

これをpointwiseな等式に書き直すとまずc=sum(nil)=0であり,
　　　　∵③式の左の要素どうしが等しいことから

　　g(a,sum(as))=　sum(cons(a,as))=a+sum(as)　　(even(a)=trueの時)
　　　　　　　　　　{　sum(as)　　　　　　　　　　　　　　(それ以外)
が成り立てば良いので,
　　　　∵③式の右の要素が等しいから　p適用後sum適用つまり、sum(p(a,as))　＝sum適用後ｇ適用つまり　g(a､sum(as))　ということか

g(a,x)=　　　a+x　(even(a)=trueの時）
　　　　　{　　x　　　(それ以外)
とすれば良いです。すなわち(|[0,g]|)=foldr(g,0)が求める関数です。