檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-01-16 (月)

お稽古ごとが得意なゆりやん

| 09:14 | お稽古ごとが得意なゆりやんを含むブックマーク

ゆりやんレトリィバァさんは吉本の芸人さんです。

*1

「2013年 NSC大阪校 35期生 首席卒業」というのがどの程度優秀なのかよく分からないのですが、「R-1ぐらんぷり2015/2016」では決勝までいっています。

ゆりやんさん、ピアノは上手だし、英語の発音もソレラシイです。書道は八段ということで、お稽古ごとのたぐいを一生懸命やったのでしょうか。山田花子さんと似た話し方は好き嫌いが分かれそうですが、僕は可愛らしいと思います。

高次圏の次元について -- toward 量子と古典の物理と幾何@名古屋

| 11:26 | 高次圏の次元について -- toward 量子と古典の物理と幾何@名古屋を含むブックマーク

量子と古典の物理と幾何@名古屋」を意識してますが、この記事の内容は一般論です。高次元の圏とは、n = 0, 1, 2, ..., ∞ に対するn-圏だと思われていますが、ほんとにそれでいいのかな? という話です。

次元ごとの圏の構成素

Cが何らかの意味でn次元の圏であるとき、Cを構成するi次元(0≦ i ≦n)のモノ(射、セル)の集合を、|C|i と書きます。この書き方は比較的最近使いはじめたものですが、なかなか便利です(古い記事ではこの記法を使ってません)。

n = 0 のとき、0次元の圏Cは単なる集合なので、

  • |C|0 = C

n = 1 のとき、1次元の圏Cは通常の圏なので、

  • |C|0 = Obj(C) = (Cの対象の集合)
  • |C|1 = Mor(C) = (Cの射の集合)

この記法の背後には、n-圏の構成素(constituents)は次元を持ち、次元の値は0以上n以下の整数だという前提があります。しかし、次元の値が非負整数区間に入ると断言するのは早計でしょう。

二重圏における次元

二重圏(double category)に関しては以下の記事で扱っています。

二重圏も含めた高次圏における記号の使い方については、

Dが二重圏のとき、Dの構成素は次のようになります。

  • |D|0 = (Dの対象の全体)
  • |D|h1 = (Dの横1-射(horizontal 1-morphism)の全体)
  • |D|v1 = (Dの縦1-射(vertical 1-morphism)の全体)
  • |D|2 = (Dの2-射の全体)

Dの次元は2だと言っていいと思いますが、Dの構成素は3種類ではなくて4種類です。もし、種類を表す次元が非負整数なら、次元の値は{0, 1, 2, 3}のはずですが、実際は{0, h1, v1, 2}です。もちろん、この話は「次元」の定義に依存しますが、いまは「次元=射の分類基準」程度の意味で考えます。

この例から、次元は非負整数値とは限らない、と言えるでしょう。{0, h1, v1, 2} は次のようなダイヤモンド形の順序構造を持つと考えられます。

   2
 / \
h1    v1
 \ /
   0

一般的に、次元の集合は線形とは限らない順序集合となり、非負整数の次元は順序集合上の“高さ関数”として現れるように思えます。

{0, h1, v1, 2}に値を取る関数は、「次元」ではなく、例えば「グレード」と呼び、グレードの高さを従来通りの次元と呼ぶほうが混乱がないかも知れません。もしfが縦1-射(垂直1-射)ならば、

  • grade(f) = v1
  • dim(f) = height(grade(f)) = height(v1) = 1

次元も多様だ

特別に難しいことを考えなくても、現実のモデルを作ると、2次元/3次元の圏が出てきてしまうことは珍しくはありません。「続・2次元の圏のための記号法」でオートマトンのモデルに3次元の圏(三重圏)が出てくる、と書きました。次元は3ですが、射(セル)は8種類出てきます。前節の言葉を使うなら、グレードの値が8個、高さ関数の値が0から3です。

高次元の圏はほんとに多様です。次元(グレード)も単純な自然数だけではない多様性を持ちます。この多様性は難しさや煩雑さに繋がりますが、一方では、応用に対する選択の幅が広いことにもなります。多様性=複雑さは受け入れざるを得ないので、多様性を積極的に利用してやろう、と思ったほうが精神衛生上よいですね。

iyashiiiyashii 2017/01/18 19:33 最初ぼーっと読んでて, グレードと次元の関係が 4=2^2, 8=2^3 になってて, ちょっと面白いなあと.
が, 考えてみればn次元の有向辺の両端点はn-1次元の有向辺なのだから
n-単体の incidence poset (face poset) と同じことで,
それは頂点集合の冪集合posetだからなんてことないのかと思い直しました.

m-hiyamam-hiyama 2017/01/19 09:29 iyashiiさん、
二重圏、三重圏のように、方体(cube)ベースで考えると射の種類は2^nになりますね。
ただし、高次射の形状は方体以外にも色々あるので、次元・グレードの在り方も色々です。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170116

2017-01-13 (金)

PROと代数系 -- toward 量子と古典の物理と幾何@名古屋

| 17:33 | PROと代数系 -- toward 量子と古典の物理と幾何@名古屋を含むブックマーク

量子と古典の物理と幾何@名古屋」まで1月を切ってしまったので、話題について考えて、このブログに記録することにします。実際にこう話すとか事前に読んで欲しいとかいうものではなくて、自分の考えをまとめるために書くものです。

全体のストーリーは置いといて(まだ確定してない)、道具として(たぶん)PROを使います。なので、PROの話をします。とはいえ、PROを前面に出したりはしないでしょう。あくまで背景にPROがあるだけです。

内容:

  1. PRO
  2. 指標と等式的公理系によるPROの構成
  3. 等式的仕様の例
  4. PROと代数系の圏

PRO

PROは、prodocut(積)の最初の3文字を取った名前らしいです。酷いネーミングだな、と思いますが、既に使われている名前なので、そのまま使います。PROは特殊なモノイド圏のことです。モノイド圏PPROだとは:

  • Pの対象集合は自然数の全体Nである。
  • Pのモノイド積の対象部分は、自然数の足し算である。

より正確には、|P| がNと同型というべきでしょうが、気にしないことにして、|P| = N と考えます。定義から、PRO Pは厳密モノイド圏で、単位対象は自然数0となります。PROの例をいくつか挙げます。

  1. Nから作った離散圏(射は恒等射だけ)に、足し算でモノイド積を入れたモノイド圏。
  2. Nに大小関係の順序を考え、順序から作ったやせた圏に、足し算でモノイド積を入れたモノイド圏。
  3. 適当な係数(成分)半環Kに対する行列圏に対角ブロック和でモノイド積を入れたモノイド圏
  4. 組み紐の圏、モノイド積は組み紐の併置。「はじめての圏論 中間付録B:アミダとブレイド」参照
  5. テンパリー/リーブ圏、「テンパリー/リーブ圏とカウフマンのスケイン関係式」参照

PROは単なるモノイド圏ですが、対称モノイド圏とした場合がPROPです。nLabによると、"product category"と"products and permutations category"の略称がPROとPROPとのことです。permutationは対称(symmetry)と同じ意味なので、PROPは対称PRO(symmetric PRO)と呼んだほうが辻褄が合うと思います。

PRO, PROP(対称PRO)と同様に、自然数の足し算の上に載ったデカルト・モノイド圏はローヴェル・セオリー(Lawvere theory)とか代数的セオリー(algebraic theory)とか呼びます。「セオリー(理論)」とは言っても単に圏のことです。これも、デカルトPRO(cartesian PRO)と呼べば辻褄が合うんですが、そう呼ぶことはないですね。

一般の場合 対象が自然数
モノイド圏 PRO
対称モノイド圏 PROP
デカルト・モノイド圏 ローヴェル・セオリー

PがPROのとき、Pからモノイド圏Cへのタイト・モノイド関手を、CにおけるPモデルとか代数と呼びます。P1つの台対象(underlying object)を持つ代数系の定義とみなせます(後述)。プログラミング言語っぽい言い方をするなら、Pのモデルは「型クラスPインスタンス」と言ってもいいでしょう。

指標と等式的公理系によるPROの構成

指標と等式的公理系を使ってPROを構成しましょう。指標(signature)とは、Nを頂点集合とする箙(「形容詞「複」「多」と箙〈えびら〉」参照)のことです。指標Σは Σ = (N, A, src, trg) と書けます。ここで:

  • N自然数全体の集合
  • Aはアロー(辺)の集合
  • srcは A→N という始頂点を取る写像
  • trgは A→N という終頂点を取る写像

Nはずっと固定するので省略して、記号の乱用で Σ = (Σ, src, trg) と書きます。また、n, m∈N に対して、Σ(n, m) := {a∈Σ | src(a) = n, trg(a) = m} とします。

箙としての指標のアローをオペレーション記号(演算記号、演算子)または単にオペレーション(演算)と呼びます。オペレーション記号aに対して src(a)をaのアリティ、trg(a)をaのコアリティと呼びます。この事情から、srcをarity、trgをcoariとも書きます。

指標Σに対して、Σを含む最小のPRO(Nを対象集合とする厳密モノイド圏)が同型を除いて一意的に決まります。このPROをFreePRO(Σ)と書き、指標Σで生成された自由PROと呼びます。アミダ図、ブレイド図(「はじめての圏論 中間付録B:アミダとブレイド」参照)、カウフマン図(「テンパリー/リーブ圏とカウフマンのスケイン関係式」参照)などの図からなる圏は、自由PROです。

アミダ図、ブレイド図、カウフマン図などでは、図を同値な図で置き換えることを許してました。これは、図のあいだに同値関係があり、商集合を考えていることを意味します。自由PROに等式の集まりによる同値関係を入れ、商を取る構成は頻繁に使われます。

PがPROのとき、P上の等式とは、Pの射のペア(f, g)のことです。ただし、arity(f) = arity(g), coari(f) = coari(g) という条件が付きます。いま、Eを、P上の等式の集合としましょう。Eが与えられると、厳密モノイド圏P上の合同関係が定まります。

P上の合同関係(coguruence)とは、射の集合Mor(P)上の二項関係〜で次を満たすものです。

  • f〜g ならば、dom(f) = dom(f) かつ cod(f) = cod(g) 。
  • 各ホムセットP(n, m)上で〜は同値関係である。
  • f〜f' かつ g〜g' ならば、f;g 〜 f';g'
  • f〜f' かつ g〜g' ならば、f¥otimesg 〜 f'¥otimesg'

P上の等式の集合Eが与えられると、「(f, g)∈E ならば f〜g」を満たすような合同関係のなかで最小なものが決まります。この合同関係を〜Eとして、Mor(P) を合同関係で割ります(商集合を作る)。割った結果は再びPROになることが示せるので、それをP/E と書くことにします。(P/E)(n, m) = P(n, m)/〜E です。

指標ΣとFreePRO(Σ)上の等式の集合Eのペア(Σ, E)を等式的仕様(equational specification)と呼びます。このとき、Eを等式的公理系(equational (system of) axioms)といいます。等式的仕様(Σ, E)に対して、PRO(Σ, E) := FreePRO(Σ)/E と定義します。

等式的仕様の例

