高次圏を考慮した指標の書き方 - 檜山正幸のキマイラ飼育記 (はてなBlog)

多相関数の話はもうしません（一段落ついた）。ですが、「多相関数と型クラス // 指標：いつもの事例で」で、指標の例を出したので、指標の話を続けようかな。高次圏論を考慮して指標の構文を決めるとどうなるか、という話です。

内容：

指標：いつもとチョットだけ違う事例
指標内のキーワードを変える
n-指標とターゲットn-圏
指標のメタ指標とusing
他の指標の利用とimport
おわりに

指標：いつもとチョットだけ違う事例

毎度毎度同じ事例で恐縮ですが、モノイドの例を使います。
...[snip]...
等式的法則として、左単位律だけ書いてあって、右単位律と結合律は省略しています。面倒だからです。

今回は、「省略はしませんがモノイドではない事例」を使います。次の例です。

signature LUnitalPointedMagma in Set {
  type U
  function m:U×U -> U
  function e:1 -> U

  equation lunit :: (λ_U)^-1;(e×id_U);m = id_U
  /* 省略はしてない。これでオシマイ */
}

この指標内に登場する記号 1, ×, λ_U, (λ_U)^-1 の意味は「多相関数と型クラス // 指標：いつもの事例で」を見てください。

この指標で定義される代数構造は左単位的付点マグマ〈left unital pointed magma〉と呼びましょう。マグマ → 付点マグマ → 左単位的マグマの順でだんだん複雑になります。マグマ〈magma〉と付点マグマ〈pointed magma〉の指標も再掲しておくと：

signature Magma in Set {
  type U
  function m:U×U -> U
}

signature PointedMagma in Set {
  type U
  function m:U×U -> U
  function e:1 -> U
}

指標のモデルの圏は Model[-] と書くことにします。ブラケット内には指標名か、指標そのものを書きます。例えば：

Model[PointedMagma]
Model[signature {type U function m:U×U -> U}]

二番目は Model[Magma] と同じです。ごく短い指標以外は、指標名を使うのが普通です。

指標のモデルの圏は、指標名を太字にした名前にするというルールを使います（別に破ってもいいルールですが）。

Magma := Model[Magma]
PointedMagma := Model[PointedMagma]
LUnitalPointedMagma := Model[LUnitalPointedMagma]

モデルの圏の射〈準同型写像〉の定義は、指標から自動的に決まります。それを説明するためには、記法の約束が必要です。Xが指標PointedMagmaのモデル（つまり、PointedMagmaの対象）だとして：

Xの台集合は、X.U と書く。
Xの二項演算は、X.m と書く。
Xの特定要素をポイントする写像は、X.e と書く。

より詳しくは「構造とその素材の書き表し方」参照。

この約束で、モデルの圏PointedMagmaの射〈準同型写像〉f:X → Y in PointedMagma は、次の図式を可換にするような台集合のあいだの写像 f:X.U → Y.U in Set のことです。

$\require{AMScd} \begin{CD} X.U\times X.U @>{X.a}>> X.U \\ @V{f\times f}VV @VV{f}V \\ Y.U\times Y.U @>{Y.a}>> Y.U \end{CD} \\ \:\\ \begin{CD} {\bf 1} @>{X.e}>> X.U \\ @| @VV{f}V \\ {\bf 1} @>{Y.e}>> Y.U \end{CD}\\ \:\\ \mbox{commutative in }{\bf Set}$

圏LUnitalPointedMagmaの射の定義も同じです。左単位的付点マグマを特徴づける左単位律（の等式）は、準同型写像の定義には影響を与えません。また、圏Magmaの射は、一番目の図式の可換性だけを要求します。

インスティチューション理論（そういう理論がある）では、左単位律のような条件〈公理〉は指標とは切り離しますが、「何を条件として切り離すか？」の基準がハッキリしないので（「指標と仕様」参照）、ここでは条件〈公理〉も指標内に記述します*1。

指標内のキーワードを変える

「多相関数の「パラメトリック性 vs 満足性」」にて：

標準的なキーワードは、type, function ではなくて、sort, operation ですが、キーワードに違和感を持つ人が多いので type, function にします。

