本編ネタ

半グラフ

近傍半辺集合〈近傍フラグ集合〉: ボリソフ/マニンは $`F_\tau(v) = \partial^{-1}(v)`$ edge-corolla : 頂点とその近傍半辺集合から作られるカローラ grafted edge : ソースグラフのテールがペアリングされて作られたターゲット側の内部辺 edge preserv…

インターフェイス、オペセット、算子〈アイテム〉

「ホムセット要素/色/極性の相当物の呼び名」の続き。 図/図式〈ダイアグラム〉はキャンバスに描かれる。 キャンバスに穴〈holes〉があるかも知れない。 穴はインターフェイスを持ち、キャンバス自体も(外部境界の)インターフェイスを持つ。 複数の穴は…

バエズ/ドーラン・ツリーの呼び名

バエズ/ドーラン・ツリー 星座図 入れ子のワイヤリング図 バエズ/ドーラン低木〈shrub〉 平坦な星座図 ワイヤリング図 バエズ/ドーラン低木 シームレス・バエズ/ドーラン・ツリー 高さ1以下のバエズ/ドーラン・ツリー ワイヤリング・パターン = ワイヤ…

ホムセット要素/色/極性の相当物の呼び名

ホムセット相当物の要素をなんと呼ぶか? セル アロー エッジ フェース ハイパーエッジ 射 オペレーション テンソル 状態 項 構造(スピシーズのとき) オブジェクト(一般的なモノとして) ホムセット相当物に作用する写像は: コンビネータ メタオペレーシ…

半グラフの分類基準

位相的形状 安全性: 例外ループ禁止〈安全〉 vs. 例外ループ許容 連結性: 連結性要求〈連結〉 vs. 連結性不問 修飾 色: 色無し vs. 色付き 極性: 無極 vs. 有極〈偏極〉 向き: 有向 vs. 無向 形容詞短縮形: safe conn $`\mathfrak{C}`$-color polar dir

原圏〈urcategory〉

モジュラーオペラッドを原圏〈urcategory | 原始圏 | ウル圏〉と呼ぶ。ウル〈ur-〉の意味は、https://www.etymonline.com/jp/word/ur- 「原始的な、初期の」という意味の接頭辞で、ドイツ語の「ur-」から派生しました。 ドイツ語の元々の意味は「外側、原始…

「HRY19b」のメモ

[HRY19b] Title: Modular operads and the nerve theorem Authors: Philip Hackney, Marcy Robertson, Donald Yau Submitted: 4 Jun 2019 (v1), 26 Apr 2020 (v2) Pages: 32p URL: https://arxiv.org/abs/1906.01144 URL (PDF): https://arxiv.org/pdf/1906.…

「JK09」のメモ

グラフィカルな色々 - (新) 檜山正幸のキマイラ飼育記 メモ編 の [JK09] 再掲。 [JK09] Title: Feynman graphs, and nerve theorem for compact symmetric multicategories (extended abstract) Author: Andr? Joyal, Joachim Kock Submitted: 19 Aug 2009 P…

「Ray21」のメモ

グラフィカルな色々 - (新) 檜山正幸のキマイラ飼育記 メモ編 の [Ray21] のメモ。 [Ray21] Title: Brauer diagrams, modular operads, and a graphical nerve theorem for circuit algebras Autor: Sophie Raynor Submitted: 10 Aug 2021 (v1), 18 Nov 2022…

グラフィカルな色々 リンク集

人物 ダンクソ/ハラーチェバ/ロバーツォン [DHR] ハックニー/ロバーツォン/ヤウ [HRY] ジョイアル/コック [JK] ソフィー・レイノア [Ray] ラルフ・カウフマン(ルイス・H・カウフマンと別人)/ワード [KW] ブラウダー [Bro] マニン [Man] nLab https:/…

(書きかけ) 含意演算と論理順序: 追認と妥協のために

**** この記事は書きかけ、今後、追加・修正・変更をして本編記事にする予定。本編に移したらこのエントリーは削除します。 ****含意演算と論理順序の違いをどう書き分けるか? この問題は、もう何年も、いやっ、何十年も困っています。関連する話題…

モノイド指標と代数装備圏

モノイド指標 Σ Σの圏Cでの付値モデル〈valuation model〉をΣ-代数と呼ぶ。Σ-Alg(C) := MonSIG(Σ, UC) ある種の忘却関手 MonCAT → MonSIG が必要。 モノイド指標はコンピュータッドの一種 Σ-代数装備は、圏Cの対象の弱モノイドからΣ-Alg(C)の対象の弱モノイ…

前層と米田の補題の事例

ファミリーの圏 $`{\bf Fam}[A]`$ は前層圏 順序集合に対するフィルター付き集合 $`\mathrm{FilteredSet}(A)`$ は前層圏 シェープ付き集合の圏 単体集合の圏: $`s{\bf Set}`$ 球体集合の圏: $`g{\bf Set}`$ 方体集合の圏: $`c{\bf Set}`$ 有向グラフの圏 …

