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

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

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

［参照用 記事］

ローヴェア流セオリー論と統計モデル

雑記／備忘

次はイバン・パターソンの学位論文です。

  • Title: The algebra and machine representation of statistical models
  • Author: Evan Patterson
  • Submitted: 16 Jun 2020
  • Pages: 224p
  • URL: https://arxiv.org/abs/2006.08945

Youtube動画で、上記学位論文の主に3章 "The algebra of statistical theories and models" についてパターソン自身が語っています。

サマリーだけ知りたい方は、48分30秒から5分ほどで総括されています。また、質問時間（53分30秒くらいから）にスピヴァック〈David Spivak〉やフリッツ〈Tobias Fritz〉も登場しています。

パターソンが主題としている"statistical theories"は、普通の意味（国語辞書的意味）の“理論”ではなくて、ローヴェア〈William Lawvere〉の意味の“セオリー”です。「セオリー」はどうにも紛らわしい言葉ですが、最近ますます重要性を増しているように感じるので、ローヴェア流のセオリー論〈theory of theories〉としての“パターソンの統計セオリー論”を紹介します。

内容：

セオリーの理論

「フォングの“因果セオリー”の理論」で、圏論の文脈で現れる"theory"が国語（または英語）辞書的意味ではなくてテクニカル・タームな事があると指摘しました。

“セオリー〈theory〉”の普通ではない使い方は、ローヴェア〈William Lawvere〉に由来します。ローヴェアは鋭い洞察力と豊富なアイディアを持った圏論の大家ですが、人を悩ます奇妙なネーミングをします。[...snip...]

ローヴェアの代数理論（現在は"Lawvere theory"と呼ばれることが多い）は、代数学の理論という意味ではありません。とある条件を満たす圏のことを代数理論と呼ぶのです。僕は、少しでも混乱を避けるために代数セオリー（またはローヴェア・セオリー）とカタカナの「セオリー」を使います。

フォング〈Brendan Fong〉が使っていた言葉「因果セオリー〈causal theory〉」の「セオリー」はローヴェアのセオリーのことだし、「因果」も「原因と結果」という意味はなくて単にグラフの辺（または圏の射）のことでした。因果セオリーの形式的定義は小さな厳密対称厳密マルコフ圏〈small strictly-symmetric strict Markov category〉です。

パターソンの統計セオリーもフォングの因果セオリーと同様で、小さな厳密マルコフ圏です。パターソンは、特定のひとつの射が指定された小さな厳密マルコフ圏を統計セオリー〈statistical theory〉と呼んでますが、生成系〈system of generators〉を備えた小さな厳密マルコフ圏と定義したほうがいいでしょう（後述）。生成系は、マルコフ圏の指標〈signature〉と言っても同じです。

例えば、次は一番単純で一番よく使われる指標です。パターソンは主にこの単純な指標を扱っています。

signature Simple {
  sort P // パラメータ空間
  sort D // データ空間〈標本空間〉
  operation f:P -> D // 確率法則（のパラメータ族）
}

ベイズ確率論でいう事前分布を持った指標は次のようです。

signature SimpleBayesian {
  sort P // パラメータ空間
  sort D // データ空間〈標本空間〉
  operation p:1 -> P // 事前分布
  operation f:P -> D // 確率法則（のパラメータ族）
}

(1)圏の生成系である指標、(2)指標から生成された圏であるセオリー、(3)セオリーからの関手であるモデルが、ローヴェア流セオリー論の三種の基本的構成素です。セオリー論とはいいながら、モデルを扱うモデル論〈model theory | theory of modeles〉も含んでいます。

パターソンは、ローヴェア流セオリー論を圏論的論理〈categorical logic〉として参照していますが、論理のなかでも特にモデル論を圏論的に再定義したものが圏論的セオリー論〈categorical theory of categorical theories〉です。

スピヴァックの関手データモデル（「衝撃的なデータベース理論・関手的データモデル 入門」参照）もローヴェア流セオリー論の応用例で、そこでは、指標またはセオリーはスキーマと呼ばれ、モデルはデータインスタンスと呼ばれています。

（必ずしも圏論的ではない）論理では、論理式の集合をセオリーと呼ぶことがあります。これは、無関係ではありませんが、ローヴェア流セオリー論のセオリーとは少し違うので注意してください。

統計セオリー論のアンビエント圏

圏論的に確率統計の議論をするときの基本的なツール／フレームワークはマルコフ圏〈Markov category〉です。マルコフ圏については、「マルコフ圏 A First Look -- 圏論的確率論の最良の定式化」とそこから参照されている記事を参照してください。

