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

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

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

参照用 記事

ベイズ確率論とデータベース理論の統合: カップル化可能圏

今年(2020年)の6月にマルコフ圏というものを知りました。

マルコフ圏の直接的応用は圏論的確率論(「圏論的確率論におけるCタイプとAタイプ」参照)ですが、他の分野への応用もありそうです。「マルコフ圏の一族」より引用:

マルコフ圏が応用できそうな分野には、データベース理論、形式言語理論、オートマトン理論、プログラム意味論などがあります。これらはたまたま僕が少し知っている分野で、他にも物理や工学などに応用可能ではないかと思います。

当初から、マルコフ圏はデータベース理論とは親和性が高そうだと感じていました。一方、ここ一週間くらい、確率グラフィカルモデルの圏論的定式化を探していました。

昨日・今日で*1、公理(条件化可能公理〈conditionalizable axiom〉)を追加したマルコフ圏から得られる確率空間の圏、そしてデータベース理論に向いた圏が、同じ圏論的定式化を持つことが分かりました。それがカップル化可能圏〈couplable category〉です。

カップル化可能圏は線形代数内積ベクトル空間の圏)にも事例があり、ラムダ計算やシーケント計算とも関連を持ちます。ハイパーグラフ圏(ハイパーグラフ圏 一瞥)や自己双対コンパクト閉圏もカップル化可能圏の事例になります*2

この記事では、カップル化可能圏の形式的定義とすぐ分かる性質を手っ取り早く紹介します。カップル化可能圏の応用としては、当面はベイズ確率論とデータベース理論を想定していますが、応用はまた別な記事で。

内容:

簡単に経緯の説明

僕が主たる事例として考えていた圏は「確率グラフィカルモデルの背後にある圏は何か? // 見通し」で触れた (1/D)/=a.s. です。この圏が、ハイパーグラフ圏〈ダンジョン圏〉になっていれば好都合ですが、どうもそうではないようです。ハイパーグラフ圏でなくても、自己双対コンパクト圏にはなっているのでは? と期待してみたのですが、無理矢理にコンパクト構造をでっち上げてもいいことはないようです。

そこで、自己双対コンパクト圏よりさらに弱い構造を考えてみました。ラムダ計算(モノイド閉圏の計算)やトレース計算(トレース付き圏の計算)にならって、コンビネータ〈オペレーター〉を使って定義してみました。これはうまくいくようです。構造の中核となるコンビネータは「カップル化コンビネータ」と名付けました。カップル化コンビネータを備えた圏がカップル化可能圏です。カップル化可能圏は、自己双対コンパクト圏やハイパーグラフ圏より弱い〈一般的〉概念です。

カップル化可能圏が、実は、よく知られた圏の別定義だったという可能性はあります。そうであったとしても、カップル化コンビネータを使った定式化が無意味にはならないだろうと思います。カップル化コンビネータはけっこう使い勝手がいいですから。

以前に「確率的推論・判断の計算法:マルコフ・テンソル絵算」という記事を書きました -- ひたすら具体例を述べている記事です。この過去記事の「マルコフ・テンソル絵算」は、未整理ではありますが、今回述べるカップリング計算(カップル化可能圏の計算)であったようです。

今回の記事では、応用については述べませんが、カップル化可能圏の一般概念がデータベースとベイズ確率では何に対応するかを表にしておきます。末尾にアスタリスクが付いた言葉は、当該分野には対応する語がないので、檜山がテキトーにネーミングしたものです。

データベース ベイズ確率 カップル化可能圏
ドメイン 確率変数 対象
テーブルスキーマ 確率変数のリスト 多対象
関連 マルコフ核 射、多射
テーブル 同時確率分布 多ポイント
二部テーブル* 二部同時確率分布* カップ
二部テーブル化* 二部同時化* カップル化
関連化* 条件化 カップル化
等値ジョイン ジョイン* ジョイン
転置* 転置* 転置
反転* ベイズ反転 ダガー

カップル化可能圏の定義

