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

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

2018-09-21 (金)

昭和歌謡の歌詞、今ならアウトだろう

| 16:47 | 昭和歌謡の歌詞、今ならアウトだろうを含むブックマーク

居酒屋のランチを食べていたら、懐かしの昭和歌謡が流れていたのですが、その歌詞が、今はもう「ダメだろ、これは」としか思えない。とはいえ、当時は大ヒットしたのだし、作詞は時代を代表する作詞家。

世の価値観が変わった、ということなんですね。

この二曲、詞の雰囲気が似てる。

  • [A] だからいつもそばにおいてね、邪魔しないから。
  • [B] あなたの決してお邪魔はしないから、おそばに置いてほしいのよ。
  • [A] 悪いときはどうぞぶってね
  • [B] 私に悪いところがあるのなら、教えてきっと直すから。

ウワーーーッ。

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

2018-09-20 (木)

告知:9月29日に「ゲーデルの不完全性定理」無料ガイダンス回

| 15:42 | 告知:9月29日に「ゲーデルの不完全性定理」無料ガイダンス回を含むブックマーク

2009年に3回続きのセミナーをやったことがあります。そのタイトルは「ラムダ計算、論理、圏」で、メインの話題はカリー/ハワード対応でした。が、他の話もあって、「プログラムの停止性判定の不可能性」も入れていました。

「プログラムの停止性判定の不可能性」は、主題ではなかったので急ぎ足でしたが一応の説明をした記憶があります。その当時の記録は:

「プログラムの停止性判定の不可能性」は、「ゲーデルの不完全性定理」の仲間です。どちらも、メタレベルから分析することにより、ある種のアルゴリズムの非存在を主張するものです。

セミナーよりさらに3年前の2006年に、一連のブログ記事として「ゲーデルの不完全性定理」を扱ったこともあります。

セミナーから10年近く、ブログ記事からは10年以上が経過したわけですが、ものすごく久々にこのネタで話をします。割と長いシリーズ(全6回)のセミナーがあるのですが、そのガイダンス回を9月29日に行います。ガイダンス回(第0回)は無料なので、お時間の都合のつく方は是非にお越しくださいませ。

次のページから申し込みできます。

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

2018-09-19 (水)

デカルト構造の無限タワー: 怖がらずに登れ

| 13:01 | デカルト構造の無限タワー: 怖がらずに登れを含むブックマーク

マイクロコスモ原理と構造の無限タワー」に、yamさんからコメントをいただきました。yamさんの疑問(モヤモヤ)は、少し前に僕が持っていた疑問(モヤモヤ)とたぶん同種のものでしょう。その疑問(モヤモヤ)は、「もう、無限に続くタワーを登るしかないんだな」と僕が覚悟を決めた動機のひとつでした。

順序対(ペア) (a, b) はどっから来るのでしょう? その起源、故郷はどこにあるのでしょうか? -- これがその疑問(モヤモヤ)です。順序対(ペア)は無限の彼方、天空の世界からやって来ると考えざるを得ず、順序対(ペア)の故郷を訪ねるには、デカルト構造の無限タワーを登るしかないようです。(下の絵はタワーじゃなくて豆の木)

*1

内容:

  1. 記法の変更と追加
  2. デカルト構造
  3. 二項演算とペアリング
  4. おわりに

記法の変更と追加

マイクロコスモ原理と構造の無限タワー」と記法を少し変えます。それについては、メモ編の次の記事に書きました。

太字や下線などの装飾を使うのが辛い(欠点もある)ので、ダッシュ(プライム、シングルクォートで代用)を使うことにしたのが大きな変更点*2。例えば、Y(U, U) は Y'(U, U) とします。それと、単位対象(0-射)と単位射(1-射)を区別します。

  • 単位対象は1(イチ)と書く。とある圏Cに注目してるなら、1∈|C|。
  • 単位射はi(小文字アイ)と書く。i:1'→C なので、iはCの外にある射。

さらにいくつかの約束をここで追加します。

中置演算子記号を前置演算子記号(関数記号)にしたいときは、Haskellのセクション記法と同様に丸括弧で囲みます。例えば、掛け算 a×b は (×)(a, b) とも書きます。僕は、(×)をしばしばYと書いてました。Yを使う理由は「モノイドやモノイド圏の指標 補足解説」に書いています。

n-圏の結合〈composition〉はイッパイあり得ますが、それらを一律に「#」で表すことは「マイクロコスモ原理と構造の無限タワー」でやりました。このとき、上下の添字(#nk の n, k)は省略することがあります。自然変換(成分表示)の下添字も明らかなら省略することがあります。省略は好ましくないけど、簡潔さのため(めんどうだしさぁ)。

なにか対象A(アトムかも知れないし、集合かも知れないし、圏かも知れないし、関手かも知れないし、2-圏かも知れないし、…)があるとき、その恒等を一律にA^と書きます。これはDOTNの流儀です。AとA^を同一視してしまう流儀もあります -- 簡潔だけどちょっと分かりにくいので採用しません。

デカルト構造

小さいデカルト圏 C = (C, ×, 1, α, λ, ρ) を考えます。圏論的直積がデカルト・モノイド積×で与えられます。デカルト・モノイド積の単位対象1は、Cの終対象になっています。α, λ, ρ は、モノイド圏としての律子(律子に関しては「律子からカタストロフへ」を参照)です。

デカルト圏Cのデカルト・モノイド積×のプロファイルは:

  • (×):C×CC in Cat

んっ? … オイオイオイオイ、C×C の×って何だよ? -- これは2-圏Catに備わったデカルト・モノイド積です。Catは単なる2-圏ではなくて、デカルト2-圏だったのです。Cの構造の一部である×とCatの構造の一部である×を区別するにはダッシュ記法(「モノイドやモノイド圏の指標 補足解説」参照)を使います。

  • (×):C×'CC in Cat
  • (×'):Cat×''CatCat in 2-CAT

2-CATは、必ずしも小さくない2-圏からなる3-圏とします。2階層分だけ書きましたが、(×''), (×'''), (×''''), ... の定義は無限に続きます。この無限性から逃れようがないです。でも、安定するなら平気です。

ここであやしいことを口走りますが; 「安定するなら平気」と思うことが、無基底・無限階層の世界における「悟り」なんだと思います。無限性を拒絶せずに受け入れるのです。

デカルト圏に話を戻します; デカルト圏は単なるモノイド圏以上のものです。デカルト構造を記述するには、モノイド構造に対し、さらに構成素を付け加える必要があります。追加の構成素は、終射 !、射影 π1, π2、対角 δ です。集合圏は小さな圏ではないですが、説明のために集合圏で言えば:

  • !A:A→単元集合 は、単元集合への唯一の写像
  • 1)A,B:A×B→A は、第一射影の写像
  • 2)A,B:A×B→B は、第ニ射影の写像
  • δA:A→A×A は、a|→(a, a) という写像

!, π1, π2, δ は自然変換ですが、そのプロファイルは、2-圏Catのなかで次のように書けます。

  • ! :: C^⇒!'C#i : CC in Cat (i:1'→C in Cat
  • π1 :: (×)⇒(π'1)C,C : C×'CC in Cat
  • π2 :: (×)⇒(π'2)C,C : C×'CC in Cat
  • δ :: C^⇒δ'C#(×) : CC in Cat

ここで:

  • !' :: Cat^⇒!''Cat#i' : CatCat in 2-CAT (i':1''→Cat in 2-CAT
  • π'1 :: (×')⇒(π''1)Cat,Cat : Cat×''CatCat in 2-CAT
  • π'2 :: (×')⇒(π''2)Cat,Cat : Cat×''CatCat in 2-CAT
  • δ' :: Cat^⇒δ''Cat#(×') : CatCat in 2-CAT

デカルト圏Cをホストする2-圏であるCatがデカルト圏であり、×', 1', α', λ', ρ', !', π'1, π'2, δ' を備えているのです。そのデカルト圏Catをホストする3-圏である2-CATもまたデカルト圏の構造(×''など)を持つのです。

「デカルト圏をホストする(より高次の)圏はデカルト圏である」というマイクロコスモ原理は無限に適用できるので、デカルト構造という構造は(上方)無限タワーを形成し、この無限タワーを通してしかデカルト構造の包括的理解は得られません

幸いにも、デカルト構造の無限タワーは安定し、Catより上の次元(階層)では同じことの繰り返しになります。構造をホストする環境の次元はどんどん上がりますが、その環境の2-構造(0射, 1射, 2射 までの構造)しか関与しないので、神ならぬ我々でも無限の彼方まで見通すことができます。それが「安定する」の意味です。

無限タワーを恐れず、積極的に登ろうという気分を盛り上げるには、「高次圏: 無基底・無限階層 補足」、特にスザウィールの言葉を参照。

二項演算とペアリング

二項演算とペアリング(ペアを作る操作)は密接に関連しています。この二者の相関が、ジグザグ状の軌跡を描いて無限タワーを登っていくことになります。その様子を見てみましょう。

なんかの二項演算の中置演算子記号を・とします。a, b に対して a・b を考えることができます。とある範囲Aのなかでしか a・b は定義できないでしょう。つまり、a∈A, b∈A に対して(のみ)、a・b ∈A が定義される。

記号・を前置演算子記号(関数記号)に変更すると、a・b は (・)(a, b) と書けます。これはまた、ペア (a, b) を関数 (・) に入れた (・)((a, b)) とみなされて、次のプロファイルを得ます。

  • (・):A×A→A

集合の直積記号×は中置演算子記号です。集合 A, B に対して、A×B を考えることができます。直積といえども、とある範囲C(多くの場合はSet)でしか A×B は定義できないでしょう。つまり、A∈0C, B∈0C に対して(のみ)、A×B ∈0C が定義される。x∈0Y は、x∈|Y| と同じ意味です。

記号×を前置演算子記号(関数記号)に変更すると、A×B は (×)(A, B) と書けます。これはまた、ペア (A, B) を(二項)関手 (×) に入れた (×)((A, B)) とみなされて、次のプロファイルを得ます。

  • (×):C×'CC

圏の直積記号×'は中置演算子記号です。圏 C, D に対して、…[以下省略]…

今述べたような文面は、いつまでもいつまでも続くのです。しかし、「同じことを言ってるだけじゃないか」となります。無限に続くが循環する、安定するのです。循環も含めてデカルト構造の無限タワーを構成します。

ここで重要な注意は、これぞデカルト構造の無限タワー〈The infinite tower of cartesian structures〉と呼べるモノは特にないことです。集合圏以外にデカルト圏はいくらでもあります。ひとつ選んだデカルト圏をホストする“より高次の圏”もいくらでもあります。いくらでもある選択肢の無限階層があり、そのなかから我々は目的や好みに応じてひとつの無限タワーを選ぶだけです。無限タワーが無限にあり、特別な基底はなく、それらは相互依存しています。

おわりに

デカルト構造の無限タワーは安定します。安定するので、ある階層から先は同じことの繰り返しになります。別な言い方をすると、指標と等式的法則により、あからさま〈explicitly〉に循環定義を書き下せるってことです。

循環定義を書き下す作業は、やれば出来ることですが自明ではありません。記法・図法の工夫をしないと、なかなかうまく書き下せないですし、意外に量があるんですよね。僕が見た範囲では、デカルト構造のキチンとした循環定義は公開されてないようです。内容的には“当たり前のことの再確認”なので、誰もやりたがらない作業なのかな? できれば、デカルト構造の全貌(=無限タワーの総体)を晒したいと思っています。

*1:画像: https://fanart.tv/movie/81005/jack-the-giant-slayer/ 映画『ジャックと天空の巨人』

*2:手書きのときは、オーバーラインがいいかも知れません。オーバーラインなら、2本、3本重ねることが出来て、比較的に視認性もいいですから。

yamyam 2018/09/21 01:30 記事読ませていただきました。
簡単に表すと
(a:A, b:B) : A × B
(A:A', B:B') : A' ×' B'
...
という関係があるのですね。
そうすると、pairing自体は二項演算ではなくメタ構文ってことでしょうか。

m-hiyamam-hiyama 2018/09/21 14:54 yamさん、
> という関係があるのですね。
そういう理解でいいと思います。

