こんな簡単なトレース付きモノイド圏があったなんて - 檜山正幸のキマイラ飼育記 (はてなBlog)

「こんな簡単な×××があったなんて」というタイトル、けっこう人目を惹きそうでしょ。でも「×××」が「トレース付きモノイド圏」じゃねぇー、誰も集まってこないわな。まーいいや。

内容：

GoI構成とInt構成
自然数の基本的な性質
自然数の順序から作る圏
自然数の足し算から作るモノイド圏
引き算で作る対称モノイド圏上のトレース

GoI構成とInt構成

GoI（Geometry of Interaction）なんてことを言い出したのは、線形論理の創始者ジラール（J.-Y. Girard）だと思います。GoI構成とは、トレース付きモノイド圏からコンパクト閉圏を作り出す操作です。GoI構成は別名Int構成とも呼びます。ジラールとは独立に同じ方法が発見され、Int構成と名付けられたのだと思います。Int構成の起源が誰なのかは知りません*1。

GoIは"Geometry of Interaction"の略記ですが、Intの語源はなんでしょう？ Integer -- 整数です。自然数から整数を構成するのと同じ方法なのでInt構成と呼ぶのですね。つまり、自然数はトレース付きモノイド圏で、整数はコンパクト閉圏なんです。

一度に説明するのは大変なので、まず今日は自然数の全体 {0, 1, 2, 3, ...} がトレース付きモノイド圏となることを説明します。正確に言えば、{0, 1, 2, 3, ...} は圏の対象集合で、{0, 1, 2, 3, ...}×{0, 1, 2, 3, ...} の一部が射の集合となります。

自然数の基本的な性質

これから考える数は自然数（0を含める）だけです。記号「≦」は大小関係、記号「+」は足し算、記号「-」は引き算を表すとします。自然数に関する法則を以下に列挙します。法則の仮定を横棒の上に、結論を横棒の下に書きます。

    (仮定なし)
  ---------------[1:反射律]
     a ≦ a


   a≦b   b≦c
  ---------------[2:推移律]
      a≦c


   a≦b   c≦d
  ---------------[3:足し算]
   a+c ≦ b+d


   x+a ≦ x+b
  ---------------[4:引き算]
     a ≦ b

最後の法則を「引き算（の法則）」と呼んでいるのは、a' = x+a, b' = x+b と置くと次の形に書けるからです。

      a' ≦ b'
  ------------------[4:引き算']
  a' - x ≦ b' - x

これらの法則を見れば、自然数がトレース付きモノイド圏となることはわかるでしょう -- ってのは気が早過ぎですね。順番に見ていきましょう。

自然数の順序から作る圏

a, b を自然数だとして、a≦b であるペア [a, b] を射とする圏を考えます。[a≦b] と書くと事情がハッキリするので、射はこの記法で書くことにします。圏としての自然数をNaC（natural numbers as a category）として、圏の定義をちゃんと述べておきます。

対象の集合 Ob(NaC) = |NaC| は、{0, 1, 2, ...} である。
射の集合 Mor(NaC) は [a≦b] というペアの全体。
dom([a≦b]) = a, cod([a≦b]) = b
id(a) = [a≦a]
[a≦b];[b≦c] = [a≦c]

以上に定義した構造が圏であるためには、f = [a≦b], g = [b≦c], h = [c≦d], id_a = [a≦a] などとして、次が成立する必要があります。

(f;g);h = f;(g;h)
id_a;f = f;id_b = f

恒等射 id_a = id(a) や結合「;」がちゃんと定義される（well-definedな）ことや、「;」の結合律と単位律は、先の自然数の基本的性質から簡単に導けますね。

自然数の足し算から作るモノイド圏

圏NaCに足し算を考えます。対象のあいだの足し算は普通の自然数の足し算そのものです。射の足し算は次のように定義します。

[a≦b] + [c≦d] = [a+c ≦ b+d]

対象と射が混じった足し算も次のように定義しておくと便利です。

a + [b≦c] = [a≦a] + [b≦c] = [a+b ≦ a+c]
[a≦b] + c = [a≦b] + [c≦c] = [a+c ≦ b+c]

x, y, z は対象でも射でもどっちでもいいとして：

(x + y) + z = x + (y + z)
0 + x = x + 0 = x

f, g, h, kを射、a, bを対象として：

(f + g);(h + k) = (f;h) + (g;k)
id_a+b = id_a + id_b

これらも、自然数の基本的性質からすぐに出ます。つまり、NaCに足し算「+」と足し算の単位「0」を一緒に考えると、モノイド圏となります。足し算は可換なので、より詳しくは対称モノイド圏です。[a+b ≦ b+a], [b+a ≦ a+b] が、a+b と b+a の同型（対称性）を与える射です。

引き算で作る対称モノイド圏上のトレース

まだ使ってない自然数の基本的性質は、引き算の法則です。[x+a ≦ x+b] のとき、「≦」の両側からxを引いてもいい、という法則です。この引き算は、対称モノイド圏NaCの上のトレースを定義します。

トレースってなんだ？その定義（むしろ雰囲気）は、「やっぱりこれからはフローチャートだな」で紹介した長谷川真人（はせがわ・まさひと）さんによる「再帰プログラムの意味論について」（PDF）の3.2節、特に9ページの絵を眺めてもらえるといいと思います。

自然数のひき算により定義されるトレースが、トレースの公理を満たしていることのヒントを並べておきます。Tr^x([x+a ≦ x+b]) = [a≦b] とします。

単位バニッシング：Tr⁰([0+a ≦ 0+b]) = [a≦b]
足し算バニッシング：Tr^y(Tr^x([x + y + a ≦ x + y + b])) = Tr^x+y([x + y + a ≦ x + y + b])
左タイトニング：Tr^x([x+a ≦ x+b];[x+b ≦ x+c]) = [a≦b];Tr^x([x+b ≦ x+c])
右タイトニング：Tr^x([x+a ≦ x+b];[x+b ≦ x+c]) = Tr^x([x+a ≦ x+b]);[b≦c]
スライディング：Tr^x([x+a ≦ x+b];[x+b ≦ x+b]) = Tr^x([x+a ≦ x+a];[x+a ≦ x+b])
ヤンキング：Tr^a([a+a ≦ a+a]) = [a≦a] = id_a
スーパーポージング（強度性）：Tr^x([x+a+c ≦ x+b+c]) = Tr^x([x+a ≦ x+b]) + c

トレース付きモノイド圏の典型例は、通りぬけ可能な紐が作る“組み紐の圏”でしょう。紐が互いに通りぬけ可能と仮定すると、もはや組み紐（ブレイド）と呼ぶのは不適切で、やっぱりアミダの圏かな。なんにしろ紐なんです。それと、再帰プログラムや正規表現のモデルもトレース付きモノイド圏です。自然数の順序と足し算から作るトレース付きモノイド圏は、おそらく（非自明な）一番簡単な例だろうと思います。

*1:ジョイアル／ストリート／ヴェリティ（Andre Joyal, Ross Street, Dominic Verity）の "Traced monoidal categories" (1996) じゃなかろうかと思いますが、見たことないので確証はありません。