C = (C, \otimes, I, σ) (記号の乱用、一部省略)は対称モノイド圏とします。β:I → I\otimesI in C は、I と I\otimesI のあいだの同型だとします(β = λI = ρI)。Cの対象 X, Y ごとに写像 CouX,Y が割り当てられている状況を考えます。(X, Y) \mapsto CouX,Y が以下の条件〈公理〉を満たすとき、対称モノイド圏とコンビネータ〈オペレーター〉の組 (C, Cou) がカップル化可能圏〈couplable category〉です。

  1. CouX,Y:C(X, Y) → C(I, X\otimesY) in Set
  2. CouX,Y は可逆で、逆写像 DecX,Y:C(I, X\otimesY) → C(X, Y) in Set を持つ。
  3. [結合公式〈composition formula〉] f:X → Y, g:Y → Z in C に対して、
    CouX,Z(f;g) = CouX,Y(f);(idX\otimesg)
  4. [積公式〈product formula〉] f:X → Y, h:Z → W in C に対して、
    CouX⊗Z,Y⊗W(f\otimesh) = β;(CouX,Y(f)\otimesCouZ,W(h));(idX\otimesσY,Z\otimesidZ)
  5. [可換律〈commutative law〉] X∈|C| に対して、
    CouX,X(idX);σX,X = CouX,X(idX)

カップル化可能圏 (C, Cou) の構成素〈constituent | ingredient〉は次のように呼びます。用語のバリエーション記述に正規表現を使っています。必要なら「用語のバリエーション記述のための正規表現」を参照してください。

カップル化可能圏とは、「結合公式・積公式・可換律を満たす可逆なカップル化コンビネータを備えた対称モノイド圏」です。

カップル化と反カップル化は互いに逆ですが、対称性(あるいは双対性)はありません。例えば、次の等式は成立しません(成立するとは限りません)。

  • DecX,Z)(f;g) = (idZ\otimesf);DecY,Z(g)

結合公式・積公式・可換律の双対を仮定してしまうと、自己双対コンパクト圏になってしまいます。反カップル化には等式的法則を何も仮定してないので、自己双対コンパクト圏よりカップル化可能圏が一般的な概念になっています。どのくらい一般的になっているのか? 現状よく分かりません。事例をよく調べる必要があるでしょう。

短縮記法と幾つかの等式

モノイド圏Cにおいて、I → X\otimesY in C の形の射をカップル{射}?〈couple {morphism}?〉と呼びます。カップル化可能圏のカップル化コンビネータは、任意の射をカップルに変換するコンビネータ〈オペレーター〉です。以下、一般の射を f, g など、カップルを s, t などで表すことにします。

「射 f:X → Y in Cカップル化」、「カップル s:I → X\otimesY の反カップル化」をそれぞれ次のように略記します。

  • f := CouX,Y(f)
  • ∪s := DecX,Y(s)

これは、絵図表現との対応を強く意識した象形文字記法です(後述)。また、カリー化/反カリー化との類似性も意識しています。

ラムダ計算 カップリング計算
カリー化 f カップル化 f
反カリー化 g カップル化 s
ベータ変換等式 f = f f = f
エータ変換等式 g = g s = s

右付き添字と左付き添字の左右に意味はありませんが、これでラムダ計算とカップリング計算の区別ができます。

絵算では、カップル化/反カップル化は、トレースやカリー化と同じワイヤー曲げオペレーターwire bending operator〉になります。次がカップル化/反カップル化の図示です。図の描画方向は↓→で旗で示しています(「絵算の描画方向を示すために旗を使うことにした」)。

ηX := (idX) とすると、f = ηX;(idX\otimesf) と書けます

   f 
 = (idX;f)
 // 結合公式
 = (idX);(idX\otimesf)
 // ηX の定義
 = ηX;(idX\otimesf)

したがって、カップル化コンビネータは、特別な射 ηX とモノイド積 \otimes と結合 ; で書けます。しかし、反カップル化コンビネータが特別な射とモノイド積と結合で書けるとは限りません。

この事情は、カリー化/反カリー化のときとは逆で、反カリー化は特別な射(評価射)と結合で書けますが、カリー化(ラムダ抽象)はそうはいきません。

カップル化コンビネータと同等な機能を持つ特別な射 ηX単位〈unit〉と呼びます。コンパクト構造〈コンパクト閉構造〉の単位と同じ機能を持つからです。ただし、余単位に相当する射の存在は保証されません。その意味で、カップル化可能圏は半コンパクト構造〈semi-compact structure〉を持つ圏だと言えます。

