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} }](tex/d8a3235d27256b16ef1b5b8ca1c4ee59.png "\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]
succ . succ って「2を足す」…？ いや、本質的ではないんですが。
ああ、いいのか。後者関数 を succ.succ に置き換えたのが double なんですね。（ってそう書いてるジャマイカ）