僕は、多圏の射、または多箙の生成辺をスパイダーと呼んでいるが、スパイダーの前例がある。ボブ・クックのスパイダーは、https://arxiv.org/pdf/1004.1598.pdf の6pに定義がある。それと、https://graphicallinearalgebra.net/tag/spider-theorem/ も良い。…

僕が定義する多圏は、三部結合（tripartite composition）を持つ多圏だ。多射は、三部スパイダー（tripartite spider）。

対称とは限らないモノイド圏Cから自然に厳密モノイド圏が出来て、それから多圏が作れるのだが、中間の厳密モノイド圏をシーケンス圏 Seq(C) と呼んでいた。対象の構成法はシーケンスだが、射の構成法を見るとスパイダーなので、Cのスパイダー圏 Spid(C) とし…

圏 論理 自己双対コンパクト閉圏 超コンパクト論理 モノイド閉圏 一般コンパクト論理 対称モノイド閉圏 対称コンパクト論理 デカルト閉圏 デカルト・コンパクト論理 デカルト・コンパクト論理が、直観論理の連言・含意フラグメント。超コンパクト論理、×, I …

多圏 シーケント計算 ラムダ計算 結合 カット 変数と式の置換（substitution） 全体のモノイド積 マージ なし カリー化 含意導入 ラムダ抽象 アンカリー化 含意消去 評価 部分的モノイド積 連言導入 ペアリング 部分的モノイド積の逆 連言消去 アンペアリン…

