テンソル強度の証明図とストリング図

モナドのテンソル強度からペアリングを作って、それが結合法則や単位法則を満たすことを証明するには、ストリング図が一番だが、ストリング図に入る前に等式を変形する前処理が必要になる。

ひとつの前処理は、対象aを (+a) := λx.(x + a) （Haskellのセクション記法借用）という関手に変換すること。もうひととは、 (+Fa) を +a;F に直すこと。ここで早速にテンソル強度を使うことになる。

 +(Fa)  λx.(x + Fa)

 -------------------

 +a;F   λx.F(x + a)

対象 Fa + Fb + Fc は +(Fa + Fb + Fc) という関手になるが、次のように変形できる。

   +(Fa + Fb + Fc)

  ------------------

   +(Fa);+(Fb);+(Fc)

  ------------------

   +a;F ; +b;F ; +c;F

(+a) と a を同一視、図式順結合を単なる併置にすると、 a F b F c F と書ける。ここからスタートすれば、ペアリングの結合律は容易に示せる。

この前処理が思いつかなくて、なかなか絵算に持ち込めなかったのだった。この場合は、本番計算よりは前処理のほうが重要つうかキモ。