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

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

2018-04-26 (木)

新しい絵算手法:ストリング+ストライプ図

| 14:49 | 新しい絵算手法:ストリング+ストライプ図を含むブックマーク

ここ数日、新しい絵算〈{pictorial | graphical | diagrammatic} calculation〉を考えて試しているんですけど、けっこう使えそう。新しいとは言っても、本質的に新しいものではなくて、既存の2つの描画法を組み合わせたものです。ストリング図ストライプ図のハイブリッドなので、ベタにストリング+ストライプ図〈string+stripe diagram〉と呼んでます。メインはストライプ図なので、ストリング図機能を取り込んだストライプ図とも言えます。

内容:

  1. “モノイド圏の圏”における3つの方向
  2. 3次元見取り図
  3. 正面図:ストライプ図
  4. 側面図:ストリング図
  5. 例題のサワリ
  6. おわりに

“モノイド圏の圏”における3つの方向

2つのモノイド圏とそのあいだの関手を扱うと、射の結合の方向、モノイド積の方向、関手の結合方向の3つの方向が出てきます。3次元の見取り図を描けばいいのですけど、これは手間がかかる! それで、側面図としてストリング図、正面図としてストライプ図を使うことにします。

このとき、「射の結合方向を縦(上から下)、関手の結合方向を横(左から右)に見る」のが側面で、「射の結合方向を縦(上から下)、モノイド積の結合方向を横(左から右)に見る」のが正面とします。自然変換に関しては、縦結合の方向=射の結合方向、横結合の方向=関手の結合方向 です。

3次元見取り図

実例を出さないとピンとこないでしょう。次の絵は、モナド乗法とテンソル強度の組み合わせの3次元見取り図です。

C = (C, ¥otimes, I) がモノイド圏で、F = (F, μ, η, τ) はモノイド圏C上の強モナド〈strong monad〉とします。τはテンソル強度〈tensorial strength〉で、A, X∈|C| でインデックスされた射の族(自然変換)です。

  • τA,X:A¥otimesF(X)→F(A¥otimesX)

3次元での絵の描き方は:

  1. Cは壁のような平面とする。
  2. Cの対象は、平面内を縦に走るワイヤー
  3. Cの射は、平面内のノード(上の絵には登場しない)
  4. 関手(の断片)は、2枚の平面のあいだに在るストライプ(リボン)

関手の結合方向は、後(奥)から前(手前)の方向とします。関手 F:CC は、奥側にあるC平面から手前のC平面のあいだに在ります。F*F:CC なら、Fのストライプを2枚並べて置くことになります。モナド乗法 μ::F*F⇒F:CC は、2枚のストライプ(リボン)を1枚に融合する操作で、μを赤い縫い目で表しています。

テンソル強度は、手前のC側で対象Aを左から掛ける操作を、奥のCでの掛け算操作に変換します。このことを、手前の青ワイヤーが奥の青ワイヤーへと移動しているように描いています。縦方向は、射の結合方向/自然変換の縦結合方向ですが、同時に操作が実行される時間方向だとも解釈するといいでしょう。

正面図:ストライプ図

上記の状況を、手前から見て描いた正面図が次です。正面からの観察者は、関手の結合方向が自分に向かって来る位置から見ているとします。

関手を表すストライプは半透明だとして、奥のストライプは細い幅にします。奥から順に、対象X、一番目のF、二番目のFが入れ子に見えます。対象Aの左掛け算は、青いワイヤーを左に併置するだけです。青いワイヤーがストライプを突き抜けている箇所がテンソル強度と解釈します。ストライプの内側に入った青いワイヤーは、奥のC側での掛け算とみなされます。

側面図:ストリング図

同じ状況を側面から見てみます。ただし、3次元見取り図をそのまま横側から写生するのではなくて、ストリング図の流儀による多少の描き換えが発生します。

  1. ストリング図における圏は、平面(を側面から見た直線)ではなくて領域です。
  2. ストリング図における対象は、自明圏☆からの関手として表します。(例: X)
  3. ストリング図における掛け算(モノイド積)は、スタンピング関手として表します。(例: (A¥otimes))

このような“流儀”の違いがあるものの、ストライプ図とストリング図を併用すると、3次元的な状況を把握しやすくなります。

例題のサワリ

例題として*1、モノイド圏 C = (C, ¥otimes, I) 上の強モナド F = (F, μ, η, τ) から、対象 N = F(I) に載ったモノイド N = (N, m, e) を構成することを考えます。

単位対象Iでの値F(I)の上に、μ, ηから誘導されたモノイド構造が載ることは、直感的には“いかにも”なのですが、どう計算していいかハッキリしません。ストリング+ストライプ図だと、F(I)上のモノイド構造を比較的楽に構成できます。次の図は、N = F(I) 上のモノイドの結合律を示す図です。

この図をしばらく眺めていると、左辺から右辺へ(あるいは逆方向)の変形過程のアニメーションムービーが見えてきます。ムービーの各フレーム〈スチル | コマ〉を時間順に並べれば、求める結合律の証明が得られます。

今日は、証明=変形操作の詳細は割愛しますが、図の各部の意味は次のようです。

  1. 2本のNを囲んでいる糸は、 (N¥otimesN)¥otimesN の括弧に相当し、(N¥otimesN)¥otimesN→N¥otimes(N¥otimesN) で糸は右に移動します(移動後の糸を描き忘れているけど、まーいいでしょ)。
  2. '='が書いてあるノードは、明示的等号ノード〈explicit equality nodes〉で、N = F(I) または F(I) = N を示します。
  3. ピンクまたは赤のストライプは、関手 F:CC を表します。
  4. 点線は、単位対象Iです。
  5. N¥otimesI→N は、左単位律子〈left unitor〉λNです。
  6. 赤い横線は、モナド乗法 μ::F*F⇒F:CC です。
  7. モノイドの乗法 m:N¥otimesN→N は、τN:N¥otimesF(I)→F(N¥otimesI), F(λN):F(N¥otimesI)→(F(N) = F(F(I))), μI:F(F(I))→(F(I) = N) の縦結合で定義されます。

証明を与えるムービーにおけるフレーム間の遷移は、モナドテンソル強度に関する法則に対応します。

おわりに

前節の例題をはじめとする、強モナドの計算を幾つかしたので、そのうち紹介するかも知れません。最初、“モナドの圏の上のモナド”を作ろうとしてたのですが、それは失敗(目論見違い)でした。しかし、強モナドのイメージはだいぶハッキリと持てるようになりました。

ストリング図だけ、ストライプ図だけだとうまくいかない計算もストリング+ストライプ図だとサクサク進んだりするので、この絵算手法はまーまーいいんじゃないか、という感触です。

*1:これは、単なる一例題ではなくて、この計算を自明化したくてストリング+ストライプ図を考えた、という動機になったものです。

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

2018-04-25 (水)

自然同型と自然同値

| 17:06 | 自然同型と自然同値を含むブックマーク

僕、自然同型〈natural isomorphism〉と自然同値〈natural equivalence〉という言葉を区別してなかったわ。

nLabによると、自然同値のほうは、一般的n-圏のあいだの関手のあいだの関係のようです。よく使われる例は2-関手の2-圏における関係。しかし、

  • In 1-category theory it is a natural isomorphism.

1-圏論(通常の圏論)で自然同値と言ったらそれは自然同型のことだから、1-圏論の範囲内では、自然同型=自然同値 で間違いでもないみたい。修正はしないことにした。

2018-04-24 (火)

指数関手や加群圏の簡単な例

| 09:46 | 指数関手や加群圏の簡単な例を含むブックマーク

比較的最近の記事で二項指数関手を扱い、その例を幾つか挙げています。

上記の記事より簡単な例をここで述べます。加群圏とその準同型についても触れます。

内容:

  1. 有限集合と有限次元ベクトル空間
  2. 写像ベクトル空間の二項関手性
  3. モノイド圏上の加群
  4. 関手の連続性と指数法則
  5. 加群圏の準同型としての次元関手

有限集合と有限次元ベクトル空間

指数関手と構文論・意味論 // 二項指数関手の例」の三番目の例は、コンパクト・ハウスドルフ空間連続写像の圏CompHousと、バナッハ空間と有界(=連続)線形写像の圏Banに関するものでした -- ちょっとむずかしげ。コンパクト・ハウスドルフ空間離散なものに限ってみます。すると、離散コンパクト・ハウスドルフ空間有限集合と簡単になります。ベクトル空間も有限次元の空間だけ考えればよくなります。

以下、有限集合と写像の圏をFinSet、有限次元ベクトル空間と線形写像の圏をFdVectとします。有限次元ベクトル空間のスカラー体〈係数体 | 基礎体〉は何でもいいので特に指定しません(が、何かに固定されています)。

FinSetは、集合の直積によりモノイド圏になります。また、集合の直和によってもモノイド圏になります。FinSetにモノイド構造を考えるとき、どちらのモノイド構造かが分かるように、次の書き方をしましょう。

  • FinSet× = (FinSet, ×, 1)
  • FinSet+ = (FinSet, +, 0)

1は単元集合、0空集合です。結合律子と左右の単位律子は省略しています(律子に関しては「律子からカタストロフへ」を参照)。

FdVectも、2つのモノイド構造を持ちます。有限集合のときと同じ記法を採用します。

  • FdVect = (FdVect, ¥otimes, I)
  • FdVect = (FdVect, ¥oplus, O)

Iはスカラー体と同型な1次元ベクトル空間、Oはゼロ空間です。テンソル積モノイド構造は、今回表立っては使いません。

FdVect圏論的直積を考えると、それはベクトル空間の直和に一致します。ベクトル空間の直和は圏論的直積でもあり圏論的直和でもある双積〈biproduct〉というものです。そこで、'¥oplus'を'×'とも、OはZとも書くことにしして、次のモノイド構造(直和モノイド構造と同じ)も考えます。

  • FdVect× = (FdVect, ×, Z)

FinSetFdVectも、2つのモノイド構造が分配法則で連携しています。この意味で、この2つの圏は半環圏〈semiringal category | semiring category〉です。が、今回はこの事実は使いません。半環圏の定義については「デカルト半環圏の定義を確認してみる(デカルト半環作用圏のために)」を参照してください。

写像ベクトル空間の二項関手性

以下、X, Yなどは有限集合、V, Wなどは有限次元ベクトル空間とします。有限集合Xから有限次元ベクトル空間Vへの写像の全体をMap(X, V)とします。v∈Map(X, V) とすると、v:X→V です。このvは、Xでインデックスされたベクトルの族(I-indexed family of vectors)と考えることもできます。

