foldr の融合則が一般の融合則から導ける件

Haskell Advent Calendar 2023 の12日目の記事です。

『関数プログラミング入門』（オーム社）などを読んでいると foldr や foldl の融合則というのが出てきます。たとえば foldr の融合則は次の形です。

foldr の融合則

-- 有限リスト xs と関数 f, g, h について、
-- h (f x y) = g x (h y) のとき以下が成り立つ：

h (foldr f e xs) = foldr g (h e) xs

この法則を使うとたとえばリストを2回分走査する計算を1回分にまとめることができたりして便利なわけです。

-- 例
foldr f a . map g = foldr (f . g) a

が、この法則の見た目がややこしいですし、条件部分 h (f x y) = g x (h y) も意味がよく分からないと思っていました。

これがもっと一般的な、より短い形から導けるということを知ってびっくりしたので、学んだことを復習する意味で共有したいと思います。

一般の融合則

それがこの形です

融合則

圏 $CC$ に始対象があるとき、始対象から対象 $AA$ への唯一の射を $!A!_{A}$ と書くと、射 $f:A→Bf : A \to B$ について以下が成り立つ

$$f ∘ !A = !B f \; \circ \; !_{A} \; = \; !_{B}$$

圏論の言葉にはなりましたが、式自体はすごく簡潔になりました。むりやり可換図式にするとこんな感じでしょうか（本当は三角形にしたかった）。

$$0→!AAid↓↓f0→!BB \begin{CD} 0 @>!_{A}>> A \\ @VidVV @VVfV \\ 0 @>!_{B}>> B \end{CD}$$

この融合則で圏 C を具体的に用意してあげると foldr の融合則になるわけです。私は一般の融合則を後から知ったので、foldr の融合則がこんな当たり前っぽい式から導けるんだということにむちゃくちゃ驚きました。

F-代数

そのための準備としてまず F-代数というものを用意します。F-代数 とは、圏 $CC$ と関手 $F:C→CF : C \to C$ について $X←F XX \gets F\,X$ の形をした射のことです。

また、F-代数の間の F-準同型 というものを考えます。F-代数 $X←F XX \gets F\;X$ から $Y←F YY \gets F\;Y$ への F-準同型 とは、射 $h:X→Yh : X \to Y$ であって以下を可換にするものです。

$$X←F Xh↓↓F hY←F Y \begin{CD} X @<<< F\;X \\ @VhVV @VVF\,hV \\ Y @<<< F\;Y \end{CD}$$

このとき、F-代数を対象とし、F-準同型を射とする圏を考えることができます。この圏に始対象があるとき、それを F-始代数 といいます。

リスト型 [A] を F-始代数 として定義する

いま、対象 $AA$ を固定して、対象 $XX$ と射 $ff$ に対して関手 $FF$ を次のように定義します。

$F X=1+A×XF\;X = 1 + A \times X$
$F f=id1+idA×fF\;f = id_{1} + id_{A} \times f$

ただし $11$ は終対象、$×\times$ と $++$ は積と余積です。このとき、この F についての代数に始代数が存在することが示されます。都合上それを $[A]←1+A×[A][A] \gets 1 + A \times [A]$ と書くことにすると、始代数から他の代数への可換図式は次のように書けます。

$$[A]←[nil, cons]1+A×[A]( ⁣∣e,f∣ ⁣)↓↓id1+idA×( ⁣∣e,f∣ ⁣)X←[e, f]1+A×X \begin{CD} [A] @<[nil,\,cons]<< 1 + A \times [A] \\ @V(\!|e,f|\!)VV @VVid_{1} + id_{A} \times (\!|e,f|\!) V \\ X @<[e,\,f]<< 1 + A \times X \end{CD}$$

ここで $[A][A]$ から $XX$ への射、つまり始対象からの射は $[e,f][e, f]$ に応じて1つに決まりますので、それを $( ⁣[e, f] ⁣)(\![ e, \, f ]\!)$ という記法で表しています。

ここまで始代数をまるでリスト型やその上の関数かのように [A] や nil や cons と書いていますが、そう書いてよいことは後で分かります。いま、この図の表す等式を書き下してみます。

$( ⁣∣e, f∣ ⁣)∘[nil, cons]=[e, f]∘(id1+idA×( ⁣∣e,f∣ ⁣))(\!| e,\,f |\!) \circ [nil,\,cons] = [e,\,f] \circ (id_{1} + id_{A} \times (\!|e,f|\!))$

