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

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

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

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

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

2018-04-05 (木)

グロタンディーク宇宙って何なんだ?

| 10:05 | グロタンディーク宇宙って何なんだ?を含むブックマーク

グロタンディーク宇宙について、どうも僕は曲解していたような気がします。-- 本日も雑感垂れ流し日記。

昨日の「入れ子の宇宙を可能とする公理」で、宇宙公理〈the universe axiom〉を認めてしまえば、グロタンディーク宇宙の無限系列 U0, U1, U2, ... が作れて、「階層的な圏論的宇宙・楽観的暫定版」で述べた願望は、いとも簡単に実現されると書きました。

僕の今までの感覚・感情は、宇宙公理のような強烈でご都合主義的な仮定は出来るなら使いたくない、使うべきではない、というものでした。それを使ってしまえば願望は叶うけど、使うのを躊躇して代替案を期待するような態度でした。しかし、"Universes for category theory"の著者ロー〈Zhen Lin Low〉は、アッサリと当たり前のごとくに宇宙公理を使っています。

昨日の記事を書いた後にザッと調べた感じでは、集合論の方面から宇宙公理に反対している人は見かけません(ザッと見の範囲だからあまり当てにならないが)。グロタンディークは、代数幾何を展開する際にグロタンディーク宇宙を使ってますが、その意味で直接のユーザーと言える代数幾何界隈だと、結果的にZFCを強化してしまうグロタンディーク宇宙を快く思ってない人が少しはいるようです。

圏のサイズ問題に対して、グロタンディーク宇宙以外にも、集合論の枠内で、あるいは集合論以外からの色々なアプローチがあるようです。決定版はないし、一長一短があるでしょうが、サイズ問題解決の道具は幾つもあるので、実用上はあまり困ってない雰囲気。


グロタンディーク宇宙に対する僕の印象を述べます。

ZFC集合論の宇宙(なんらかのモデル)をVとします。集合圏Setを、|Set| = V となるように定義してしまうと、Setをもとに圏論的な構成をしたとき、例えば自己関手圏[Set, Set]を作ったとき、[Set, Set]を置くべき場所が分からんなー、とは思います。

Vよりは小さい宇宙Uがあって、|Set| = U となるように集合圏を定義すれば、色々な圏論的構成をしても、それらの構成物を置くべき場所を大きな宇宙V内に見出すことが出来るだろう、そのためにUを考える -- と僕は考えていました。この考えは、まー間違いではないでしょう。しかし、Uに対してハッキリしたイメージ/実在感が持てないので、Uを必要悪/トリックの道具のように捉えていたのです。

ここで、グロタンディーク宇宙の定義をハッキリと述べましょう。ZFCの宇宙VのサブクラスUがグロタンディーク宇宙だとは:

  1. x∈U, y∈x ならば、 y∈U (∈に関する推移性)
  2. x, y∈U ならば、{x, y}∈U (対の構成に関して閉じている)
  3. x∈U ならば、Pow(x)∈U (ベキ集合に関して閉じている)
  4. I∈U, f:I→U ならば、∪(f)∈U (族の合併に関して閉じている)
  5. UVVの要素)
  6. ω∈U (無限集合を持つ)

∪(f)は、 ¥bigcup_{i ¥in I}f(i)の略記です。ωは自然数全体の集合です。

5番目の条件 UV を外せば、V自体がグロタンディーク宇宙になります。しかし、グロタンディーク宇宙は“大き過ぎない”のがミソなので、小ささ〈smallness〉の条件として UV があります。ロー〈Zhen Lin Low〉は、最後の ω∈U を外したモノをプレ宇宙〈pre-universe〉と呼んでいます。空類(空集合)はプレ宇宙になります(虚しい例だけど)。有限集合しか含まないプレ宇宙も作れます。

さて、僕が感覚的・感情的に、あるいは無根拠に違和感を持っていたのは、

  • UV

コレです。グロタンディーク宇宙Uは、外の宇宙からみれば単なる集合です。このことは次のどちらかを意味するでしょう。

  • 圏論に必要な宇宙は、たいして大きくない。
  • 外の宇宙はもの凄く大きい。

直感的な「大きい/大きくない」はまさに感覚的・感情的なんですが、圏論が展開できる宇宙はそれなりに“大きい”気がするので、それを含む外の宇宙Vはもの凄く大きいことになります。このVの大きさが僕のイマジネーションが届かないところで、気味が悪い/怖い/使いたくない感じにつながってるのでしょう。