Map(X, V)にはVのベクトル空間構造に基づき、(標準的な)ベクトル空間構造を入れることができます。Map(X, V)をベクトル空間と考えましょう。つまり、Map(X, V)∈|FdVect| となります。さらに、φ:X→Y, f:V→W に対して、Map(φ, V), Map(X, f), Map(φ, f) を次のように定義できます。非形式的なラムダ記法を使います。

  • Map(φ:X→Y, V):Map(Y, V)→Map(X, V)
    Map(φ, V) := λu∈Map(Y, V).(λx∈X.u(φ(x)))
  • Map(X, f:V→W):Map(X, V)→Map(X, W)
    Map(X, f) := λv∈Map(X, V).(λx∈X.f(v(x)))
  • Map(φ:X→Y, f:V→W):Map(Y, V)→Map(X, W)
    Map(φ, f) := λu∈Map(X, V).(λx∈X.f(u(φ(x))))

Map(φ, f)だけを上記のように定義して、Map(φ, V), Map(X, f) を次のようにしてもかまいません。

  • Map(φ, V) := Map(φ, idV)
  • Map(X, f) := Map(idX, f)

このように定義された Map:FinSetop×FdVectFdVect が二項関手〈双関手〉になること(以下の等式)は簡単に確認できます*1

  • Map((ψ, f);(φ, g)) = Map(φ;ψ, f;g) = Map(ψ, f);Map(φ, g)
  • Map(id(X, V)) = Map(idX, idV) = idMap(X, V)

Map(-, -) を中置記法 -¥odot- と書いてみると;

  • (φ;ψ)¥odot(f;g) = (ψ¥odotf);(φ¥odotg)
  • idX¥odotidV = idX⊙V

FinSetが反変(反対圏)になっているのでちょっと形がイレギュラーですが、'¥odot'を一種の積とみなして、交替律〈interchange law | exchange law〉が成立していることになります。

モノイド圏上の加群

M = (M, ¥otimes, I) がモノイド圏、Cが単なる圏のとき、二項関手 ¥odot:M×CC左モノイド作用〈left monoidal action〉であるとは、およそ次が成立することです。

  • (X¥otimesY)¥odotA ¥stackrel{¥sim}{=} X¥odot(Y¥odotA)
  • I¥odotA ¥stackrel{¥sim}{=} A

律子と一貫性もちゃんと考慮した正確な定義は次の記事を参照してください。

モノイド圏M、圏C、左モノイド作用¥odotを組にした(M, C, ¥odot)を、加群〈left mudule category〉と呼びます。右モノイド作用と右加群圏も同様に定義できます。

加群圏(M, C, ¥odot)があると、Mのモノイド積を逆転させたモノイド圏M'に対する右加群圏(M', C, ¥odot')を作ることができます。M'は、射の向きはMと同じなので反対圏ではありません。モノイド積の向きが反転しています -- そういう圏に特に呼び名はないようです。

  • M' = (M, ¥otimes', I) として、X¥otimes'Y := Y¥otimesX
  • A¥odot'X := X¥odotA

同様に、M上の右加群圏からM'上の左加群圏が作れます。

有限集合の圏FinSetには直積モノイド構造がありました。有限次元ベクトル空間の圏は、とりあえずは単なる圏と考えます。Map(X, V)をX¥odotVとも書きます。この状況で:

  • (X×Y)¥odotV ¥stackrel{¥sim}{=} X¥odot(Y¥odotV) (Map(X×Y, V) ¥stackrel{¥sim}{=} Map(X, Map(Y, V)))
  • 1¥odotV ¥stackrel{¥sim}{=} V (Map(1, V) ¥stackrel{¥sim}{=} V)

つまり、FdVectは、左モノイド作用 -¥odot- = Map(-, -) によりFinSet×上の加群圏になります。右加群圏構造も定義できます。FinSet×は対称モノイド圏なので、左加群圏と右加群圏に本質的な差はありません。

関手の連続性と指数法則

関手の連続性は意外と厄介な概念です。連続性の定義には圏の完備性が必要で、完備性には極限が必要で、極限の定義と存在は使用する形状圏(または箙〈えびら〉)のクラスに依存します。このことは「指数関手と構文論・意味論 // 指数関手=反変連続・共変連続なモノイド作用」で述べています。極限については次の記事を参照してください。

Φを箙のクラスとして、どんな図式 Q∈Φ, F:Q→C も極限を持つときCはΦ-完備で、余極限を持つときΦ-余完備でした。Φを有限離散箙のクラスに選んだとき、Φ-完備は有限離散完備、Φ-余完備は有限離散完備になります。次が成立します。

  • Cが有限離散完備である ⇔ Cは終対象と有限直積を持つ
  • Cが有限離散余完備である ⇔ Cは始対象と有限直和を持つ

有限離散(余)完備性に関する連続性を有限離散(余)連続と呼ぶことにすると、F:CD に関して:

  • Fが有限離散連続である ⇔ Fが終対象と有限直積を保つ
  • Fが有限離散余連続である ⇔ Fが始対象と有限直和を保つ

極限が反対圏では余極限であることから、G:CopD に関して:

  • Gが有限離散連続である ⇔ Gは始対象を終対象に写し、有限直和を有限直積に移すCからの反変関手である
  • Gが有限離散余連続である ⇔ Gは終対象を始対象に写し、有限直積を有限直和に移すCからの反変関手である

さて、Map(-, -) = -¥odot- :FinSetop×FdVectFdVect は、V∈|FdVect| を固定すると FinSetopFdVect という関手となり、X∈|FinSet| を固定すると FdVectFdVect という関手になります。それぞれの関手の有限離散連続性は次のように記述されます。

  1. 0¥odotV ¥stackrel{¥sim}{=} Z
  2. (X + Y)¥odotV ¥stackrel{¥sim}{=} (X¥odotV)×(Y¥odotV)
  3. X¥odotZ ¥stackrel{¥sim}{=} Z
  4. X¥odot(V×W) ¥stackrel{¥sim}{=} (X¥odotV)×(X¥odotW)

以上に述べた性質は、指数関数の次の性質(1から4)に対応します。

  1. a0 = 1
  2. ax+y = axay
  3. 1x = 1
  4. (ab)x = axbx
  5. a1 = a
  6. (ax)y = axy

5番目と6番目は、先の述べた左加群性です。

  1. 1¥odotV ¥stackrel{¥sim}{=} V
  2. (X×Y)¥odotV ¥stackrel{¥sim}{=} X¥odot(Y¥odotV)

加群圏の準同型としての次元関手

有限次元ベクトル空間には、その次元と呼ばれる自然数が一意的に決まります。次元dimは、圏FdVectの対象達の上で定義された自然数値関数とみなされていますが、関手に仕立てましょう。さらに、次元関手は、FinSet×上の加群圏のあいだの準同型とみなせます。

まず、次元関手が値を取る圏Dを定義します。Dは、集合N自然数全体の集合)から作った余離散圏〈密着圏 | カオス圏〉です。

  • |D| = N
  • Mor(D) = {[n, m] | n, m∈N}
  • dom([n, m]) = n, cod([n, m]) = m
  • [n, m];[m, k] = [n, k]
  • idn = [n, n]

任意の圏CからDへの関手 F:CD は、その対象部分だけで決定されてしまいます。次の1:1対応があります*2

  • (関手 F:CD) ←→ (関数 |C|→|D|)

したがって、dim:|FdVect|→N は、関手 Dim:FdVectD とみなせます。

Dに対して、FinSet×の左モノイド作用を定義します。

  • X¥odotn := #(X)・n

ここで、#(X)は有限集合Xの基数である自然数、'・'は自然数の掛け算です。これが左モノイド作用である条件は次のとおり:

  • 1¥odotn := #(1)・n = n
  • (X×Y)¥odotn := #(X×Y)・n = X¥odot(Y¥odotn) = #(X)・(#(Y)・n)

#(X×Y) = #(X)・#(Y) を考慮すれば明らかですね。

モノイド圏M上の左加群C, Dがあるとき、関手 F:CD が左加群圏の準同型であるとは、およそ次が成立することです。

  • X¥odotF(A) ¥stackrel{¥sim}{=} F(X¥odotA)

次元関手Dimでは、

  • X¥odotDim(V) = Dim(X¥odotV)

つまり、

  • #(X)・dim(V) = dim(X¥odotV) = dim(Map(X, V))

が成立します。有限次元ベクトル空間の次元は、有限集合の直積モノイド圏が作用する加群圏のあいだの準同型関手の例になります。

*1:反対圏が入る等式は、ラフに書くと分かりにくいですね。図式を使ったりして丁寧に考えてみてください。

*2:圏に対象集合を対応させる関手を Obj:CatSet、集合から余離散圏を作る関手を Codisc:SetCat とすると、CodiscとObjは随伴関手対になります。Set(Obj(C), S) ¥stackrel{¥sim}{=} Cat(C, Codisc(S)) という随伴同型があります。

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

2018-04-23 (月)

モノイド・スタンピングと単純スタンピング

| 11:15 | モノイド・スタンピングと単純スタンピングを含むブックマーク

僕はモノイド・スタンピング〈monoidal stamping〉という言葉をよく使います。この言葉を使い始めたのはバーボーサ*1〈Luis S. Barbosa〉ではないかと思います。つうか、バーボーサ以外の人が使っている例を僕は知りません(僕自身は盛んに使ってますが)。

モノイド・スタンピングとは、M = (M, m, e) をモノイドとして、任意の集合XにMを直積で掛け算する操作です。F(X) = X×M, F(f:X→Y) = (f×idM:X×M→Y×M) とすると、Fは関手 SetSet になります。それだけではなくて、モノイドの乗法mと単位eを使って関手Fを台とするモナドを構成できます。このモナドモノイド・スタンピング・モナド〈monoidal stamping monad〉と呼びます*2。具体例は「単一代入のモノイド、スタンピングモナド、モナド工場」にあります。

もともとバーボーサは、計算概念〈notion of computation〉の一種としてモノイド・スタンピングを挙げています。計算概念には、次のような例があります。

  1. 部分性〈partiality〉
  2. 非決定性〈nondeterminism〉
  3. モノイド・スタンピング〈monoidal stamping〉

モッジ〈Eugenio Moggi〉に従えば、これらの計算概念は、モナドとそのクライスリ圏〈Kleisli category〉によって定式化できます。

  1. 部分性モナド=Maybeモナド=オプション・モナド
  2. 非決定性モナド=ベキ集合モナド
  3. モノイド・スタンピング・モナド

それぞれのモナドのクライスリ射(モナドで修飾した型への関数)を考えれば:

  1. 値が未定義になるかも知れない関数
  2. 値の候補が複数あるかも知れない関数
  3. 値の出力と共にコマンドを発行したり、ストレージへの書き込みを行う関数


F(X) = X×M からモナドを作るにはMのモノイド構造が必要ですが、単なる集合Aを直積する操作 F(X) := X×A でも関手にはなります。これをスタンピング関手〈stamping functor〉と呼びましょう。モノイドじゃなくて単なる集合だよ、と強調したいなら単純スタンピング関手〈simple stamping functor〉と言うことにします。そして、特定した対象Aはスタンプ対象〈stamp object〉とします。

