トップ «前の日記(2006-10-13) 最新 次の日記(2006-10-16)» 月表示 編集

日々の流転


2006-10-15 [長年日記]

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

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

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

p.334 Exercise 3:

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

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

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

  • f0´: 1→YA
  • h´ = λf,n. λa. h(n,a,f(a)) : YA×N→YA
  • φ = [f0´, h´] : F(YA×N)→YA

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

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

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

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

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

Tags: 圏論