グロタンディーク宇宙Uを持つような外の宇宙Vはもの凄く大きい、という感覚は、まったくの的外れではありません。ZFC集合論に何らかの公理を加えた集合論をZFC+αと書くことにすると、次の2つは同値です。

  • ZFC+αのモデルVがグロタンディーク宇宙Uを持つ。
  • ZFC+αでは、到達不能基数の存在が示せる。

このことは、1970年前後に既に知られていたようです。

ZFC+αの枠内で考えるなら、グロタンディーク宇宙を認めるかどうかは、到達不能基数を認めるかどうかと同じことです。そしておそらく(僕が感じる雰囲気としては)、「到達不能基数なんてなーんちゃない、全然OKでしょ」らしい。僕が「もの凄く大きい」と感じる拡がりも、専門家にはどうってことない大きさみたい。到達不能基数(のたぐい)は、巨大基数のなかでは下っ端のほうなので、たいして議論にならないのでしょう(たぶん)。

以上は集合論側の話ですが、複数のグロタンディーク宇宙に渡る圏論では、Uに対するSetUCatUに対して何かを証明したとき、別なグロタンディーク宇宙Wに対して同じ定理が成立する保証はないので、やっぱり簡単じゃないです。ある定理が圏論の宇宙(グロタンディーク宇宙)に依存しないことを主張するなら、

  • U∈Universe.( … )

という形になり、この全称束縛はいったい何なんだよ? と*1

*1[追記]「グロタンディーク宇宙は小さい」という事実から、この全称束縛は特に問題ないですね。「宇宙」という言葉から、外に出られない印象を持ってしまうのですが、外からいくらでもイジれるのがグロタンディーク宇宙の特徴。でも、なんか慣れないわ―。[/追記]

2018-04-04 (水)

入れ子の宇宙を可能とする公理

| 12:17 | 入れ子の宇宙を可能とする公理を含むブックマーク

昨日「階層的な圏論的宇宙・楽観的暫定版」において、グロタンディーク宇宙の無限系列 U0, U1, U2, ... があったらいいな、という話を書きました。

圏論の宇宙に関する資料はなかなか見つからないのですが、ロー〈Zhen Lin Low〉の次の論文があります。

集合論圏論の関係を論じるときは、到達可能圏〈accessible category〉局所表現可能圏〈locally presentable category〉などの知識が必要になります。ここら辺を僕は避けてきたので、ローの論文は全然読めません。

技術的議論は置いといて(分かんないので)、ロー論文冒頭に出てくる宇宙公理〈universe axiom〉の意味を考えてみます。単に宇宙公理というより、その内容からは、多宇宙公理〈multiverse axiom〉とか入れ子宇宙公理〈nested universes axiom〉と呼ぶのがふさわしいでしょう。

入れ子宇宙を可能とするには、2種の(公理的)集合論が必要です。ひとつは、外の宇宙、あるいは大宇宙を規定する集合論です。これはベース集合論〈base set theory〉と呼びましょう。もうひとつは、圏論のための小宇宙を規定する圏の集合論〈set theory for categories〉です。

ベース集合論としては、ZFC〈Zermelo–Fraenkel + Choice〉集合論が圧倒的によく使われますが、他にも集合論はあります。

マックレーン集合論に関する短い解説は見当たりませんが、長い(128ページ)論文なら、"The strength of Mac Lane set theory"があります。

圏の集合論は、一人前の集合論というよりは、ベース集合論の宇宙(大宇宙)のなかで、圏論を展開するためのクラスを定義する公理系のことです。通常、この目的にはグロタンディーク宇宙の公理系が使われますが、必要に応じて他のバリアントがあってもいいでしょう。

さて、ベース集合論の宇宙をVとして、VのサブクラスUで圏の集合論の公理を満たすものを圏論の宇宙〈universe for category theory〉、または小宇宙〈small universe〉と呼びましょう。この状況で、宇宙公理多宇宙公理入れ子宇宙公理)とは次のものです。

  • Vの任意の集合x(x∈V)に対して、x∈Uであって、UV である小宇宙Uが存在する。

これは非常に強い公理に思えます。Uが十分に強いなら何でも出来ちゃいそう。

例えば、xとして自然数の集合Nを取ると、Nを要素とする小宇宙U0が取れます。宇宙公理からU0Vの集合なので、U0U1 である小宇宙U1が取れます。この過程を続ければ、小宇宙の無限系列が作れて、「階層的な圏論的宇宙・楽観的暫定版」の願望はアッサリとかなえられることになります。