> そうすると、pairing自体は二項演算ではなくメタ構文ってことでしょうか。
ペアリングはデカルト構造なしには出来ないことであり、そのデカルト構造は無限階層を構成しています。
すべての階層において、×, 1, ( , ), 射影, 対角 などが準備されています。
これらの記号はすべて、次元でインデックスされて区別されると思ってください。
特定の階層に注目して、そこでの記号はインデックスなしとした場合、1つ上の階層の記号にはダッシュを1つ付ける約束にしました。
ダッシュが付いた記号は、注目している階層の1つ上、つまりメタレベルから来るものです。ただし、記号をどの階層に所属させるかの揺らぎ(恣意性)はあります。

( , ) という記号の解釈は、以下のように考えるといいと思います。

(C, 1, ×, δ, その他) はある階層のデカルト構造。A, B∈|C|, a∈|A|, b∈|B| (a, bはCから見て2階層下の存在) (a, b) ∈ |A×B|
このとき、

δ_1#(a~×b~) = (a, b)~ : 1→A×B in C

a~などは格上げです。「格上げ」はブログ内検索してみてください。
格上げが使えれば、Cに備わる ×, 1, δ, #(射の結合) により ( , ) は特徴付けられます。
したがって、( , ) をプリミティブと考える必要はありません。
より高次の射のペアも、同様な解釈が出来ます。

yamyam 2018/09/22 01:53 コメントありがとうございます。
それと、言葉が足りなかったみたいで基本的な説明をさせてしまってすみません。