これは次の2つの式に分解されます。

1. $( ⁣∣e, f∣ ⁣)∘nil=e∘id1(\!| e,\,f |\!) \circ nil = e \circ id_{1}$
2. $( ⁣∣e, f∣ ⁣)∘cons=f∘(idA×( ⁣∣e,f∣ ⁣))(\!| e,\,f |\!) \circ cons = f \circ (id_{A} \times (\!|e,f|\!) )$

ここで、もとになっている圏 C をたとえば集合と写像の圏とします。すると nil, cons, e, f は それぞれ次の形の写像になります。ただし $11$ は元を一つだけ持つ集合（一点集合）を表します。

$nil:1→[A]nil : 1 \to [A]$
$cons:A×[A]→[A]cons : A \times [A] \to [A]$
$e:1→Xe : 1 \to X$
$f:A×X→Xf : A \times X \to X$

ここで上の1番めの式より
　　$( ⁣∣e, f∣ ⁣)∘nil=e(\!| e,\,f |\!) \circ nil = e$
一点集合 $11$ の元を $()()$ として両辺に $()()$ を適用すると、
　　$(( ⁣∣e, f∣ ⁣)∘nil) ()=e ()((\!| e,\,f |\!) \circ nil) \; () = e \; ()$
左辺を計算して $nil ()nil \; ()$ を $nil‾\overline{nil}$、$e ()e \; ()$ を $e‾\overline{e}$ と書くと
　　$( ⁣∣e, f∣ ⁣) nil‾=e‾(\!| e,\,f |\!) \; \overline{nil} = \overline{e}$
となります。

