随伴系の二重圏

ひとつ前の記事「随伴系の圏の多様性」にて:

1AdjL(Cat)(あるいは、1AdjR(Cat))だけでも、モナド/コモナドを調べる道具に使えます。が、やはり随伴系の二重圏が欲しい。というわけで、随伴系の二重圏についても述べたいとは思っています(いつかわからんが)。

随伴系の二重圏は色々と使い途があるので、早めに定義しておきます。

内容:

形式論と具体論

モナドや随伴の理論には、形式論〈formal theory〉と具体論〈concrete theory〉があります。「最近のモナド論の概観と注意事項 1/2 // モナド論を分類すれば」では、形式論と“非形式論”という言葉を使ったのですが、ここでは具体論にします。

形式論は、一般的な厳密2-圏(または弱2-圏=双圏)Kを舞台として理論を展開します。それに対して、具体論は K = Cat と固定した理論になります。この記事では、主に具体論を扱いますが、ほとんどは形式論でも通用する話です。形式論の用語もけっこう使います。念の為に、「形式論 vs. 具体論」の対応表を載せておきます。

形式論 具体論
K Cat
対象=0-射
射=1-射 関手
2-射 自然変換

形式論におけるモナド/随伴系を、形式モナド/形式随伴系と言う人もいますが、そこまで区別するのは面倒だし意味もないと思うので区別しません。

厳密2-圏K内のモナドの全体を Mnd(K)、随伴系の全体を Adj(K) と書きます。しかし、モナドの全体も随伴系の全体も色々な種類があるので、'Mnd'と'Adj'に対して左下付きと右下付きで様々な修飾をします(「最近のモナド論の概観と注意事項 2/2」と「随伴系の圏の多様性」参照)。

上下左右の使い方

圏論、特に高次圏論の学習では、“上下左右”に慣れることが肝だと思います。なので、上下左右の話は、何度も何度も何度も繰り返しています*1。比較的最近だと:

その後の記事でも再度注意しています。

随伴系に関して言えば、2つの関手が構成素〈constituent | ingredient〉として含まれます。その2つの関手の片方を左関手と呼び、もう一方を右関手と呼びます。「左右」は単にペア〈カップル | コンビ〉における役割を区別するだけなので、「左関手・右関手」の代わりに「妻関手・夫関手」でも「ボケ関手・ツッコミ関手」でもかまいません。(次の記事も参照。)

一方で、図(ペースティング図とストリング図)を描いたとき、ほんとの空間的な位置・方向として上下左右を使うこともあります。さらには、空間的位置・方向にちなんで用語〈テクニカルターム〉が決められることもあります。ところがさらに、図の描き方(描画方向)が多様なので、描き方を変えると空間的位置・方向と用語は一致しなくなります。

圏論の極限を具体的に // 関手の極限の復習」に挙げた例ですが、次の圏論用語は同義語(「右カン拡張」は類義語)です。

  • 極限=逆極限=左根≒右カン拡張

もうほんとにどうにもならないグチャグチャ状況で、改善は無理でしょう。やれることは、注意して混乱や誤解を避けることだけ。今回の二重圏の話では、上下左右の議論がウンザリするほど登場します。ご注意ください。

2-射の形状

この記事では、圏を対象として随伴系を水平射として、関手を垂直射とする二重圏〈double category〉を考えます。二重圏やその実例については、次の記事に書いてあります。

随伴系の二重圏と言っても、作り方のオプションがいっぱいあるのですが、とりあえずは曖昧かつ総称的に、単に「二重圏」と呼んでおきます。

二重圏で注目すべきはその2-射〈2-セル〉です。2-射の図は2次元的な四角形になります。ここから先の説明で出てくる「上下左右」は、基本的には空間的な位置・方向のことです。ただし、左関手/右関手、(後で出てくる)左自然変換/右自然変換の「左右」は役割を識別する「左右」です。水平射を左から右、垂直射を上から下に描くことにします。

この描画方向で、二重圏の2-射αは次のようになります。

 C --(A)-→ D
 |         |
(F)   α   (G)
 |         |
 v         v
 C' -(A')→ D'

AとA'はそれぞれ随伴系で、水平射としての方向は随伴系の左関手の方向に合わせています。A = (η, ε: L -| R, L:CD), A' = (η', ε': L' -| R', L':C'D') とすれば、方向は次のようです:

  • A:CD は、L:CD と同じ方向。R:DC とは逆方向。
  • A':C'D' は、L':C'D' と同じ方向。R':D'C' とは逆方向。

もちろん、随伴系の方向を右関手の方向に合わせても何の不都合もなく、水平射の方向の選択はまったく恣意的です。

二重圏の2-射αは、実は2つの自然変換(もとにする厳密2-圏Catの2-射)から構成されます。α = (αleft, αright) とします。αleftとαrightが何モノであるか分かるように絵を描くと:

αleftは、上下辺が左関手LとL'である四角形(図のピンクの四角形)として描かれます。なので、左自然変換〈left natural transformation〉と呼ぶことにします。左関手/左自然変換の「左」は空間的位置・方向ではなくて、役割を識別する形容詞です。同様に、上下辺が右関手RとR'である四角形(図で奥側の水色の四角形)として描かれる自然変換は右自然変換〈right natural transformation〉です。左自然変換と右自然変換のペアが二重圏の2-射を構成します。

2-射αの構成素である左自然変換αleftを考えると、その方向の選び方は二種類あります。

  1. αleft: F*L'⇒L*G (下図の左側)
  2. αleft: L*G⇒F*L' (下図の右側)

一番目の方向を(地図の方向から)北東〈North-East〉方向、二番目の方向を南西〈South-West〉方向と呼ぶことにします。

2-射αの右自然変換αrightの方向の選び方も同様に2つの方向があります。

  1. αleft: R*F⇒G*R' (下図の左側)
  2. αleft: G*R'⇒R*F (下図の右側)

ただし、この図では、随伴系の右関手 R, R' のアローの方向が右から左になっています。通常の左から右にすれば、自然変換の方向も変化して見えます。我々は、右関手を逆向きに描くこの描画法を採用します。最初の立体的な絵において、左自然変換の面を正面に見る方向から観測して描いていると思ってください(裏側からは見ない)。図の左側が南東〈South-East〉方向、図の右側が北西〈North-West〉方向です。

αleft, αrightの方向の組み合わせは4種類になります。

  1. αleftが北東方向、αrightが南東方向
  2. αleftが北東方向、αrightが北西方向
  3. αleftが南西方向、αrightが南東方向
  4. αleftが南西方向、αrightが北西方向

しかし、とある条件(次節)を付けてふるい落とすと一種類だけが残ります。左自然変換が北東方向、右自然変換が南東方向が我々が使う組み合わせです。最初に選ぶ随伴系の方向を右関手に合わせると、右自然変換が南西方向、左自然変換が北西方向になります。とある条件については、次節で説明します。

メイト

前節で多様な方向について述べました。随伴系の方向の選び方が2種あり、それぞれについて、二重圏の2-射(=左自然変換と右自然変換のペア)の方向の選び方が4種あるので、二重圏としての方向の選び方は8種あり、方向の定義が異なる8つの二重圏が出来ます。

しかし、モナドと随伴系の関係を調べる目的では、8つの二重圏は無駄に一般的過ぎるようです。モナド論のなかでは、2-射の左自然変換と右自然変換が無関係である場合は出現しないからです。2-射の左自然変換と右自然変換には次の条件を課します。

  • 2-射を構成する左自然変換と右自然変換は、互いにメイト〈mate〉である。

今からメイトの説明をしますが、「互いにメイト」の特殊ケースでよく知られたものがあります。紹介しておきます。

  1. 随伴系によるホムセットの同型 D(L(A), Y) \stackrel{\sim}{=} C(A, R(Y)) により、射 g:L(A)→Y と f:A→R(Y) が互いに転置になる。
  2. ベクトル空間のあいだの2つの線形写像 f:V→W と g:W*→V* が互いに双対になる。

「互いに転置」「互いに双対」は、「互いにメイト」の特殊ケースです。今日は、メイトの一般論とその特殊ケースの関係を論じることはしませんが、随伴系の転置、線形写像の双対については次の記事で述べています。

さて、メイトという言葉をどのように使うかを説明します。実際の定義は次節です。

  • とある2つの自然変換の集合のあいだに1:1の対応がある。この対応をメイト対応〈mate correspondence〉、またはメイト同型〈mate isomorphism〉と呼ぶ。
  • メイト対応で対応付けられる2つの自然変換は互いにメイト〈mate〉であるという。

メイト対応

A = (η, ε: L -| R, L:CD) と A' = (η', ε': L' -| R', L':C'D') を2つの随伴系とします。次のような自然変換の集合を考えます。

  1. Nat(F*L', L*G:CD') : 関手 F*L':CD' から関手 L*G:CD' への自然変換の集合
  2. Nat(R*F, G*R':DC') : 関手 R*F:DC' から関手 G*R':DC' への自然変換の集合
  3. Nat(L*G, F*L':CD') : 関手 L*G:CD' から関手 F*L':CD' への自然変換の集合
  4. Nat(G*R', R*F:DC') : 関手 G*R':DC' から関手 R*F:DC' への自然変換の集合