[追記]
「半コンパクト」って言葉を使いましたが、以前「超コンパクト」って言い方をしたことがありましたね。

関係圏と超コンパクト論理

このときの「超コンパクト」は、自己双対コンパクトの意味です。半コンパクトは、自己双対コンパクトよりもっと弱い構造になります。
[/追記]

可換律(カップル化可能圏の公理)から単位は次を満たします*3

  • ηXX,X = ηX

ラムダ計算の自然性とお絵描き」で述べたタイトニング等式とスライディング等式(の類似)はカップル化/反カップル化でも成立します。ストレートなスライディング等式は結合公式そのものです。

  • [タイトニング等式〈tightening〉] カップル s:I → X\otimesY in C と 射 g:Y → Z in Cに対して、
    (s;(idX\otimesg)) = (s);g
  • [ストレート・スライディング等式〈straight sliding〉 射 f:X → Y, g:Y → Z in C に対して、
    f;(idX\otimesg) = (f;g)

後で述べるダガー(記号は (-))を使うと、カーブに沿ったスライディング等式も成立します。

  • [カーブ・スライディング等式〈curved sliding〉] 射 f:X → Y, h:X → T in C に対して、
    f;(h\otimesidY) = (h;f)

タイトニング等式、カーブ・スライディング等式は絵算を使えば容易に示せます(次節参照)。

絵図表現と絵算

(C, Cou) はカップル化可能圏だとします。カップル化コンビネータと反カップル化コンビネータは、前節の絵のように、ワイヤーを曲げる操作として描きます。したがって、カップル化/反カップル化された結果は曲がったワイヤーを持ちます。

カップル化可能圏における一般的な射 f:X → Y in Cカップル s:I → X\otimesY in C、単位 ηX:I → X\otimesX は次のように描きます。

単位 ηX は CouX,X(idX) のことでした。カップル化は、単位を前結合〈pre-compose〉することで得られました、f = ηX;(idX\otimesf) 。

カップル化と反カップル化が逆であることを表す f = f (一種のニョロニョロ等式)は、単位を使って次のようにも表せます。

カップル化可能圏の公理である3つの法則は、絵等式では下のように描けます。

  1. [結合公式] (f;g) = f;(idX\otimesg)
  2. [積公式] (f\otimesg) = β;(f\otimesg);(idXσY,ZidZ)
  3. [可換律] ηXX,X = ηX

タイトニング等式は下のようです。

  • [タイトニング等式] (s;(idX\otimesg)) = s;g

カーブ・スライディング等式は次のようです。ここで、h は、下側の等式を満たすような射です(一意に決まる)。

  • [カーブ・スライディング等式]
  • [ダガーの定義] (h) = h;σX,T

カップルの圏

カップル化可能圏 (C, Cou) に対して、対象類〈対象集合〉は共有して、カップルを射とする新しい圏を作れます。新しい圏を D := Couple(C) として以下に定義します。

  1. |D| := |C|
  2. D(X, Y) := C(1, X\otimesY)
  3. 結合: s∈D(X, Y), t∈D(Y, Z) に対して、s*t := (s;t)
  4. 恒等射: cidX := ηX

この定義に従えば、(D, *, cid) が圏になることは示せます。さらにDは、次のモノイド積 \boxtimes により対称モノイド圏になります。

  • s:X → Y in D, u:Z → W in Dに対して、
    s\boxtimesu := β;s\otimesu;(idX\otimesσY,Z\otimesidW)

定義等式の右辺では、s, u をCのなかで考えていることに注意してください。

カップルの結合とモノイド積は次のように図示します。

以上のように D := Couple(C) を定義すると、CouX,Y:C(X, Y) → D(X, Y) in Set となります。ホムセット間の写像 CouX,Y をすべて寄せ集めると、モノイド積も厳密に保存する関手 Cou:CD になります。つまり、次が成立します。

  1. Cou(f;g) = Cou(f)*Cou(g)
  2. Cou(idX) = cidX
  3. Cou(f\otimesh) = Cou(f)\boxtimesCou(h)

カップル化は Dec:DC という関手になり、CouとDecは互いに逆な関手になります。CouとDecにより、モノイド圏CDはモノイド同型なモノイド圏です。モノイド同型ということは、CDは区別がつかない程にソックリなモノイド圏ということです。

カップル化可能圏のカップルは、I → X\otimesY という形から積カップル〈product couple〉と言えるでしょう。一方、ラムダ計算で使うモノイド閉圏のカップルは I → [X, Y] という指数カップル〈exponential couple〉です。カップリング計算とラムダ計算が似ているけど違うのは、積カップルと指数カップルが似ているけど違うからでしょう。

ダガー構造

カップル化可能圏 (C, Cou) から作られたカップルの圏 D = Couple(C) のモノイド圏構造は次の記号を使うことにしました。

結合 s*t
恒等射 cidX
モノイド積 s\boxtimesu

D の射(カップル)をもとの圏Cで考えることもあります。そのときは、;, id, \otimes で計算することもできます。

カップル s:I → X\otimesY in C (s:X → Y in D) に対して、sの転置〈transpose〉を次のように定義します。

  • sT := (s;σX,Y in C)

定義等式の右辺はCのなかで考えてますが、こうして作られた sT を sT:Y → X in D と解釈します。

転置は次の性質を持ちます。

  1. (sT)T = s
  2. (s*t)T = tT*sT
  3. (cidX)T = cidX

これはダガー圏の公理です。さらに、ダガーはモノイド構造と協調します。

  1. (s\boxtimest)T = sT\boxtimestT
  2. X,Y,Z)T = (αX,Y,Z)-1
  3. X)T = (λX)-1
  4. X)T = (λX)-1