集合圏に限らず一般のモノイド圏でスタンピング関手を考えることができます。C = (C, ¥otimes, I, α, λ, ρ) をモノイド圏とするとき、F(X) := X¥otimesA, F(f:X→Y) := f¥otimesidA でスタンピング関手を定義できます。Cが対称〈symmetric〉とは仮定してないので、左スタンピング関手と右スタンピング関手を区別する必要があります。

  • 左スタンピング関手: F(X) := A¥otimesX
  • 右スタンピング関手: F(X) := X¥otimesA

対称モノイド圏であっても、左右の区別はしたほうがいいと思います。

スタンピング関手は、スタンプ対象と左右の別で一意的に決まります -- これにいちいち名前を付けるほどのこともないので、無名のラムダ変数'-'(ハイフン)を使って、次のように書くことにしましょう。

  • 左スタンピング関手: (A¥otimes-)
  • 右スタンピング関手: (-¥otimesA)

さらに、ハイフンを省略してしまうこともあります。

  • 左スタンピング関手: (A¥otimes)
  • 右スタンピング関手: (¥otimesA)

Haskellのセクションと同じ記法になります。


スタンピング関手は、関手としては非常に簡単なものですが、テンソル強度〈tensorial strength〉や“加群圏〈module category〉の準同型”などに関係して出現します。簡単ではあっても、ツマラナイわけではありません。

最近、スタンピング関手/スタンピング・モナドと、その拡張概念に関する計算法について、もう一度考え直す必要があるんじゃないかと思っています。

*1:スペイン語(https://ja.forvo.com/search/Barbosa/es/)だと「バルボサ」に近い音ですが、ポルトガル語(https://ja.forvo.com/search/Barbosa/pt/)だと「バーボーサ」に近いようです。Luis S. Barbosaはポルトガルのミーニョ大学(https://www.uminho.pt/)の人なので、たぶんポルトガル語の人名かと。

*2:コモノイドをスタンピングすれば、コモナドを作れます。

2018-04-20 (金)

TypeScriptでモナド 改善編

| 10:20 | TypeScriptでモナド 改善編を含むブックマーク

以前にTypeScriptでモナドを書いてみたことがあるのですが、名前の組織化がイマイチな感じだったので改善してみました。

内容:

  1. モナド
  2. モナドの各部を表す名前
  3. TypeScriptへの翻訳
  4. TypeScriptコード
  5. おわりに

モナド

モナドなんて知らないぞ、って方は次の記事を読んでみてください。最近、入門的記事をあんまり書かないので、だいぶ昔の記事ですが。

圏論の立場からのモナドの定義は:

いや、そもそも圏論が分からん、て方は次の記事からはじめてはいかがでしょう。

このブログは、モナドで溢れてます。あまり整理されてませんが、探せば色々な話題が見つかるでしょう。

モナドの定義としては、クライスリ拡張オペレーターを使う“拡張方式”と、自己関手圏内のモノイドとして定義する“モノイド方式”があります。今回使うのは“モノイド方式”のほうです。

Cを圏とします。C上のモナドmonad〉は3つの構成素を持ちます。

  1. C上の自己関手 F:CC
  2. 自然変換 μ::F*F⇒F:CC
  3. 自然変換 η::C^⇒F:CC

C^は、圏Cの恒等関手IdCのことです。その他、ここで使う記号については次を参照してください。

モナドを(F, μ, η)のように書きます。F:CCモナド台関手〈underlying functor〉、μ::F*F⇒F:CCモナド乗法〈multiplication〉、η::C^⇒F:CCモナド単位〈unit〉と呼びます。3つ組(F, μ, η)がモナドであるためには、次の法則を満たす必要があります。

  • [結合律] (μ*F^);μ = (F^*μ);μ
  • [左単位律] (η*F^);μ = F^
  • [右単位律] (F^*η);μ = F^

単位律における左右の別は、書き方により変わります。反図式順記法で書くなら:

  • [結合律] μ¥circ(F^・μ) = μ¥circ(μ・F^);
  • [右単位律] μ¥circ(F^・η) = F^
  • [左単位律] μ¥circ(η・F^) = F^

2つのモナド M = (F, μ, η), N = (G, ν, ε) があるとき、記号を節約するために、M = (FM, μM, ηM), N = (FN, μN, ηN) のような書き方をします。さらには、記号の乱用により、F = (F, μF, ηF), G = (G, μG, ηG) とも書きます。モナド全体とモナドの台関手を同じ文字で表します。FやGがモナドを表しているのか、台関手を表しているのかは文脈で判断してください。

モナドの各部を表す名前

以前次の記事で、TypeScriptでモナドを書いてみました。

上記の過去記事内で:

型構成子と型パラメータを持つ関数があれば、とりあえずモナドは定義できるのですが、モナドを構成する型構成子と総称関数達をうまくまとめる機構が欠けている感じはします。

“うまくまとめる機構”が欠けているとは、名前の組織化/名前の管理がイマイチだということです。次の記事はその点に関する改良案です -- が、満足できる所までいってません。

TypeScriptのモジュールとは内部モジュールのことで、現在は名前空間〈namespace〉と呼ばれています。今回使う道具も名前空間〈内部モジュール〉です。

この記事の目的・目標は、前節で導入した F = (F, μF, ηF) に出来るだけ近い書き方をTypeScriptで実現することです。ただし、関手Fを(F, mapF)のように分解します。この点を以下で説明しましょう。

関手 F:CC は、対象部分〈object part〉と射部分〈morphism part〉に分解できます。

  • Fobj:Obj(C)→Obj(C)
  • Fmor:Mor(C)→Mor(C)

対象部分Fobjを単にFと書き、射部分FmorをmapFと書くことにします。mapの由来は圏論ではなくて関数型言語で、ある種の高階関数をmap関数と呼ぶからです。この書き方に従うと、モナドは次のような4つ組で書けます。

  • F = (F, mapF, μF, ηF)

モナド全体と台関手の射部分が同じ名前になります(オーバーロードされます)。Gが別なモナドの名前なら、次のように書けます。

  • G = (G, mapG, μG, ηG)

TypeScriptへの翻訳

例題にはMaybeモナドを使います。「TypeScriptのモジュール:Maybeモナドの例」と同じ例なので、必要があればソチラを参照してください。

例題のモナドの名前がMaybeですから、次のようになります。

  • Maybe = (Maybe, mapMaybe, μMaybe, ηMaybe)

しかしプログラミング言語では、上付き添字やギリシャ文字は使えません。次のようにします。

  • 上付き添字の代わりに、ドット区切り接頭辞を使う。mapMaybeはMaybe.mapとなる。
  • ギリシャ文字μの代わりに英字綴joinを使う。
  • ギリシャ文字ηの代わりに英字綴unitを使う。

そうすると:

  • Maybe = (Maybe, Maybe.map, Maybe.join, Maybe.unit)

上記モナドの4つの構成素が、プログラミング言語TypeScriptにおいて何になるかと言うと:

  1. Maybeは、型パラメータを1つ取る型構成子である。
  2. Maybe.mapは、型パラメータを2つ取る総称高階関数である。Maybe.map<X, Y>:Maybe<X>→Maybe<Y>
  3. Maybe.joinは、型パラメータを1つ取る総称関数である。Maybe.join<X>:Maybe<Maybe<X>>→Maybe<X>
  4. Maybe.unitは、型パラメータを1つ取る総称関数である。Maybe.unit<X>:X→Maybe<X>

モナド全体を表す名前Maybeは、名前空間の名前とします。TypeScriptでは、型構成子(型パラメータを持つ型別名)と名前空間の名前が同じになっても問題ありません*1

TypeScriptコード

早速、前節の翻訳方針にしたがって、MaybeモナドをTypeScriptで書いてみます。

// 補助的なクラス
class MaybeValue<X> {
  defined: boolean;
  value: X|undefined;
  constructor(defined: boolean, value: X|undefined) {
    this.defined = defined;
    this.value = value;
  }
}

// 型構成子=モナドの台関手の対象部分
type Maybe<X> = MaybeValue<X>;

// 名前空間=モナドの他の部分をまとめる入れ物
namespace Maybe {
  // map総称関数=モナドの台関手の射部分
  export
  function map<X, Y>(f: (x:X)=>Y): (mx:Maybe<X>)=>Maybe<Y> {
    return (
      (mx: Maybe<X>)=>{
        if (mx.defined) {
          return new MaybeValue<Y>(true, f(mx.value));
        } else {
          return new MaybeValue<Y>(false, undefined);
        }
      });
  }
  // join総称関数=モナドの乗法
  export
  function join<X>(mmx: Maybe<Maybe<X>>): Maybe<X> {
    if (mmx.defined) {
      return mmx.value;
    } else {
      return new MaybeValue<X>(false, undefined);
    }
  }
  // unit総称関数=モナドの単位
  export
  function unit<X>(x: X): Maybe<X> {
    return new MaybeValue<X>(true, x);
  }
}

これで、名前はかなりスッキリと編成されました。けっこう満足できます。

機能的にはこれで十分ですが、HaskellのMaybeモナドだと、Just, Nothingというデータ構成子が使えます。これらはあれば便利なので、追加しておきましょう。map, join, unitのなかも少し書き換えました。


// ...省略...

// 型構成子=モナドの台関手の対象部分
type Maybe<X> = MaybeValue<X>;

// 名前空間=モナドの他の部分をまとめる入れ物
namespace Maybe {
  // JUST総称関数 確定した値を生成する
  export
  function JUST<X>(x: X): Maybe<X> {
    return new MaybeValue<X>(true, x);
  }
  // NOTHING総称関数 値がないことを示す値を生成する
  export
  function NOTHING<X>(): Maybe<X> {
    return new MaybeValue<X>(false, undefined);
  }
  // map総称関数=モナドの台関手の射部分
  export
  function map<X, Y>(f: (x:X)=>Y): (mx: Maybe<X>)=>Maybe<Y> {
    return (
      (mx: Maybe<X>)=>{
        if (mx.defined) {
          return new MaybeValue<Y>(true, f(mx.value));
        } else {
          return NOTHING<Y>();
        }
      });
  }
  // join総称関数=モナドの乗法
  export
  function join<X>(mmx: Maybe<Maybe<X>>): Maybe<X> {
    if (mmx.defined) {
      return mmx.value;
    } else {
      return NOTHING<X>();
    }
  }
  // unit総称関数=モナドの単位
  export
  function unit<X>(x: X): Maybe<X> {
    return JUST<X>(x);
  }
}

[追記]unitとJUSTがまったく同じ機能で重複している理由は:

  • unitは、どんなモナドでも備えるべき関数の名前です。TypeScriptには、名前空間の仕様を記述する機能はないので、人のあいだのお約束(命名規則)です。
  • JUSTは、Maybeモナド特有の名前で、習慣的に使われているので入れてみたものです。他のモナドでは無意味な名前だろうし、必須でもありません。[/追記]

おわりに

関手の射部分、モナドの乗法/単位に関する名前(ローカル名)は、コレダという定番はなくて、けっこうゆらいでいます。

  • 関手の射部分: fmap, map, lift
  • モナドの単位: single, return, unit, embed
  • モナドの乗法: flatten, join, union, merge

グローバルな合意は難しいですが、ローカル・ルールでいいなら、どれかに決めて守ればいいだけです。

実は、一種のテストとして、モナド法則を部分的に確認してみたのですが、その話は長くなりそうなので割愛しました。別な記事にするかも知れません。

今回の名付け方式を使って、モナドの準同型、ベックの分配法則テンソル強度などもTypeScriptで書けそうです。これも別記事ですね。

*1:この事実に気付いたことで、今回の名前方式が実現できました。

2018-04-18 (水)

距離空間と位相空間と連続写像

| 12:10 | 距離空間と位相空間と連続写像を含むブックマーク

「イプシロン-デルタ論法って、なんすかアレ? 全然分からないっす!」と言っていた
N君も、最近では一般の位相空間の話なんぞをしています。今回は、距離空間位相空間のあいだの関係を把握するヒントを書いておきます。

内容:

  1. 距離と開球体の復習
  2. 写像の連続性
  3. 開集合族
  4. 距離連続性と位相連続性
  5. 2つの連続性が同値であること
  6. 距離から導かれる位相と距離とは無関係な位相

距離と開球体の復習

イプシロン-デルタ論法はなぜ難しいのか? どうしたら分かるのか? 分かる必要があるのか?」と同じ用語・記法を使うことにします。集合Xとその上の距離関数 dX:X×X→R≧0 を組にした(X, dX)が距離空間〈metric space〉でした。記号の乱用により X = (X, dX) とも書きます。同じ文字Xを、距離空間の意味でも、その台集合〈underlying set〉の意味でも使います。また、dXのXが明らかなときは単にdと略記します。

距離空間(X, d)があるとき、a∈X と r∈R>0R>0 = {r∈R | r > 0})に対して

  • OBallX(a, r) := {x∈X | d(a, x) < r}