先に導入した左自然変換/右自然変換と、自然変換の地図的方向を使って表現すれば:

  1. Nat(F*L', L*G:CD') : 北東方向の左自然変換の集合
  2. Nat(R*F, G*R':DC') : 南東方向の右自然変換の集合
  3. Nat(L*G, F*L':CD') : 南西方向の左自然変換の集合
  4. Nat(G*R', R*F:DC') : 北西方向の右自然変換の集合

地図的方向は、左自然変換を正面に見る視点から観測して言ってることで、右関手は奥側を右から左に向かっています。

さて、メイト対応は、次のような対応です。

  • Nat(F*L', L*G:CD') ←→ Nat(R*F, G*R':DC')

互いに逆写像であるペアなので、2つの写像があります。それらは、絵(ストリング図)を使えば簡単で印象的に表せます。

写像に名前を付けるより、次のような象形文字風の演算子記号を使うと分かりやすいでしょう。

  • (-):Nat(F*L', L*G:CD')→Nat(R*F, G*R':DC')
  • (-):Nat(R*F, G*R':DC')→Nat(F*L', L*G:CD')

(-)(-) が互いに逆なのは、随伴のニョロニョロ関係式〈snake relation〉から明らかです。

Nat(L*G, F*L':CD') と Nat(G*R', R*F:DC') のあいだでは、随伴系の単位・余単位を使ったメイト対応がうまく定義できないことが(やってみれば)分かります。随伴は完全な対称性は持ってないのですよね。ただし、(ストリング図で言えば)左右のワイヤーを交換するノードがあれば、メイト対応もどきが定義できるかも知れません(未確認)。

互いにメイトである自然変換のペアをメイトペア〈mate pair〉と呼ぶことにします。メイトペアの相方〈パートナー〉を求めるには、演算子 (-) または (-) を適用すれば済みます。

二重圏としてのAdjの定義

メイトペアの準備ができれば、随伴の二重圏を定義できます。

まず、水平圏として 1AdjL(Cat) か 1AdjR(Cat) のどちらかを選びます。今は 1AdjL(Cat) を選んだとしましょう。2-射は、互いにメイトになっている左自然変換と右自然変換のペアを選びます。こうして作った二重圏を次のように書きます。

  • dAdjL(Cat)

水平圏を 1AdjR(Cat) に選ぶと、次の二重圏ができます。

  • dAdjR(Cat)

dAdjL(Cat) と dAdjR(Cat) の2-射の状況は、次のように図示できます。バッテンに交差した2本の二重矢印は、互いにメイトである自然変換を表します。

dAdjL(Cat), dAdjR(Cat) が二重圏の公理を満たすことを確認する必要がありますが、ペースティング図かストリング図を使えば容易に確認できます。

二重圏Adjの利用

今回定義したような随伴の二重圏は、1960年代後半には、パルムクイスト〈Paul H. Palmquist〉*2により調べられていたようです。(紙の出版物でしかアクセスできないので、実物は見てません。)

  • Paul H. Palmquist. The Double Category of Adjoint Squares. PhD thesis, University of Chicago, 1969.

メイト対応を含めた随伴系の全体を把握するために、二重圏に編成するのはとても良いアイデアだと思います。二重圏の基本理論を適用して、随伴系達の構造がハッキリと見えるようになります。

二重圏を定義する場合、随伴系を水平射とするか垂直射とするかもオプションなので、随伴系を垂直射とした定義もあります。当然ながら、上下左右の話は丸っきり変わってしまいます。(が、本質的には同じこと。)

具体的な厳密2-圏Catをベースに話をしましたが、一般的・抽象的な厳密2-圏Kに対しても二重圏 dAdjL(K), dAdjR(K) を定義できます。さらには、弱2-圏〈双圏〉Kに対しても同様な議論ができます。

メイト」の節でちょっと触れたように、双対ベクトル空間/双対線形写像は、単対象弱2-圏とみなした VectK(Kは適当なスカラー体)に対する dAdjL(VectK) を使って定式化できます。

そしてもちろん dAdj(K)(右下の'□'には'L'か'R'が入る) は、モナドと随伴系の関係を調べるときの基本的な道具になります。モナドの圏は、dAdj(K) に埋め込むことができます。

dAdj(K) に、さらに3-射を加えて3次元の圏を作れます。この3次元構造は、モナドの2-射(モナドのあいだの射のあいだの射)を調べるときに必要となります。

また、dAdj(K) は、二重圏の事例としても面白いと思います。パラメータKを変えれば様々な二重圏を作れるので、事例の供給源になりそうです。

*1:自分(檜山)が上下左右のような空間認識が苦手で苦労しているので、過度に強調しているかも知れません。

*2:https://ja.forvo.com/search/Palmquist/ によると、"Pa"は「パ」とは発音しないようですが、うまくカタカナ表記できないし、綴りが連想できるように「パ」にしました。

随伴系の圏の多様性

随伴系〈adjunction | adjoint system〉の全体を、圏に編成することができます。しかし、その編成の方法と出来上がる圏は実に様々です。この多様性を捨て去るのではなくて、多様性自体を主題にするのも面白いかもな、と思います。

この記事は、モナド関連の話をダラダラするゆるいシリーズの一環。同じ話題のひとつ前の記事は「複合モナドから花輪積へ」。

内容:

随伴系の圏の次元と射の形状

随伴系の全体を圏に仕立てる場合、圏の次元が色々あり得ます。

  • 随伴系の1-圏
  • 随伴系の2-圏
  • 随伴系の3-圏

