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

ご連絡は上記 X アカウントに DM にてお願いします。

[参照用 記事]

ボックス の検索結果:

カリー化、内部ホム、カックンカックンのストリング図

…対象を表し、ノード(ボックスや丸いオダンゴ)で射を表します。ワイヤーは恒等射を表すこともあります。以下の図は、「ボブ・クック教授による、対称とは限らないモノイド閉圏における絵の描き方」からの再掲です。これは、対象でもあり(ときに)恒等射でもあるワイヤーの描き方です。左から $`A \otimes B`$(モノイド積 | テンソル積)、$`A \lhom B`$(左内部ホム)、$`A \rhom B`$(右内部ホム)です。ロリポップ記号 $`\lhom,\; \rhom`$ は…

コンウェイ不動点オペレーター: 圏論的背景と計算公式

…グ図とオペレーター・ボックスを使うと楽ちんです。例えば、結合順入れ替え公式からパラメータ付き不動点性を出すのはほぼ自明になります。ストリング図とオペレーター・ボックスの技法は、相対モナドやカン拡張などでも使えるものなので、いずれまとめて説明するかも知れません。 *1:圏論的概念なので、実際の変数が出てくるわけではないです。言葉の綾です。 *2:デカルト・ペアリングは、対角 $`\Delta`$ とデカルト積 $`\times`$ を使って、$`\langle f, g\ran…

ベント〈bent〉とベンド〈bend〉: 訂正と説明

…めで、ストリング図のボックス(ノード)内に閉じ込められています。仮想ベンドは“描画上の補助線”のような存在であり、仮想ベンドを射として扱うことは出来ません。「モノイド閉圏: カリー化からニョロニョロまで」に登場しているラムダベンド $`\overset{\lambda}{\cap}`$ とガンマベンド $`\underset{\gamma}{\cup}`$、評価器〈エバル〉や余評価器〈コエバル | インス〉の内部構造としてのベンドは仮想ベンドです。トレース・オペレーターで作ら…

カローラ:: 2次元のカローラ

…圏/添加仮想二重圏/ボックスオペラッドなどの射を図示するために使います。おわりに2次元のメッシュ/タイル/カローラの例を挙げました。モノイド圏/複圏/2-圏/二重圏/仮想二重圏などの図示の基礎を提供できたと思います。しかし、2次元カローラの概念が解明できたか? と言うと、まだ曖昧な部分がたくさんあります。直感と比喩に頼った説明を多用しているので、直感・比喩のなかに隠れている暗黙の前提/制約/法則などが十分明示的に記述できていません。今回は、$`\mbf{Tile}`$ の射に…

低次元高次圏へのカローラ・アプローチ: はじめに

…category〉 ボックスオペラッド 弱構造〈weak structure〉や一貫性〈coherence〉を十分には扱えないので、原則的に厳密な構造〈strict structure〉に限定されます。これらの圏類似構造をカローラ・アプローチにより図示すると、その計算はタイル計算により表現できます。これはどういうことかと言うと; 2次元の射は“模様が描かれた矩形”(「タイル〈tile〉」と呼ぶことにする)になり、タイル達を縦横にピッタリくっつけて並べたモノが計算式に相当する、…

一般化圏と一般化グラフ

…properad〉やボックス・オペラッド〈box operad〉のような、n-圏とは呼べない代数系も一般化圏に含まれます。一方、圏〈1-圏 | 通常の圏〉や集合〈0-圏〉も一般化圏に含まれます。「一般化」が付いたからといって、圏や集合を除外するわけではありません。圏は一般化圏であり、集合も一般化圏です。「一般化圏」という名前の初出は、以下の過去記事です。 ベックの分配法則に基づく“一般化圏の製造工場”(2025年1月) それ以来、「一般化圏」は使っていますが、一貫して「一般化…

ホーア論理とホーアオートマトン 5/n : 整理と注意

…合、このブログの検索ボックスで青い文字を検索すると関連記事が出てきます。必要なら、既存の用語(青い文字)の定義を記事内で繰り返し書くこともあります。この記事で導入・定義する用語は赤い文字です。赤い文字が新規の用語、あるいは既存の用語でも意味を少し変えて使用する場合があります。赤い文字がよく知られた既存の用語のこともあります。特に話題にしたい用語が赤い文字、ということです。 マゼンタの文字は、この記事の後方または引き続く記事内(未来)で定義・説明される概念・用語です。茶色の文字…

ホーア論理とホーアオートマトン 1/n

…合、このブログの検索ボックスで青い文字を検索すると関連記事が出てきます。必要なら、既存の用語(青い文字)の定義を記事内で繰り返し書くこともあります。この記事で導入・定義する用語は赤い文字です。赤い文字が新規の用語、あるいは既存の用語でも意味を少し変えて使用する場合があります。赤い文字がよく知られた既存の用語のこともあります。特に話題にしたい用語が赤い文字、ということです。 マゼンタの文字は、この記事の後方または引き続く記事内で定義・説明される概念・用語です。概要と予告ラベル付…

AI支援形式証明への道 報告-2 off-the-shelf

…の通信・対話をすべて人間が手作業で仲介するので、ソフトウェアがやっていることがブラックボックス化することはありません。Lean のチェックが失敗して、エラーメッセージを参考にAIが修正するといった過程もすべて人間がモニターできます(つうか、モニターせざるを得ない)。不便さ・面倒さは残ってはいるのですが、off-the-shelf なことは大きなメリットだと思います。キャッチフレーズは: 既製ツールだけでやるAI支援形式証明「コンビニ食材だけで作る美味しいディナー」のノリです。

AI支援形式証明への道 報告-1

…われます。命題が推論ボックスのラベルになっているときは、そのボックスは命題から作られた推論です。命題 $`Y`$ に対応する推論ボックス(ラベルは同じ $`Y`$)は次のように描けます。次は、連言消去右〈conjunction Elemination right | ∧-Er〉の推論ボックスです。ボックスをワイヤーで繋ぐと、次のような回路図〈circuit diagram〉ができます。上部に、$`X`$ をコピーする二股分岐を繋ぐと以下のようです。上部の $`X`$ のワイヤ…

相対モナドのアイレンベルク/ムーア圏

…しかありません。拡張ボックスは計算に便利なので、拡張ボックスを使った絵算〈{graphical | pictorial | diagrammatic} {calculation | computantion}〉により入れ子法則と単位法則を記述します。描画法に関して次の約束をします。 $`\cat{C}, \cat{D}`$ の対象は実線のワイヤーで描く。 $`J`$ は点線のワイヤーで描く。 $`T`$ は実線に1本以上の斜線を添えたワイヤーで描く。 $`\cat{D}`$ …

スケマティック系の振り返りと整理 その2

…図 頂点の集合 V ボックスの集合 B フラグの集合 F ポートの集合 P 辺の集合 E ワイヤーの集合 W 例外ループの集合 L 例外ループの集合 L フラグ境界写像 β ポート所属写像 β カップリング対合 ι ワイヤリング関数 ι 未定義 ⊥ 外部ボックス〈キャンバス〉 B0 未定義値ボトムを特定する関数にギリシャ文字小文字オミクロンを使っているのは、ワイヤリング図における外部ボックス〈outer box | output box | outgoing boundary…

属性付き半グラフ

…ワイヤリング図の境界ボックス〈外部ボックス〉に相当するものは考えない。ただし、ワイヤリング図でも境界ボックス〈外部ボックス〉を考えないこともある。 半グラフでは、特にことわりがなければ修飾(後述)はないが、ワイヤリング図は最初から修飾を考えていることが多い。 用語法の対応は次のようです。 半グラフ ワイヤリング図 頂点 ボックス フラグ ポート 辺 ワイヤー 例外辺 ベアワイヤー〈bare wire〉 例外ループ サークル(使用を非推奨) パートナー指定対合 ワイヤリング対合…

有限コレクションとスケマティックなシステム記述

…べし」というブラックボックス原理と整合するように、複合システムの制御インターフェイスを定義するのが困難。この困難さには関数の決定性の要求も絡んでいるので、決定性の要求を諦めることも考えられます。が、そうすると、非決定性に伴う煩雑さ/面倒さを抱え込むことになります。あちらを立てればこちらが立たずな状況です。 「IOCシステムと制御ラッパーの構造」への追記: 以下に出てくる $`\quad \mathrm{Ctrl}(\Phi ; \Psi) \cong \mathrm{Ctrl…

マイヤースのシステム理論への違和感と代替案

…すときは、システムのボックスに対して、入力のワイヤー、出力のワイヤー、制御のワイヤーの3本のワイヤーが繋がった絵を描きます。上の図で、入力から出力への方向は上から下です。制御のワイヤーは横に飛び出しています。制御は双方向通信になるので方向の矢印はあえて書かないことにします。制御ワイヤーの斜線は、それが制御ワイヤーであることを示す符丁です。スティックマン U(User のつもり)からは、制御インターフェイスのみが見えます。一方、スティックマン D(Designer のつもり)か…

状態遷移系達の二重圏の直接的定義

…態遷移系は、ブラックボックス内にある内部バンドルと、インターフェイスを提供する外部バンドルを持ちます。バンドル射のペア(内部側と外部側)が状態遷移系の準同型射を与えます。この具体例は、マイヤースのアリーナの二重圏に対する直感的な理解を促します。古典的状態遷移系古典的状態遷移系〈classical state transition system〉は次の構成素からなります。 内部状態空間〈internal state space〉 $`S \In \mbf{Set}`$ 外部状態…

導出系: 反省と課題

…のプロセスをブラックボックス化して、入力である初期集合(語彙相当)と出力である帰納極限だけに注目したほうが話が簡単になるかも知れません。メタ導出系とは何なのか?導出系の集まり(ドクトリン)を記述するためにメタレベルの導出系を使うことはよくあります。例えば、自然演繹の導出系達を形式的に扱うとき、シーケント計算風(あるいは型判断形式の)メタ導出系を使うでしょう。よくやっていることだと思うのですが、どうもハッキリしません。メタ導出系の記述対象がオブジェクトレベルの導出系だとすると、…

テレスコープと包括クラン

…ための圏論”のツールボックスに付け加えます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\msc}[1]{\mathscr{#1}} \newcommand{\u}[1]{\underline{#1}} %\newcommand{\id}{\mathrm{id}} %\newcommand…

バエズ/ドーラン曲面の意義と使い方

…図は、ワイヤーだけ(ボックス〈ノード〉がない)のストリング図が描かれた曲面です。バエズ/ドーラン曲面の例ですね。*53つの穴のうちの2つに A, B と名前〈識別子〉を付けています。ワイヤーの端点となる境界上の点はポート〈port〉と呼びます。ポートは全部で9個あるのですが、一部は見えていません。また、ポートのうち 6個には、a, b, c, d, e, f で名前〈識別子〉を付けています(3個は無名です)。見えてないワイヤー/ポートが見えるように、潰して平面に押し広げましょ…

リントン/ローヴェア・モナド構成の明示公式

…の集合。 ワイヤーとボックスは、$`\Sigma`$ で提供される素材を使って組み立てる。 スポット(「穴、スポット、エリア、シーム」参照)の内容は、$`X`$ のセルにより埋める。 穴達のプロファイルの有限コレクション(「有限コレクション: 再配置の圏から」参照)は、$`H`$ である。 ストリング図全体のプロファイル(キャンバスボックスのプロファイル)は $`A`$ である。 $`P\H\mbf{Bun}_C(\hyp, \hyp)`$ は、圏 $`P\H\mbf{Bun…

リントンの定理: 概要、実例、注意事項

…| ポート〉を持ったボックス〈ノード〉ですが、上の2本が入力、下の1本が出力です。結合法則 $`\T{assoc}`$ の言っていることを絵に描きましょう。ちゃんと描くの面倒だから、象形文字を使ったアスキーアートで図示します。 Y Y Y ⇒ Y上段の Y(象形文字)を、下段の一番目(左)の入力に“接ぎ木〈grafting〉”する操作が $`;_1`$ です。下段のニ番目(右)の入力に“接ぎ木〈grafting〉”する操作は $`;_2`$ です。$`m \mathop{;_…

ストリング図、ストリング図動画が“使える”とは?

…ンバスストリング図はボックス&ワイヤー図〈boxes-and-wires diagram〉とも呼びます。ボックスとワイヤーが絵図の素子〈picture element〉です。絵を自由に描くというよりは、レゴブロックを組み立てるように、既存のガジェットを組み合わせて創作物〈作品〉を創り出します。ストリング図を描く場所、絵図の素子(ボックスとワイヤー)を置く場所をキャンバス〈canvas〉と呼びます。キャンバスを意識しないことも多いようですが、キャンバスはそれ自体で幾何的物体〈g…

有限コレクション: 再配置の圏から

…レーター〉」「辺」「ボックス」「テンソル」などと呼ばれるモノの集りです。それらのモノには境界プロファイル〈boundary profile〉が決まっています。「射/セル/オペレーション〈オペレーター〉/辺/ボックス/テンソル」の境界プロファイルは、「対象/型/ソート/色/頂点」などと呼ばれるモノの有限コレクションです。では、有限コレクションとは何でしょうか? その事例を挙げることは出来ます。 ペアは有限コレクションの一種である。 リストは有限コレクションの一種である。 バッグ…

一般化ハイパーグラフ → P-バンドル、P-ファミリー

… 辺 ノード、頂点、ボックス 射、オペレーション、オペレーター、セル 頂点 色、型 対象、色 境界写像 (特に呼び名はない) dom/cod、src/trg 一般化ハイパーグラフの辺が、ストリング図では頂点〈ノード | ボックス〉のことで、一般化ハイパーグラフの頂点が、ストリング図では(ポートやワイヤーに付く)色〈型〉のことです。「そう呼ぶと約束してるんだからしょうがないだろう」が建前の主張ですが、実際には混乱しますよね。一般化ハイパーグラフとストリング図を一緒に語るときは、…

一般化ハイパーグラフ

… diagram〉はボックス&ワイヤー図〈boxes-and-wires diagram〉とも呼ばれます。ストリング図においては、辺がノード(あるいはボックス)となり、辺に接続する境界頂点達は、ノード〈ボックス〉のポートとして描かれます。ノードは好みと目的により、丸、三角形、四角形などで描き、ポートは短い棒で描きます。ポートの並び順は明示的に描いてませんが、左から右です。そしてそれから一般化ハイパーグラフの種類は、プロファイル・コンストラクタで決まります。この記事で出したプロ…

環境付き計算と依存アクテゴリー 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次元の図形)のなかで、円板の内…