日々の流転

λ. 第二十二回圏論勉強会

今日は圏論勉強会だった。写真

今回はかつてない人数で驚いたが、とても楽しかった。

p.334 Exercise 3:

元の問題の意図に沿う方法はともかく、とりあえずparamorphismの概念を使って示しておく。paramorphismの定義と一意性の証明については Categorical programming with inductive and coinductive types を参照せよ。

(N, [0,s])を自己関手 F(X)=1+X の始代数とする。

f₀: A→Y と h: N×A×Y→Y を使って以下を定義する。

• f₀´: 1→Y^A
• h´ = λf,n. λa. h(n,a,f(a)) : Y^A×N→Y^A
• φ = [f₀´, h´] : F(Y^A×N)→Y^A

すると、f ∘ [0,s] = φ ∘ F <f,id> を満たす f : N→Y^A が一意に存在する(この f がparamorphismで <|φ|> などと書く)。この等式を展開すると、

• f∘0 = f₀´
• f∘s = h´∘<f,id>

となり、これは大雑把に解釈すると

• f(0,a) = f₀(a)
• f(n+1,a) = h´(f(n),n)(a) = h(n,a,f(n,a))

ということを表しているので、目的の関数fは一意に存在する。