随伴系の1-圏(通常の圏)は、圏を対象として、そのあいだの随伴系を射とするものです。2-圏と3-圏は、随伴系の1-圏にそれぞれ、2-射と3-射を追加したものです。僕が想定しているケースでは、2-圏/3-圏は球体モデル〈globular model〉の圏ではありません。つまり、2-射/3-射の形状〈shape〉が2-球体〈円板 | ニ辺形〉/3-球体〈二面体〉ではありません。2-射の形状は四角形〈方形〉、3-射の形状は円柱形です。

随伴系の1-圏は普通の圏〈ordinary category〉で、随伴系の2-圏は二重圏〈double category〉の構造を持ちます。

  • 随伴系の1-圏 = 随伴系の圏
  • 随伴系の2-圏 = 随伴系の二重圏

随伴系の圏は、随伴系の二重圏のなかに水平圏(対象と水平射の圏)として埋め込まれます。

随伴系の3-圏は、… ンート … もっと複雑になります。今日のところはこれ以上説明はしません。(短い説明が出来ない。)

圏の次元と射の形状を今述べたように決めても、作り方にさらにいくつかの選択肢があります。随伴系の圏は射の方向が違う2種類、随伴系の二重圏は射(1-射と2-射)の方向〈direction〉と弱さ〈weakness〉*1で特徴付けられます。随伴系の二重圏がいったい何種類になるかは、勘定の仕方が(僕は)分からなくてハッキリしません。

随伴系の3-圏が何種類できるかは、もっと(僕は)分かりません。

随伴系の1-圏

とりあえず、圏を対象として随伴系を射とする(通常の)圏を考えます。この圏を 1Adj(Cat) とします。左下付きの'1'は1-圏であることを示します。右下付きの四角マーク'□'のところには'L'または'R'が入ります。小さい圏の厳密2-圏Catのなかで随伴系を考えますが、任意の厳密2-圏Kに対して*2 1Adj(K) を考えることができます。

随伴に馴染みがない方は、事前に次の記事を呼んでおくといいかも知れません。

L:CD, R:DC in Cat が関手の対〈ペア〉だとして、単位自然変換 η::C^⇒L*R:CC 、余単位自然変換 ε::R*L⇒D^:DD があり、(η, ε: L -| R) が随伴系になっているとします。(X^ は IdX の意味です。)

この随伴系の“向き”を左関手Lと同じ向きだと考える場合は、

  • (η, ε: L -| R, L:CD)

と書き、右関手Rの向きだと考えるなら次のように書きます。

  • (η, ε: L -| R, R:DR)

A = (η, ε: L -| R, L:CD), B = (ι, δ: M -| S, M:DE) のとき、

  • A:CD in 1AdjL(Cat)
  • B:DE in 1AdjL(Cat)

と考えます。1AdjLにおける下付きの'L'は、左関手〈left functor〉の向きに合わせることを意味します。

随伴系AとBの結合 A*B は次のように定義します。

  • A*B := (ε;(L*ι*R), (S*ε*M);δ : L*M -| S*R , L*M:CE)

アスタリスク'*'を結合の図式順記号に使ったのは、この結合を後で横(水平)方向の結合とみなす心積もりからです。定義の右辺に出てくる'*'は横結合またはヒゲ結合で、';'は縦結合です。

絵(ストリング図)を描いてみれば、定義の由来は明らかでしょう。この結合に関する結合律と単位律も絵で容易に示せます。

1AdjR(Cat) は、1AdjL(Cat) と同様に定義しますが、随伴系の向きを右関手〈right functor〉の向きにとります。一般的厳密2-圏Kに対する 1AdjL(K), 1AdjR(K) も同じ議論で定義できます。



1AdjL(Cat)(あるいは、1AdjR(Cat))だけでも、モナド/コモナドを調べる道具に使えます。が、やはり随伴系の二重圏が欲しい。というわけで、随伴系の二重圏についても述べたいとは思っています(いつかわからんが)。

*1:「弱さ」というと弱点/弱みという感じで否定的な感じがしますね。別な言葉がないかな? でも、意味は「弱さ」としか言いようがない。

*2:厳密2-圏ではなくて、弱2-圏=双圏に対しても随伴系の圏は定義できます。

素粒子の質を作り変えよう

おおおおー、すげーな、これ。

素粒子の質を作り変えるのかぁ。となると、加速器が必要でしょうね。例えば、CERN〈欧州原子核研究機構〉のLHC〈Large Hadron Collider | 大型ハドロン衝突型加速器〉は周長27kmの巨大施設。

CERNといえば、最近(2019年1月)、次世代の加速器建設計画を発表したようです。

周長100kmの加速器、建設費用は3兆円で、2050年代後半に稼働予定だそうです。

今なら、3兆円もかけずに無料で素粒子の質を作り変えることができるそうです、まー素敵。

松本さんはアイスクリームつくります

柔道の松本薫(元)選手、精悍な顔つきと俊敏な動きがとてもカッコよくて好きです。

でも、現役は引退なんですね。次の目標の「アイスクリームつくります」もなんかいいなー。

零項演算とは何か?

セミナーで受けた質問シリーズ(なのか?)、その3: 過去に何度も聞かれたことがある一般的な質問; 数の足し算・掛け算、集合の合併・共通部分などの演算に対して、オペランド(演算すべき対象物)が一つもないときどうなるのか?

内容:

オペランドが一つもないとき

幾つかの数 a1, a2, ..., an を全部足し算すること(あるいはその結果である総和)を次のように書きます。

  • \sum_{i = 1}^{n} a_i

a1, a2, ..., an を全部掛け算するなら:

  • \prod_{i = 1}^{n} a_i

幾つかの集合 A1, A2, ..., An を全部合併することは次のように書きます。

  •  \bigcup_{i = 1}^{n} A_i

A1, A2, ..., An 達すべての共通部分なら:

  •  \bigcap_{i = 1}^{n} A_i

これらは、数や集合のリストに対する演算と思えるので、次のように書いてもいいでしょう。

  •  \sum (a_1, a_2, \cdots, a_n)
  •  \prod (a_1, a_2, \cdots, a_n)
  •  \bigcup (A_1, A_2, \cdots, a_n)
  •  \bigcap (A_1, A_2, \cdots, a_n)

n = 2 の場合は:

  •  \sum (a_1, a_2) =  a_1 + a_2
  •  \prod (a_1, a_2) =  a_1 \times a_2
  •  \bigcup (A_1, A_2) = A_1 \cup A_2
  •  \bigcap (A_1, A_2) = A_1 \cap A_2

n = 1 の場合は次でいいでしょう。

  •  \sum (a_1) =  a_1
  •  \prod (a_1) =  a_1
  •  \bigcup (A_1) = A_1
  •  \bigcap (A_1) = A_1

さて、n = 0 の場合はどうなるのでしょうか?

  •  \sum () =  ?
  •  \prod () =  ?
  •  \bigcup () = ?
  •  \bigcap () = ?

[補足]
ここで言っている零項演算は、最初に二項演算があり、その二項演算から作ったn項演算において、n = 0 としたものです。つまり、「二項演算ありき」の状況設定です。二項演算がなくて、いきなり集合X上の零項演算〈無項演算 | nullary operation〉と言った場合は、X0→X という写像のことです。集合Xの零乗は単元集合なので、1→X となり、(いきなりの)零項演算はXの特定要素と同一視できます。例えば、付点集合〈poited set〉は、零項演算〈無項演算〉をひとつ備えた構造になります。
[/補足]

リストの連接から考える

2つのリスト (a1, ..., an), (b1, ..., bm) に対してその連接〈concatenation〉を次のように定義します。

  • (a1, ..., an) # (b1, ..., bm) := (a1, ..., an, b1, ..., bm)

