このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ボックス の検索結果:

環境付き計算と依存アクテゴリー 2/n

…生成射 ラベル付きのボックス〈ノード〉 $`\strdiag{D}`$ がデカルト・ストリング図だとして、$`\strdiag{D}`$ が表す多射〈P.M. = polymorphism〉を $`\mrm{PM}(\strdiag{D})`$ とします。我々は、次のメタ定理を信じて絵算をしてます。 デカルト・ストリング図 $`\strdiag{D}`$ をデカルト・ストリング図 $`\strdiag{E}`$ へと“変形”できるならば、$`\mrm{PM}(\strdiag…

カン拡張と充填三角形 補遺

…手の結合方向、上から下に自然変換の縦結合方向です。ストリング図の描画方向に合わせるために、ペースティング図に鏡映や回転の変換を施しています(「双対や随伴に強くなるためのトレーニング」参照)。スパン/コスパンを三角形で充填する問題の解である2次元の射が、ストリング図ではボックスで描かれています。ボックスのラベルである run, lun, drop, dlop がそれぞれ、右カン拡張、左カン拡張、右カン持ち上げ、左カン持ち上げを構成する2-射〈自然変換〉のラベル〈構成素名〉です。

コステロの半グラフ圏によるシステム記述

… 連結成分 ブラックボックス化した独立サブシステム・ノード 半グラフの連結成分は、独立サブシステムとみなします。異なる独立サブシステムどうしは、切り離されているので互いに無関係です。連結成分は、部分半グラフ(サブシステム設計図)とみなすときと、中身が見えないノードとみなすときがあります。この2つの見方は、半グラフ〈システム設計図〉の結合のときに重要な役割を演じます。「インターフェイス」、「仕様」、「指標〈シグネチャー〉」、「プロトタイプ」、「プロファイル」などの言葉はほぼ同じ…

テンソルの計算法則の絵(ストリング図)

…s〉が出た“テンソルボックス”達をワイヤーで繋いだ図形になります。脚がたくさんあったり、複雑なワイヤリングをすることもあります。テンソルの計算法則の絵をまとめたものがないかと探したら、意外に見つからない。なので、手描きで描いてみました。トレース(ワイヤーをループ状にする操作)は含まれていませんが、他の演算と法則は絵にしています。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\hyp}{\text{-} } \newcomman…

穴、スポット、エリア、シーム

ストリング図はボックス&ワイヤー図とも呼ばれます。「ボックス」の意味はちょっと曖昧です。「バエズ/ドーラン・ツリー: 色々な描画法」で、かなりクリアになったと思います。「注意点のまとめ」に曖昧性についても書いてあります。ストリング図の「ボックス」は、円板表示における次のどれかになるでしょうが、どれだかハッキリしないことがあるのです。 円板〈disc | disk〉: 図を描くキャンバスに使う板、2次元の図形。 穴〈hole〉: 円板の境界円周(1次元の図形)のなかで、円板の内…

バエズ/ドーラン・ツリー: 色々な描画法

…性)を含めた情報を(ボックスの)ボーダー〈border〉と呼ぶことにします。ボーダーは境界の幾何的形状ではなくて、組み合わせ的情報です。 図形としての円周よりはポートに注目して「ボーダー」と呼んだのですが、ポートを載せている図形とポート達を含めた概念としてボーダー〈border〉を使うことにします。その意味で、スポットを囲む円周とポート達もボーダーです。結局、ボーダーはニ種類あることになります。 境界円周とポート達 スポットの縁とポート達 円板内部の穴が代入可能な変数に相当し…

コレクション、対称性、シーケンス、色付け

…リング図を描く際に、ボックス〈ノード〉は基本的かつ重要な描画要素です。絵に描いたボックスに対応する組み合わせ構造はいったい何なのでしょう? ボックスは、色付きコレクションの視覚化なのだとみなすのが良さそうです。なので、この記事では色付きコレクションについて述べます。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\pipe}{\mid } \newcomman…

変換手2-圏の代数構造とストリング図表現

…〈ドット | まるいボックス〉で描く。黒丸は生の2-自然変換です。 $`A`$ の単位ラクセイター $`\iota^A`$ は黒三角〈上にとがったボックス〉で描く。黒三角は特殊な生の2-自然変換です。 ワイヤーとボックス(黒丸、黒三角のボックス)の内部構造を描くときはストライプ図を使います。ストライプの内部には $`\cat{K}`$ の様子を、ストライプの外部(キャンバスの地の部分)には $`\cat{L}`$ の様子を描きます。ストリング図の絵図要素〈pictorial …

生の2-関手と生の2-自然変換

…、エリア/ワイヤー/ボックス〈ノード〉の意味は変わりますから注意。この1-射 $`f`$ をテンプレートのストライプ内にはめ込みます(テンプレートの具体化)。すると、次のようになります。この具体化により、エリア、ワイヤー、ボックス〈ノード〉なども具体化されるので、ラベルを書き込みましょう。この絵を上下に分割して、上段を辿ってみると次のようです。$`\quad S(a) \overset{S(f)}{\to} S(b) \overset{\alpha(b)}{\to} T(b)…