宇宙公理が他の公理と矛盾しないのか、あるいは、宇宙公理は他の公理から導けるのか(実は定理なのか)あたりが問題になります。もちろんこれは、ベース集合論と圏の集合論の取り方に依存します。

仮に、ベース集合論が宇宙公理を満たすとしても、小宇宙の拡張/取り替えなどで圏論側の問題が出てくるから、そう簡単じゃないよ、てのがロー論文の主張のようです。技術的困難や注意事項が色々とありそうですが、しかしそれでも、「階層的な圏論的宇宙・楽観的暫定版」で述べたような楽観主義を否定する根拠はないように思えます。いずれは、入れ子の宇宙を定義して安全に取り扱う処方箋が確立されるんじゃないのかな(と、これも楽観主義)。

2018-04-03 (火)

階層的な圏論的宇宙・楽観的暫定版

| 11:33 | 階層的な圏論的宇宙・楽観的暫定版を含むブックマーク

1つまたは少数の圏を扱う場合でも、圏論的宇宙全体の構造を知っていたほうがいい場合があります。とはいえ、圏論的宇宙全体は難しいですね。とりあえずは、次の基本的な観測を合理化することを考えます。

  • j次元の圏の全体は、(j + 1)次元の圏とみなせる。


高次圏: 複雑さの3つ目の方向と相対階数」で次のように書きました。

圏論的宇宙は、次のような所属関係の系列であるのが望ましいと思われます。

  • 0-Cat0 1-Cat0 2-Cat0 ...

しかし、普通の定義ではこのような系列を作ることは出来ません。解決のための正攻法があるのか、トリックを使うのか? それとも、そもそもこういう問題設定が間違いなのか? どうすべきかは分かりませんが、相対階数が増える方向が事態を困難にする方向であるのは確かです。

上記の「所属関係の系列」を作るために、グロタンディーク宇宙の無限系列 U0, U1, U2, ... を考えます。この系列では次が成立しているとします。

  • UrUr+1 (r = 0, 1, 2, ...)

こんな無限系列が実際に作れるとか、存在証明が出来るとか主張しているのではなくて、単に要求仕様とか願望を述べているだけです、残念ながら。

A⊆Ur のとき、Aはr階のクラス〈class〉と呼び、a∈Ur のとき、aはr階の小集合〈small set〉と呼びましょう。r階の小集合ではないr階のクラスは、r階の真クラス〈proper class〉とか大集合〈large set〉と呼びます。ここで出てきた階数は、「高次圏: 複雑さの3つ目の方向と相対階数」の相対階数ではなくて、絶対的な階数です。

「a⊆Ur ならば a∈Ur」は言えませんが、次は言えます。

  • a∈Ur ならば a⊆Ur
  • A⊆Ur ならば A∈Ur+1

大きな階数の宇宙に移行すれば、大集合〈真クラス〉を小集合とみなせます。また、階数が上がっても小集合はそのまま小集合として使い続けることができます。なんか、激しくご都合主義的な気がするのですが、こうだったら確かに嬉しい

Urの意味での“小さいj-圏”からなる(j + 1)-圏をj-Cat#rとします。右下付きの#rが考えている宇宙の番号です。rを固定して、jのほうを動かすことができます。この場合は、Urの意味の“小さいj-圏”しか考えないので、サイズの問題は起きません。しかし、j-Cat#r∈|(j+1)-Cat#r| とはなりません。

階数rを動かすことにより、次が言えます。

  • j-Cat#r∈|(j+1)-Cat#r+1| … j次元の圏の全体は、(j + 1)次元の圏とみなせる

これより、次の所属関係の系列が得られます。

  • 0-Cat#00 1-Cat#10 2-Cat#2 ...

この系列だけではなくて:

  • 1-Cat#00 2-Cat#10 3-Cat#2 ...
  • 2-Cat#00 3-Cat#10 4-Cat#2 ...

などなど。次元jと階数rは好きなタイミングで上げればいいのです。


Urはグロタンディーク宇宙としましたが、もっと弱い宇宙でもよいならば、U0U1 ∈ ... は実際に作れるでしょう。しかし、あまりにも弱い宇宙だと、j-Catや関連する構造を作れない懸念があります。2つの宇宙 UV とレイフィケーションで無限系列をシミュレートする手があるかも知れません。

いずれにしても僕には、適切な強さを持つ宇宙の系列を実際に作ってみせる技量はないので、楽観的に「たぶん大丈夫」と考えて、ご都合主義的マルチバースを想定することにします。けっこう多くの人がこういうパラダイスを期待している、あるいは(潜在的には)使っているんじゃないかと思います。

