お絵描き
位相的形状 安全性： 例外ループ禁止〈安全〉 vs. 例外ループ許容 連結性： 連結性要求〈連結〉 vs. 連結性不問 修飾 色： 色無し vs. 色付き 極性： 無極 vs. 有極〈偏極〉 向き： 有向 vs. 無向 形容詞短縮形： safe conn $`\mathfrak{C}`$-color polar dir
半グラフは開放辺を持つ無向グラフである。半グラフに対するアンカリングとは： Aアンカリング： 各頂点に接続する辺の集合に全順序を入れる。Aは All ports から。 Bアンカリング： 各頂点に接続する辺の集合を二分割して、2つのパートにそれぞれ全順序を入…
$`f`$ のフルカリー化を $`f^\wedge`$ として次が意味的には同じであること。 $`f(a_1, \cdots, a_n)`$ $`f^\wedge(a_1) \cdots (a_n)`$ $`(\cdots(f^\wedge\triangleleft a_1) \cdots )\triangleleft a_n`$ $`f^\wedge\: a_1\: \cdots\: a_n`$ これをストリ…
テキスト ピクチャー ラベル（名前) ワイヤー頂点 型（命題含む） 色付きワイヤー 項 ストリング図 宣言 入力端頂点とワイヤー コンテキスト ワイヤーパレット シーケント ノード 公理シーケント 展開不可能ノード 割り当て 展開可能ノード ステージ パレッ…
いずれの描画法でも、平面を順方向エリアと逆方向エリアに区切っている。この区切り線を中心線と呼ぶことにする。代表的な3つの描画法を述べる。もちろん、他の選択肢もある。描画の約束によりファントム交差／ファントムカーブは生じる。相互変換には鏡映変…
k-オペレータはk-射に作用するオペレータ、関手は (0 | 1)-オペレータ。 絵図要素 圏論 射の次元 ワイヤー 対象 Cの0-射 ノード 射 Cの1-射 ボックス 1-オペレータ Cの射ではない 細いストライプ 0-オペレータ Cの射ではない ストライプ 関手 Cの射ではない …
https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の P.3 の11個の規則 IDENTITY WEAKENING CONTRACTION EXCHANGE MULTI-COMPOSITION （もとは無名） PAIRING PROJ-1 PROJ-2 ABS APP UNIT（むしろTERMINALだろうが） 使う文は以下。確…
ストリング図の描画指令〈instruction〉と記述〈description〉のための言語 Drawing Instruction Description Language 目的は違うが名前が似ているもの： https://www.ijcai.org/Proceedings/03/Papers/069.pdf LADDER (LAnguage to Describe Drawing, disp…
コンステレーションの図示にいおて、1次元キャンバスの場合も2次元に描く習慣があるのか？ -- これは混乱のもとだな、良くない。 1次元穴あきキャンバス： 区間に穴が開いている。穴は幅0でも有限幅でもいい。穴の境界にプロファイル情報が載るが、それは A …
Title: Shapely monads and analytic functors Authors: Richard Garner, Tom Hirschowitz Submitted: 18 Dec 2015 (v1), 10 Oct 2017 (v3) Pages: 52p URL : https://arxiv.org/abs/1512.05980 多項式の一般化。多圏と類似物がまとめてあるのがいい。多射に…
JS91 "The geometry of tensor calculus, I" → https://www.sciencedirect.com/science/article/pii/000187089190003P JS93 André Joyal and Ross Street. “Braided tensor categories” → https://www.sciencedirect.com/science/article/pii/S0001870883710…
NDed は双デカルト圏モノイド構造その1 対象 射 モノイド積 単位対象 モノイド構造その2 対象 射 モノイド積 単位対象 PolyNDed は双デカルト圏モノイド構造その1 対象 射 モノイド積 単位対象 対象のリテラル： モノイド積： モノイド構造その2 対象 射 モ…
左含意導入
xy環境内で、マトリックスの直後に drop-frameコマンド（描画インストラクション）を付ける。
連言導入選言消去
連言導入パターン 選言消去パターン 選言消去パターン 2
[tex:\require{color}% \newcommand{\deform}[1\]{% {#1}\\% \xymatrix{ *[.\]{}\ar@2{~>} [d\] \\{} }% }% % \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1\]{ \langle\![{#1}\]\!\rangle }% \newcommand{\As}{\;::\;}% …
デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編、ラムダ図 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。とても良い描画法を思いついた。青で書いているのは黒がなかったせい。ラムダハウスは関手ボックス／関手ストライプ／オペレ…
ラムダ図は、ラムダノードとワイヤーからなる。 ラムダノードは三角または台形で描く。 ノードに接合するワイヤーには、入力ワイヤー（0本以上）、ラムダワイヤー（0本以上）、出力ワイヤー（1本だけ）がある。ラムダノードは逆行ワイヤーとして描く。 ワイ…
「-----」は、アトミックな証明＝推論ルール 「~~~~~」は、アトミックとは限らない証明（アトミックを排除しない） 「=====」は、アトミックなリーズニング＝タクティク 「+++++」は、アトミックとは限らないリーズニング＝スクリプト (A∧B)→C ⇒ A→(B→C) の…
連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。モヤモヤを晴らすためにすること。 ラムダ項の圏論的位置付けをハッキリさせる。 単なる圏ではなくて復圏〈オペラッド〉を使う。 デカルト閉復圏＝…
選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。絵は裏写りがすごくて、ゴミが入っていたりする。図の右下はゴミ（別な図の一部）。左から右、上から下の順で説明。 ∀elim ： ∀i∈I.A ⇒ A(a) （⇒はシーケント矢印）の証明。ケーブ…
いいこと思いついた。たいぶいいこと思いついた。NK風証明図のストリング図による描画で、けっこう困るのが選言〈論理OR〉の処理。これの描画法を思いついた。思いついた時系列に沿って説明する。分配法則 A∧(B∨C) ⇒ A∧B ∨ A∧C （シーケント矢印は二重矢印）…
variables (P Q:Prop) theorem sample (hp : P) (hq : Q) : P ∧ Q ∧ P := begin apply and.intro, -- 5 assumption, -- 4 apply and.intro, -- 3 assumption, -- 2 assumption -- 1 endtry it! ☆ ☆ ---------- 1 ---------- 2 P, Q → P P, Q → Q ☆ ---------…
構造： 順序（あまり使わない） 二部 InOut 二部順序 InOut順序（装飾済み） 図 実線矢 ならば（構造忘却） 点線矢 細工している（埋め込み写像） 点線まる あまり使わない https://bit.ly/3e8A2oh spider-decoration.svg digraph{ 順序[style=dotted] 二部 …
装飾の種類 付与 忘却 leg order structure ordering unordering leg bipartite structure bi-partitioning fusioning in-out structure in-out assignment in-out forgetting 割り当てと忘却を使うと： order assignment ←→ order forgetting bi-partition …
チャンネル理論とデータベースと符号理論 - (新) 檜山正幸のキマイラ飼育記 メモ編 論理とテンソル計算 - (新) 檜山正幸のキマイラ飼育記 メモ編 ドメイン圏とテーブル代数 - (新) 檜山正幸のキマイラ飼育記 メモ編 新ERモデル 2 - (新) 檜山正幸のキマイラ…
ストリング図から辺の向きをなくした図をカップリング図と呼ぶ。カップリング図の意味はダガー厳密モノイド圏（https://ncatlab.org/nlab/show/dagger+category）から作られた多圏を置換同型で商をとった商圏内のポインティング射である。ストリング図に比べ…