> δ_1#(a~×b~) = (a, b)~ : 1→A×B in C
登場する記号の定義を擬似Haskellで書き出してみたのですが、まだ納得いきません。
疑問に思った部分を説明してみますね。
(a, b) :: A × B
これはいいですね。前置にするため、仮にカリー化と部分適用を認めてみます。
(,) a b :: A × B
(×):(C×C)→C in Catなので、本当は1引数C×Cを取るはずです。よって、
(,) :: A ×' B -> A × B
として部分適用を取り除くことができ、
(,) (a,b)' :: A × B
と書けそうです。新しいペアリングを前置にすると、
(,) ( (,)' a b ) :: A × B
(,)' :: A ×'' B -> A ×' B
同様に、
(,) ((,)' ((,)'' a b)) :: A × B
(,)'' :: A ×''' B -> A ×'' B
無限回の繰り返しを認めると、
lim(n->inf) (,) (... ((,)^n' a b) ...) :: A × B
(,)^n' :: A -> B -> A ×^n' B
どうしても部分適用がなくならないので、モヤモヤしています。
書いてみて思ったのですが、これは無限タワーとは別の問題かもしれないですね。

m-hiyamam-hiyama 2018/09/22 10:11 yamさん、
内容的な話は連休明けにでもお応えするとして、ちょっとした指摘だけ。

> これは無限タワーとは別の問題かもしれないですね。
いや、まさに無限タワーの問題です。なぜなら、
> モヤモヤしています。
このテのモヤモヤを解消するには、無限タワーを考えたほうがいいぞ、必要があれば上の階層に登っていこう、と言っているわけなんで。

> (×):(C×C)→C in Catなので、本当は1引数C×Cを取るはずです。よって、
> (,) :: A ×’ B -> A × B
> として部分適用を取り除くことができ、
> (,) (a,b)’ :: A × B
このへんが、外(上の階層)に出ないで、同じ階層内で処理しようとしているように思えます。
外に出ないと、ホントに解決できないダメな循環定義になります。
僕が言っている(良い)循環定義は、実際はタワーをどんどん上に登るものです。
http://d.hatena.ne.jp/m-hiyama/20180913/1536819898 :
article> 無限の彼方に基礎があります。あるいは、無限の彼方に向かって歩み続ける行為そのものが基礎なのかも知れません。

それと、
hiyama> ( , ) をプリミティブと考える必要はありません。
と言いましたが、( , )は単なる略記、構文マクロのようなものです。
構文マクロなんで、( , )自体をプロファイル(型付け)するのは無理があります。
プロファイル可能な実体としては、δ_1#(a~×b~) を考えたほうがいい、ということです。

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

2018-09-17 (月)

高次圏: 無基底・無限階層の世界とn-圏

| 10:05 | 高次圏: 無基底・無限階層の世界とn-圏を含むブックマーク

思想的/哲学的な話をするなんてことはまったくなくて、n-圏〈高次圏〉の捉え方と使い方に関する技術的な話の背景を非技術的に語ろう、ということです。

内容:

  1. 中観派アプローチ?
  2. 無限階層性
  3. 無基底性の不安をどうやって解消するか
  4. で、何が嬉しいのか

[追記]2つの補足記事があります。どちらも同日の記事なので、本日の記事全体で3つの記事をまとめて読めます。→ 2018-09-17 (月) [/追記]

中観派アプローチ?

大乗仏教中観派と一般モデル理論」で、ラズヴァン・ダイアコネスク〈Răzvan Diaconescu〉のエッセイ「インスティチューション、中観派、一般モデル理論〈Institutions, Madhyamaka, and Universal Model Theory〉」を紹介しました。中観派〈ちゅうがんは〉は大乗仏教の学派です。

ダイアコネスクは、中観派思想を熱心に勉強した上で、それがインスティチューション/一般モデル理論/圏論などと同じ発想だと言っています。でも僕は、仏教は何も知らない(勉強する気もない)ので、ほんとのところ「同じ発想」かどうかは分かりません。確信がないので、記事タイトルに「中観派」は入れませんでしたが、ダイアコネスク論文から想像するに、僕がこの記事で言いたいことも中観派のアプローチに近いのでは? と思ってます。

ダイアコネスクからの受け売りで言えば、中観派の特徴は非本質〈non-essential〉とか無基底〈groundless〉とかのキーワードで表わされるようです。でも、non-essential, groundless を辞書で引くと、「不必要なもの」「事実無根」と、いい意味の言葉じゃないようです。groundless, baseless, unfounded などは、どうも誤解を招きそうな言葉なので、無基底であることは ground-fee がいいかも。

ここで言ってる基底〈ground, base, basis, foundation〉とは、「それ自身で絶対的に信頼できるモノ・コト」といった意味です。ベクトル空間の基底とかではないです。(おそらく)中観派によれば、基底なんてありゃしない、と*1。その代わり、すべてのモノ・コトは相互依存〈interdependent〉しているので、関連性はあるよ、ってことでしょう。

それと、中観派思想かどうか分かりませんが、手塚治虫が『火の鳥』で描いていたような、「世界は無限階層の構造を持ち、それぞれの階層は別物だが類似している」という世界観がありますよね。

フラクタルのように、相似変換で重なるってもんでもない。似てはいるけれど、階層ごとの個性のようなものもある、というような ……

[追記]今僕の手元には『火の鳥』は一冊もなくて、おぼろげな記憶だけです。検索で調べてみたら、火の鳥が無限階層の世界を語るのは『第2部 未来編』のようです。『未来編』の主人公・山之辺マサトが、ミクロの世界から宇宙の外側までを旅する(夢をみる?)シーンがあるので、それが僕の記憶に残っているのでしょう。特定の仏教思想とかではなくて、手塚治虫自身の世界観なのだと思います。手塚治虫が仏教の影響を受けている可能性はあるでしょうが。[/追記]

とまー、ダイアコネスクからの受け売り、手塚治虫からの受け売りをボンヤリ並べているわけですが、ここで出てきたキーワード、無基底性、相互依存性、無限階層性などは、n-圏(高次圏)を考える上でも重要だと思うのです。

無限階層性

最近の記事「マイクロコスモ原理と構造の無限タワー」で、モノイドという構造・概念は、無限階層の世界における無限タワーとして定義されること(のアウトライン)を示しました。これはモノイドに限ったことではないでしょう。つまり:

  • すべての構造・概念は、無限階層のなかの無限タワーとして現れる。

なんらかの構造・概念、例えば「集合」という構造・概念に対して、それに1という番号を付けて1-集合と呼んでみます。すると、1-集合以外に2-集合、3-集合がありそうな気がしてきます。あるいは、0-集合、(-1)-集合、(-2)-集合もあるかも知れません。それらが、集合概念のトータルな姿を表すのでしょう。

  • 集合: ..., (-2)-集合, (-1)-集合, 0-集合, 1-集合, 2-集合, 3-集合, ...

我々にお馴染みなのは1-集合です。その1-集合に対して、別な系列が存在する可能性も否定できません。

  • 集合': ..., (-2)-集合', (-1)-集合', 0-集合', 1-集合' = 1-集合, 2-集合', 3-集合', ...

現状における理解では、次のようなn-集合(n = ..., -2, -1, 0, 1, 2, 3, ...)があると思われています(「ファンタジー: (-1)次元の圏と論理」参照)。

n n-集合
-2
-1
0 真偽値
1 集合
2
3 2-圏

「集合概念を表す系列はこれに限る」と言い切ってしまうと、「絶対的に信頼できるモノ・コト」を導入してしまうので無基底でなくなります*2あくまで一例としてのトータルな集合概念です。

無基底性の不安をどうやって解消するか

無限階層〈infinite hierarchy〉の世界観のなかで無基底性を考えると、

  1. 水平方向の無基底性
  2. 垂直方向の無基底性

に分類されるでしょう。

特定の階層を考えたとき、その階層内で「これが基底だ/本質だ」といえるモノなどない -- こう主張するのが水平方向の無基底性です。一方、どこかの階層を特定して、それが基底層だとはいえない -- こう主張するのが垂直方向の無基底性です。

これらの無基底性は、何も信用できないような不安、自分が立っている足元もいつ崩れ落ちるか分からないような不安を与えます。これは、僕がマイクロコスモ原理に感じた不安感です。

水平方向にも垂直方向にも無基底な無限階層の世界でも、次の事実はあります。

  1. 絶対的基底はなくても、典型的事例はある。
  2. 無限に階層が続いても、具体的に構成可能な無限タワーがある。

「これが唯一の基底だ」とは主張できなくても、世界のなかのモノ・コトを「馴染み深い」「扱いやすい」という理由で選択することはできます。無基底だということは、多様性が認められることであり、その多様さのなかから選ぶ自由もあります。

前節のn-集合の例でも、真偽値Bool、集合圏Set、圏の圏Catなどは、「馴染み深く扱いやすい」という理由で選んでいるといえます。それ以上の大義名分は要りません。

もし「すべての構造・概念は、無限階層のなかの無限タワーとして現れる」なら、そのなかには得体の知れない無限タワーもあるでしょう。「高次圏: 複雑さの2つの方向と半厳密性」で言及した、もっとも弱い定義のn-圏の系列wn-Catは得体の知れない無限タワーです。しかし、ストリクトなn-圏の系列sn-Catは下から順に帰納的に構成可能な無限タワーです。n-モノイドの系列(「マイクロコスモ原理と構造の無限タワー」参照)も、途中で安定するので具体的に構成可能な無限タワーと言っていいでしょう。

要するに、わけわからんモノが無限にあるけど、チャンと分かっていて具体的に触れるモノも確かにあるから、それらを手がかりにすればいいんじゃない、ってことです。

で、何が嬉しいのか

無限階層を認め、基底に頼らない考え方のメリットは何か?

まず、無限階層性と無基底性により、視野が固定されることがなくなり、モノゴトの共通性・類似性を観測しやすくなります。n-モノイド、n-集合を挙げましたが、他のn-ナントカを考えると、個々のn(次元、階層のレベル)によらない構造やnが変わったときの変化が見えてきたりします。

最近気付いた例を述べると; 要素/ベクトル/点は、それぞれ集合/ベクトル空間/位相空間の“インスタンス”と言えるでしょう。単に“インスタンス”ではなくて、“1-インスタンス”と呼んでみましょう。そうすると、1-インスタンスが所属する集合/ベクトル空間/位相空間は“1-クラス”(あるいは“1-タイプ”)と言えます。1を2に増やして、2-インスタンスと2-クラスは何でしょうか? しばらく考えると、2-インスタンスは既に様々な呼び名をされていることに気付きます: モデル、代数、加群、表現など。一方で、2-クラスにはこれといった呼び名がないようです。この状況を一般化すれば、n-インスタンスとn-クラスの関係を議論できます。このことは、意図的に無限タワーを作ってみて(少しだけ)分かったことです。

すべての構造・概念を無限タワー化するのは非常な労力がかかるので、すぐに出来るようなことではありませんが、目ぼしい構造・概念を無限タワー化するだけでも、世界の見え方がだいぶ変わります。具体例を挙げないとピンと来ないと思いますが、事例はいずれそのうち。

高次圏: 無基底・無限階層 補足

| 15:41 | 高次圏: 無基底・無限階層 補足を含むブックマーク

本日(世間は振替休日*3)の「高次圏: 無基底・無限階層の世界とn-圏」に少し補足; 無基底・無限階層の発想(なんかいい呼び名がないかな?)の適用事例として、ドクトリン(ハイパードクトリンとは違う)なんかいいんでないかな。ドクトリン〈doctrine〉ってなんかよく分からん概念だけど、あれは無限タワーで理解できるかも。

最近気付いた例を述べると; ...[snip]... この状況を一般化すれば、n-インスタンスとn-クラスの関係を議論できます。このことは、意図的に無限タワーを作ってみて(少しだけ)分かったことです。

これはドクトリンを無限タワーで理解しようとした話なんです。少ししか分かってないけど。

とりあえず、ドクトリンのnLab項目をみてみましょう。

ドクトリンはセオリーの2次元(圏化)版で“2-セオリー”と呼ぶべきものだと書かれています。「ドクトリン=1-ドクトリン=2セオリー」「セオリー=1-セオリー=0-ドクトリン」です。セオリー=1-セオリーは、2-圏とみなしたドクトリン=2-セオリーの対象なのだと説明した後で:

one can also imagine considering 2-theories as objects of some 3-theory, and so on. (Unfortunately this approach involves us in an infinite regress when we look for a formal definition!)


次にように夢想する人がいるかもしれない; 2-セオリーは3-セオリーの対象だとみなせるだろう、そして3-セオリーは4-セオリーの…… などなど。(残念ながら、この発想を形式的定義として厳密化しようと試みると、我々は無限後退に巻き込まれてしまう。)

「残念ながら〈Unfortunately〉」とか「無限後退〈infinite regress〉」とかの言葉がありますね。これって、大幅な意訳(つうか憶測)すると「マイクロコスモ原理に阻まれちゃってダメみたい、トホホ」と嘆いてるのでは。

nLab著者も、僕と同じようにマイクロコスモ原理からの無限後退に悩んでいる様子です。でも、たぶん大丈夫。n-セオリーの無限タワーも、どこかで安定するか既存の無限タワーに合流するだろうと(楽観的に)予想できます。

最近たまたまチラ見したスタニスワフ・スザウィール〈Stanisław Szawiel〉の学位論文*4に、次のような段落があります。

In short, understanding category theory starts with a 2-category. This pattern repeats itself indefinitely: to understand the mentioned universal constructions in Cat properly, one needs to work with 3-categories. In general, the understanding of n-categories requires knowledge of (n + 1)-categories. The internal consistency of category theory demands the development of higher categories.

若干補足しながら意訳すると:

圏論で扱うモノ、つまり圏の全体は2-圏Catを構成するので、圏論を理解することは2-圏の学習なんだ、と言える。このパターンは無限に繰り返される: 圏論に登場するCatにおける普遍構成をチャンと理解するには、3-圏を知る必要がある。一般に、n-圏の理解には(n+1)-圏を知ることが要求される。こういう事情だから、圏論に内在する構造(それは決して矛盾したものじゃない)から言って、1次元圏論だけではなくて高次の圏論を開拓する必要があるんだ。

「n-圏を理解するには(n+1)-圏を知る必要がある」は、マイクロコスモ原理ですが、スザウィールはそれを悲観的に捉えている様子はありません。むしろ、高次圏論の必要性を正当化する積極的理由としてアピールしています。

マイクロコスモ原理を回避したり消し去ることは出来ないようなので、「圏論に内在する構造」とみなすのが正しい -- かどうか分からないけど、精神衛生上は良い態度ですね。

高次圏: セオリーと指数関手タワー

| 16:28 | 高次圏: セオリーと指数関手タワーを含むブックマーク

さらに補足。

nLab(https://ncatlab.org/nlab/show/HomePage)は、たいていの概念に対して明確で信頼できる定義を提供してくれます。ですが、ドクトリンの定義(https://ncatlab.org/nlab/show/doctrine)は、なんだかハッキリしません。ドクトリンの定義がいくつもあるって事情もあるでしょうが、それを差し引いてもやっぱりモンヤリ

これは象徴的な事態だと思います。どんな意味で象徴的かと言うと; 無限タワーを考えないとうまくいかないことを示す例として。

nLabの(主要な)定義では、ドクトリン=2-セオリーです。そして、セオリー=1-セオリーなので、「1-セオリー, 2-セオリー」は考えています。しかし、k = 1, 2 以外のkまで含めたトータルなk-セオリー(k = ..., -1, 0, 1, 2, ...)を考えてはいません。「高次圏: 無基底・無限階層 補足」で引用したように、無限後退〈infinite regress〉を嫌っているのです。

無限タワーとしてのセオリーを考えると、「n-セオリー」という言葉の曖昧さも見えてきます。

  • ひとつの無限タワーの特定次元(それがn)の部分(n-成分、n-部分)を「n-セオリー」と呼んでいるのか?
  • ひとつの無限タワーの、特定次元(それがn)より下側を切り落とした上切片〈upper segment〉を「n-セオリー」と呼んでいるのか?
  • ある特定次元(それがn)以上の部分しか持たい無限タワー全般を「n-セオリー」と呼んでいるのか?

このへんがハッキリしてないので、ドクトリン=2-セオリーの定義もモンヤリしてしまいます。

一般に、ある構造・概念Xが無限タワーであるとは、すべての整数(負の数も含めて)kに対してXkが定義されていることだとします。ある整数nに対して、k < n の部分が定義されてない(むしろ、定義が自明で考えなくてもよい)とき、下限次元〈lower bound dimension〉がnの上方無限タワー〈upper infinite tower〉と呼ぶことにします。例えば、モノイドという構造・概念は、下限次元が1の上方無限タワーとみなしていいでしょう。なぜなら、k < 1 に対するk-モノイドを考える必要はないからです*5

さて、無限タワーとしてのセオリーとは何かというと、実は二項指数関手を無限タワー化したものと捉えればよさそうです。二項指数関手については:

上記の一番目の記事の「一般化:2次元化と相対化」の節で、無限タワー化が必要そうだが難しい、ということは書いています。

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

難しいんだけど、多少イイカゲンであってもn次元の(二項)指数関手の定義がやっぱり必要。もし、すべての次元に渡って二項指数関手の概念が定義できれば:

  • セオリー = 表示を持つ二項指数関手の無限タワー
  • n-セオリー = 表示を持つ二項指数関手の下限次元nの上方無限タワー

と定義できます。具体的なnに対しては:

  • セオリー = 1-セオリー = 表示を持つ二項指数関手の下限次元1の上方無限タワー
  • ドクトリン = 2-セオリー = 表示を持つ二項指数関手の下限次元2の上方無限タワー

冒頭で参照したnLabのドクトリン(2-セオリー)の定義は、k = 2 だけで定義しようとして、k = 3, 4, ... の部分を無視しているのでスッキリしないものになっています。

とかエラソーに言ってますが、二項指数関手の上方無限タワーを実際に構成するのはだいぶ大変だわー。適当に手を抜いたヤツ*6は作ってみようと思ってるけど。

*1:言葉の使い方として、相互依存する一部分を取り出して、便宜的・暫定的にどれかを「基底」と呼ぶことは何の問題もありません。これは、絶対的な基底(本質)ではなくて相対的な基底(関連性)です。

*2:無基底性はある種の相対主義〈relativism〉でしょう。相対主義に対しては、「相対主義を絶対化している点で相対的じゃない」という話が出てきますが、そんな議論はしたくないです。なぜなら、無基底性を有効な作業仮説と思っているから使うのであって、「有効そうだ」以上の根拠を求める気はないからです。

*3:僕も歳だけは敬われる立場になっている。歳だけ。

*4:"A Unified Approach to Opetopic Algebra" https://depotuw.ceon.pl/bitstream/handle/item/1115/doktorat.pdf

*5:「考えないことも許されるでしょ」ってことです。0-モノイドや(-1)-モノイドを考えてはいけない、とは言ってません。考えたい人はどうぞ。

*6:手の抜き方がひとつのテクノロジーなんだけどね。

2018-09-14 (金)

10等身?

| 14:05 | 10等身?を含むブックマーク

モデルのアンジェラ芽衣の謳い文句は「10等身ハーフモデル」。

*1

全身写真にグリッドをかぶせてみたのですが:

*2

どうみても“10等身”にはなってない。これも一種の詐称ですわ。

*1:画面ショットの元記事: https://mdpr.jp/interview/detail/1792522

*2:画像の元記事: https://news.walkerplus.com/article/159150/

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

2018-09-13 (木)

マイクロコスモ原理と構造の無限タワー

| 15:24 | マイクロコスモ原理と構造の無限タワーを含むブックマーク

悩みとフラストレーションの種であったマイクロコスモ原理ですが、「無限のタワーを登るんだ」と覚悟を決めたら悩みは軽くなりました。

内容:

  1. マイクロコスモ原理
  2. 使っている記号の一覧表
  3. モノイドの指標とモノイド圏の指標
  4. 指標の書き方の整理
  5. 指標の名目次元と実質次元
  6. 安定した指標
  7. 構造の無限タワーと安定化

[追記]メモ編の「モノイドやモノイド圏の指標 補足解説」に、この記事より若干使いやすそうな記法を説明しています。併せて読むと、構文に関する理解が捗るでしょう。[/追記]

マイクロコスモ原理

マイクロコスモ原理〈microcosm principle〉について最初に書いたのは次の記事; 一年前なので、それほど昔じゃないですね。

2018年に入って、比較的詳しい分析をしています。

マイクロコスモ原理の主張は「ある代数的構造(例:モノイド)を定義するとき、その前に、環境となる圏(例:モノイド圏)を定義しろよ」と解釈できます。これを律儀に守ろうとすると、無限後退(むしろ無限前進か?)を強いられます。いつまでたっても定義が終わんねーじゃねーかよ!

マイクロコスモ原理は、ほんとに頭痛の種。2017年記事のタイトルにある「恐怖」は大げさではなくて、強い不安感を感じます。なかなかスッキリした解決が得られません。

最近、発想を変えてみました。無限後退(あるいは無限前進)に文句を言わないで、「そういうもんだ」と受け入れてみたのです。つまり、「いかにして無限後退を回避するか?」という問は捨てて、「いかにして無限後退をするか?」に切り替えるのです。

そもそもの話; n-圏(n次元の圏)という概念は、いまだに広く合意された定義がありません。定義を求めて努力しているわけです。これは、適当なn(例えば n = 10)で定義する行為を打ち切りたい、という話ではありません。すべてのnに渡って「n-圏とはなんぞや」に答えを出そうとしています。

そうであるなら、nを 0, 1, 2, ... と増やして“次元の階段”を登る行為を「途中でやめたい」という発想は違うのではないか、本来、「無限に登るしかないのではないか」と思い直した、ってことです。

使っている記号の一覧表

後で使う記号の一覧表を先に出しておいたほうがいいような気がします。必要に応じてこの表を参照してください。

n = 1 n = 2 n = 3
k = 0 台対象 U U -
k = 1 恒等射 idUIdU = J -
k = 1 乗法/積 m ¥otimes = Y × = Y
k = 0, 1 単位(対象・射) i I I
k = 2 結合律子 α α
k = 2 左単位律子 λ λ
k = 2 右単位律子 ρ ρ

横に並んでいる n = 1, 2, 3 は、代数的構造の“次元”を示す整数です。つまり、1次元構造の場合、2次元構造の場合、3次元構造の場合がそれぞれ縦に並びます。ここでいう「次元」は幾何的概念ではなくて、圏論的な次元です。1次元構造は1-圏内に棲息する構造、2次元構造は2-圏内に棲息する構造です。

縦に並んでいる k = 0, 1, 2 は、代数的構造を構成する射の次元です。k = 1 なら1-射ということになります。0-射は圏の対象のことです。空欄は存在しないことを示し*1、ハイフンは明示的な記号を使ってないことを示します。

モノイドの指標とモノイド圏の指標

モノイドの指標を次の形で書きましょう。

signature mon := {
 sort U;
 operation m:U¥otimesU→U;
 operation i:I→U;
}

ざっと説明します。

  • 指標〈signature〉とは、代数系を構成する素材を表す記号を列挙した記述です。
  • Uは、モノイドの台対象〈underlying object〉を表す記号です。集合圏で考えるなら、台対象は台集合〈underlying set〉です。集合圏以外の圏でもモノイドは考えられます。
  • mは、モノイドの乗法〈multiplication〉または〈product〉を表す記号です。mはU上の二項演算(を表す記号)です。集合圏で考えるなら、¥otimesは直積×の意味で、 m:U¥otimesU→U は写像を表すことになります。
  • iは、モノイドの単位〈unit〉を表す記号です。iはUの定数ですが、単位対象Iからのポインティング射(単位射)と捉えます。集合圏で考えるなら、単位対象Iは単元集合で、単位射 i:I→U は単元集合からのポインティング写像を表すことになります。

指標は素材(を表す記号)を記述しているだけです。モノイドの定義には、さらに法則が必要です。法則(律)は等式で書きます。';'は、射の図式順結合(左から右への合成)記号です。

  • 結合律: (m¥otimesidU);m = αU,U,U;(idU¥otimesm);m : (U¥otimesU)¥otimesU→U
  • 左単位律: (i¥otimesidU);m = λU : I¥otimesU→U
  • 右単位律: (idU¥otimesi);m = ρU : U¥otimesI→U

法則のなかに、自然変換 α, λ, ρ が出てきたことに注目してください。これらの自然変換は、モノイドが定義される環境である圏が構造として備えている(はずの)ものです。

モノイドの指標と法則のなかに登場した記号達 ¥otimes, I, α, λ, ρ は、モノイドが棲む環境(つまりモノイド圏)を定義する指標から供給されます。環境側の指標がコレ(↓)、モノイド圏の指標ですね。'*'は、関手の図式順結合(左から右への合成)記号です。

signature mon-cat := {
 sort U;
 operation Y = ¥otimes:U×UU;
 operation I:IU;
 operation J = IdU:UU;
 2-operation α::(Y×J)*Y⇒αU,U,U*(J×Y)*Y:(U×U)×UU;
 2-operation λ::(I×J)*Y⇒λU:I×UU;
 2-operation ρ::(J×I)*Y⇒ρU:U×IU;
}

この指標が、記号 ¥otimes, I, α, λ, ρ を提供しています。

  • Uは、モノイド圏の台圏を表す記号です。圏は“圏の圏”の対象です。
  • ¥otimesにYという別名を付けています。そのYは、U上の二項演算(を表す記号)です。つまり、双関手(を表す記号)です。双関手は“圏の圏”の射です。
  • Iは、Uの定数ですが、単位圏(自明圏)Iからのポインティング関手(を表す記号)と捉えます。ポインティング関手も“圏の圏”の射です。
  • 恒等関手IdUにJという別名を付けています。これは表記を簡略化するためです(それ以上の意味はありません)。
  • αは、結合律を表現する自然変換(を表す記号)です。自然変換は、“圏の圏”の2-射です。
  • λは、左単位律を表現する自然変換(を表す記号)です。自然変換は、“圏の圏”の2-射です。
  • ρは、右単位律を表現する自然変換(を表す記号)です。自然変換は、“圏の圏”の2-射です。

モノイド圏の定義にも法則が必要です。マックレーンの五角形法則と三角形法則がモノイド圏が満たすべき法則です。その詳細は省略します(「マイクロコスモ原理と逆帰納ステップ」参照)。

モノイド圏の指標と法則には、次の太字記号が登場しました。

  1. 単位圏を表す I
  2. デカルト積双関手を表す ×
  3. ×に伴う自然変換を表す α, λ, ρ

これら太字の記号は、“圏の圏”が生息している環境である”圏の圏の圏”を定義する指標から提供されるものです。こうして我々は無限後退(あるいは無限前進)の道を歩むことになります。

指標の書き方の整理

高次元の指標も書けるように、指標の書き方を整理します。次元ごとに固有な名前・記号を使うのを出来るだけ避けて、次元を表す番号を使うことにします。その方針でモノイドの指標を書き換えると:

1-signature 1-mon := {
 0-morphism U;
 1-morphism m:U¥otimesU→U;
 1-morphism i:I→U;
}

1-指標〈1-signature〉は、1次元までの射の宣言を含みます。2次元以上の射の宣言は入れられません。ただし、1次元の射が(あるいは0次元の射も)なくてもかまいません。1-指標(と法則)で定義される実体(モデル〈model〉と呼ぶ)は、1-圏のなかに棲んでいると考えます。モデルであるモノイド達の、標準的な棲息環境は1-圏Setです。

モノイド圏の指標は次のように書きます。

2-signature 2-mon := {
 0-morphism U;
 1-morphism Y = ¥otimes:U×UU;
 1-morphism I:IU;
 1-morphism J = IdU:UU;
 2-morphism α::(Y×J)*Y⇒αU,U,U*(J×Y)*Y:(U×U)×UU;
 2-morphism λ::(I×J)*Y⇒λU:I×UU;
 2-morphism ρ::(J×I)*Y⇒ρU:U×IU;
}

モノイド圏は、モノイドを2次元化(圏化)したものと捉えて、2-monという名前を付けています。モノイド圏(2-mon)を定義する指標は2-指標なので、2次元までの射を書けます。実際、α, λ, ρ は2次元の射〈2-射〉です。2-指標(と法則)で定義されるモデルは、2-圏のなかに棲んでいると考えます。モデルであるモノイド圏達の、標準的な棲息環境は2-圏Cat、または必ずしも小さくない圏の2-圏CATです。

さて、「次元ごとに固有な名前・記号を使うのを避ける」と言ったのですが、文字の種類や装飾は、通常の習慣に従って色々使っています。これらも一律にします。一律にすると、次元ごとの違いが判読しにくくなり、分かりにくくなります。しかし、次元ごとに別な文字種/文字装飾を使うことは、「すべての次元を考える」場合にはどうせ無理です。次元によらず、次の記号を使うことにします。

k = 0 台対象  U
k = 1 Uの恒等射  J 
k = 1 乗法/積  Y 
k = 0, 1 単位(対象・射) I 
k = 2 結合律子  α 
k = 2 左単位律子 λ 
k = 2 右単位律子 ρ 

n-指標には、環境を表す(n+1)-指標から提供される記号が出てきます。1次元高い指標から来る記号は、一律に太字+下線で表すことにします。下線も付けるのは視認性のためです。

今述べたルールで指標と法則を書き換えると次のようになります。

1-signature 1-mon := {
 0-morphism U;
 1-morphism J:U→U;
 1-morphism Y:Y(U, U)→U;
 1-morphism I:I→U;
}

法則は 2-morphism
 2-morphism as:: Y(Y, J);Y = αU,U,U;Y(J, Y);Y : Y(Y, J)→Y(J, Y);
 2-morphism lu:: Y(I, J) = λU : Y(I, U)→U;
 2-morphism ru:: Y(J, I) = ρU : Y(U, I)→U;

2-signature 2-mon := {
 0-morphism U;
 1-morphism J:U→U;
 1-morphism Y:Y(U, U)→U;
 1-morphism I:I→U;
 2-morphism α::Y(Y, J)*Y⇒αU,U,U*Y(J, Y)*Y:Y(Y, J)→Y(J, Y);
 2-morphism λ::Y(I, J)*Y⇒λU:Y(I, U)→U;
 2-morphism ρ::Y(J, I)*Y⇒ρU:Y(U,I)→U;
}

法則は 3-morphism
 省略

1-mon(通常のモノイド)の指標には、環境から提供される記号として、下線付き太字の Y, I, α, λ, ρ が使われています。それらの下線付き太字記号は、2-mon(モノイド圏)の指標における Y, I, α, λ, ρ として定義されるものです。

2-mon(モノイド圏)の指標にも、環境から提供される記号として、下線付き太字の Y, I, α, λ, ρ が使われています。それらの下線付き太字記号は、モノイド圏をホストする2-圏、例えばデカルト圏としてのCatにおける Y, I, α, λ, ρ として具体化されます。

最後に、圏の結合記号〈composition symbol〉を統一します。射の結合、関手の結合、自然変換の縦結合、自然変換の横結合などを別な記号(オーバーロードあり)で表していますが、単一の記号'#'にします。その代わり、次元の添字を付けます。'#nk'は、2つのn-射をk次元の境界で貼り合わせる結合です。

通常の記法 統一した記法
射の結合 ; #10 of C
関手の結合 * #10 of CatCAT
自然変換の縦結合 ; #21 of CatCAT
自然変換の横結合 * #20 of CatCAT

ここから先では、統一した記法を使うことにします。

指標の名目次元と実質次元

我々の目的は、無限に続く次元の階段を登り切ることです。1-指標と法則で定義される1-構造(1次元の構造)があり、その1-構造をホストする2-構造(2次元の構造)は2-指標と法則で定義され、その2-構造をホストする3-構造(3次元の構造)は3-指標と法則で定義され、… … … を延々と続けたいわけです。

モノイド構造の例で言えば:

  • 1-signature 1-mon と法則で1-モノイド構造が定義される。
  • 2-signature 2-mon と法則で2-モノイド構造が定義される。
  • 3-signature 3-mon と法則で3-モノイド構造が定義される。
  • … … …

指標の次元が上がるにしたがって、より高い次元の射がどんどん追加され、法則も増えて、構造はどんどん複雑になっていくのではないか -- それが僕には“恐怖”でした。しかし、構造の記述(指標+法則)がどこかで安定化〈stabilize〉すれば、無限に続いていても怖くはないです。安定化とは、次元が上がっても構造の複雑化は起きなくなることです。

安定化のメカニズムを説明するために、指標の名目次元と実質次元という量(整数値)を導入します。具体例として次の指標を考えます。

2-signature 2-1-mon := {
 0-morphism U;
 1-morphism J:U→U;
 1-morphism Y:Y(U, U)→U;
 1-morphism I:I→U;
}

法則は 2-morphism
 2-morphism as:: Y(Y, J)#10Y = αU,U,U#10(Y(J, Y)#10Y) : Y(U, U)→U;
 2-morphism lu:: Y(I, J) = λU : Y(I, U)→U;
 2-morphism ru:: Y(J, I) = ρU : Y(U, I)→U;

これは、先に出した1-指標の定義をほぼそのままコピーしたものです。前節の約束に従って、';' → '#10' としてますが、それ以外で変更した所は、

  • 1-signature 1-mon → 2-signature 2-1-mon

これだけ。中身を一切変えずに、「これは2-指標だぞ」と言い張るだけです。2-指標に2-射を要求するわけではないので、「2-指標だぞ」と言っても責められることはありません。このような場合、指標の名目次元が2、実質次元が1だと言います。

  • 名目次元〈formal dimension〉: 指標の先頭にある次元宣言に書かれた値
  • 実質次元〈actual dimension〉: 指標に登場する射の最高次元

指標の名目次元がnであるとは、その指標に出現する記号をn-圏で解釈するという指示です。実質次元mは、実際に使う射の最高次元です。m ≦ n は必須ですが、m = n は要求しません。

例に挙げた指標は、もともとは1-指標であったモノイドの指標の名目次元を2にしたものです。モノイドの指標は1-圏(例えばSet)で解釈するものですが、2-圏(例えばCat)でも解釈できます。よって、2-signature 2-1-mon は、解釈の場が2-圏であるようなモノイド対象の指標です。具体的には、完全にストリクト*2な(小さな)モノイド圏は、2-指標2-1-mon(と法則)の2-圏Catにおけるモデルになります。

一般に、n-圏Kがあるとき、Kから、mを超える次元の射を削り落としたm-圏をK[m]と書くことにします。実質次元がmであるn-指標(と法則)は、n-圏Kを次元mで切り捨てた〈truncated〉K[m]で解釈可能です。この切り捨て〈truncation〉は、神ならぬ我々にとっては極めて重要です。高次射が把握できなくても、把握可能な次元(例えば2次元)まで見ればいいことになるからです。

安定した指標

お気付きの方もいると思いますが、2-signature 2-1-mon の法則の部分を指標内部に入れて、わずかに変更すると、それは 2-signature 2-mon と同じになります。

2-signature 2-mon := {
 0-morphism U;
 1-morphism J:U→U;
 1-morphism Y:Y(U, U)→U;
 1-morphism I:I→U;
 2-morphism α:: Y(Y, J)#10Y ⇒ αU,U,U#10(Y(J, Y)#10Y) : Y(U, U)→U;
 2-morphism λ:: Y(I, J) ⇒ λU : Y(I, U)→U;
 2-morphism ρ:: Y(J, I) ⇒ ρU : Y(U, I)→U;
}

一般的な n-signature n-mon を考えて、n = 1, n = 2 で解釈を変えるだけです。標準的な解釈を表にしてみます。

n = 1 n = 2
解釈の場集合圏 Set 圏の圏 Cat
#10 写像の結合関手の結合
U 台集合 台圏(小さい)
J Uの恒等写像 Uの恒等関手
Y 集合の直積 圏の直積
I 単位ポインティング写像 単位ポインティング関手
α 結合律(等式) 結合律子(自然変換)
λ 左単位律(等式)左単位律子(自然変換)
ρ 右単位律(等式)右単位律子(自然変換)

2-signature 2-mon を構成する2-射(自然変換)である律子(律子に関しては「律子からカタストロフへ」を参照)を、特に恒等自然変換に固定すると、それは(法則も含めた)モノイドの記述になります。

「1-signature 1-mon → 2-signature 2-1-mon → 2-sinature 2-mon」という指標の構成・変更と同じ手順で、「2-signature 2-mon → 3-signature 3-2-mon → 3-sinature 3-mon」とすると、3-モノイド構造の3-指標が得られます。その3-指標の標準的な解釈の場、つまり3-モノイド構造(モデル)の棲息地は、例えば小さなストリクト2圏を対象とする3-圏s2-Catでしょう。

3-sinature 3-mon とそのモデルについて今詳しくは述べませんが、特筆すべきは、同様な手順で次元を上げて 4-mon, 5-mon, … を作っても形が変わらないことです。指標のなかに、その指標では定義できない下線付き太字記号が残り続けますが、記号の個数は増えません。次元が上がっても、同じ景色がずっと見え続けるような状況になるわけです。

モノイドの定義が無限に先送りされる状況ではありますが、無限に複雑さが増えるわけではありません。必要な射や法則が増えるのも頭打ちになり、構造は変わらず次元のみが淡々と増えるだけ。「マイクロコスモ原理と逆帰納ステップ」で述べた逆帰納ステップは止まりませんが、安定はするのです。

構造の無限タワーと安定化

安定した指標は、自分自身に依存する、あるいは自分自身に立ち戻ってくるので、循環的定義〈{cyclic | loop} definition〉になっています。循環を線形に展開すれば無限タワー〈stabilized infinite tower〉になります。

*3

通常の再帰・帰納とは違い、n = 0 に基礎があるのではなくて、無限の彼方に基礎があります。あるいは、無限の彼方に向かって歩み続ける行為そのものが基礎なのかも知れません。

マイクロコスモ原理と逆帰納ステップ」で次のように書きました:

どうもスッキリとは解決できないんです。仏教に帰依しようか … なんてね。

...[snip]...

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

よく知らん仏教を引き合いに出すのはイカガナモノカだけど、「確固たる基礎が望めないような階層的世界」においては、「階層のどかで止まる」という発想は好ましくないようです。今は、次のように考えています。

  1. 構造は、無限のタワーとして定義される。
  2. 我々は、安定する無限タワーしか具体的に扱えない。
  3. 無限タワーの作り方は物凄い多様性を持つ。

これまで事例に出したのは、n-mon (n = 1, 2, 3, ... )だったのですが、他の無限タワーの例も見つけたいですね。色々な例を見ないと実情が把握できませんから。

とりあえず、安定する無限タワーという概念により、マイクロコスモ原理に対する恐怖感はだいぶ薄らいだ、とは言えます。

*1:等式的な法則も射と解釈すれば存在します。

*2:"strict"は「厳密」ではなくて、カタカナで「ストリクト」と書くことにします。

*3:元記事: http://765.blogspot.com/2007/06/infinite-in-every-direction.html
画像: https://www.flickr.com/photos/sevensixfive/218194699/

yamyam 2018/09/18 02:53 いつも檜山さんの記事を楽しみにしています。
ところで、\otimesは二項演算なのにU×Uという1引数を取っているように見えてしまい、どうも腑に落ちません。
Yと(_,_)の関係を説明しようとしても、うまく言葉にならないというか。
気づいたらこんな時間になっていました。

m-hiyamam-hiyama 2018/09/18 12:52 yamさん、
> 気づいたらこんな時間になっていました。
確かにタイムスタンプは深夜ですね。
> Yと(_,_)の関係を説明しようとしても、うまく言葉にならないというか。
鋭い! まさにそこ、ペアを作る操作が問題なんです。マイクロコスモ原理にやられちゃうポイントなんです。
コメント欄で説明するには、余白が足りない話題なので、ちょっと待ってください。

m-hiyamam-hiyama 2018/09/19 13:10 yamさんの疑問は僕が持っていた疑問と同種だろう、と推測して http://d.hatena.ne.jp/m-hiyama/20180919/1537329676 を書きました。見当違いならごめんなさい。
でも、多少の参考にはなるかと思います。

2018-09-11 (火)

正確な記述と演繹のための非日本語記法

| 16:22 | 正確な記述と演繹のための非日本語記法を含むブックマーク

少し前に「TypeScriptで(無理して)論理式: 言霊排除」という記事を書きました。タイトル内の「言霊排除」の意味は、次のようなことです。

自然言語(日本語)には言霊〈ことだま〉が宿るとかいいますが、強烈なイメージ喚起力は言霊のパワーなのかも知れません。...[snip]... 数学的・論理的な命題の記述と解釈においては、言霊の影響 -- 現実世界や感情の世界への連想・参照 -- をできるだけ排除したい。...[snip]... ともかく、命題を扱う際は真偽判定に集中してください。言霊の影響を断ち切ってください。

命題自体を日本語(自然言語)で書くのをやめても、その周辺で使っている日本語により、またしても日常的な不正確さ/曖昧さ/根拠薄弱な推論の悪習へと引きずり込まれてしまうことがあるようです。なんとかせねば。

この記事の内容は「証明の“お膳立て”のやり方」シリーズと類似してますが、より入門的な構成・語り口にしています。モノをチャンと考えるときの枠組みのお話です。

内容:

  1. 日本語と日常と非論理
  2. 命題の例
  3. 命題の正しさ
  4. 文脈
  5. 文脈を命題のなかに押し込む
  6. 文脈付き命題の操作
  7. 正しさの根拠
  8. 共有されている予備知識
  9. おわりに

日本語と日常と非論理

我々はほとんど常に日本語を使い/日本語で考えています。日本語による表現には不正確さや曖昧さがあります*1。その日本語表現をベースに、根拠がハッキリしない雰囲気的な推論を日常的に行っています。そして、それでもたいして不都合はないのです。日常生活において、正確な表現や確実な推論が必要な場面は意外に少ないからです。

日本語の語彙と文法のなかで、正確な表現/確実な推論をこなす人も確かにいます。しかし、日本語を使用することにより、考え方までグダグダになってしまう人もいます。悪しき言霊の影響を受けやすい人は、論理的思考において日本語を使うのをやめるほうがいいと思います。

そうなると、日本語ではない人工言語を習得することになり、習得の負担が増えます。でも、それは仕方ない。日本語のなかで論理的思考をチャンとしている人は、語彙と文法が日本語と共通している別な言語を使っているのです。もうひとつの言語の習得はいずれにしても必要なのです。新言語が、なまじ日本語と同じ語彙・文法だとかえって混乱する人のほうが多いので、語彙・文法は日本語と違っていたほうがむしろ望ましいと言えます。新言語により、曖昧さと雰囲気の世界から脱出しましょう。

命題の例

等式や不等式は典型的な命題です。次の等式・不等式を例に使います。

  1. (a + b)2 = a2 + 2ab + b2
  2. (a + b)2 = a2 + b2
  3. x + y ≧ 0

これらは記号的な表現だけで構成されていますが、次の命題には日本語が含まれます。

  • n, mが3の倍数ならば、 n + m は3の倍数である

「3の倍数である」を表す記号的な表現を「M3」としましょう。「6は3の倍数である」は「M3(6)」です。「nは3の倍数である」は「M3(n)」と書きます。この記法を使えば:

  • M3(n) かつ M3(m) ならば M3(n + m)

さらに、「かつ」と「ならば」も記号的表現にして:

  • (M3(n) ∧ M3(m)) ⇒ M3(n + m)

この命題を含めて4つの命題が今後使う例です。

  1. (a + b)2 = a2 + 2ab + b2
  2. (a + b)2 = a2 + b2
  3. x + y ≧ 0
  4. (M3(n) ∧ M3(m)) ⇒ M3(n + m)

命題の正しさ

命題が提示されたことと、その命題が正しいことは別なことです。なにかが正しい根拠として、「テレビで誰々が言っていた」「インターネットのなんとかページに書いてあった」とかを引き合いに出す人がいますが、これは、命題が提示されていたことを即座にその命題の正しさに結びつけています。

もちろん、「十分に信頼できる人が言った/十分に信頼できるメディアに書いてあった」は正しさの根拠として使ってもよいのですが、単に「提示されていた」から即座に「正しい」という判断を下すのは危険です。とある命題が正しいことを英語で言えば The proposition is correct. となるでしょう。語順を変えて「IsCorrect 命題」という形を、命題の正しさの主張(メタ命題と呼ぶことがある)に使います。逆に、とある命題が正しくないという主張は「IsWrong 命題」とします。

前節で挙げた4つの命題は単に提示されただけと考えると、それらを真偽判定した結果(の可能性)は次の8つになります。

  1. IsCorrect (a + b)2 = a2 + 2ab + b2
  2. IsCorrect (a + b)2 = a2 + b2
  3. IsCorrect x + y ≧ 0
  4. IsCorrect (M3(n) ∧ M3(m)) ⇒ M3(n + m)
  5. IsWrong (a + b)2 = a2 + 2ab + b2
  6. IsWrong (a + b)2 = a2 + b2
  7. IsWrong x + y ≧ 0
  8. IsWrong (M3(n) ∧ M3(m)) ⇒ M3(n + m)

命題が真か偽か分からないときは、IsUncertain を使うことにします。これも入れると、真偽判定の結果は12個になります。

  1. IsCorrect (a + b)2 = a2 + 2ab + b2
  2. IsCorrect (a + b)2 = a2 + b2
  3. IsCorrect x + y ≧ 0
  4. IsCorrect (M3(n) ∧ M3(m)) ⇒ M3(n + m)
  5. IsWrong (a + b)2 = a2 + 2ab + b2
  6. IsWrong (a + b)2 = a2 + b2
  7. IsWrong x + y ≧ 0
  8. IsWrong (M3(n) ∧ M3(m)) ⇒ M3(n + m)
  9. IsUncertain (a + b)2 = a2 + 2ab + b2
  10. IsUncertain (a + b)2 = a2 + b2
  11. IsUncertain x + y ≧ 0
  12. IsUncertain (M3(n) ∧ M3(m)) ⇒ M3(n + m)

文脈

例にしている4つの命題について、真偽判定を実際にしようとすると、情報が不足していることに気付きます。

例えば、x + y ≧ 0 で、文字x, yが何を表すかわかりません。x, yに関して、何かの条件が事前に課されていたかもしれません。このような、当該の命題以外の情報を文脈〈context〉と呼びます。通常、命題は文脈のなかに置かれます。文脈から切り離すと真偽不明どころか意味不明になるかも知れません。

文脈を明示的に書くために、Forというキーワードを使うことにします。例えば:

For x∈N, y∈N.
  x + y ≧ 0

文脈を複数のForで書いてもいいとします。

For x∈N.
For y∈N.
  x + y ≧ 0

同じ命題を別な文脈のなかに置いてみましょう。

For x∈R, y∈R.
  x + y ≧ 0

さらに別な文脈に置いてみます*2

For x∈R, y∈R.
For x ≧0, y ≧0.
  x + y ≧ 0

文脈付きの(文脈のなかに置かれた)命題に真偽判定の結果を追加すると、次のようになります*3

For x∈N, y∈N.
  IsCorrect x + y ≧ 0

For x∈N.
For y∈N.
  IsCorrect x + y ≧ 0

For x∈R, y∈R.
  IsWrong x + y ≧ 0

For x∈R, y∈R.
For x ≧0, y ≧0.
  IsCorrect x + y ≧ 0

文脈を命題のなかに押し込む

「命題は文脈のなかに置かれる」と言いました。となると、文脈なしでは真偽判定ができないことになります。これでは困ることがあります。そこで、文脈を命題側に押し込む操作をします。

例えば、

For x∈R, y∈R.
For x ≧0, y ≧0.
  x + y ≧ 0

これの二番目のForで書かれた文脈を、命題に入れてしまうと:

For x∈R, y∈R.
  (x ≧0 ∧ y ≧0) ⇒ x + y ≧ 0

文脈としてはカンマで区切ってあった命題を、記号「∧」(かつ)でつないで、「⇒」(ならば)の前に入れればいいのです。

文脈を複数のForに分割するやり方は一通りではありません。それによって、文脈を押し込んだ命題の形は変わります。例えば、

For x∈R, y∈R.
For x ≧0.
For y ≧0.
  x + y ≧ 0

から、下2つのForを順次命題側に押し込むと:

For x∈R, y∈R.
  x ≧0 ⇒ (y ≧0 ⇒ x + y ≧ 0)

これで何の問題もありません。次の2つの命題は表現が違うだけで内容的に同じなのです。

  1. (x ≧0 ∧ y ≧0) ⇒ x + y ≧ 0
  2. x ≧0 ⇒ (y ≧0 ⇒ x + y ≧ 0)

さて、For x∈R, y∈R. という文脈も命題に押し込みましょう。変数がどの集合に所属しているかを示す命題は、プログラミングでいうと変数の型宣言みたいなものです。このタイプの命題は特別扱いをします。x∈R ならば、∀x∈R. という形に直して、命題の先頭に付けます。例えば、

For x∈R, y∈R.
  (x ≧0 ∧ y ≧0) ⇒ x + y ≧ 0

から、次の形に変形されます。

∀x∈R.∀y∈R.( (x ≧0 ∧ y ≧0) ⇒ x + y ≧ 0 )

得られた命題を、強いて日本語に翻訳するなら:

  • 任意の実数x、任意の実数yに対して、x ≧0 かつ y ≧0 ならば x + y ≧ 0

この命題なら、文脈なしでも不明な点や誤解される所はないでしょう。

文脈付きの命題でも、文脈をどんどん命題のなかに詰め込んでしまえば、文脈なしで通用する単独の命題にパッケージ化できます。

文脈付き命題の操作

命題を論理的に操作することはもちろん重要です。例えば、二重否定の法則とかド・モルガンの法則を使って命題を変形するとかですね。しかしそれだけではなくて、文脈の操作もとても重要です。命題をうまく扱えない原因が、実は文脈をうまく扱えないことであることは多いです。

4つの例に、文脈を付けてみます。

For a∈R.
For b∈R.
  (a + b)2 = a2 + 2ab + b2

For a, b∈R.
  (a + b)2 = a2 + b2

For x∈Z, y∈Z.
  x + y ≧ 0

For n, m∈Z.
  (M3(n) ∧ M3(m)) ⇒ M3(n + m)

これらは文脈の一例で、他の文脈を付けることもできます。当然に、文脈により真偽も変わります。例えば、(a + b)2 = a2 + b2 も、文脈によっては真になります。

For a = 0.
For b = 1.
  (a + b)2 = a2 + b2

練習のために、前節で述べた「文脈を命題のなかに押し込む」ことをやってみます。そのとき、変形前の文脈付き命題を横線('-'の並び)の上に、変形後の文脈付き命題を横線の下に書く書き方を使います。次のようになりますね、変形を追いかけてみてください。

 For a∈R.
 For b∈R.
   (a + b)2 = a2 + 2ab + b2
 --------------------------------------------------
 For a∈R.
   ∀b∈R.( (a + b)2 = a2 + 2ab + b2 )
 --------------------------------------------------
   ∀a∈R.( ∀b∈R.( (a + b)2 = a2 + 2ab + b2 ) )

 For a, b∈R.
   (a + b)2 = a2 + b2
 ------------------------------------
   ∀a, b∈R.( (a + b)2 = a2 + b2 )

 For x∈Z, y∈Z.
   x + y ≧ 0
 --------------------------------
   ∀x∈Z.∀y∈Z.( x + y ≧ 0 )

 For n, m∈Z.
   (M3(n) ∧ M3(m)) ⇒ M3(n + m)
 ----------------------------------------------
   ∀n, m∈Z.( (M3(n) ∧ M3(m)) ⇒ M3(n + m) )

 For a = 0.
 For b = 1.
   (a + b)2 = a2 + b2
 ----------------------------------------------
 For a = 0.
   b = 1 ⇒ (a + b)2 = a2 + b2
 ----------------------------------------------
   a = 0 ⇒ ( b = 1 ⇒ (a + b)2 = a2 + b2 )

文脈を押し込んだ単一の命題に対して、真偽判定の結果を添えてみましょう。

  1. IsCorrect ∀a∈R.( ∀b∈R.( (a + b)2 = a2 + 2ab + b2 ) )
  2. IsWrong ∀a, b∈R.( (a + b)2 = a2 + b2 )
  3. IsWrong ∀x∈Z.∀y∈Z.( x + y ≧ 0 )
  4. IsCorrect ∀n, m∈Z.( (M3(n) ∧ M3(m)) ⇒ M3(n + m) )
  5. IsCorrect a = 0 ⇒ ( b = 1 ⇒ (a + b)2 = a2 + b2 )

正しさの根拠

前節の最後で、命題の先頭にIsCorrectまたはIsWrongを付けた形を並べました。命題に真偽判定の結果を添えたわけです。このとき、真偽はどうやって判定したのでしょう?つまり、「真偽判定の正しさ」が問題になります。

  • 命題が提示されただけでは、その命題が正しいかどうか分からない。
  • 真偽判定の結果が提示されただけでは、その判定が正しいかどうか分からない。

真偽判定に対して、そう判定した根拠を書かなくてはなりません。それが証明〈proof〉です。IsCorrectと判定したなら正しい根拠、IsWrongと判定したなら間違いである根拠を示す必要があります。IsWrongの根拠のほうは反証〈disproof | 反駁〉と呼びますが、広い意味の証明は反証も含みます。

ここでは、判定の根拠(証明または反証)を書くためににBecauseというキーワードを使うことにします。次のような形式になります。

For a∈R.
For b∈R.
  IsCorrect (a + b)2 = a2 + 2ab + b2
Because
  ここに
  証明を書く
End

証明の書き方は今回の話題ではないので述べません。肯定的な証明(IsCorrectの根拠)だけではなくて反証(否定の証明)を書く場合もあります。

For a, b∈R.
  IsWrong (a + b)2 = a2 + b2
Because
  ここに
  反証を書く
End

曖昧で雰囲気的な議論を避ける、つまり論理的な議論をするには、次の構成要素をセットとして考えます。

  1. 命題に対する文脈
  2. 命題
  3. 命題の真偽判定(ここでは IsCorrect, IsWrong で示した)
  4. 真と判定したなら肯定的な証明、偽と判定したなら否定的な証明(反証)

これらのうち一部が省略されることはしばしばあります。何が省略されているのかを強く意識しましょう。必要があれば確認しましょう。そうでないと、曖昧で雰囲気的な議論へと堕ちていきます。曖昧さと雰囲気を許してしまう態度、マーマーなーなーな精神こそ、論理的議論遂行の最大の障害です。

共有されている予備知識

次の文脈付きの命題を考えます。

For n, m∈Z.
  (M3(n) ∧ M3(m)) ⇒ M3(n + m)

これは文脈が付いているので、真偽判定が可能なはずです。実際、IsCorrectと判定しています。しかし、真偽判定の際に、M3が「3の倍数」という意味であることを考慮しています。いきなり、何の説明もなく上の文脈付き命題を出されたら、M3が不明なので真偽判定は不可能です。

「M3とは何であるか」の情報も文脈に必要なのです。ただ、文脈に書くと煩雑になるので、独立した別な記述にしましょう。

For n∈N.
  M3(n) := (n%3 = 0)

これは、M3の定義です。':='は定義のための等号です。定義の書き方は色々あります。いくつか書き方の例を挙げますが、「色々あるよ」ってだけで、どれかひとつ理解できれば書き方のバラエティを気にする必要はありません*4

M3(n∈N) := (n%3 = 0)

M3(n∈N) :⇔ (n%3 = 0)

M3 := λn∈N.( (n%3 = 0) ∈Bool)

∀n∈N.( M3(n) :⇔ n%3 = 0 )

(M3(n) ∧ M3(m)) ⇒ M3(n + m) という命題では、記号「M3」を既に知っている前提があるわけです。つまり、命題を解釈する際の予備知識があったわけです。予備知識がM3だけだったのか? というと、そうではありません。

(a + b)2 = a2 + 2ab + b2 に出てくる指数表記に関しても、それが掛け算を表すことは予備知識のひとつです。次のような定義を事前に知っている必要があります。

For a∈R.
  a2 := aa

さらに、単にaを並べることが、実は掛け算であることも予備知識です。

For a∈R.
  aa := a×a

(a + b)2 = a2 + 2ab + b2 の証明のなかで、実数の掛け算の交換法則が使われますが、それも予備知識ですね。

For a, b∈R.
  a×b = b×a

他にもたくさんの予備知識が必要ですが、それらをイチイチ書き出すことは通常はしません。それは、対話の当事者のあいだで共有されている予備知識だよね、ということで暗黙に前提されるのです。

ただし、暗黙の前提は危険でもあります。共有されていると思っていた予備知識が、実は共有されていない、ズレていたってことはありますよね。共有されているかどうか不安なときは、確認作業をしましょう。

おわりに

ねんがらねんぢゅう論理的な議論をする必要はありません。そんなことしていると嫌われますからね(苦笑)。ですが、論理的に考えて、論理的に表現して、論理的に説得する必要があるときは、それが出来るほうが望ましいでしょう。

命題について云々するときは、その命題そのものだけでなく、次のフォーマットで必要事項を書き出すといいでしょう。

その命題の文脈

  真偽判定
  命題

真偽判定の根拠

具体例を出せば:

その命題の文脈: a, b∈R

  真偽判定: IsWrong(偽である)
  命題: (a + b)2 = a2 + b2

真偽判定の根拠:
  a = 1, b = 1 としたとき、
  左辺 = (1 + 1)2 = 22 = 4
  右辺 = 12 + 12 = 1 + 1 = 2
  これは命題の反例となっているので、
  この命題は偽である。

文脈では書き切れない予備知識が背後にありますが、その予備知識が、対話の当事者間でチャンと共有されているかどうかの確認も重要です。

*1:日本語固有の問題ということではありません。自然言語は総じて不正確さ/曖昧さを避けられません。

*2:僕がローカルに使っていた(いる)記法では、変数が所属する集合(型)の指定にはFor、事前に想定する命題はGivenで書き分けますが、ここでは全部Forにしました。

*3:僕がローカルに使っていた(いる)記法では、IsCorrectの代わりにHoldsです。IsWrong相当は、Holdsの後の命題を否定にします。Holdsに相当する論理における標準的記法は、|- です。

*4:書き方のバラエティはとんでもない量であるので、そんなことをイチイチ気にしていたら消耗してしまいます。単に「いっぱいあるなー」と心得ておけばいいのです。

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

2018-09-07 (金)

モナドはモノイドだが、モノイドじゃない

| 11:30 | モナドはモノイドだが、モノイドじゃないを含むブックマーク

わけわからん記事タイトルを付けてしまいました。モナドが、あるモノイド圏内のモノイド対象であることは事実です。が、モノイドとして扱ってもラチがあかない問題もあります。さあ、どうしましょう。


定期的に、いやっ不定期的にだけど、マイ・モナドブームがやって来ます。2,3日前からn(不明)回目のマイ・モナドブームです。今回のブームのテーマは、「2-圏論からモナドを考える」です。キャッチフレーズは「モナドはモノイドじゃない」かな。

もちろん「モナドはモノイドだ」は嘘じゃないし、そう理解することは色々と役に立ちます。しかし、「モナドはモノイドだ」は特殊な視点からのモノの見方なので、モナドの全貌がモノイドとして把握できるわけではありません。

例えば、異なる圏の上のモナドのあいだの準同型射を定義するにはどうしたらいいでしょうか? この問に対して、「モナドはモノイドだ」と唱えてもご利益があるとは思えません。「モナドはモノイドだ」とは別な視点/別なアプローチが必要そうです。

モナドとは何であるか?」に対する「モノイドだ」とは別な見方として、「自明な2-圏から2-圏CATへのラックス2-関手である」という定義があります。これについては、「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き) // 自明な2-圏からのラックス2-関手」で触れています。「モナドはラックス2-関手だ」という見方をすると、モナドのあいだの準同型射はラックス2-自然変換〈lax 2-natural transformation〉だろうと見当が付きます。

では、どんなときに異なる圏の上のモナドのあいだの準同型射が欲しくなるのでしょう。プログラミング言語の構文論は、指標と呼ばれるデータ構造の圏の上のモナドと解釈できます。モナドが構文生成規則(文法)の定式化になります。一番簡単な例は、単なる集合を指標とみなして、構文生成は連接を自由に使ってよいとするものです。

このモナドを (Set, L, μ, η) とすると:

  • 指標の圏=集合圏Set
  • (L, μ, η) はリスト・モナド

集合(基本記号の集合=アルファベット)Aに対して、L(A) = List(A) = A* と書けます。A*はクリーネスターです。μA:L(L(A))→L(A) は、リストのリスト(列の列)を平坦にする写像; ηA:A→L(A) は、基本記号を長さ1のリストとみなす写像です。

必ずしも集合圏ではない圏C上のモナド (C, L, μ, η) があり、これがプログラミング言語の構文論を記述しているとします。別なプログラミング言語の構文論は別なモナド (D, M, ν, ε) で記述されるでしょう。(C, L, μ, η) から (D, M, ν, ε) への構文的変換(翻訳)は、モナドのあいだの準同型射として定式化するのが自然でしょう。これは、異なる圏上のモナドのあいだの準同型射、つまりラックス2-自然変換の応用例となります。

モナドはモノイドだ」視点は、2-圏論的対象物であるモナドの基礎圏=0-射部分を固定して1-圏論(=通常の圏論)に持ち込む方法に頼っています。そのまま2-圏論的に見たほうがモナド本来の生態が観察できる気がします。

関連する記事:

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

2018-09-06 (木)

前層の圏における記法と計算 もう少し

| 17:31 | 前層の圏における記法と計算 もう少しを含むブックマーク

日本列島は自然災害に苛まれています。皆さんご無事でしょうか。

前層の圏における記法と計算」に関してもう少し。定義コンテキストと引数の話。

内容:

  1. 定義のための構文
  2. 関手と自然変換での例
  3. プロファイルリストと定義の正規化
  4. おわりに

定義のための構文

構文の説明をします。退屈にならないように、簡単な例に沿って説明します。平面R2の距離dを例にしましょう。

  • d(x, y) := sqrt( (x1 - y1)2 + (x2 - y2)2 )

名前(変数)や式の型情報をちゃんと付けると:

  • d(x∈R2, y∈R2) := (sqrt( (x1 - y1)2 + (x2 - y2)2 ) ∈R)

あるいはラムダ記法を用いて:

  • d := λ(x, y)∈R2×R2.(sqrt( (x1 - y1)2 + (x2 - y2)2 ) ∈R)

次に、R2の一点aを固定して、その点からの距離を考えることにしましょう。

  • d(x∈R2) := (sqrt( (x1 - a1)2 + (x2 - a2)2 ) ∈R)

このとき、aに関する型情報も提供するために、次の形を使います。

  • For〔a∈R2〕 d(x∈R2) := (sqrt( (x1 - a1)2 + (x2 - a2)2 ) ∈R)

なにかを定義する場合の一般的な構文として、次を形式を採用することにします。Forの後の括弧が大きい(亀甲括弧)のは視認性のためです(それ以上の理由はありません)。

  • For〔名前の型情報〕 式1 := 式2

名前の型情報の部分を定義コンテキスト〈definition context〉、式1を定義ヘッド〈definition head〉、式2を定義ボディ〈definition body〉と呼ぶことにします。

定義ヘッドは名前だけ、または名前に仮引数並びを付けた形です。そして仮引数並びは、名前または型情報付きの名前を並べたもの(リスト)です。次はいずれも定義ヘッドになれる式です。

  1. d
  2. d(x, y)
  3. d(x∈R2, y∈R2)

仮引数並びに型情報が欠落している場合は、定義コンテキストで補うことができます。例えば:

  • For〔a∈R2, y∈R2〕 d(y) := (sqrt( (a1 - y1)2 + (a2 - y2)2 ) ∈R)

戻り値型の情報を定義ヘッド側(':='の左側)に付けてもいいとします。例えば:

  • For〔a∈R2, y∈R2〕 d(y) ∈R := sqrt( (a1 - y1)2 + (a2 - y2)2 )

今述べたルールだと、定義の書き方にはかなりの自由度があります。標準的な書き方に“正規化”することは後でまた触れます。

関手と自然変換での例

実際に僕が遭遇した例を説明します。とある状況で、ラムダ式 λu.F(u)(x) や、無名ラムダ変数(ハイフン)を使った F(-)(x) で計算していたのですが、だんだんワケワカラナクなってきました。この F(-)(x) をチャンと書き下すことにします。

とりあえず、F(-)(x) (λu.F(u)(x) でも同じ)の意味が分かりませんよね。Fは関手です。となると、Fの引数は対象か射です。uはたぶん射だろうと推測して、F(u)は、関手Fのターゲット圏の射だろうと見当が付きます。しかし、F(u)(x) の'(x)'の部分が不明。実は、Fは集合圏に値をとる関手でした。よって、F(u)は写像で、F(u)(x)は写像に引数(集合の要素)xを適用したものです。

とまー、そんなことをゴチャゴチャ説明するよりは、正確な記法で書いたほうが早い!

  1. C in Cat 、または C∈|Cat|
  2. F:CopSet in CAT 、または F∈CAT1(Cop, Set)
  3. A in C 、または A∈|C|
  4. x∈F(A)
  5. X in C 、または X∈|C|
  6. u:X→A in C 、または u∈C(X, A)
  7. F(u):F(A)→F(X) in Set 、または F(u)∈Set(F(A), F(X))
  8. F(u)(x)∈F(X)

F(-)(x) と書いたときの背後にこういった状況(文脈)があるわけです。とりあえず、F(-)(x) = λu.F(u)(x) に型情報を付けると:

  • λu∈C(X, A).(F(u)(x) ∈F(X))

このラムダ式で定義される写像をΨとすれば:

  • Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

出現している名前 A, x, X に関する型情報を定義コンテキストに置けば:

  • For〔A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

さらに、Cが小さい圏で、FがCからSetへの関手であることも定義コンテキストに含めると:

  • For〔C in Cat, F:CopSet in CAT〕 For〔A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

定義コンテキストは、Forの入れ子で書いてもフラットに書いても同じことです。なので、上の表現は次のようにフラットに書いてもかまいません。

  • For〔C in Cat, F:CopSet in CAT, A in C, x∈F(A), X in C〕 Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

逆に、新たな入れ子を作ってもかまいません。

  • For〔C in Cat, F:CopSet in CAT〕For〔A in C〕For〔x∈F(A), X in C
      Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

うまく入れ子を作ると、ひとつのコンテキスト内では依存性をなくす(プロファイル宣言の順番を変えてもいい)ように出来ます。

プロファイルリストと定義の正規化

プロファイルは型と同じようなものです。型はモノの種類ですが、プロファイルも種類で、次元が加味されています -- 前回の記事、より詳しくは「圏論的宇宙と反転原理と次元付きの記法」を参照してください。名前にプロファイルを付けるには、in記法、または集合の所属(∈)記法を使います。

プロファイル付きの名前をカンマ区切り*1で並べたものをプロファイルリスト〈profile list〉と呼びます。リストなので、原則的に順序を変えることは出来ません(特定の条件化で並べ替えが出来ることはあります)。例えば、前節最後の定義のコンテキスト内部はプロファイルリストです。

  • C in Cat, F:CopSet in CAT, A in C, x∈F(A), X in C

定義に登場する次の3つの部分は、すべてプロファイルリストです。

  1. 定義コンテキスト(の内部)
  2. 定義ヘッドの仮引数リスト
  3. ラムダ抽象のラムダリスト(ラムダ束縛変数のリスト)

単に構文が同じだけではなくて、定義コンテキスト/仮引数リスト/ラムダリストは相互に入れ替えが可能です。

定義コンテキストは、暗黙の引数と考えることができます。なので、定義コンテキストの一部または全部を、定義ヘッドの仮引数リストに移すことができます。例えば、最初の距離の例で、

  • For〔a∈R2, y∈R2〕 d(y) ∈R := sqrt( (a1 - y1)2 + (a2 - y2)2 )

型宣言(プロファイル宣言)を、仮引数リスト内に移すと:

  • d(a∈R2, y∈R2) ∈R := sqrt( (a1 - y1)2 + (a2 - y2)2 )

前節の例:

  • For〔C in Cat, F:CopSet in CAT〕For〔A in C〕For〔x∈F(A), X in C
      Ψ:C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

で、定義コンテキスト内のプロファイル宣言の一部を仮引数リストに移すと次のようになります。

  • For〔C in Cat, F:CopSet in CAT〕For〔A in C
      Ψ(x∈F(A), X in C):C(X, A)→F(X) := λu∈C(X, A).(F(u)(x) ∈F(X))

さらに、定義ヘッド(左辺)の仮引数リストは、定義ボディ(右辺)のラムダリストに移すことができます。距離の例なら:

  • d := λ(a∈R2, y∈R2).(sqrt( (a1 - y1)2 + (a2 - y2)2R)

関手/自然変換の例では(複雑になってきたので改行・インデントします):

For〔C in Cat, F:CopSet in CAT〕
For〔A in C〕
  Ψ :=
  λ(x∈F(A), X in C).(
    λu∈C(X, A).(
       F(u)(x)
    ∈F(X)
    )
  : C(X, A)→F(X) in Set
  )

定義の書き方にバラエティがあるので、標準の形を決めたいなら、例えば(あくまで一例)、定義ボディは名前だけにして、in記法を'∈'に書き換えることにすれば、

For〔C∈|Cat|, F∈CAT1(Cop,  Set)〕
For〔A∈|C|〕
  Ψ :=
  λ(x∈F(A), X∈|C|).(
    λu∈C(X, A).(
      F(u)(x)
    ∈F(X)
    )
  ∈Set(C(X, A), F(X))
  )

さらに、定義コンテキストの一部をラムダリスト内に押し込むことができます。

For〔C∈|Cat|, F∈CAT1(Cop,  Set)〕
  Ψ :=
  λ(A∈|C|).(
    λ(x∈F(A), X∈|C|).(
      λu∈C(X, A).(
        F(u)(x)
      ∈F(X)
      )
    ∈Set(C(X, A), F(X))
    )
  : F(A)×|C|→Nat(C(-, A), F) in Set
  )

このなかの Nat(C(-, A), F) = Nat(C(-, A), F:CopSet) は、CAT2(C(-, A), F) のことですが、Cが小さいので、集合(Setの対象)とみなしたものです。米田の補題から、Nat(C(-, A), F) ¥stackrel{¥sim}{=} F(A) なので、同型をあたかもイコールのように扱えば、最後のプロファイル行は次のように書けます。

  • Set(F(A)×|C|, F(A))

Set(F(A)×|C|, F(A))は、必要に応じて Set(F(A), Set(|C|, F(A))), Set(|C|, Set(F(A), F(A))) とみなすことができます。

おわりに

定義コンテキスト、定義ヘッドの仮引数リスト、定義ボディのラムダリストがいずれもプロファイルリストであり、相互に取り替え可能なことは重要な事実です。型理論と型つきラムダ計算を高次元(とりあえず2次元)に拡張する際のヒントがここにあるような気がします。

*1:区切り記号も、別に何でもいいんですけどね。

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

2018-09-05 (水)

前層の圏における記法と計算

| 18:35 | 前層の圏における記法と計算を含むブックマーク

圏の記法はある程度整備されてますが、圏の圏や関手圏のなかの計算だと、これといった決まりごとはありません。決めておかないと不便なので、おおよその約束ごとをこの記事に書いておきます。関手圏、とくに前層の圏での計算を目的にします。

内容:

  1. 前層の圏
  2. プロファイリングとin記法
  3. ラムダ記法
  4. 等式とon記法
  5. 自然変換に関する等式

前層の圏

射、関手、自然変換に関する演算記号は、「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号」に従います。念のために再掲すると:

演算 反図式順演算子記号 図式順演算子記号
射の結合 ¥circ ;
関手の適用 丸括弧 .
関手の結合 *
自然変換の適用 下付き添字 .
自然変換の縦結合 ¥circ ;
関手と自然変換のヒゲ結合 *
自然変換の横結合 *

“小さな圏”の圏をCatとして、局所小〈locally small〉だが“全体としては大きいかも知れない圏”の圏をCATとします。“大きいかも知れない圏”の圏の定義は、実際には難しい(「圏のサイズとサイズによる“圏の圏”の分類」参照)のですが、深入りしないことにします。扱う圏はすべて局所小で、CatCAT, Set∈|CAT| と考えます。

C, Dに対する関手圏[C, D]は、CDも小さいなら小さい圏となるので、二項(反変-共変)関手 [-, -]:Catop×CatCat として意味を持ちます。しかし、CAT上では関手圏をうまく定義できません。局所小の条件が満たされないからです(例えば、[Set, Set])。

Cが小さくて、D = Set のときは扱いやすいので、共変関手の関手圏[C, Set]と反変関手の関手圏[Cop, Set]は非常によく利用されます。それぞれ、余前層の圏〈category of copresheaves〉、前層の圏〈category of presheaves〉と呼ばれます。前層の圏のほうがよく出てくるので、ここでは前層の圏を扱います。

前層の圏[Cop, Set]の対象は、C上の前層〈presheaf on a category C〉と呼びます。C上の前層の圏をSetCopとも書きますが、上付きの入れ子になるので嬉しくない。短くPSh(C)とも書きます。手書きや印刷物ではさらに短く  ¥hat{¥mathcal{C}}と書くことがあります。ここではCと書くことにします。

  • C =  ¥hat{¥mathcal{C}} = PSh(C) = SetCop = [Cop, Set]

ここでよく使う記法は、Cと[Cop, Set]です。Cが小さくないときは、C上の前層の圏は考えません

プロファイリングとin記法

関手や自然変換を扱うとき、当該の関手/自然変換を“どこで”考えているかにより解釈と扱い方が変わってきます。例えば、Cを小さい圏として、関手 F:CSet があるとき、これは「圏の圏CATの射」なのか、それとも前層の圏Cの対象なのか、それによって解釈と扱い方は変わります。

「“どこで”考えているか?」をハッキリさせることは、関手/自然変換のプロファイルを明確にすることです。プロファイルの明確化=プロファイリング〈profiling〉*1とは、高次圏まで含めた圏論的実体〈categorical entity | categorical thing〉に対して、その次元と所属している区域(圏の一部分)を指定することです。プロファイルの書き方は、「圏論的宇宙と反転原理と次元付きの記法」に従います。

CATに関して、k-射の集合(0-射は対象)を挙げましょう。次元kは上付きで添えます。

  1. |CAT|0 = Mor0(CAT) = Obj(CAT) = |CAT| = {すべての局所小な圏}
  2. |CAT|1 = Mor1(CAT) = {すべての関手}
  3. |CAT|2 = Mor2(CAT) = {すべての自然変換}

つまり、次の同値が成立します。

  1. Cは(局所小な)圏 ⇔ C∈|CAT|0
  2. Fは関手 ⇔ F∈|CAT|1
  3. αは自然変換 ⇔ α∈|CAT|2

関手(1-射)と自然変換(2-射)には両端があるので、それも明示すると:

  1. CAT1(C, D) = Hom1CAT(C, D) = Functor(C, D) = {CからDへのすべての関手}
  2. CAT2(F, G) = Hom2CAT(F, G) = Nat(F, G) = {FからGへのすべての自然変換}

つまり、

  1. FはCからDへの関手 ⇔ F∈CAT1(C, D)
  2. αはFからGへの自然変換 ⇔ α∈CAT2(F, G)

一般に、k-射zを z:(k)x→(k)y のように書きます。ここで、「:(k)」は、セミコロンをk個並べた記号、「→(k)」はk重の矢印です。k = 0 のときは、コロンも矢印もなくて、x, y もないものとします。

  1. k = 0: z
  2. k = 1: z:x→y
  3. k = 2: z::x⇒y

今扱っているCATにおいては、

  1. k = 0: 圏 C
  2. k = 1: 関手 F:CD
  3. k = 2: 自然変換 α::F⇒G

自然変換をより丁寧に表したいなら α::F⇒G:CD のように書きます。F⇒G:CD, F⇒G, CD などが射のプロファイル〈profile〉でした。プロファイルにより、射の次元と所属する区域が確定します。プロファイルの詳細は「圏論的宇宙と反転原理と次元付きの記法」を見てください。

射の両端が分からない/興味がない/不要であるときは、F:?→?, α::?⇒? と書きます。コロンの個数/矢印の太さで次元が分かるので、次のようなin記法〈"in" notation〉が可能になります。

  1. C in CATC∈|CAT|0
  2. F:?→? in CAT ⇔ F∈|CAT|1
  3. F:C→D in CAT ⇔ F∈CAT1(C, D)
  4. α::?⇒? in CAT ⇔ α∈|CAT|2
  5. α::F⇒G in CAT ⇔ α∈CAT2(F, G)

次元を、セミコロン個数と矢印太さで重複して表現しているので、セミコロンだけ書いて F:?, α::? でも問題ありませんが、矢印も書いておいたほうが落ち着く感じはします。

ラムダ記法

(インフォーマルな)ラムダ記法は、関手と自然変換の計算でも役立ちます。つうか、ラムダ記法なしでは辛い! 必須と言っていいでしょう。

関手 F:CD を表現するには、Fを対象部分〈object part〉と射部分〈morphism part〉に分けて、対象部分は F0:|C|→|D| という関数で、射部分はホムセットごとの関数の集まり F1X,Y:C(X, Y)→D(F0(X), F0(Y)) として書き下します。次の形ですね。

  • F0 := λX∈|C|.(F0(X) ∈|D|)
  • F1X,Y := λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))

射部分の表示において、X, Yも変数なので、これもラムダ抽象すれば:

  • F1 := λX, Y∈|C|.(λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y))))

同じ'λ'だと視認性が悪いので、大文字'Λ'にします。これは視認性だけの理由で、'λ'と'Λ'に本質的な違いはありません。

  • F1 := ΛX, Y∈|C|.[λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))]

ΛX, Y の部分は、総称関数における型パラメータなので、∀X, Y と全称記号を使う場合もありますが、'∀'は論理式にだけ使いたいので'Λ'にしました。

結局、関手を定義する形式は:

F:CD :=
  λX∈|C|.(F0(X) ∈|D|)
  and
  ΛX, Y∈|C|.[λf∈C(X, Y).(F1X,Y(f) ∈D(F0(X), F0(Y)))]

これは、対象・射の対応手順を示しているだけなので、関手性〈functoriality〉の証明は別に必要です。上記のように定義された写像の集まりが、関手的〈functorial〉とは、圏の結合と恒等を保存することです; 保存するという性質が関手性です。

自然変換 α::F⇒G:CD は、|C|でインデックスされたDの射の族なので、関手より簡単に表現できます。αの表示は次にようになります。

α::F⇒G:CD :=
  ΛX∈|C|.[αX:F0(X)→G0(X) in D]

Dが一般の圏のときは、αX:F0(X)→G0(X) in D をラムダ記法で表示できる保証はありませんが、D = Set のときはラムダ記法が使えます。

αX:F(X)→G(X) in Set :=
  λx∈F(X).(αX(x) ∈G(X))

組み合わせると:

α::F⇒G:CSet :=
 ΛX∈|C|.[λx∈F(X).(αX(x) ∈G(X)) : F(X)→G(X) in Set]

自然変換の表示も対応手順だけなので、自然性〈naturality〉の証明は別に必要です。上記のαの自然性を主張する等式的命題は次の形です。('on set'は次節で説明します。)

∀f:A→B in C.
∀x∈F(A).
  αB(F(f)(x)) = G(f)(αA(x)) on set G(B)

等式とon記法

等式 x = y において、xとyが所属する集合を明示して、x =A y のように書くことがあります。等号が集合でインデックスされます。インデックスがイヤなときは、x = y on A と書くことにします。さらにAが集合であることを強調したいときは、x = y on set A とします。

集合上の等式以外に、クラス上(on class)の等式と圏上(on cat)の等式を扱います。圏C上の等式はさらに、対象のあいだの等式と射のあいだの等式に分けます。

  • 対象のあいだの等式: A = B on cat C
  • 射のあいだの等式: f = g : A→B on cat C

それぞれ、クラス上の等式、集合上の等式に還元できます。

  • A = B on class |C|
  • f = g on set C(A, B)

Cが小さい圏のときは、対象のあいだの等式も集合上の等式に還元できます。

  • A = B on set |C|

2つの関手F, Gの等しさ、F = G を考えると、とりあえずは F = G on class |CAT|1 ですが、F, Gの両端が等しいのは前提されるので

  • F = G : CD on cat CAT

つまり、

  • F = G on class CAT1(C, D)

前節の関手の表現を考慮すると、上記等式は次のように還元できます。

∀X∈|C|.
  F0(X) = G0(X) on class |D|

∀X, Y∈|C|.
  F1X,Y(f) = G1X,Y(f) on set D(F0(X), G0(Y))

D = Set のときは、

∀X∈|C|.
  ∀x.(x∈F0(X) ⇔ x∈G0(X))

∀X, Y∈|C|.
  ∀x∈F0(X).
     F1X,Y(f)(x) = G1X,Y(f)(x) on set G0(Y)

F = G を証明するとは、上記の2つの命題を証明することです。F, Gが前層(を表す関手)のときは、向きを逆転します。

今まで説明したような、等式を「“どこで”考えているか?」を'on'で明示する記法をon記法〈"on" notation〉と呼びます。

自然変換に関する等式

α, β:F→G in C に関して、等式 α = β を考えてみます。

α, β:F→G は、C上の前層の圏Cの2つの射です。これを、外側の環境CATで考えれば、

  • α, β::F⇒G:CopSet in CAT

したがって、等式は、

  • α = β on set CAT2(F, G)

(クラスではなく)集合上の等式であるのは、Cが小さいことからCAT2(F, G)も小さくなるからです。CAT2(F, G)より、Nat(F, G:CopSet)と書いたほうが事情がハッキリするので、そう書くことにして:

  • α = β on set Nat(F, G:CopSet)

自然変換の等しさは成分ごとに等しければいいので、次のように還元できます。

∀X∈|Cop|.
  αX = βX on set Set(F(X), G(X))

集合圏のホムセット上の等式、つまり写像のあいだの等式なので、値ごとの等しさに還元できます。

∀X∈|Cop|.
  ∀x∈F(X).
    αX(x) = βX(x) on set G(X)

証明のお膳立ての観点から言うと、α = β : F→G on cat C という命題が示すべきターゲット命題として与えられたとき、次のような変形(ターゲットの還元)が許されます。

  Γ |-? α = β : F→G on cat C
 ----------------------------------[自然変換の等値性]
  Γ, X∈|Cop|, x∈F(X) |-?
      αX(x) = βX(x) on set G(X)


このような記法/計算を使う実例は、たぶんそのうち(割とすぐに)出します。

*1:プロファイリングは、型理論における型つけ〈typing〉を高次元まで拡張したものです。