というわけで、より伝統的なキーワードに戻せば：

signature LUnitalPointedMagma in Set {
  sort U
  operation m:U×U -> U
  operation e:1 -> U

  equation lunit :: (λ_U)^-1;(e×id_U);m = id_U
}

キーワードがどうであれ、Uは集合圏Setの対象で、m, e は集合圏Setの射です。圏論用語をキーワードに使うならば：

signature LUnitalPointedMagma in Set {
  object U
  morphism m:U×U -> U
  morphism e:1 -> U

  equation lunit :: (λ_U)^-1;(e×id_U);m = id_U
}

さらに一歩進めて、高次圏論〈n-圏論〉の用語をキーワードにしてしまいましょう。高次圏〈n-圏〉入門には次の記事があります。

n-圏とは何だろう（2008年）

過去記事の冒頭に注記がありますが、当時と今とでは記法が変わっています。現在僕が使っている記法については次の記事を。

関手と自然変換の計算に出てくる演算子記号とか

さて、高次圏フレンドリーにした指標の構文は：

signature LUnitalPointedMagma in Set {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U
}

対象は0-射（0次元の射）で、通常の射は1-射（1次元の射）です。等式が2-射になってますが、これはどういうことでしょう？集合圏Setは1-圏、つまり、0-射と1-射を持つ圏ですが、実は2-射も（それどころか、任意のk-射を）持つのです。集合圏の2-射とは、1-射のあいだの恒等2-射です。恒等2-射は、1-射のあいだのイコールと同じことです。1-圏における2次元以上の射はすべて恒等射（イコール）になってしまうのです。

1-圏において、k ＞ 1 であるk-射は、すべて恒等k-射（(k - 1)-射のあいだのイコール）である。
一般のn-圏において、k ＞ n であるk-射は、すべて恒等k-射（(k - 1)-射のあいだのイコール）である。

したがって、1-指標の equation を 2-morphism とするのは理にかなっています。2-射（射のあいだのイコール）の宣言を丁寧に書くと次のようです。

2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U:U -> U

一般に、k-射の宣言〈プロファイル宣言〉は次のパターンになります。◯の所には名前や式が入ります。

0-射の宣言 0-morphism ◯
1-射の宣言 1-morphism ◯:◯ -> ◯
2-射の宣言 2-morphism ◯::◯ => ◯:◯ -> ◯
3-射の宣言 3-morphism ◯:::◯ ≡> ◯::◯ => ◯:◯ -> ◯

より一般的で詳しい話は：

n-指標とターゲットn-圏

今まで出てきた指標は、通常の圏、つまり1-圏で解釈する前提です。実際、指標を解釈する圏は集合圏Setだとしてきました。1-圏での解釈が前提の指標を1-指標〈1-signature〉と呼びます。1-指標の解釈の場となる1-圏を（その指標の）ターゲット1-圏〈target 1-category〉と呼びます。集合圏とは限らない圏Cをターゲット1-圏とする1-指標は次の書式になります。

1-signature ◯◯◯ in C {
  /* 0-射、1-射、2-射のプロファイル宣言 */
}

我々の事例である 1-signature LUnitalPointedMagma が任意の圏Cで解釈できるかというと、そうはいきません。LUnitalPointedMagma には次の記号が含まれました。

集合圏ではこれらの記号を解釈できますが、どんな圏でも意味を持つ記号ではありません。だからといって、集合圏Set以外では絶対に解釈できないわけでもありません。'1'を1次元ベクトル空間とみなしたR、'×'をベクトル空間のテンソル積、λをテンソル積の左単位律子〈left unitor〉とみなせば、実係数ベクトル空間の圏Vect_R内の左単位的付点マグマを考えることができます。

それらしくなるように、'1'を'I'に、'×'を'⊗'に置き換えて、Vect_R内の左単位的付点マグマの指標を書くと：

1-signature LUnitalPointedMagma in Vect_R {
  0-morphism U
  1-morphism m:U⊗U -> U
  1-morphism e:I -> U

  2-morphism lunit :: (λ_U)^-1;(e⊗id_U);m => id_U
}

それらしいかどうかは心理的な問題で、まったく本質的ではないので、もちろん元の記号でもかまいません。