等式的仕様として、一番よく引き合いに出される例はモノイド仕様でしょう。指標Σを次のように定義します。

  • Σ(2, 1) = {μ}
  • Σ(0, 1) = {ε}
  • その他のΣ(n, m) = {}

FreePRO(Σ)の結合(の記号)を「;」、モノイド積を「¥otimes」とします。対象に関しては、n¥otimesm = n + m です。E = {assoc, lunit, runit} として、それぞれの等式は次のようにします。

  • assoc = ((μ¥otimesid1);μ, (id1¥otimesμ);μ)
  • lunit = ((ε¥otimesid1);μ, id1)
  • runit = ((id1¥otimesε);μ, id1)

もう少し普通の書き方をすると:

  • μ:2→1
  • ε:0→1
  • assoc:: (μ¥otimesid1);μ = (id1¥otimesμ);μ : 3→1
  • lunit:: (ε¥otimesid1);μ = id1 : 1→1
  • runit:: (id1¥otimesε);μ = id1 : 1→1

以上で決まる等式的仕様が「モノイドの仕様」です。

(Σ, E)がモノイドの仕様のとき、厳密モノイド圏PRO(Σ, E)から(厳密とは限らない)モノイド圏Cへのタイト・モノイド関手FがPRO(Σ, E)のモデルまたは代数です。今の場合は、モデルはモノイド圏C内のモノイドになります。F(1)∈|C| がモノイドの台対象となります。F(n) = F(1)¥otimesn と、自然数nに対する値はF(1)のモノイド積累乗になります。

モノイド圏Cを変えると、色々なモノイド概念が得られます。通常のモノイド(集合圏のモノイド)以外に、結合的多元環(ベクトル空間の圏のモノイド)やモナド(自己関手圏のモノイド)などがあります。

可換モノイドを定義するには、変数を入れ替える σ:2→2 を指標に入れて、入れ替え(置換、対称)の等式的公理系を追加しておく必要があります。このような手間を省くには、最初から対称が入ったPROP(対称PRO)を使えば楽です。同様に、変数のコピーと破棄も必要なら、ローヴェル・セオリー(代数的セオリー、デカルトPRO)を使えばいいでしょう。

PROと代数系の圏

2つのモノイド圏C, Dに対して、TightMon(C, D)はタイト・モノイド関手の全体とします。モノイド自然変換も一緒に考えることにして、TightMon(C, D)は圏として扱います。

(Σ, E)を前節で定義したモノイドの仕様として、タイト・モノイド関手 PRO(Σ, E)→CC内のモノイドを決めます。つまり、C内のモノイドの全体をMon(C)とすると:

  • Mon(C) = TightMon(PRO(Σ, E), C)

モノイドという代数系とその準同型射からなる圏は、モノイド仕様(Σ, E)に対するPROからの関手圏として定義できるわけです。

これはモノイドに限らず、単一の台対象(underlying object)を持つ代数系(単ソート代数という)は、適当なPRO(あるいはPROP、ローヴェル・セオリー)からの関手とみなせます。当該の代数系と準同型射のなす圏は、関手圏として構成できます。

以上のことは、「代数系を関手で表現できる」ことを意味します。逆に考えると、「関手を代数系で表現できる」可能性も示唆します。実際、タチの良い関手は代数系エンコードできることがあります。

「量子と古典の物理と幾何@名古屋」では、とある現象を定式化する関手を、代数系エンコードする事例を示すつもりです(予定)。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170113

2017-01-12 (木)

弱2-圏内のモナドに関する補足:モナドが作る2-圏の多様性

| 13:05 | 弱2-圏内のモナドに関する補足:モナドが作る2-圏の多様性を含むブックマーク

モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き)に補足をしておきます。

Bが弱2-圏(双圏)として、B内のモナドからなる弱2-圏を次のように構成しました。

  • |MonadB|0 = (B内のモナドの全体)
  • |MonadB|1 = (B内の左斜め加群の全体)
  • |MonadB|2 = (B内の左斜め加群準同型の全体)

MonadBの対象(0-射、0-セル)であるモナドはいいとして、1-射や2-射とその結合演算に関しては他の選択肢もあります。

0-射であるモナドと1-射である左斜め加群はそのままとして、2-射を変更してみます。Mが対象X上のモナド、Nが対象Y上のモナドとします。F, G:X→Y in B、α::M*F⇒F*N:X→Y in B、β::M*G⇒G*N:X→Y in B で、(F, α)と(G, β)は左(M, N)-斜め加群になっている状況を考えます。

このとき、左斜め加群のあいだの準同型φを、φ::F⇒G:X→Y ではなくて、φ::F⇒G*N:X→Y の形の2-射だとします。Bの2-射φは次の条件を満たすとします。

この図で、白丸はφ、線の交差は“斜め作用”αとβ、黒丸はモナド乗法です。

このような準同型を、図の形状からバイデント準同型(bident homomorphism)と呼びましょう。バイデントとは下のオジサンが持っている二股槍のことです。(BSDのデーモン君は三股槍です。)

*1

バイデント準同型の横結合「*」と縦結合「;」は次のように定義します。白丸がバイデント準同型の2-射、交差は斜め作用、黒丸はモナド乗法です。

こうやって定義したバイデント2-射が準同型の条件を満たすことは良い練習問題です。

以上から、次のような弱2-圏も作れることが分かります。

  • |MonadbidentB|0 = (B内のモナドの全体)
  • |MonadbidentB|1 = (B内の左斜め加群の全体)
  • |MonadbidentB|2 = (B内の左斜め加群のバイデント準同型の全体)

左斜め加群の代わりに右斜め加群にしても事情は同じでが、両側斜め加群という構造も定義できます。両側斜め加群を1-射とする弱2-圏も定義できます。

斜め加群ではなくて、通常の両側加群(双加群)を1-射とすることも考えられます。両側加群のときは横結合が難しくなります。代数的な発想では、両側加群の横結合はテンソル積です。行列計算の発想では、横結合は行列の積です。どちらの発想に基づいても、具体的な構成に手間がかかることもあります。

モナド概念を固定しても、「モナドのあいだの準同型」「モナドのあいだの準同型のあいだの準同型」という概念は一意的には決まらないようです。適用分野や目的ごとに選ぶことになるのでしょう。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170112

2017-01-11 (水)

モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き)

| 17:16 | モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き)を含むブックマーク

お正月に考えてみたことを記します。書くのにけっこう時間がかかりました。長いです。

圏の基本事項を学んだ後にモナドの概念が導入されます。しかし、モナド概念を使って圏を調べるということも出来そうです。「圏論モナド論 → 圏論」という循環が生じますが、こんな循環はしょっちゅう生じる現象なので気にする必要はありません。

狭義の圏論(あくまで狭義)とは、圏Catを調べることだと言っていいでしょう。Catには、圏、関手以外に自然変換も含まれるとして、2次元の圏と捉えましょう。2次元の圏Catよりも扱いやすかったり、豊富な構造を持つナニモノカをXCatとします。うまいXCatが見つかると、通常の圏論がより簡単になったり、より面白くなったりするかも知れません。

そんなXCatを定義し調査することを、仮に代替圏論と呼ぶことにします。ここでは、モナドの構成をヒントにして、(ひとつの)代替圏論を試みてみます。まだ詰めは甘い話です。予備知識に関して、弱2-圏(双圏)の事などけっこう説明してますが、それでもself-containedではないので、必要に応じてnLabなどを参照しながら読んでください。

この記事のアイディアは、(お正月に眺めた)次のラックの論文に基づくものです。

内容:

  1. モノイド、モナド、圏
  2. 代替圏論の枠組と効能
  3. 圏論の用語法の問題点と対策
  4. 2-圏と2-関手の図示法
  5. スパンの弱2-圏 = 二部箙の弱2-圏
  6. 2-圏の例 10選
  7. 単対象2-圏からのラックス2-関手
  8. 自明な2-圏
  9. 自明な2-圏からのラックス2-関手
  10. 弱2-圏BipartQuiv内のモナドは圏
  11. 左斜め加群と右斜め加群
  12. 左斜め加群の圏
  13. ラックス2-関手の2-圏
  14. まとめと展望

モノイド、モナド、圏

モナドが一種のモノイドであることはよく知られています。モナドは、自己関手(endofunctor)の圏のなかのモノイドになっています。では、モノイドとモナドを全く同じように扱うか、というと、そうではありません。特定のモナドは特定の圏C上の自己関手圏 EndCat(C) = Cat(C, C) 内に存在しますが、すべてのモナドを考えるときは、Cを動かさなくてはなりません。Cを小さい圏に限るなら、モナドはすべての小さい圏の圏Catの2次元構造(自然変換を含む構造)のなかに棲んでいることになります。

モナドCat内に居る生き物であるのに対して、通常のモノイドは集合の圏Setのなかに棲んでいて、集合と写像から構成されます。モノイドとモナドの特徴をまとめると:

モノイド モナド
構成要素 集合と写像 圏と関手と自然変換
環境となる圏 集合圏Set 圏の圏Cat
環境となる圏の次元 1次元 2次元

モノイドとモナドは類似の構造であるが、「構造の次元が違う」と言えます。

ところで圏は、これまた一種のモノイドとみなせます。小さな圏だけを考えるとして、集合Xを対象集合とする圏Cは、Xを頂点集合とする有向グラフの圏Graph[X]のなかのモノイドとなります。モナドのときと同様に、すべての圏を考えるときは、Xを動かさなくてはなりません。このことから、モナドの構成と圏の構成に類似性があるだろう、と見当が付きます。

  1. 特定の圏C上のモナドCat(C, C)内のモノイドであるのと同様に、特定の集合X上の圏はGraph[X]内のモノイドとなる。
  2. モナドと圏は、共通の構成法を持つだろう。局所的には(CやXを固定すれば)どちらもモノイドなのだから。
  3. モナドが2次元の圏Cat内に棲むように、圏もなんらかの2次元の圏(生息環境)のなかに存在するのだろう。

代替圏論の枠組と効能

前節の見通しに従って、代替圏論を試みてみましょう。通常の“圏の圏”Catに変わる新しい“圏の圏”をXCatと書くことにします。Xは未知なるモノとしてのエックスと、extendedの意味で付けています。

細部の説明は後回しにして、結論を先に言ってしまうと、XCat = Lax2(1(2), SPAN(Set)) が新しい“圏の圏”の定義です。この定義は、モナドの全体が Lax2(1(2), Cat) と書けることをヒントにしたものです。より一般には、(小さいとは限らない)双圏Bに対して Lax2(1(2), B) という構成法があり、その2つの事例がモナドと圏の構成法になっています。

XCatが通常のCatよりメリットがある点を述べておきます。Lax2(1(2), SPAN(Set)) という定義のなかに、集合圏Setが含まれますが、これは終対象とファイバー積(プルバック)を持つ任意の圏*1に置き換えることができます。つまり、XCatは終対象/ファイバー積を持つ圏でパラメトライズされているのです。

  • XCat(C) = Lax2(1(2), SPAN(C))

ベースとなる圏Cを取り替えることにより、Set以外をベースとした圏論を展開できます。これは、Cの内部圏の理論に対応します。XCatの定義のなかには、SPAN(-), 1(2), Lax2(-, -) なども含まれます。これらを一般化したり取り替えることにより、別な圏概念が得られる可能性もあります。