として開球体〈open ball〉が定義できます。aは開球体の中心、rは開球体の半径です。「球」だけでは、球体〈ball〉か球面〈sphere〉か曖昧ですが、ここでは球体だけを扱うので 球=球体 だと解釈してください。よって、OBallX(a, r)を開球とも呼びます。

開球の集まりを、

  • OBALLSX(a) = {OBall(a, r) | r∈R>0}
  • OBALLSX = {OBall(a, r) | a∈X, r∈R>0}

とします。OBALLSX(a)とOBALLSXとの関係は、

  • OBALLSX(a) = {A∈OBALLSX | center(A) = a} (centerは球体の中心)
  • OBALLSX = ∪(a∈X | OBALLSX(a)) (aを動かした合併)

となります。OBALLSX(a)やOBALLSXはXの開球の集まりなので、開球族開球体族〈family of open balls〉と呼びます。

X = Rn, d = (標準のユークリッド距離) のケースでは、

  • OBALLSRn(a) ¥stackrel{¥sim}{=} R>0
  • OBALLSRn ¥stackrel{¥sim}{=} Rn×R>0

という集合の同型があります。一般の距離空間Xでは、同型になっているとは限りませんが、aを固定したOBALLSX(a)とOBALLSXはそれぞれ、R>0とX×R>0で(重複を許して)パラメトライズ(またはインデキシング)されるとは言えます。

写像の連続性

2つの距離空間 (X, dX), (Y, dY) があって、f:X→Y は写像だとします。このとき、点aでのfの連続性〈continuity〉を、距離関数と正実数の大小関係を使って表現する方法が、イプシロン-デルタ論法〈ε-δ論法〉でした。

  • 自然言語: どんな正実数δに対しても、適当な正実数εを選べて、Xの点xが dX(a, x) < ε ならば、dY(f(a), f(x)) < δ とすることが出来る。
  • 論理式: ∀δ∈R>0.∃ε∈R>0.(∀x∈X.(dX(a, x) < ε ⇒ dY(f(a), f(x)) < δ))

この書き方はゴチャゴチャしていて何を言いたいか分かりにくく、直感的描像も得られないので、開球を使った記述のほうが望ましいだろう、ということが「イプシロン-デルタ論法はなぜ難しいのか? どうしたら分かるのか? 分かる必要があるのか?」の内容でした。

開球の族OBALLSX, OBALLSYを使うと、点aでのfの連続性の記述は次のようになります。

  • 自然言語: 任意の“f(a)を中心とするYの開球B”に対して、aを中心とするXの開球Aがあって、f*(A)⊆B と出来る。
  • 論理式: ∀B∈OBALLSY(f(a)).∃A∈OBALLSX(a). f*(A)⊆B

Y側の開球Bに対して、X側の開球Aを選んで f*(A)⊆B を達成するゲームと考えればいいのでしたね。ここで、f*(A)は、fのよる集合Aの像〈image〉で、f*(A) = {y∈Y | ∃x∈X.(x∈A ∧ f(x) = y)} です。単に像をf(A)と書くことも多いですが、混乱しないように区別しています。ちなみに、逆像〈inverse image〉は(f-1(B)ではなくて)f*(B)とここでは書きます。f*(B) = {x∈X | ∃y∈Y.(y∈B ∧ f(x) = y)}。

一点aでのfの連続性が上記のように定義できれば、Xのすべての点で連続な写像〈関数〉として、連続写像連続関数 | continuous {map | function}〉が定義されます。

開集合族

距離空間 X = (X, d) の部分集合U(U⊆X)が開集合〈open set〉であるとは、次のことでした。

  • 自然言語: Uの任意の点xに対して、xを中心とする開球Aで、A⊆U となるものが在る。
  • 論理式: ∀x∈U.∃A∈OBALLSX(x). A⊆U

距離空間Xの開集合の全体をOSETSXとします。OSETSXは“集合の集合”なので、

  • OSETSX ⊆ Pow(X)
  • OSETSX∈Pow(Pow(X))

Pow(X)はXのベキ集合で、Y∈Pow(X) ⇔ Y⊆Y です。OSETSX(Xの開集合の集合)は、Xのベキ集合のベキ集合の要素です。OSETSXをXの開集合族〈family of open sets〉と呼びます。

ところで、Iをインデックス集合〈{index | indexing} set〉として、I→OSETSX という写像のことも開集合族と言いますね。こっちはインデックス族〈indexed family〉です。用語・記法の乱用・不整合・混乱は日常茶飯事なので、気にしてたらキリがないのですが、紛らわしいときは、OSETSXのほうを全開集合族*1と呼ぶことにします。全開集合族の部分集合(部分族、これも集合の集合)、または全開集合族への写像を、「開集合族」と呼ぶ可能性があるわけです。

距離空間Xの全開集合族OSETSXは次の性質を持ちます。

  1. ¥emptyset∈OSETSX
  2. X∈OSETSX
  3. U, V∈OSETSX ならば、(U∩V)∈OSETSX
  4. (Ui | i∈I) が開集合のインデックス族ならば、(∪(Ui | i∈I))∈OSETSX

一番目の「 ¥emptyset∈OSETSX 」は、そう約束していると思ってもかまいません。論理的には、開集合の条件 ∀x∈U.(...) を ∀x.(x∈U ⇒ ...) と書き換えてみると、x∈¥emptyset が偽になるので、全体は真となり空集合¥emptysetは開集合となります。

二番目の「 X∈OSETSX 」で、「Xに孤立点があったら成立しないのでは?」という質問を受けたことがあります。X⊆Rnの場合、OBallRn(a, r)とOBallX(a, r)を同じだと思ってしまう誤解がありますが、OBallX(a, r) = X∩OBallRn(a, r) です(同じとは限らない)。OBallRn(a, r)⊆X じゃなくても OBallX(a, r)⊆X となることはあります。a∈X が孤立点のとき、適当なεに関して、{a} = OBallX(a, ε) となりますが、{a}⊆X なので、OBallX(a, ε)⊆X です。孤立点であれ何であれ、xを中心とする小さな(いや、小さくなくても)開球はスッポリXに入ります。

三番目「 U, V∈OSETSX ならば、(U∩V)∈OSETSX 」は特に問題ないでしょう。練習問題ですね。

四番目「 (Ui | i∈I) が開集合のインデックス族ならば、(∪(Ui | i∈I))∈OSETSX 」は、インデックス族を使わなくても、全開集合族(集合の集合)OSETSXの任意の部分集合の合併が再びOSETSXの要素だ、とも言えます。

  • W⊆OSETSX ならば、∪(W)∈OSETSX

この性質も簡単に分かると思います。

距離空間とは限らない位相空間では、上記の全開集合族の性質を基本に据えます。距離空間では、実数値を取る距離関数や実数の大小比較(不等号)などで議論しました。そのテの数量的評価から、“部分集合/部分集合の集合(集合族)/写像の像・逆像”などへと記述の道具が変わってきます。したがって、“集合の集合”や“集合引数を取る関数”や、“集合値を返す関数”などに慣れる必要があるのです。

距離連続性と位相連続性

距離とは関係なく位相空間を定義するときは、台集合XとXの部分集合の族OXOX⊆Pow(X))の組(X, OX)で、OXが前節で出した全開集合族と同じ性質を満たすものを考えます。

  1. ¥emptysetOX
  2. X∈OX
  3. U, V∈OX ならば、(U∩V)∈OX
  4. (Ui | i∈I) がOXの要素のインデックス族ならば、(∪(Ui | i∈I))∈OX

一般の位相空間では正実数値の大小比較とかの数量的概念は使えなく/使わなくなります。数量的記述と集合的記述の中間的な、あるいは架け橋的な定式化が開球族による連続性の定義(「イプシロン-デルタ論法はなぜ難しいのか? どうしたら分かるのか? 分かる必要があるのか?」の定義)でした。開球は、中心と半径により定義されますが、開球族では正実数値である半径を表立って扱うことはなくなります。

ここから後では、距離空間の開球族を用いた連続性の定義と、開集合族を用いた連続性の定義が同値であることを示しましょう。開球の族OBALLSX, OBALLSYを使った連続性の定義は前節で述べたとおりです。開集合を用いた連続性の定義は次のようになります。

前節と同じ設定で、f:X→Y が連続であるとは:

  • 自然言語: 任意のYの開集合Vに対して、f*(V)はXの開集合である。
  • 論理式: ∀V∈OSETSY. f*(V)∈OSETSY

2つの連続性の定義は結果的に同値だとは言いながら、区別しないと同値性のステートメントを書けないので、距離空間の意味の連続性を距離連続、位相空間の意味の連続性を位相連続と区別しておきます。で、示すべきことは:

  • f:X→Y が距離連続 ⇔ f:X→Y が位相連続

2つの連続性が同値であること

「 f:X→Y が距離連続 ⇒ f:X→Y が位相連続 」を先に示しましょう。ターゲット命題は含意(⇒)が入れ子になるので、証明の“お膳立て”シリーズで導入した証明要求の書き方を使いましょう。我々に課せられた証明要求は次のとおりです。

  • Γ/ f:X→Y が距離連続 |-? f:X→Y が位相連続

