僕が使っている計算法：絵算と図式順記法

僕は、「リストモナドの結合律を書き下せ」とか言われても絶対にできません。だって、まったく憶えてないし、憶える努力をしても僕にはとうてい憶えられるシロモノではないからです。

でも、ナプキンペーパーとボールペン（できれば3色）が与えられて、しかも気分と調子がいいときなら、数分後には次のような結果を出せると思います。

リストモナドの結合律は次の通り。

• lislislis∈List<List<List<X>>> に対して、
  List.flatten<X>(List.map(List.flatten<X>)(lislislis)) = List.flatten<X>(List.flatten<List<X>>(lislislis))

気分と調子がいいときの僕が、ナプキンペーパーとボールペンでどういう計算をするかを紹介しましょう。まずは、僕がなんで普通の計算をしないのか／できないのかの理由から。

絵を使うしか方法がない

とにかく憶えられない！ 老化で記憶力が減退した、という事情もあるんでしょうが、そもそも僕は生まれつき記憶力が極端に悪いのです。特に、数字やアルファベットの羅列を記憶することが苦手なのは病的で、日常生活にも随分と不都合がありました。当然に、長い公式を暗記するなんてことは絶望的に不可能です。

じゃ、なんかの直観やひらめきがあるこというと、そんなことも全然ないので、2桁の整数の足し算から自然変換の縦横結合まで、僕が「計算」を間違わずに遂行するのは困難を極めます。

記憶力もひらめきもない人間*1が普通に計算を行うには、普通とは違うツールが必要です。そのツールが -- 圏論計算に限定されますが -- 僕の場合は絵算（pictorial/graphical/diagrammatic calculation）です。

絵算自体は、既に知られた手法なので僕のオリジナリティはまったくありません。「絵算＜えざん＞」という訳語を考えて使っているところはオリジナルかもしれません ^^; 便利で強力な絵算ですが、次の問題があります。

• 絵をテキストとして書き下す、あるいはその逆方向の翻訳がかなりのストレス。
• うまく絵が描けないケースもある。このときは等式的計算をするしかない。

そこで、「絵算 ←→ テキストによる等式的計算」の翻訳がストレートに行えるように、図式順（左から右）を徹底した記法DOTN（Diagrammatic-Order Text Notation）を考えました。

DOTNの説明 http://www.chimaira.org/docs/DOTN.htm を書いた頃と多少変わってきたところもあります； 以前は、関手の結合、関手と自然変換の結合に「;;」を使っていましたが、「;;」が頻繁に登場するので、最近は演算記号なしの並置を使っています。つまり、「F;;G 」を「FG」、「F;;α, α;;F」を「Fα, αF」です。自然変換の横結合「α*β」も「αβ」と書くことが多いですね。混乱が生じそうなときは、明示的に演算記号を入れていますけど。

DOTNは象形文字みたいなもので、テキストによる表現を見て、直接的に（頭で考えずに）絵をイメージできます。要するに、「絵図 ←→ テキスト」の脳内変換の労力を最小化することを目的にした記法で、絵算の補助として利用するのです。

モノイドの結合律

モナドの結合律をDOTNで書くと：

• μF|μ = Fμ|μ

これは十分簡単な等式ですが、実は、僕はこれも憶えていません。

しかし、自然数N（普通は太字でNと書くが面倒なのでN）の足し算に関する結合律は、さすがに僕でも憶えてます。次のとおりです。

• 任意の n, m, k ∈N に対して、(n + m) + k = n + (m + k)

これを絵に描くと下のようになります。

N      N     N      N      N      N

 ＼  ／     ／       ＼     ＼  ／

   ＋     ／           ＼     ＋

    ＼  ／       ＝      ＼  ／

      ＋                   ＋

      ｜                   ｜

モナドもNと同様にモノイドなので、同じ絵が描けます。ただし、次のように置き換えます。

• 集合N ←→ 関手F
• 演算+ ←→ 自然変換μ

次がその絵図です。