XCatはあからさまにモナドと類似しています。なので、モナドに関する概念を圏に持ち込むことが(ある程度は)できるでしょう。例えば、ベックの分配法則により2つのモナドの複合モナドを構成できます。同様に、2つの圏の複合圏(直積や直和ではない)を構成できるかも知れません*2テンソル強度(tensorial strength)と強モナド(strong monad)という概念に対応する強圏(strong category)という概念も定義可能かも知れません。逆に、圏同値や随伴対は圏論の概念ですが、モナド側ではどんな概念でしょうか?

思いついたばかりでロクに考えてないので、楽観的な期待感を述べているだけですが、けっこう面白い気がします。

圏論の用語法の問題点と対策

XCatの定義である Lax2(1(2), SPAN(Set)) について説明したいわけですが、圏論の用語法の不統一性と混乱が説明とコミュニケーションの障害となります*3。今回の話では、メジャーな用語法に従うと表現が破綻してしまうので、破綻を回避する言葉づかいを選択します。用語法を改善するだけで、難解さが格段にやわらいだりします*4

まず「n-圏」という言葉ですが、これは n = 0, 1, 2, ... に対するn次元の圏の意味です。強n-圏(strong n-category)と弱n-圏(weak n-category)という区別があります。最近では、単にn-圏というとそれは弱n-圏を意味することが多いです。また、「強」よりは「厳密(strict)」を使うことが多くなっていると思います。「弱」は「非厳密(non-strict)も許す」の意味です。ここでの非厳密とは、「イイカゲンで当てにならない」という意味では無いですよ! 厳密性も非厳密性もチャンと(厳密に)定義された概念です。ややこしいのは、厳密n-圏を弱n-圏の特殊なモノとみなす場合(これが普通)と、「弱=非厳密」という用法があることです。ここでは、「弱=厳密または非厳密」です。

n = 2 の場合は例外的で、単に2-圏というと、厳密2-圏の意味です。弱2-圏は双圏と呼びます。n = 2 だけ用語法が違っているのです。しかも、「双」という厄介な形容詞が付いています(「「余」と「双」の使い方がバラバラ」参照)。この記事では、これから先「双圏」は使わず、弱2-圏を使います。通常の「2-圏」は厳密2-圏と形容詞「厳密」を付けます。厳密2-圏は弱2-圏の特別なモノです。厳密・非厳密が文脈から明らかなときや、厳密・非厳密を気にする必要がないときは単に「2-圏」ということもあります。

弱2-圏のあいだの関手をなぜか疑関手(pseudofunctor)と呼びます。この「擬」の用法は他の用語との統一性・整合性がまったく無いので使用せず、2-関手と呼ぶことにします。

ただし、2-関手には種類があります。この種類はモノイド圏のときと形容詞を合わせて、次のように呼びます。

  1. 厳密2-関手(strict 2-functor)
  2. タイト2-関手(tight 2-functor)
  3. ラックス2-関手(lax 2-functor)
  4. 反ラックス2-関手(oplax 2-functor)

これらの呼び名(形容詞)については、「モノイド圏の随伴性を“豊饒圏の圏”の随伴性に持ち上げる: 計画編」でも言及してます。「タイト」という形容詞は一般的ではありませんが、形容詞「強」や形容詞なしによる混乱を避けるために「タイト」を使います。

「強」の代わりに「厳密」「タイト」を使うのは、「テンソル強度を持つ(with tensorial strength)」の意味で形容詞「強」を使う習慣があり、様々な意味の「強」がかち合ってしまうからです。「強」はテンソル強度の意味だけに使うようにします。

実は、疑関手を弱2-関手(weak 2-functor)と呼ぶ人もいます。強モノイド関手の「強」を流用するなら、疑関手は強2-関手となります。すると、疑関手=弱2-関手=強2-関手 というハチャメチャな状況になります。この点からも、形容詞「強(strong)」は避けるべきと思います。僕の過去の記事では「強」を使っているのですが、それはご容赦ください。

モノイド圏は、単対象(対象がひとつだけ、single-object)の2-圏と考えることができます。一般の2-圏と単対象2-圏に同じ用語法を適用するようにします。これで、だいぶスッキリします。

一般の2-圏 単対象の2-圏
厳密な圏 厳密2-圏 厳密モノイド圏
非厳密な圏 弱2-圏 モノイド圏
厳密関手 厳密2-関手 厳密モノイド関手
タイト関手 タイト2-関手 タイト・モノイド関手
ラックス関手 ラックス2-関手 ラックス・モノイド関手
反ラックス関手 反ラックス2-関手 反ラックス・モノイド関手

2-圏には、対象と射以外に2次元の構成素がありますが、これは2-射と呼ぶことにします。2-セル、または単にセルと呼ぶこともありますが、基本的な(生成元となる)2-射を2-セルと呼ぶこともあるので、今回は用語「2-射」を採用します。0-射は対象、1-射は通常の射のことです。

2-圏と2-関手の図示法

弱2-圏はモノイド圏の拡張であり、モノイド圏は弱2-圏の特殊ケースです。このため、弱2-圏の定義はモノイド圏と非常によく似ています。単対象の2-圏がモノイド圏なのですが、通常は次元をズラして記述します。この事情を表にまとめておきます。次元のズレで混乱してしまう人は多そうなので注意してください。

単対象の2-圏 モノイド圏
0-射(ただ1つ) 考えない
1-射 対象(0-射)
2-射 射(1-射)
ホム圏 モノイド圏全体
1-射の横(水平)結合 対象のモノイド積
2-射の縦(垂直)結合 射の結合
2-射の横(水平)結合 射のモノイド積

一般の2-圏(弱2-圏)とモノイド圏の違いは、対象がたくさんある(multi-object)かどうかだけです。一般の2-圏(弱2-圏=双圏)の形式的な定義はnLabのエントリーを参照してもらうとして、ここでは2-圏の“描き方”を述べます。

ストリング図を使う場合は、2-圏の対象、射、2-射の描き方はモノイド圏の場合とほとんど同じです。異なるのは、背景色が“単色”から“多色”になるだけです。ここで背景色とは、対象(0-射、0-セル)を表す領域の色のことです。

念のために、2-圏の構成要素(constituent, entity)と図形の対応を示しましょう。

2-圏 ストリング図
対象(0-射) 面(領域)
射(1-射 ) 辺(ストリング、ワイヤー)
2-射 頂点(ドット、ボックス、丸など)

モノイド圏の場合は、暗黙の(言及されない)0-射を表す平面領域が単色(または無色)だったのに対して、2-圏では様々な色(あるいはラベル)で識別されます。

絵の実例に関しては、「絵算のススメ 2015 年末版」で紹介したマースデンの論文などを参照してください。

2-圏のあいだの2-関手、特にラックス2-関手の図示にはマッカーディのストライプ図を使うのが便利です。ストライプ図については、次の記事を参照してください。

次は多色のストライプ図の例です("Frobenius Morphisms of Bicategories"より)。

ストライプ図は、モノイド圏を含む2次元の圏とそのあいだの関手の計算に大変便利な道具です。

スパンの弱2-圏 = 二部箙の弱2-圏

弱2-圏とそのあいだの関手の準備ができれば、XCat = Lax2(1(2), SPAN(Set)) という定義の説明ができます。1(2)とSPAN(Set)は弱2-圏であり、これらの弱2-圏のあいだのラックス2-関手の全体が Lax2(1(2), SPAN(Set)) です。(後で、Lax2(-, -)上に2-圏構造を入れますが、今は気にする必要はありません。)

まずは弱2-圏SPAN(Set)ですが、これは「スパンの圏と行列の圏」で説明しています。「スパンの圏と行列の圏」の目的は、SPAN(Set)とMAT|Set|Set が事実上同じであることを説明することでした。SPAN(Set)が弱2-圏(双圏)であることを強調してませんが、圏係数行列の圏とみたときの行列の積が横結合を与えます。

弱2-圏の概念 圏係数行列の圏の概念
対象 添字集合
1-射 (対象の)行列
2-射 射の行列
1-射の横結合 行列の積
2-射の縦結合 射の行列の結合
2-射の横結合 射の行列の積

集合圏Setが係数圏のとき、行列の係数(成分)は集合(1-射)または写像(2-射)となります。形式上は、通常の行列計算と同じ計算ができます。

弱2-圏SPAN(Set)は、行列表示以外の別な表示も持ちます。SPAN(Set)の1-射は箙〈えびら〉とみなせるのです。(quiver)は有向グラフ(directed graph)と同義です(この言葉を選んだ事情は「形容詞「複」「多」と箙〈えびら〉」、応用例は「高次圏の下部構造を箙〈えびら〉で表現してみる」を参照してください)。代替圏論のためには、SPAN(Set)を箙で解釈するのが便利です

集合V, Eと、写像 src, trg:E→V の組 (V, E, src, trg) が箙です。頂点の集合Vを2つの集合X, Yに分けて、src:E→X, trg:E→Y としたモノを二部箙(bipartite quiver)と呼びます。もちろん、二部グラフ(bipartite graph)とも呼びます、というか、二部グラフが普通の呼び名です。

A = (X, Y, E, src, trg) を二部箙とします。二部箙の有向辺をアローとも呼びます。アローは始頂点集合Xに始点を持ち、終頂点集合Yに終点を持つことになります。x∈X, y∈Y に対して A(x, y) := {f∈E | src(f) = x, trg(f) = y} とすると、(x, y)|→A(x, y) という対応は、X×Y→|Set| となるので集合係数行列を定めます。これが、二部箙と集合係数行列を同一視する方法です。

二部箙を記述するために、X, Y, Eのような文字をたくさん消費するのはイヤなので、次のように約束します。

  • 記号の乱用で、アロー(有向辺)の集合EをAと書く。(二部箙全体と同じ記号を使う。)
  • X = Src(A), Y = Trg(A) と書く。
  • 異なる箙に属するsrc, trgを区別したいときは、srcA, trgAのように添字を付ける。
  • 以上の約束のもと、A = (Src(A), Trg(A), A, srcA, trgA) と書ける。

二部箙の全体が構成する弱2-圏をBipartQuivとします。BipartQuivはSPAN(Set)と同じものです -- この2つは、メンタルモデルの違いしかないと言っていいでしょう。念のために弱2-圏BipartQuivの仕様を箇条書きにしておきましょう。|-|iは弱2-圏を構成するi次元の構成素(i-射、i-セル)の全体の集合です。

  1. Obj(BipartQuiv) = |BipartQuiv|0 は、すべての集合からなる類である。
  2. Mor(BipartQuiv) = |BipartQuiv|1 は、すべての二部箙からなる類である。
  3. X, Y∈Obj(BipartQuiv) に対して、ホム圏 BipartQuiv(X, Y) が定義できる。以下にホム圏の定義:
  4. ホム圏BipartQuiv(X, Y)の対象(BipartQuivの射)は、Src(A) = X, Trg(A) = Y であるような二部箙 A = (X, Y, A, srcA, trgB) である。
  5. ホム圏BipartQuiv(X, Y)の射(BipartQuivの2-射) F:A→B は、箙のアロー集合のあいだの写像であって、srcとtrgを保存するものである。F:A→B in BipartQuiv(X, Y) を、弱2-圏BipartQuivの2-射とみるときは、F::A⇒B:X→Y と書く。
  6. ホム圏BipartQuiv(X, Y)の結合(BipartQuivの2-射の縦結合)は、写像の結合(合成)である。
  7. ホム圏BipartQuiv(X, Y)の恒等射(BipartQuivの恒等2-射)は、恒等写像である。
  8. 二部箙(BipartQuivの1-射)(X, Y, A, srcA, trgA)と(Y, Z, B, srcB, trgB)の横結合は、スパンの横結合として定義する。集合Y上のファイバー積を使う。
  9. BipartQuivの2-射 F::A⇒A':X→Y G::B⇒B':Y→Z の横結合は、写像のファイバー積として定義する。
  10. 集合Xに対する自明な二部箙 (X, X, X, idX, idX) が、横結合に対する単位となる。