'#'が連接演算の演算子記号です。連接の単位元〈中立元〉は空リスト () になります。

  • () # (a1, ..., an) = (a1, ..., an)
  • (a1, ..., an) # () = (a1, ..., an)

リストは太字で書くことにすれば、

  • () # a = a
  • a # () = a

前節の「リストの要素全部をナニカする」演算と、リストの連接には次の関係があります。

  •  \sum ({\bf a} \;\#\; {\bf b}) = \sum {\bf a} \,+\, \sum {\bf b}
  •  \prod ({\bf a} \;\#\; {\bf b}) = \prod {\bf a} \,\times\, \prod {\bf b}
  •  \bigcup ({\bf A} \;\#\; {\bf B}) = \bigcup {\bf A} \,\cup\, \bigcup {\bf A}
  •  \bigcap ({\bf A} \;\#\; {\bf B}) = \bigcap {\bf A} \,\cap\, \bigcap {\bf A}

足し算に関して、連接の片側を空リストに置いてみると:

  •  \sum {\bf a} = \sum (() \;\#\; {\bf a}) = \sum () \,+\, \sum {\bf a}
  •  \sum {\bf a} = \sum ({\bf a} \;\#\; ()) = \sum {\bf a}  \,+\, \sum ()

これより、 \sum () は足し算の単位元〈中立元 | 零元〉でなければならないことが分かります。足し算以外も同様で:

  •  \sum () = 0
  •  \prod () = 1
  •  \bigcup () = \emptyset
  •  \bigcap () = X

ここで、Xは部分集合の親となる全体集合です。

集合演算の定義から直接導く

集合演算の場合は、その定義から直接に零項演算の結果が何であるかが分かります。

Iをインデックスセットとします。I = {1, 2, ..., n} だと思ってもかまいません。Iでインデックス付けられた集合族〈I-indexed family of sets〉の合併と共通部分は、次の論理同値で定義されます:

  •   \mbox{For} \;x \in X,\: (x \in \bigcup_{i \in I} A_i) \:\Leftrightarrow\: \exists k \in I.(x \in A_k)
  •   \mbox{For} \;x \in X,\: (x \in \bigcap_{i \in I} A_i) \:\Leftrightarrow\: \forall k \in I.(x \in A_k)

ここで、インデックスセットIを空集合に置いてみると:

  •   \mbox{For} \;x \in X,\: (x \in \bigcup_{i \in \emptyset} A_i) \:\Leftrightarrow\: \exists k \in \emptyset.(x \in A_k)
  •   \mbox{For} \;x \in X,\: (x \in \bigcap_{i \in \emptyset} A_i) \:\Leftrightarrow\: \forall k \in \emptyset.(x \in A_k)

「i∈\emptyset に対する Ai」が不思議ですが、空集合をインデックスセットとするような部分集合の族は(ただ一つだけ)存在し、それがAなのです -- Aは空リストのことだと思ってもいいです。さて、上記の同値の右側の条件を変型すると:

  •   \mbox{For} \;x \in X,\: \exists k \in \emptyset.(x \in A_k) \:\Leftrightarrow\: \exists k.(k \in \emptyset \land x \in A_k)
  •   \mbox{For} \;x \in X,\: \forall k \in \emptyset.(x \in A_k) \:\Leftrightarrow\: \forall k.(k \in \emptyset \Rightarrow x \in A_k)

 k \in \emptyset は偽ですから:

  •   \mbox{For} \;x \in X,\: \exists k.(k \in \emptyset \land x \in A_k) \:\Leftrightarrow\: \exists k.(False \land x \in A_k) \:\Leftrightarrow\: False
  •   \mbox{For} \;x \in X,\: \forall k.(k \in \emptyset \Rightarrow x \in A_k) \:\Leftrightarrow\: \forall k.(False \Rightarrow x \in A_k) \:\Leftrightarrow\: True

下側(二番目)の同値では、含意の前件(左側)が偽なら含意命題は問答無用に真になることを使っています。

以上より:

  •   \mbox{For} \;x \in X,\: (x \in \bigcup_{i \in \emptyset} A_i) \:\Leftrightarrow\: False
  •   \mbox{For} \;x \in X,\: (x \in \bigcap_{i \in \emptyset} A_i) \:\Leftrightarrow\: True

つまり、次が言えます。

  •   \forall x \in X.(x \notin \bigcup_{i \in \emptyset} A_i)
  •   \forall x \in X.(x \in \bigcap_{i \in \emptyset} A_i)

結局:

  •   \bigcup_{i \in \emptyset} A_i = \emptyset
  •   \bigcap_{i \in \emptyset} A_i = X

順序集合の上限と下限

前節の議論を、少し別な観点から見てみましょう。インデックスセットIでインデックス付けられたXの部分集合族〈I-indexed family of subsets of X〉Aは、A:I→Pow(X) という写像のことです(Pow(X)はXのベキ集合)。

写像A単射の場合は、写像Aの代わりにその像集合

  • {S∈Pow(X) | S = Ai (Ai = A(i)) となる i∈I が在る}

を考えても同じことです。また、部分集合族の表現として、単射写像を選ぶことができるので、「Iでインデックス付けられたXの部分集合族 ←→ Pow(X)の部分集合」という相互変換(1:1ではない*1)が出来ます。

話を一般化して、ベキ集合Pow(X)とは限らない順序集合 L = (L, ≦) を考えます。Lの部分集合Aに対して、Aの上限〈supremum | 最小上界 | least upper bound〉とAの下限〈infimum | 最大下界 | greatest lower bound〉を定義しましょう。

a∈L が A⊆L の上限だとは、aが次の条件を満たすことです。

  1. x∈A ならば x ≦ a
  2. 「x∈A ならば x ≦ b」となるbに対して、a ≦ b

下限の定義は順序関係をひっくり返すだけです。aがAの下限だとは:

  1. x∈A ならば a ≦ x
  2. 「x∈A ならば x ≦ b」となるbに対して、b ≦ a

勝手に選んだAに対して上限・下限が存在することは(一般には)保証されませんが、在るならそれらを sup(A), inf(A) と書きます。

さて、空集合\emptysetに対して sup(\emptyset), inf(\emptyset) が在るとして、それはどんなものでしょうか? 上限の定義のAのところに\emptysetを入れると:

  1. x∈\emptyset ならば x ≦ a
  2. 「x∈\emptyset ならば x ≦ b」となるbに対して、a ≦ b

一番目の条件は常に真(前件が偽だから)なので、二番目だけ考えればいいですね。二番目の条件内の「x∈\emptyset ならば x ≦ b」も常に真なので、bに関する縛りは何もなくなって:

  • 任意のbに対して、a ≦ b

論理式で書くなら:

  • ∀b∈L.(a ≦ b)

これは a = sup(\emptyset) がLの最小元〈least element〉であることを意味します。同様に、inf(\emptyset) はLの最大元〈greatest element〉になります。

  • sup(\emptyset) = least(L)
  • inf(\emptyset) = greatest(L)

(L, ≦) として (Pow(X), ⊆) を取ったときは:

  • sup(\emptyset) = least(Pow(X)) =  \emptyset
  • inf(\emptyset) = greatest(Pow(X)) = X

ここで、\emptysetが、\emptyset⊆Pow(X) と \emptyset⊆X の意味で登場することに注意してください。

前節の話との関連性は:

  •  sup(\emptyset) = \bigcup_{i \in \emptyset} A_i
  •  inf(\emptyset) = \bigcap_{i \in \emptyset} A_i

*1:インデキシングの写像全射単射に分解して、その単射部分を取り出せば、像集合と同一視できます。

三段論法とは何か?

昨日に引き続き、セミナーで受けた質問で一般的なものを; 「三段論法とは何ですか?」に答えておきます。

内容:

アリストテレスがやっていたヤツ

「三段論法」という言葉は、割とよく耳にしますが、数理論理学のテクニカルタームとしては定義されてないと思います。ローカルに定義する人がいるかも知れませんが、広く合意された定義はないでしょう。国語辞典に載っている言葉(日常語、非専門語)として解釈したほうが無難です。

言語運用状況の統計的証拠はありませんが、「三段論法」の用法で多そうなのは、アリストテレスがやっていた論理の手法を指す場合だと思います。僕は歴史に疎いので、古代ギリシアの論理はよく知りませんが、「大前提/小前提/結論」という形式があるので「三段」と呼ぶんじゃないかと想像します。でも、英語(もとはギリシャ語)だと"syllogism"〈シロジズム〉で、特に「三」の意味はないようです。

モーダスポネンス

次のような推論の形式をモーダスポネンス〈modus ponens | MP〉といいます。モーダスポネンスはラテン語みたい。

   A   A⇒B
  ----------MP
      B

モーダスポネンスをシーケントで書くなら:

  • A, A⇒B → B

このモーダスポネンスを三段論法と呼ぶこともあるようです。アリストテレスのシロジズムにもモーダスポネンスのような論法はあるので、モーダスポネンスがアリストテレスとまったく無関係とは言いにくく、モーダスポネンスを三段論法と呼んでも別にいいんじゃないかな、と思います。

あるいはまた、次のような推論を三段論法と思っている人もいるかも知れません。

   A⇒B   B⇒C
  -------------
      A⇒C

これは、モーダスポネンスから導くことができます。自然演繹風の証明図(セミナーでは、証明図ではなくて推論図と呼んでます*1)で描くなら:

  #1
  ---
   A  A⇒B
  ---------MP
      B       B⇒C
     --------------MP
          C
        -------#1
         A⇒C

ここで、二箇所に'#1'と書いてあるのは、仮定のAを消して含意の前件に持ってきたことを示します -- カリー化とかラムダ抽象に相当する*2操作です。

上記の証明(推論)の仮定と結論だけをシーケントで書けば:

  • A⇒B, B⇒C → A⇒C

これも、A, B, C という三つの命題が出てくるから三段論法なのかもね。

カット

論理式のリストを、Γ, Δ などのギリシャ文字大文字で表すことにして、シーケント計算における次の規則(セミナーではシーケントの推論規則を基本リーズニングと呼んでます*3)をカット〈cut〉といいます*4

  Γ → A   A, Δ → B
 ======================Cut
    Γ, Δ → B

先に出てきた自然演繹風証明図と区別するため、横棒は二本棒にしています。

カットが部分的な結合〈partial composition〉であることは見て取れると思いますが、通常の結合があれば、カット=部分結合は導くことができます。

                ☆
             ========
  Γ → A    Δ → Δ
 =====================Prod
    Γ, Δ → A, Δ          A, Δ → B
   ===================================Comp
       Γ, Δ → B

ここでは、ゲンツェンのLKシーケントとは違って、右辺のカンマも連言の意味です。Prodは、左辺どうし/右辺どうしをそのまま連接する操作で、Compは順次結合する操作です。ProdやCompについてより詳しいこと、あるいはもっとグラフィカルな表現については:

えーとそれで、カット〈部分結合〉のことも三段論法と呼ぶことがあります。



結局、「三段論法」という言葉は大変に曖昧です。もともとが曖昧なんだから、どんな意味で使おうが目くじらは立てませんが、曖昧性を避けたいなら使わないのが吉です。

*1:証明図と呼ばず推論図と呼ぶには事情があります。

*2:「相当する」は、カリー/ハワード対応により関係付けられることを意味します。

*3:推論/証明とは呼ばずリーズニングと呼ぶには事情があります。

*4:もう少し一般的な形にすることが多いかも。

論理式の集合とは何か?

セミナーで受けた質問ですが、一般的な話なので、応答をこちらに書きます。命題を形式化した構文的対象物が論理式です。この論理式の集合を正確に定義するとどうなるのか? という話です。

内容:

用途と論理を決める

論理式には、絶対的唯一の定義があると思っている方がいるかも知れませんが、それは誤解です。プログラミング言語が何十何百もあるのはご存知でしょう。プログラミング言語ごとにその構文は違います。同様に、論理式(の言語)も人工言語なので、何十何百もあります。論理式の言語と集合は、使用状況と好みに応じてその場その場で作る(定義する)ものだと考えたほうがいいでしょう。

ただし、論理式(の言語と集合)を定義するための、だいたいのガイドラインはあります。このガイドラインも唯一ではなくて、いくつもあります。多様多彩な世界なんです。ここでは、典型的なガイドラインと、そのガイドラインに沿った構文定義の実例をひとつ挙げます。

まず用途が決まらないと、論理式を定義することが出来ないので、ここでは、自然数の計算や、自然数に関わる推論を行うことを目的にします。そして、どんな論理を使うかを決めます。ここでの例では、一番ポピュラーな古典論理を使うことにします。

基本記号を全部挙げる

目的と論理が決まったら、使う記号をすべて列挙します。このとき、記号を分類するガイドラインが役に立ちます。

  1. 定数記号
  2. 変数記号
  3. 演算記号〈関数記号〉
  4. 述語記号〈関係記号〉
  5. 論理記号〈論理結合子記号と限量子記号〉
  6. 補助記号

説明は後にして、各種の記号を並べてしまいます。

  1. 定数記号: '0', '1'
  2. 変数記号: すぐ下で定義する
  3. 演算記号: '+', '*'
  4. 述語記号: '=', '≦'
  5. 論理記号: '∧', '¬', '∀'
  6. 補助記号: '(', ')', ',', '.'

変数記号は無限個あるので、書き並べるわけにいきません。変数記号は次のように決めます。

  • 英字〈ラテン文字〉小文字1文字、またはその後に数字〈digit〉を任意個付けたもの。

例えば、'x', 'a', 'x1', 'k123' などは変数です。'x1'のような複数文字でも、全体としてひとつの記号とみなします。'x'と'1'に分解したりはしません。

上記の基本記号を選んだ方針や理由を述べておきましょう。利便性は考慮せず(実際、不便になります)基本記号を節約する方針です。

  • 定数記号は'0'と'1'だけなので、例えば2を表すには "1 + 1"とする。
  • 演算記号は'+'と'*'だけなので、引き算や割り算は(必要なら)後で定義する。
  • 述語記号も、'≧'や'<'が必要なら後で定義する。
  • 論理記号も通常より少ない。古典論理を使うので、ド・モルガンの法則などを根拠に後から定義できる。
    • A∨B は、¬(¬A∧¬B) と後で定義する。
    • ∃x.A は、 ¬∀x.¬A と後で定義する。
    • A⇒B は、¬A∨B と後で定義する。
  • 自然数しか扱わないので、型の指定はしない。したがって型を表す記号は入ってない。

今までに挙げた記号を基本記号〈{basic | atomic | primitive} symbol〉と呼びます。いくつかの基本記号を、デタラメでもいいので並べたものを記号列〈{string | sequence} of symbols〉と呼びます。複数文字の単一記号もあるので、記号列内の記号をピッタリくっつけるわけにはいきません。空白を挟むことにします。また、記号列全体は二重引用符で囲みます。例えば:

  • "a1 0 ¬ k123 * ≦ ∀ . 1"

こういうデタラメな記号列では、空白(区切り記号)が必要ですが、文法〈構文規則〉で制限した記号列(それが後述する項や論理式)では、空白は必須ではなくなります。例えば、次の記号列は論理式ですが、実際には空白は不要です。

  • "∀ n , m . ¬ ∀ q , r . ( ¬ ( ( n = ( ( q * m ) + r ) ) ∧ ( ( r ≦ m ) ∧ ¬ ( r = n ) ) ) )"

'∃'や'<'を使うことを許して、括弧も適宜省略して書くなら:

  • "∀n,m.∃q,r.(n = q*m + r ∧ r < m)"

構文の定義

記号列のほとんどはデタラメなゴミです。ゴミではない、我々が使うべき記号列をハッキリさせる規則が構文規則〈文法〉です。構文規則の記述には、BNFバッカス/ナウア形式〉が便利であり標準的でもあります。

プログラミング言語に多少の馴染みがあるのなら、次の記事を読むと構文定義(や意味定義)の方法が手っ取り早く分かるでしょう。

BNFに関しては、「UMiToL言語の構文」の節に簡単な例と他の記事への参照があります。

というわけで、構文の定義にはBNFを使うことにします。構文定義の際に、項の定義と論理式の定義の二段階に分けます。〈term〉とは、(今の場合)自然数を表す式のことで、論理式〈formula〉は命題を表す式です。

「項と論理式に分けて定義する」というのもガイドラインのひとつで、「分けないで定義する」というガイドライン(流儀)もあります*1。僕は、分けたほうが分かりやすいと感じています。

項の定義
基本項 ::= '0' | '1' | 変数記号
項 ::= 基本項 | '(' 項 '+' 項 ')' |  '(' 項 '*' 項 ')' | '(' 項 ')'

次は基本項の例です。

  • 0
  • 1
  • x
  • a
  • x1
  • k123

基本項は、記号ひとつからなる記号列なので、"0", "1", "x1" のように書くべきでしょうが、もう二重引用符や空白を律儀に書くのはやめます。

変数記号は無限個あるので、基本項も無限個あります。次は、基本項とは限らない一般の項の例です。

  • ((1 + 0) + 1)
  • ((x*1) + (((1 + 1) + 1)*k123))

上記の構文規則に従えば、演算するごとに括弧で囲むので、括弧が大量に付きます。0, 1, 2, 3, 4 のような定数も次の項で表現します。

  • 0
  • 1
  • (1 + 1)
  • ((1 + 1) + 1)
  • (((1 + 1) + 1) + 1)

人が読み書きするにはひどく不便ですが、機械による処理が単純化されます。

論理式の定義
基本論理式 ::= '(' 項 '=' 項 ')' | '(' 項 '≦' 項 ')'
論理式 ::= 基本論理式 | 論理式 '∧' 論理式 | '¬' 論理式 | '∀' 変数並び '.' '(' 論理式 ')' | '(' 論理式 ')'
変数並び ::= 変数 | 変数並び ',' 変数

この規則から、括弧が相当にうるさい論理式が定義されます。とりあえずは、処理しやすい(構文解析木が作りやすい)構文定義をしました。人間の読み書きのためには、別に略記の規則を導入すればいいでしょう。

もちろん、最初から人間可読性〈human readability〉に優れた構文を定義してもいいですが、構文定義も構文解析処理も複雑になります。ここらへんの兼ね合いは、なかなかに難しいですね。

論理式の集合

最初に決めた基本記号の集合をSymbolとします。

  • Symbol = {'0', '1', '+', '*', '=', '≦', '∧', '¬', '∀', '(', ')', ',', '.', 'x', 'a', 'x1', 'k123', ...}

集合Symbolの要素を並べたものである記号列の集合をSymbol*と書きます。右肩の星はクリーネスターと呼び、「並べたもの」を表す星です。集合Symbol*の要素を幾つか挙げれば:

  • "a1 0 ¬ k123 * ≦ ∀ . 1" ∈ Symbol*
  • "(((1 + 1) + 1) + 1)" ∈ Symbol*
  • "∀ n , m . ¬ ∀ q , r . ( ¬ ( ( n = ( ( q * m ) + r ) ) ∧ ( ( r ≦ m ) ∧ ¬ ( r = n ) ) ) )" ∈ Symbol*

集合Symbol*のなかで、項と認められる記号列の集合をTermとします。もちろん、Term⊆Symbol* です。さらに、論理式と認められる記号列の集合をFormulaとします。Formula⊆Symbol* です。

以上で、集合Formulaがちゃんと定義されました。ここで重要な注意は、集合Formulaは、今ここで「自然数の計算や、自然数に関わる推論を行うこと」を目的に「古典論理を使うこと」を前提に作られたことです。別な目的で別な論理を使うなら、別なFormulaが定義されます。この世に唯一のFormulaが在るわけじゃありません。たくさんのたくさんのFormulaが在り得るのです。

コンテキストに関する注意

集合Formulaの要素、つまり論理式に対してその“意味”を考えます。通常は、論理式の意味は外延(あるいは真理集合)として与えます。例えば、"(x + y = 10)∧(x ≦ y)" の意味なら、{(x, y)∈N2 | (x + y = 10)∧(x ≦ y)} という集合がその意味になります。

しかし、外延(真理集合)が {(x, y, z)∈N3 | (x + y = 10)∧(x ≦ y)} であってもかまいません。「zという変数は入ってないからダメ」とか言うと、「3次元空間R3内で、x2 + y2 = 1 は円筒を表す」といった主張も禁止することになります。何がマズイのかと言うと、変数を含む(含まなくてもいいのだが)論理式と、変数の領域を一緒に考えてないことです。

変数(複数かも知れない)が走る領域に対する指定をコンテキスト〈context〉と呼びます。コンテキストが明示されず、暗黙の前提で済まされることは多いです。そんなときは、「論理式」にコンテキストが暗黙に刷り込まれていると解釈します。

暗黙の前提は、誤解と混乱の原因になるのでやめたほうがいい(あるいは、ほどほどにしたほうがいい)と僕は思いますが、現実には多用されているのでご注意ください。

*1:この例で言えば、型Natと型Boolを導入すれば、項だけで話が済みます。

花輪?

昨日「複合モナドから花輪積へ」で、花輪積〈wreath product | リース積〉の話をしたのですが、花輪だから次のような画像を添えました。

*1

でも、「お花がたくさん」はふさわしくなくて、次のようなモノかも。

*2

後で気が付いたんだけど、モナドの文脈では、木の枝とか蔦を絡めて作った輪が、リースの意味するところじゃないのかな?

ベックの分配法則(特に混合分配法則)を"entwining"とも呼びます。"entwine"の意味は、「からみつく、巻きつく、からませる、まつわらせる、からませる、編む、織り込む」だそうです。おそらく(想像だが)、複数の素材が絡まった構造をリースと呼んだのでしょう。

リース積は、小枝や蔦が絡まった輪から、別な絡み輪を作る操作、って感じなのでしょう。そう思うと割と腑に落ちる。ストリング図の計算は、絡んだ蔦をいじっているみたいだからね。

複合モナドから花輪積へ

2つのモナドのあいだにベックの分配法則〈Beck's distributive law〉があれば、それらを組み合わせて複合モナドを作れます。複合モナドの構成は、2つのモナドから1つのモナドを生成するので、一種の“積”と考えられます。この“積”を花輪積〈wreath product | リース積〉と呼びます。

花輪積をちゃんと定義して調べるには、けっこう大掛かりな舞台装置が必要です。技術的な細部・正確さにはこだわらず、花輪積を定義するためのアイデアについて手みじかに述べます。

*1

内容:

サイズと宇宙

圏のサイズの問題に対処するために、グロタンディーク宇宙の系列 U0U1U2 ... を想定します。宇宙 Ur のなかで小さい集合の圏/小さい圏の厳密2-圏を、それぞれ Set#rCat#r と書きます。同様に、宇宙 Ur のなかで小さい厳密n-圏からなる厳密(n + 1)-圏を sn-Cat#r と書きます。

宇宙の番号(階層番号)が明示してなくて、単に Set, Cat, sn-Cat と書いてある場合は、適当なrがデフォルトとして前提されています。そのような前提が一切ない場合は r = 0 とみなします。

この記事の以下の記述では、階層番号rを明示しません。これは、必要に応じてrを取ると考えます。例えば('∈0'は「対象として含む」の意味)、Set#00 Cat#10 s2-Cat#2 という系列が必要なら、r = 2 として、s2-Cat#2 を単に s2-Cat と書きます。通常の議論は、rを2か3に取れば十分でしょう。

モナド論に必要なサイズと宇宙については、次を参照してください。

モナド達の2-圏

Kを厳密2-圏として、K内のモナドの全体を考えます。モナドのあいだの準同型射〈morphism〉と、モナドのあいだの準同型射のあいだの準同型2-射〈2-morphism〉を一緒に考えると、K内のモナド達は厳密2-圏を構成します。この厳密2-圏を s2MndEM(K) と書きます。左下付きの's2'は、厳密2-圏であることを忘れないための目印です。語尾の'EM'はアイレンベルク/ムーア構成と相性がいいように定義したことを示します*2

s2-Cat を厳密2-圏からなる圏とします。s2-Cat は厳密3-圏になりますが、単なる圏(1-圏)とみなしたものを 1(s2-Cat) と書きます。左下付きの'1'は、1-圏であることを忘れないための目印です。1(s2-Cat) の対象は厳密2-圏で、射はラックス2-関手です。ラックス2-関手については、次を参照してください。

s2MndEM(-) は、厳密2-圏に厳密2-圏を対応付けますが、ラックス2-関手 F:KL in 1(s2-Cat) に対して s2MndEM(F):s2MndEM(K)→s2MndEM(L) in 1(s2-Cat) はうまく定義できるので、s2MndEM(-) は、1(s2-Cat)→1(s2-Cat) in CAT という自己関手になります(CAT は一階層上の“圏の厳密2-圏”)。

s2MndEM上に載ったモナド構造

s2MndEM(-):1(s2-Cat)→1(s2-Cat) in CAT なので、厳密2-圏 CAT 内に、s2MndEM(-) を台関手とするようなモナドを構成できる可能性があります。

まずモナド単位ですが、これは、

  • triv::Id1(s2-Cat)s2MndEM(-):1(s2-Cat)→1(s2-Cat) in CAT

とします。成分で書けば:

  • trivK:Ks2MndEM(K) in 1(s2-Cat)

trivK は、圏 1(s2-Cat) の射なので、ラックス2-関手ですが、K対象Aに、A上の自明なモナド〈trivial monad | identity monad | 恒等モナド〉を対応させます。自明なモナドとは、単位も乗法も恒等であるモナドです。

次は、s2MndEM(-) 上のモナド乗法です。モナド乗法を作るのはなかなか難しいですが、それが出来たとして、wtp("wreath product"から)としましょう。

  • wtp::s2MndEM(s2MndEM(-))⇒s2MndEM(-):1(s2-Cat)→1(s2-Cat) in CAT

成分で書けば:

  • wtpK:s2MndEM(s2MndEM(K))→s2MndEM(K) in 1(s2-Cat)

このモナド乗法=花輪積〈wreath product〉を具体的に構成することが課題になります。

モナドを構成する行為が再びモナドになっているという、またしても“入れ子の世界”の現象に出会いました。

参考資料

花輪積に関する基本的な文献は次です。花輪積の演算対象物として花輪〈wreath〉という概念が定義されています。K内の花輪とは、s2MndEM(s2MndEM(K)) の対象です。複合モナドの発展形は、“花輪の理論”です。

*1:画像: https://www.creema.jp/item/1629213/detail より

*2:実際の s2MndEM(K) の構成は、単にモナドの全体に射と2-射を入れたというものではなくて、アイレンベルク/ムーア構成を使って自由完備化を行うもので、簡単ではありません。

さまざまなモナド類似物とベックの分配法則

モナドとコモナド、それらを組み合わせたもの、条件の一部を取り除いたものなどを、モナド類似物monad-like entity〉と呼ぶことにします。今までに、さまざまなモナド類似物に出会ってはいるのですが、それらを統一的に理解することがなかなか出来ませんでした。

最近になって多少は進展がみられて、昔の疑問が解けたりしています。今日は、そんな話。

内容:

バーの論文

ベックの分配法則〈Beck's distributive law〉に関して、マイケル・バー〈Michael Barr〉の短い論文があります。

たった5ページですが、示唆に富む内容で、いくつかの方向に発想を広げるヒントになります。

この論文を書いたバーの動機は、線形論理に出てくる自然変換 δA,B,C:A\otimes(B\oplusC) → (A\otimesB)\oplusC が、ベックの分配法則として説明出来ないか? というものです。結果的に、線形論理のδはベックの分配法則の事例になっています。そのことを示すためにバーは、分配法則を一般化しています。

現在、よく知られている分配法則のタイプは:

  1. 2つのモナドのあいだの分配法則
  2. 2つのコモナドのあいだの分配法則
  3. モナドとコモナドのあいだの分配法則(混合分配法則〈mixed distributive law〉)

バーは、モナドでもコモナドでもない単なる自己関手のあいだに分配法則を定義して、ベックの持ち上げ定理が何の条件もなしに成立することを証明しています。

2011年に僕は、動機はまったく違うのですが、ほぼ同じ問題を考えていました。

今読み返して、すじ(方向性)は悪くないと思いますが、詰めが甘く、モヤッとしたままでした。バーのアイデアを使うと、モヤモヤに決着が付きそうです。

2011年のモヤモヤ

双代数と双モノイド」に曰く:

Cを固定して、F, Gが2つの自己関手(F = G でもかまいません)として、(A, a:F(A)→A) がF代数、(A, b:A→G(A)) がG余代数だとします。βが β::FG⇒GF:CC という自然変換とします。ここで「FG」は、関手の反図式順の結合「Gの後にF」を意味するとします。僕は図式順が好きですが、ここでは慣例に従い反図式順を使います。

F代数とG余代数の組み合わせ (A, a, b) がFGβ双代数だとは、次の五角形が可換図式となることです。

「FGβ双代数」という名称はともかくとして、設定と定義はこれで合ってます(と、現時点では断言できる)。しかし、確信が持てないので、最後の段落にモヤッとしたことを書いています。

最後に気なることを: 双代数法則に出てくるβはどっから来るのでしょうか? βの条件として次があります。

  1. F(b);βA:F(A)→GF(A) が、F(A)上のG余代数余演算となる。
  2. βA;G(a):FG(A)→G(A) が、G(A)上のF代数演算となる。

この条件でどこまでβが決まるのかは(僕には)よく分かりません。ベックの分配法則と類似の状況になっているようには思えますが。

「βの正体や特徴付けが分からない」けど「ベックの分配法則っぽい」とは書いています。「っぽい」ではなくて、βはまさにベックの分配法則そのものです(ただし、混合分配法則)。僕の歯切れが悪いのは、単なる自己関手 F, G に対して「ベックの分配法則」なんて言っていいのか? そんなものに意味があるのか? と、戸惑い躊躇していたからです。

バーは、単なる自己関手でもベックの分配法則を考えてもいいと喝破し、モナドの分配法則の場合と類似の結果が(ある程度は)成立することを示しています。

モナド類似物の分類

バーの結果は、戸惑いと躊躇を振り払ってしまえば、かなり簡単な話です。広い範囲のモナド類似物に対してアイレンベルク/ムーア構成が有効なんだ、という観察が基本になります。

ここで、モナド類似物に呼び名がないので困ってしまいます。集合ベースの代数系との類似性から命名をすることにします -- 次のような集合ベースの代数系はよく知られています。

代数系 一言説明
マグマ 何の法則も仮定しない
半群 結合律が成立する
モノイド 結合律と単位律が成立する
コモノイド 余結合律と余単位律が成立する
半環 2つのモノイド演算があり、分配律が成立する

これらの集合ベースの代数系と似た関手ベースの代数系を、XXX-like monad と呼ぶことにします。"XXX-like"を「XXX様」で表すことにします。

モナド類似物 一言説明
マグマ様モナド 何の法則も仮定しない
半群モナド 結合律が成立する
モノイド様モナド 結合律と単位律が成立する
コモノイド様モナド 余結合律と余単位律が成立する
半環様モナド 2つのモノイド演算があり、分配律が成立する

モノイド様モナドは通常のモナドで、コモノイド様モナドはコモナドです。そして、半環様モナドが「ベックの分配法則、ベック分配系、複合モナド」で述べたベック分配系になります。

これらのモナド類似物に対して、アイレンベルク/ムーア構成が定義できます。つまり、モナド類似物が与えられると、そのアイレンベルク/ムーア圏が作れます。アイレンベルク/ムーア圏の対象を何と呼ぶか? またしても呼び名がない。

アイレンベルク/ムーア圏の対象の大分類としては、演算が1つのときは代数〈algebra〉か余代数〈coalgebra〉、演算が2つのときはそれらの組み合わせになります。例えば:

  1. モノイド様モナド〈通常のモナド〉 (F, η, μ) のアイレンベルク/ムーア圏の対象は、代数 a:F(A)→A in C
  2. コモノイド様モナド〈コモナド〉 (G, ε, Δ) のアイレンベルク/ムーア圏の対象は、余代数 b:A→G(A) in C
  3. 半環様モナド〈ベック分配系〉 ((M, η, μ), (A, ζ, α), δ) のアイレンベルク/ムーア圏の対象は、A上の2つの代数 m:M(A)→A in C, a:A(A)→A in C

代数/余代数は基本的大分類なので、個々のモナドアイレンベルク/ムーア圏の対象はさらに呼び分ける必要があります。例えば:

  1. マグマ様モナドアイレンベルク/ムーア圏の対象は、アイレンベルク/ムーア・マグマ
  2. 半群モナドアイレンベルク/ムーア圏の対象は、アイレンベルク/ムーア・半群
  3. モノイド様モナドアイレンベルク/ムーア圏の対象は、アイレンベルク/ムーア・モノイド
  4. コモノイド様モナドアイレンベルク/ムーア圏の対象は、アイレンベルク/ムーア・コモノイド
  5. 半環様モナドアイレンベルク/ムーア圏の対象は、アイレンベルク/ムーア・半環

ベックの分配法則、ベック分配系、複合モナド」では、アイレンベルク/ムーア・モノイドを1演算代数〈1-operation algebra〉、アイレンベルク/ムーア・半環を2演算分配代数〈2-operation distributive algebra〉と呼んでいます。注意すべきは、半群/モノイド/コモノイド/半環などが、ほんとにそのような代数系を意味するのではなくて、単なる比喩的な呼び名だ、ということです。

マグマレベルの議論

ベックは、分配法則によってモナドを“持ち上げる”ことが出来ることを示しました。この持ち上げ〈lifting〉には、モナド構造はなくてもよく、単なる自己関手であっても持ち上げは可能です。誰がそれに気付いたのかは知りませんが、冒頭に紹介したバーの論文には明確に書いてあります。

双代数と双モノイド」と同じ状況設定をします。F, G は圏C上の自己関手とします。次のように定義します。

  • A∈|C| に対して、F(A)→A in C を、Fのアイレンベルク/ムーア・マグマ〈Eilenberg-Moore magma〉、または単にF-マグマ〈F-magma〉と呼ぶ。
  • A∈|C| に対して、A→G(A) in C を、Fのアイレンベルク/ムーア・コマグマ〈Eilenberg-Moore comagma〉、または単にG-コマグマ〈F-comagma〉と呼ぶ。
  • 自然変換 β::G*F⇒F*G:CC を、Gに対するFの分配法則〈distributive law of F over G〉と呼ぶ。
  • A∈|C| に対して、F-マグマ F(A)→A とG-コマグマ A→G(A) の構造と、分配法則 β::G*F⇒F*G があり、冒頭に引用した可換図式を満たすとき(すぐ後で再論)、(F, G, β)-双マグマ〈(F, G, β)-bimagma〉と呼ぶ。

代数系何の法則もないので、代数/余代数/双代数の代わりに、マグマ/コマグマ/双マグマという言葉を使っています。マグマ/コマグマ/双マグマの準同型射を常識的に定義すれば圏になります。それらの圏を次のように書きます。

  • C上のF-マグマの圏: Mag(C, F)
  • C上のG-コマグマの圏: Comag(C, G)
  • C上の(F, G, β)-双マグマの圏: Bimag(C, (F, G, β))

(a:F(A)→A, b:A→G(B)) が双マグマである条件は、次の五角形図式が可換になることです。

可換図式より絵(ストリング図)にしたほうが分かりやすいでしょう。

絵の見方に関しては、「ベックの分配法則、ベック分配系、複合モナド // ベック分配系」の絵の周辺にちょっと書いてあります。

以上のセッティングで、次が成立します。

  • Comag(Mag(C, F), G↑β) \stackrel{\sim}{=} Bimag(C, (F, G, β))
  • Mag(Comag(C, G), F↑β) \stackrel{\sim}{=} Bimag(C, (F, G, β))

ここで:

  • G↑βは、G:CC を Mag(C, F) 上の自己関手に持ち上げたもの。
  • \stackrel{\sim}{=} は圏同型(圏同値より強い)。
  • F↑βは、F:CC を Comag(C, G) 上の自己関手に持ち上げたもの。

上の圏同型は、「ベックの分配法則、ベック分配系、複合モナド」と同様な絵(ストリング図)の計算をすれば、比較的容易に出ます。具体的な計算は今日は割愛します。

おわりに

単位や乗法を持たない単なる自己関手でも、そのアイレンベルク/ムーア圏(今の場合は、マグマ/コマグマ/双マグマの圏)を定義できます。また、ベックの分配法則が、自己関手のアイレンベルク/ムーア圏への持ち上げを誘導します。そして、前節に述べたような持ち上げ定理が成立します。

これで話はだいぶスッキリしたのですが、標準的なモナド以外に、さまざまなモナド類似物があるので、それらを系統的に記述して命名する手段がないと辛いな、と感じましたね。なんとかせねば。