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

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

2018-02-13 (火)

対称モノイド閉圏におけるカリー化の変種

| 13:54 | 対称モノイド閉圏におけるカリー化の変種を含むブックマーク

ずっと気になっていたことなのでメモしておきます、小ネタだけど。

内容:

  1. モノイド閉圏とカリー化
  2. 左指数と右指数
  3. 対称な場合

モノイド閉圏とカリー化

最初に、モノイド閉圏とカリー化の話題を扱った過去記事へのリンクを示します。

絵の描き方については、上記の2つの記事を参照してください。モノイド積や指数の記号法が安定しない事情は次の記事に書いてあります。

さて、(C, ¥otimes, I, α, λ, ρ)をモノイド圏とします。いつもの記号の乱用で、C = (C, ¥otimes, I, α, λ, ρ) とも書きます。

対象 A∈|C| を固定して、対象のあいだの対応: X|→A¥otimesX、射のあいだの対応: f|→idA¥otimesf で決まる関手 CC を、(A¥otimes-)、あるいは単に(A¥otimes)と書きます。(A¥otimes)は、モノイド積の意味での左からの掛け算関手です。関手 (A¥otimes):CC に右随伴関手があるとします。(掛け算の左右と随伴の左右は別な話で関係はありません。)

  • C(A¥otimesX, Y) ¥stackrel{¥sim}{=} C(X, R(Y))

このとき、(A¥otimes)の右随伴関手Rは対象Aから決まるので、R(-) = (A▷-) とします。つまり、

  • R(Y) = (A▷-)(Y) = A▷Y

たまたまうまく選んだAではなくて、Cすべての対象Aに対して(A¥otimes)の右随伴があるとしましょう。

  • A∈|C| ごとに、C(A¥otimesX, Y) ¥stackrel{¥sim}{=} C(X, A▷Y)
  • A∈|C| ごとに、(A¥otimes) -| (A▷)

(A▷-)を単に(A▷)と書いています。Aを固定して Y|→A▷Y は定義より関手ですが、(A, Y)|→A▷Y は二項関手 Cop×CC となります。変数Aに関しては反変となることに注意してください。

今述べたような二項関手 (-▷-):Cop×CC指数関手〈{exponent | exponential | exponentiation} functor〉、または内部ホム〈internal hom〉と呼びます。

最近まで、指数/内部ホムはモノイド積があるから定義できるのだと僕は思っていたのですが、モノイド積がない状況でも指数/内部ホムは定義(公理化)できるようです。そのことは、次のnLabエントリーを参照。

モノイド圏Cが指数関手(内部ホム)を持つとき、Cモノイド閉圏〈monoidal closed category〉と呼び、C = (C, ¥otimes, I, α, λ, ρ, ▷, Λ) と書きます。▷は指数関手です。Λは、(A¥otimes)と(A▷)の随伴においてホムセットの同型を与える写像です。Λは3つのインデックスを持ちます。

  • ΛAX,Y:C(A¥otimesX, Y)→C(X, A▷Y)

ラムダ計算の用語法を使って、Λをカリー化〈currying〉と呼びます。Λは、ホムセットのあいだの写像として可逆なので、(ホムセットごとに)逆写像Λ-1を持ちます。Λ-1反カリー化〈uncurring〉です。

左指数と右指数

前節の定義では、左からの掛け算(A¥otimes)の右随伴を(A▷)と表しました。では、右からの掛け算(¥otimesA)の右随伴はどうでしょう。モノイド積¥otimesが対称でないときは、(A¥otimes)の右随伴があっても(¥otimesA)の右随伴の存在が保証されません。右からの掛け算(¥otimesA)の右随伴(それがあるとして)は、(◁A)とします。

  • A∈|C| ごとに、C(X¥otimesA, B) ¥stackrel{¥sim}{=} C(X, B◁A)
  • A∈|C| ごとに、(¥otimesA) -| (◁A)

前節の(A▷)は左指数〈left exponentiation〉、(◁A)は右指数〈left exponentiation〉と呼びましょう。カリー化でも左右の区別をします。

  • A∈|C| ごとに、lΛAX,Y:C(A¥otimesX, Y)→C(X, A▷Y)
  • A∈|C| ごとに、rΛAX,Y:C(X¥otimesA, Y)→C(X, Y◁A)

lΛが左カリー化〈left currying〉、rΛが右カリー化〈right currying〉です。反カリー化についても同様です。

非対称なモノイド圏では、左指数と左カリー化を持つモノイド閉圏と、右指数と右カリー化を持つモノイド閉圏は区別すべきです。しかし、A¥odotB = B¥otimesA として新しいモノイド積¥odotを定義すると、掛け算の左右がすっかり入れ替わるので、どちらか一方について考えればいいことにはなります。

対称な場合

モノイド閉圏で一番よく使うのはデカルト閉圏でしょう。デカルト閉圏のデカルト・モノイド積は対称です。対称な場合は、左右の区別に神経質になる必要はありません。そのため、指数やカリー化に関する左右をどうするかの自由度が増えて、むしろ混乱するのではないかと思います。このことが、「ずっと気になっていたこと」です。

対称モノイド圏の対称〈symmetry〉をσとします。

  • σA,B:A¥otimesB→B¥otimesA

対称モノイド圏 C = (C, ¥otimes, I, α, λ, ρ, σ) が左指数▷と右指数◁の両方とも最初から持つとします。もちろん、左カリー化/左反カリー化、右カリー化/右反カリー化も持ちます*1

  • A∈|C| ごとに、lΛAX,Y:C(A¥otimesX, Y)→C(X, A▷Y)
  • A∈|C| ごとに、rΛAX,Y:C(X¥otimesA, Y)→C(X, Y◁A)

これ以外にもカリー化の変種が存在します。次のように定義されるものです。

  • rlΛAX,Y(f) := lΛAX,YA,X;f) : C(X¥otimesA, Y)→C(X, A▷Y)
  • lrΛAX,Y(f) := rΛAX,YX,A;f) : C(A¥otimesX, Y)→C(X, Y◁A)

rlΛを絵で描けば次のようになります。

全部並べてみると:

  1. A∈|C| ごとに、lΛAX,Y:C(A¥otimesX, Y)→C(X, A▷Y)
  2. A∈|C| ごとに、rΛAX,Y:C(X¥otimesA, Y)→C(X, Y◁A)
  3. A∈|C| ごとに、rlΛAX,Y:C(X¥otimesA, Y)→C(X, A▷Y)
  4. A∈|C| ごとに、lrΛAX,Y:C(A¥otimesX, Y)→C(X, Y◁A)

2番目か3番目が使われているケースが多いように思います。しかし、左右の指数を区別しない(どちらか一方を単に指数とする)ので、使っている人がどちらを意図しているかは分かりません。複数ある指数とカリー化のどれを使っているかを明示しない/適当に混ぜる習慣は混乱を招くので良いとは思いません。

僕は、対称の場合でも左右の指数を区別する方針ですが、そのための適切な記法がないので苦労します。それが記号法が安定しない事情です。今回は、▷, ◁, lΛ, rΛ, rlΛ, lrΛ で区別しました。

*1:そもそも、カリー化/反カリー化(ホムセットの同型)の存在を前提として「指数」「内部ホム」という言葉を使います。

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

2018-02-07 (水)

マイクロコスモ原理と逆帰納ステップ

| 18:45 | マイクロコスモ原理と逆帰納ステップを含むブックマーク

最近、高次圏の話をいくつか書いてますが、高次圏そのものに興味を持ったというより、高次圏と向き合わざるを得ない感じなのです。

マイクロコスモ原理の問題がけっこうシリアスで、なんとか回避したいのですが、どうもスッキリとは解決できないんです。仏教に帰依しようか … なんてね。

内容:

  1. マイクロコスモ原理
  2. 無限後退は回避されるのか
  3. マックレーンの五角形で試してみると
  4. 五角形の等式を検証
  5. モノイドの定義が先送りされる構造
  6. 帰納ステップ
  7. 帰納ステップを止める手段
  8. 内部からの視点だけで処理すること

マイクロコスモ原理

過去に何度か触れてますが、もう一度、マイクロコスモ原理の短い説明を引用しておきます。

https://ncatlab.org/nlab/show/microcosm+principle

Microcosm principle: Certain algebraic structures can be defined in any category equipped with a categorified version of the same structure.


マイクロコスモ原理: 特定の代数構造は、その代数構造を圏化した構造を備える圏のなかで定義可能である。

マイクロコスモ原理を素朴に解釈すれば、ある代数構造の定義をしたいときに、その構造の圏化〈categorification〉を際限なく続けなくてはならず、結局は何も定義できないように思えます。次の記事に、「これは怖い」と書きました。

マイクロコスモ原理では、構造を載せる対象物と、その対象物が棲んでいる環境が出てきます。対象物は圏論的意味での対象〈object〉で環境は圏〈category〉です。この「対象と圏」という関係が繰り返し繰り返し現れます。

高次圏: 複雑さの3つ目の方向と相対階数」において、「対象と圏」の関係を表すために'∈0'という記号を導入しました。X ∈0 Y は、X∈|Y| と同じ意味です。

直感的かつ素朴に考えてみると、次のような所属関係の系列(「所属関係の系列」も、「高次圏: 複雑さの3つ目の方向と相対階数」で定義しています)がありそうです。

  • 対象 ∈0 圏 ∈0 圏の圏 ∈0 圏の圏の圏 …

マジメに考えると、この系列を構成することは難しいのですが、素朴な発想のまま話を続けます。

代数構造の事例としてモノイド構造を考えます。モノイド構造を持った対象はモノイド対象と呼んでいいでしょう(実際にそう呼びます)。形容詞「モノイド」を同様の意味で使うと:

  1. モノイド対象
  2. モノイド圏
  3. モノイド(圏の圏)
  4. モノイド(圏の圏の圏)

といったモノイド・ナントカ達が出現します。「モノイド(圏の圏)」という書き方をしたのは、「(モノイド圏)の圏」と区別するためです。「圏の圏」にモノイド構造が載ったものが「モノイド(圏の圏)」で、「モノイド圏」達を対象とする圏は「(モノイド圏)の圏」です。

モノイド構造に対してマイクロコスモ原理を適用すると:

  1. モノイド対象を定義するには、モノイド圏の定義が必要である。
  2. モノイド圏を定義するには、モノイド(圏の圏)の定義が必要である。
  3. モノイド(圏の圏)を定義するには、モノイド(圏の圏の圏)の定義が必要である。

いったいどうすりゃいいんじゃい?! となります。

無限後退は回避されるのか

僕が当初抱いた感想は、「実際にはモノイド対象が定義できているのだから、何らかのメカニズムで無限後退は抑えられているのだ」というものです。「何らかのメカニズム」がハッキリすれば、恐怖も不安も解消されるはずです。