ホム圏BipartQuiv(X, Y)において X = Y としたエンド圏BipartQuiv(X, X)をQuiv[X] と書くことにします。するとQuiv[X]は、Xを頂点集合とする通常の箙(有向グラフ)となります(箙と有向グラフは同義なので、Quiv[X] = Graph[X])。BipartQuivの横結合がQuiv[X]内ではモノイド積になり、Quiv[X]はモノイド圏となります。このモノイド圏Quiv[X]のなかのモノイド対象が、対象集合をXとする小さな圏となることに注意してください -- 後でこの事実を系統的に定式化します。

2-圏の例 10選

高次圏の話はどうしても抽象的になってしまうので、具体例が欲しくなります。2-圏の具体例を幾つか挙げておきます。次元0, 1, 2の構成素と三種類の結合(compositions)だけ示します。

1. 圏の圏

前節で説明したBipartQuiv(SPAN(Set)と同じ)は非厳密2-圏です。厳密2-圏の典型例は圏の圏Catでしょう。

  • 対象は、(小さい)圏である。
  • 射は、関手である。
  • 2-射は、自然変換である。
  • 射の横結合は、関手の結合である。
  • 2-射の縦結合は、自然変換の縦結合である。
  • 2-射の横結合は、自然変換の横結合である。
2. 順序集合の圏

順序集合の圏Ordは、厳密2-圏の例になります。Ordは簡易版Catのようなものです。「n-圏とは何だろう」の主要な例になっているので、詳細はそちらを参照してください。

  • 対象は、順序集合である。
  • 射は、単調写像(順序を保つ写像)である。
  • 2-射は、単調写像のあいだの順序である。
  • 射の横結合は、単調写像の結合である。
  • 2-射の縦結合は、単調写像のあいだの順序の推移律である。
  • 2-射の横結合は、単調写像の結合の順序(に関する法則)である。
3. モノイド圏

モノイド圏はただ1つの対象を持つ弱2-圏でした。厳密モノイド圏は単対象の厳密2-圏です。直積を入れた集合圏やテンソル積を入れたベクトル空間の圏は非厳密2-圏です。

  • 対象は、0(なんでもいい)である。
  • 射は、モノイド圏の対象である。
  • 2-射は、モノイド圏の射である。
  • 射の横結合は、モノイド圏の対象のモノイド積である。
  • 2-射の縦結合は、モノイド圏の射の結合である。
  • 2-射の横結合は、モノイド圏の射のモノイド積である。
4. 2-離散な2-圏

任意の圏Cに対して、恒等2-射だけを持つ2-離散な厳密2-圏を作れます。こうしてCから作った厳密2-圏をC(2)と書くことにします。

  • 対象は、Cの対象である。
  • 射は、Cの射である。
  • 2-射は、Cの射 f:X→Y ごとの idf::f⇒f:X→Y である。(その他の2-射はない。)
  • 射の横結合は、Cの射の結合である。
  • 2-射の縦結合は、恒等2-射の自明な結合である。(特に考える必要はない。)
  • 2-射の横結合は、iff;idg = idf;g で与えられる。
5. 順序半環係数の行列の圏

K = (K, +, 0, ・, 1, ≦) が順序半環のとき、K係数(Kを成分とする)行列の圏は厳密2-圏の構造を持ちます。K = N自然数に、常識的な順序半環構造) とか K = ({true, false}, ∨, false, ∧, true, (true<false とする順序)) が事例です。より詳しくは「これならいじれるぞ、2-圏の簡単な例」を参照してください。

  • 対象は、自然数である。
  • 射は、K係数の行列である。
  • 2-射は、成分ごとに比較する順序関係である。
  • 射の横結合は、行列の積である。
  • 2-射の縦結合は、行列のあいだの順序の推移律である。
  • 2-射の横結合は、行列の積の順序(に関する法則)である。
6. 関係圏

関係圏Relも順序構造を考慮すると厳密2-圏になります。これは、すぐ上の例である行列の圏で、真偽値半環を係数とした場合の拡張です。同様な拡張は任意の順序半環に対して行えます。「スパンの圏と行列の圏」も参照してください。

  • 対象は、集合である。
  • 射は、集合のあいだの関係である。
  • 2-射は、関係のあいだの包含関係である。
  • 射の横結合は、関係の結合である。
  • 2-射の縦結合は、関係のあいだの包含関係の推移律である。
  • 2-射の横結合は、関係の結合の包含関係(に関する法則)である。
7. アルファベット集合と翻訳の圏

クリーネスターと関係圏を利用して、形式言語理論で使える厳密2-圏を定義できます。

  • 対象は、集合(アルファベット集合)である。
  • 射は、文字列のあいだの翻訳である。アルファベットX上の文字列からアルファベットY上の文字列への(非決定性で線形な)翻訳は、X→Y* という非決定性写像とする。ここで、上付きスターはクリーネスター。
  • 2-射は、翻訳をクリーネスターのあいだの関係と見ての包含関係である。(非決定性写像は関係とみなせる。)
  • 射の横結合は、関係の結合である。
  • 2-射の縦結合は、関係のあいだの包含関係の推移律である。
  • 2-射の横結合は、関係の結合の包含関係(に関する法則)である。
8. 入出力を持つオートマトンの圏

入出力を持つ非決定性オートマトンは、次のようなモノで構成されます。

  1. 入力アルファベット集合X
  2. 出力アルファベット集合Y
  3. 状態集合S(空ではない)
  4. 状態遷移非決定性写像(あるいは遷移関係) δ:X×S→S×Y*
  5. 始状態の集合 I∈S
  6. 終状態の集合 F⊆S

入出力を持つオートマトンの全体は、入出力の結合と模倣関係により弱2-圏を構成します。その記述はちょっと長くなるので今回は割愛します。S = {0} と固定すると、すぐ上の例と同じになります。

9. 0次元のコボルディズム圏

微分同相による同値関係で割る前のコボルディズム圏は厳密2-圏になります。幾何的次元(扱う多様体の次元)が高くなると記述が面倒ですが、0次元なら簡単に記述できます。

  • 対象は、有限個の点である。
  • 射は、n個の始点とm個の終点を境界とするコンパクトでなめらかな1次元有向多様体である。
  • 2-射は、なめらかな1次元有向多様体のあいだの境界を固定したなめらかな写像である。微分同相写像に限定する場合が多いが、ここでは任意のなめらかな写像とする。
  • 射の横結合は、終点境界と始点境界を貼り合わせることである。
  • 2-射の縦結合は、なめらかな写像の結合である。
  • 2-射の横結合は、なめらかな写像を貼り合わせることである。
10. 双加群の圏

代数的な例として、双加群(両側加群)の弱2-圏があります。

単対象2-圏からのラックス2-関手

圏の次元が上がると、関連する定義や記述が面倒になってきます。2次元でも既に、関手の構造はけっこう複雑です。以前、ラックス・モノイド関手の説明はしたことがあるので、ラックス・モノイド関手の拡張としてラックス2-関手を定義しましょう。

一般的な弱2-圏をA, Bなどとします。弱2-圏の構成素を表す記号は次のように約束します。

  • 対象は、X, Yなどの大文字で表す。
  • 射は、f, gなどの小文字で表す。
  • f:X→Y のとき、X = left(f), Y = right(f) と表す(dom, codは2-射に関して使うことにする)。
  • 2-射は、α, βなどのギリシャ文字で表す。
  • α::f⇒g:X→Y のとき、f = dom(α), g = cod(α), X = left(α), Y = right(α) と表す。
  • 射の横結合はf*gで表す(f;gではないので注意)。
  • 2-射の縦結合はα;βで表す。
  • 2-射の横結合はα*βで表す。(射のときと同じ記号を使う。)
  • 対象Xに対する単位射はunitXで表す(idXではない)。unitXは横結合*に対する単位(中立元)となる。
  • 射fに対する恒等2-射をidfで表す。idfは縦結合;に対する恒等(中立元)になる。
  • unitXのidは、idunitX と書く。

この約束はこの記事のローカルルールで、記法の選択に特に根拠はありません(けど、なにかしらの約束は必要です)。次元を明示すれば、このような約束は不要ですが、とても煩雑になります。以上の約束により、次のような“みなし”が導入されます。

  • 大文字Xは、暗黙に X∈|A|0 とみなす。
  • 小文字fは、暗黙に f∈|A|1 とみなす。
  • ギリシャ文字αは、暗黙に α∈|A|2 とみなす。
  • *は、|A|1×|A|1→|A|1 という部分写像である。
  • ;は、|A|2×|A|2→|A|2 という部分写像である。
  • *は、|A|2×|A|2→|A|2 という部分写像で、同じ記号がオーバーロードされている。
  • unitは、|A|0→|A|1 という写像である。
  • idは、|A|1→|A|2 という写像である。
  • idunitは、|A|0→|A|2 という写像である。

次元がもっと高くなると、「文字種によって次元を区別する」「次元ごとに別な名前で呼ぶ(例:「単位」と「恒等」)」ような約束は使えなくなります。一般的な表記法のヒントは「高次圏の下部構造を箙〈えびら〉で表現してみる」にあります。

さて、弱2-圏Aの対象が1個だけの場合を考えます。ただ1つの対象をXとします。この場合、ラックス2-関手はラックス・モノイド関手とほとんど同じものです。ラックス・モノイド関手については、次の記事を参照してください。

Aが単対象の弱2-圏(モノイド圏)のとき、AからBへのラックス2-関手は次のモノから構成されます。

  1. Bの対象Y
  2. Aのホム圏A(X, X)からBのホム圏B(Y, Y)への関手F
  3. B(Y, Y)の射(Bの2-射) ε:unitY→F(unitX)
  4. ホム圏A(X, X)の2つの対象(Aの射)f, gを添字に持つB(Y, Y)の射(Bの2-射)の族 μf, g:F(f)*F(g)→F(f*g)

対象がXだけの場合は、弱2-圏Aとそのホム圏A(X, X)は同じものです。それにも関わらず、構成素の次元はズレます。一般に、2つのモノを繋ぐホム構造の次元は下がるので、ホム構造内での構成素の次元も下がります。

弱2-圏の構成素 ホム圏の構成素
対象X なし
射 f:X→Y 対象 f
2-射 α::f⇒g:X→Y 射 α:f→g

