1. rinse_

    Posted

    rinse_
Changes in title
+おじいさん、今日のご飯はAnamorphismですよ
Changes in tags
Changes in body
Source | HTML | Preview

$\require{AMScd}$

昨日のご飯 -> おじいさん、今日のご飯はCatamorphismですよ

昨日のCatamorphismに引き続き、F余代数から出発して、Anamorphismを理解することを目指します。

F余代数

ある関手Fに対して、対象と射の組 $(A, a : A \rightarrow F(A))$ のこと。名前の通り、F代数の双対。

\begin{CD}
A @>a>> F(A)
\end{CD}

Haskellで書くと、

type Coalgebra f a = a -> f a

F余代数の準同型

ある2つのF余代数 $(A, a)$, $(B, b)$ に対して、 $a \circ f = F(f) \circ b$ を満たす射 $f : B \rightarrow A$ のこと。
可換図式を見ると、F代数の準同型のそれと比べて矢印の向きが全て反転していることがわかる。

\begin{CD}
F(A) @<a<< A \\
@AF(f)AA @AfAA \\
F(B) @<b<< B
\end{CD}

F終余代数

任意のF余代数 $(X, \varphi)$ への準同型が一意に定まる特別なF余代数。F終余代数の対象を特に終対象と呼ぶ。
ここで、$(T, t)$ がF終余代数であるならば、 $T \simeq F(T) $ ということが知られている1。つまり、任意のF余代数 $(X, \varphi)$ に対して以下の可換図式が成り立つ。

\begin{CD}
F(T) @<t<< T \\
@AF(f)AA @AfAA \\
F(X) @<\varphi<< X
\end{CD}

Haskellで書くと、

newtype Fix f = InF { outF :: f (Fix f) }

Fix fが終対象$T$に, outFが可換図式の射 $t : T \rightarrow F(T)$ に相当する。InF は $t$ の逆射 $t^{-1} : F(T) \rightarrow T$ である。
名前の由来は終対象 $T$ が関手 $F$ の最大不動点であることから。

おや、このFix f昨日のご飯の献立に出てきたFix fと全く同じものだ。

\begin{CD}
F(Fix(F)) \overset{inF}{\underset{outF}{\rightleftarrows}} Fix(F)
\end{CD}

Haskellでは、ある関手 $F$ に対するF始対象とF終余対象は同じ型 Fix fで表すことができるのである。

Anamorphism

上の可換図式で、射 $f$ は任意のF余代数 $(X, \varphi)$ からF終余代数への準同型である。これをAnamorphismと呼ぶ。
関手 $F$ におけるF終余対象が関手 $F$の 不動点であることを強調するために、上図 $T$ を $Fix(F)$ に置き換えた図を示す。

\begin{CD}
F(Fix(F)) @<outF<< Fix(F) \\
@AF(ana(\psi))AA @Aana(\psi)AA \\
F(X) @<\psi<< X
\end{CD}

Haskellで書くと、

ana :: Functor f => (a -> f a) -> a -> Fix f
ana psy = InF . fmap (ana psy) . psy

可換図式の見方はcataのときと同様だ。Haskellの実装は、可換図式を左側からぐるっと回り込むようなイメージでされている。
inFは $outF$ の逆射で、F終余代数の性質 $Fix(F) \simeq F(Fix(F)) $ より得られる。

\begin{CD}
ana(\psi) = X @>\psi>> F(X) @>F(ana(\psi))>> F(Fix(F)) @>inF>> Fix(F)
\end{CD}

プログラミングにおける意義

Catamorphismはプログラミングにおける畳込み処理と対応していた。Anamorphismの場合はどうだろう。
Fix fが何らかの再帰的構造を表していた(Fix f = f (Fix f) = f (f (Fix f)))ことを思い出すと、ある一つの から再帰的な構造を作り出す何かだと想像できる。再帰的構造を一つの値に潰すfoldは想像がつきやすいが、一つの値から再帰的構造を作るとは一体どういうことなのだろうか?