また、「マルコフ圏の一族 // 様々な装備圏」で触れた装備〈supply〉概念*1は、もはやアノ界隈では常識のようです。アノ界隈とは、スピヴァック、フォング、フリッツ、そしてパターソンなどが参加している MIT Categories Seminar の周辺のことです。

装備（僕はモダリティと呼んでいた）概念を使えば、マルコフ圏とは余可換コモナド装備付き半デカルト・モノイド圏です。マルコフ圏のあいだのマルコフ関手は、モノイド関手（幾つかの種類がある）であって装備を保存する関手〈supply-preserving functor〉として定義できます。マルコフ自然変換も、装備と整合する*2モノイド自然変換として定義できるでしょう。

マルコフ圏を対象として、マルコフ構造（モノイド構造と余可換コモナド装備）と整合する関手と自然変換を1-射／2-射とする2-圏 MarkovCAT を構成できます。これはマルコフ圏の2-圏〈2-category of Markov Categories〉です。小さな厳密マルコフ圏（“厳密”はモノイド圏としての厳密性）からなる部分2-圏は StrMarkovCat ⊆ MarkovCAT とします。

2-圏 MarkovCAT は、統計セオリー論〈theory of statistical theorys〉を展開する環境となる圏なのでアンビエント圏〈ambient category〉と呼びましょう（実際は2-圏ですけど）。アンビエント圏の重要な性質は、A∈|StrMarkovCat| と C∈|MarkovCAT| に対して、関手圏 [A, C] が作れることです。関手圏は、モノイド構造やマルコフ構造を必ずしも持たなくてもいいので、[A, C]∈|CAT| と考えます（とりあえずは）。すると、[-. -] は次のような二項関手〈双関手〉です。

  • [-, -]:StrMarkovCatop×MarkovCat → CAT

このテの二項関手については次の記事で説明しています。

マルコフ指標と統計セオリー

統計セオリーを生成する指標は統計指標と呼ぶのが良さそうですが、「統計指標」って言葉で全然違った連想・印象を持つ人が多そうなのでマルコフ指標にします。それに、マルコフ指標と呼んだほうがネーミングの一貫性が保てます（次の段落）。

指標は、コンピュータッド〈computad〉とか多グラフ〈polygraph〉とも呼ばれ、圏を生成・定義する手段として用いられます。圏の種別（ドクトリン、メタ指標）ごとに指標の種別も決まります。今は、マルコフ圏という圏の種別を扱っているので、対応する指標はマルコフ指標〈Markov signature〉です。

マルコフ指標Σは、Σ0, Σ1, Σ2 という3つの集合（空であるかも知れない）で構成されます。Σ0 は圏の対象を表す記号の集合、Σ1 は圏の射を表す記号の集合、Σ2 は圏の等式的制約（可換図式と言っても同じ）を表す記号の集合です。

Σ1 の記号の域・余域としては、Σ0 の記号の連接が使え、連接は圏のモノイド積に対応します。Σ2 の記号の域・余域（等式の左辺・右辺）としては、Σ1 の記号とマルコフ圏の装備に対応する記号を使った項（射を表す複合記号）が使えます。

マルコフ指標Σから、小さい厳密マルコフ圏 Σ◇ が一意的に生成されます。が、Σ と Σ◇ をキチンと記述するのは煩雑な組み合わせ的議論があって大変です。詳細は割愛します。

マルコフ指標Σから生成された小さい厳密マルコフ圏 Σ◇ が統計セオリー、あるいはマルコフ・セオリーです。この意味での統計セオリーは、その部分系（部分圏とは限らない）として生成系Σを持っているし、Σから Σ◇ は決まってしまいます。したがって、マルコフ指標Σと統計セオリー〈マルコフ・セオリー〉Σ◇ はしばしば同一視されます。セオリーの理論は指標の理論でもあるわけです。

上記の事情から、セオリー射〈theory morphism〉と指標射〈signature morphism〉、セオリーの圏〈category of theories | theory category〉と指標の圏〈category of signatures | signature category〉もしばしば同一視されます。が、ここでは区別したいので、マルコフ指標の圏をMarkovSign、統計セオリー〈マルコフ・セオリー〉の圏をMarkovTheoとします。MarkovTheo は、MarkovSign（マルコフ・ドクトリン配下の2-コンピュータッドの圏）と StrMarkovCat を両端とする随伴ペアが誘導するモナドのクライスリ圏です。つまり、MarkovTheo の対象はマルコフ指標で、2つのマルコフ指標 Σ, Σ' のあいだのセオリー射は、自由生成関手 (-)◇ （の自由・忘却-随伴ペア）から得られるモナドのクライスリ射です。

