このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

こんな簡単なトレース付きモノイド圏があったなんて

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

内容:

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)として、圏の定義をちゃんと述べておきます。

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

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

  1. (f;g);h = f;(g;h)
  2. ida;f = f;idb = f

恒等射 ida = 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 は対象でも射でもどっちでもいいとして:

  1. (x + y) + z = x + (y + z)
  2. 0 + x = x + 0 = x

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

  1. (f + g);(h + k) = (f;h) + (g;k)
  2. ida+b = ida + idb

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

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

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

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

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

  1. 単位バニッシング:Tr0([0+a ≦ 0+b]) = [a≦b]
  2. 足し算バニッシング:Try(Trx([x + y + a ≦ x + y + b])) = Trx+y([x + y + a ≦ x + y + b])
  3. 左タイトニング:Trx([x+a ≦ x+b];[x+b ≦ x+c]) = [a≦b];Trx([x+b ≦ x+c])
  4. 右タイトニング:Trx([x+a ≦ x+b];[x+b ≦ x+c]) = Trx([x+a ≦ x+b]);[b≦c]
  5. スライディング:Trx([x+a ≦ x+b];[x+b ≦ x+b]) = Trx([x+a ≦ x+a];[x+a ≦ x+b])
  6. ヤンキング:Tra([a+a ≦ a+a]) = [a≦a] = ida
  7. スーパーポージング(強度性):Trx([x+a+c ≦ x+b+c]) = Trx([x+a ≦ x+b]) + c

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

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