抽象テンソルシステムは縮約付き色彩的モノイド・スピシーズ

…入出力の別〉を持ったボックスとして描きます。型付け $`\tau`$ と極性付け $`\rho`$ を組み合わせてひとつの関数にします。$`\quad \langle \tau, \rho\rangle : A \to T \times \{+, -\} \In {\bf Set}`$前節の最後に述べた方法で $`T`$ から作った色パレットを $`\mathfrak{T}`$(フラクトゥール体の T)とします。色パレットの作り方から、$`\quad \u{\mathfrak…

回路代数とグラフ置換モナド

…ヤリング図のすべてのボックスごとに、ポートに全順序が付いている。-- Anchored 注意事項: ここでのラベル付けは、一般的なラベリング(任意の関数)のことではなくて、識別用の名前を付けることです。 ワイヤーの orientation と direction は同義語です(詳細は後述)。 ボックスごとにポートに全順序を与えることをアンカリング〈anchoring〉といいました(「テンソルの可視化のための半グラフ」参照)。 対称オペラッド〈対称複圏〉の“表現”は、必ずしも“…

絵図的手法: 中間整理

…ソルネットワークは、ボックスがテンソルを表すワイヤリング図です。)有限集合に載る構造有限集合に追加する構造として次のようなものがあります。 付点構造: 有限集合の一点〈特定要素〉を指定する。 ラベリング: ひとつの集合 $`L`$ を決めて、有限集合から $`L`$ への写像を指定する。 全順序構造: 有限集合の要素を一列に順序付ける。 循環順序構造: 実際には順序ではないが、全順序構造と同様に後者〈サクセッサ〉を指定できる。 典型的ラベリングには次があります。 型付け〈ty…

スケマティック圏: お絵描きできる場所

…しての $`w`$ ボックス達が通し番号で識別されていて、キャンバスボックス〈外部ボックス〉が0番になっているような半グラフです。繋ぎ合わせ方(How To Wire Them)の指定にボックスの名前はどうでもいいので、通し番号でも問題ありません。次に、オペレーション〈複射〉のオペラッド結合〈operadic composition〉を定義します。オペラッド結合として、ナロー結合〈narrow composition〉を採用する流儀と、ワイド結合〈wide compositi…

入れ子の半グラフとバエズ/ドーラン・ツリー

…ート ポート 頂点 ボックス 小円板 コンポネント 辺 ワイヤー ワイヤー ワイヤー 未定義値〈ボトム〉 キャンバスボックス 大円板 システム境界 入れ子円板はオペラッドのオペレーションの表現であり、オペラッド結合が定義されていました。となると、半グラフやシステムの全体もオペラッドになり、オペラッド結合が定義できるような気がします。実際、それは可能です。境界の情報幾何的半グラフにおいて、ひとつの頂点に接続する半辺の集合を(その頂点の)カローラ〈corolla〉(花の冠、花びら…

半グラフからシステムの記述へ

…B`$ を考えます。ボックスの集合は次のようだとします。 $`\mrm{Box}(A) = \{A_0, A_1, A_2\}`$ 、$`A_0`$ がキャンバスボックス $`\mrm{Box}(B) = \{B_0, B_1, B_2\}`$ 、$`B_0`$ がキャンバスボックス $`A`$ のポートは合計で8個あり、$`B`$ のポートは合計で6個あります。型付け〈typing〉写像の詳細は省略します。型付き半グラフ $`A`$ の内側に型付き半グラフ $`B`$ が入…

