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

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

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

参照用 記事

圏のクリーネスター構成 もっと -- エフイチに触発されっぱなし

僕のように下心ドリブンでエフイチ(F1、一元体)を語ると、ロマンチックなエフイチ発見の物語がどうも詩情に欠ける世間話になってしまってアレだな、とは思います。ティッツの夢想を、有限幾何と組合せ論とかを素材に語ればロマンを回復できそうですが、もう少し「圏のクリーネスター」の続きを。ロマンはありませんが、妄想には満ちています。

10日ほど前のエントリー「圏のクリーネスター構成 -- エフイチに触発されて」で、エフイチからの教訓として次を挙げました。

  • あまりにも単純でヒドクつまらなそうなモノでも、想像を絶する深い構造を持つかもしれないぞ。
  • まったく異なった分野・領域でも類似の現象があれば、それは偶然ではないかもしれない。
  • ある体系内で欲しいモノが存在しないなら、その体系のほうを疑ってみる。
  • 圏論使ってみ、うまくいくかもよ。
  • 特にモノイド積(テンソル積)。

同じことの繰り返しですが、言葉を換えて言うと:

  • ゼロやイチについてほんとに真剣に考えてみろ。
  • 簡単な例をバカにしない!
  • 共通性や類似性に敏感であれ。
  • 妄想をたくましくしろ。

そんなわけで、共通性や類似性を頼りにして妄想の翼を広げてみます。まー妄想なんで、嘘が入っているかもしれないのでヨロシク。

内容:

  1. 「圏の圏」の上のリストモナド
  2. コレクションモナドとシーケント計算
  3. どこがエフイチ?

「圏の圏」の上のリストモナド

「圏のクリーネスター構成 -- エフイチに触発されて」の最後で指摘したように、1 + X + X2 + ... という式の形は色んな所で現れますが、圏のクリーネスター構成では、任意の長さのタプルを表すのでした。タプルは、配列とかリストとか言っても同じなんで、1 + X + X2 + ... = List(X) と書いてみます。

圏Cの非対称クリーネスター構成C#は、C# = List(C) となり、圏の圏Cat上の関手とみなせます。普通のList関手は、集合の圏Set上のモナドになっていますが、List:CatCatCat上のモナドになっています。関手 F:C→D に対して、List(F):List(C)→List(D) という関手を対応させることができます。それだけでなくて、自然変換 α::F⇒G:C→D があれば、List(α)::List(F)⇒List(G):List(C)→List(D) というリスト自然変換を対応させることができるので、Listは、厳密2-圏としてのCat上のモナドになっています。

モナドがあるということは、なんらかの随伴関手対があるはずです。List関手、つまり圏の非対称クリーネスターの作り方から、この関手は任意の圏Cに対して自由モノイド圏を対応させています。モノイド圏(とモノイド関手)の圏をMonCatとすると、List関手は、CatMonCatとみなせます。CatMonCatとみなしたList関手を特にFMC(Free Monoidal Category)とします。忘却関手を U:MonCatCat とすると、自由生成関手と忘却関手は随伴のはずですから、次の随伴性があるはずです。

  • Cat(C, U(M)) ≒ MonCat(FMC(C), M)

同様に、圏の対称クリーネスターは、与えられた圏Cから自由対称モノイド圏を作る関手(あるいは2-関手)FSMC(Free Symmetric Monoidal Category)です。対称モノイド圏全体からなる圏をSymMonCatとすると、次の随伴があるはずです。

  • Cat(C, U(S)) ≒ SymMonCat(SFMC(C), S)

FMCとFSMCに忘却関手を結合するとCat上のモナドになります。これらのモナドアイレンベルク/ムーア圏(Eilenberg-Moore category)の対象、つまりCat内のモナドの代数がモノイド圏/対称モノイド圏を再現しそうですよね、2-関手として考える必要があるでしょうが*1。それでは、これらのモナドのクライスリ圏(余代数の圏)は何に使えるのでしょうか? 経験上、クライスリ圏の射は計算概念に対応していたので、Cat上のクライスリ圏は関手計算の拡張を与えると期待できます。

コレクションモナドとシーケント計算

集合圏Setに戻って考えましょう。Set上のListモナドは、典型的なコレクションデータ型でした。もう少し正確に言うと、型Xからリスト型を構成する型構成子あるいは総称型がList(X)(プログラミング言語だと、List<X> と書くほうが多いでしょう)です。そして、マップ関数(高階関数)が関手の射部分(morphism part)を与えます。モナドとしての乗法と単位は、自然変換に対応する総称関数(flattenとunit)で与えられます。

典型的なコレクションデータ型としては、リスト以外にバッグ(マルチセット)とセットがあります。リスト・インスタンスを丸括弧、バッグ・インスタンスを角括弧、セット・インスタンスを波括弧(ブレイス)で書くとします。この三者の違いは次の不等式(非等式か?)/等式を見ればわかるでしょう。

  • (b, a, b) ≠ (a, b, b), (a, b, b) ≠ (a, b)
  • [b, a, b] = [a, b, b], [a, b, b] ≠ [a, b] 順序を問題にしない
  • {b, a, b} = {a, b, b}, {a, b, b} = {a, b} 重複を問題にしない

