…on）で使われる絵はストリング図（string diagram）と呼ばれます。とある文書でストリンググラフ（string graph）という言葉を見たんですよね。ストリング図の同意語だろう、と思ってました。しかし、ストリンググラフの定義のなかで"node vertex"なんて奇妙な概念が出てきて、「はぁ、なにそれ？」 -- 少し調べてみました。内容： ストリンググラフの起源と参考文献 ストリング図を幾何学的に眺める ストリング図の組み合わせ的な表現 ストリンググラフの起源と参…

…則の左辺・右辺の項をストリング図で表すと、同型は2次元図形の変形になるので、その軌跡は3次元の図形になります。結合律を表す結合律子（associator）の形状は次の動画で確認できます。これ、いまいち分かりにくい気もします。手前味噌ですが、僕が昔描いた立体図がけっこう分かりやすいかと。双対／随伴を表すニョロニョロ法則を表す図形の動画もあります。動画タイトルは、zigzagerator。ニョロニョロ法則はジグザグ法則とも呼びますからね。もちろん、snakerator（ニョロニョ…

…事例 DOTN二号とストリング図 今後使う予定の演算子記号 酷い話https://en.wikipedia.org/wiki/Natural_transformation では、自然変換の縦結合と横結合について、次のような記法を採用しています。 縦結合： η : F → G と ε : G → H に対して、その縦結合は εη : F → H 横結合： η : F → G : C → D と ε : J → K : D → E に対して、その横結合は ηε : JF → KG…

…を使って絵を描くと、ストリング図のストリングが幅を持ったストライプになるので、描かれた絵をストライプ図と呼びます。立体的に描いたときはチューブ図とも呼ぶようです。先に引用したBourke and McCurdyの論文には、色鮮やかなストライプ図による計算・証明が載っています。さて、ストライプ図を使って、モノイド関手の構造射である μA,B:F(A)F(B)→F(AB) と ε:I→F(I) を描くと次のようになります。この絵で採用した描画方向（「絵算の描画方向を示すために旗を…

…ックス＆ワイヤー図、ストリング図）と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏（polycategory）という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。 2011年1月 デカルト閉圏を計算するスタックマシン、シーケント計算、カリー／ハワード対応 タプルの一変数じゃなくて多変数の関数を扱うなら、普通の圏より複圏（multicategory）のほうが便利です。多値関数も含めるなら多圏（polycategory）を使うと…

…かしながら、「絵算（ストリング図）における池袋駅問題の真相」で指摘したような問題があります。絵の描き方、特に方向の取り方は人によりバラバラなんです。地図では、北が上で東が右と決まっています。もしこの決まりがなくて、地図ごとに方向の取り方がバラバラだったら、随分と不便だと思いませんか。現状のストリング図の状況は、北をどちらにするかが決まってなくて地図が流通しているようなもんです。当面、方向の取り方を統一するのは無理です。地図の方向の取り方がバラバラでも、北を示す方位磁針の印が描…

…おいては、テキストもストリング図（下に例）も変わりはありません。違うのは、ストリング図（や3次元内の曲面を使うサーフェイス図）が、本質的に2次元以上の空間を必要とすることです。[*1] [*2] [*3]テキストだって2次元に配置されますが、あれは折り返しているだけ*4。音声読み上げでテキストを時間方向に展開できるのは、実質的に1次元しか使ってないからです。ストリング図では、上下方向も左右方向も意味を持ちます。サーフェイス図なら奥行き方向も使います。抽象化した文字形状をグリフ…

…。しかし、高次圏論とストリング図をベースにしたソフトウェアが現に動いているという事実は素晴らしいと思います。Globularが存在することが、新しい認識／新しい問題意識／新しい課題／新しい世界観を生み出す契機になるかも知れません。Globularの機能不足や使い勝手の悪さに文句をたれるのは容易ですが、ではどうしたらいいのかを提案するのは難題です。このテのソフトウェアを設計・実装することの困難さが身に沁みて分かります。Globularを触ってみて、僕が深刻な問題だと感じたのはコ…

