日々の流転

λ. CPO圏で始代数が存在しないための条件

CPO圏CとCPO関手F:C→Cを考える。 もしCに非正格な t:1→E と自然変換 ε: F→Id が存在するならば、 Fの始代数は存在しない。

証明

任意の e: 1→E と φ: FX→X とについて、 (e o !) : X→E は φ: FX→X から ε_E: FE→E への準同型になっていることがわかる。

ここで t:1→E は非正格なので、少なくとも二つの異なる準同型が存在する。

1. t o ! = t o ⊥_{X→1} ≠ ⊥_{X→E}
2. ⊥_{1→E} o ! = ⊥_{X→E}

よって、φは始代数では有り得ない。

具体例

• Fがcomonadの場合
  • 直積 F(X) = A×X
  • 恒等関手 Id
  • ストリーム Stream(A) = νX. A×X
• (constant) exponential functor F(X) = A⇒X
  • a: 1→A を適当に選べば、自然変換 ev o <id_{A⇒X}, a o !> : FX→X が得られるので、条件を満たす。

疑問

これは十分条件だけど、この方向で必要十分条件は存在するか?

適用例 (1)

Haskellでは以下のような product comonad を考えることがある。

class Functor w => Comonad w where
  extract   :: w a -> a
  duplicate :: w a -> w (w a)
  extend    :: (w a -> b) -> (w a -> w b)

  extend f  = fmap f . duplicate
  duplicate = extend id

instance Comonad ((,) a) where
  extract   (c,x) = x
  duplicate (c,x) = (c,(c,x))

もし (A,B) を厳密に(A×B)_⊥と解釈すると、以前の議論から F(X) = (A×X)_⊥ には始代数が存在し、背理法により extract :: (a,x) -> x は自然変換ではないことになる。したがって、この場合には厳密にはcomonadになっていない。

適用例 (2)

Akihito Takano と Erik Meijer の Short-cut deforestation in Calculational Form では F代数を正格な FA→A と定義していて、始代数が存在すると言っているが、これは誤り。代数を正格に制限しても、準同型は正格なものに制限されていないので、前述のような関手に対しては始代数が存在しない。

しかし、Erik Meijer は Program Calculation Properties of Continuous Algebras では準同型も正格なものに制限してたはずなのに、この論文ではどうしてやめたんだろうね。

λ. 多相関数≠自然変換

多相関数が自然変換にならないことがあるというのは、漠然と知ってはいたけど、実際に直面してみると嫌らしいな。以前は yoriyukiさんの「Haskellは複雑すぎる気がする」という意見に同意できなかったけど、今なら完全に同意出来るよ(苦笑)

λ. 自然変換 ε: F→Id の性質

幾つかメモ。

ε_X: FX→X は正格

⇒ (⊥ o !) is strict
⇔ (ε_X o F⊥) is strict
⇒ ε_X is strict

したがって、任意のXについて ε_X は正格。

F は非正格性を保存

f: X→Yとする。

Ff is strict
⇒ (ε_Y o Ff) is strict
⇔ (f o ε_X) is strict
⇒ f is strict

対偶をとって「f is not strict ⇒ Ff is not strict」。

λ. CPO圏での自然変換の性質

上記の ε: F→Id についての話はもう少し一般化できるか。

α: F→G を自然変換とする。

正格性

α_X is strict
⇒ G⊥ o α_X is strict
⇔ α_Y o F⊥ is strict
⇒ α_Y is strict

よって「任意のXについて α_X は正格」もしくは「任意のXについて α_X は非正格」。

αとFfがstrictならGfも正格

αが正格だとする。

Ff is strict
⇒ α_Y o Ff is strict
⇔ Gf o α_X is strict
⇒ Gf is strict