「何らかのメカニズム」として、自然的と人為的の二種類がありそうに思えました。

  1. 自然的: マイクロコスモ原理に従って、圏化の階層を昇る(所属関係の系列を右に行く)と、そのうち自然に圏化のプロセスが止まってしまう。
  2. 人為的: 圏化のプロセスを、人為的に(強制的に)やめる。しかし、人為的中断には合理的な根拠がある。

自然に階層(所属関係の系列)が止まるのが望ましい解決です。なので僕は、マイクロコスモ原理が適用できなくる地点があって、そこで階層が自然に止まることを期待していました。もし自然に止まらなかったら? 階層の適当なところでマイクロコスモ原理の適用を強制的にやめる算段を検討するしかないでしょう。

マックレーンの五角形で試してみると

モノイド構造の事例で、「マイクロコスモ原理が適用できなくる地点」を探してみましょう。それをやってみたのが次の記事です。(「マイクロコスモ原理の恐怖」にも概要は書いてあります。)

以下では、すぐ上に引用した記事とほぼ同じ記法を使いますが、ひとつ変更します。モノイド圏Cの単位対象を1(太字のイチ)で表し、唯一の対象と恒等射からなる自明圏はI(太字の大文字アイ)で表します。

Cは小さい圏だとして、Cにモノイド構造を載せます。構造を載せる対象物であるCは、圏の圏Catという環境に棲んでいます。Catの対象〈0-射〉であるCの上の構造は、Cat内の1-射(関手)や2-射(自然変換)を使って定義されます。それら、構造を定義するための1-射、2-射は:

  • 1-射 I = IdC : CC  ― 恒等関手
  • 1-射 Y = ¥otimes : C×CC  ― モノイド積二項関手
  • 1-射 i : IC  ― 単位対象を識別するポインティング関手
  • 2-射 α :: YI*Y⇒IY*Y : C×C×CC  ― 結合律子自然変換
  • 2-射 λ :: iI*Y⇒I : CC  ― 左単位律子自然変換
  • 2-射 ρ :: Ii*Y⇒I : CC  ― 右単位律子自然変換

そして、これらの素材からの(Cat内に拡がる)構成物を支配する法則として、マックレーンの五角形と三角形があります。今は五角形のほうに注目しましょう。

マックレーンの五角形をインデックスなしの等式で表す」では、マックレーンの五角形を3-射として記述しました。

  • 3-射 penta ::: YII*α ; IIY*α ≡> αI*Y ; IYI*α ; Iα*Y :: YII*YI*Y ⇒ IIY*IY*Y : C×C×C×CC

2-圏であるCatの3-射とは等式なので、次のように書けます。

  • 等式 YII*α ; IIY*α = αI*Y ; IYI*α ; Iα*Y :: YII*YI*Y ⇒ IIY*IY*Y : C×C×C×CC

等式の両辺である自然変換は同じプロファイルを持っていて、そのプロファイルは次です。

  • YII*YI*Y ⇒ IIY*IY*Y : C×C×C×CC

実は、ここの記述が不正確です。僕だけでなく、ほとんど常に不正確に書かれています。「ごまかしている」と言われかねない状況です。

上記のプロファイルが意味を持つには、次が要求されます。

  • dom(YII*YI*Y) = dom(IIY*IY*Y) = C×C×C×C

よく考えてみると、この等式は成立していません(次節で詳述)。なので、何らかの補正をしないと、マックレーンの五角形に関する記述の根底が崩れて無意味になります。左右の単位律子やマックレーンの三角形も不正確で、先に挙げたままではダメです。

五角形の等式を検証

前節の最後の等式:

  • dom(YII*YI*Y) = dom(IIY*IY*Y)

'*'は関手の結合を意味するので、

  • dom(YII*YI*Y) = dom(YII)
  • dom(IIY*IY*Y) = dom(IIY)

となります。よって、次の等式を吟味すればいいでしょう。

  • dom(YII) = dom(IIY)

直積の記号'×'を省略しているので、ちゃんと書くと:

  • YII = (Y×I)×I
  • IIY = (I×I)×Y