Seq(C)とPoly(C)はアルファベット（または指標）で相対化する。アルファベットの構成要素は、 |C| の有限部分集合V Mor(C| の有限部分集合E dom, codをE上に制限したときに、(V, E)が有向グラフになることが条件。さらに関係の有限性を入れる。 Cにおいて(V,…

記法を変える。PolyFull(C)じゃなくて、Seq(C)にする。 Seq(C)は単なる圏。その対象を列（シーケンス）、その射をシーケントと呼ぶ。 Seq(C)のモノイド積（連接）は、# と書く（++, ##の略記）。 |Seq(C)| = |C|* Seq(C)(Γ, Δ) C(Prod(Γ), Prod(Δ)) シングル…

圏 積 指数 双対 テンパリー／リーブ圏 釘列の併置 積に同じ 自己双対 符号付きテンパリー／リーブ圏 釘列の併置 双対との積 符号の反転 関係圏 集合の直積 積に同じ 自己双対 ベクトル空間の圏 テンソル積 双対との積 双対空間 集合圏 直積 関数集合 なし …

やたっ、これでうまくいきそう。Poly(C)の構成の方針 - 檜山正幸のキマイラ飼育記 メモ編の続き。地獄のHerculean taskを回避できそう。Poly(C)の構成の要点は： Cに部分対称構造（partially symmetric structure/system）を導入する。 Poly(C)とCの中間にPo…

目的は非対称非厳密なモノイド閉圏でラムダ計算とコンパクト論理を展開すること。この目的に特化する。閉圏、弱いラムダ計算、弱い論理 - 檜山正幸のキマイラ飼育記 参照。 シーケントはコンパクトシーケントを使う。 基本命題＝基本型はCの対象。現実には有…

非厳密な多圏は難しい - 檜山正幸のキマイラ飼育記 メモ編 : 別な方法として、Cの厳密化をしないで、多圏を作る方法があるが、これは難しい。というか、見当がつかない。 だいたい見当が付いた。|C|*（クリーネスター）に対しいて、[|-|]:|C|*→|C| を定義す…

http://arxiv.org/pdf/math/0606735v3.pdf より： For a start, the sheer quantity of data that one must check for even simple proofs quickly becomes overwhelming. sheer : 〔生地などが〕シアーの、透けるほど薄い overwhelming : 〔感情的に人を〕…

次を読めば参考になるはず。 Title: Quasistrict symmetric monoidal 2-categories via wire diagrams Author: Bruce Bartlett URL: http://arxiv.org/abs/1409.2148 Pages: 18p. Title: Polycategories via pseudo-distributive laws Author: Richard Garne…

ラムダ計算の重箱の隅(?)：タプルと成分 - 檜山正幸のキマイラ飼育記 メモ編 ： やっぱり多圏の議論をしないとどうにもならない、と感じる。 ... 重箱の隅でもないな、これは。 難しい問題が持ち上げる。Cが厳密モノイド圏のとき、それから厳密多圏Poly(C)を…

やっぱり多圏の議論をしないとどうにもならない、と感じる。ラムダ計算は、「タプルを出さないのが粋」みたいな風潮にもウンザリ。タプルを扱うなら、項レベルでペア構文 (E, F) は必要だ。これを、カンマが二項演算子と解釈する。ただし、カンマは左結合的…

Cが非対称（対称とは限らないという意味）厳密モノイド圏だとして、対応する多圏Poly(C)を定義する。S = |C|*（クリーネスター）として、Sは連接で厳密なモノイドになるとする。α = (A1, ..., An), β = (B1, ..., Bm) をSの要素として、PolyHom(α→β) := C(<α…

20070416 直積と射影がらみの高階関数たちの相関図 - 檜山正幸のキマイラ飼育記 20090325 演繹系とお絵描き圏論 - 檜山正幸のキマイラ飼育記 今、けっこう真面目に考えている。多圏の導入と使い方。[追記]だいたい出来た→ http://d.hatena.ne.jp/m-hiyama-me…

次のエントリーから検索できる。 圏を係数とする行列やテンソル - 檜山正幸のキマイラ飼育記 メモ編 形式テンソルだけ、ここで再検索： 形式テンソルの検索 http://d.hatena.ne.jp/m-hiyama-memo/archive?word=%B7%C1%BC%B0%A5%C6%A5%F3%A5%BD%A5%EB 極性付…

箱入りのタングルを考える。箱は例えば3次元として、上下の矩形内にn個の点をバラまいてタングルの境界とする。タングルの境界点（マーク点）に圏Cの対象、ストランドに圏Cの射を対応させて、iCラベル付きタングルと呼ぶ。Cラベル付きタングルは、構文的な存…

*は任意のマルチインデックス、x, yは極性の符号、**は任意の極性付きマルチインデックス 射 ポリ行列 圏の射 極性なし、1→1 シェイプ 複圏の射 極性なし、*→1 シェイプ 多圏の射 極性なし、*→* シェイプ 双対付き圏の射 極性あり、1x→1y シェイプ 双対付き…

http://d.hatena.ne.jp/m-hiyama-memo/20160209/1454977682に書いたように、伝統的古典テンソル計算（古式テンソル計算）では、コンパクト閉圏の表現が出来ないことが分かった。ポリ行列という概念を導入する。 極性なしポリ行列 ←→ 極性なしスパイダー 極性…

ある意味驚いた。なんとなく、コンパクト閉圏をベースにした線形代数は古典テンソル計算に翻訳できると思っていたが、表現力が足りなくて無理だった。多圏におけるストリング図をスパイダー図と呼ぶことにする。コンパクト閉圏の図では極性が必要になるので…

本編： 感動か効率性か - 檜山正幸のキマイラ飼育記 オカシイと文句を垂れるなら、修正案を提示しないとね。シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、…

calculationの訳語に運算を使う。 運算スキーム 構文圏 セマンティック圏 ツリー 複圏 モノイド圏 クローンツリー 余対角付き複圏 デカルト圏 ヘッジ 多圏 モノイド圏 クローンヘッジ 余対角付き多圏 デカルト圏 行列 半加法多圏 半加法圏 運算スキームは、…

オペレーション＝オペラッド射＝複射 をテンプレートと考えて、文法規則をテンプレートにより扱う。 形式言語 テンプレート ガード文字記号 定数ワイヤーラベル 文字記号（終端） 定数（ソリッド）ボックスラベル 変数記号（非終端） 穴ボックスラベル 規則…

昨日引用した↓ Title: COMPOSITION OF MODULES FOR LAX FUNCTORS Author: ROBERT PARE URL: http://www.tac.mta.ca/tac/volumes/27/16/27-16.pdf Pages: 53p. ↑これは、weak double category の話が多い。 Title: Tile Transition Systems as Structured Coa…

モノイド多圏は次のものから構成される。 単対象：集合Oの要素。 多対象：Oの列であるO*の要素。空列はεとして、A∈A に対する[A]（長さ1の列）はしばしばAと同一視する。 多射：α、βが多対象であるとき、集合 P(α, β) の要素。 モノイド積：多対象α、βの連接…

f:A→ B1, ..., Bn と g:A→ C1, ..., Cn がスパイダー射（cooperation）のとき、f▲g という射が定義できる。 f▲g : A → B1×C1, ..., Bn×Cn fとgは形状が同じだから、重ねあわせて、域の側はそのまま、余域側はワイヤー（成分）ごとに積を作る。多圏には積があ…

カリー／ハワード対応は、「論理⇔プログラム」の対応。典型例は、「連言と含意のNK」と「型付きタプル付きラムダ計算」の対応。型の計算（型推論）がNKの証明に対応している。ジラールとその周辺による対応はもうちょっと範囲が広いし、少し観点が違うように…

あ、そうか。グラフのある点から、n本以下の辺をたどっていける頂点＋辺のスター状近傍をn-近傍と呼ぶことにする。0-近傍、1-近傍、2-近傍、と定義できる。半整数に関しても近傍を考えればいいんだな。特に、1/2-近傍＝半近傍が大事だ。1/2の意味は、辺を真…