同じfやαの次元が、見方により変わるのです。

  • (f:X→Y in A) = (f in A(X, X))
  • (α::f⇒g:X→Y in A) = (α:f→g in A(X, X))

以上に説明した (1) Y∈|B|0, (2) ホム圏のあいだの関手 F:A(X, X)→B(Y, Y), (3) ε::unitY⇒F(unitX):Y→Y in B, (4) μf,g::F(f)*F(g)⇒F(f*g):Y→Y in B の組み合わせは、特定の法則を満たすことを要求されます。その法則は、結合律、左単位律、右単位律です。

以下は、結合律と左単位律(右単位律は左と同様)を示すストライプ図です。

テキスト表記と可換図式を使ったラックス2-関手の詳細な記述は、nLabの定義を参照してください。

いま定義した(Y, F, μ, ε)は、一般的なラックス2-関手ではなくて、単対象2-圏(モノイド圏と同じモノ)からのラックス2-関手です。今回の目的では、単対象2-圏からの関手で十分なので、一般的なラックス2-関手の説明はしません。(必要なら、すぐ上のnLab記事などを参照。)

自明な2-圏

XCat = Lax2(1(2), SPAN(Set)) に登場する1(2)は自明な2-圏です。自明な2-圏は、空な2-圏(何もない)を除けば、2圏のなかで最も簡単なものです。簡単過ぎてかえって分かりにくい存在かも知れません。

1(2)以外に、自明な0-圏1(0)、自明な1-圏1(1)も一緒に説明しましょう。記法を単純にするために:

  • I := 1(0)
  • J := 1(1)
  • K := 1(2)

とします。これから I, J, K について考えます。

Iは単なる集合で、I = {0} とします。Jは通常の圏で、

  • 対象:|J|0 = I = {0}
  • 射: |J|1 = {1}
  • dom, cod: dom(1) = cod(1) = 0
  • 恒等: id0 = 1
  • 結合: 1;1 = 1

2-圏Kは、1-圏Jに恒等2-射を付け加えて2-離散な2-圏です。具体的に定義しましょう。

  • 対象:|K|0 = I = {0}
  • 射: |K|1 = |J|1 = {1}
  • 射のleft, right: left(1) = right(1) = 0
  • 単位: unit0 = 1
  • 射の横結合: 1*1 = 1
  • 2-射: |K|2 = {2}
  • left, right: left(2) = right(2) = 0
  • dom, cod:dom(2) = cod(2) = 1
  • 恒等: id1 = 2
  • 2-射の縦結合: 2;2 = 2
  • 2-射の横結合: 2*2 = 2

すべての定義が自明ですが、それでもややこしいところがあります。Kの2-射を捨てて、対象と射を考えると通常の圏(1-圏)になります。その圏をK1とすると:

  • K1 ¥stackrel{¥sim}{=} J

一方、2-圏Kのホム圏K(0, 0)も通常の圏でJと同型な圏です。

  • K(0, 0) ¥stackrel{¥sim}{=} J

しかし、K1K(0, 0)は違う圏です。K1の構成素は{0, 1}、K(0, 0)の構成素は{1, 2}です。次元が高いほうを捨てて作ったのがK1で、次元が低いほうを忘れて次元をズラして作ったのがK(0, 0)です。また、ホム圏K(0, 0)には横結合に由来するモノイド積*が入り、モノイド圏となります。結合もモノイド積も実質は同じ演算ですが、K(0, 0)は名目上2つの演算を持つのです。

自明な2-圏からのラックス2-関手

1(2)は単対象の2-圏なので、1(2)から弱2-圏Bへのラックス2-関手は次のモノで決まります。

  1. Bの対象X
  2. ホム圏1(2)(0, 0)からホム圏B(X, X)への通常の関手
  3. F(-)*F(-) から F(-*-) への自然変換 μ::F(-)*F(-)⇒F(-*-):1(2)(0, 0)×1(2)(0, 0)→B(X, X)
  4. ε:unitX→F(1) in 1(2)(0, 0) (ε::unitX⇒F(1):X→X in B

結局、横結合をモノイド積とするモノイド1(2)(0, 0)から、同様に作ったモノイド圏B(X, X)へのラックス・モノイド関手(F, μ, ε)がラックス2-関手となります。モノイド圏としての1(2)(0, 0)は自明なモノイド圏なので、(F, μ, ε)はモノイド圏B(X, X)内のモノイド(F(1), μ1,1, ε)と同じことです -- このことは次の記事に書いてあります。

「モノイド圏B(X, X)内のモノイド」の別な言い方が、「弱2-圏B内のX上のモナド」です。よって、次の3つの概念は同じです。

  1. 自明な2-圏1(2)から弱2-圏Bへのラックス2-関手
  2. 弱2-圏Bのホム・モノイド圏B(X, X)内のモノイド
  3. 弱2-圏B内のX上のモナド

特に、B = Cat とした場合が、通常のモナドとなります。

弱2-圏BipartQuiv内のモナドは圏

いよいよ(やっと)、圏(小さい圏)の別定義を述べることができます。我々の代替圏論における圏とは、二部箙の弱2-圏BipartQuiv内のモナドです。BipartQuivの対象Xを選ぶと、X上のモナドは、ホム・モノイド圏BipartQuiv(X, X)内のモノイドです。このモノイドの構成素は次のモノです。モノイド圏BipartQuiv(X, X)のモノイド積(ファイバー積)を¥otimesで表します。

  1. 集合X
  2. 二部箙 A = (X, X, A, srcA, trgA)
  3. 二部箙の準同型写像 μ:A¥otimesA→A
  4. 二部箙の準同型写像 ε:unitX→A

二部箙と書いてますが、始頂点集合と終頂点集合が一致しているので、Aは通常の箙(有向グラフ)で、Xがその頂点集合です。BipartQuiv(X, X)の射は箙の準同型なので、(A, μ, ε)は箙を台とするモノイドになります。

箙(有向グラフ)を台とするモノイドと言えば圏であることはお馴染みでしょうが、次の点に注意して確認してください。

  • A¥otimesAは {(f, g)∈A×A | trg(f) = src(g)} と書ける。
  • x, y∈X に対して、A(x, y) = {f∈A | src(f) = x かつ trg(f) = y} とすると、(A¥otimesA)(x, z) = Σ(y∈X | A(x, y)×A(y, z)) と書ける。
  • 従ってμは、μ[x, y, z]:A(x, y)×A(y, z)→A(x, z)により記述できる。
  • ε: unitX→A は、単なる写像 X→A(このAは箙のアロー集合)と同じである。

箙 A = (X, A, srcA, trgA) に、箙の準同型写像 μ:A¥otimesA→A, ε:unitX→A がある状況で、満たすべき法則結合法則、左単位法則、右単位法則で、それは次の形に書けます。ただし、弱2-圏の結合律子(associator)と左右の単位律子(unitor)は省略しています(律子(りつし)に関しては「律子からカタストロフへ」を参照してください)。

  • (μ[x, y, z]×idA(z, w));μ[x, z, w] = (idA(x, y)×μ[y, z, w]);μ[x, y, w] : A(x, y)×A(y, z)×A(z, w)→A(x, w)
  • (ε(x)×idA(x, y));μ[x, x, y] = idA(x, y) : A(x, y)→A(x, y)
  • (idA(x, y)×ε(y));μ[x, y, y] = idA(x, y) : A(x, y)→A(x, y)

左斜め加群と右斜め加群

圏を弱2-圏BinpartQuiv内のモナドとして定式化しました。この方法のメリットは、通常のモナドと圏に共通の定義を与え、お互いの理論が行き来する通路を与えることです。もうひとつのメリットは、圏のあいだの準同型写像が一般化されることです。モナドのあいだの準同型写像が、通常の関手よりずっと広い概念だからです。

一般的なモナドとは、自明な2圏1(2)から弱2-圏(厳密2-圏も含む)Bへのラックス2-関手なので、モナドの準同型はラックス2-自然変換だと考えるのが自然でしょう。ラックス2-自然変換の、より分かりやすい(と思える)定式化として、ここでは斜め加群(oblique module)という概念を紹介します。概念に新しいものはありませんが、「斜め加群」という言葉は僕の造語です。

Bが弱2-圏で、(X, M, μ, ε)がB内の(X上の)モナドとします。(Mは大文字ですが、ここではBの射を表します。)念のため繰り返すと、モナドの構成素は:

  1. Bの対象X
  2. Bの射 M:X→X
  3. Bの2-射 μ::M*M⇒M:X→X (*はBの横結合)
  4. Bの2-射 ε::unitX⇒M:X→X (unitXBの単位射)

ホム圏B(X, X)の言葉で言えば:

  1. B(X, X)の対象M
  2. B(X, X)の射 μ::M*M→M (*はB(X, X)のモノイド積)
  3. B(X, X)の射 ε::unitX→M (unitXB(X, X)の単位対象)

満たすべき法則は、結合律、左単位律、右単位律です。

M = (X, M, μ, ε), N = (Y, N, ν, ι) がB内の2つのモナドのとき、左(M, N)-斜め加群は次のモノから構成されます。

  • Bの射 F:X→Y
  • Bの2-射 α::M*F⇒F*N:X→Y

左(M, N)-斜め加群(F, α)が満たすべき法則モナド乗法とモナド単位の擦り抜け法則です。これらの法則をストリング図で表せば次のようになります。

右(M, N)-斜め加群(F, β)も同様に定義されます。

  • Bの射 F:X→Y
  • Bの2-射 β::F*N⇒M*F:X→Y

左(M, N)-斜め加群を使っても右(M, N)-斜め加群を使っても同じことですが、ここでは左斜め加群を使うことにします。ラックス2-自然変換の定義として右斜め加群を採用していることもある(多数派かも)ので注意してください。

左斜め加群の圏

前節に引き続き、Bは弱2-圏(Bは厳密2-圏でもよい)だとします。M = (X, M, μ, ε), N = (Y, N, ν, ι) をB内の2つのモナドとします。言い方を換えると、MはB(X, X)内のモノイド、NはB(Y, Y)内のモノイドです。左(M, N)-斜め加群の全体をLeftOblModB(M, N)と書くことにします。下付きのBは省略することがあります。

(F, α), (G, β)∈LeftOblModB(M, N) のとき、(F, α)から(G, β)への左斜め加群の準同型とは次のモノです。

  • 弱2-圏Bの2-射 φ::F⇒G:X→Y
  • φは、α;(φ*N) = (M*φ);β を満たす。

満たすべき法則をストリング図で描けば次のようです。

Y上のモナドNが、N = (Y, unitY, unitY*unitY⇒unitY, idunitY) という自明なモナドの場合、左斜め加群は左加群モナドによる左作用)とみなせ、左斜め加群の準同型は左加群の準同型と同じ概念になります。

この節の最初で、LeftOblModB(M, N)を左(M, N)-斜め加群全体の集合(類)としましたが、ホムセットを定義して、LeftOblModB(M, N)を圏とみなすことができます。

  • 対象: |LeftOblModB(M, N)| = (左(M, N)-斜め加群の全体)
  • ホムセット: (LeftOblModB(M, N))((F, α), (G, β)) = ((F, α)から(G, β)への左斜め加群の準同型の全体)
  • 射の結合: Bの2-射としての縦結合
  • 恒等射: Bの恒等2-射