“宇宙”関係:

  1. 集合の宇宙論
  2. ファンタジー: (-1)次元の圏と論理
  3. 圏論的宇宙と反転原理と次元付きの記法
  4. 有界な圏論的宇宙と圏論的パス式
  5. 圏論的宇宙の対象化原理

2018-03-29 (木)

なにゆえにカン拡張なのか

| 13:34 | なにゆえにカン拡張なのかを含むブックマーク

カン拡張のために、柱の絵を描く」にて:

特にシリーズ記事とかにしませんが、関連する幾つかの記事達が、全体としてカン拡張の説明になればいいな、というゆるい計画はあります。

というわけですが、カン拡張を知ったら何かいいことがあるんでしょうか?

内容:

  1. 圏論内部からの動機
  2. 関手データモデルとデータ移行関手
  3. 型クラスとモデル
  4. 相対モナド
  5. プログラム最適化
  6. おわりに

圏論内部からの動機

カン拡張というと、マックレーンの有名な言葉:

  • All Concepts are Kan Extensions

があります。圏論に出現するすべての概念はカン拡張で説明できる、ということです。ちょっと大げさな気がしなくもないですが、標準的・典型的な圏論の概念がカン拡張に包摂されるのは事実です。

極限/余極限は、圏論の重要な道具ですが、それぞれ右カン拡張/左カン拡張の特別な場合になります。つまり、「極限はカン拡張」(Limits are Kan extensions)です。

随伴〈adjoint | adjunction〉は圏論の中心的な概念ですが、随伴系 (η, ε): F -| G :DC (この書き方は「随伴系の書き方」参照)はカン拡張で説明できます。「随伴はカン拡張」(Adjunctions are Kan Extensions)です。

普遍性〈universal property〉とか普遍的構成〈univesal construction〉は圏論の指導原理です(僕は余り好きじゃないけど*1)。これらは、極限や随伴に帰着できるので、結局はカン拡張で説明できます。

カン拡張までたどり着けば、(標準的学習コースで)それ以前に習った概念はカン拡張に吸収されることになります。カン拡張は、圏論における統合フレームワーク〈unifying framework〉として機能します。

以上の話は、圏論内におけるカン拡張の意義と位置付けであり、道具として圏論を使いたい下心ケンロニスト*2にはあんまりアピールしないかも、と思います。

関手データモデルとデータ移行関手

僕にとって、強く印象に残ったカン拡張の応用はスピヴァックの関手データモデルです。

文字通り衝撃的でした。このことは「データベースとカン拡張と思い出 // データベースとカン拡張」に書いてあり、そちらと重複もありますが、少し補足します。

スピヴァック理論は、現在では、プログラミング言語型理論とデータベースの統合を目指した代数データベース理論へと発展しています。

  • Title: Algebraic Databases
  • Authors: Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, Ryan Wisnesky
  • Pages: 80p
  • URL: https://arxiv.org/abs/1602.03501

代数データベース理論は、高度化・複雑化して当初のシンプルさはなくなっています。当初の関手データモデルで、何が驚いたかって、そのシンプルさです。データベース用に新しい概念を作ることは一切せずに、既存の圏論的概念だけで鮮やかな再解釈を提示したのです。

なかでも注目すべきは、データ移行関手〈data migration functor〉*3です。φ:S→T がデータベーススキーマのあいだの射のとき、S上のデータとT上のデータを変換する3種のデータ移行関手が自動的に構成できます

  • データ引き戻し関手 Δφ:Data(T)→Data(S)
  • データ前送り関手(右) Πφ:Data(S)→Data(T)
  • データ前送り関手(左) Σφ:Data(S)→Data(T)

Data(S)は、データベーススキーマS上のデータ状態(データインスタンスとも呼ぶ)とデータ状態遷移からなる圏です(Data(T)も同様)。

データベーススキーマを変更したとき、新しいスキーマ上に既存データを移し替える必要があります。このとき、データ(情報)の欠損や重複が生じるのは避けられないかも知れません。そうだとしても、“最良のデータ移行”をしたいのは当然の要求でしょう。さて、“最良のデータ移行”ってなに?