関係圏と絵算と不等式セオリー

https://arxiv.org/abs/1711.08699 48p Functorial Semantics for Relational Theories https://arxiv.org/abs/1909.00069 31p Regular and relational categories: Revisiting 'Cartesian bicategories I' https://arxiv.org/abs/2109.14123 62p Regular Ca…

指標とセオリー

https://www.mscs.dal.ca/~selinger/papers/graphical.pdf https://ncatlab.org/nlab/show/DisCoPy https://arxiv.org/abs/2204.02284 Free gs-Monoidal Categories and Free Markov Categories https://arxiv.org/abs/1308.3586 Abstract Tensor Systems as…

データ従属性

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mvto}{ \twoheadrightarrow } \newcommand{\Iff}{\Leftrightarrow} \newcommand{\Imp}{\Rightarrow} `$関数従属性$`\mrm{FD}(X\to Y)(R) :\Iff \\ \quad \forall t_1, t_1 \in R. \, t_1[X] = t_2[X] \Im…

データベースの例

http://webdam.inria.fr/Alice/pdfs/Chapter-8.pdf より。Movieテーブル title Director Actor Showing〈上映〉テーブル theater screen title snack : 提供しているスナック(飲料と軽食) 昔は2本立てがあったが、今はほぼない。以前から使っている。学生…

メタ巡回性、自己言及、非可述性、手塚治虫、火の鳥

画像:*1*2 *3リンクと引用: 火の鳥 未来編 『COM』 1967/12-1968/09 Wikipedia 手塚治虫とデカルト閉圏 https://tezukaosamu.net/jp/manga/399.html より: 猿田博士が暮らすスノーグローブのような半球状のドームは、生命を封じ込めたグローブ=地球そのも…

タクティクに関する引用

URL: https://courses.engr.illinois.edu/cs576/sp2015/doc/isar-overview.pdf Title: A Tutorial Introduction to Structured Isar Proofs Author: Tobias Nipkow ブラケットは檜山が挿入。 a [tactic] proof is a more or less structured sequence of com…

判断・定義とプロファイル

$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは:$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

矢印記号の使用案

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}

区別するかしないか?

区別するなら ◯、しないなら/出来ないなら ☓、無意味なら - 。プログラミング言語に関しては、定義時と呼び出し時で二つ。△はやる気になればやれるが、普通はやらない、ほぼ☓。 集合圏 デカルト閉圏 TypeScript Lean 4 関数と関数データ ◯ - ◯, ☓ ◯, ☓ 関数…

シーケントの多目的使用

関数・定理の定義・記述 Γ |- ψ : A 型推論問題の質問 Γ |-? ψ : ? 項推論問題の質問 Γ |-? ? : A プロファイル宣言 Γ |- _ : A (アンダースコアは不定の意味) 単なる省略 Γ |- ψ : _ (不定だが、型推論で確定可能) ホムセット {f | f: Γ |- _ : A} 毎回…

TypeScriptで検証、表とリスト

論理記号 導入規則 除去規則 ∧ And導入 And除去左, And除去右 ∨ Or導入左, Or導入右 Or導入 ⇒ Imp導入 Imp除去 T True導入 (通常の証明) ⊥ (背理法による証明) False除去 ¬ Not導入 Not除去 1 And intro 基本証明 2 And elim left 基本証明 3 And elim righ…

TypeScriptで検証の絵

digraph { logic[label="形式化された\n定義/公理/定理/証明"] ts[label="TypeScript\nプログラムコード"] js[label="JavaScript\nプログラムコード\n(不要)"] logic -> ts[label=" 人手で相互翻訳", dir=both] ts -> js[label=" トランスパイラが翻訳 "]…

(n +2)度目:カリー/ハワード対応

And_intro And intro And_left And elim left And_right And elim right Or_inl Or intro left Or_inr Or intro right fun_OR_MAKE なぜか無い 後で定義 Or elim 特殊 Imp intro MP(不要だが) Imp elim trivial True intro EFQ False elim 不要 Not intro …

TypeScriptの良い特徴

アロー関数とアロー〈二重矢印記号〉を使った関数空間型の記述 declareを使った外部環境の型宣言 オンライン・プレイグラウンド 対応: TypeScript 疑似言語 function theorem const evidence declare function axiomatic theorem declare const axiomatic e…

(n +1)度目:カリー/ハワード対応

型と値は区別する必要がある。 計算と演算を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。 関数と計算は一応区別するが、ヘッド部(後述)の有る無しの違いしかないので、混同して使っても差し支えない。 型と型の…

n度目:カリー/ハワード対応

テーゼ: 十分に強力な型システム/型チェッカーを持ったプログラミング言語は、証明記述/証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…

証明のストリング図

digraph { label="proof" subgraph cluster_not_a { label="not_a" h[shape=triangle] And_left h -> And_left[ label="¬A∧¬B"] } subgraph cluster_not_b { label="not_b" h1[shape=triangle, label="h"] And_right h1 -> And_right[ label="¬A∧¬B"] An…