F      F     F      F      F      F

 ＼  ／     ／       ＼     ＼  ／

   μ     ／           ＼     μ

    ＼  ／       ＝      ＼  ／

      μ                   μ

      ｜                   ｜

この絵の左辺を上下に分割します。

F      F     F

 ＼  ／     ／

   μ     ／  (1)

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

    ＼  ／    

      μ      (2)

      ｜      

(1)と書いてある段を横に見ていくと「μ F」（右のFは、Fとラベルされた線（ワイヤー）に出会ったことを表します、内容的には関手Fの恒等自然変換です）。(2)と書いてある段を見れば「μ」です。これらが横棒で上下に区切ってあります。上から下への絵図を、左から右へのテキストに変えて、横棒を縦棒に直すと：

• (μ F) | μ

同様にして右辺の図は：

• (F μ) | μ

これらを等号でつなげば、モナドの結合律です。縦棒より並置のほうが演算の優先度が高いので括弧は省略できます。余分な空白も入れなければ、μF|μ = Fμ|μ 。

結合律の成分表示

関手Fと自然変換αの結合 Fα, αF は再び自然変換で、関手Fの恒等自然変換をι_F、自然変換の横結合を *（スター）で表すと：

• Fα = ι_F*α
• αF = α*ι_F

DOTNでは、自然変換αのx成分を、α_x ではなくて x.α と書きます。対象xと関手Fの適用も x.F と書きます。この書き方で、Fα, αF の成分表示は次の自然な形式で与えられます。

• x.(Fα) = (x.F).α = x.F.α
• x.(αF) = (x.α).F = x.α.F

また、自然変換の縦結合 α|β の成分表示は次のとおり。

• x.(α|β) = (x.α);(x.β) = x.α ; x.β

以上の公式を組み合わせると、μF|μ = Fμ|μ の成分表示は次のようになります。

   x.(μF|μ)

 = x.(μF) ; x.μ

 = x.μ.F ; x.μ
   x.(Fμ|μ)

 = x.(Fμ) ; x.μ

 = x.F.μ ; x.μ
よって結合律は：

 x.μ.F ; x.μ = x.F.μ ; x.μ

世間に合わせる

DOTNと、世間でメジャーな記法との違いを列挙します。

• 圏の対象は小文字xではなくて、大文字Xで書くことが多い。
• x.μ ではなくて μ_X と書くことが多い。
• x.F ではなくて F(X) と書くことが多い。
• 射の結合は、f;g ではなくて、g・f と書くことが多い。

x.μ.F ; x.μ = x.F.μ ; x.μ をメジャーな記法に翻訳すると次のようになります。

• μ_X・F(μ_X) = μ_X・μ_F(X)

僕の感覚では、この翻訳結果は、記号上の対称性が崩れて汚くてイヤなんですが、まーいたしかたない。

Xが集合のとき、この等式は、FFF(X)→F(X) という関数に関する等式なので、集合 FFF(X) の要素をzとすると、次の等式が得られます。

• μ_X(F(μ_X)(z)) = μ_X(μ_F(X)(z))

リストモナド

関手F、自然変換μの具体例としてリストモナドを取り、プログラムっぽい記法で書き表すことにしましょう。

• F(X) -- 型構成子 List<X>
• F(f) -- マップ関数 List.map(f) : List<X>→List<Y> （f:X→Y）
• μ_X -- 平坦化関数 List.flatten<X> : List<List<X>>→List<X>

先に得られた一般的公式（結合律）をすぐ上の書き方で具体化すると：

μX(F(μX)(z))

  ‖ 具体化

  ∨

List.flatten<X>(List.map(List.flatten<X>)(lislislis))
μX(μF(X)(z))

  ‖ 具体化

  ∨

List.flatten<X>(List.flatten<List<X>>(lislislis))
よって、

  List.flatten<X>(List.map(List.flatten<X>)(lislislis)) 

= List.flatten<X>(List.flatten<List<X>>)(lislislis)

はい、これでリストモナドの結合律のでき上がり。

*1:理解力も不足しているらしい →http://d.hatena.ne.jp/m-hiyama/20090721/1248137196