型付き半グラフと指標

…〉を考えます。また、ボックスの型の仕様である指標〈signature〉も定義します。データベースへの応用を念頭に置いていますが、型付き半グラフとその指標は他の目的でも使えるでしょう。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\twoto}{\Rightarrow } \newcommand{\In}{\text{ in } } %\newcommand{…

テンソルの可視化のための半グラフ

…造としての半グラフ ボックス、ポート、ワイヤー 様々なラベリング 極性付けとワイヤーの向き アンカリング ストリング図とテンソル 過去記事 なぜ半グラフなのか?ソフトウェア構成、データベース、ベイズ確率などに関する“状況”を、ストリング図として視覚化しようとすると、ワイヤーの方向や並んだワイヤー達の順番が不明であったり、気にしたくないことがあります。このような場合、当該の“状況”をとりあえず無向グラフとして記述しておいて、後から方向や順番を考えるほうが楽です。あるいは、方向や…

反対圏/反変関手と、2-圏のストリング図

…ます。レーンは、関手ボックスやストライプとは違い、特に実体はなくて単にキャンバスの一部を意味するだけです。$`[\cat{C}, \cat{D}]`$ とマークされたレーン内のワイヤーには、上から下(順方向)への矢印で方向付けします。一方、$`[\cat{C}, \cat{D}]^\op`$ とマークされたレーン内のワイヤーには、下から上(逆方向)への矢印で方向付けします。これは、キャンバスの描画方向を変更するものではありません。ワイヤーの方向は、常に上から下へと読みます(キ…

ダガー・ハイパーグラフ圏とドット付きワイヤリング図

…ング図は、頂点極性とボックス(頂点のグルーピング)を持ったハイパーグラフと解釈できます。今日はダガー・ハイパーグラフ圏の実例について述べませんが、データベースや統計・確率の話に使えそうです(それが動機)。$`\newcommand{\cat}[1]{\mathcal{#1}} %\newcommand{\Imp}{ \Rightarrow } \newcommand{\In}{ \text{ in } } \newcommand{\mrm}[1]{\mathrm{#1}} \…

レイヤー化ストリング図: スプリット図

…トリング図では、関手ボックス/関手コボックスとその変種を用います。関手ボックス(または関手コボックス)のサイズを大きくすると、関手ボックスの境界がキャンバスを二分するように見えます(下図)。このとき、キャンバスを二分している境界線を関手スプリッター〈functor splitter〉と呼ぶことにします。そして、関手スプリッターを使った図をスプリット図〈split diagram〉と呼びましょう。繰り返しますが、関手スプリッターは関手ボックスのサイズ/レイアウトを変えただけのも…

層化ストリング図

…層化プロップ 関手コボックスとスプリッター図 おわりに 裏返し反変関手ロブスキ/ザンサイ〈Leo Lobski, Fabio Zanasi〉は、層化プロップ〈layered prop〉という概念を導入してますが、これは(おそらく意図的に)構文論と意味論がゴッチャになっています。意味論側だけを切り出すと、インデックス付き圏〈indexed category〉です。ただし、最初に余インデックス付き圏(共変関手)を出して、後からインデックス付き圏〈反変関手〉を追加する構成になってい…

代数的な随伴系から自然なホムセット同型へ

…名を右上にマークしたボックスで表します。引数〈argument〉はボックス内に入れます。引数が描き込まれたボックス全体はコンビネータの値〈return value | output〉になります。コンビネータ $`\varphi`$ は次のような対応になります。その定義は次のとおり。逆向きの反転置コンビネータ〈opposite-transposition combinator〉$`\psi`$ の対応は次のとおり。定義も転置コンビネータと同様で、単位 $`\eta`$ の代わり…

証明と計算は同じこと: 形式証明におけるノードとコネクター

…グ図のテキスト化: ボックス&ポート方式」参照)の場所を識別する目印です。2つ目の解釈は、入力を持たないノードの名前です。入力を持たないノード(三角で描いている)は、集合・型なら要素、命題なら証拠(仮定を持たない証明)と解釈できます。これら2つの解釈は、状況に応じて使い分けてください。ラベルを型〈命題〉の別名と解釈しがちですが、それは違います。例えば、2変数関数の記述 $`\quad x:{\bf R}, y:{\bf R} \mapsto x^2 + y^2 \;: {\b…

証明支援系がダメだった理由と、AIでブーストする理由

…語サーバーと、VSCodeのようなクライアントが必要です。 *2:逆に、ストリング図をテキストに書き写す方法は「ストリング図のテキスト化」「ストリング図のテキスト化は何が大変か?」「ストリング図のテキスト化: ボックス&ポート方式」にあります。 *3:自然言語AI技術も、テキスト言語にもとづいているので、“一目瞭然な絵図の世界”への転換には役立ちません。ただし、画像解釈・生成/動画〈ムービー〉解釈・生成の技術が進展すれば、非テキスト言語の世界が拓ける端緒になるかも知れません。

ヤシコフスキ/カリシュ/モンタギュー形式の証明: 人間可読・将来的機械可読

…キの証明図は入れ子のボックスを使ってレイアウトします。これも、罫線文字を使った文字組版技術でぎりぎり描けそうです。後年、カリシュ〈Donald Kalish〉とモンタギュー〈Richard Montague〉は、書籍"Logic: Techniques of Formal Reasoning"のなかでヤシコフスキ流証明図を少しだけ変更して使用します。カリシュ/モンタギュー形式では、これから証明すべき命題をキーワード $`\text{Show}`$ に続けて宣言します。その命題…

プロ関手のコエンド同値関係

… %`$内容: 関手ボックスによる説明 コイコライザー 多項関手のスイムレーン描画法 プロ関手と2レーン描画法 コエンドを定義するためのセットアップ 射の左作用と右作用 コエンド同値関係 補足:左作用/右作用 関手ボックスによる説明このブログの過去記事「米田テンソル計算 1: 経緯と発想 // 関手ボックス」において、コエンド同値関係の説明をしています。 コエンドの具体的構成で使われるコエンド同値関係も、関手ボックスを使って次のように描けます。 絵に続けて、箇条書きで説明も書…

グリッド計算とコーナリング、そして二重圏

…が、ノード(あるいはボックス)の意味は不明です。ノード達は、生成系〈system of generators | generating system〉と関係〈relations〉により定義します。二種類の生成ノード〈generating node〉があります。 $`\cat{C}`$ の射 $`f:A \to B`$ に対して、グリッド図のノード $`\mrm{proc}(f) :: \varepsilon \dblto{A}{B} \varepsilon`$ がある。このタ…

ワイヤリング図とケリー/マックレーン・グラフ

…グ図のテキスト化: ボックス&ポート方式 モノイド圏上のテンプレート・オペラッド:具体例とソフトウェア的解釈 内容: ワイヤリング図とポート ケリー/マックレーン・グラフ ワイヤリング図からケリー/マックレーン・グラフへ 極性付き集合 ワイヤリング関数 ワイヤリング図とポート次の図は、スピヴァック〈David I. Spivak〉のスライド "Wiring diagrams and state machines" からコピーしたものです。これは、簡単なワイヤリング図〈wiri…

述語論理: 様々な多圏達の分類整理

… -- ノードまたはボックスと呼んでます。[補足]The ZX-calculus では、ストリング図のZノード〈緑ノード〉とXノード〈赤ノード〉をスパイダーと呼んでいます。例えば次の論文参照。 Title : Interacting Quantum Observables: Categorical Algebra and Diagrammatics Authors: Bob Coecke, Ross Duncan Submitted: 25 Jun 2009 (v1), 21…

圏論的述語論理とお絵描き

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