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

日々の流転


2006-06-14 [長年日記]

λ. 融合変換の簡単な例

N = μX.1+X として、double = fold [zero, succ.succ] : N -> N という関数があったときに、double . double を融合することを考える。double は (N, [zero,succ]) から (N, [zero, succ.succ]) への準同型であると同時に、(N, [zero, succ.succ]) から (N, [zero, succ.succ.succ.succ]) への準同型でもあるので、double . double = fold [zero, succ.succ.succ.succ] であり、これが目指す結果である。

\xymatrix@+40pt{ 1+{\mathbb N} \ar[d]|{[\mbox{zero},\mbox{succ}]} \ar[r]^{\mbox{id}_1+\mbox{double}} \ar@{}[dr]|*++{\Huge \circlearrowleft} & 1+{\mathbb N} \ar[d]|{[\mbox{zero},\mbox{succ}^2]} \ar[r]^{\mbox{id}_1+\mbox{double}} \ar@{}[dr]|*++{\Huge \circlearrowleft} & 1+{\mathbb N} \ar[d]|{[\mbox{zero},\mbox{succ}^4]} \\ {\mathbb N} \ar[r]_{\mbox{double}} & {\mathbb N} \ar[r]_{\mbox{double}} & {\mathbb N} }

具体的にどう変換するか。 doubleを(N, [zero, succ.succ]) からの準同型にするような代数を探すのは中々面倒だけど、ここでは double = build (λ[z,s]. fold [z, s . s]) が成り立っているので、以下のように変換することができる。

double . double
= fold [zero, succ . succ] . build (λ[z,s]. fold [z, s . s])
= { fold/build shortcut deforestation }
  fold [zero, (succ . succ) . (succ . succ)]
= fold [zero, succ . succ . succ . succ]

なお、ここでのbuildは以下で定義される関数である。

build : (∀X. (1+X -> X) -> X) -> N
build h = h [zero, succ]

関連エントリ

Tags: 圏論
本日のツッコミ(全2件) [ツッコミを入れる]
ψ たけを (2006-06-15 07:01)

succ . succ って「2を足す」…? いや、本質的ではないんですが。

ψ たけを (2006-06-15 07:29)

ああ、いいのか。後者関数 を succ.succ に置き換えたのが double なんですね。(ってそう書いてるジャマイカ)