指標とセオリーに関して色々な概念が登場しましたが、これらは指標／セオリーの一般論からのもので、マルコフ指標／マルコフ・セオリー〈統計セオリー〉に特有のものではありません。後で述べるように、プログラム意味論でも使われている道具・枠組みです。

統計モデル

マルコフ指標Σから生成された統計セオリー T := Σ◇ を固定します。定義により、T は小さな厳密マルコフ圏でした。T は、構文領域（記号の世界）を提供する圏です。構文に意味を付与するには意味領域を提供する圏が必要です。

意味領域が具体的であることを保証するために、確率的圏（昨日の記事「統計的反転の圏論的セットアップ 1/2 // 確率的圏と準確率的圏」参照）Cを選んで固定します。Cが意味領域、あるいは意味論〈semantics〉のターゲット圏〈target category〉です。

統計セオリーTの確率的圏Cにおけるモデル〈model〉とは、マルコフ関手 M:T → C in MarkovCAT です。アンビエント圏MarkovCATの性質から、モデルの全体は関手圏 [T, C]∈|CAT| を構成します。

T-統計モデルの全体 [T, C] が圏の構造を持つことから、モデルが同型であることを圏論的に定義できます。同型に限らず、モデルのあいだの関係を射として明確に表現できます。その具体例は、パターソンの動画や論文で述べられています。

もうひとつのマルコフ指標Σ'と統計セオリー T' := (Σ')◇ があったとしましょう。セオリー射 ψ:Σ → Σ' in MarkovTheo はマルコフ関手（セオリー射ψのクライスリ拡張） ψ#:T → T' in StrMarkovCat を誘導します。さらに、ψ# のプレ結合引き戻し〈pre-composition pullback〉(ψ#)*:[T', C] → [T, C] in CAT により、統計モデルの圏のあいだの関手を定義できます。

パターソンは、(ψ#)* をモデル移行関手〈model migration functor〉と呼んでいます。スピヴァックのデータ移行関手〈data migration functor〉に合わせた用語法ですね。セオリー射に沿ったモデル移行関手もスキーマ射に沿ったデータ移行関手も同じ概念です。プログラム意味論（のインスティチューション理論）ではリダクト関手〈reduct functor〉、インデックス付き圏の文脈では再インデキシング関手〈reindexing functor〉とも呼ばれます。

モデル移行関手を使えば、異なる統計セオリー上の統計モデルを比較することができます。パターソンは、モデル移行関手の実例も出しています。例えば、線形モデルが一般化線形モデルの特殊例であることは直感的には当たり前そうですが、厳密な記述と証明は出来るでしょうか？ パターソンの動画でこの例が語られています。

それから

ローヴェア流セオリー論（ローヴェア流モデル論でもある）のいいところは、構文と意味の関係が圏論的に整理できて事情がクリアになることです。パターソンは、ローヴェアのレシピを統計セオリー／統計モデルに適用したわけです。その結果、統計に関わる構文と意味の関係は実際クリアになりました。

クリアになった景色を眺めると、幾つか気が付くことがあります。

スピヴァックは、データ移行関手に関して、カン拡張を利用したΣ-Δ-Π随伴トリオ（「Σ-Δ-Π随伴、もう一言」参照）を構成しています。統計モデルのモデル移行関手についても同様なΣ-Δ-Π随伴トリオは可能でしょうか？ データベースの場合（単なる圏）と比べると統計モデルの場合（マルコフ圏）は事情が複雑なので、あまり期待は出来ない気がします。しかし、部分的にでもΣ-Δ-Π随伴トリオが構成できれば面白そう。

ジェイコブス〈Bart Jacobs〉達は、確率の計算にプログラム意味論の状態変換子／述語変換子の概念を移入しました（「ベイズ確率論、ジェイコブス達の新しい風」参照）。ドールクゥイスト〈Fredrik Dahlqvist〉達は、ベイズ反転の定式化のためにプログラム意味論のω完備性の概念を移入しました（「統計的反転の圏論的セットアップ 1/2」参照）。実は、スピヴァック／パターソンが利用したローヴェア流セオリー論も、プログラム意味論におけるインスティチューション理論〈institution theory〉としてかなり整備されています（「インスティチューション」のブログ内検索）。

どうも、プログラム意味論の各種手法は、確率統計に適用できる可能性が高いようです。いま例に挙げた、状態変換子／述語変換子、領域理論、インスティチューション理論以外にも、適用可能な手法があるかも知れません。それに、確率統計の計算を実際に行うときにコンピュータを使うことからも、確率統計と計算科学の相互浸透は歓迎できることですね。

*1:https://arxiv.org/abs/1908.02633 参照。

*2:「整合する」がどういう条件か僕はよく分かってません。ひょっとすると、特に条件は要らないのかも。