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

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

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

参照用 記事

最近のモナド論の概観と注意事項 1/2

モナドの理論を高次圏論を使って定式化すると、だいぶスッキリします。しかし、ベースになる高次圏論の概念・用語・記法が安定してないので、解説を読むのに苦労します。解説の解説(ガイダンス)があるといいような気がするので、ザッと書いてみます。落とし穴を指摘した道案内といったところです。

この記事と、あともう一回続きを書く予定です。

内容:

続きの記事:

関連する記事:

最近のモナド論とは

モナドの理論は、形式理論(後述)も含めて、1960年代/1970年代に完成したと言っていいでしょう。代表的な著作を挙げれば*1

  • ベック〈J. Beck〉の"Distributive Laws"が1969年
  • ストリート〈R. Street〉の"The Formal Theory of Monads"が1972年
  • グレイ〈J. Gray〉の"Formal Category Theory: Adjointness for 2-Categorires"が1974年

もちろん、その後もさまざまな方向への発展や、さまざまな分野への応用は続きましたが、中核的な内容は前世紀に出来上がっていたのです。

記事タイトルの「最近」とは、ここ20年くらいの話です。モナド論の中核的な内容が、高次圏論を用いて整理されました(もともと、モナドは高次圏的な概念ではありますが)。昔から知られていた事実でも、新しい側面からの解釈が生まれたりしました。今世紀に入って「今風にリフォーム(あるいはリフォーミュレーション)された」と言えばいいでしょうか。

しかし、モナド論を整理・リフォームするために使われる低次元の高次圏論〈low-dimensional higher category theory〉自体が未整理で混乱した様相を呈しています。このため、せっかくの今風のモナド論も、分かりにくく見えてしまいます。

低次元の高次圏論の(だらしなくザンネンな)用語法につては次の記事に書いてあります。僕の立場(つうか好み)による用語の選択もしています。

圏の“弱さ”が色々あって、話が難しくなったり曖昧になったりする事情は次の記事:

圏のサイズの問題と、それに対する楽観的態度については:

高次圏論(特に低次元部分)は、現状ではグチャグチャしているのですが、モナド論は高次圏論のよい応用なので、モナドをきっかけと題材として低次元高次圏論に入門するのもアリだと思います。

モナド論を分類すれば

モナドの理論を、次のようなダイコトミー〈二分法〉により分けておくと便利そうです。

  • 局所 vs. 大域
  • 形式 vs. 非形式

組み合わせると、次のようなモナド論があることになります。

  1. 非形式局所モナド
  2. 非形式大域モナド
  3. 形式局所モナド
  4. 形式大域モナド

このなかで、形式局所モナド論はあまり意味がないので取り除き、形式大域モナド論を単に形式モナド論とも呼ぶことにします。

局所モナド〈local theory of monads〉とは、特定の圏Cを固定して、C上のモナドだけを考えることです。C上のすべてのモナドを考えるかも知れませんが、異なる圏上のモナドを一緒に考えることはしません。それに対して大域モナド〈global theory of monads〉は、モナドの台圏〈underlying category〉を固定せずに、すべての圏の上のすべてのモナドを同時に考えます。

「形式〈formal〉」という言葉は注意が必要です。論理やプログラミング理論の形式体系〈formal system〉の意味の「形式」とは(無関係ではありませんが)違いますモナドは、圏、関手、自然変換を使って定義されます。それを、2-圏の対象、2-圏の射、2-圏の2-射に置き換えた定義から出発する理論がモナドの形式論〈formal theory of monads〉、あるいは形式モナドです。

圏の圏Catは、典型的な2-圏なので、Cat上で形式モナド論を展開できます。これが、通常の(形式化しない)モナド論です。非形式モナド論では、具体的に与えられた特定の2-圏(CatまたはCAT)内のモナドを考えますが、形式モナド論は、(適当な条件を満たす)2-圏ならどれでも通用する形で理論を構成します。

モナドは、「2-圏K内の対象C上のモナド」という特徴付けがされますが、モナドが居る環境である2-圏KCat(またはCAT)に固定し、さらにモナドの台Cも固定した議論が非形式局所モナドです。台を固定しないで、Cat(またはCAT)内の任意の対象を許した形が非形式大域モナドです。さらに、モナドが居る環境を(適当な条件を満たす)任意の2-圏にして考えると形式大域モナド論=形式モナドになります。

モナド論をホストする圏

前節の分類は、モナドをどこで考えるか? に関わっています。つまり、モナド論を展開する“場”が問題なのです。この“場”もまた圏(高次圏〈n-圏〉)です。よって、“場”となる圏をハッキリさせておきましょう。

一般的な“圏の圏”を次の形で表すことにします。

  • ρ-Cat#r

ρは圏の次元と“弱さ”を表します。n次元の“弱さ”を表すラベルの集合をWnとします。n = 0, 1, 2, 3 に関しては:

n Wn
0 {0}
1 {1}
2 {s2, w2}
3 {s3, ..., w3}

nが3以上になるとWnはよく分かりません。一番“強い”種類である sn (厳密n-圏という種類)はハッキリしています。wn は一番”弱い”種類ですが、nが大きくなると(おそらく n = 5 以上では)wn-圏の定義を具体的に書き下すことは事実上不可能になります。順序集合(またはプレ順序集合)としてのWnを明確にするのはとても難しいでしょう。