…いでしょう。いつものストリング図です。添字を省略してしまうと、 (γP);γ = (Pγ);γ : PPP→P なので、モノイドの結合律と同じです。左単位律、右単位律も同様です。構造同型射α-1、λ-1、ρ-1まで入れた正確な形を、結合律も含めて書き下せば： αP(a, b),P(b, c),P(c, d)-1;(γa,b,cP(c, d));γa,c,d =(P(a, b)γb,c,d;γa,b,d : P(a, b)(P(b, c)P(c, d))→P(a, d) λP(…

…変形：対応する絵算（ストリング図）：次に、ヒンズ論文p.5の命題です。テキストによる等式的変形：対応する絵算（ストリング図）：ヒンズ論文では、定義や法則を引用しながら、何段階かの等式的変形（equational reasoning）をしてますが、絵算では描いてしまえば一目瞭然、特に計算・証明すべきことはありません。何もしなくても命題は明らかだと判断できます。何を説明するのか前節の2つの命題は次でした。今は意味不明でかまいません。 (α∩)∪ = α (∪α)∩ = ∪(α∩)…

…にオススメする3つのストリング図解説 （とオマケ）」という記事を書きました。絵算（お絵描き計算、pictorial/graphical/diagrammatic calculation）は、圏論の理解や計算を、図式を使って行う方法です。使用される図式をストリング図（string diagram）と呼びます。最近、ストリング図の良い解説を見つけました。ダニエル・マースデン（Daniel Marsden）の次の論文です。 Title: Category Theory Using …

…ンカレ双対を取ると、ストリング図となります。ストリング図では、圏が2次元（面）、関手が1次元（線）、自然変換が0次元（点）となります。習慣として、自然変換は大きさを持たない点ではなくてボックスやオダンゴで表されることが多いです。下の図の左側は上と同じドット＆アロー、右側が対応するストリング図（オダンゴ図）です。ドット＆アロー図とストリング図のポアンカレ双対については、ウィラートン（Simon Willerton）がきれいな絵を描いているので、それを引用します。ウィラートンは「…

…っているのは2次元のストリング図の操作で、主に自然変換の計算をします。言葉を変えると、小さい圏を対象とする2-圏Catのなかでの縦方向／横方向（vertical/horizontal）の計算です。このセッティングは、絵算がうまくハマる状況のひとつです*1今述べた状況で、キュリアの絵算とDOTN二号を、その背景と考え方を含めて紹介します。内容： ズボラ・イイカゲンの精神 種類が多すぎる！ 格上げ操作 細かい印はメンドクセー ズボラ・イイカゲンの精神圏論の計算は抽象度が高くそれな…

…的な計算法です。絵（ストリング図）だけでなく、テキスト記法でも使えます。発想は別に難しくはありません（気づくのは難しい）。自然変換 α::F⇒F をストリング図では次のように描きます。（面倒なのでアスキーアートで。） F | (α) | G ひとつの圏の内部の射 f:A→B は次のように描きます。 A | (f) | B 絵としては同じなので、だったら混ぜちゃえ、というわけです。混ぜるために、射のほうを自然変換に“格上げ”して、計算は自然変換の世界で行います。問題は「どうやっ…

…にオススメする3つのストリング図解説 （とオマケ）」において、ピエル-ルイ・キュリア（Pierre-Louis Curien）の "The Joy of String Diagrams"（http://hal.archives-ouvertes.fr/docs/00/69/71/15/PDF/csl-2008.pdf）について、「圏論がある程度わかったら、ストリング図入門の最初に読むのにいいと思います。」と言ったのですが、これは取り消します。最初に読むにはちょっと難しいです。…

…痴っています。絵算（ストリング図）はすごく便利なんですが、人によって描き方がバラバラ、絵に限らずテキスト記法もバラバラ、それが混乱や誤解をまねくし、いろいろな流儀に慣れるのも大変だ、ってことです。さて、昨日の記事「絵算したい人のためにオススメする3つのストリング図解説 （とオマケ）」で、ストリング図の解説をいくつか挙げました。もう一度繰り返します。キュリア： Title: The Joy of String Diagrams Author: Pierre-Louis Curi…

…然変換の計算に必要なストリング図の基礎が10ページにまとめてあります。圏論がある程度わかったら、ストリング図入門の最初に読むのにいいと思います。←[追記]最初に読むにはふさわしくないかも。理由はそのうち説明します。[/追記]←[さらに追記]「キュリアの絵算」に説明を書きました。[/さらに追記] 次は、ポール-アンドレ・メリス（Paul-Andre Mellies、http://www.pps.univ-paris-diderot.fr/~mellies/）の "Functor…

…論／証明 写像の計算 自然変換の計算 証明図 計算図 ストリング図 自然変換の「シフト（shift）」という言葉は次の論文で使われていた用語です。 Ralf Hinze, "Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick." http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf 「アンシフト」はシフトの逆として、僕が勝手に使っているだけです。

…しいお絵描き 絵算（ストリング図）は一般的にかなり使われていますが、徹底して左から右の図式順記法はあんまり使われていません（ユーザーは僕だけかも ^^;）。致し方ないので、バイダイレクショナルな記法を説明します。しかし、次の点は譲れないです。 射の結合（composition）は、左から右に f;g と書く。気になる人は、f;g が出てきたら g・f に置き換えてください。 自然変換αのA成分は、αA と下付き添字が普通です。が、テキストエディタで書くときに負担なので、ブラケ…

…ますし、圏論界隈ではストリング図（string diagram）と呼ぶことも多いです*2。僕のこのダイアリー内で説明用に出てくる絵図は（たいてい）ストリング図です。すぐ下の絵は、白旗優（しらはた・まさる）さんの論文 "Geometry of Interaction explained" (http://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/43041/1/1318_19.pdf) からの引用です。これだってフ…

… diagram）とストリング図（string diagram）が典型的です。1次元のときのグロービュラー図*1は、通常のドット＆アロー図となります。ストリング図は、グロービュラー図のポアンカレ双対となります。ストリング図のほうが図形的直感*2が効くので、実際の計算にはストリング図が便利でしょう。高次圏（n-圏）では、絵図は「便利な表現法」ではなくて、定義の一部になります。そのへんの事は以前少し書いたことがあります。 n-圏とは何だろう おとぎ話としてのn-圏 -- 計算でき…

…使って示せます。絵（ストリング図）が描ければ、お決まりの変形です。実を言うと、絵算ではイコールと同型の区別がつきにくくて、やっているうちに、up-to-isoかon-the-noseかが分からなくなります。今でも分からないままですが、まー、いいでしょ。計算の途中で、余二項演算 δ：I→I□I が余結合律と余単位律を満たしていることも使います。僕は今まで意識してなかったのですが、モノイド圏の単位Iは、自明にモノイドかつコモノイドになっているんですね。豊饒圏との関係Xを集合（大き…

…、グロービュラー図やストリング図を駆使する絵算派とは対極的で、テキスト記号で頑張るやり方です。そのコォゼンが、関手と自然変換の計算をベクトル空間のスカラー乗法に例えていました； 紹介します。F, Gなどを関手、α, βなどを自然変換として、関手の反図式順結合を「・」で表します。関手Fと自然変換αの結合を次のように定義します。 (α・F)X := αF(X) 「・」の左右を入れ替えると定義が変わります。 (F・α)X := F(αX) 記号「・」を次の3つの意味でオーバーロード…

…んな人々により再発明された技法なので、方言があるのは当然だし、名前さえないのですよね。僕もなんて呼ぶか分からなかったので、2004年の末に勝手に命名したことがあります。 ETBダイアグラム http://www.chimaira.org/docs/EtbDiagrams.htm 最近は「ストリング図」（string diagram）と呼ばれることが多い気がしますが、「バードトラック」も悪くないですね。 [追記]もう冗談としか思えない。確かにこれじゃ組版が大変だろう。[/追記]

…ワイヤー図、あるいはストリング図において、ワイヤー（ストリング）の並置はモノイド積を表します。モノイド積が2種類、例えば×と＋があると、単に並置するだけではどっちの積か分かりません。そこで、ワイヤー間の帯状領域に色を塗って区別することにします。例えば、×が赤、＋が青とか、3色ペンの出番ですぜ。また、A, B, C 3本のワイヤーがあるとき、「AとB」、「BとC」のどちらを先に演算するかを示すために、束ね糸を使うことにします。このお絵描き方式で分配律を描くと次のようです。分配律…

…プを作って、モナドやストリング図に関するビデオをYouTubeに投稿しているぞ！ これは、テクノロジーをほんとに有意義に使っている素晴らしい例だね。 Eugenia Cheng and Simon Willerton have formed a little group called the Catsters - and under this name, they've put some videos about monads and string diagrams onto…

…対（dual）であるストリング図を用いるほうが絵算です。どっちもグラフィカルな方法なので、別になんと呼ぼうといいんですが、図示の流儀は異なるのです。先に述べたように、例がないので、例を自分で追加しないと耐えられない感じだと思います。有限集合の圏をメインに使うといいかな。「紹介：Web上で圏論をグラフィカルにデモ」で紹介したサイトも利用するといいでしょう。線形（線型）代数を知っているなら、ベクトル空間と線形写像の例もけっこう実感が湧きます。二、三の注意圏の射は写像とは限らないし…

…ンゴを小さくした図はストリング図と呼びます。superstring04さん曰く： ｆ＾はｘを引数として、得体の知れないものを返している。この得体の知れないものがλｙ．（２ｘ＋ｙ）に対応する。 ｆ＾＾は引数を取らず、しこたま得体の知れない λｘ．λｙ．(２ｘ＋ｙ) というものを返す関数、とわかる。 「得体の知れないナニカ」という認識はまったく正しいです。ラムダ式（小さなラムダ式）の実体が何であるかを詮索しても不毛なんです。Eと書かれたevalとかapplyと呼ばれる関数（高階関…

…ックス＆ワイヤー図、ストリング図）と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏（polycategory）という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。僕が想定しているシナリオでは、ラムダ計算も命題論理もお絵描き（回路図）ありきなので、絵が描きやすいことが最優先の定式化になっているのです。 *1:セミナーで提示した系では、破棄を禁止したので技巧的変形が残ってしまいました。証明図＝大きなラムダ式の出力を1つに限りたか…

…準備：ボックス図からストリング図へ 準備：徹底的に左から右の記法 自己関手の圏End(C) 余談：圏論は、ほぼ計算だけ 厳密モノイド圏 実例：行列の圏 実例：非負の実数 実例：釘にラベルが付いたブレイド図の圏 ほんとに面白いのは モナドはモノイドだ -- 言ってるだけ実は、「モナドはモノイドだ」ということは、アッチコッチで断片的に述べてます。「無理して(圏論的)モナドをJavaで説明してみる」の「モナドの効用」のところで、 モナド結合律とモナド単位律が、通常の（例えば整数の掛…