ここで、α, λ, ρ は、モノイド圏の構造射(結合律子、左単位律子、右単位律子)です。

f = ((f)T) の関係で結ばれる、C上のダガー〈dagger〉に関しても同じ法則に従います。つまり、CもCouple(C)もダガー対称モノイド圏であり、CouとDecはダガー構造も含めた同型を与えることになります。

対称モノイド圏の標準簡約多圏の利用

今までの話は、まず対称モノイド圏があり、そこに様々な構造を載せていくスタイルでした。しかし、カップル化可能圏を計算デバイスと考えるときは、「対称モノイド多圏(簡約版)」で導入した簡約多圏を利用するのが便利です。

対称モノイド圏には、標準簡約多圏が存在します。標準簡約多圏は、対象がリスト(多対象)であり、厳密対称モノイド圏になっています。厳密モノイド圏は一般のモノイド圏に比べて扱いやすく、ストリング図との対応もより直接的になります。

カップリング計算の計算デバイスを組み立てる目的では、対称モノイド多圏を最初から準備して、その上にカップル化コンビネータ、反カップル化コンビネータを与えるほうがよさそうです。

おわりに

急ぎ足でカップル化可能圏の説明をしました。公理的定義は思い付いたばかりなので、不足や冗長性があるかも知れません。公理の妥当性を確認するには、具体例、特に「確率グラフィカルモデルの背後にある圏は何か? // 見通し」の (1/D)/=a.s. をよく調べる必要があります。データベースからの具体例も重要です。

感触としては、カップル化可能圏は絵算との相性が良く、かなりの再配置可能性〈reshapability〉(「ダンジョン圏における確率伝搬法」参照)を持つので、使いやすい気がします。

[追記]
2017年の初春に、確率の計算をゴタゴタ考えたことがあったけど、マルコフ圏とカップル化可能圏を使って整理できるかも知れないな。

[/追記]

*1:10月12日、池尻大橋駅すぐそばのカフェ・ベローチェで気づきました。 「余可換コモノイド・モダリティ事件の解説」に書いた余可換コモノイド・モダリティと部分圏の関係に気づいたのもカフェ・ベローチェでした。

*2:カップル化可能圏の事例達の相互関係; ハイパーグラフ圏は必然的に自己双対コンパクト閉圏になります。データベース理論に向いた圏(関係圏Rel)と内積ベクトル空間の圏は、自己双対コンパクト閉圏の事例です。マルコフ圏から得られる確率空間の圏は別種の事例です。

*3:絵図表現すると、可換律は、一種のヤンキング等式と言えます。