この3つのコレクションデータ型に対応するSet上のモナドをそれぞれ、List, Bag, FinSet とします。FinSetは有限集合のつもりです、Setとすると圏Setと同じ綴りになるのでこうしました。

さて、Listモナドに対応する圏Cat上のモナドは圏の非対称クリーネスターで与えられます。Bagモナドに対応する圏Cat上のモナドは圏の対称クリーネスターと考えていいでしょう。なぜならば、対称σa,b:a□b→b□a により、aとbの順序の違いを無視することができるからです。対称モノイド圏では、モノイド積はほぼ可換、つまり順序をほぼ気にしなくていいようになります。「ほぼ」なのは、対称σを介在させる必要があるからです。(対称については「圏論小ネタ:ヤン・バクスター方程式の圏論的な意味」も参照。)

次の対応表を考えましょう。

データ型 Set上のモナド Cat上のモナド 関係する圏の種類
リスト型 Listモナド 圏の非対称クリーネスタ モノイド圏
バッグ型 Bagモナド 圏の対称クリーネスタ 対称モノイド圏
セット型 FinSetモナド

表の疑問符部分が何であるか考えます。セット型の圏バージョンです。問題は「Cが圏のとき、FinSet(C) が何を表すべきか?」ですね。

ポイントは {a, b, b} = {a, b}、これね。同じモノが二度出てきたら1つにしていい、あるいは逆に、1つのモノを同じモノ2つ*2にしてもいい。ここで、ゲンツェン(Gerhard K. E. Gentzen)のシーケント計算を思い起こしましょう。シーケント計算には構造規則があり、それは次の3つです。(「換・増・減」というカッコイイ訳語は竹内外史によるものでしょうか?)

  1. 換 Exchange -- A, B → B, A
  2. 増 Weakening (Thinning) -- A → A, A
  3. 減 Contraction -- A, A → A

規則「換」を導入すると列(リストと思っていいです)の順序を無視することができます。そして、規則「増」と規則「減」により、重複出現を無視することができて、列は(有限)集合とみなしていいことになります。このことから、リストからバッグには規則「換」、バッグからセットには規則「増」「減」があればいいと分かります。

規則「換」に相当する圏論的概念は対称 σa,b:a□b→b□a でいいでしょう。規則「増」「減」の圏論バージョンがあればいいわけです。「増」の圏論バージョンがは対角(diagonal)、「減」の圏論バージョンは余対角(codiagonal)と呼ばれ、普通、Δと∇と書かれます。これらも対称(symmetry)σと同じく、対象でインデックスされた射の族(indexed family of morphisms)です。

  • 対角射の族 Δa:a→a□a
  • 余対角射の族 ∇a:a□a→a

もちろん、対角/余対角射の族には法則があります。その法則をきれいにまとめようとすると、余単位射 εa:a → 11はモノイド単位対象)と単位射 ηa:1→a も必要になります。対角/余対角/余単位/単位に関する“あると良さそう”な法則を全部書き下すと、双デカルト*3になります。

というわけで、セット型に対応する圏の種類は双デカルト圏であり、自由双デカルト圏を生成する関手がFinSetモナド圏論バージョンのように思えます。ただし、対称モノイド圏と双デカルト圏のあいだはだいぶ距離があるので、中間に対角付き対称モノイド圏(symmetric monoidal category with diagnals)とかデカルト圏(あるいは余デカルト圏)を入れてもいいと思います。

いずれにしても、重複させる(「増」)、重複を除く(「減」)のような単純な操作も、深い構造と驚くような一般化を持っています。今回は、コレクションモナドSetからCatにポーティングする話ですが、Maybeモナドのようなコレクション以外のモナドCatに持っていくとどうなるでしょう。2-関手の2-セル部分をうまく使うと何かできないでしょうか?

どこがエフイチ?

「エフイチに触発されっぱなし」と言う割にはエフイチが出てきてませんね。でも僕は、ゼロやイチのような自明なモノとすごく単純な操作をベースに妄想を語ったのでした。もっと露骨にエフイチと関係付けることもできます(例えば、ボトムとか計算の部分性とか)。「足し算がなくても線形代数が使える」と思うだけでも心理的な自由度は格段に上がります。妄想に躊躇しなくなります。いざとなったらエフイチ線形代数でツジツマを合わせられそうな安心感があるからです(ほんとにツジツマが合うかどうかは知らんけど)。

*1:代数系の指標はモナドでうまく定義できますが、代数系の法則をどうすれば表現できるのか分からないでいます。等式や同型は高次のセルなので、高次のモナドで表現できる気もしますが、、、

*2:「同じモノ2つ」とは面妖な言い方だ、同じなら1つだろうよ。で、線形論理

*3:デカルト圏とは、対角/余対角/余単位/単位を使って、すべての対象に双代数の構造が入るような圏です。通常の意味のデカルト圏になっており、双対的に余デカルト圏にもなっています。