1-signature LUnitalPointedMagma in Vect_R {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U
}

記号は決まっていれば何でもいいですが、LUnitalPointedMagmaの1-指標は、モノイド圏で解釈する必要はあります。集合圏Setもベクトル空間の圏Vect_Rも、モノイド圏だからLUnitalPointedMagmaのターゲット圏となり得るのです。

モノイド圏を定義する指標は2-指標となります。次のような形をしているでしょう。

2-signature MonCAT in CAT {
  /* なにやらかにやら */
}

「なにやらかにやら」の部分を実際に書き下そうと思うと、なかなかに難しい問題にぶち当たります。それについては：

とりあえずは難しいことは考えないことにして、次のような2-指標が存在すると信じましょう。

2-signature MonCAT in CAT ：モノイド圏を定義する2-指標
2-signature SymMonCAT in CAT ：対称モノイド圏を定義する2-指標
2-signature CartMonCAT in CAT ：デカルトモノイド圏を定義する2-指標

これらの指標のなかで、各種の圏を構成する関手や自然変換を表す記号が定義されます。使う記号に強い標準はありませんが目安としては：

'⊗', '×' ：モノイド圏のモノイド積、'×'はデカルト積
I, 1 ：モノイド圏のモノイド単位、'1'はモノイド単位兼終対象
α, λ, ρ ：モノイド積の結合律子〈associator〉、左単位律子〈left unitor〉、右単位律子〈right unitor〉
σ ：対称モノイド圏の対称
Δ ：デカルトモノイド圏の対角
! ：デカルトモノイド圏の終射（終対象への唯一の射）
π¹, π² ：デカルトモノイド圏の射影

これらの記号は、適切な2-指標で定義されているとします。射の結合記号';'、恒等射を表す記号'id'、逆射を表す記号'^-1'は、2-指標で定義されるのではなくて組み込み〈builtin〉の記号だとします。

1-指標、2-指標があるなら、0-指標もあるのか？あります。例を出せば：

0-signature abc in X {
  0-morphism a
  0-morphism b
  0-morphism c

  1-morphism bc_eq : b -> c
}

0-指標は、0-圏、つまり集合をターゲットとします。ターゲットXは集合です。0-圏〈集合〉の0-射とは要素です。したがって、指標で3つの要素 a, b, c を宣言しています。ここまでなら、集合Xの3つの要素を意味する指標です。が、0-指標に1-射が出来ています。これは、0-圏の1-射、つまり集合の要素のイコールです。bとcは等しいことを意味します。

それらしいキーワードで書き直すならば：

0-signature abc in X {
  element a
  element b
  element c

  equation bc_eq : b -> c
}

0-指標はあまり面白いものではありません。しかし、もう少し複雑な構文を許すと、0-指標もけっこう面白いものになります（今日は述べない）。

ここで、n-指標のk-射を宣言する“それらしいキーワード”をまとめておきましょう。確かに“それらしい”のですが、ゴチャゴチャとして統一性を欠き、俯瞰的な理解を阻害している要因だとも言えます。

	0-指標	1-指標	2-指標
0-射	element	sort, type, object	sort, kind, object
1-射	equation	operation, function, morphism	operation, morphism
2-射		equation	2-operation, 2-morphism
3-射			equation

心理的な“それらしさ”を取るか、理論的な整合的性を取るか？一概には判断できませんが、統一的・俯瞰的な理解を目指すなら、“それらしさ”は犠牲にするしかありません -- キーワードは味気ない番号（次元）で区別することになります。

指標のメタ指標とusing

1-指標のなかで、0-射〈対象〉Xに対する恒等射 id_X と、2つの射〈1-射〉 f, g の結合 f;g は自由に使ってかまいません。なぜなら、1-指標のターゲットは1-圏〈通常圏〉なので、恒等射も射の結合も備えているからです。しかし、モノイド積（双関手）やモノイド単位、なにか特別な対象（例：始対象、終対象）、なにか特別な自然変換（例：対角や射影）を使いたいときは、それらの関手や自然変換を表す記号がどこかで宣言されている必要があります。