I = IdC : CC であり、Y = ¥otimes : C×CC だったので、

  • dom(YII) = (dom(Y)×dom(I))×dom(I) = ((C×CCC
  • dom(IIY) = (dom(I)×dom(I))×dom(Y) = (C×C)×(C×C)

以上より、等式 dom(YII*YI*Y) = dom(IIY*IY*Y) は、 等式 ((C×CCC = (C×C)×(C×C) と同値です。しかし、((C×CCC = (C×C)×(C×C) は成立しません。等式ではなくて:

  • ((C×CCC ¥stackrel{¥sim}{=} (C×C)×(C×C)

この同型を与えるのは、Catが備えている直積×に関する結合律子です。Cの結合律子α(Cat内の2-射=自然変換)と区別するために、太字のαを使うと、直積×に関する結合律子αは:

  • α :: (×)×IDCat×IDCat ; (×)×IDCat ; (×) ⇒ IDCat×IDCat×(×) ; IDCat×(×) ; (×)

'×'は、Catが棲んでいる環境が備えている直積の記号です。結合の記号';'も、上記の式内では環境における2-射の縦結合を意味します。

さて、「圏の圏Catが棲んでいる環境」とはいったいどこでしょう? Catは厳密2-圏なので、「(厳密2-圏)の圏」が環境でしょう。しかし、Catは大きな厳密2-圏なので、「(小さな厳密2-圏)の圏」ではダメです。「(必ずしも小さくない厳密2-圏)の圏」をs2-CATとしましょう。このs2-CATが「圏の圏Catが棲んでいる環境」と考えてよさそうです。つまり、

  • Cat0 s2-CAT

モノイドの定義が先送りされる構造

Cの対象のひとつをAとすると、Aから始まる所属関係の系列があります。

  • A ∈0 C0 Cat0 s2-CAT

この系列に沿って、マイクロコスモ原理は次のように適用されます。

  1. 対象Aのモノイド構造は、圏Cのなかで定義される。Cのモノイド構造が必要。
  2. Cのモノイド構造は、圏の圏Catのなかで定義される。Catのモノイド構造が必要。
  3. 圏の圏Catのモノイド構造は、圏の圏の圏s2-CATのなかで定義される。s2-CATのモノイド構造が必要。

定義に必要な射を表にまとめると:

環境 A C Cat s2-CAT
構造の0-射     1, A I, CJ, Cat
構造の1-射 m, e ¥otimes, i ×, i
構造の2-射 as, lu, ru α, λ, ρ α, λ, ρ
構造の3-射 penta, tri penta, tri
構造の4-射
  • 1は、モノイド圏Cの単位対象です。
  • as, lu, ruはそれぞれ、結合律、左単位律、右単位律の等式です。
  • J∈|s2-CAT| は、唯一の対象と恒等射と恒等2-射からなる自明な厳密2-圏です。
  • α, λ, ρ は、α, λ, ρ と同様な役割を持つs2-CATの2-射です。
  • penta, tri は、penta, tri と同様な法則を表すs2-CATの3-射です。

モノイド構造には、二項演算である乗法と、無項演算(定数)である単位があります。それがどのようになっているかを示します。

  • 対象Aの上のモノイド構造: m:A¥otimesA→A, e:1→A in C
  • の上のモノイド構造: ¥otimes:C×CC, i:IC in Cat
  • 圏の圏Catの上のモノイド構造: ×:Cat×CatCat, i:JCat in s2-CAT

Cat×Cat」の×は上の表には出てこなくて、圏の圏の圏s2-CATが棲んでいる環境(圏の圏の圏の圏)のなかの1-射(関手)です。この×のプロファイルは、×:s2-CAT𝕏s2-CATs2-CAT のようになり、さらにs2-CATの環境の環境(圏の圏の圏の圏の圏)のなかの1-射である直積𝕏を要求します*1

もうお分かりと思いますが、「自然に階層(所属関係の系列)が止まる」ことは期待できそうにありません。「環境の環境の…」として「圏の圏の…」がいくらでも出現してしまいます。

ひとつ注意事項を加えます。上の表のなかの「?」についてです。s2-CATは3-圏になるので、3-射は等式(恒等3-射)以外にも在ります。もし、等式を可逆3-射に弱めると、可逆3-射であるpentatriを統制する法則としての4-射、つまり3-圏s2-CATのなかの等式が必要でしょう。その等式が不明なので「?」を入れています。

楽観的な見通しとしては、「?」は不要かと思います。3-圏s2-CATの全体は不要で、3-射を削り落として2-圏とみなしたs2-CAT(2)を考えて、penta, tri はやはり等式として扱うのです。所属関係の系列が伸びていっても、圏の次元は2よりは上がらない(上げる必要がない)だろう、と楽観視してます。けど、モノイド圏を弱化した構造も意味があるとは思います。

帰納ステップ

数学的帰納法には、ベースとステップがあります。自然数kを含む命題P(k)があるとき、「P(k)ならばP(k + 1)」の形が帰納のステップです。k = 0 と置いたベースP(0)とステップが一緒になると、任意の自然数nに対するP(n)が成立します。

さて、「P(k + 1)ならばP(k)」という形の命題を考えます。帰納ステップと逆*2なので帰納ステップと呼びましょう。

マイクロコスモ原理の状況では、逆帰納ステップ形式の命題が現れます。A ∈0 C0 Cat0 s2-CAT のような所属関係の系列に対して、基準を決めて相対階数(「高次圏: 複雑さの3つ目の方向と相対階数」参照)を導入します。左端のAを基準として、相対階数が 0, 1, 2, ... と自然数になるようにしましょう。こうやって決めた相対階数を、一時的に単に階数と呼びます。

所属関係の系列をひとつ固定して(例えば、A ∈0 C0 Cat0 s2-CAT0 …)、「階数rの対象物にモノイド構造が定義できる」という命題を考えます。この命題をQ(r)とします。

  1. Q(0) ⇔ 階数0の対象物にモノイド構造が定義できる
  2. Q(1) ⇔ 階数1の対象物にモノイド構造が定義できる
  3. Q(2) ⇔ 階数2の対象物にモノイド構造が定義できる

マイクロコスモ原理は、「Q(r)であるためにはQ(r + 1)を要求する」なので「Q(r + 1)ならばQ(r)」の形で逆帰納ステップになります。

帰納ステップの形の命題では、Q(r)の成立をQ(r + 1)に先送りすることになります。今の場合は、rが階数を表すので、ひとつ上の階数へと先送りします。階数が上がると外の環境へ・外の環境へと階層を昇るので、逆帰納ステップは、事物に関する命題の記述を環境の構造に依存させる形になります。

普通に考えれば、逆帰納ステップの命題を与えられてもどうにもなりません、何も言えません。

帰納ステップを止める手段

rが自然数全体を動くとして、「Q(r + 1)ならばQ(r)」の形の逆帰納ステップがまったく無意味とは思いません。不動点や終対象は、そのような状況に意味を与えてくれることがあります。しかし、今考えている「Q(r) ⇔ 階数rの対象物にモノイド構造が定義できる」の文脈では、rを無限に大きくしていくことは(僕には)考えにくいです。

有限な自然数Nに対してQ(N)を確定させて、逆帰納ステップを止めることを考えます。どうやって止めるか? 考えられる候補は次のようなものでしょう(他にも在るかも知れないけど)。

  1. Q(N)は、経験的・直観的*3に明らかだとする。
  2. Q(N)を、より単純で強い命題に置き換えてしまう。
  3. Q(N)の証明を、圏論から離れて別な方法で行う。

それぞれの手段をより具体的にみていきましょう。

まず、「経験的・直観的に明らかだとする」とは、階数Nの環境は熟知しているので、それ以上の形式化は不要だと判断することです。A ∈0 C0 Cat0 s2-CAT0 … の例では、階数2のCat内の現象は十分に知っているから、そこから外には出ないと決めることです。これは、「マイクロコスモ原理の恐怖 // どうやって無限後退を避けるか」でも書いた方法です。

「より単純で強い命題に置き換える」は、環境となる圏が備える直積(デカルト・モノイド積)を厳密だと仮定することです。実際には、直積は厳密モノイド積じゃないことが多いのですが、厳密モノイド積だと仮定しても不都合はないだろう、と考えます。暗黙にこの方法が使われている例は多そうです。ほんとに不都合がないことを示すには、厳密化定理が必要です。厳密化定理の定式化に現れるモノイド圏の定義をどうするか? で、また循環に陥〈おちい〉りそうな気配もあります。

最初の方法で、Catは十分に知っているから、そこから外には出ないことにしました。十分に知っている根拠が経験と直観だというのが気になるなら、Cat集合論のなかで具体的に定義して、集合論的対象物として処理する方法があります。おそらくこれが標準的な方法だと思います。

内部からの視点だけで処理すること

マイクロコスモ原理から逆帰納ステップの形の命題が生じます。この逆帰納ステップが自然に止まることはないので、どこかで人為的に止める必要があります。前節で止める方法(の候補)を述べました。

正直なところ、心情的にあまりスッキリしません。しかしいずれにしても、ある環境のなかでの自己充足的な処理は必要です。環境の外に出ることはしないで、すべての事をその環境内の道具だけで遂行します。もはやそれ以上は外に出られない環境を、ワーキング宇宙(のトップレベル)という言葉で表現したことがあります。

世界を外から見られる視点と世界のなかだけしか見えない視点、それらの相互関係を正確に把握することが肝なんだと思うのですが、なかなかに難しい。

大乗仏教中観派と一般モデル理論」で紹介したダイアコネスクは、中観派〈ちゅうがんは〉思想に傾倒している様子でしたが、確固たる基礎が望めないような階層的世界の解釈には仏教が相性がいいのかも知れません。でも、僕の仏教との接点は法事とお墓参りくらい、ですね。

*1:記号'𝕏'は、黒板太字(blackboard bold)のエックスです。ユニコードのU+1D54Fの文字です。

*2:逆は、含意命題の前件と後件が入れ替わっていること。

*3:直感と直観は意味が違うらしいんだけど、辞書引いてもその後すぐに忘れます。

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

2018-02-01 (木)

高次圏: 複雑さの3つ目の方向と相対階数

| 17:00 | 高次圏: 複雑さの3つ目の方向と相対階数を含むブックマーク

高次圏に関してダラダラ書くシリーズ。

前回「高次圏: 複雑さの2つの方向と半厳密性」において、高次圏は、高次化と弱化の2つの方向で難しくなると書きました。もうひとつの難しさの方向として、階数が上がる方向について考えてみます。

内容:

  1. 所属関係
  2. 相対階数
  3. 相対階数と次元
  4. 相対階数が増える方向

所属関係

Aが集合であるとき、Aは集合圏Setの対象ですから、A∈|Set| と書けます。ここで使っている記号'∈'は、集合論的な普通の所属関係です。ただし、|Set|は通常の意味の集合ではないので、大きな集合(類ともいう)まで考えての所属関係です。

一般に、Cが圏のとき、A∈|C| であることを、A∈0C と書くことにします。'∈0'は、「対象(0-射)として所属する」ことを意味します。A∈0C を単に A∈C と書くことが多いですが、Cには対象(0-射)以外に射(1-射)も含まれます(高次圏なら高次の射もあります)。なので、'∈'と'∈0'は別な記号のほうがいいでしょう。

集合圏Setは圏ですが、Set0Cat とはなりません。Catは“小さい圏の圏”と定義されているので、大きな圏であるSetを含むことはできません。大きくてもよい(しかし局所小な)圏の圏をCATとすれば、Set0CAT は成立すると考えられます。

集合A、集合圏Set、局所小な圏の圏CATの三者のあいだには次のような所属関係が成立します。

  • A ∈0 Set0 CAT

このように、所属関係でつながれた並びを所属関係の系列〈{series | sequence | chain} of membership relations〉と呼ぶことにします。

相対階数

A0, A1, ..., Ap をn-圏とします。次元nはそれぞれ異なっていいとします。これらのn-圏(さまざまなn)が所属関係の系列を作っているとします。

  • A00 A10 ... ∈0 Ap

この状況で、相対階数〈relative rank〉を次のように定めます。

  1. A0, A1, ..., Ap のなかのどれか1つのAj(0≦ j ≦p)を選んで、Ajの相対階数を0とする。
  2. Ai(0≦ i ≦p)の相対階数は i - j により定義する。

例えば、所属関係の系列 A ∈0 Set0 CAT において、Setの相対階数を0と決めると、次のような相対階数の割り当てになります。

n-圏 A Set CAT
相対階数 -1 0 1

相対階数は、基準の決め方で変わるので、次のような割り当てもあります。

n-圏 A Set CAT
相対階数 その1 -1 0 1
相対階数 その2 0 1 2
相対階数 その3 -2 -1 0

あくまで相対的なのです。相対階数は系列のなかで決まるだけで、一般的に決まるわけではありません。

相対階数と次元

所属関係の系列 A ∈0 Set0 CAT を考えます。集合Aを基準とした相対階数と、n-圏としての次元(n)は次のようになります。

n-圏 A Set CAT
相対階数 0 1 2
次元n 0 1 2

この例を見ると、相対階数が上がると次元も上がるように思えますが、そうとは限りません。

CAT(1)を2-圏であるCATから2-射を除外して1-圏と考えたものだとします。A ∈0 Set0 CAT(1) は所属関係の系列になります。この系列内では:

n-圏 A Set CAT(1)
相対階数 0 1 2
次元n 0 1 1

別な例を挙げます。Kを小さい2-圏とします。2-Cat(1)を、小さい2-圏の3次元圏から3-射と2-射を除外した1-圏とします。CAT(0)は、CATから2-射と1-射を除外した0-圏(単なる集合)と考えたものだとします。このとき、K0 2-Cat(1)0 CAT(0) は所属関係の系列になります。この系列内では:

n-圏 K 2-Cat(1) CAT(0)
相対階数 0 1 2
次元n 2 1 0

相対階数の上昇と次元の上昇は関係ありません。所属関係において親となるほうのn-圏の次元が同じだったり、むしろ次元が下がる場合もあります。

系列の作り方により次元はどうにでもなるので、相対階数と次元のあいだに法則的な関連性はありません。

相対階数が増える方向

所属関係の系列において相対階数を考えると、相対階数が上がっても次元が上がるとは限りません。しかし、次元がどうであれ、相対階数が上がれば話は難しくなります。

n-圏Cがあるとき、Cが所属するようなk-圏を作るのは簡単です。例えば、対象としてCだけを持ち、射としてCの同型関手だけを持つ1-圏が作れます。話が難しくなるのは、Cだけではなく、Cと同類のその他もろもろのn-圏をすべて含むような上位のk-圏を作ることです。

なんらかの性質をもつn-圏をすべて含むk-圏Dを作れば、C0 D という所属関係が成立します。そして、Dは十分に大きなk-圏となります。十分に大きな圏Dは便利ですが、D0 E となるような十分に大きな圏Eを作るのが困難になります。D自体が大きいので、それを収容するEが作りにくいのです。

一般に、十分大きな圏からなる所属関係の系列を伸ばすのは難しいのです。サイズの問題〈size {issue | problem}〉が現れるからです。

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

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

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

2018-01-30 (火)

マックレーンの五角形をインデックスなしの等式で表す

| 14:44 | マックレーンの五角形をインデックスなしの等式で表すを含むブックマーク

モノイド圏の定義でマックレーンの五角形と三角形が出てきます。最初は何だか意味不明なんですが、マックレーンの五角形/三角形の可換図式は、モノイド圏の肝のひとつです。これらの可換図式をインデックス(パラメータ、全称限量子の束縛変数)なしの等式で表してみます。

なんでそんなことをするかは最後の節でちょっと触れます。

内容:

  1. マックレーンの五角形
  2. 色々な描き方
  3. ツリーの変形としての五角形
  4. 記法の工夫をしないと
  5. 2次元の等式的定義

マックレーンの五角形

マックレーンの五角形と三角形の可換図式は次のようなものです。

*1

*2

五角形の上側の二辺を時計回りにたどると:

  1. αA⊗B,C,D
  2. αA,B,C⊗D

五角形の下側の三辺を反時計回りにたどると:

  1. αA,B,C¥otimesidD
  2. αA,B⊗C,D
  3. idA¥otimesαB,C,d

モノイド圏をCとして、Cの射の図式順結合を';'で表せば、五角形可換図式は次のような等式になります。左辺が上側時計回り、右辺が下側反時計回りです。

  • αA⊗B,C,D ; αA,B,C⊗D = αA,B,C¥otimesidD ; αA,B⊗C,D ; idA¥otimesαB,C,D

この等式では、自然変換αの成分表示を使っています。A, B, C, DはCの任意の対象なので、実際には次のように全称限量子が等式の先頭に付きます。

  • ∀A, B, C, D∈|C|.( αA⊗B,C,D ; αA,B,C⊗D = αA,B,C¥otimesidD ; αA,B⊗C,D ; idA¥otimesαB,C,D )

限量子もインデックス(成分表示における下付きの対象)もなしで五角形を等式表示できないでしょうか。この問〈とい〉がこの記事の主題ですが、次節では絵の話をします。

色々な描き方

マックレーンの五角形/三角形は手書きで何度か描いたことがあります。

2月の圏論勉強会 - 檜山正幸のキマイラ飼育記(五角形の上側は反時計回り、五角形の下側は時計回り)

マックレーンの五角形の絵 - 檜山正幸のキマイラ飼育記(五角形の上側は反時計回り、五角形の下側は時計回り)

モノイド圏と加群圏に関するフォークロアとマックレーン五角形・三角形(五角形の上側は時計回り、五角形の下側は反時計回り)

これらの図で、五角形の頂点はツリーで、五角形の辺はツリーの変形になっていることが分かるでしょう。ストリート(Ross Street)は、ツリーの代わりに五角形を使って、“五角形を頂点に描いた五角形”を使ったりしています(珍しい描き方です)。

*3

ギロー/マルボス(Yves Guiraud, Philippe Malbos)のスライドには、綺麗な五角形の絵があります。ただし、この絵では、五角形の辺が3-射(3次元の射)で、五角形全体が表す射は4-射になっています。我々が扱う状況は次元が1つ下がって、五角形の辺が2-射で、五角形全体は3-射です。

*4

*5

ツリーの変形としての五角形

さて、五角形をツリーの変形過程の絵として捉えましょう。次の図を使うことにします。冒頭の可換図式と同じレイアウトにツリーの絵を足したものです。

豊饒圏をちゃんと定義したい - 檜山正幸のキマイラ飼育記(五角形の上側は時計回り、五角形の下側は反時計回り)

この図の上側の時計回り(青い矢印 1→5→4)の変形をアスキーアートで描いてみます。

Y I I     Y Y     | | Y
 Y |  ==>  Y  ==>  | Y
  Y                 Y

これを、“絵”ではなくて“式”として合理化します。

  1. Cの恒等関手 IdC:CC をIと書くことにする。I:CC (IはCの単位対象ではないので注意
  2. Cのモノイド積 ¥otimes:C×CC をYと書くことにする。Y:C×CC
  3. 圏の直積、関手の直積を併置(空白を挟んでもよい)で表す。例えば、IdC×IdC×IdC = III = I I I 、¥otimes×IdC = YI = Y I 。
  4. 関手の図式順結合を'*'で表す。
  5. 関手の結合(アスタリスク)より直積(併置)のほうが演算子の優先度が高いとする。

以上の約束で、上のアスキーアートの左のツリーは、YII*YI*Y と書けます。縦にスタックする代わりにアスタリスク'*'を使います。上から下へのスタックが、アスタリスクをはさんだ左から右への1行でテキスト表示されます。

結合律子α(律子に関しては「律子からカタストロフへ」を参照)は、次のように書けます。

  • α:: YI*Y⇒IY*Y : CCCC

これを反図式順('・'は右から左に読む)の普通の記法で書くと:

  • α:: ¥otimes・(¥otimes×IdC)⇒¥otimes・(IdC×¥otimes) : C×C×CC

見てのとおり煩雑になるし、ツリーとの対応も取れなくなるので、この記法は使いません。

α::YI*Y⇒IY*Y を YII*YI*Yの下側のYI*Yに適用すれば次のようになります。

Y I I     Y | |
 Y I  ==>  I Y
  Y         Y

この変形を YII*α と書きます。これは関手YIIと自然変換αのヒゲ結合〈whiskering〉です。ヒゲ結合も自然変換の横結合も通常同じ演算子記号(ここでは'*')で表します。

直積はモノイド積なので、交替律〈interchange law〉 FG*F'G' = (F*F')(G*G') があります。交替律を使うと、次のツリーはいずれも同じ関手を表します。グラフとして同じトポロジーなら同じ関手です。

Y | |   Y Y   Y Y   | | Y
 I Y    | |    Y     Y |
  Y      Y            Y

上の一番右のツリーの下側のYI*Yに α::YI*Y⇒IY*Y を適用すると、

I I Y     I I Y
 Y I  ==>  I Y
  Y         Y

この変形は、関手IIYと自然変換αのヒゲ結合ですから IIY*αと 書けます。

今説明した2つの変形を繋げると五角形の上側になるので、YII*α ; IIY*α が以下の変形です。

Y I I        I I Y
 Y I  ==>==>  I Y
  Y            Y

同じ要領で五角形の下側もたどると、それぞれの変形は次のように表せます。

  1. α(I*I)*Y = αI*Y (I*I = I なので)
  2. IYI*α
  3. (I*I)α*Y = Iα*Y

繋げれば、

  • αI*Y ; IYI*α ; Iα*Y

ですね。

したがって、五角形が表す等式は、

  • YII*α ; IIY*α = αI*Y ; IYI*α ; Iα*Y

となります。

この記事では、マックレーンの三角形のほうには焦点を当ててませんが、同様にして次の等式が得られます。

  • IiI*α = ρI*Y ; Iλ*Y

ここで:

  • 1は、ひとつの対象と恒等射からなる自明な圏
  • i:1C は、単位対象を特定するポインティング関手
  • λ::iI⇒I:CC は、左単位律子
  • ρ::Ii⇒I:CC は、右単位律子

記法の工夫をしないと

次の表は、「関手と自然変換の計算に出てくる演算子記号とか」で出した表の抜粋(に直積を追加)したものです。

演算 反図式順演算子記号 図式順演算子記号
圏/関手の直積 × 併置
関手の結合 *
自然変換の縦結合 ¥circ ;
関手と自然変換のヒゲ結合 *
自然変換の横結合 *

特に工夫をしない反図式順で前節の等式(下に再掲)を書き下してみましょう。

  • YII*α ; IIY*α = αI*Y ; IYI*α ; Iα*Y

部分ごとに翻訳します。

  • 左辺の右 [α・(IdC×IdC×¥otimes)]
  • 左辺の左 [α・(¥otimes×IdC×IdC)]
  • 右辺の右 [¥otimes・(IdC×α)]
  • 右辺の中 [α・(IdC×¥otimes×IdC)]
  • 右辺の左 [¥otimes・(α×IdC)]

これらを組み合わせると:

  • [α・(IdC×IdC×¥otimes)] ¥circ [α・(¥otimes×IdC×IdC)] = [¥otimes・(IdC×α)] ¥circ [α・(IdC×¥otimes×IdC)] ¥circ [¥otimes・(α×IdC)]

煩雑で図式的直感も働かなくて、何もいいことがないのですが、現状のメジャーな記法は反図式順記法です*6

2次元の等式的定義

マイクロコスモ原理の恐怖」で、マイクロコスモ原理について紹介しました。

https://ncatlab.org/nlab/show/microcosm+principle

Microcosm principle: Certain algebraic structures can be defined in any category equipped with a categorified version of the same structure.


マイクロコスモ原理: 特定の代数構造は、その代数構造を圏化した構造を備える圏のなかで定義可能である。

ある代数構造を定義したいとき、それを定義する環境にも類似の構造が要求される、ということです。マイクロコスモ原理の典型例は、モノイドを定義するための環境としてモノイド圏が要求されることです。

では、モノイド圏を定義する環境にはいかなる構造が要求されるのでしょう。このことを調べるために、モノイド圏の定義の一部であるマックレーンの五角形/三角形を等式的に記述したかったのです*7

サイズの問題を避けるために、Cは小さなモノイド圏だとします。すると、Cは小さい圏の圏Cat内で定義されます。Catは直積を持つ厳密2-圏で、演算として、直積/縦結合/横結合を持ちます。

射の次元 直積 × 縦結合 ; 横結合 *
0-射=圏 圏の直積 - -
1-射=関手 関手の直積 関手の結合 -
2-射=自然変換 自然変換の直積 自然変換の縦結合自然変換の横結合

Catのなかで、モノイド圏Cが定義される様〈さま〉を観察しましょう。モノイド圏を構成する素材を列挙します。素材は、上の表に書いた各次元の射(0-射, 1-射, 2-射, 3-射)です。3-射は、実は等式です。

  1. 0-morphism C
  2. 1-morphism I: CC (I = IdC
  3. 1-morphism Y: CCC
  4. 1-morphism i: 1C
  5. 2-morphism α:: YI*Y⇒IY*Y : CCCC
  6. 2-morphism λ:: iI*Y⇒I : CC
  7. 2-morphism ρ:: Ii*Y⇒I : CC
  8. 3-morphism penta::: YII*α ; IIY*α ≡> αI*Y ; IYI*α ; Iα*Y :: YII*YI*Y ⇒ IIY*IY*Y : CCCCC
  9. 3-morphism tri::: IiI*α ≡> ρI*Y ; Iλ*Y :: IiI*YI*Y⇒Y : CCC

2-圏における3-射が等式になることは、以下の記事に書いてある(-1)次元の圏と反転原理から言えます。

1-圏(単なる圏)における2-射である等式を使った定義は等式的定義ですが、これは1次元までの素材(生成射)に関する等式なので1-等式的定義と呼びます。モノイド圏の定義は、2次元までの素材に関する等式なので2-等式的定義〈2-equational definition〉となります。

マイクロコスモ原理に話を戻すと、具体的な“直積を持つ厳密2-圏”Cat内で、2-等式的定義としてモノイド圏の定義が得られたのでここでオシマイと考えることもできます。しかし、モノイド圏を定義する環境としての“直積(あるいは一般のモノイド積)を持つ厳密2-圏”を定義する環境は何か? と考えると、マイクロコスモ原理による梯子をさらに上に昇ることになります。この梯子をどこまで昇ればいいんだろう? という不安な感じが“マイクロコスモ原理の恐怖”です。

この恐怖感を払拭するひとつの手段は「抽象化をやめる」ことなのかも知れません。しかし、抽象化をしたい欲求もあります。現状、うまく折り合いが付いてません。

*1:画像を含む元記事: http://math.ucr.edu/home/baez/quantum/node4.html

*2:画像を含む元記事: http://math.ucr.edu/home/baez/quantum/node4.html

*3:画像を含む元記事: https://www.sciencedirect.com/science/article/pii/002240498790137X

*4:画像を含む元記事: https://www.irif.fr/~guiraud/exposes/tianjin.pdf

*5:画像を含む元記事: https://www.irif.fr/~guiraud/exposes/tianjin.pdf

*6:表記法と描画法の混乱ぶりは「絵算(ストリング図)における池袋駅問題の真相」を参照。

*7:等式的記述をしたい理由は他にもありますが。

2018-01-26 (金)

山中伸弥教授のこと

| 12:50 | 山中伸弥教授のことを含むブックマーク

山中先生、あまりにもあまりにもかわいそう。いやっ、「かわいそう」という言葉を使うのは失礼な感じがするんだが、心情としてはそう思う。こんなに酷い扱いを受けて、怒りもせず/絶望もせず、というのはちょっとあり得ないのではないか。

テレビ番組に、解説者のような学者タレントのような感じで出演されているのを見たときも、「たぶん、必要性があるからされているんだろう」と思い、なんか心が傷んだ。

もし山中先生が国外に出たら、日本にとっては大損失だろうが、山中先生個人の問題として考えれば、「もうそんなに我慢しなくてもいいんじゃないか」と思う。日本より世界を救うのが山中先生のミッションだろうし。

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

2018-01-22 (月)

高次圏: 複雑さの2つの方向と半厳密性

| 15:36 | 高次圏: 複雑さの2つの方向と半厳密性を含むブックマーク

タイトルに付いている「高次圏:」の意味は、前回記事「高次圏: 用語法と文脈(主に2次元)」を参照してください。要するに、ダラダラした記事です。

「高次圏論は難しいなー」とため息をついているだけでは生産的じゃないですが、「なんで難しいか?」と考えてみるのは意味があるでしょう。難しさを引き起こす2つの要因についてダラダラ書きます。

内容:

  1. 高次化と弱化
  2. 弱さの集合
  3. 半厳密n-圏

高次化と弱化

高次圏: 用語法と文脈(主に2次元)」で述べたように、高次圏論の用語法はハチャメチャです。これは、高次圏論を学習困難にしているひとつの理由ではありますが、問題を引き起こしているのは人間です。

人間の行為云々は抜きにしても、高次圏という対象物は、それ自体で難しい対象物です。難しさの主たる理由は複雑さでしょう。その複雑さを2種類、あるいは2方向に分けて考えるとよさそうです。

  1. 次元が増えることによって複雑さが増す。
  2. 定義を弱くすることによって複雑さが増す。

図にするとこんな(↓)感じです。

  • 縦軸の0, 1, 2, 3, 4, ... は次元を表します。
  • 縦軸上に乗っている黒丸は、0次元の厳密圏, 1次元の厳密圏, 2次元の厳密圏, 3次元の厳密圏, 4次元の厳密圏, ... (厳密n-圏)を表します。
  • 0次元と1次元では、厳密圏しかありません。s0-Cat=集合の圏、s1-Cat=通常の圏の圏。
  • 2次元以上では、厳密圏以外に弱い圏〈weak category〉が登場します。横方向は、“弱さ”の拡がりです。
  • 弱さにはバリエーション(弱さの程度)があります。次元が増えるにしたがって、弱さのバリエーションは急激に増大します。
  • 赤枠で囲ってある部分は、常識的な労力で定義が書き下せそうな範囲です。

最後の「常識的な労力で定義が書き下せそう」は僕の主観です。“常識的”でない例はあります。例えば、トッド・トリンブル〈Todd Trimble〉は、次元4の弱い(おそらく最も弱い)圏の定義を書き下しています。http://math.ucr.edu/home/baez/trimble/tetracategories.html の"2. The Definition of Tetracategory"から参照されているPDFに、合計51ページの定義があります。これは大変な力技で「常識的な労力」とは思えません。

弱さの集合

厳密n-圏の全体をsn-Catと書きます。sはstrictから、nは自然数を動く変数です。sn-Catの定義では、自然数nに関する数学的帰納法が使えるので、(簡単ではないが)ハッキリとした定義ができそうです。ハッキリとしていても、nが大きくなれば複雑な定義になります。

厳密とは限らない弱いn圏の全体をwn-Catと書きます。wはweakからです。任意のnに対して、wn-Catがハッキリ定義できるかどうかはよく分かりません。現状では、定義がたくさんあり、どれがベストか分かりません。そもそもベストな定義があるのかどうかも分かりません。なので、wn-Catは、実体的に存在するというより、希望的観測による想定上の存在です。

想定上の存在について語るので、雰囲気的な話になります。何もないよりは雰囲気でもあるだけマシでしょう。

いま、wn-Catは、最も弱い、あるいは完全に弱い〈fully weakened〉n-圏の定義に基づくクラス(大きい集合)だとします。すると、sn-Catws-Cat と考えていいでしょう。しかし、意味のあるn-圏のクラスはsn-Catws-Catだけに限らないでしょう。何らかの意味でのn-圏のクラスWがあり、sn-CatWws-Cat と位置付けられるでしょう。

前節の図をもう一度見てもらうと、点線の横棒は、nが多くなると幅が拡がっていきます。この横棒を“弱さ”を表すインデックス集合と考えて、Wnとします。Wnがどんな集合か? と聞かれると分かりませんが、存在はすると思います。“弱さ”を組み合わ的に分類すれば、Wnは有限集合にできる(有限種類に分類できる)のではないかと期待してます(期待だけ)。

nが何であっても、s, w∈Wn であって、任意の ρ∈Wn に対して次の包含関係が成立します。

  • sn-Catρn-Catws-Cat

ρ, τ∈Wn に対して、

  • ρn-Catτs-Cat ⇔ ρ ≦ τ

となるような順序関係≦を定義できます(できると想定する)。この順序関係で、sは最小元、wは最大元です。

nが2, 3, 4くらい(低次元のケース)なら、Wnとその上の順序構造を具体的に決定できるんじゃないのかな(期待だけ)。Wnがハッキリすれば、それはn-圏の世界の地図のようなものになります。

半厳密n-圏

半厳密n-圏〈semistrict n-category〉という概念があります。各次元ごとのWnと、ρ∈Wn に対するρn-Catが定義されて、さらに弱n-圏の同値性が定義されれば、半厳密性も定義できます。ここで、弱n-圏の同値性とは、「弱n-圏として事実上同じ」ことですが、nが大きくなれば同値性の定義も大変になります。n = 2, 3 のケースでは、biequivalent, triequivalentとして同値性が定義されています。

ρ∈Wnに対するρn-Catが次の性質を持つとします。

  • 任意の C∈|wn-Cat| に対して、CDが同値となる D∈|ρn-Cat| が存在する。

最も一般的なクラスwn-Catの代わりにρn-Catを用いても大丈夫だ、ということです。

ρn-Catが上の性質を持っていて、さらに次が成立するとします。

  • τ < ρである任意のτ(τ∈Wn)に対して、τn-Catは上の性質を持たない。

つまり、ρを小さくするともはや一般性を失います。一般性を失わないで、ギリギリまで厳密方向に近いn-圏達のクラスがρn-Catです。このとき、ρn-Catの対象を半厳密n圏と呼びます。Wnが全順序とは限らないので、半厳密n-圏の定義も一意的ではありません。

n = 2 では、すべての弱2-圏が厳密2-圏と同値(biequivalent)なので、半厳密性は n ≧ 3 で意味を持ちます。n = 3 では、Gray-圏の圏が半厳密性を持つことが知られています。

半厳密性を持つ ρ∈Wn が見つかれば、ρn-Cat は“n-圏の圏”としての一般性を持ち、厳密に近いことから扱いやすいはずです。半厳密n-圏のクラスを見つけることは、適切な作業環境を手に入れることなので重要です。wn-Catではなくても、何らかの目的に対して十分なτn-Catがあるとき、τn-Catに対する“半厳密n-圏の圏”ρn-Catも役に立ちます。

2018-01-20 (土)

高次圏: 用語法と文脈(主に2次元)

| 11:04 | 高次圏: 用語法と文脈(主に2次元)を含むブックマーク

高次圏論〈higher category theory〉に興味はあるし、必要性も感じているのですが、難しくてよく分からん、の状態が何年も続いています。

高次圏に関してちゃんとした事をちゃんと書くのは僕には荷が重いので、思い付きをダラダラ書くことにします。そういう記事のタイトルには「高次圏:」を接頭語に入れます。ダラダラ記事でも(少なくとも自分自身にとっては)無意味ではないと思います。錯綜した分野なので、道案内のヒントはそれなりに有意義かと。

内容:

  1. テキスト(教科書的資料)
  2. だらしなくザンネンな用語法
  3. 文脈により言葉の解釈が変わる
  4. 厳密n-圏
  5. n-圏の意味
  6. 厳密、強、ラックス、反ラックス
  7. 2-関手と擬関手
  8. 自然変換の種類
  9. まとめ

シリーズ:

  1. 高次圏: 用語法と文脈(主に2次元)
  2. 高次圏: 複雑さの2つの方向と半厳密性
  3. 高次圏: 複雑さの3つ目の方向と相対階数

テキスト(教科書的資料)

2次元の圏論のテキストを挙げておきます。よく引用されるレンスターの論文から:

概要、第0節に次のように書いてあります。

A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem.

This is a minimalist account of the coherence theorem for bicategories.

とにかく簡潔です。定義がダーッと並んでいるだけ。懇切丁寧な説明はありませんが、短いので参照には便利です。

同じ趣旨で、モノイド圏に関するconcise guide/minimalist accountをバエズが書いています。

パワーの論文も同様にconcise/minimalですが、より特殊な状況を扱っているので、こっち(↓)のほうが分かりやすいかも知れません。

もっと丁寧で豊富な話題を扱った(そのぶん長い)テキストをラックが書いています。

最近、ヨーナス・ヒーデマン*1の次のテキストを見つけました。

通常の圏論の知識を仮定しておらず、4章までは圏論の説明です。5章と6章(合計で25ページ)はレンスター論文とだいたい同じです。1次元と2次元の圏論をまとめて書いてあるテキストとしてなかなかいいんじゃないでしょうか。

だらしなくザンネンな用語法

レンスターは、2次元/高次元の圏論の用語法は evolved messily〈乱雑に/だらしなく発展した〉と語っています。ヒーデマンも、ideally, ... but sadly ...〈概念的には … であるはずだが、哀しいかな(実際は) … である〉という言い回しを使っています。ほとんどの人が「困った状況だな」とは思っているでしょうが、どうしようもないので諦めているのでしょう。

規範となる標準的な用語法はないので、レンスター(ヒーデマンもほぼ同じ)の用語法をここでの一時的な基準とします。しかし僕自身、レンスターに従っているわけでもないので、僕の方針についてもこの記事でコメントします。

過去にも、「だらしないなー、ザンネンだなー、どうしたものか」という愚痴は書いたことがあります。ダブルスラッシュ'//'の後は、記事内の節のタイトルです。

  1. 2008年 n-圏とは何だろう // 高次圏に関連する概念/記法/用語
  2. 2011年 緩関手、反緩関手、強関手、厳密関手とか、おぼえられねー
  3. 2013年 絵算(ストリング図)における池袋駅問題の真相 (絵の描き方)
  4. 2014年 「余」と「双」の使い方がバラバラ
  5. 2016年2月 絵算の描画方向を示すために旗を使うことにした (絵の描き方)
  6. 2016年4月 関手と自然変換の計算に出てくる演算子記号とか (記号の使い方)
  7. 2016年7月 モノイド自然変換とモノイド同値関手 // 各種のモノイド関手の呼び名
  8. 2016年12月 モノイド圏の随伴性を“豊饒圏の圏”の随伴性に持ち上げる: 計画編 // 言葉と記号の約束
  9. 2017年1月 モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き) // 圏論の用語法の問題点と対策
  10. 2017年12月 ファンタジー: (-1)次元の圏と論理 // 高次圏の話

文脈により言葉の解釈が変わる

言葉の意味が文脈依存なのは当然です。が、高次圏論では、その文脈が多様・多彩過ぎます。個人ごとに別な用語法を持っているのがたぶん実情でしょう。とりあえず、大雑把な分類をすると:

  1. 2次元の圏論の文脈
  2. 低次元の圏論の文脈
  3. 一般次元の圏論の文脈
  4. 無限次元の圏論の文脈

こんな感じでしょうか。

2次元の圏論は比較的整備されています。低次元とは、2, 3, 4次元あたりです。3, 4次元の圏論はそれほど開発されてません。5次元以上は手付かずに近いと思います。個別の次元によらずに、任意のnに関する議論が一般次元の圏論です。ほんとに一般的だと難しすぎるので、扱いやすいモノを探して詳しく調べる感じです。無限次元も、やはり手頃な無限次元圏を探すのがミソでしょう

用語法・記号法の雰囲気は、2次元と低次元ではだいたい共通しています。一般次元と無限次元も同じように思えます。よって、最も大雑把な分類は、(2次元を典型例とする)低次元圏論の文脈と、一般のn次元圏論(n = ∞ を含む)の文脈の2種類です。

低次元圏論と一般のn次元圏論で何が違ってくるかというと、一般のnだと個別の概念に名前を付けられなくなることです。例えば、関手、自然変換、より高次元な類似概念は次のように命名されています。

  1. 関手〈functor〉
  2. 自然変換〈natural transformation〉
  3. 変更〈modification〉
  4. 摂動〈perturbation〉

この調子でずっと名前を付け続けるわけにはいきません。そこで、(n, k)-変換手〈(n, k)-transfor〉という番号kを含む概念・用語を作って、次のように考えます(nは省略してkを動かします)。

  1. 0-変換手=関手
  2. 1-変換手=自然変換
  3. 2-変換手=変更
  4. 3-変換手=摂動
  5. 4-変換手
  6. 5-変換手
  7. ... (k-変換手)

一般のn次元圏論では、次元そのものや次元に関連する番号で用語・記法が整理されるので、スッキリします。しかし、番号で呼ぶと味気なくてイマジネーションが湧かないデメリットもあります。

厳密n-圏

定義と構成法がハッキリしている高次圏の一族として厳密n-圏〈strict n-category〉があります。厳密1-圏と厳密2-圏は次のように定義します。

  1. 厳密1-圏は通常の圏である。
  2. 厳密1-圏の全体と関手からなる圏をs1-Cat(1)とする。右肩の(1)は、自然変換については考えないで、圏と関手からなる通常圏であることを示す。
  3. s1-Cat(1)に、圏の直積を考えると対称モノイド圏となる。
  4. 対称モノイド圏としてのs1-Cat(1)を豊饒化圏〈enriching (base) category〉とする豊饒圏を厳密2-圏と呼ぶ。
  5. 厳密2-圏のあいだの関手は、s1-Cat(1)-豊饒関手として定義する。

この定義で使っている道具は、直積による対称モノイド圏と豊饒圏です。つまり、モノイド圏と豊饒圏の概念は事前に準備されている、という前提です。

厳密k-圏が既に定義されているとして、厳密(k + 1)-圏は次のように定義します。

  1. 厳密k-圏の全体と関手からなる圏をsk-Cat(1)とする。
  2. sk-Cat(1)に、厳密k-圏の直積を考えると対称モノイド圏となる。
  3. 対称モノイド圏としてのsk-Cat(1)を豊饒化圏とする豊饒圏を厳密(k + 1)-圏と呼ぶ。
  4. 厳密(k + 1)-圏のあいだの関手は、sk-Cat(1)-豊饒関手として定義する。

この定義が有効であるためには、次が必要です。

  • sk-Cat(1)に直積があるとき、s(k+1)-Cat(1)にも直積が入る。

直積の構成が出来るなら、n = 1 をベースとして、数学的帰納法により任意のnに対する厳密n-圏とそのあいだの関手が定義できます。

n-圏の意味

厳密n-圏は、n次元の圏の定義としては狭すぎることが分かっています。非厳密な(不正確という意味ではない!)n-圏を考える必要があります。

ここで、用語法の困った問題に出会います。

厳密n-圏 厳密n圏+非厳密n-圏
用語法A n-圏 次元ごとに別な名前
用語法B 厳密n-圏 弱n-圏 または単にn-圏

この問題は次の過去記事で指摘しています。

傾向としては、低次元圏論の場合は用語法Aが使われて、「2-圏=厳密2-圏」になります。弱2-圏は双圏〈bicategory〉という名前で呼びます。2次元圏論のテキストであるレンスター論文では用語法Aを使ってます。一般n次元圏論では、「次元ごとに別な名前」は無理なので、「n-圏=弱n-圏」(用語法B)が多いようです。

現状における対策は、形容詞「厳密」「弱」を必ず付けるか、デフォルト・ルール(形容詞なしの解釈)をちゃんと明示するかです。

2次元のときは、非厳密も許す2次元圏の定義はひとつしかありませんが、3次元以上になると非厳密な圏も様々なバリエーションがあります。非厳密だが、厳密に近い圏を半厳密n-圏〈semistrict n-category〉と呼ぶことがありますが、半厳密の定義も立場や目的により様々です。

「厳密」の代わりに「強〈strong〉」という形容詞を使うことがあります。「強←→弱」でバランスはいいのですが、強度〈テンソル強度 | tensorial strength〉に関わる形容詞が「強」なので困ったことになります。例えば、次の記事に「強関手」という言葉が出てきます。

形容詞「強」は使わないほうがいいと思います*2

「弱」の代わりに「ラックス」を使って、非厳密を許すn-圏をラックスn-圏と呼ぶ人もいますが、少数派です。

厳密、強、ラックス、反ラックス

「厳密」の意味の「強」を排除しても、別な意味の「強」が出てきます。

モノイド圏は、対象がひとつだけの2次元圏とみなせます。なので、厳密モノイド圏と弱モノイド圏(非厳密モノイド圏を許す)があります。なぜか、「モノイド圏=弱モノイド圏」というデフォルト・ルールが定着しています。(定着しているんだから、文句はないです。)

モノイド関手は、原理的には次の2種類に分けられるはずです。

  1. 厳密モノイド関手: 法則が等式で成立する。
  2. 非厳密モノイド関手: 法則が等式では成立しない。

非厳密を許すモノイド関手を弱モノイド関手と呼んでもよさそうですが、そうではありません。

法則が等式 法則が同型 法則が同型とは限らない
用語法A 厳密モノイド関手 強モノイド関手 ラックス・モノイド関手
用語法B 厳密モノイド関手 モノイド関手 弱モノイド関手
用語法C 厳密モノイド関手 タイト・モノイド関手 ラックス・モノイド関手

用語法Aの強モノイド関手は、「テンソル強度を保存するモノイド関手」と言葉が競合してしまうし、用語法Bはデフォルト・ルールに頼るのがよろしくない。で、僕は用語法Cを使っています。「タイト←→ラックス」がまーまーバランスいいし、厳密〈strict〉はタイト〈tight〉よりもっときびしい感じがするでしょ(たぶん)。用語法Cは次の記事から使っています。

ラックス・モノイド関手の双対についても用語法が幾つかあります。混乱をまねく程のバリエーションではないでしょう。

ラックス・モノイド関手の双対
用語法A 反ラックス・モノイド関手〈oplax monoidal functor〉
用語法B 余ラックス・モノイド関手〈colax monoidal functor〉
用語法C ラックス・余モノイド関手〈lax comonoidal functor〉
用語法D ラックス・反モノイド関手〈lax opmonoidal functor〉

2-関手と擬関手

厳密2-圏であれ弱2-圏であれ、そのあいだをつなぐ関手は2-関手〈2-functor〉と呼びます。nLabの2-functorの項目に:

the prefix is not really necessary

the prefixは'2-'のことです。弱2-圏のあいだの関手に'2-'を付けても付けなくとも意味は変わらないということです。'2-'は、関手の両端が2次元の圏だと明示するだけで、関手に対する条件などとは関係ありません。したがって、「'2-'が何を意味するか」ではなくて、「単に2-関手と言ったときに何を意味するか」というデフォルト・ルールが問題になります。

法則が等式 法則が同型 法則が同型とは限らない
用語法A 2-関手 疑2-関手 ラックス2-関手
用語法B 厳密2-関手 2-関手 ラックス2-関手
用語法C 強2-関手 弱2-関手 ラックス2-関手
用語法D 厳密2-関手 タイト2-関手 ラックス2-関手

低次元圏論では、用語法Aが多いように思います(印象なので確証はありません)。用語法Bでは、「法則が同型」のときをデフォルトにしています。デフォルト(形容詞なし)を使うなら、この選択が一番多そうです(印象)。用語法Cは、「厳密」を「強」と呼ぶ場合で、好ましくないし、使う人は少なくなっているでしょう。最後の用語法Dは僕が使っているもので、「強」を避けてデフォルトも使いません。

なお、タイト2-関手を強2-関手、ラックス2-関手を弱2-関手と呼ぶ例があるかも知れません。僕は見たことないですが、ありそうな雰囲気。ラックスの双対は「反ラックス」または「余ラックス」と呼ぶと思います。

レンスターは、そもそも関手/2-関手という言葉を使わずに、双圏〈弱2-圏〉のあいだの射〈morphism〉と呼んでいます。余計な用語の導入を避けるための一方法です。双圏の圏Bicat(1)の射だから、辻褄はあってますが、圏の構成素である射と混乱します。

法則が等式 法則が同型 法則が同型とは限らない
レンスター 厳密準同型射 準同型射
  • 厳密準同型射=strict homomorphism
  • 準同型射=homomorphism

レンスターはどうやら形容詞「疑〈pseudo〉」を嫌ったようです。僕も「疑」には違和感があります。一番普通の関手概念を「擬関手」と呼ぶのはイカガナモノカ? と。

自然変換の種類

関手の場合と同様に、2-自然変換(より一般にn-自然変換)と'2-'を付けても特に意味は付加されません。2次元の圏を考えている文脈では、「2-自然変換=自然変換」です。

ただし、自然変換にも種類があります。レンスターの用語法を先に見ると:

法則が等式 法則が同型 法則が同型とは限らない
レンスター 厳密変換 強変換 変換
  • 厳密変換=strict transformation
  • 強変換=strong transformation
  • 変換=transformation

レンスターは、一般的なほうをデフォルトに採用して、条件がきびしいほうに形容詞を付ける方針のようです。

「疑」を使う用語法では、

法則が等式 法則が同型 法則が同型とは限らない
用語法A 自然変換 疑自然変換 ラックス自然変換
用語法B 厳密自然変換 疑自然変換 ラックス自然変換
  • 厳密自然変換=strict natural transformation
  • 疑自然変換=pseudonatural transformation
  • ラックス自然変換=lax natural transformation

用語法Aは厳密なケースをデフォルトにしていて、用語法Bはすべて形容詞を付けています。厳密なケースをデフォルトとするのは、レンスターと反対の方針だし、一般的n-圏の用語法とも整合しないので良くないですね。僕は、モノイド圏の場合も含めて同じ形容詞を使いたいので次が推奨です。

法則が等式 法則が同型 法則が同型とは限らない
檜山 厳密自然変換 タイト自然変換 ラックス自然変換

まとめ

人間達の行為を積み重ねた結果としての用語法は、どの分野であれ乱れることになります。それにしても、高次圏論の状況はだいぶひどい。事前の定義や断り書きがないと意味不明です。そして、事前の定義や断り書きがないケースが意外に多いという … 。すぐに改善するとは思えないので、注意するしかないですね。

以下のまとめでは、関手/自然変換の分類には、「厳密/タイト/ラックス/反ラックス」を使います。

  1. 「n-圏」の意味はハッキリしない。
    1. 低次元圏論では、「n-圏=厳密n-圏」が多い。
    2. 一般のn次元圏論では、「n-圏=弱n-圏」が多い。
  2. n ≧ 3 では、弱の意味は確定しない。さまざま非厳密n-圏がある。
  3. 明示的に「厳密」「弱」を付けるのが望ましい。
  4. 「厳密」、「ラックス」、「反ラックス」の意味は比較的安定している。
  5. 「強」「弱」は不安定で、他の情報がないと判断に苦しむ。
    1. 用法1: 強=厳密 -- この用法は減る傾向だが、残っている。
    2. 用法2: 強=タイト
    3. 用法3: 弱=タイト -- この用法は減る傾向だが、残っている。
    4. 用法4: 弱=ラックス
  6. 「強」「弱」は使わないほうがいいだろう。
  7. 「疑」は「タイト」と同義。
  8. 「2-関手」、「2-自然変換」などの'2-'に意味はない。次元を明示するだけ。
  9. 何をデフォルトにするかは不安定。明示されないと判断に苦しむ。
    1. 用法1: 厳密がデフォルト -- この用法は減る傾向だが、残っている。
    2. 用法2: タイトがデフォルト
    3. 用法3: ラックスがデフォルト
  10. デフォルトに頼らないで、明示的に形容詞を付けるのが望ましい。

*1:forvoで調べたら、スウェーデン人の名前のようです。

*2:アブラムスキー達が提唱した強コンパクト閉圏は、セリンガーの提案によりダガー・コンパクト閉圏に修正されました。

2018-01-17 (水)

TypeScriptのはなし : ユニオン型がけっこうイイね

| 11:47 | TypeScriptのはなし : ユニオン型がけっこうイイねを含むブックマーク

TypeScriptのはなし : サンプル記述に最良の言語」に続き、「ごめんねTypeScript」シリーズ第二弾。って、シリーズにするほどの話題があるか分からんけど、TypeScriptのいい点を紹介したり褒めたりする話です。

内容:

  1. TypeScriptのユニオン型はこんなに便利
  2. TypeScriptのユニオン型はこんなことも出来る: 有限集合型

TypeScriptのユニオン型はこんなに便利

型Xと型Yのユニオン型〈union type〉は、X | Y と書かれ、“ユニオン型 X | Y”の値としてXの値でもYの値でも許されます。縦棒'|'は、集合のユニオン(合併)演算子'∪'と解釈していいです。

まず、以前の記事(事実誤認あり)でも紹介した例をもう一度挙げます。

// ユーザーIDはユーザー名とユーザー番号の
// どちらもあり得る
type UserId = string | number;

// nullも許すstring型
type nullableString = string | null;

上記のnullableString型が意味を持つのは、stringにnullが入らないことが前提ですから、コンパイルオプションstrictNullChecksを付けてください(「TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった」参照)。

型パラメータも使えるので、nullableStringを次のようにも書けます。

// nullも許す型 一般
type nullable<X> = X | null;

// nullも許すstring型
type nullableString = nullable<string>;

ちょっと作為的だけど、こんなん(↓)も。

// なんかの限界値の設定に使う
// (リテラルは、その値だけを含むシングルトン型を表す)
type limit = number | "unlimited";

// 三値の真偽値
type TriValLogical = boolean | undefined;

次の例題として、ツリーのデータ構造(二進木にします)を考えてみましょう。ツリーのノードをオブジェクトで表すとして、次のようなコードを書くことが多いと思います。

// 注意! 単にNodeという名前にすると、DOMのNodeと
// 名前がかぶってしまう。
interface TreeNode {}

class Branch implements TreeNode {
  left: TreeNode;
  right: TreeNode;
  constructor(left: TreeNode, right: TreeNode) {
    this.left = left;
    this.right = right;
  }
}

class Leaf implements TreeNode {
  value: string;
  constructor(value: string) {
    this.value = value;
  }
}

var helloWorld : TreeNode = new Branch(new Leaf("Hello"), new Leaf("World"));
var greeting : TreeNode = new Branch(new Leaf("greeting"), helloWorld);

この書き方はいくつか鬱陶しいところがあります。

  1. 分岐ノード〈branch node〉と末端ノード〈leaf node〉を一律に扱うために、実質的意味がないインターフェイスTreeNodeを導入している。
  2. ノードが必ずTreeNode(を実装した)オブジェクトである必要があるため、末端ノードに生の文字列や数値を使えない。
  3. オブジェクト型に必ずnullが入ってしまう仕様だと(例えばJava)、空なツリーを認めるかどうかをプログラマがコントロール出来ない。

TypeScriptのユニオン型を使ってみます。

class Branch<T> {
  left: T | Branch<T>;
  right: T | Branch<T>;
  constructor(left: T | Branch<T>, right: T | Branch<T>) {
    this.left = left;
    this.right = right;
  }
}

type Tree<X> = void | X | Branch<X>;

var helloWorld : Tree<string> = new Branch<string>("Hello", "World");
var greeting : Tree<string> = new Branch<string>("greeting", helloWorld);

ユニオン型を使わないバージョンと比較してみると:

  1. インターフェイスTreeNodeのようなものは導入してない。分岐ノードも末端ノードも一様に扱うために、ユニオン型 T | Branch<T> を使う。
  2. 末端ノードは何でもよい。特定のインターフェイスを実装する必要もないし、オブジェクト型である必要さえない。
  3. 上記の例では、空なツリー(ノードをまったく持たないツリー)はvoidとして指定している。voidを入れなければ空なツリーは除外される。(voidを入れないほうが使いやすいと思いますが、例として入れてみました。)

また、ユニオン型使用バージョンでは最初から型パラメータを入れてますが、インターフェイス使用バージョンに型パラメータを入れること(ジェネリック化)は、ちょっと面倒でした。

interface TreeNode {
}

class Branch implements TreeNode {
  left: TreeNode;
  right: TreeNode;
  constructor(left: TreeNode, right: TreeNode) {
    this.left = left;
    this.right = right;
  }
}

class Leaf<T> implements TreeNode {
  value: T;
  constructor(value: T) {
    this.value = value;
  }
}

var helloWorld : TreeNode =
  new Branch(
    new Leaf<string>("Hello"),
    new Leaf<string>("World")
  );
var greeting : TreeNode =
  new Branch(new Leaf<string>("greeting"), helloWorld);

Leafにだけ型パラメータを入れました。これだと、var helloWorld : TreeNode<string>; のような型宣言(型注釈)が書けません。TreeNodeには型パラメータがないからです。TreeNodeに単純に型パラメータを追加するとコンパイルできず、結局次のようにしました。

interface TreeNode<T> {
  value?: T
}

class Branch<T> implements TreeNode<T> {
  value?: T;
  left: TreeNode<T>;
  right: TreeNode<T>;
  constructor(left: TreeNode<T>, right: TreeNode<T>) {
    this.left = left;
    this.right = right;
  }
}

class Leaf<T> implements TreeNode<T> {
  value: T;
  constructor(value: T) {
    this.value = value;
  }
}

var helloWorld : TreeNode<string> =
  new Branch<string>(
    new Leaf<string>("Hello"),
    new Leaf<string>("World")
  );
var greeting : TreeNode<string> =
  new Branch<string>(new Leaf<string>("greeting"), helloWorld);
  1. interface TreeNode<T> {} としたかったのですが、「型パラメータTを使ってない」と怒られます*1。しょうがないので、 value?: T を入れました。
  2. 分岐ノードTreeBranchに値を持たせる気はないので、 value?: T; は書きたくないのですが、「interface TreeNode<T> を満たしてない」と怒られます。
  3. value? という書き方は、「valueはあってもなくてもいい」という意味だから、実装クラス側で省略してもインターフェイスに違反してないと思うのだけど、「書け」とおっしゃる。でも、書いたら今度は、valueの存在を許すから、僕の意図(分岐ノードに値はない)と違う。

TypeScriptは、「ツリーのノード用にオブジェクトを定義することなんて面倒くさい」というモノグサ野郎(僕です)も面倒みてくれるでしょうか? 分岐ノードとして長さ2の配列を使って、配列要素で左右のサブツリーを表すことにします。

// ジェネリック版
// >>> コンパイルエラー
type SimpleTree<X> =  X | [SimpleTree<X>, SimpleTree<X>]

// 具体的な型(string)の版
// >>> コンパイルエラー
type SimpleStringTree = string | [SimpleStringTree, SimpleStringTree];

残念ながら、型パラメータがある無しに関わらず「循環参照はダメよ」と言ってコンパイルしてくれません。typeによる定義は、単に型の別名を定義する趣旨なので、ここはそんなに頑張んなくてもいいかも知れません。

しかし、このような循環的(再帰的)型定義が絶対に処理できないわけではありません。以前、Kuwataさんと、完璧じゃないけど実用上は問題ない程度の再帰的型定義は実装したことがあります。ココラヘンに名残があります。確か、完全に処理できるアルゴリズムもあったと思います。

TypeScriptのユニオン型はこんなことも出来る: 有限集合型

有限個の値からなる型は、通常は列挙型として定義します。

// 「はい・いいえ」の返答の値
enum YesNo {
  YES,
  NO
}

// 飲食店を、
// 星ナシから星五つのあいだで評価するときに使う
enum StarRating {
  Star0,
  Star1,
  Star2,
  Star3,
  Star4,
  Star5
}

TypeScriptの列挙型は、型ごとに名前空間を持つ*2ので、その値は YesNo.NO とか StarRating.Start3 とか書きます。StarRating.3 という値を定義したり書けたりすると便利だな、と思うのですが、それは出来ません。

TypeScriptはモノグサ野郎にやさしい仕様で、次のようにしても有限集合型を定義できます*3

type YesNo = "Yes" | "No";

type StarRating = 0 | 1 | 2 | 3 | 4 | 5;

列挙型のメリットのひとつは、switch文に余分なcaseが入ってないかコンパイラがチェックしてくれる点です。例えば、次の関数は case 6: のエラーが指摘されます。

function showRating(r : StarRating) : void {
  switch (r) {
  case 0:
    console.log("no rank"); break;
  case 1:
    console.log("one star rank"); break;
  case 2:
    console.log("two star rank"); break;
  case 3:
    console.log("three star rank"); break;
  case 4:
    console.log("four star rank"); break;
  case 5:
    console.log("five star rank"); break;
  case 6: // コンパイルエラー
    console.log("six star rank"); break;
  }
}

列挙型でもユニオンによる有限集合型でも、「漏れなく」はチェックしてくれないようです。漏れじゃなくて意図的な省略もあるのでエラーにはできないでしょう。でも、defaultがなくて、caseが抜けている場合って、たいていはプログラマのミスでしょうから警告して欲しいのですが。

[追記]「漏れ」のチェックは出来ます。次のようなdefaultを書きます。

  switch (r) {
  // 省略
  default:
    const _exhaustiveCheck: never = r;
  }

列挙した残りの値の集合が空集合だというセマンティクスだけど… ウーン、しかし、これは技巧的に過ぎるよな。手でこんなん書かなくても、コンパイルオプションかなんかで漏れを検出して欲しい。[/追記]

ユニオン型(バリアント型とも呼ぶ)が巷で積極的に推奨されない理由として、型による制約がユニオン型でゆるくなったり、制約逃れの手段にユニオン型が使われるリスクがあります*4。設計がまずいせいで、ユニオン型を多用せざるを得ない、なんてこともあります。

なので、ちょっと良いか悪いか分からんのですが、次のようなこともできます。

enum Judge {
  YES,
  NO
}

type YesNo = "Yes" | "No";

// 二値の返答が色々あるんだよなー
type Answer = boolean | Judge | YesNo;

function replyToAnswer(a : Answer) : void {
  // 色々ある値を分類して処理する
  switch(a) {
  case true:
  case Judge.YES:
  case "Yes":
    console.log("Thank you!");
    break;
  case false:
  case Judge.NO:
  case "No":
    console.log("It's a pity.");
    break;
  }
}

色々ゴチャゴチャあるのを何でもいいから混ぜちゃえ、と事後対策としてユニオン型を使うのは好ましくありませんが、事前にちゃんと考えてユニオン型を使うなら、便利で役に立ってくれます。

*1:ちょっと厳しすぎる感じなので、なんらかの手段で緩和できるのか?

*2:const enumは実行時の名前空間を持ちません。

*3:既存の型の部分集合型は、たとえ有限集合であっても扱いが面倒になるので、型システムの実装者には嫌われる傾向があります。既存型の有限集合型をサポートする判断は、実用性・利便性を重視してのことなのでしょう。こういう判断をするところも僕は好きです。

*4:悪用されなくても、そもそも型が複雑になるので嫌だ、ということもあるでしょう。

2018-01-16 (火)

離散集合ってなに?

| 10:23 | 離散集合ってなに?を含むブックマーク

N君に「で、離散集合ってなんですか?」と聞かれて、どう答えていいか困ってしまいました。

対話

N君 :「実数の全体は連続集合ですよね」
檜山:「そうだね」
N君 :「自然数の全体は離散集合ですよね」
檜山:「うん、そうだね」
N君 :「有限集合は離散集合ですよね」
檜山:「はい、そうだね」
N君 :「つまり、可算集合は離散集合ですよね」
檜山:「ん? いやっ、… あれ?」

連続と離散

「連続集合」はたまに使う言葉ですが、その意味はあんまりハッキリしません。R(実数の全体)の基数(濃度)を連続濃度と呼ぶので、Rと同じ基数を持つ集合を連続集合と呼んでいるのではないかと思います。この用法だと、「連続」とはいいながら、位相とは何の関係もなくて、単に集合を基数で分類・特徴づけしているだけです。

歴史や語源を僕は知りませんが、たぶん(たぶんです)、RRn、その部分集合などを連続体と呼んでいたことから、形容詞「連続」が「連続体と同等の」という意味で使われたのでしょう。

一方の「離散集合」ですが、これは集合の基数による分類・特徴づけとは関係ないように思えます。形容詞「離散」が「自然数(またはその部分集合)と同等の」という意味で使われている気がしないのです。もちろん、言葉の使用・運用は多様なので、「離散=可算」の用例が絶対ないとは断言できませんが。

離散集合は、集合の話ではなくて、位相の文脈で使われる言葉でしょう(多くの場合は)。つまり、離散集合は離散位相空間と同義だと思われます。

「連続」と「離散」は、対になる言葉としてよく一緒に使われますが、「連続集合←→離散集合」に関しては、対としての対称性はないようです。

離散空間としての離散集合

位相空間Xが離散であることの定義は簡単で、Xのすべての部分集合が開集合になることです。連続集合であるRを離散空間にすることもできます。位相空間Xの部分集合Aが離散集合であるとは、Xの位相から誘導されたAの位相(相対位相)により、Aが離散であることです。

上記のような定義を採用すると、「有限集合は離散集合である」もあやしくなります。集合{0, 1}の開集合族を{{}, {0, 1}}と決めると、({0, 1}, {{}, {0, 1}})は離散空間にはなりません。「有限集合を台とする位相空間は離散空間である」は正しくないのです。とはいえ、我々が有限集合に想定する位相は離散位相なのだとは思います。

自然数の全体は離散集合」も同様な事情で、我々がNに暗黙に想定する位相が離散位相なのでしょう。典型的には、Rに普通の位相(詳細略)を考えて、NR からの相対位相は離散位相です。

可算集合は離散集合」と言われれると「あれ?」となるのは、この言い回しは「可算集合の上に載る位相構造は離散である」と解釈できるからです。こうなると正しくない。Rの普通の位相と QR から誘導されるQの位相は離散位相ではありません。

言葉の国語辞書的な意味や語感・印象に基いて話していると、「あれ?」な状況(アレな状況)になったりしますね。

sasa2718sasa2718 2018/01/16 10:48 自然数は順序を持ち、それが誘導する位相が離散位相になります。だから自然数は離散だと言われても私には違和感はないのですが、これが普通かと言われると全く自信がありませんね

m-hiyamam-hiyama 2018/01/16 14:51 sasa2718さん、
> 自然数は離散だと言われても私には違和感はないのですが、
僕も全然違和感ないです。多くの人が「自然数は離散だ」は納得すると思います。
自然数には、何らかの構造が暗黙に仮定されるのでしょう。
それに対して可算集合は構造が抜けるので、「可算集合は離散だ」は変な感じがするのかと。

sasa2718sasa2718 2018/01/20 10:15 可算集合に対しては何も構造がないのだから自己全単射で不変から、離散、密着、フレシェ位相以外は脱落しますが、これが普通かと言われるとやはり全く自信がありません

m-hiyamam-hiyama 2018/01/20 12:00 sasa2718さん、
なるほど。普通じゃないと思います。

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

2018-01-15 (月)

TypeScriptのはなし : サンプル記述に最良の言語

| 11:28 | TypeScriptのはなし : サンプル記述に最良の言語を含むブックマーク

先週の金曜(2018-01-12)に、「TypeScript、お前もか: nullやundefinedの扱いがイイカゲン過ぎ」という記事(後にタイトルに「【事実誤認あり】」を追加)を書いたのですが、ほぼ言いがかりでした。謝罪と修正は「TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった」に書いてあります。

申し訳ないことをしたので、TypeScriptに関してポジティブな話を書きます。そもそも僕はTypeScript好きなんですよ。文句を付けた記事の書き出しは、

  • TypeScriptには期待してたんだけど、ガッカリだよ。

ですが、第二の文は、

  • それでもまー、割と好きだけど。

本文中にも、

  • nullやundefinedに関しても、整合的で安全なセマンティクスをかぶせているだろう、と。「期待していた」というより、思い込んでいた、信じていたのです。

と、信頼を寄せていた心情が伝わるでしょ。早とちりで「信じていたのに裏切られた」と誤解してカッとなったのですけど。

さて、TypeScriptはJavaScript+αなのですが、もとが極めてポピュラーなJavaScriptであって、+αの機能も持っていることから、現状において、サンプルコードを書くには最良の言語だと思います。

僕は、かなり昔から「サンプルコードはJavaScriptで書こう」と決めていました。2006年1月21日に書いた次の短い記事でそう表明しています。

当時の状況も書いてあったりして、懐かしい気分になります。

実を言えば、このあいだまでJavaScriptは「なんかトンデモない言語仕様の、ひどく貧弱な言語」-- みにくいアヒルの子と捉えていたのですが、りっぱな白鳥に、でも灰色の斑点が少し残った白鳥に成長しそうですね。

という見通しはだいたい当たったようです。

「サンプルをJavaScriptで書こう」と決めた第一の理由は、「誰でもどこでも使える」ことです。サンプルを試してみるのに、処理系のインストールやセットアップは不要です。ブラウザさえあればOK、最近のメジャーブラウザは[F12]でJavaScriptコンソールが使えます。そして、言語仕様も多くの人が知るところです。

JavaScriptは、無節操な(よく言えばマルチパラダイムな)言語なので、他の言語の書き方を真似しやすいのもいいですね。どんなスタイルのコードを書いても「JavaScriptはカクカクシカジカだから、その書き方はよくない」なんて話は(滅多に)出ません、もとが無節操だから。

ただ、型が書けないのはやはり辛い。例えば、

function isEmptyString(s) {
  return s.length == 0;
}

この例では、関数名が「引数は文字列だ」と強く暗示してますが、もっと素っ気なく、

function e(s) {
  return s.length == 0;
}

これだと、「引数は文字列だ」は伝わりにくいでしょう。ドキュメンテーションと型チェックを入れるなら、

function e(s/* string */) /* returns boolean */{
  if (typeof s != 'string' && !(s instanceof String)) {
    throw "Bad Arg";
  }
  return s.length == 0;
}

なんだか、みにくくなってしまいます。

TypeScriptなら、

function e(s : string) : boolean {
  return s.length == 0;
}

スッキリ書けます。

ただし、TypeScript言語処理系のインストールが必要なので、「誰でもどこでも使える」メリットは失われてしまいます。これはトレードオフなので致し方ないですけど。救いはインストールが比較的簡単なことです。node.jsとnpmのエコシステムはよく整備されていて、node.jsさえインストールしてしまえば、TypeScriptや関連ツール/ライブラリはnpm(最近ならyarnか)でインストールできます。

型がないと、説明とサンプルを書くことが困難なことがあります。2008年1月16日に書いた記事「CPS(継続渡し方式)変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ」では、型パラメータが必要でした。この記事の第1節「未来のJavaScript」で、次のようなコードが書ける疑似言語を仮定しています。

function<X, Y>
makePair(first:X, second:Y):Array2<X, Y> {
  return [first, second];
}

架空の言語の代わりに、実在するTypeScriptを使って型パラメータを使った話題を書けるようになりました。

JavaScriptだけで済む話なら、「誰でもどこでも使える」JavaScriptが望ましいでしょう。ですが、型が必須の話題/サンプルはTypeScriptを使うのが現状では最善だと思います。