僕が知る限り、スピヴァック以前に“最良のデータ移行”の定義(経験や雰囲気ではなくて、明確な“良さ”の基準)はなかった気がします。スピヴァックはここでも、圏論の標準的な概念だけを使って“最良のデータ移行”を定義しています。

  • 引き戻し関手〈pullback functor〉Δφは、φの前結合で誘導される関手
  • 右前送り関手〈right pushforward functor〉Πφは、Δφの右随伴=φに沿った右カン拡張
  • 左前送り関手〈left pushforward functor〉Σφは、Δφの左随伴=φに沿った左カン拡張

Δφは特殊なケースとしてテーブルの射影(カラムの制限)を含み、Πφは特殊なケースとしてテーブルのジョインを含み、Σφは特殊なケースとしてテーブルのユニオンを含みます。別な言い方をすると、よく知られたデータ操作の(極端な)一般化としてデータ移行関手が定義されています。

この定式化/ストーリーはなかなかにシビレルものがあり、これを理解するためだけでもカン拡張を学ぶ価値があると思います。

型クラスとモデル

型クラスは、関手データモデルと類似の枠組みで扱えます。おおよその対応は:

データベース 型クラス関連
データベーススキーマ 型クラス
データベース状態 実装(モデル)
データベース状態遷移 実装のあいだの模倣
データ移行 実装の構成

ただし、「まともな型クラス への入門: 関数型とオブジェクト指向の垣根を越えて // 壮絶な車輪の再発明と混乱を極める用語法」で述べたように、多義語・同義語・類語が多すぎて、用語法を整理・再定義しないと誤解なしに語ることは難しいです。例えば、「実装」と言っても構文的な概念(プログラムコード)と意味論的な概念(実行系)があり、それらを区別しないとわけわからん話になります。

ちなみに、「型クラス」と同義・類義と思われる言葉は:

  • 指標〈signature〉
  • 仕様〈specification〉
  • (形式)セオリー〈(formal) theory〉
  • インターフェイス〈interface〉
  • プレゼンテーション〈presentation | 表示 | 表現〉
  • (構文)生成系〈(syntactic) {generators | generating set | system of generators (and relations)}〉
  • コンピュータッド〈computad〉
  • ポリグラフ〈polygraph〉
  • などなど…

とりあえず、「型クラス」を理論的に取り扱った概念を「指標」と呼ぶことにすると、指標のあいだの射〈signature morphism〉φ:S→T があると、モデル圏のあいだの関手 Δφ:Model(T)→Model(S) が定義できます。Model(-)は、指標に対するモデル(意味論的な実装)からなる圏です。同じ記号を使っていることから分かるように、Δφはデータ引き戻し関手に相当する“モデル引き戻し関手”です*4

さて、問題はモデル引き戻し関手Δφの右随伴(=右カン拡張)/左随伴(=左カン拡張)が存在するか? です。もし存在するなら、カン拡張が“最良の実現”を与えることから、最良のモデル構成法が得られます。

プログラムの場合、データベースのスキーマ変更に対応するのは、インターフェイス(指標/仕様)変更です。インターフェイス変更に伴う最良の実装はカン拡張で実現できます。ただし、データベース(関手データモデル)の場合ほど状況が単純ではないので、強力な結果は期待できないかも知れません。また、右カン拡張と左カン拡張の二種類の“最良”があり、これらの現実的な意味や使い分けがいまひとつハッキリしません。

夢のようにオイシイ話ではありませんが、データだけでなくプログラムに対しても、“仕様変更に伴う最良の移行”をカン拡張を基準に考えることができるでしょう。

相対モナド

相対モナド〈relative monad〉は、アルテンキルヒ達により提案されたモナドの一般化です。

(↑)これは2010年前後に出たものです。arXivに、40ページに増やした2014年版があります。

「普通のモナドじゃどうも痒いわー」と思っていた2011年頃、相対モナドはイケるんじゃないか、と思いました。次の記事で言及しています。

上記論文のタイトルのとおり、モナドの台関手〈underlying functor〉を F:CC から F:CD としてモナド概念を一般化しています。相対モナドの定義は、クライスリ拡張オペレータを使ってなされます。“とあるモノイド圏内のモノイド”という定義が難しいからです。

ところが、関手圏 [C, D] = DC に特殊なモノイド積を入れると、結局は“モノイド圏[C, D]内のモノイド”として相対モナドを再定義できます。このとき、“特殊なモノイド積”の構成に左カン拡張が使われます。

2010年頃に登場した相対モナドは、僕が期待したほどには注目・評価されませんでした。が、実用的な応用もポチポチと出ていて、モナドの変種〈バリアント〉として定着しそうです。例えば、次のスライド/動画(どちらも"Using Relative Monads for Cheap Syntax"という話題)があります。