ここで、Γ〈ガンマ〉は使ってよい予備知識をまとめて表したものです。位相連続であることを論理式に展開すると:

  • Γ/ f:X→Y が距離連続 |-? ∀V∈OSETSY. f*(V)∈OSETSX

右辺の全称束縛を、Vを自由変数にして左辺に移すと:

  • Γ/ f:X→Y が距離連続, V∈OSETSY |-? f*(V)∈OSETSX

開集合の定義により、f*(V)∈OSETSY を書き換えると:

  • Γ/ f:X→Y が距離連続, V∈OSETSY |-? ∀x∈f*(V).∃A∈OBALLSX(x). A⊆f*(V)

右辺の全称束縛を、xを自由変数にして左辺に移すと:

  • Γ/ f:X→Y が距離連続, V∈OSETSY, x∈f*(V) |-? ∃A∈OBALLSX(x). A⊆f*(V)

x∈f*(V) を同値な命題 f(x)∈V と置き換えて:

  • Γ/ f:X→Y が距離連続, V∈OSETSY, f(x)∈V |-? ∃A∈OBALLSX(x). A⊆f*(V)

ここで、一般的な定理として、次を思い出しましょう。

  • f*(S)⊆T ⇔ S⊆f*(T)

順序随伴性: ガロア接続の圏論」で述べた順序随伴性の例2です。これを A⊆f*(V) に対して適用すると:

  • f*(A)⊆V ⇔ A⊆f*(V)

証明要求に出てくる命題を同値な命題で置き換えてもいいので、我々の証明要求は次の形になります。

  • Γ/ f:X→Y が距離連続, V∈OSETSY, f(x)∈V |-? ∃A∈OBALLSX(x). f*(A)⊆V

証明要求の変形(お膳立て)はこのくらいでいいでしょう。前方推論〈forward reasoning〉による証明に切り替えます。

V∈OSETSY, f(x)∈V より、B∈OBALLSY(f(x)), B⊆V となるYの開球Bが存在します。fは距離連続だったので、Yの開球Bに対して、f*(A)⊆B となるXの開球Aが取れます(A∈OBALLSX(x))。f*(A)⊆B, B⊆V より f*(A)⊆V 。これで目的の命題(証明要求の左辺)を示せたので、証明要求が満足されて、次の証明判断が得られました。

  • Γ/ f:X→Y が距離連続, V∈OSETSY, f(x)∈V |- ∃A∈OBALLSX(x). f*(A)⊆V

これで、当初のターゲット命題「 f:X→Y が距離連続 ⇒ f:X→Y が位相連続 」が示されたことになります。逆向きの含意「 f:X→Y が位相連続 ⇒ f:X→Y が距離連続 」については、証明のお膳立てだけ示しておきます。

  Γ/ f:X→Y が位相連続 |-? f:X→Y が距離連続
  --------------------------------------------------- 距離連続の定義
  Γ/ f:X→Y が位相連続 |-?
    ∀x∈X.∀B∈OBALLSY(f(x)).∃A∈OBALLSX(x). fX(A)⊆B
  --------------------------------------------------- 全称束縛の変形
  Γ/ f:X→Y が位相連続, x∈X |-?
    ∀B∈OBALLSY(f(x)).∃A∈OBALLSX(x). f*(A)⊆B
  --------------------------------------------------- 全称束縛の変形
  Γ/ f:X→Y が位相連続, x∈X, B∈OBALLSY(f(x)) |-?
    ∃A∈OBALLSX(x). f*(A)⊆B
  --------------------------------------------------- 同値な命題で置き換え
  Γ/ f:X→Y が位相連続, x∈X, B∈OBALLSY(f(x)) |-?
    ∃A∈OBALLSX(x). A⊆f*(B)

距離から導かれる位相と距離とは無関係な位相

さて、今示した「 距離連続 ⇔ 位相連続 」がどんな意味・意義を持つかを考えてみましょう。

今回扱ってきたのは距離空間です(一般の位相空間の定義にも触れてますが)。距離空間(X, dX)から出発して、全開集合族を付加した(X, dX, OSETSX)を考えると、写像の連続性の定義は、dXには一切言及せずに、OSETSXの言葉だけでも記述できることが分かりました。

であるならば、距離から出発するのではなくて、「全開集合族ありき」の(X, OSETSX)から連続性を定義しても連続関数の理論は出来そうです。実際に、連続関数を載せる構造は、「集合+全開集合族」がふさわしいと信じられています。抽象的に全開集合族を規定する公理が先に述べたOXの性質です。

  1. ¥emptysetOX
  2. X∈OX
  3. U, V∈OX ならば、(U∩V)∈OX
  4. (Ui | i∈I) がOXの要素のインデックス族ならば、(∪(Ui | i∈I))∈OX

これらの公理を満たす全開集合族OXを備えた集合(X, OX)が位相空間〈topological space〉です*2。抽象的・公理的な意味での全開集合族を位相〈topology〉と呼ぶので、「位相空間とは位相を備えた空間(点集合)」ということで用語法の辻褄はあいます。

距離から導かれた位相の例は多いですが、距離とはまったく違った方法で定義される位相もあります。計算科学と順序に由来するスコット位相〈Scott topology〉、論理とブール代数に由来するストーン空間〈Stone space〉の位相、代数幾何に由来するザリスキー位相〈Zariski topology〉などは距離と無関係です。距離では捉えられない空間を扱うには、開集合族ベースの定義に移行せざるを得ないのです。

距離と無関係な位相と言えば、随分以前に、ブール代数のストーン空間の構成は、二元体上の可換環のスペクトルにザリスキー位相を入れることと同じだ、という話を書いたことがあります。

一方で、我々が常識的に想定する「空間」は距離空間なので、距離から導かれた位相はやはり重要です。距離から導かれる位相の特徴付けは熱心に研究された課題で、幾つかの距離化定理〈metrization theorems〉があります。


距離は、色々な位相空間の例を提供してくれますが、距離では定義できない位相空間もあります。距離と無関係な位相空間にも目を向けましょう、というお話でした。

*1:これはこれで、全開〈フルオープン〉な集合の族みたいで、語感が良くないのですが。

*2:位相を定義する方法は、開集合族以外にもたくさんあります。歴史的な紆余曲折を経て、現在の標準的定義が開集合族の公理に落ち着いている、ということです。

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

2018-04-13 (金)

指数関手と構文論・意味論

| 17:35 | 指数関手と構文論・意味論を含むブックマーク

論理やプログラミング言語の構文論と意味論の枠組みとして、指数関手が使えるだろう/使いたい、と思っています。そのなかで、高次圏(少なくとも厳密2-圏)カン拡張も必要となります。

内容:

  1. 動機:構文論・意味論の記述
  2. 指数関数とその用語法
  3. 指数関数から指数関手へ
  4. 指数関手=反変連続・共変連続なモノイド作用
  5. 二項指数関手の例
  6. 一般化:2次元化と相対化

動機:構文論・意味論の記述

論理系〈logical system〉を作るとき、基本記号を決めて、それから項〈term〉や論理式〈formula〉を定義します。これは論理の構文論〈syntax〉です。項や論理式の意味は、意味論〈semantics〉として定義します。項には意味として値や関数が対応し、論理式には意味として真偽値が対応します。

プログラミング言語の場合も同様な構成をします。本物のプログラミング言語は複雑なので、単純化して、例えばラムダ式〈lambda {expression | term}〉を構文的な対象物と考えて、意味はデカルト閉圏〈cartesian closed category〉で与えたりします。このテの意味論は表示的意味論〈denotational semantics〉と呼ばれたりします。ラムダ計算の表示的意味論に関しては「セマンティック駆動な圏的ラムダ計算とシーケント」とそこから参照される記事群を見てください。

僕は、フローチャートストリング図が好きなのですが、絵図では、幾何的図形が構文的な対象となります。絵図はグラフ構造を持つので、頂点や辺に“意味”を対応させることが意味論となります。意味的対象物は、圏の対象や射になります。絵図もまた言語であるという話は「「コミュニケーションの多次元化」という革命に立ち会っているのだと思う」に書いています。

上記のような、何らかの系〈system〉の構文論・意味論を、全体的・俯瞰的に定式化したいのです。この動機のもとで、どんな道具が使えるだろう?適切だろう? と考えてみると、指数関手〈exponential functor〉に思い至るのです。

以下では、指数関手についてザッと説明します(細部は端折ります)。指数関手を使って構文論・意味論を記述するところまでは話が届いていません。そこいらの話題はまたボチボチと。

指数関数とその用語法

まずは、数(実数)を変数とする指数関数の話からはじめます。この段階で既に、用語法がグチャグチャなので、少し整理を試みます。

変数aとxに対する ax2変数の指数関数〈exponential function {of | with} two {variables | arguments | parameters}〉と呼びます。この場合、aもxも変数です。次の形にも書きます。

  • e(x, a) = ax

aとxの順序が普通と逆ですが、後で出てくる記法と合わせるためです。

2変数の指数関数で、変数aを固定した(定数とした)1変数関数を、1変数の指数関数〈exponential function {of | with} one {variable | argument | parameter}〉と呼びます。普通「指数関数」というとコッチですね。

  • ea(x) = ax
  • ea = λx.(ax) (ラムダ記法による定義)

2変数/1変数の指数関数に関わる言葉を英語と日本語のWikipediaで調べてみました。

英語と日本語の対応は:

? 冪乗
exponentiation 冪演算
power function 冪函数
exponent 冪指数
base
repeated multiplication 累乗
exponential function 指数関数

ここで僕の漢字の使い方について注意しておくと; 「データベースへの論理的アプローチ: NULLについてチャンと考えよう」より:

「ベキ」は古い難しい字で「冪」と書くか、あるいは略字の「巾」を使います。どちらも難読なので、僕はカタカナ書きしています。

Wikipediaでは「関数」と「函数」が混じってますが、事典であれば表記を統一したほうがいいかと思います(現実的に無理かも知れないが)。「函数」は古い表記なんですが、若い人のほうが好んで使うような気がします。一種の復古主義なのか、泰斗・俊英を擁するスクールが使っているからなのか、ともかく「函数」のほうがカッコイイと思われているみたい。

それはともかく; 日本語Wikipediaの見出し語「冪乗」の英語は何だか分かりませんでした。たぶん、exponentiation〈冪演算〉とpower〈冪〉の両方の意味で使うんだと思います。しかし、冪演算という言葉は一般的じゃないです。実際のところは、冪、冪乗、指数という言葉が曖昧イイカゲンに使われていますね。

この記事では次のようにします。

exponentiation 2変数指数関数
power function ベキ関数, ベキ乗関数
exponent 指数部
base
exponential function 1変数指数関数

意味は:

  • xを固定して変数aの関数とみた axベキ関数、またはベキ乗関数と呼ぶ。
  • ax のxを指数部と呼ぶ。
  • ax のaをと呼ぶ。

exponentiationとexponential functionの区別は、明示的に形容詞「1変数」「2変数」を付けることにします。exponent=指数部 は、浮動小数点数で使われている言葉なので馴染みがあるでしょう。