関手や自然変換を表す記号を宣言するのが2-指標です。具体的には、2-signature MonCAT in CAT, 2-signature SymMonCAT in CAT, 2-signature CartMonCAT in CAT などです。1-指標を書くときは、その1-指標の親玉となる2-指標を選択する必要があります。1-指標のメタ指標〈meta signature〉と言ってもいいでしょう。

メタ指標の指定には using というキーワードを使うことにします。

using 2-signature CartMonCAT
1-signature LUnitalPointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U
}

この1-指標で使われている名前・記号を色分けしてみます。

任意の圏で使える組み込みの記号は赤色
メタ指標で宣言されている記号はオレンジ色（メタ指標の名前もオレンジ色）
この指標で宣言されている記号は水色（この指標の名前も水色）

using 2-signature CartMonCAT
1-signature LUnitalPointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U

  2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U
}

こうして見ると、出現しているすべての名前・記号は、どこかで宣言されていることが分かります。組み込みの記号か、メタ指標で宣言済みか、当該の指標で宣言されているかです。正体不明の記号はありません。正体不明の記号をなくすことで、指標による記述の精密さを担保したいのです。

この 1-signature LUnitalPointedMagma には、ターゲット1-圏が指定されていません。指標にターゲット圏が指定されてないときは、モデルの圏を作るときにターゲット圏を指定します。Model[LUnitalPointedMagma, Set] のように。ここで、ターゲット圏は何でもいいわけではありません。指標（1-指標）のメタ指標（2-指標）のモデルである圏に限られます。今の例では、1-signature LUnitalPointedMagma のメタ指標は 2-signature CartMonCAT なので、ターゲット圏はデカルトモノイド圏である必要があります。

1-指標のメタ指標である2-指標は、1-指標で使う記号を提供するだけではなく、1-指標のターゲット圏の種類も規定します。メタ指標（である2-指標）は、1-指標と、それに関連する構文論／意味論のすべての部分に影響します。2-指標をドクトリン〈doctrine〉と呼ぶこともあります。実際、2-指標＝ドクトリンは、構文論と意味論が絡み合った組織体を統制する教義〈基本原理〉になっています。

他の指標の利用とimport

指標（単に指標と言えば1-指標）を書くときに、既にある他の指標を利用したいことがあります。例えば、1-signature LUnitalPointedMagma は、1-signature PointedMagma に等式〈2-射の宣言〉を付け加えただけです。付け加える差分だけ記述できれば便利です（いわゆる“継承”のような書き方）。

他の指標を利用可能とするためのキーワードは import にします。次が import の使用例です。

using 2-signature CartMonCAT

1-signature PointedMagma {
  0-morphism U
  1-morphism m:U×U -> U
  1-morphism e:1 -> U
}

1-signature LUnitalPointedMagma {
  import 1-signature PointedMagma

  2-morphism lunit :: (λ_U)^-1;(e×id_U);m => id_U
}

import 1-signature PointedMagma の部分に、1-signature PointedMagma の内部がそのまま展開されると思えばいいです。複数の指標をインポートするときは、名前のバッティングの問題を処理する必要がありますが、今日は触れません。

おわりに

高次圏を考慮した指標の書き方を紹介しました。実際のところ、指標について調べるには、高次圏は避けられないでしょう。1-指標の構文と、意味論のためのターゲット1-圏は、メタ指標である2-指標によって支配されます。その2-指標の構文と、意味論のためのターゲット2-圏は、さらにメタ指標である3-指標により支配されます。その3-指標の‥‥ 無限に続きます。

この無限に続く構文論・意味論のタワーは、僕をずっと悩ませてきました。精神安定のために、有限階で安定的に循環するのだ、と信じています（例えば「デカルト・タワーを求めて」参照）。有限階を考えれば十分だと保証できれば、安心できます。

特に、2-指標と2-圏まで考えれば十分な状況が作れれば、特定の2-指標をメタ指標として固定して、そのメタ指標で支配される1-指標達の議論ができます。無限タワーの2階までを自由に使いこなせれば、それだけでも、かなりの程度の構文論・意味論が展開できます。そのとっかかりは「指標とは何か？」をハッキリさせることです。

*1:構成素と条件の境界線が恣意的になってしまう気がします。必然的な境界線が存在するのでしょうか？わかりません。