2-Catのような書き方は曖昧なので、s2-Cat, w2-Cat を使います。“弱さ”がハッキリしないときは、?3-Catのように、「不明」と明示して書くことにします。ワイルドカード'*'を使って *n-Cat と書くと、任意の“弱さ“を持つn-圏を意味することにします。([追記]'?'や'*'を付けるルールは守れないですね。単にn-Catと書くと、?n-Cat, *n-Cat の意味だと解釈するのが現実的です。[/追記]

下付きの"#r"で使うrは整数で、圏のサイズの階層を表します。U0は、可算無限集合ωを要素として含むグロタンディーク宇宙とします。そして、U0U1U2 ∈ ... をグロタンディーク宇宙の所属系列とします。このような所属系列が存在することは、楽観的な仮定ですが、それについては「入れ子の宇宙を可能とする公理」参照。

宇宙Ur内で考えた“小さなn-圏の(n+1)-圏”を ρ-Cat#r(ρ∈Wn)と書きます。wn-Catr∈|w(n+1)-Catr+1| が成立します。

よく使う圏は、次のように略記します。

  • Set := 0-Cat#0
  • SET := 0-Cat#1
  • Cat := 1-Cat#0
  • CAT := 1-Cat#1
  • s2-CAT := s2-Cat#1
  • Bicat := w2-Cat#0
  • BICAT := w2-Cat#1

Set∈|CAT|, Cat∈|s2-CAT| が成立します。

Cがn-圏で、0 < k ≦ n を整数だとして、kC は、(k + 1)次元以上の射をすべて捨ててしまったk-圏を意味します*2。例えば、1Cat は、“小さい圏の圏”ですが、自然変換を考えないものです。0C = |C|, nC = C が成立します。

C |→ kC は、圏(n-圏)を加工して圏を作る対応です。構成素の一部を捨てているので、切り捨て〈truncation〉です。切り捨ては、実はけっこう重要な操作です。

参考文献と著者

僕が眺めた(読んだとは言ってない)論文を古い順に並べます。

クリメン/ソリヴェレス 2010

アイレンベルク/ムーア構成〈Eilenberg-Moore construction〉とクライスリ構成〈Kleisli construction〉の関係を調べているときに引っかかった論文で、この話題(アイレンベルク/ムーア構成とクライスリ構成)に関して、丁寧に書かれた良い解説だと思います。また、例が、順序、論理、位相、一般代数〈universal algebra〉などから引かれていて面白いです。

ただし、読みやすくはないですね。あまり一般的でない用語・記法(例:conjugateとtranspose)が、他の文献への参照で済まされているのですが、参照先が(昔の紙の資料で)入手にしくいんですよ。前半がかなり冗長な感じなので、そこを圧縮してもうちょいセルフ・コンテインドにして欲しかった。また、記号のオーバーロードが激しい(例:圏EM、関手EM)ので、これも読みにくい原因かも。

ザワドウスキ 2010

短い論文ですが、密度が高くて難しいです。3-圏、4-圏を使ってモノイド・モナドを解説してますが、後半は僕にはよく理解できません。前半で、アイレンベルク/ムーア構成とクライスリ構成が今風に導入・定義されています。が、定義が特殊ケース過ぎる気もします。

なお、arXiv.org にある2010年投稿論文(上記)の、出版(ジャーナル掲載)されたバージョンがあります。

バスケス-マルケス 2015

"クリメン/ソリヴェレス 2010"と"ザワドウスキ 2010"の内容を咀嚼してより分かりやすく書いています。これは読みやすいです。中心となる概念の定義が付録にまとまっているので、付録を最初に、あるいは必要な時点で参照しないとワケわからないことになります。

ブーム 2018

今年出た論文ですが、定義を比較する目的で最初の数ページを眺めただけです。モノイド構造を持つモナドを一般化した形式論らしいです(読んでないのでよく知らんが)。


名前をカタカナ表記するために調べた情報を記します。

クリメン/ソリヴェレス

J. Climent Vidal と J. Soliveres Tur は、スペインのバレンシア大学の人のようです。省略されている J. は二人とも Juan で、スペイン語では「ホアン」と発音するようですが、「カタルーニャ語の人名であるジョアン(Joan)をスペイン語式に読んだもの」だとか。カタルーニャ出身なのかも知れません。

名前が3つの部分からなるので、最後の Vidal と Tur で呼べばいいかと思ったのですが、他から参照されるときに J. Climent and J. Soliveres と書かれていたので、クリメン〈Climent〉/ソリヴェレス〈Soliveres〉とします。クリメンさんは、Juan と Climent の間にもうひとつ名前(の要素)が入るみたいです、メールアドレスが Juan.B.Climent@uv.es なので。

ザワドウスキ

ポーランドワルシャワ大学の人のようです。Zawadowski の発音がForve(https://ja.forvo.com/)にもPronounceNames(https://www.pronouncenames.com/)にもなかったので、みたまんまで「ザワドウスキ」とします。

バスケス-マルケス

メキシコのインカーネット・ワード大学バヒオ校〈Universidad Incarnate Word Campus Bajio〉の人みたい。テキサス州サンアントニオにあるインカーネット・ワード大学のメキシコ・キャンパスなんじゃないのかな、たぶん。Incarnate Word のメキシコ(スペイン語)での発音は、「インカルナテ・ウオルー」に近いようです。

Vazquez-Marquez はハイフンで繋がっているので、これでひとつの名字なんでしょう。

ブーム

ハンガリーブダペストにあるウィグナー物理研究所〈Wigner Research Centre for Physics, Budapest〉の人みたいです。ファーストネームのガブリエラ〈Gabriella〉から女性だと思います。

続きは

タイトルに「1/2」を付けているので、もう一回続きを書く予定でいます(たぶん来年だろうが)。次回は、モナド論の中心的なトピックとか、事前に知っておくとよさそうな予備知識とか、誤解・勘違いしそうな所について書きます。

*1:ベックのモナド性定理〈Beck's monadicity theorem〉も1960年代の代表的な成果ですが、原典が分かりませんでした。

*2:高次圏: 用語法と文脈(主に2次元)」では、C(k)という書き方をしていました。