ラックス2-関手の2-圏

代替圏論における“圏の圏”は、次のように定義されるのでした。

  • XCat = Lax2(1(2), SPAN(Set))

通常の“圏の圏”Catは2-圏(厳密2-圏)なので、XCatも2-圏の構造を持つべきです。となると、右辺Lax2(1(2), SPAN(Set))に2-圏の構造が必要です。

ラックス2-関手の全体に対して、次のような構成素により2-圏構造を入れることができます。

  • 対象は、ラックス2-関手
  • 射は、ラックス2-関手のあいだのラックス2-自然変換
  • 2-射は、ラックス2-自然変換のあいだの変更手(modification)

変更手は2-自然変換のあいだの変換です。一般に、n-自然k-変換という概念があり、ラックス2-関手は(ラックスな)2-自然0-変換、2-自然変換は2-自然1-変換、変更手は2-自然2-変換です。こらについては次を参照してください。

幸いに、自明な2-圏からのラックス2-関手の場合は、n-自然k-変換(高次変換)の理論を持ち出さなくても、ラックス2-関手の2-圏を記述できます*5

高次変換の概念 代数的概念
ラックス2-関手 モナド
ラックス2-自然変換 左斜め加群
変更手 左斜め加群の準同型

弱2-圏Bに対して、Lax2(1(2), B)をMonadBと略記すると。MonadBは2-圏であり、次の構成素からなります。

2-圏MonadBのホム圏は、

  • MonadB(M, N) = LeftOblModB(M, N)

M, N, Lが3つのモナドで、(F, α):M→N in MonadB, (G, β):N→L in MonadB のとき、(F, α)と(G, β)の横結合は、αとβのBにおける横結合で与えられます。

  • (F, α)*(G, β) = α*β = (α*G);(F*β)

左斜め加群の準同型の横結合も、Bの横結合として定義できます。

まとめと展望

長々と説明してきましたが、“高次でラックスな圏と変換の理論”の特殊ケースを取り上げただけです。

  • A, B が弱2-圏のとき、「ラックス2-関手、ラックス2-自然変換、変更手」から構成される2-圏Lax2(A, B)を構成できる。
  • 特に、A = 1(2) のとき、Lax2(1(2), B)はB内のモナドの2-圏となる。
  • MonadB = Lax2(1(2), B) に対しては、「モナド、左斜め加群、左斜め加群の準同型」という代数的な記述が可能である。

さらにBを特定の2-圏にすると:

2-圏XCatの理論が代替圏論です。代替圏は通常のモナドと明らかな類似性があります。ただし今回は、通常の「圏、関手、自然変換」の2-圏Catと代替圏の2-圏XCatとの関係にあまり言及してません。CatXCatに埋め込めますが、埋め込み方が自明とも言えません。[追記]埋め込めるかな? Catを素直に埋め込みのためには、XCatの定義を変えたほうがいいかも知れません。「弱2-圏内のモナドに関する補足:モナドが作る2-圏の多様性」を参照。[/追記]

枠組は出来たので、ベックの分配法則を代替圏に適用することが次の目標になるでしょう。また、Cat, BipartQuiv(SPAN(Set))以外の2-圏Bに対する MonadB = Lax2(1(2), B) を作ってみるのも面白そうです。

*1:終対象とファイバー積を持つことは、終対象と直積と等値核(イコライザー)を持つと言っても同じです。また、有限完備とか「有限極限を持つ」とも言い換えられます。

*2:ラックの論文"Composing PROPs"では、ベックの分配法則を使っています。

*3:これは圏論に限ったことじゃないですけどね。例えば、型理論の用語法も酷いもんです。→「型推論に関わる論理の概念と用語 その2

*4カレン語だと「言葉がきまじっちゃってるのが、やわらがります。」

*5:僕は、高次変換(transfor, higher transformation)の理論を理解してません。

2017-01-10 (火)

モノクロだと判読できない数式

| 10:41 | モノクロだと判読できない数式を含むブックマーク

分かりやすくするために絵図をカラーで描くのはよくあることだと思います。等式に絵が埋め込まれたりすると、その絵がカラーになることもあるでしょう。例えば、次の絵入り等式は、https://arxiv.org/pdf/1509.02937v1.pdf p.34のキャプチャです。

絵ならともかく、テキストによる記述がカラーじゃないと判読できない事態には、「えっ!?」とたじろぎます。次は、https://arxiv.org/pdf/1601.04964v1.pdf p.17です。絵はありませんが、色がないと判読できません。

今どきモノクロのデバイスもないから、これでもいいのかな(アクセシビリティの問題は残りますが)。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170110

2017-01-04 (水)

2017年 圏論に関する参考文献の案内(無料オンライン版含む)

| 11:15 | 2017年 圏論に関する参考文献の案内(無料オンライン版含む)を含むブックマーク

2017年最初のコメントとして、内海さんから次の情報を教えていただきました; 2016年12月30日に、レンスター(Tom Leinster)の書籍"Basic Category Theory"がオンラインに無料公開されました。

書籍の表紙画像が表示されないときは、このページをリロードしてみてください。

目を通してないので内容に立ち入ったコメントは出来ませんが、目次を見る限り、極限と随伴までを丁寧に解説している本のようです。著者のレンスターは信頼できる人なので、入門書として選んで間違いはないでしょう。

文献を紹介した過去記事の一覧

圏論の本を教えてください」と聞かれることがたまにあります。過去に何度か文献をまとめたことがあるので、それらのエントリーへのリンク(文献への間接参照)を以下にまとめます。この記事内では、文献のタイトルと著者だけ示します。参照を何度かたどれば圏論の文献に到達できます。並び順は、古い記事から新しい記事の順です。

2006年記事:圏論とラムダ計算の参考書
  • 『プログラム意味論』 / 横内寛文
  • "Categorical Logic and Type Theory" / B. Jacobs,
  • "Handbook of Categorical Algebra 2" / Francis Borceux
  • "Categories and Computer Science" / R. F. C. Walters
  • "Introduction to Higher-Order Categorical Logic" / J. Lambek, P. J. Scott

『プログラム意味論』には圏論のコンパクトな解説が含まれます。"Handbook of Categorical Algebra"は、1, 2, 3の三部からなる大作です。

2007年記事: 書評:理工系のための トポロジー・圏論・微分幾何
2009年記事: 竹内さんの『層・圏・トポス』を読む人達へ
  • 『層・圏・トポス 現代的集合像を求めて』 / 竹内外史
2013年記事: スピヴァックの圏論教科書 Category theory for scientists
  • "Category theory for scientists" / David I. Spivak
2013年記事: スピヴァックによる圏論文献案内と、彼の本の位置付け
  • "Conceptual Mathematics: A First Introduction to Categories" / F. William Lawvere, Stephen H. Schanuel
  • "Categories for the Working Mathematician" / Saunders Mac Lane
  • 圏論の基礎』 / Saunders MacLane, 三好博之, 高木理
  • "Category Theory" / Steve Awodey
  • "Category Theory for Computing Science" / Michael Barr, Charles Wells (online)
2013年記事:余代数を知りたいなら、これだ
  • "Introduction to Coalgebra" -- Towards Mathematics of States and Observations / Bart Jacobs (online)
2016年記事: 無料で入手できる本格的(紙なら高額)な理数系専門書15選
  • "Category Theory for the Sciences" / David I. Spivak (online)
  • "Higher Topos Theory" / Jacob Lurie (online)
  • "Tensor Categories" / Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik (online)
  • "Lectures on Tensor Categories and Modular Functors" / Bojko Bakalov,Alexander Kirillov (online)
  • "Monoidal Functors, Species and Hopf Algebras" / Marcelo Aguiar, Swapneel Mahajan (online)
  • "Homotopy Theory of Higher Categories" / Carlos T. Simpson (online)

補足

どれが良いかは、目的や予備知識によって変わるので一概には言えません。日本語の入門書で、僕が簡単なコメントと注意書きを付けたのは次の2冊です。

マックレーンのバイブル本を僕はあまり推奨しないのですが、その理由はスピヴァックが書いているので、その引用を読んでみてください。

圏論のご利益を知りたいなら、丸山さんの論説はいいかも知れません。[追記]残念ながら、PDFがダウンロード出来なくなっているようです。[/追記]

ビデオ教材なら、ウィラートンとチェンのシリーズがあります。

まったく何も知らない状態なら、僕が書いた入門記事が、最初の取っ掛かりとして多少の役には立つかも知れません。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170104

2016-12-28 (水)

滝沢カレンさんの言語芸術

| 16:48 | 滝沢カレンさんの言語芸術を含むブックマーク

滝沢カレンさんの変な日本語が2015年に評判になったようです。もうすぐ2017年ですけど。

僕は知らなかったので、「どんな日本語だったんだろう?」とYouTubeを探したら過去の動画がけっこうあります。確かにすごい日本語をしゃべります。勘違い(言葉の覚え間違い)・言い間違いのたぐいもありますが、独特なセンスを感じる言葉づかいもあります。

勘違い・言い間違いに近いもの(でもセンス感じる):

  • 「きまじっちゃって」→「気になっちゃって」(「気まずい」の意味はないが、「気まずくなった」の意味で使えそう)
  • 「やわらがります」→「柔らかくなります」(「和らぐ」の意味が入っているのだろう)
  • 「家の外から出ない」→「家の中から出ない」(単純な言い間違い)
  • 「アトゴエが欲しい」→「後押しする声が欲しい」
  • 「何の落ちぶれもなく」→「何の前触れもなく」
  • 「まるめこんで置いとく」→「まるめて置いとく」

「鬼っている」という表現を聞いたとき、僕は「これは分かる」と思ったのですが、「鬼になっている」と言い直し、意図は「お似合いになっている」だったらしい、分かってなかった。敬語を使おうと努力してオカシクなることは多くて:

  • 「おらっしゃる」(いらっしゃる)
  • 「お会話」
  • 「ご次回も」
  • 「お好きになって」
  • 「(母親と一緒に)暮らさせていただいてます」(最近なら許容範囲かも)
  • 「おたくさん」(敬称)
  • 「お見て、よろしいですか」(「ご覧になってください」かな?)

2015年11月の時点で「何のつらみもない」と発言してますが、この言い方は2016年になってポピュラーになりましたよね、先駆者だ! 「縄跳びの実行系列を見てみたい」という言い方も、正確な表現だな、と僕は思いました。

彼女が知っている諺は:

  • 「備えあれば嬉し恥ずかし」
  • 「豚も歩けば真珠も当たる」

さて、顰蹙を買いそうだが、それでも使ってみたくなる言葉・言い回し:

  • 「ありにしもなきず」
  • 「現実がウンと言ってないものたち」
  • 「マイナーな支障が出る」
  • 「世界の尋常じゃないぐらい嫌い」

最後の「世界の…」は、「世界で一番嫌い」と「尋常じゃなく嫌い」が発話段階でミックスされたものか?「ほんとに嫌いだ」を強烈に表現してます。もはや芸術。

[追記]下手すぎて、それが芸術に昇華してしまった事例としては、はいだしょうこおねえさんの絵がありますね。→「伝説の画伯[/追記]

2016-12-27 (火)

