…ックス＆ワイヤー図、ストリング図）と相性がいいのです。一般的な「n-入力 m-出力」の回路図の全体は、圏というより多圏（polycategory）という構造を作るのですが、お絵描き計算には非常に都合がいい舞台です。僕が想定しているシナリオでは、ラムダ計算も命題論理もお絵描き（回路図）ありきなので、絵が描きやすいことが最優先の定式化になっているのです。 命題論理にかぎらず述語論理でも（僕にとっては）「絵が描きやすいことが最優先」です。述語論理では、$`\cat{C}`$ の異な…

…は、自然変換の計算はストリング図で行うのが望ましいと思っています。しかし、諸般の事情でそうもいかないので代わりにラムダ計算をしよう、ということです。頭にはストリング図を思い浮かべながらテキストで書くので、できるだけストリング図をイメージしやすい、つまり象形文字的記法にしたいのです。テキスト記法が辛いのは、2次元の情報がバイダイレクショナル1次元文字列に潰れているからです。そこで、縦方向の演算と横方向の演算を明確に区別することにします。ここでの“演算”とは、評価〈適用 | 引数…

米田の補題をストリング図で描いておくと、米田同型〈the Yoneda isomorphism〉の作り方を忘れないんじゃないかと思います。$`% \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } \newcommand{\Iff}{\Leftrightarrow }…

…にくいと感じる人は「ストリング図と相性が良いテンソル計算 1/2」の記法に書き換えると視認性・可読性が向上します。テンソルの結合とテンソル積は次のように定義します。$`\For f:\lis{n} \to \lis{m}, g:\lis{m} \to \lis{l}\In {\bf Tens}\\ \Define g\circ f := \\ \quad \lambda\, (x, z)\in \prod(\bar{\lis{n}})\times \prod(\bar{\li…

「ストリング図のテキスト化は何が大変か？」にて： [ストリング図のテキスト化は]大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情報伝達手段がテキスト化する以外にないので。 という事情で、テキスト化の方法をハッキリさせていくことにします。目の前にあるストリング図をテキストとして書き下すには次の作業が必要です。 ストリング図のすべての構成素に名前（番号も含む）を付ける。 構成素のあいだの繋がり具合を何らかの形で書き出す。 ストリング図…

昨日の記事「ストリング図のテキスト化」で、「テキスト表示を使って、オペラッド結合の記述や計算をするのは、やる前に気力が萎える」と言いました。つまり、大変なんです。大変でやる気になれないのですが、でもやらざるを得ないでしょう -- 低コストの情報伝達手段がテキスト化する以外にないので。実際のテキスト化を実行する前に、「テキスト化の大変な部分はどこなのか？」を明らかにしておくのは無駄ではないでしょう。「ここが大変」と理解した上で覚悟を決めよう、ってことです。内容： 絵による結合の…

僕はストリング図が大好きです。ストリング図の利用・応用の範囲は広がっているようです。しかしながら現状においては、ストリング図の作成・公開・交換は容易ではないので、テキストに翻訳してコミュニケーションに使用することになります。テキスト化が好ましい手段でないのは重々承知ですが、現実的には致し方ありません。ストリング図利用者は、ストリング図のテキストへのエンコード、テキストからストリング図へのデコードに習熟する必要があります。将来的には、ストリング図を直接使ってコミュニケーションが…

…存在しない射だけど、ストリング図では“射であるかのごとく”に描くと便利なもの -- 仮想スパイダーの話をします。$`% \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\id}{ \mathrm{id} } \newcommand{\In}{ \text{ in } } \require{color} \newcommand{\Keyword}[1]{ \…

…というよりは、とあるストリング図のクラスに属するストリング図のことです。ストリング図はモノイド圏の射を表すので、スパイダーを圏の射として定義することもできます。この記事では、スパイダーを圏の射として定義してみます。スパイダー付き圏モートンは、前節で参照した論文 "Belief propagation in monoidal categories" のなかで、スパイダー付き圏〈spidered category〉を次のように定義しています。 a strict symmetric…

…ーフェイス図〈3次元ストリング図〉の話です。この2-圏*1におけるサーフェイス図は、2-射〈自然変換〉を表します。サーフェイス図が描かれる場所である3次元キャンバスは、実数単位区間 $`[0, 1]`$ の直積である $`[0, 1]^3`$ であると仮定します。この仮定はまったく便宜上のもので必然性はありません。座標軸の取り方は昨日の記事のとおりです（図再掲）。キャンバス方体〈キューブ〉の z = 0 の面を上面、z = 1 の面を下面と呼ぶことにします。また、y = 0 …

…の約束で2つの2次元ストリング図は次のようにテキスト化されます。 $`(h \otimes h')\cdot (g \otimes \id_C) \cdot f`$ $`(h \otimes h')\cdot (g' \otimes \id_C) \cdot f`$ 奥から手前を左から右に書き換えると（$`f`$ の下に2本ワイヤーは間違いですね）：$`\alpha`$ は次のようにテキスト表示できます。$`\quad (h \otimes h')\cdot (g \otim…

「ストリング図と相性が良いテンソル計算 2/2」において： マルコフ行列／マルコフテンソルのときは、確率に特有なワイヤーベンディング・オペレーターが登場します。それは条件化〈conditionalization〉オペレーターです。条件化オペレーターもワイヤーベンディングとして描かれますが、行列・テンソルのプロファイルを変えるだけのワイヤーベンディング・オペレーターと条件化オペレーターは別物です。...[snp]...別物に同じ記号を流用するのは混乱の弊害がありますが、構造的類…

「ストリング図と相性が良いテンソル計算 1/2」の続きです。今回は、ベイズ確率やデータベースで実際に使う記述・計算を紹介します。$`\newcommand{\Idx}[2]{ {\scriptsize \begin{pmatrix} #1 \\ \downarrow\\ #2\end{pmatrix} } } %\newcommand{\IdxDU}[2]{ % index down-to-up {\scriptsize \begin{pmatrix} #2 \\ \upar…

ストリング図とテンソル計算については、以下の過去記事で述べました。 ストリング図とテンソル計算： クソバカ丁寧編 上記過去記事では、律儀に愚直にテンソル計算する方法を説明しました。もっと素早く計算する方法があることは記しておきました。 ここまでのプロセスは過剰に丁寧な記述・計算です。うまくサボることにより、もっと素早く記述・計算する方法があります。上下の添字を巧みにあやつる“インデックス・ジャグリング”としての古典テンソル計算は、サボるテクニックを洗練させたものです “インデ…

「ストリング図とハイパーグラフ図」でハイパーグラフ図を紹介しました。その記事で、次のように書きました。 ハイパーグラフ図は、ストリング図とかなり似ているので、僕は積極的にハイパーグラフ図を使うことはなかったのですが、...[snip]... 僕がハイパーグラフ図を使わなかった理由は、メリットよりもデメリットのほうが目立つからです。それらのデメリットは、ハイパーグラフ図を使う上での注意事項となります。$`\require{color} \newcommand{\orange}[…

…に表す描画法として、ストリング図とペースティング図があります。もうひとつの描画法としてハイパーグラフ図を紹介します。内容： 圏論の描画法 ハイパーグラフ 多射とハイパー辺 ハイパー辺の描画法 モノイド積と指数 カリー化と反カリー化 圏論の描画法ストリング図とペースティング図は一長一短があり、ストリング図を完全にペースティング図で置き換えるわけにはいかないし、ペースティング図を完全にストリング図で置き換えることも出来ません。ハイパーグラフ図は、ストリング図とかなり似ているので、…

…てペースティング図もストリング図も描いてませんが、各自描いてみることをおススメします。随伴系の圏最初に、随伴系の圏 を定義します。これは、任意の厳密2-圏 に対して定義できる の、 と置いた具体例です。以下、 である場合は、と略記します。 は大きい圏となるので、 です。ここで、 は大きいかも知れない圏〈1-圏〉達の2-圏です。圏 の対象の集合は次のようになります。つまり、（小さい）圏が の対象です。その意味で、 は“圏の圏”と言えますが、射は関手ではありません。圏 の射は随伴…

…ンズ 最初の一歩： ストリング図を中心に」において、レンズには有法則レンズ〈lawful lens〉と無法則レンズ〈lawless lens〉があると書きました。「有法則／無法則」という形容詞を使うのは初めて見ました（レンズ以外で見たことがなかった）。この「有法則／無法則」、他でも使えますね。曖昧多義語の解決に役立ちそう。けっこう困っていたのは、自己関手の「代数〈algebra〉」という言葉です。 用法その1： 自己関手 に対して、 をFの代数と呼ぶ。 用法その2： モナド …

…字で と書きます。 ストリング図のラベルとしては、 の代わりに ☆ を使うことがあります。0, 1, 2個のモノからなる集合／圏特定された単元集合は：唯一の要素 が具体的に何であるかは保留にしておきます。どうしても具体的に決めたいときは目的により都合がいい要素を選びます。 はブール値〈真偽値〉の二元集合とします。一方、0, 1, 2個の対象を持つ圏は次のように書きます。いずれも集合圏 の充満部分圏で：射はそれぞれ、0本、1本、3本持ちます。 が離散圏（恒等しか射がない圏）では…

ストリング図とテンソル計算に関して僕が言えること、言いたいことは「やってみてください」です。ある意味“機械的な作業”なので、やれば出来ます。ボブ・クック教授に言わせれば「幼稚園児でも出来る」（「幼稚園児のための量子力学とその周辺」参照）。もっとも、この記事では、字を知らない園児ではとうてい出来そうにない作業も扱いますが。注意： この記事で使っている「ベント〈bento〉」は間違いです。正しくは「ベンド〈bend〉」です。「ベント〈bent〉とベンド〈bend〉： 訂正と説明」…

…できると思います。 ストリング図の描画法に、ボブ・クック達（オックスフォード／ケンブリッジ・グループ）の描画法を取り入れる。 関手ボックスをもっと積極的に使用する。 米田埋め込みをもっと明示的に利用する。 テキストの表記法を古典テンソル計算風にする。 ロマン論文で扱っていることは（論文タイトルにもあるとおり）コエンド計算〈coend calculus〉です。ロマンのアイディアに基づいて、上記のような変更・拡張を施したコエンド計算を米田テンソル計算〈Yoneda tensor …

…〉 テレオロジー圏とストリング図 テレオロジー圏の定義 最初の記事＋シリーズ目次 参考文献テレオロジー圏〈teleological category〉は、次で論文でヘッジズによって導入されました。 Title: Coherence for lenses and open games Author: Jules Hedges Submitted: 15 Sep 2017 (v3) Pages: 30p URL: https://arxiv.org/abs/1704.02230 …

…ンズ 最初の一歩： ストリング図を中心に 圏論的レンズ 2： 具象オプティック 圏論的レンズ 訂正と補足： 具象レンズ＝具象オプティック これらの記事を（読むのではなく）眺めてもらえれば分かると思いますが、レンズ／オプティックの記述・計算はストリング図なしではキビシイです。レンズ／オプティックのストリング図を描くときの注意点を述べておきます。ストリング図の一般的なことは次の記事を参照してください。 絵算をはじめた人への注意 ストリング図の基本概念と描き方 ストリング図計算のコ…

…ンズ 最初の一歩： ストリング図を中心に」において、具象レンズの圏 の形式的定義は省略しましたが、具象オプティックの圏 をちゃんと定義すれば、具象レンズの圏はその部分圏として確定します； 。 この記述は、未確認の状況に対する僕の誤認に基づいていました。 ではなくて、実際は となります。「2つの圏が同じ圏なら部分圏と言えるので論理的に間違ったことは言ってない」と強弁もできますが、同じ圏だと思ってなかったという点で完全に勘違いしてました。内容： 表示が異なっても同じ同値類 具象オ…

…ンズ 最初の一歩： ストリング図を中心に」において、元祖レンズと具象レンズを紹介しました。元祖レンズを少し一般化すると具象レンズになるのでした。この記事では、具象レンズをさらに少し一般化して具象オプティックを導入します。[追記]この記事で導入した具象オプティックは具象レンズの一般化ではなくて、具象レンズ＝具象オプティックでした。詳しくは「圏論的レンズ 訂正と補足： 具象レンズ＝具象オプティック」を参照してください。[/追記]内容： 具象オプティックとは 具象オプティックの実装…

…べます。記述と計算にストリング図を使用します。内容： 元祖レンズ 元祖レンズの圏 元祖レンズ達はホントに圏なのか？ Webサーバーモデル 具象レンズ 元祖レンズと具象レンズ おわりに シリーズ目次（リンク）： 圏論的レンズ 最初の一歩： ストリング図を中心に（この記事） 圏論的レンズ 2： 具象オプティック 圏論的レンズ 訂正と補足： 具象レンズ＝具象オプティック 圏論的レンズ 3： レンズ／オプティックのための描画法 圏論的レンズ 4： テレオロジー圏 圏論的レンズ 5： …

…言う）檜山が、絵算〈ストリング図計算〉のコツと小技を書いてみますよ。似た趣旨の過去記事に次があります。 絵算をはじめた人への注意 ストリング図の基本概念と描き方 今回の記事は、一般的入門的解説ではなくて“コツと小技”です。内容： 前置きと例題 名称と形状 ノードの形状と塗りパターン 圏論的オペレーター 命題の記述 定義の記述 計算と証明の記述 前置きと例題人に見せることを考慮しないで、自分の作業としてストリング図を描き・操作する状況での話をします。ストリング図は、単色の鉛筆や…

「ストリング図の基本概念と描き方」に次のように書きました。 「描画方向と逆向きに走るワイヤーを見たぞ」とか「曲がったワイヤーが描けないだろ」とか思うでしょうが、違うんですよ。「逆向きに走るワイヤー」じゃなくて、負の極性〈polarity〉を割り当てられたワイヤーをあたかも逆向きに走るワイヤーのように描く習慣があるだけです（便利ですけどね）。曲がったワイヤーの正体は次のようなものです。 この部分に補足します。 を有限次元実ベクトル空間の圏とします。 として、 をその双対空間とし…

…いるセミナーのなかでストリング図を描く練習をしたのですが、ストリング図の基本的（ほんとに基本的）なことを復習したほうがいいかな、と感じました。ほんとに基本的なことは意外と言及されてないので。内容： ストリンググラフ ワイヤー頂点 キャンバスと描画方向と禁則 スパイダーノード ストリンググラフストリング図は、グラフ理論で扱うグラフのようなものですが、標準的なグラフの定義ではストリング図を記述できません。ストリング図は開放辺〈{open | half | dangling} ed…

…ある射です。これらはストリング図のノードですが横線で描いています。2番、5番は視認性の都合で“代表点”を描いていますが、これも自然変換の成分です。シングレット＆ズボンの比喩から次のように呼ぶことにします。 ベルト： 余モナドの余乗法 シングレットの股： 反ラックス・モノイド関手の余乗法 シングレットの左裾： 余モナドの余単位 シングレットの右裾： 余モナドの余単位 ズボンの股： 反ラックス・モノイド関手の余乗法 ズボンの左裾： 余モナドの余単位 ズボンの右裾： 余モナドの余単…