また2番目の式の両辺に (x, xs) を適用して、
　　$(( ⁣∣e, f∣ ⁣)∘cons) (x,xs)=(f∘(idA×( ⁣∣e,f∣ ⁣))) (x,xs)((\!| e,\,f |\!) \circ cons) \; (x, xs) = (f \circ (id_{A} \times (\!|e,f|\!) )) \; (x, xs)$
左辺と右辺をそれぞれ計算して
　　左辺
　　$=(( ⁣∣e, f∣ ⁣)∘cons) (x,xs)= ((\!| e,\,f |\!) \circ cons) \; (x, xs)$
　　$=( ⁣∣e, f∣ ⁣) (cons (x,xs))= (\!| e,\,f |\!) \; (cons \; (x, xs))$
　　右辺
　　$=f ((idA×( ⁣∣e,f∣ ⁣)) (x,xs)= f \; ((id_{A} \times (\!|e,f|\!)) \; (x, xs)$
　　$=f (x,( ⁣∣e,f∣ ⁣) xs)= f \; (x, (\!|e,f|\!) \; xs)$
左辺 = 右辺の形に戻して
　　$( ⁣∣e, f∣ ⁣) (cons (x,xs))=f (x,( ⁣∣e,f∣ ⁣) xs)(\!| e,\,f |\!) \; (cons \; (x, xs)) = f \; (x, (\!|e,f|\!) \; xs)$

まとめると

$( ⁣∣e, f∣ ⁣)(\!| e,\,f |\!)$ が満たす式

$( ⁣∣e, f∣ ⁣) nil‾=e‾(\!| e,\,f |\!) \; \overline{nil} = \overline{e}$
$( ⁣∣e, f∣ ⁣) (cons (x,xs))=f (x,( ⁣∣e,f∣ ⁣) xs)(\!| e,\,f |\!) \; (cons \; (x, xs)) = f \; (x, (\!|e,f|\!) \; xs)$

となりますが、これを foldr の定義

foldr f e [] = e
foldr f e (x:xs) = f x (foldr f e xs)

と見比べると、 $( ⁣∣e,f∣ ⁣)(\!|e,f|\!)$ は foldr f e と同じ意味だと分かります。同様に、$nil‾\overline{nil}$ は [] と、$conscons$ は : と、$[A][A]$ は [a] と同じ意味ということになります。

foldr の融合則を導く

さきほどのF-代数の圏に融合則を適用します。次の可換図式で、

$$[A]←[nil, cons]1+A×[A]( ⁣∣e,f∣ ⁣)↓↓id1+idA×( ⁣∣e,f∣ ⁣)X←[e, f]1+A×Xh↓↓id1+idA×hY←[d, g]1+A×Y \begin{CD} [A] @<[nil,\,cons]<< 1 + A \times [A] \\ @V(\!|e,f|\!)VV @VVid_{1} + id_{A} \times (\!|e,f|\!) V \\ X @<[e,\,f]<< 1 + A \times X \\ @V h VV @VVid_{1} + id_{A} \times h V \\ Y @<[d,\,g]<< 1 + A \times Y \\ \end{CD}$$

一番上の $[A]←1+A×[A][A] \gets 1 + A \times [A]$ は始対象ですから、融合則は $h ∘ ![e,f] = ![d,g]h \; \circ \; !_{[e, f]} \; = \; !_{[d, g]}$ の形になります。$![e,f]!_{[e, f]}$ はつまり $( ⁣∣e,f∣ ⁣)(\!|e,f|\!)$ のことなので、

$h∘( ⁣∣e,f∣ ⁣)=( ⁣∣d,g∣ ⁣)h \circ (\!|e,f|\!) = (\!|d,g|\!)$

となります。また、下側の四角形の可換性を書き下すと次のようになります。

$h∘[e,f]=[d,g]∘(id1+idA×h)h \circ [e, f] = [d, g] \circ (id_{1} + id_{A} \times h)$

これは次の2つの式に分解されます。

1. $h∘e=d∘id1h \circ e = d \circ id_{1}$
2. $h∘f=g∘(idA×h)h \circ f = g \circ (id_{A} \times h)$

1番の式から $d=h∘ed = h \circ e$ であることが分かるので、融合則は結局

$h∘( ⁣∣e,f∣ ⁣)=( ⁣∣h∘e,g∣ ⁣)h \circ (\!|e,f|\!) = (\!|h \circ e,g|\!)$

となります。前と同様に集合と写像の圏だと思って両辺に xs を適用すると
左辺
　　$=(h∘( ⁣∣e,f∣ ⁣)) xs= (h \circ (\!|e,f|\!)) \; xs$
　　$=h(( ⁣∣e,f∣ ⁣) xs)= h ((\!|e,f|\!) \; xs)$
右辺
　　$=( ⁣∣h∘e,g∣ ⁣) xs= (\!|h \circ e,g|\!) \; xs$
左辺 = 右辺の形に戻して
　　$h (( ⁣∣e,f∣ ⁣) xs)=( ⁣∣h∘e,g∣ ⁣) xsh \; ((\!|e,f|\!) \; xs) = (\!|h \circ e,g|\!) \; xs$

2番の式でも同様に両辺に (x, y) を適用すると
左辺
　　$=(h∘f) (x,y)= (h \circ f) \; (x, y)$
　　$=h (f (x,y))= h \; (f \; (x, y))$
右辺
　　$=(g∘(idA×h)) (x,y)= (g \circ (id_{A} \times h)) \; (x, y)$
　　$=g ((idA×h) (x,y))= g \; ((id_{A} \times h) \; (x, y))$
　　$=g (x,h y)= g \; (x, h \; y)$
左辺 = 右辺の形に戻して
　　$h (f (x,y))=g (x,h y)h \; (f \; (x, y)) = g \; (x, h \; y)$

まとめると

融合則から導かれる式

$h (( ⁣∣e,f∣ ⁣) xs)=( ⁣∣h∘e,g∣ ⁣) xsh \; ((\!|e,f|\!) \; xs) = (\!|h \circ e,g|\!) \; xs$
ただし以下を満たすとき
$h (f (x,y))=g (x,h y)h \; (f \; (x, y)) = g \; (x, h \; y)$

となりますが、これは $( ⁣∣e,f∣ ⁣)(\!|e,f|\!)$ が foldr f e だったことを思い出すと、冒頭の foldr の融合則

h (foldr f e xs) = foldr g (h e) xs
-- ただし以下を満たすとき
h (f x y) = g x (h y)

と同じ意味であることが分かります。

まとめ

翻って考えると、foldr の融合則の条件 h (f x y) = g x (h y) は h が準同型という意味だったんですね。実のところまだよく分かってないのですが、前よりはイメージがつかめた気がします。

参考文献

圏論勉強会：第7回 @ワークスアプリケーションズ（中村晃一）
http://nineties.github.io/category-seminar/7.html

「代数的データ型」以降のページで、上の内容のほとんどがより丁寧に書かれています。本記事でやったのはリストの catamophism の融合則が foldr の融合則と一致することを具体的に確かめたことだけです。

『関数プログラミング入門』（オーム社）
『Algorithm Design With Haskell』（Cambridge University Press）

foldr の融合則についてはこの本で知りました。