…れらの圏の計算では、ストリング図を使うのが便利です。このブログでは、図式の描画に園部さんの XyJax（Xy-pic の MathJax 版）を使っています。XyJax は可換図式には非常に便利で、ペースティング図もなんとか描けます。が、ストリング図には向いていません。向いてないけど、カリー化を無理して描いてみます。（トレースと不動点は、いずれまた。）記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\…

… 1/n」において、ストリング図で説明しています。過去記事では、$`\cat{C}^A`$ ではなくて $`\cat{C}_{(A \times)}`$ という記法を使っています（要注意）。また、別な過去記事「不動点理論と対角自然性（dinaturality）」でも同様な話題を扱っています。こっちの過去記事では、記法 $`\cat{C}^A`$ を使っています（今回の記事と同じ記法）。インデックス付き圏〈indexed category〉であることを強調したいときは $`\c…

…ためのコスト 「層化ストリング図 // 裏返し反変関手」で導入した、C の裏返し関手〈reversing functor〉 $`\mrm{Rev}_\cat{C}`$（対象パートも射パートも恒等写像であるほんとの反変関手）と、オーバーライン記法を使うと、次のような公式が成立します。 $`\o{f} = \mrm{Rev}(f)`$ $`F^\op(\o{f}) = \o{F(f)}`$ $`\o{F^\op(\o{f})} = F(f)`$ ほんとの反変関手（「イイカゲンとイ…

…cdot}\ar[r] &{\cdot} } `$この図の上のほうは $`\lrcorner+`$ で、下のほうは $`\urcorner-`$ で描いています。8種類の描画規約すべてが実際に使われる可能性があります。ストリング図はペースティング図のポアンカレ双対なので、やはり8種類の描画規約があります。しかし、「ペースティング図 ←→ ストリング図」の対応は一意的には決まりません。どのように対応付けるかも恣意的な選択になってしまいます。そのことについては次の機会に述べます。

…規約が色々あります。ストリング図の描画の規約も色々です。かなり面倒くさい状況になっているので整理しようと思ったら、作用亜群とその上の前層を持ち出さないと無理な感じがしてきました。という事情で、この記事では、作用亜群とその上の前層について述べます。出てくる具体例は、二重圏の描画規約に関連するものです。記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\m…

…関わる概念や計算を、ストリング図（ワイヤーとノード）を使ったグラフィカル・ラムダ計算の枠組みに取り込もう、というものです。この計画は半分忘れてましたが、最近またちょっと考えてみました。過去にやったことをうまくまとめる方法を思いつきました。また、新しいことも少し分かってきました。この記事では、グラフィカル・ラムダ計算の全体像をキューブ〈立方体〉の図を使ってまとめます。今回強調したい話題のひとつは、小学校で習った掛け算に関する概念を、モノイド圏／2-圏の文脈で徹底的に復習すること…

…は「ベンド」）は、“ストリング図のワイヤーがカーブしたところ”の意味で使っていました。ワイヤーの“曲がり”は次のような場面で登場します。 デカルト閉圏におけるカリー化／反カリー化 デカルト閉圏とは限らないテンソル-ホム・随伴系〈tensor-hom adjunction〉 コンパクト閉圏の双対性の単位と余単位 コンパクト閉圏とは限らないリジッド・モノイド圏〈rigid monoidal category〉の強双対性〈strong duality〉*1の単位と余単位 トレース付…

