確率的圏、存在命題とスコーレム・コンビネータ - 檜山正幸のキマイラ飼育記 (はてなBlog)

以前に書いた記事「圏論的確率論におけるCタイプとAタイプ」と、昨日書いた記事「マルコフ圏におけるベイズの反転定理」に対する補足を書きます。

内容：

確率的圏
確率的圏の事例
存在命題
スコーレム・コンビネータ

確率的圏

確率的圏〈stochastic category〉とは何か？広く合意された定義はありません。が、曖昧なまま言葉を使うのはコミュニケーションに差し障りがあるので、暫定的あるいはローカルな定義をしておきます。

Measを、すべての可測空間と可測写像からなる圏として、Meas上のジリィモナドを Giry = (Giry, μ, η) （記号の乱用）とします。すると、圏Stocは、ジリィモナドのクライスリ圏として定義されます。

Stoc := Kl(Meas, Giry)

これは、具体的な圏Stocのハッキリとした定義です。

確率的圏とは、Stocへの埋め込み関手を持つ圏だとします。「埋め込み関手が存在する」ではなくて、特定の埋め込み関手を備えた構造を確率的圏と呼ぶことにします。

圏Cと埋め込み関手 J:C → Stoc の組 (C, J) が確率的圏です。例によって記号の乱用で C = (C, J) と書きます。

確率的圏の事例

同様にして、Measの部分圏（むしろ、|Meas|の部分集合）からStocの充満部分圏が決まります。例えば、FinStoc、FinDiscStoc など（「マルコフ圏の一族から典型例を7つ」参照）。

確率的圏の別な例として、マルコフ行列〈確率遷移行列〉の圏があります。実数係数の行列の圏をMatとします。Matの対象集合はNで、行列の幅〈列数〉と高さ〈行数〉が dom, cod となります。次の条件を満たす行列をマルコフ行列〈Markov matrix〉と呼ぶます。

成分は非負実数
成分を縦に足すと1

マルコフ行列の全体はMatの部分圏となるので、それをMarkovMatとします*1。J(n) := ({1, ..., n}, Pow({1, ..., n})) と対応させると、自然数nは有限離散可測空間に対応します。マルコフ行列Aは、有限離散可測空間のあいだのマルコフ核と解釈してそれを J(A) とすると、埋め込み関手 J:MarkovMat → Stoc になります。これで、(MarkovMar, J) は確率的圏になります。

MarkovMatには標準的なモノイド構造はないので、（無理矢理にモノイド構造を入れない限り）モノイド圏にはなりません。もちろんマルコフ圏にもなりません。確率的圏だからマルコフ圏であるとは限らないのです。確率的圏は具体的な圏としての性質であり、マルコフ圏の公理を満たす事とは直接的な関係はありません。ただし、実用的に使いやすい確率的圏はマルコフ圏になっています。

存在命題

「マルコフ圏におけるベイズの反転定理」において、マルコフ圏Cにおける命題としてCONDITを定義しました。
$\mathrm{CONDIT} :\Leftrightarrow \\ \:\:\forall (s:I \to X\otimes Y \mbox{ in }\mathcal{C}). \\ \:\:\exists (F:X \to Y \mbox{ in }\mathcal{C}). \\ \:\:\:\: s = s;(\Delta_X \,\otimes\, !_Y);(\mathrm{id}_X \otimes F)$

命題CONDITは、ベイズの条件化定理〈Bayes' conditionalization theorem〉を意味します。ベイズの反転定理〈Bayes' conversion theorem〉を意味する命題CONVSも定義しておきましょう。
$\mathrm{CONVS} :\Leftrightarrow \\ \:\:\forall (F:X \to Y, s:I \to X \mbox{ in }\mathcal{C}). \\ \:\:\exists (G:Y \to X \mbox{ in }\mathcal{C}). \\ \:\:\:\: s;\Delta_X;(\mathrm{id}_X \otimes F) = s;F;\Delta_Y ;(G\otimes \mathrm{id}_Y)$

使っている文字は「マルコフ圏におけるベイズの反転定理」と変えてあります。対称 $\sigma_{X,Y}$ を使うのはやめています。が、内容的にはまったく同じで、反転定理（を表す命題）です。

命題CONDITと命題CONVSは、一番外側に全称限量子（'∀'のこと）がありますが、キモは「条件を満たすモノの存在」を主張しているところなので、存在命題といっていいでしょう。マルコフ圏に存在命題を公理として付け加えると、より強い性質を持った圏を定義できます。

マルコフ圏の公理＋ CONDIT ＝条件化可能マルコフ圏の公理
マルコフ圏の公理＋ CONVS ＝反転可能マルコフ圏の公理

「マルコフ圏におけるベイズの反転定理」で述べたことにより、「Cが条件化可能マルコフ圏 ⇒ Cが反転可能マルコフ圏」です。これは、公理的な議論（「圏論的確率論におけるCタイプとAタイプ」における「Aタイプの圏論的確率論」のスタイル）で証明されているので、具体的なマルコフ圏でCONDITが確認できれば、CONVSの成立は保証されます。

スコーレム・コンビネータ

集合 X, Y に関して次の形の存在命題があったとします。

$\forall x\in X. \exists y\in Y. P(x, y)$

すると、f:X → Y という関数で、次の性質を持つものが（超越的には）作れます。

$\forall x\in X. P(x, f(x))$

このような関数fを、存在命題に対するスコーレム関数〈Skolem function〉と呼びます。

同様な発想で、圏論の存在命題があると、対応するコンビネータを作れることがあります。マルコフ圏における存在命題 CONDIT, CONVS に関しては実際に対応するコンビネータを作れます。

For X,Y∈|C|, Condit_X,Y:C(I, X $\otimes$ Y) → C(X, Y) in Set
For X,Y∈|C|, Convs_X,Y:C(X, Y)×C(I, X) → C(Y, X) in Set

スコーレム関数と考え方が同じなので、スコーレム・コンビネータ〈Skolem combinator〉と呼ぶことにします。Conditは存在命題CONDITに対するスコーレム・コンビネータで、Convsは存在命題CONVSに対するスコーレム・コンビネータです。

スコーレム・コンビネータを使うと、存在命題の形で述べられていた圏の性質を、「コンビネータを備えた圏」という形で再定義できます。コンビネータ方式のほうが、操作的〈operational〉・運算的〈calculational〉で計算には向いているようです。

コンビネータの利用はスコーレム・コンビネータには限りません。「マルコフ圏におけるベイズの反転定理」で述べた周辺化〈marginalize〉のコンビネータMargはスコーレム・コンビネータではありません。結合とモノイド積を組み合わせた計算をコンビネータとしています。

結合とモノイド積を組み合わせたコンビネータは、実数体上で言えば多項式関数のようなものです（例え話）。スコーレム・コンビネータは、平方根の存在定理から作られるルート関数sqrtのようなものです。多項式関数とルート関数を組み合わせるとより複雑な関数が作れるのと同様に、マルコフ圏上のコンビネータを様々に組み合わせて新しいコンビネータを構成できます。

圏論的確率論では（たぶん他の分野でも）、圏だけではなくて、その上のコンビネータ計算が重要になります。コンビネータを定義して積極的に使っていきましょう。

*1:|MarkovMat| = N_≧1 とします。N_≧1 は1以上の自然数の集合です。0を入れたらダメってわけじゃないですが、何かと面倒なので除外しておいたほうが楽です。