相対モナドの別な話題: 「米田埋め込み、米田拡張、そして米田モナド」において、米田埋め込みを単位とするモナドについて(曖昧に)述べていますが、これは普通のモナドとして定義できません。大規模な相対モナドになるはずです。その定義には、米田埋め込みに沿ったカン拡張=米田拡張が使われるでしょう。

相対モナドのまた別な話題: ホモトピー型理論のヴォエヴォドスキーは、相対モナドに注目していたようです。残念ながら、2017年9月30日に彼は亡くなりましたが、2016年に相対モナドの論文を書いています。

ヴォエヴォドスキーは、依存型の理論を作り直そうとしていたらしく(未完のプロジェクト)、その基本的道具のひとつに相対モナドがあったようです。

プログラム最適化

この論文については、「独身男性にもコウノトリはモナドを運んでくるのか」に次のようなメモがあります。

このラルフ・ヒンズの論文は、CPS(continuation passing style)変換によるプログラム最適化の背後にある現象をカン拡張で説明しようとするものです。このなかで、余密度モナド(codensity monad)ってのが出てくるのですが、これがなんだか面白い

余密度モナドを絵に描こうとしていたのがコレ(「なんかのお絵描き」より)。

絵を描いているうちに、右カン拡張がラムダ計算類似の絵算で取り扱えそうだ、と気付きました。

ところで、ヒンズ論文のサブタイトル"Art and Dan Explain an Old Trick"って、最初サッパリ意味不明でした。どうやら、ArtとDanは人の名前(短縮名)らしく、

  • Art = アーサー・ケイリー〈Arthur Cayley〉
  • Dan = ダニエル・カン〈Daniel Kan〉

群に関するケイリーの表現定理(の発想)とカン拡張が、プログラム最適化技法の背後にある理屈を説明してくれるよ、という意味でしょう。

ケイリーの表現定理って、圏論的文脈に置けば米田埋め込み(米田表現)の特殊ケースなんですよ。登場人物を圏論の巨匠二人にして、

  • Nob and Dan Explain an Old Trick

のほうがいいような気がしますけどね。

  • Nob = 米田信夫〈Nobuo Yoneda〉

おわりに

カン拡張は意外に多くの場面で登場しますね。圏論内部で統合フレームワークとして機能するということは、圏論の外の世界でも、抽象度が高く包括的な記述の道具に使えることが期待できます。

今回出した例は、いずれもデータベース/プログラムに関連していて、そのテの知識がないと理解できないことが残念な点です。特定分野の予備知識を要求しない事例があるといいんですが … 何かあったら教えてください。

*1:とある圏の終対象または始対象の議論なのに、あえて「普遍」とか難しげな言葉を使う理由が分かりません。

*2:「ケンロニスト」はbonotakeさんによる造語

*3:"migration"の訳語は「転送」「移動」「移送」とかもあるでしょう。

*4:インスティチューション理論では、リダクト関手〈reduct functor〉と呼びます。

2018-03-27 (火)

随伴系の書き方

| 12:35 | 随伴系の書き方を含むブックマーク

F:CDとG:DC が随伴関手対で、Fが左随伴、Gが右随伴のとき、僕はこの事を次のように書いています(「圏論の随伴をちゃんと抑えよう // 随伴系の書き方と事例」参照)。

  • F -| G:DC

ターンスタイル記号'-|'を使うのは一般的です。しかし、その後に書く圏と矢印の書き方は色々あります。

  1. CD
  2. DC
  3. C←→D
  4. D←→C

僕と反対方向の記号や用語を使う人はもちろんいます。例えば:

同じセッティングでも、「CからDへの随伴」と呼んでいます。

ところで、「圏論の随伴をちゃんと抑えよう」で、随伴の主役はC, D, F, Gではなくて、単位ηと余単位εだと言いました。η, εも添えた書き方をしている人もいますね。

ただし、逆ターンスタイルにη, εを埋め込んだ記号を使うのは難しいので、代替案としては次のようかな。

  • (η, ε): F -| G :DC

これで、随伴系を構成する構成要素は全部記述しています。主役が明示されている点がいいです。

随伴系がホムセット同型で与えられるときは、

  • Φ: F -| G :DC

これは、次の自然同型(可逆自然変換)があることを意味します。

  • ΦA,X:D(F(A), X)→C(A, G(X))

省略して書くなら、(η, ε)やΦではなくて、むしろC, Dを省略すべきでしょう。

  • (η, ε): F -| G
  • Φ: F -| G