実数の関数としては、power function=ベキ関数 で問題ないと思いますが、関数を関手に置き換えるとマズイことになります。集合Xのベキ集合Pow(X)は関手となり、これをベキ関手〈power functor〉と呼ぶことがあるのです*1 -- 共変ベキ関手 Pow*:SetSet、反変ベキ関手 Pow*:SetopSet。Xのベキ集合は、2 = {0. 1} として 2X と書けるので、べき関数じゃなくて(1変数の)指数関数に似てるんですが、今さらどうにもなりません

関手の場合は、Xを固定して変数Aの関数とみた AXベキ乗関手と呼んで、ベキ集合関手としてのベキ関手と区別しましょう。英語でなんて言っていいか分からんけど、乗=multiplication として、multiplicative-power functor とか? かな。

ところで、exponent〈指数部〉とベキ〈power〉の違いを説明する次の絵をみつけました。

*2

わかりやすいんだけど、実際の用法はこの絵の通りでもないですね。https://en.wikipedia.org/wiki/Exponentiation#Power_functions だと、

Real functions of the form f(x)=cxn with c≠0 are sometimes called power functions.

だし、http://wmueller.com/precalculus/families/1_41.html だと、

  • f(x) = axb

The parameter b , called either the exponent or the power, determines the function's rates of growth or decay.

ってな具合。

この辺のところって、あんまりチャンと区別してないよね。僕もイイカゲンです。

ホム関手が指数とみなされる理由」にて:

指数関数とは、ba の形で、二変数関数として扱うことも、aかbのどちらか一方を固定した一変数関数とみなすこともあります。aを固定した λx.xa は、指数関数というよりベキ(漢字で書くと冪)関数ですが、ここでは、「指数、ベキ(冪)、累乗」をうるさく区別しないことにします。

指数関数から指数関手へ

1変数指数関数か2変数指数関数かが文脈から分かるとき、またはどっちでもいいときは、単に指数関数という言葉を使います。

指数関数の性質を列挙します。

  1. a0 = 1
  2. ax+y = axay
  3. 1x = 1
  4. (ab)x = axbx
  5. a1 = a
  6. (ax)y = axy

関数呼び出し形式 e(x, a) で書くなら:

  1. e(0, a) = 1
  2. e(x + y, a) = e(x, a)×e(y, a)
  3. e(x, 1) = 1
  4. e(x, a×b) = e(x, a)×e(x, b)
  5. e(1, a) = a
  6. e(y, e(x, a)) = e(x・y, a)

これらと類似の性質を持った二項関手(双関手)として二項指数関手〈{binary | 2-arguent} exponential functor | exponentiation bifunctor〉を定義します。

Xは始対象0と直和〈デカルト余積〉+を持ち、それとは別にモノイド積¥otimes、モノイド単位Iを持つとします。圏Aは終対象1と直積〈デカルト積〉×を持つとします。上記の2変数指数関数の性質を、二項関手 E:Xop×AA の性質に翻訳すると、次のようになります。

  1. E(0, A) ¥stackrel{¥sim}{=} 1
  2. E(X + Y, A) ¥stackrel{¥sim}{=} E(X, A)×E(Y, A)
  3. E(X, 1) ¥stackrel{¥sim}{=} 1
  4. E(X, A×B) ¥stackrel{¥sim}{=} E(X, A)×E(X, B)
  5. E(I, A) ¥stackrel{¥sim}{=} A
  6. E(Y, E(X, A)) ¥stackrel{¥sim}{=} E(X¥otimesY, A)

これらの性質を持つ二項関手 E:Xop×AA が、二項指数関手〈指数二項関手〉です。第一変数(モノイド圏X上を走る変数)が反変であることに注意してください。

Cが始対象/直和を持つデカルト閉圏だとして、X = A := C と置いて、モノイド積¥otimesとモノイド単位Iを直積×と終対象1とすれば、デカルト閉圏の指数〈exponentiation〉E(-, -) = [-, -] :Cop×CC は上記の性質を持ちます。

指数関手=反変連続・共変連続なモノイド作用

Qを箙〈えびら | quiver〉(多重辺・自己ループ辺を許す有向グラフ)とします。箙から圏への箙準同型写像図式〈diagram〉と呼びます。Qから自由生成した圏を Q = FreeCat(Q) とします。“Qからの図式”と“Qからの関手”はあまり区別する必要がありません。次の随伴系があるからです。

  • Cat(Q, C) ¥stackrel{¥sim}{=} Quiv(Q, U(C))

ここで、Quivは箙の圏で、Uは圏から箙への忘却関手 CatQuiv です。この随伴系による1:1対応により、図式と関手は適宜同一視します。

Φを箙のクラス(大きいかも知れない集合)として、Q∈Φ であるQからの図式 D:Q→C極限を持つとき、圏CΦ-完備〈Φ-complete〉と呼びます。

例えば、Φが有限離散箙(有限個の頂点だけの箙)のクラスのとき、Φ-完備は、終対象と直積を持つことです。Φが有限箙のクラスのときのΦ-完備は、有限完備と呼びます。Φが任意の(小さい)箙からなるクラスのとき、Φ-完備を単に完備と言います。

Φ-余完備〈Φ-cocomplete〉はΦ-完備の双対概念で、Φに属する箙からの図式が余極限を持つことです。

CDが共にΦ-完備で、FはCからDへの関手だとします。このとき、任意の(Φに関する)極限が関手Fで保存されるなら、FはΦ-連続〈Φ-continuous〉だといいます。この言い方は、連続関数の古典的な定義とのアナロジーからです。

  • FがΦ-連続 ⇔ ∀Q∈Φ.( F(Lim(D:Q→C)) ¥stackrel{¥sim}{=} Lim(F¥circD:Q→D) )

Limは図式(あるいは関手)の極限対象を取るオペレーターです。

上記は共変関手の連続性でしたが、反変関手の場合は、余極限を取るオペレーターColimを用いて次の形に書いたほうが分かりやすいでしょう。

  • F(Colim(D:Q→C)) ¥stackrel{¥sim}{=} Lim(F¥circD:Q→D)

反対圏を使えば、極限だけで話を済ませることができますが、共変・反変を区別する場合は、「極限を極限に移す共変連続関手」「余極限を極限に移す反変連続関手」と捉えます。

さて、ここで2変数指数関数の次の性質を考えます。

  1. e(0, a) = 1
  2. e(x + y, a) = e(x, a)×e(y, a)

和を任意個の数の総和にするなら、この2つの等式は次の形に書けます。

e(¥sum_{i}x_i,¥, a) ¥,= ¥prod_{i}e(x_i,¥, a)

iが走る添字範囲が空のときは、0個の和が0/0個の積が1となるので、e(0, a) = 1 は総和形式に吸収されます。

関数を関手に置き換えます。総和の類似物が余極限、総乗の類似物が極限なので、次のように書けます。

  • E(Colim(S), A) ¥stackrel{¥sim}{=} Lim(E(S, A))

これは、二項関手 E:X×AA が、第一変数に関して反変連続であることを示します。完備性/連続性を与える箙のクラスΦは適当に決めます。

今度は別な2つの性質を考えましょう。

  1. e(x, 1) = 1
  2. e(x, a×b) = e(x, a)×e(x, b)

これは次のように書けますね。

e(x,¥, ¥prod_{i}a_i) ¥,= ¥prod_{i}e(x,¥, a_i)

関手における類似物は:

  • E(X, Lim(D)) ¥stackrel{¥sim}{=} Lim(E(X, D))

これは、二項関手 E:X×AA が、第ニ変数に関して共変連続であることを示します。

つまり、二項関手Eに関する以下の4つの性質は、「第一変数に関して反変連続・第ニ変数に関して共変連続」とまとめることができます。

  1. E(0, A) ¥stackrel{¥sim}{=} 1
  2. E(X + Y, A) ¥stackrel{¥sim}{=} E(X, A)×E(Y, A)
  3. E(X, 1) ¥stackrel{¥sim}{=} 1
  4. E(X, A×B) ¥stackrel{¥sim}{=} E(X, A)×E(X, B)

あと2つの性質が残っています。

  1. E(I, A) ¥stackrel{¥sim}{=} A
  2. E(Y, E(X, A)) ¥stackrel{¥sim}{=} E(X¥otimesY, A)

二項指数関手 E:X×AA を中置記法で¥odotと書いてみます。

  1. I¥odotA ¥stackrel{¥sim}{=} A
  2. Y¥odot(X¥odotA) ¥stackrel{¥sim}{=} (X¥otimesY)¥odotA

左右の選び方は交換可能なので、次のように書いても同じです。

  1. A¥odotI ¥stackrel{¥sim}{=} A
  2. (A¥odotX)¥odotY ¥stackrel{¥sim}{=} A¥odot(X¥otimesY)

これは、モノイド圏Xが、圏Aに左から(または右から)作用〈act〉していることを意味します。モノイド圏による作用を持つ圏を加群〈module category〉とも呼びます。次の記事で詳しく解説しています。

以上のことから、二項指数関手 E:X×AA とは、「第一変数に関して反変連続・第ニ変数に関して共変連続なモノイド作用」のことになります。あるいは、圏Aがモノイド圏X(の反対圏)による連続作用を持つ加群〈module category with continuous action〉だ、と言っても同じです。

二項指数関手の例

前節で説明した二項指数関手では、構文論・意味論の定式化にはまだ不十分です。もっと一般化する必要があります(次節参照)。しかし、一般化が出来てるわけではないので、現状の定義で幾つかの実例を紹介します。

ここでの話は、スピヴァックの関手データモデルとの類似点があるので、以下の記事が参考になるかも知れません。

Quivを箙の圏とします(既に出てきました)。Quivには始対象・直和・余等値核〈余イコライザー〉を定義できます。終対象・直積も定義できるので、モノイド積として直積を選びます。これにより、Quivは有限余完備でモノイド積を持つ圏となります。このQuivが、関手データモデルのスキーマの圏、インスティチューションの指標圏に相当します。

二項関手 E:Quivop×CatCat を次のように定義します。

  • E(X, C) := [X, C]

ここで、[-, -]は圏Catの内部ホム、つまり関手圏です。Xは箙ですが、Xは圏なので、関手圏[X, C]を作れます。

Eは、s:X→Y in Quiv に対してはsの前結合で反変的に、H:CD に対してはHの後結合で共変的になります。E(X, C)は、関手データモデルのデータベース状態〈データベース・インスタンス〉、インスティチューションのモデル圏に相当します。

  • E(s:X→Y, C) = [s, C] : [Y, C]→[X, C] in Cat
  • E(X, H:CD) = [s, H] : [X, C]→[X, D] in Cat

完備性と連続性を定義する箙クラスΦとしては、有限箙の圏を選んで、有限完備性/有限連続性を使うことにしましょう。

以上の状況で、Eが二項指数関手、つまり、反変連続・共変連続なモノイド作用であることを示すのは、けっこう面倒です。しかし、面倒なだけで難しくはありません。