…。1次元のメッシュがストリング図の形状を与えます。したがって、n次元のメッシュは高次元ストリング図の形状の候補となります。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} %\newcommand{\msf}[1]{\mathsf{#1}} %\newcommand{\mbb}[1]{\mathbb{#1}} %\ne…

…が日常的に使っているストリング図と相性がいいアプローチが欲しかったからです。カローラ・アプローチは、ストリング図を直接に定義する、ストリング図のためのアプローチです。カローラ・アプローチには明白なメリットとデメリットがあります。 メリット： 低次元での利便性 デメリット： 高次元での複雑性 次元が 3 までなら、メリットが勝ります ―― 便利です。が、4 以上の次元では、デメリットである複雑性が目立ってきてシンドくなります。よって、カローラ・アプローチの適用範囲は低次元（3次…

…記述も計算も簡単で、ストリング図を徹底的に利用することができます。すべての複圏／多圏をポリモノイド圏で置き換えられるわけではありませんが、論理や型理論に出現する複圏／多圏の多くはポリモノイド圏で代替可能です。この記事でポリモノイド圏を導入・定義します。具体例や応用の詳細は別な機会に回しますこの記事の説明のなかで知識グラフ（用語・用法図を含む）を使います。知識グラフ／用語・用法図については、以下の過去記事を適宜参照してください。 パンダ用法と用語・用法図 用語・用法図から知識グ…

…然言語記述や他の図（ストリング図やペースティング図）による記述も遠慮なく使う、ということです。知識グラフは記述・説明の手段と割り切って、定義や証明には（無理には）使わないのも方針です。知識グラフを使った推論はある程度はできるだろうし、面白い話題ですが、過剰な期待はしないことにします。知識グラフが定義や証明の補助にはなっても、主役にはなれないでしょう。不均質性意図的というより結果的なんですが、知識グラフは複数の目的を持ち、複数の手法を併用・混合しています。 構文記述と意味記述 …

僕は、ストリング図やペースティング図が好きです。数式（論理式も含む）や自然言語文より、絵図〈picture | diagram | figure | graph〉による表現を好むという意味で絵図主義者です。絵図によって伝えたいことは、なんらかの形式のテキストでも表現できます。絵図はテキストにシリアライズ可能なわけです。それなら、絵図なんて不要なのではないか？ いえ、違います。絵図とテキストでは“わかりやすさ”〈認知的負荷〉がまったく違います。人間は、入り組んだ数式や自然言語文…

…\ {} &{\T{ストリング図}} \\ {} &{\T{可換図式}} \ar@{_{(}->}[d] \\ {\T{【曖昧】図式}} \ar[uuur]^1 \ar[uur]^2 \ar[ur]^3 \ar[r]^4 \ar[dr]_5 \ar[ddr]_6 &{\T{ペースティング図}} \ar@{_{(}->}[d] \\ {} &{\T{コンピュータッド}} \ar@{=}[r] &{\T{ポリグラフ}} \\ {} &{\T{図式的ヘテロ射} } \ar@{}[u…

…\ {} &{\T{ストリング図}} \\ {} &{\T{可換図式}} \ar@{_{(}->}[d] \\ {\T{【曖昧】図式}} \ar[uuur]^1 \ar[uur]^2 \ar[ur]^3 \ar[r]^4 \ar[dr]_5 \ar[ddr]_6 &{\T{ペースティング図}} \ar@{_{(}->}[d] \\ {} &{\T{コンピュータッド}} \ar@{=}[r] &{\T{ポリグラフ}} \\ {} &{\T{図式的ヘテロ射} } \ar@{}[u…

…んペースティング図かストリング図に変換して、ペースティング図／ストリング図に対して意味を割り当てます。この記事のなかでも、暗黙にペースティング図への変換は使っています。実は、次のパターンの知識グラフを、その下のペースティング図に変換していたのです。$`\quad\xymatrix{ {} &{\T{【一般名】◯◯}} &{} \\ {\T{【役割り名】☓☓1}} \ar[ur]^{\T{part-of}} \ar[d]_{\T{should-be}} &{} &{\T{【役割…

依存型理論にストリング図が効果的に使えることが分かりました。このときストリング図の形状である半グラフに、型・名前・番号など様々な属性を考える必要があります。つまり、属性付き半グラフを使うわけです。そこで、属性付きグラフ／属性付き半グラフについて再確認しようと思います。属性付きグラフ／属性付き半グラフについては以下の過去記事で述べています。 属性付き2次元グラフ： 図式言語の基本 属性付き半グラフ 今回の記事で再び属性付きグラフ／属性付き半グラフについて述べますが、今回は、より…

…えることが出来ます。ストリング図〈string diagram〉やケリー／マックレーン・グラフ〈Kelly-Mac Lane graph〉などの絵図的表現と相性がいいのも $`\HoareAutom`$ 魅力です。隠蔽指標のモデルゴグエン指標を対象とする圏を $`\mbf{GogSign}`$ とします。「ゴグエンとローヴェアの世界観」で述べた処方箋を $`\cat{S} := \mbf{GogSign}`$ のセッティングで適用すると、次のファイブレーションが得られます。$…

…ンズ 最初の一歩： ストリング図を中心に 形容詞「無法則」が便利なので、指標に対しても使うことにしたのです。以下の記事も参照してください。 有法則代数と無法則代数 オブジェクト指向風の指標前節の指標の例は代数系〈代数構造〉を定義するものでした。この節では、オブジェクト指向風にデータ構造とメソッドを定義する例を挙げます。オブジェクト指向風の指標では、状態空間を表すソート〈型 | 集合〉を特別扱いします。確かに特別扱いする必要はあるのですが、特別扱いの程度にバラつきがあり、分かり…

…`G`$ は、「層化ストリング図 // 裏返し反変関手」で導入した裏返し関手〈reversing functor〉を用いて $`\mrm{Rev}_{\mbf{SS}}*G`$ と書けます。反対圏と反変関手の扱いは、かなりイイカゲンと言わざるを得ません。興味があれば、次の過去記事も参照。 イイカゲンとインチキを悔い改めるためのコスト [/補足]インデックスだけで考えると、$`\mbf{SS}`$ の恒等射以外の一般の射は、次の形です。$`\quad (k, i_0); (k …

…、コンピュータッド、ストリング図 また、アタッチメントと自由拡張の繰り返しはCW指標〈CW signature〉とも同じことです。 CW指標とCWテレスコープ（実例） コンピュータッドもCW指標も、指標と指標が生成する圏（高次圏含む）を定式化するための構造です。コンピュータッド／CW指標の定義は色々ありますが、アタッチメントと自由拡張の繰り返しは議論をスッキリさせる効果がありそうです。 *1:「(k - 1)-圏である」という仮定は落として、必要なときに追加するほうが良いかも…

…`$ 「米田の補題とストリング図 // 米田同型」に従い、米田写像をフラット記号、米田写像の逆写像をシャープ記号で表すことにします$`\quad (\hyp)^\flat : \mrm{Nat}(よ^a , F)\to F(a) \In \mbf{Set}\\ \quad (\hyp)^\sharp : F(a) \to \mrm{Nat}(よ^a , F) \In \mbf{Set} `$ 音楽記号〈musical notation symbol〉を使う記法は微分幾何で使わ…

…は完全に忘れたい。 ストリング図やオペラッド〈複圏〉と相性が良い構文にしたい。 格納されたデータと論理的な条件を同等に扱いたい（WHERE句をテーブル扱いしたい）。 データ型は抽象的・概念的な構造として定義したい。 通常のプログラミング言語と同様に変数・関数を使いたい。 単純明快で夾雑物がなくスッキリしていることが第一で実用性なんてもんは考えません。この記事の最後に、この記事と引き続く記事の「動機と目的と方針」を書いています。最後の節を最初に読むほうがいいかも知れません。$`…

…ース付きモノイド圏のストリング図における縮約は、外部辺の架橋〈bridging〉（または架橋した後で縮減）に対応します。架橋と縮減は別な操作です。といった事情で、半グラフに対して「縮約〈contraction〉」は使いません。 graft〈接ぎ木する〉 を bridge〈架橋する〉に変えたのは、graft が substitute〈置き換える〉の意味で使われることがあるからです。特に、ツリーに対するリーフの置き換え〈substitution〉は接ぎ木〈grafting〉と呼ば…

…： ワイヤリング図〈ストリング図テンプレート〉の全体は複圏〈multicategory〉の構造を持ちます。 ...[snip]... ワイヤリング図達の複圏を $`\cat{WD}`$ とします。$`\cat{WD}`$ が何者であるか？は、今は保留します。そういう複圏があるのだ、と思ってください。 ごく最近でも「保留」状態で、ワイヤリング複圏（とその土台となる基礎圏）の完全な記述が出来ていないのです。問題点・疑問点まず第一の、そして最大の問題・疑問は「スケマティック系って、…

…グ図ワイヤリング図はストリング図テンプレートの同義語です（「有限コレクションとスケマティックなシステム記述 // ワイヤリング図達の複圏」参照）。ストリング図テンプレートとストリング図を区別しないこともあるので、結果的に、ワイヤリング図、ストリング図テンプレート、ストリング図はあまり区別されません。半グラフとワイヤリング図もほぼ同じです。違いは： 半グラフは、特にことわりがなければ辺に向きはないが、ワイヤリング図は原則的にワイヤーに向きがある。 半グラフでは、ワイヤリング図の…

… diagram〉とストリング図テンプレート〈string diagram template〉は同義語です。ワイヤリング図／ストリング図テンプレートについては、以下の過去記事を参照してください。 モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 オペラッドと型付きラムダ計算 ワイヤリング図とケリー／マックレーン・グラフ 強いて言えば、ストリング図テンプレートで、出現するすべてのノード〈ボックス〉が穴〈プレースホルダー | テンプレート変数〉である場合がワイヤ…

…osition〉は、ストリング図ではワイヤリングにより記述されています。ワイヤリングの集合圏における解釈は集合係数のテンソル計算で与えられます。IOCシステムとレンズ射〈制御ラッパー〉が混じった計算は、集合係数のテンソル計算とレンズ計算のハイブリッドになります。実例： オートマトン$`\mbf{IOCSys+Lens}`$ により定式化できる具体例として、形式言語理論に出てくるオートマトンを取り上げます。形式言語理論／オートマトン理論の伝統では、ラベル付き遷移系〈labele…

…よる計算は出来るが、ストリング図による計算がうまくいかない。 ペースティング図による計算は複雑になりがち。 実際のシステムに関する素朴な直感があまり効かない。 そこで、準同型方向はとりあえず捨てて、入出力方向、制御方向、モノイド積方向の三方向を考えます。グロタンディーク二重構成のような大道具は使わずに、出来るだけ素朴かつ直接にシステム概念を定式化することにします。$`\newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\In}{\tex…

…ていました。図式にはストリング図もあります。ストリング図をグラフとして扱う方法として、ストリンググラフ〈string graph〉があります。ストリンググラフでは、ノード頂点とワイヤー頂点という二種の頂点を使います。以下の過去記事にストリンググラフの説明があります。 ストリング図とストリンググラフ、何が違う？ ストリンググラフとストリング図 半グラフ〈semigraph〉を使ってもストリング図の定義ができます。 半グラフの様々な定義 半グラフに関する記事はけっこうな量あります…

…を記入するノード、「ストリング図と因子グラフ」参照）と同じ役割りをはたします。vnam属性は、例えば次の形に描けます。$`\quad \xymatrix@C+1pc{ {x: \mbf{R}} \ar[r] \ar[d] \ar@{}[dr]|{\SWArrow} &{n : \mbf{N} } \ar[d] \\ {\cdot} \ar@{=}[r] &{\cdot} }`$ 矢印の属性の表現方法前節の例を考えます。class属性（すぐ後に説明）を追加します。$`\quad…