僕の「フローチャート」のイメージ(と心情)はこんなです

| 12:11 | 僕の「フローチャート」のイメージ(と心情)はこんなですを含むブックマーク

昨日書いた記事「「フローチャート」騒ぎ、もう少し頭使って考えてみようよ」のなかで:

そもそも、批判/否定している対象であるフローチャートって何なの? 厳密な定義じゃなくてもいいから、どんなイメージを持っているのか知りたいですね。どこがそんなに嫌いなの? なんでダメだと思うわけ? 別に挑発や煽りではなくて言うのだけど; 誰か説明してくれないかなー。

「じゃ、お前はどんなイメージを持っているんだ?」に対して、僕が「フローチャート」という言葉からイメージするものを記しておきます。誰かと議論する機会はないような気もするけど(ほんとの批判者はいないのかも知れないので)、言葉の使い方を合意するために。

平凡で標準的なイメージだと思う

昨日の記事でも、僕のイメージは書いてます。

もう一度言うと、「四角やひし形の箱を線で繋げた図式」がフローチャートで、図式の構成要素の意味は:

  • 四角は、何らかの処理を表す。
  • ひし形は、条件判断と分岐を表す。
  • 線は、制御やデータの流れを表す。

これは、キッカケとなった記事「若手プログラマー保存版!フローチャート徹底解説と作成カンニングペーパー」を書いている野崎晋平さんなんかのイメージと同じだと思うんだよね。野崎さんの記事ではキレイな図が掲載されているけど、僕が手描きで書くと↓のようになります。while(p){f} という繰り返し構造の絵です。

fが四角じゃなくて丸いのは、手描きだと四角が描きにくいから。「ロバストネス図は素晴らしい」でも書いたことだけど、丸のほうが素早く描ける。条件判断のNo(false)側にチェックマークを付けてYes/Noを区別してます。本音は菱形もメンドクサイのだけど、これも丸にしちゃうとさすがに判読しにくいので一応菱形にしてます。

ひょっとして、「フローチャートはダメ、UMLのアクティビティ図はいい」とか言っている人って、図中の絵記号のデザインを問題にしているの? 四角のカドがチャント尖っているのか、丸のなかを塗り潰しているのか、とか。そのテの描画のお作法は、僕は気にしてないです -- 速く楽に描けるのが一番だと思ってますから。

変種

基本的な図示法とその素朴な解釈においては、僕が世間からズレているとは思わないですけど、変種も使っていて、そこは標準的フローチャート(多数派のイメージ)と違うかも知れないです。

例外は次のように描きます。

点線の左が正常処理の世界で、右が異常(例外)の世界。ここでの左右併置は直和を意味するので、例外を投げるかも知れない処理fのプロファイルは、f:A→B+Y です。

ストレージへの書き込みがある場合は、

Sがストレージ状態空間で、Mがストレージへの書き込み命令のモノイド、黒丸はMのSへの作用で、書き込みを実行します。この場合の左右併置は直積で、f:A→B×M となります。

処理が環境を参照する場合は、

Eが環境で、Eはコピー(または参照を共有)されて出力側にも現れます。fのプロファイルは f:E×A→B です。

あと、条件分岐ですけど、菱形よりガード条件を基本に置きたいです。条件式(述語、論理式)pによるガードを三角で描いて、菱形は次のように定義します。

とはいっても、これは好みの問題です。if(p) then f else g (菱形)をプリミティブにしても、p then f (三角)をプリミティブにしても、たいした違いはありません。

参考

例外の扱いは、

↑の記事に絵はありませんが、前節の最初の方法で絵に描けます。

ストレージへの書き込みは、

環境を参照する計算は、

↑の記事にも絵がありません。先に挙げた環境を参照する絵を使えば事情が分かりやすくなります。

ガード条件の図示は、

再帰方程式を解いてwhile文を構成する話は、

バエズのアイディアに基づく留め金により、指数型(関数空間)を描く方法は次の記事にあります。

心情(苛立ち)

僕が絵に対して持っているセマンティクスは、トレース付きモノイド圏やデカルト閉圏なので、素直に「ストリング図」と呼んでおけばいいじゃないか、という意見は「そりゃそうだ」と思います。こころ穏やかに図式の話をするために、呼び名を変えるのは現実的な対処法でしょう。

でもね、「平凡で標準的なイメージだと思う」に書いたとおり、描画のお作法を除けば、いわゆるフローチャートとストリング図に差はないですよ。内実が同じモノの呼び名を変えただけで批難の対象になってしまう、という状況が、すっげー苦々しいわけ。呼び名「フローチャート」が、「これは無根拠に批難してもいいモノ」を示すラベルになっている、というね。イデオローグがいるわけじゃなく、相手は空気とモブなので、議論も説得もできないし。

発端となった野崎晋平さんの記事もタイガイでさー、なんであんな安っぽい取り上げ方するかなぁ。案の定、空気とモブに叩かれるという類型的顛末。定形の手順が自動実行されるような様に、僕はイラッとくるんです。感情的反応なので、なんで苛立つか分析できないですけど。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20161227

2016-12-26 (月)

「フローチャート」騒ぎ、もう少し頭使って考えてみようよ

| 11:13 | 「フローチャート」騒ぎ、もう少し頭使って考えてみようよを含むブックマーク

割と最近、次の記事がブックマークと注目を集めたようです。

見る前に予想したように、「何言ってんだ!? コイツ」「アホかバカか」的な扱いでしたね。雰囲気としては、「ホメオパシー効いたよ、マジおすすめ」という類の記事への反応と似たようなものです。

上記「フローチャート徹底解説」記事は、特段に酷いとは思いませんが、かといってたいして役立ちそうにないし、反感を買いそうな記述もある*1ので、記事を擁護する気はありません。しかし、フローチャート自体は強く擁護してきたので、ここでまたフローチャート擁護論を展開すべきかな、… と思わなくもないですが、あんまり乗り気じゃない -- 言いたいことは過去にほぼ書き尽くしていて、繰り返しになってしまうからです。

それと、僕がなにか言ったくらいでは、根強いアンチ・フローチャートの空気や信仰をどうこう出来る状態ではないようで、ちょっと虚しい。なので、フローチャート擁護つうより、フローチャート批判にホントに根拠あるのか? を問いたいと思います。

内容:

  1. あなたが嫌っている「フローチャート」って何なの?
  2. 感情と論理を整理してみよう
  3. 古い! 確かに。だから?
  4. ほんとの批判者はいないのかも知れない

あなたが嫌っている「フローチャート」って何なの?

本気で僕は不思議に思ってるのですが、何を根拠にフローチャートを批判/否定しているの? そもそも、批判/否定している対象であるフローチャートって何なの? 厳密な定義じゃなくてもいいから、どんなイメージを持っているのか知りたいですね。どこがそんなに嫌いなの? なんでダメだと思うわけ? 別に挑発や煽りではなくて言うのだけど; 誰か説明してくれないかなー。

皆んなが忌み嫌い攻撃したがるモノと、僕が擁護しようとしているモノがズレているのかなぁ。それについては、過去に「「フローチャート」という言葉の問題」に書いたことがあります。僕自身は、「四角やひし形の箱を線で繋げた図式」程度の意味で「フローチャート」という言葉を解釈し使っています。この広い意味だと、ストリング図(例えば「絵算のススメ 2015 年末版」参照)もフローチャートの仲間、つうか、僕にとってはストリング図が典型的なフローチャートです。

なので、次のようなことを言われても、何でそう考えちゃうのか? 理解できないのです。

  • フローチャートは手続きしか表現できない。
  • フローチャートはgoto文だからダメ。
  • フローチャートは関数型言語オブジェクト指向言語とは無縁。
  • フローチャートはダメだ、UMLのアクティビティ図ならいい。

もう一度言うと、「四角やひし形の箱を線で繋げた図式」がフローチャートで、図式の構成要素の意味は:

  • 四角は、何らかの処理を表す。
  • ひし形は、条件判断と分岐を表す。
  • 線は、制御やデータの流れを表す。

こういった図式法で、プログラムや構文を表すのが何故にマズイと判断するのでしょうか? 論理的な根拠じゃなくて、感情的な理由でもいいでから知りたい。

[追記]僕(檜山)が「フローチャート」という言葉に抱いているイメージは、

[/追記]

感情と論理を整理してみよう

前節の“感情的な理由”については、「苦い経験?」で、僕の想像(実体験ではない)を書いています。フローチャートを憎む人は、次のようなイヤな経験をしたのではないだろうか? という想像です。

  1. 現場の開発工程のなかでフローチャート作成を義務付けられた。
  2. プログラムコード(テキスト記述)と同じ内容を重複して無駄に書かされた。
  3. 他人が描いた図を見ても、制御とデータの流れがゴチャゴチャでワケワカんなかった。
  4. 図をキレイにレイアウトしないと文句を付けられた。

もし、そんなことがあれば嫌いにもなるでしょう。しかし、そのようなイヤな経験は、手法やアイディアとしてのフローチャートの評価とは別物です。どんな手法やアイディアでも、運用される環境や制度によってはイヤな経験に結びつくかも知れません。

例えば「ワタシの場合はホメオパシーで風邪が治った、だからホメオパシー効く」という論法に、皆さんはどう反応しますか。個人的・個別的経験から「効く」という一般論を導くのは早計だ、と思いますよね。たまたま自然治癒した可能性もありますから。

「俺はフローチャートで酷い目にあった、だからフローチャートはダメだ」は、上の「ホメオパシーは効く」と同様に、個人的・個別的経験から「ダメだ」という一般論を、他の要因を考慮することなく導く論法になっています。

もうひとつ、僕が論理的妥当性を疑う点は、フローチャート批判に際して、いったん誇張してから批判していることがある点です。どういうことか言うと、次のような主張に対して批判をしていることです。

  1. すべてのプログラマは、フローチャートを学ばねばならない。
  2. プログラマコードを書く前に、必ずフローチャートを描かねばならない。
  3. テキストコードと1:1対応するようにフローチャートを描かねばならない。
  4. フローチャートは何でも表現できる。

こういう極端なことを言う人はあまりいないと思います(「フローチャートはもちろん万能じゃない」も参照)。こういう極論、例外的主張を取り出して(あるいは捏造して)批判するのは詭弁のたぐいです。「論理的であるかのごとくに装って、根拠のないイチャモンをつける 13+2 の方法」の「傾向や量に関する主張に、勝手に全称限量子を付けてしまう」を実践しているわけです。

フローチャート否定の説得的な根拠が見いだせないので、次のような状況ではないかと僕は考えています。

  1. 否定する人も肯定する人も、実は「フローチャート」に対して明確な定義を持ってないし、イメージがズレている可能性がある。
  2. イヤな経験から感情的に「フローチャートはダメだ」という人が一定数いる。
  3. 経験も自分の意見もなく、あまりものを考えない人が「フローチャートはダメだ」と言ってみる。
  4. 「フローチャートはダメだ」な空気が醸成される。
  5. この空気のなかで、あまりものを考えない人が(以下略)

古い! 確かに。だから?

このテの話題だと、id:JavaBlackさんが言及してるんじゃないかと確認してみたら、ビンゴ、語ってましたね。