今の例のバリアントとして、Quivを少し変形した例も作れます。“小さい圏の圏”をCatとすると、CatQuiv随伴関手対で結ばれます。これも先に出しました。

  • ΨQ,C: Cat(Q, C) ¥stackrel{¥sim}{=} Quiv(Q, U(C))

自由生成関手 (-):QuivCat と忘却関手 U:CatQuiv が随伴対なんですね。次のように書けます。

  • ΨQ,C: (-) -| U :CatQuiv

この随伴対から、圏Quiv上にモナドが誘導されます。モナドの台関手は U(-):QuivQuiv です。以下、U(-)をF(-)と略記します。また、記号の乱用 F = (F, μ, η) によりQuiv上のモナドを表します。

この設定で、圏Sを次のように定義します。

  • S := Kl(Quiv, F)

Kl(-, -)は、モナドのクライスリ圏です。Sのホムセットは、次のようになります。

  • S(X, Y) := Quiv(X, F(Y)) = Quiv(X, U(Y))

二項関手 E:Sop×CatCat の定義は先と同じです。

  • E(X, C) := [X, C]

細かい修正が入りますが、最初の例とほぼ同じようにして、Eが二項指数関手であることを示せます。


構文論・意味論とは関係ないのですが、指数関手〈連続なモノイド作用〉の例をもうひとつ出しておきます。関連する話題が次の記事にあります。

コンパクト・ハウスドルフ空間連続写像の圏をCompHous、バナッハ空間と有界(=連続)線形写像の圏をBanとします。「連続」という言葉が、位相的連続と圏論的連続の2つの意味で登場するので注意してください(文脈で区別)。「完備」も距離空間的完備と圏論的完備がありますね、こういう多義性〈オーバーロード〉はどうにもならないので、各自で注意。

ベクトル空間の圏では、直和と直積が一致しますが、今回の目的から、(直和ではなく)直積の記法を採用して、バナッハ空間VとWの直和をV×Wと書きます。V×Wのノルムは、|(v, w)| := max(|v|, |w|) で定義します。そして、バナッハ空間としての1はゼロ空間のことです(Rのことではありません)。

Xをコンパクト・ハウスドルフ空間、Vをバナッハ空間として、C(X, V)を、XからVへの連続写像の空間とします。Vのベクトル空間構造からC(X, V)にもベクトル空間構造が入り、最大値ノルムでC(X, V)にノルムを入れて、C(X, V)∈|Ban| とします。

f:X→Y in CompHous に対する C(f, V):C(Y, V)→C(X, V) はfによる引き戻しで定義して、φ:V→W に対する C(X, φ):C(X, V)→C(X, W) はφによる前送りで定義すると、C(- , -)は CompHousop×BanBan という関手になります。

圏論的完備性/連続性を定義する箙クラスとして離散有限箙からなるクラスを選びます。連続関手は、“始対象と直和”/“終対象と直積”を適切に移す関手となります。

この状況で、C(-, -)が二項指数関手であることは、次の条件が満たされることです。

  1. C(¥emptyset, V) ¥stackrel{¥sim}{=} 1
  2. C(X + Y, V) ¥stackrel{¥sim}{=} C(X, V)×C(Y, V)
  3. C(X, 1) ¥stackrel{¥sim}{=} 1
  4. C(X, V×W) ¥stackrel{¥sim}{=} C(X, V)×C(X, W)
  5. C(1, V) ¥stackrel{¥sim}{=} V
  6. C(Y, C(X, V)) ¥stackrel{¥sim}{=} C(X×Y, V)

これらは、定義と比べるだけで分かるでしょう。

一般化:2次元化と相対化

今まで述べた内容は、過去にも(断片的であれ)触れたことがあります。最近思っていることは「これじゃ足りないな」ということです。構文論・意味論を包括的に扱うには、指数関手に対して次のような一般化をする必要があります。

  1. 2次元化
  2. 相対化

前節の例で、E:Quivop×CatCat という二項指数関手が出てきました。Catは1次元の圏ではなくて2次元の圏(厳密2-圏)です。しかし、Catの2次元構造はあまり使っていません。指数関手の定義は、1次元の圏論のなかで済ませています。

二項指数関手 E:Xop×AA において、XAのどちらか、あるいは両方が2-圏のときを考える必要があります。2次元構造を考慮した指数関手の定義が欲しいのです。出来ることなら、n次元の指数関手の定義が望みですが、それは難し過ぎますね。

次に相対化ですが、これは指数関手が値を取る圏を一般化したい、ということです。E:Xop×AA ではなくて、E:Xop×AB という形を許したいのです。ここで、ABは同じでなくてもかまいません。

指数関手の条件を見ると、A = B であることが前提になっているものがあるので、まったく無関係のABを許すのは無理です。J:AB という決まった関手があり、関連する関手はJに沿った左カン拡張が可能だとします。必要なら、Jに沿った左カン拡張を行って、指数関手の条件に意味を持たせることができます。

この文脈での相対化は、モナドから相対モナド〈relative monad〉を定義したときと同様です。もともとが同一の圏を前提としていた定義を、異なる圏でもいいように一般化します。ただし、繋ぎの道具としてカン拡張の存在は仮定します。

2次元化と相対化の両方を行うと、指数関手は相対2-指数関手と呼ぶべきものになります。あるいは、モノイド2-圏による連続作用を持つ2-加群とも言えます。そのような構造を完全に理解するのは大変そうですが、部分的な定義や理解でも、構文論・意味論の記述に役に立つだろうと期待してます。

*1:ペキ集合関手〈powerset functor〉と呼ぶ人が多いとは思いますが。

*2:記事: https://keydifferences.com/difference-between-exponent-and-power.html
画像: https://keydifferences.com/wp-content/uploads/2017/02/exponent-vs-power.jpg

2018-04-11 (水)

圏のサイズとサイズによる“圏の圏”の分類

| 13:35 | 圏のサイズとサイズによる“圏の圏”の分類を含むブックマーク

先週の話題を引っぱって、圏のサイズ問題なんですが、圏のサイズを何種類か定義して、それに伴って現れる“圏の圏”に名前を付けておきます。

Uがグロタンディーク宇宙である条件に、ω∈U を含めます。ωは自然数の集合Nと同じです。ωは加算無限基数の意味ですが、Nと思ってかまいません。

ロー〈Zhen Lin Low〉に従って、ω∈U を外した場合はプレ宇宙〈pre-universe〉と呼びます(「グロタンディーク宇宙って何なんだ?」参照)。

あなたはこの公理を信じますか」で引用したレヴィ〈Paul Blain Levy〉の論文 "Formulating Categorical Concepts using Classes" に(だいたい)従って、圏のサイズを分類します。

Uを単一宇宙公理として、ZFC+UはZFCの公理系に単一宇宙公理Uを加えたものです。

  • [U 単一宇宙公理] グロタンディーク宇宙Uが存在する。

VをZFC+Uのモデルとして、単一宇宙公理で存在が保証されたグロタンディーク宇宙Uを固定して考えます。UはZFC(ZFC+Uではない)のモデルになっています。

Cの対象の集合|C|と、a, b∈|C| ごとのホムセットC(a, b)達のサイズに条件を付けて、圏を分類します。“圏のサイズ”とは、単独のサイズではなくて、対象集合のサイズとホムセット達のサイズの組み合わせで定義します。

Vの集合xがUに関して小さいU-小〈U-small〉)とは、x∈U のことだとします(他の定義もありますが)。また、Vの集合yがUに関してクラス(U-クラス〈U-class〉)であるとは、y⊆U のことだとします(他の定義もありますが)。U-クラスであることも、サイズに関する制約とみなせます。

レヴィによる、サイズに基づく圏の分類を表にまとめます。

Cに関する条件→ |C|∈U |C|⊆UC(a, b)∈UC(a, b)⊆U
小〈small〉
局所小〈locally small〉 - -
軽〈light〉 -
穏和〈moderate〉 - -

二重丸'◎'は、定義により成立する条件、丸'○'は定義から導かれる条件です。この定義のまんまで話がスムーズに進むかは定かでないのですが、目安と考えてください。

特定のサイズ条件を満たす圏の全体からなる“圏の圏”は次のように書くことにします。

  1. CatU -- Uに関して小さい圏〈small categories〉の圏
  2. CATU-- Uに関して軽い圏〈light categories〉の圏
  3. ℂATU -- Uに関して穏和な圏〈moderate categories〉の圏
  4. ℂ𝔸𝕋 -- 無条件な圏の圏

ℂ𝔸𝕋は、外側の大宇宙V内で定義される圏の圏で、Vから見れば小さい圏の圏なので、

  • ℂ𝔸𝕋 = CatV

と書けます。上記のように字種・字体を変えて区別*1すれば、小宇宙Uは省略してもかまいません。

  1. Cat = CatU
  2. CAT = CATU
  3. ℂAT = ℂATU

複数の小宇宙〈グロタンディーク宇宙〉を考えているときは、混乱してしまうので単純な省略はできません。


サイズの問題は、(僕が)想像していたより複雑で、ボンヤリ考えているのはやっぱりマズイなと思いました。小さい圏の圏をCatと書くのはよく使われる記法・習慣ですが、大きい圏に関しては、その“大きさ”が分析されてなくて、雰囲気的にCATを使ってしまうこともあるでしょう。少なくとも僕は、あまり考えずに“大きいかも知れない圏の圏”をCATと書いてました。上記のレヴィのCATの意味か、ℂ𝔸𝕋の意味か、あるいは別な小宇宙U'に対するCatU'か、区別してなかったですね。

状況設定をハッキリさせないと、例えば「CATデカルト閉か?」のような問に答えることができず、安易な推論でしくじりそうです。やっぱり、ボンヤリ・雰囲気はダメですね。

*1:白抜きの太字は黒板文字〈blackboard bold〉と呼ばれます。Unicodeの文字番号は、白抜きC(複素数用) U+2102, 白抜きA U+1D538, 白抜きT U+1D54B です。

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

2018-04-09 (月)

ホムセットは交わるのか

| 11:25 | ホムセットは交わるのかを含むブックマーク

Cが圏のとき、A, B, C, D∈|C| として、ホムセットの共通部分

  • C(A, B)∩C(C, D)

はいったいどうなってんでしょう?

内容:

  1. dom/codを使った定義では
  2. 集合圏上の豊饒圏としては
  3. 米田埋め込みへの影響
  4. たいした問題ではない

dom/codを使った定義では

f∈C(A, B)∩C(C, D) とすると:

  • dom(f) = A かつ cod(f) = B
  • dom(f) = C かつ cod(f) = D

なので、

  • dom(f) = A = C
  • cod(f) = B = D

となるので、

  • C(A, B)∩C(C, D) が空でないならば、A = C かつ B = D

です。対偶をとれば:

  • A ≠ C または B ≠ D ならば、C(A, B)∩C(C, D) は空集合

あるいは、

  • (A, B) ≠ (C, D) ならば、C(A, B)∩C(C, D) は空集合

