2005-03-08 [長年日記]
λ. Hylomorphisms
関手Tの始代数 (μT,in) が存在して、 (μT,in-1) が終余代数 (νT,out) になっているとする。 すると、T余代数 (A,ψ) から得られる関数 unfold(ψ):A→νT と、 T代数 (B,φ) から得られる関数 fold(φ):μT→B を合成して、 fold(φ) ∘ unfold(ψ): A→B という関数を定義できる。 これを hylomorphism と呼び、 しばしば 〚φ,ψ〛T と書かれる。
Program Calculation Properties of Continuous Algebras, Maarten M Fokkinga and Erik Meijer には、hylo の語源について次のように書いてあった。
The prefix hylo- comes from the Greek ύλη
meaning “matter”, after the Aristotelian philosophy that form
and matter(= data) are one.
(In conjuction with -morphism the vowel η changes into ο .)
ちなみに、日本語では、ύλη は「質料」と訳されているようだ。「質料」「形相」等で検索するとアリストテレス哲学に関する記述が沢山見つかる。
[2005-03-27 追記] WikiPedia: hylomorphism には以下のように書いてあった。
Hylomorphism (Greek υλο- hylo-,
"wood, matter" + -morphism < Greek -μορφη, morph, "form") is a philosophy that
highlights the significance of matter in the structure of being, regarding matter as important (or even more so) as form.
Hylomorphism served as a useful tool in medieval philosophy from (at least) Avicebron to (at least) Thomas Aquinas.
λ. Hylomorphismと不動点コンビネータ
以下のように図式を張り合わせると、この関数 fold(φ) ∘ unfold(ψ): A→B は x = φ ∘ Tx ∘ ψ の解の一つであることがわかる。
![\xymatrix@+25pt{
A \ar[d]_{\psi} \ar[r]^{\mbox{unfold}_T(\psi)} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu T = \mu T} \ar@<-1ex>[d]_{\mbox{out}_T} \ar[r]^{\mbox{fold}_T(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& B
\\
TA \ar[r]_{T(\mbox{unfold}_T(\psi))}
& T{\nu T} = T{\mu T} \ar@<-1ex>[u]_{\mbox{in}_T} \ar[r]_{T(\mbox{fold}_T(\phi))}
& TB \ar[u]_{\phi}
}](tex/38b55cc8435f305118b1d65102974517.png "\xymatrix@+25pt{
A \ar[d]_{\psi} \ar[r]^{\mbox{unfold}_T(\psi)} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu T = \mu T} \ar@<-1ex>[d]_{\mbox{out}_T} \ar[r]^{\mbox{fold}_T(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& B
\\
TA \ar[r]_{T(\mbox{unfold}_T(\psi))}
& T{\nu T} = T{\mu T} \ar@<-1ex>[u]_{\mbox{in}_T} \ar[r]_{T(\mbox{fold}_T(\phi))}
& TB \ar[u]_{\phi}
}")
一方、cartesian closed でかつ不動点コンビネータが存在するのなら、fix(λf. φ ∘ Ff ∘ ψ) *1 によって別の解を定義することが出来る。この二つは等しいか?
homsetがCPOでかつ合成が正格かつ連続で不動点コンビネータが最小不動点を返すならば、等しいことは簡単に言える。α,β,γを次のように定義する。
- α(f) = φ ∘ Tf ∘ in-1
- β(f) = out-1 ∘ Tf ∘ ψ
- γ(f) = φ ∘ Tf ∘ ψ
すると、
- fold(φ) = ∨n<ω αn(⊥μT→B)
- unfold(ψ) = ∨n<ω βn(⊥A→νT)
- fix(λf. φ ∘ Ff ∘ ψ) = ∨n<ω γn(⊥A→B)
であり、帰納法によって αn(⊥μT→B) ∘ βn(⊥A→νT) = γn(⊥A→B) が証明でき、合成は連続なので fold(φ) ∘ unfold(ψ) = fix(λf. φ ∘ Ff ∘ ψ) が言える。
*1 CCCの射としてちゃんと書くのは面倒なのでラムダ式で書いておく
λ. Hylo Shift Law
自然変換 η: F→G に対して、
μη = foldF(inG ∘ ημG): μF→μG
と定義する。すると、foldF(φ ∘ ηB) = foldG(φ) ∘ μη が成り立つ。
![\xymatrix@+25pt{
F(\mu F) \ar[r]^{F(\mu\eta)} \ar[dd]_{\mbox{in}_F} \ar@{}[ddr]|*++{\circlearrowleft}
& F(\mu G) \ar[r]^{F(\mbox{fold}_{G}(\phi))} \ar[d]_{\eta_{\mu G}} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\eta_B}
\\
& G(\mu G) \ar[r]^{G(\mbox{fold}_G(\phi))} \ar[d]_{\mbox{in}_G} \ar@{}[dr]|*++{\circlearrowleft}
& GB \ar[d]^{\phi}
\\
\mu F \ar[r]_{\mu\eta}
& \mu G \ar[r]_{\mbox{fold}_G(\phi)}
& B
}](tex/7696115a83b967ba6e064066bbde7405.png "\xymatrix@+25pt{
F(\mu F) \ar[r]^{F(\mu\eta)} \ar[dd]_{\mbox{in}_F} \ar@{}[ddr]|*++{\circlearrowleft}
& F(\mu G) \ar[r]^{F(\mbox{fold}_{G}(\phi))} \ar[d]_{\eta_{\mu G}} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\eta_B}
\\
& G(\mu G) \ar[r]^{G(\mbox{fold}_G(\phi))} \ar[d]_{\mbox{in}_G} \ar@{}[dr]|*++{\circlearrowleft}
& GB \ar[d]^{\phi}
\\
\mu F \ar[r]_{\mu\eta}
& \mu G \ar[r]_{\mbox{fold}_G(\phi)}
& B
}")
同様に νη = unfoldG(ηνF ∘ outF): νF→νG と定義すると、unfoldG(ηA ∘ ψ) = νη ∘ unfoldF(ψ) が成り立つ。
T∈{F,G} について (μT,in-1)=(νT,out) ならば、μη=νη となるので、foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ μη ∘ unfoldF(ψ) = foldG(φ) ∘ νη ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(ηA ∘ ψ) が言える。
この等式 foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(ηA ∘ ψ) によって、自然変換ηを移動させることが出来る。これを Hylo Shift Law と呼ぶ。
λ. Hylomorphismの三つ組み表現 (Hylomorphisms in triplet form)
Hylo Shift Law によって自然変換を自由に移すことが出来るので、foldF(φ ∘ ηB) ∘ unfoldF(ψ) = foldG(φ) ∘ unfoldG(ηA ∘ ψ) を φ: GB→B, η: F→G, ψ:A→FA の三つ組みによって 〚φ,η,ψ〛G,F: A→B と表すことがある。
λ. 酸性雨定理 (Acid Rain Theorem)
パラメトリシティを仮定すると、
- C→μF ≅ C→(∀X.(FX→X)→X) ≅ ∀X.(FX→X)→(C→X)
- νF→C ≅ (∃X.(X→FX)×X)→C ≅ ∀X.(X→FX)→(X→C)
が成り立つのだが、 それぞれの右辺の型にパラメトリシティを適用することで以下を導ける。
- Acid Rain : Catamorphism
- ∀g:∀X.(FX→X)→(C→X), φ:FA→A. fold(φ) ∘ (gμF inF) = gA(φ)
- Acid Rain : Anamorphism
- ∀h:∀X.(X→FX)→(X→C), φ:A→FA. (hνF outF) ∘ unfold(φ) = hA(φ)
これらを酸性雨定理と呼ぶそうだ。
パラメトリシティを仮定すると色々な事が言えてとても楽しいのだけど、不動点コンビネータやseqの存在と相性が悪いという問題がある。
λ. Cata-HyloFusion / Hylo-AnaFusion
τ:∀A.(FA→A)→(FA→A) にパラメトリシティを適用すると、
∀A,φ:FA→A,B,ψ:FB→B,h:A→B. (h ∘ φ = ψ ∘ Fh) ⇒ (h ∘ τA(φ) = τB(ψ) ∘ Fh) が言える。ここで、fold(ψ) ∘ in = ψ ∘ F(fold(ψ)) なので、fold(ψ) ∘ τμF(in) = τB(ψ) ∘ F(fold(ψ)) 。
universality (cata-fusion) により、
fold(ψ) ∘ fold(τμF in) = fold(τB ψ) 。
![\xymatrix@+30pt{
{F\mu F} \ar[d]_{\mbox{in}} \ar[r]^{F(\mbox{fold}(\tau_{\mu F}\mbox{in}))} \ar@{}[dr]|*++{\circlearrowleft}
& {F\mu F} \ar[d]|{\tau_{\mu F} \mbox{in}} \ar[r]^{F(\mbox{fold}(\psi))} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\tau_B \psi}
\\
{\mu F} \ar[r]_{\mbox{fold}(\tau_{\mu F}\mbox{in})}
& {\mu F} \ar[r]_{\mbox{fold}(\psi)}
& B
}](tex/39dabfd4955261a1ae3719c0028a59dc.png "\xymatrix@+30pt{
{F\mu F} \ar[d]_{\mbox{in}} \ar[r]^{F(\mbox{fold}(\tau_{\mu F}\mbox{in}))} \ar@{}[dr]|*++{\circlearrowleft}
& {F\mu F} \ar[d]|{\tau_{\mu F} \mbox{in}} \ar[r]^{F(\mbox{fold}(\psi))} \ar@{}[dr]|*++{\circlearrowleft}
& FB \ar[d]^{\tau_B \psi}
\\
{\mu F} \ar[r]_{\mbox{fold}(\tau_{\mu F}\mbox{in})}
& {\mu F} \ar[r]_{\mbox{fold}(\psi)}
& B
}")
同様に、σ:∀A.(A→FA)→(A→FA) にパラメトリシティを適用すると、
∀A,φ:A→FA,B,ψ:B→FB,h:A→B. (Fh ∘ φ = ψ ∘ h) ⇒ (Fh ∘ σA(φ) = σB(ψ) ∘ h)
が言える。
ここで、out ∘ unfold(φ) = F(unfold(φ)) ∘ φ なので、F(unfold(φ)) ∘ σA(φ) = σνF(out) ∘ unfold(φ)。
universality (ana-fusion) により、
unfold(σνF out) ∘ unfold(φ) = unfold(σA φ) 。
![\xymatrix@+30pt{
A \ar[d]_{\sigma_A \phi} \ar[r]^{\mbox{unfold}(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& {F\nu F} \ar[d]|{\sigma_{\nu F} \mbox{out}} \ar[r]^{\mbox{unfold}(\sigma_{\nu F}\mbox{out})} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu F} \ar[d]^{\mbox{out}}
\\
FA \ar[r]_{F(\mbox{unfold}(\phi))}
& {F\nu F} \ar[r]_{F(\mbox{unfold}(\sigma_{\nu F}\mbox{out}))}
& {F\nu F}
}](tex/e27585ac30ad32e6b24bd7722c3d54c4.png "\xymatrix@+30pt{
A \ar[d]_{\sigma_A \phi} \ar[r]^{\mbox{unfold}(\phi)} \ar@{}[dr]|*++{\circlearrowleft}
& {F\nu F} \ar[d]|{\sigma_{\nu F} \mbox{out}} \ar[r]^{\mbox{unfold}(\sigma_{\nu F}\mbox{out})} \ar@{}[dr]|*++{\circlearrowleft}
& {\nu F} \ar[d]^{\mbox{out}}
\\
FA \ar[r]_{F(\mbox{unfold}(\phi))}
& {F\nu F} \ar[r]_{F(\mbox{unfold}(\sigma_{\nu F}\mbox{out}))}
& {F\nu F}
}")
この二つを hylomorphism を使った形で表現すると、以下を得る。
- Cata-HyloFusion
- τ: ∀A.(FA→A)→FA→A ⇒ 〚φ,η1,outF〛G,F ∘ 〚τ(inF),η2,ψ〛F,H = 〚τ(φ ∘ η1),η2,ψ〛F,H
- Hylo-AnaFusion
- σ: ∀A. (A→FA)→A→FA ⇒ 〚φ,η1,σ(outF)〛G,F ∘ 〚inF,η2,ψ〛F,H = 〚φ,η1,σ(η2 ∘ ψ)〛G,F
……と、ここまで書いてきて気づいたのだけど、酸性雨定理から証明できるな。
λ. fold/build shortcut deforestation
パラメトリシティを仮定すると C→μF ≅ ∀X.(FX→X)→(C→X) が成り立つと上で書いた。 この同型は具体的には次の関数で表現される。
-
build : (∀X.(FX→X)→(C→X)) → (C→μF)
build g = gμF inF -
unbuild : (C→μF) → (∀X.(FX→X)→(C→X))
unbuild f = ΛX. λφ. foldX(φ) ∘ f
したがって、関数 f: C→μF を build g の形で書いておけば foldX(φ) ∘ f = foldX(φ) ∘ build g = (unbuild (build g))X φ = gX φ という書き換えが出来る。 これは酸性雨定理からも明らか。
リストの場合については、GHC等のHaskellコンパイラで最適化のために広く使われている。以下はGHC.Baseから引用。
foldr :: (a -> b -> b) -> b -> [a] -> b foldr k z xs = go xs where go [] = z go (y:ys) = y `k` go ys build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a] build g = g (:) [] {-# RULES "fold/build" forall k z (g::forall b. (a->b->b) -> b -> b) . foldr k z (build g) = g k z #-}
λ. destroy/unfold shortcut deforestation
パラメトリシティを仮定すると νF→C ≅ ∀X.(X→FX)→(X→C) が成り立つと上で書いた。 この同型は具体的には次の関数で表現される。
-
destroy : (∀X.(X→FX)→(X→C)) → (νF→C)
destroy h = hνF outF -
undestroy : (νF→C) → (∀X.(X→FX)→(X→C))
undestroy f = ΛX. λφ. f ∘ unfoldX(φ)
したがって、関数 f: νX→C を destroy h の形で書いておけば、 f ∘ unfoldX(φ) = destroy h ∘ unfoldX(φ) = (undestroy (destroy h))X φ = hX φ という書き換えが出来る。 これは酸性雨定理からも明らか。
リストの場合、destroy/unfoldr として知られているものになる。
unfoldr :: (b -> Maybe (a,b)) -> b -> [a] unfoldr phi b = case phi b of Just (a,b') -> a : unfoldr phi b' Nothing -> [] destroy :: (forall b. (b -> Maybe (a,b)) -> b -> c) -> [a] -> c destroy g = g psi where psi [] = Nothing psi (a:as) = Just (a, as)