遅くとも「人月の神話」は1975年には出ていたらしいから,その頃にはフローチャートが役に立たないというのは,既に広く知られた事実だったと言って良い.あれからいったい何十年たったと思ってるんだよ.

さすがにJavaBlackさん、良い情報を提供してくれます。1975年頃にはフローチャートは役に立たないという認識があった、ということです。つまり、はるか昔に否定されているんだ、ってことです。それは事実でしょう。

1975年、確かに昔ですよね。だったら、その知見が古い、って可能性は考えないのかな?

フローチャート研究の歴史(断片)」に書いておきましたが、1970年代/80年代に、アービブ&マナ、ロビン・ミルナー、ダナ・スコットなどの大家がフローチャートの研究をしていて、80年代にはカザネスクとステファネスクが精力的にフローチャート(フローノミアル→ネットワーク代数と名前を変えて)理論を整備しています。トレース付きモノイド圏(traced monoidal category)としては、90年代にハイランド、長谷川などが不動点理論を完成させています(「トレース付き対称モノイド圏とはこんなモノ」、「絵算で見る「カザネスク/ステファネスク/ハイランド/長谷川の定理」」参照)。

フローチャートを復権させよう -- 2020年代のプログラミングへ」より:

1990年代以降、トレース付きモノイド圏/前モノイド圏の計算科学への応用は長足の進歩をしました。いまや、フローチャートは科学として扱えるのです。再びプログラミンミングの有効な道具としてフローチャートがカムバックする準備は出来ています。忌まわしい過去は忘れましょう。

時代は変わったのに、「フローチャートってダメなんだよね」とか根拠もなく盲信しているのって、なんなの?

「いまどきフローチャート」、「ふっ、古過ぎる」、「昭和だ、20世紀だ」といった揶揄も見かけますが、「古いからダメ」って主張したいなら、次の命題が必要ですよね。

  • ∀X.(Xは古い ⇒ Xはダメ)

これはいくらでも反例があるでしょ。ハードウェアなんかは古いと使いものにならないけど、手法やアイディアって、けっこう寿命が長い。TCP/IPもHTTP/HTMLもLispモナドも20世紀でしょ*2米田の補題なんて1954年だよー、驚いちゃうよね*3

ほんとの批判者はいないのかも知れない

今回のように、フローチャートに関してなんか言うと批判が集まる、という現象は観測されます。しかし、誇張した(勝手に全称限量子を付けた)主張への批判や、おそらくはイヤな経験からの感情論や、とりあえずイチャモン付けたいだけの人の戯言しか見つからないので、ほんとの(本気の)批判者はいないのかも知れない、という気もしてきます。

ネット上で根拠のない(ときに虚偽の)情報が高速大規模に拡散される様をみて、ものを考えない人が増えた、と感じる人もいるでしょう。実際は、ものを考えない人の行動が露出しやすいだけかも知れません。空疎な反射行動のみで、もともと根拠ある発言や指摘なんてなかった、と。

もしそうだとすると、僕は今、何の手応えもない、ひょっとすると存在しない相手に理由と根拠を問いかけているってことになりますね。あー、やっぱり虚しかったか。


[追記]

技術的な内容には全然触れてなかったので、ちょっと書き足しておきます。

箱と線(ワイヤー)の組み合わせで、ワイヤーを曲げて逆行することも許すと、その図式(チャート、ダイヤグラム)はトレース付きモノイド圏の射を表します。

  • 箱 -- 基本の射
  • ワイヤー -- 対象
  • 箱/ワイヤーの併置 -- モノイド積
  • 曲げて逆行 -- トレース

これに菱形の条件判断を入れたいときの描画法は、例えば「非決定性プログラミングだって絵を描いてみれば一目瞭然」あたりを参照。

箱とワイヤーの図をフローチャートと呼ぶのが過度な拡大解釈だと思う人もいるでしょう。確かに、一番の齟齬の原因は「狭義の解釈」と「広義の解釈」のズレかも知れません。でもね、広く解釈すると楽しいことがあるんですよ。例えば、量子情報学の絵図なんていかが。眺めてるだけで楽しくなれます。

[/追記]

*1:「初心者に必須」とか「コーディング前に描きましょう」とかは、さすがに現実性がないので反感を買うだけです。強調すべきは、プログラム意味論と、グラフ書き換えによるプログラム変換です。

*2:Mizarは1970年代、処理系の古臭さにはさすがにイライラしてます。→「Mizar、嫌いじゃないんだけどな

*3:米田の補題は、今回の話題と関係はないです。けどね、圏論が始まってすぐの時期、60年以上も前ですよ。古いけどスゴイ。

2016-12-16 (金)

Mizar証明の抜群な分かりやすさ

| 17:11 | Mizar証明の抜群な分かりやすさを含むブックマーク

Mizarの処理系はまったく使いにくいです。その使い勝手は極悪ですわ。それにも関わらず僕が我慢して使おうとしているのは、Mizarの構文と意味モデルが素晴らしいからです。最高ですわ。特に、他の証明系のタクティク言語の難読さに辟易した人には感激もんです。

証明検証系Mizarを試してみる」で例に出した次の証明記述コードを例にします。

reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof
  defpred P[natural number] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume B0: i+0 = j+0;
    B1: i+0 = i by INDUCT:3;
    B2: j+0 = j by INDUCT:3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k st P[k] holds P[succ k]
  proof
    let l such that C1: P[l];
    assume C2: i+succ l=j+succ l;
    then C3: succ(i+l) = j+succ l by C2,INDUCT:4
    .= succ(j+l) by INDUCT:4;
    hence thesis by C1,INDUCT:2;
  end;
  for k holds P[k] from INDUCT:sch 1(A1,A2);
  hence thesis;
end;

これは、チュートリアル・スライド http://mizar.org/cicm_tutorial/mizar.pdf の45ページから取ったものですが、コンパイル(検証)できませんでした。単にenviron部が書いてないだけでなく、構文エラーがあります。また、MML(Mizar Mathematical Library)には存在しないアーティクルを参照しています。

なんとかコンパイルできるように修正したコードが以下です。修正してみると、証明すべき命題 i + k = j + k implies i = j はちょっと簡単過ぎて、自動証明(証明探索)能力がほとんどないMizarでさえ自力で(人間の支援なしで)証明しちゃいます。トホホ*1。まーそれでも、数学的帰納法の使用例としては意味があるでしょう。完全なenviron部と、証明内で使用する基本命題を記述しています。

:: tihs is induct_samp.miz
:: verified by: Mizar Ver. 8.1.04 (Win32/FPC)
::
environ

:: From NAT_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;

 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

:: Added
 constructors NAT_1;
 registrations NAT_1;
 schemes NAT_1;

begin

BASIC1: for n, m being Nat holds
        n + 1 = m  + 1 implies n = m;
BASIC2: for n being Nat holds
        n + 0 = n;
BASIC3: for n, m being Nat holds
        n + (m + 1) = (n + m) + 1;

reserve i,j,k,l,m,n for Nat;

i + k = j + k implies i = j
proof
  defpred P[Nat] means
    i + $1 = j + $1 implies i = j;
  A1: P[0]
  proof
    assume
    B0: i + 0 = j + 0;
    ::hereupon
    B1: i + 0 = i by BASIC2;
    B2: j + 0 = j by BASIC2;
    hence thesis by B0,B1,B2;
  end;
  A2: for k be Nat st P[k] holds P[k + 1]
  proof
    let m such that C1: P[m];
    assume C2: i + (m + 1) = j + (m + 1);
    then C3: (i + m) + 1 = j + (m + 1) by C2,BASIC3
                        .= (j + m) + 1 by BASIC3;
    hence thesis by C1,BASIC1;
  end;
  for k holds P[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

簡単なことを持って回って言ってるような所に目をつぶれば、証明の筋は読み取れるでしょう。英語ベースだからという点で日本人には分かりにくいかも知れません。キーワードを日本語に置換してみましょう。以下は、ほとんど文字列置換ですが、一部は日本語として自然な語順になるように語の入れ替えをしています。また、Mizarのラベルは、アンダースコアを含めたり括弧で囲んだり出来ませんが、その制限は取り払って考えています。コメントも若干足しています。

基本命題_1: 任意の 自然数 n, m に対して、
        n + 1 = m + 1 ならば n = m 。
基本命題_2: 任意の 自然数 n に対して、
            n + 0 = n 。
基本命題_3: 任意の 自然数 n, m に対して、
            n + (m + 1) = (n + m) + 1 。

以下、i, j, k, l, m, n は 自然数 とする。
このとき、
i + k = j + k ならば i = j
証明:
  まず 述語を定義する: P[自然数] とは ※(その自然数は $1)
    i + $1 = j + $1 ならば i = j であること。
  (A1): P[0] ※帰納法のベース: i + 0 = j + 0 ⇒ i = j
  証明:
    次を仮定する:
    (B0): i + 0 = j + 0 。
    このとき、
    (B1): i + 0 = i その根拠は 基本命題_2 。
    (B2): j + 0 = j その根拠は 基本命題_2 。
    従って 目的の命題、その根拠は B0,B1,B2 。※目的の命題: i = j
  終り。
  (A2): 任意の k ただし P[k] に対して P[k + 1] ※帰納法のステップ
  ※ (i + k = j + k ⇒ i = j) ⇒ (i + (k + 1) = j + (k + 1) ⇒ i = j)
  証明:
    m を導入、ただし
    (C1): P[m] 。※ i + m = j + m ⇒ i = j
    次を仮定する:
    (C2): i + (m + 1) = j + (m + 1) 。
    すると
    (C3): (i + m) + 1 = j + (m + 1) その根拠は C2,基本命題_3
                     .= (j + m) + 1  その根拠は 基本命題_3。
    従って 目的の命題、その根拠は C1,基本命題_1。※目的の命題: i = j
  終り。
  任意の k に対して P[k]、その推論は 数学的帰納法(A1,A2)。
  従って 目的の命題。
終り。

以下に対応表を示します。順番は語の出現順です。

日本語 Mizar
任意の for
自然数(語順変更) being Nat
に対して holds
ならば implies
;
以下 (捨てる)
(捨てる)
は とする(語順変更) reserve
このとき (捨てる)
証明: proof
まず (捨てる)
述語を定義する: defpred
とは means
::(コメント)
であること (捨てる)
次を仮定する: assume
その根拠は by
従って hence
目的の命題 thesis
終り end
を導入(語順変更) let
ただし st
すると then
その推論は from
数学的帰納法 NAT_1:sch 2

Mizarの構文が素晴らしいのは、他の証明系とは違い、証明記述で使われる自然言語の分析に基づいていることです。最初に人工言語があり、それを自然言語に近づけようとゴチャゴチャ細工しているのとは訳が違います。人間側の言語使用、言語行為、論理的思考をなるべく忠実にコンピュータにシミュレートさせるように設計されています。

人間にフレンドリーな構文なんですよ。なのに、なのに、なのに、処理系はなんであんなにフレンドリーじゃないんだよ! ギャップが凄いわ。凄すぎるわ。

ともかく、構文(は)最高よ。

*1:Mizarは人間が書いた証明を検証する処理系です。Mizar自身が証明できる命題を人間がご丁寧に証明したからといって文句は言いません。人間が書いた証明の正しさをチェックします。