結び目を勉強しなかった不徳
次の本を渋谷の本屋でパラパラめくっていた。
- 作者: 小島定吉
- 出版社/メーカー: 朝倉書店
- 発売日: 2002/10/01
- メディア: 単行本
- クリック: 4回
- この商品を含むブログ (5件) を見る
146ページ以降に、いつも僕が絵算で描いている図がワラワラと出てきてビックリした。冷静になってみれば、ブレイド圏などが3次元トポロジーや位相的場の量子論（TQFT）に関係するのだから、まー、サモアリナンなんだけど。
しかし、タングル基本図式がストレートな単一線、2種のブレイド生成元（互いに逆）、Kelly単位／余単位に対応する半円形なのか（P.147）。これらで自由生成される図形に同値関係を入れるのだが：
- 縦スライドは、僕がストレートジャンクションの伸ばし／縮め、射のずらし（シフト）と呼んでいるものだ。
- 極点対の消滅は、ジグザグ公式、または剛性だ。
- 交点の回転は、クロスオーバー公式とクロスの計算をあわせたものだろう。
ヤンキングとアルチン・ブレイド関係式に相当するライデマイスター移動（ヤンキングがそのI, アルチンがII, III）と、上の縦スライド、対消滅、交点回転をトゥラエフ（Turaev）移動と呼ぶそうだ。トゥラエフ移動で移る図式はイソトピーらしい。
うーむ、、、しかし、僕は激しくあさはかだった。むかーし、図書館で結び目理論の翻訳本（おそらくクロウェ ル＆フォックス 寺阪＆野口訳）を見つけたことがあった。そのとき僕は、結び目理論は箱庭みたいなもんだと思った。趣味的に面白いかもしれないが、小さな閉じた世界と感じたわけだ。広がりや普遍性がないものが好きでなかった僕は、こんなものは勉強するに値しないと判断した。
これはとんでもないオオマチガイだった。タングル、絡み目、結び目、ブレイドは、今や整数論から数理物理まで、そして圏論にも多大な影響と刺激を与える壮大な理論になってしまった。素数も量子重力場も、その根源はタングルや結び目のようなものだというハナシまである。あのとき、あの本をちゃんと読んでいれば、、、と、そんな後悔ばっかし。
多圏上のシーケント計算
シーケント計算は、別に論理と考える必要はなくて、単なる計算法と割り切ったほうがいいようだ。
トレース付き対称多圏（traced symmetric polycategory）を考えることはできる。そこでの計算はシーケント計算が便利。まずは、トレースによるカット（trace-cut）を基本推論として導入する。
Γ, x ⇒ Δ, x
----------------[trace]
Γ ⇒ Δ
トレース・カットを使って伝統的なカットを導いてみる。
Γ ⇒ Δ, x x, Φ ⇒ Ψ
-------------------------[monoidal product]
Γ, x, Φ ⇒ Δ, x, Ψ
-------------------------[symmetry]
Γ, Φ, x ⇒ Δ, Ψ, x
-------------------------[trace]
Γ, Φ ⇒ Δ, Ψi.e.
Γ ⇒ Δ, x x, Φ ⇒ Ψ
==========================[cut]
Γ, Φ ⇒ Δ, Ψ
これって、f;g = Tr[(f×g);σ] のことだ！
命題変数に順序が入れば、それから公理系を作れる。図形的には有向グラフから多圏を作って、その上でシーケント計算することになる。極性（polarity）は否定（negation）として解釈することもできるだろうし、ベキがあればそれはimplicatioになる。
そういや、白旗さんも線形論理の文脈でコンパクト閉圏を持ち出していたし、線形分配圏（多圏）も線形論理から来ていた。線形論理には近付きたくなかったのだが、なんか引き寄せられているような、、、
Janusと圏／多圏
ベースとなるトレース付き（対称）モノイド圏Cだが、これはセオリーの列(A1, ..., An)またはセオリーのレコード{a1:A1, ..., an:An}を対象とする。射f:A→Bは、ライブラリ／プラットフォームBを使ってサービスAを提供するプログラムになる（「プログラム」って何だ？ってことにはなるが）。
Cのなかに、振る舞い正規化（マイヒル／ネロード関手）とそれによる振る舞い同値関係を入れて、この同値関係と整合する振る舞い関手を定義したい。
コンポネントの圏は、CからInt構成で作る。一方で、Cに対応するtraced symmetric polycategory Poly(C)も作っておきたい。Int構成は多圏の圏でも使えるかな？ そもそも多圏の圏のmorphismをどう定義すべきか？polyfunctorか、morphism of polycategoriesなのか？ いずれにしても圏PolyCat、SymmPolyCat、TrPolyCat、ComClPolyCatなんかが必要。