2つのホムセットは、まったく同じか無共分〈disjoint〉かのどちらかです。ホムセットが同じになるのは、両端が同じときに限ります。

集合圏上の豊饒圏としては

通常の圏は、集合圏Set上の豊饒圏〈enriched category over Set*1と同じだと言われています。ほんとに同じなら、前節で述べた次の事実は、Set上の豊饒圏でも成立するはずです。

  • (A, B) ≠ (C, D) ならば、C(A, B)∩C(C, D) は空集合

しかし、豊饒圏の定義からは、「両端が一致しない限りホムセットが交わらない」は出てこないようです。豊饒圏の定義は次で述べています。

nLab項目なら:

「両端が一致しなくてもホムセットが交わる」例を作ってみましょう。豊饒化圏〈enriching (base) category〉Setのモノイド積は直積×、モノイド単位は 1 = {0} とします。

これから作る豊饒圏をCとして、|C| = A = {1, 2} とします。豊饒圏を定義するホム写像は:

  • C(-, -):A×A→|Set|

A×A = {1, 2}×{1, 2} = {(1, 1), (1, 2), (2, 1), (2, 2)} ですから、C(-, -) は次のように具体的に与えます。

  1. C(1, 1) = {0} = 1
  2. C(1, 2) = {0} = 1
  3. C(2, 1) = {} = ¥emptyset
  4. C(2, 2) = {0} = 1

結合を与える写像 γa,b,c:C(a, b)×C(b, c)→C(a, c) in Set は、次のどちらかにします。

恒等を与える写像 ιa:1C(a, a) in Set は、{0}→{0} の恒等写像とします。

以上の状況で、結合律と左右の単位律は自明に成立するので、集合圏Set上の豊饒圏になってます。両端が異なるホムセットC(1, 1)とC(1, 2)が交わっています。はい、「両端が一致しなくてもホムセットが交わる」例です。

異なる結果が出るので、通常の圏の定義とSet上の豊饒圏の定義は完全に同じじゃないですね。

米田埋め込みへの影響

ホムセットの交わり(共通部分)C(A, B)∩C(C, D) を気にすることはほとんどないと思います。僕も気にしたことありません。無意識に交わらないことを前提にしている気がしますが、交わって困ることもすぐには思いつきません。何かないかな? -- 米田埋め込みが埋め込みじゃなくなるかな。

米田埋め込みが充満忠実関手〈full-and-faithful functor〉であることは、米田の補題からすぐに出ます。つまり、ホムセットごとに集合の同型(全単射)を与えます。米田埋め込みの対象部〈object part〉についてはどうでしょう。

対象部が単射であることは、

  • a, b∈|C| に対して、a = b ならば a = b

と書けます。ここで、上付きのコメは「困った時の米田頼み、ご利益ツールズ」で導入した「米田の星」記法です。これを示すには、

  • ∀x∈|C|.(C(x, a) = C(x, b)) ならば、a = b

が言えれば十分です(関手の等しさの定義から)。対偶をとると:

  • a ≠ b ならば、∃x∈|C|.(C(x, a) ≠ C(x, b))

「両端が一致しない限りホムセットが交わらない」という前提があれば、x = a と置けば、C(a, a) ≠ C(a, b) が得られて、米田埋め込みの対象部が単射であることが分かります。

しかし、「両端が一致しなくてもホムセットが交わる」場合は、米田埋め込みの対象部が単射とは限らず、「埋め込み」と呼ぶのが憚〈はばか〉られる気がします。

たいした問題ではない

CSet上の豊饒圏として定義されている圏だとします。|C| = A として、C(-, -):A×A→|Set| は、ホムセットが交わる状況を作り出しているかも知れません。

新しい圏C'を次のように定義します。

  • C'(a, b) := {(a, f, b) | f∈C(a, b)}

新しいホムセットでは、射の両端がラベルとして付加されているので、両端が異なればこのラベルが異なります。(a, f, b)と(c, g, d)が等しいためには、f = g だけではなく、a = c かつ b = d も要求されるので、ホムセットの交わりはなくなります。

上記のような手順を経由すれば、ホムセットは交わらないと仮定しても問題はありません。

では、豊饒圏の定義のなかに、「ホムセットは交わらない」を入れ込むことは出来るでしょうか。これは無理です。豊饒化圏が集合圏のときは「交わり」概念がありますが、一般のモノイド圏では「ホム対象が交わる」ことを定義できません。したがって、「ホム対象が交わらない」という条件を記述する術〈すべ〉がありません。

豊饒化モノイド圏Vの対象に交わり概念はないにしろ、等しい/等しくないは判断できます。次の条件はどうでしょうか。

  • C(a, b) = C(c, d) in V ならば、(a, b) = (c, d)

この条件は強すぎます。例えば、一般化された距離空間は豊饒圏の例です。次の記事で述べています。

一般化された距離空間におけるホム対象は実数値です。C(a, b)の代わりにdist(a, b)と書いて距離らしくすると:

  • dist(a, b) = dist(c, d) in R≧0 ならば、(a, b) = (c, d)

これは、「距離が等しい点の対は、(対として)等しい」ことを要求しています。距離空間の概念からは、まったく受け入れられない条件です。

まとめれば、次のようなことでしょう。

  • 圏の一般化としての豊饒圏では、ホム対象の交わりや等しさに対して特に条件は付けない。そもそも条件が書けなかったり、条件がキツすぎることがあるので。
  • 集合圏上の豊饒圏では、ホムセットが交わらないほうが都合がいいことがある。そのときは、少しの変更で望みがかなう。深刻な問題ではない。

*1:enriched category in Set とも言います。このときは、集合圏内の豊饒圏ですね。

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

2018-04-06 (金)

あなたはこの公理を信じますか

| 14:26 | あなたはこの公理を信じますかを含むブックマーク

信じる者は救われる or 巣食われる

公理というのは、明らかに矛盾があれば別だけど、そうじゃないなら、採用するかしないかの判断基準て特にないんだよね。その公理を信じる人/メリットを感じる人が採用するだけ。

正しさを担保しようにも、論理的にはそれ以上は遡れない*1ので、「正しそう」という状況証拠を積み上げるとか、役に立った事例を並べるとか、コレがないと不便だぞと訴えるとか、そういう行為でしか公理の正当化、いやプロモーション活動はできません。

で、ここ何日かダラダラと話題にしている宇宙公理〈the universe axiom〉だけど、これを受け入れるかどうかも、感覚・感性・感情・心情でしか判断できない。あるいは、信仰〈faith〉の問題、とも言えます。

もう一度宇宙公理を述べますが、二種類に分けましょう。「ZFCの宇宙(ときに大宇宙と呼びます)のなかに、グロタンディーク宇宙(ときに小宇宙と呼びます)が少なくとも1つは存在する」という内容の命題をU(Univereseの'U')とします。「いくらでも好きなだけグロタンディーク宇宙を取れる」という内容の命題のほうはMU(Multiple-Universe = Multiverse から)としましょう。

  • [U 単一宇宙公理] ZFCの宇宙Vのなかにグロタンディーク宇宙Uが存在する。
  • [MU 多宇宙公理] ZFCの宇宙Vの任意の集合x(x∈V)に対して、x∈U となるグロタンディーク宇宙Uが存在する。

到達不能基数(非可算な強到達不能基数)の存在を主張する公理をIとすると、ZFC+UとZFC+Iが同値なことは知られています。同様に、ZFC+MUも基数の言葉で書けますが、基数に興味があるわけじゃないので、宇宙公理は大宇宙と小宇宙に関する命題と捉えます。

宇宙公理(UにしろMUにしろ)を積極的に支持する気になれない/なれなかったのは、「あれば便利だ」以外に、「そうであるべき」理由が見つからないからです。でも、ここ二,三日で心境が変化して、「あれば便利だ」だけでも十分な理由のような気がしてきました。宇宙公理を回避したり代替案を探すのに労力をかける意義も見当たらないし、だったら受け入れて楽になればいいじゃん、と。

ここは楽園か

ここから先のVは、ZFC+UまたはZFC+MUの宇宙とします。つまり、V内にグロタンディーク宇宙Uを取れます。通常の構成や議論はUのなかで行います。必要があれば、Uの外に出て、Uを外からいじってもかまいません。

Uの部分集合は、Uの観点からはクラスです -- U-クラスと呼びましょう。U-クラスが真クラス〈大きい集合〉のときもあるでしょう。しかし、Vから見ればU-真クラスだろうが何だろうが単なる集合(小さい集合)で、U-クラスの全体Pow(U)もまた単なる集合です。U-クラスを集めたモノの全体Pow(Pow(U))だって単なる集合です。

Uに関するメタ理論が、Vの普通の集合論で行なえます。構文的/論理的な道具は何も追加しないで、U-クラスの理論が作れます。ほぼタダで、メタ理論/クラス理論が手に入るのです。

何も気にすることなく、VのなかでUを操作できます。ZFC+MUを仮定するなら、なにか困ったことが起きてもUより上位の宇宙U'に移れば収拾できるでしょう。

まー、素敵。

楽園なんてない

今年(2018年)に出たレヴィ〈Paul Blain Levy〉(Call-By-Push-Valueの人です)の論文には、僕のような安直な改宗者を愕然とさせることが書いてあります。

とにかくうまくいかない!

  • タプルがうまく作れない。タプルを集めた直積も作れない。
  • 同値関係による商がうまく作れない。
  • 圏の圏がデカルト閉にならない。
  • 米田の補題がうまく定式化できない。
  • そのくせ、比較的簡単に病的例を作れる。

もう散々ですよ。

レヴィは、ZFC+Uだけを前提としてます。ZFC+MUまで使えば解決できる問題もありますが、ZFC+MUには次の難点があります。

  • 複数の小宇宙を使うので、今どの小宇宙で議論しているかを常に意識しなくてはならない。めんどくさい。
  • ある小宇宙での議論が、そのまま他の小宇宙でも通用するとは限らない。めんどくさい。
  • 素のZFC上の理論と、複数小宇宙を使った理論との対応関係が複雑化する。めんどくさい。

単一の小宇宙だけなら、SetU, CatU のような小宇宙パラメータ(下付き添字にしている)を省略できます。Uの部分集合を「クラス」と呼び、真クラスも含めたクラス概念で諸々のことをやろう -- それがレヴィの方針です。

この「至極ごもっとも」な方針で、素朴に作業すると上記のような困難に出会うのです。レヴィは、様々な工夫とk-クラスという概念により、トラブルを乗り切って比較的にきれいな定式化を得てますが、「はーっ、楽園じゃなかったわ」とため息が出ます。


サイズ問題へのアプローチは、宇宙公理だけではないので、他の方法を調べる/試すことは意味があるでしょう。しかし、「楽ちんで全てがうまくいく」という方法は期待できないかも知れませんね。これは、そうそうウマい話は転がってないよ、というだけのことで、悲観的になる事じゃないとは思いますが。

*1:既に知られた体系との同値を示すとか、埋め込みを構成して正当性を主張することはできますが、これは信頼できる前例がある場合に限られます。