これをリストに特殊化した関数がHaskellではunfoldrとして提供されている。anaとは似ても似つかない外見だ。

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]

これを見ると、ある bからある値aと次項のための種bを得ることを再帰的に繰り返し、得られた値全て[a]を返す関数のようだ。あまり見慣れない関数なので、使用例を見てみよう。

>>> iota :: Int -> Maybe (Int, Int)
>>> iota n = Just $ (n, n + 1)
>>> unfoldr iota 0
[0,1,2,3,4,5,6,7,8,9,..]

>>> fib :: (Int, Int) -> Maybe (Int, (Int, Int))
>>> fib (m, n) = Just $ (m, (n, (m + n)))
>>> unfoldr f (0, 1)
[0,1,1,2,3,5,8,13,21,34,..]

>>> fiz :: Int -> Maybe (String, Int)
>>> fiz n
>>>     | n `mod` 15 == 0 = Just ("fizzbuzz", n + 1)
>>>     | n `mod` 3 == 0  = Just ("fizz", n + 1)
>>>     | n `mod` 5 == 0  = Just ("buzz", n + 1)
>>>     | otherwise = Just (show n, n + 1)
unfoldr fiz 1
["1","2","fizz","4","buzz","fizz","7","8","fizz","buzz","11","fizz","13","14","fizzbuzz",..]

一つ目は最もシンプルな例だ。種と値が共にIntで、初項0等差1の数列を作っている。
二つ目は種がタプルになっているが、これは初項を2つ渡しているというだけの話だ。お馴染みフィボナッチ数列である。
三つ目は値の方がStringだが、やっていることは一つ目と同じだ。fizzbuzzの無限リストを作っている。

少しunfoldrに慣れてきたところで、anaがこれとどう関係しているのかを確認してみよう。やり方はcataのときと同じだ。
$ListF_X = 1 + X \times Y$ という関手の不動点 $Fix(ListF_X)$ は、$List(X)$ と同型である。よって、関手 $List_X$ におけるAnamorphismはunfoldrと本質的に同じであるはずだ。

-- ListFx = 1 + X * Y
data ListF a b = Nil | Cons a b deriving (Functor)

-- ListFで特殊化したana
ana :: (b -> ListF a b) -> b -> Fix (ListF a)

もう一度unfoldrの型を確認しよう。

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]

cataの時と同じように、anaの型を同型を使って変形していき、最終的にunfoldrの型が得られることを確認しよう。

  1. Fix (ListF a) ~= [a]
    まずは、$ListF_X$の不動点がリスト$List$と同型であるので、そこから置き換えていく。

    ana :: (b -> ListF a b) -> b -> [a]
    
  2. ListF a b ~= Maybe (a, b)
    $ListF_X = 1 + X \times Y$ だった。
    (a, b)が $X \times Y$ 、Maybe aが $1 + X$ と対応する。

    ana :: (b -> Maybe (a, b)) -> b -> [a]
    

できた。

まとめ

F余代数を学ぶところから出発して、任意のF余代数からF終余代数への準同型であるAnamorphismを学んだ。また、これをHaskell上に表現したcataやそれを特殊化したunfoldrを使うとうまく数列や漸化式を表すことができることを確認した。

最後に、AnamorphismとCatamorphismの可換図式をくっつけてみよう。

\begin{CD}
F(X) @<\psi<< X \\
@VF(ana(\psi))VV @Vana(\psi)VV \\
F(Fix(F)) @<outF<< Fix(F) \\
@| @| \\
F(Fix(F)) @>inF>> Fix(F) \\
@VF(cata(\varphi))VV @Vcata(\varphi)VV \\
F(Y) @>\varphi>> Y
\end{CD}

おや、$X \rightarrow Y$ という射が見えるぞ。これはいったい何morphismなんだ……?

おじいさん、明日のご飯はhylomorphismですよ。