…い。 ストリング図やオペラッド〈複圏〉と相性が良い構文にしたい。 格納されたデータと論理的な条件を同等に扱いたい（WHERE句をテーブル扱いしたい）。 データ型は抽象的・概念的な構造として定義したい。 通常のプログラミング言語と同様に変数・関数を使いたい。 単純明快で夾雑物がなくスッキリしていることが第一で実用性なんてもんは考えません。この記事の最後に、この記事と引き続く記事の「動機と目的と方針」を書いています。最後の節を最初に読むほうがいいかも知れません。$`\requir…

…複圏は、単なる複圏〈オペラッド〉ではなくて、亜群の圏のなかに居る構造です。つまり、対象の集まり $`|\cat{WM}|`$ も複射〈multimorphism〉の集まり $`\mrm{MMor}(\cat{WM})`$ も集合ではなくて亜群です。$`\quad |\cat{WM}| \in |\mbf{GPD}|\\ \quad \mrm{MMor}(\cat{WM}) \in |\mbf{GPD}| `$ そして、次の関係があります。$`\quad |\cat{WM}| …

…リング複圏から結合（オペラッド結合）や恒等を捨てる〈忘れる〉と複グラフになりますが、この複グラフが単なる複グラフではなくて亜群構造を持っています。亜群上の複グラフについては、以下の過去記事を参照してください。 亜群上の豊穣複グラフ： 豊穣化・基礎強化の例 亜群の射は置換〈permutation〉がベースになっています。ところで、ワイヤリング複圏の結合（オペラッド結合）はワイヤリング図の置換〈substitution〉です。アレレ、用語のコンフリクト〈かち合い〉が生じてしまった…

…フ達が作る圏や複圏〈オペラッド〉に関して長いことモヤモヤしてたのですが、霧が晴れそうです。これで、スケマティック系のまともな定式化も出来そう。要するに道具立てが足りてなかったのです。その道具立てが表題の“圏達の圏のなかのスパン達の二重圏”です。なかなかに大規模・複雑な構造なんですが、これを使えばモヤモヤが解消できる手応えがあります。スケマティック系に関して「これでいける」と感じたのは実は初めてです。ずっと「これじゃない」感がつきまとっていたので。“圏達の圏のなかのスパン達の二…

…圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 オペラッドと型付きラムダ計算 ワイヤリング図とケリー／マックレーン・グラフ 強いて言えば、ストリング図テンプレートで、出現するすべてのノード〈ボックス〉が穴〈プレースホルダー | テンプレート変数〉である場合がワイヤリング図です。しかし、穴ではないノード〈ボックス〉を許したワイヤリング図もあるので、「ワイヤリング図 ＝ ストリング図テンプレート」です。もし、穴しか持たないワイヤリング図を特に参照したいなら純ワイヤリン…

…圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 オペラッドと型付きラムダ計算 圏論におけるフレーム充填問題 1-圏でもフレーム充填問題、因子分解と比較子 フレーム充填問題と解空間関手 ストリング図、ストリング図動画が“使える”とは？ ここから先、$`S, T`$ などは、形状達の圏 $`\cat{S}`$ の対象ではなくて、包含射を表わすとします。包含射は、域と余域から一意的に決まってしまうので、次のように書けます。$`\quad S = (\mrm{dom}(S…

…の一種です。導出系はオペラッドだとみなすといいでしょう。以下の過去記事を参照してください。 演繹系とオペラッド いつものことで、導出系〈演繹系〉とオペラッドでは用語法（概念へのラベルの貼り方）が違います。 オペラッド 演繹系 色 項 または 判断 生成オペレーター {演繹}?ステップ オペレーター {演繹}?ツリー 「演繹〈deduction〉」と「導出〈derivation〉」と「証明〈proof〉」は互いに置き換え可能なので、演繹ステップは、導出ステップ、証明ステップでも…

…あります。 演繹系とオペラッド 論理や型理論の圏論的意味論 // 導出システムの圏と圏の圏 カリー／ハワード／ランベック対応のための“呼び名”と“書き方” // 導出系 また、演繹系と帰納構造との関係は最近の記事で扱っています。 帰納構造と帰納原理 // 演繹系から作る帰納構造 上記記事の最後「「考え直したほうがいい点」」に次のように書きました。 帰納構造の台集合は大きな集合も許すべきだろう。なんなら台集合を宇宙にとってもいい。 帰納構造を、集合論または型理論の宇宙ともっと密…

…ください。 演繹系とオペラッド 演繹系は、生成系〈system of generators | generating system〉が指定された色付きオペラッド〈colored operad〉とみなすのがよいでしょう。演繹系には別な呼び名〈同義語〉が幾つかあります。正規表現パターンで表すなら： {演繹 | 推論 | 導出 | 証明}{系 | システム} オペラッドと用語と演繹系の用語の対応は以下のとおりです。 オペラッドの用語 演繹系の用語 オペラッドの生成系 {演繹 | 推…

…分からないのですが、オペラッドの文脈でも斜モノイド圏が出てきます。 [Lac16] Title: Operadic categories and their skew monoidal categories of collections Author: Stephen Lack Submitted: 20 Oct 2016 Pages: 37p URL: https://arxiv.org/abs/1610.06282 *1:「リントンの定理： 概要、実例、注意事項」の $`…

…〉とする複圏〈色付きオペラッド〉です。これは圏ではありませんが、双線形写像の居場所を提供するだけなので、複圏を知らなくても気にしなくていいです。$`B`$ が有限次元ベクトル空間のあいだの双線形写像であることを以下のように書きます。$`\quad B: (V, W) \to X \In \mbf{FdMultiLin}`$ 双線形写像とテンソル積空間の関係から、次の（集合のあいだの）同型が成立します。$`\quad \mbf{FdMultiLin}( (V, W), X) \…

…「複余有向コンテナ〈オペラッドコンテナ〉によるオペラッドの定義」では、複圏の複射達の集合に上線を使っている。アーマン／チャップマン／ウウスタル〈Danel Ahman, James Chapman, Tarmo Uustalu〉の書き方を踏襲。 「状態遷移系としての前層・余前層・プロ関手」では、反対圏の対象・射に上線を使っている。ボルトルッシ／モンベリ〈Noelia Bortolussi, Martín Mombelli〉の書き方を踏襲。 $`\o{(\hyp)}\:`$ に…

…合とする複圏〈色付きオペラッド〉達の1-圏です。色達の集合を固定しているので、複圏のあいだの一般的な複関手は出てきません。この事例はいずれ詳しく述べます。“一般化圏の製造工場”は抽象度が高い工場で、製造〈出力〉されるものは、ひとつの一般化圏〈圏類似代数系〉ではなくて、一般化圏達が作る1-圏や2-圏です。出力が一般化圏達のドクトリンなのです。一般化圏達のドクトリンに所属するひとつの一般化圏を構成するのはまた別な話になります。$`\mrm{Mnd}_{(\mrm{List}, \…

…なかには、モジュラーオペラッドやテンソルネットワークのように、射〈オペレーション | オペレータ | セル | テンソル〉の“脚”に入力と出力の区別がないものもあります。我々が（比較的に）よく使う“圏、複圏〈オペラッド〉、多圏”では、射の“脚”に入力と出力の区別があります。別な言い方をすると、射が方向〈direction〉を持ちます。射が方向を持つような圏類似代数系を、有向な圏類似代数系〈directed category-like algebraic system〉と呼ぶこ…

…なら、$`A`$ はオペラッド構造を持つだろう、と予想できます。また逆に、$`A`$ 上にオペラッド構造があれば、それから係数付き多項式モナドを作れるでしょう。上記の予想よりもっと一般的なことを誰かが証明していた気がするので、一般的定理の特殊ケースに過ぎないだろうと思います。（ちゃんと確認してないので確信はないけど。）次に、スケマティック（「スケマティック」参照）なリントンの定理（「リントンの定理： 概要、実例、注意事項」も参照）に出てくるリントン／ローヴェア・モナドは、係数…

…内で考えます。複圏〈オペラッド〉を使うアプローチを採用するなら、$`\mrm{SAT}\mbf{Multicat}`$ を使います。$`\mrm{SAT}\mbf{Multicat}`$ の対象は複圏ですが、複関手〈1-射〉と複自然変換〈2-射〉（「回路代数とグラフ置換モナド」参照）により2-圏になります。SAT複圏は一般的複圏の特別なものなので、次の包含関係が成立します。$`\quad \mrm{SAT}\mbf{Multicat} \subseteq \mbf{Multi…

…ategory | オペラッド | operad〉で解釈する前提なら、次のような指標になります。$`\T{signature }\NX{\mrm{Semigroup}}\: \{\\ \quad \T{sort }\NX{U}\\ \quad \T{operation }\NX{m}: (U, U) \to U\\ \quad \T{equation }\NX{\T{assoc}} :: m \mathop{\KX{;_1}} m \twoto m \mathop{\KX{;…

…圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈」に載せたもので、キャンバスをピンク色に塗ることにより、穴とソリッドなボックスを区別しています。矩形キャンバス上に、1つの穴と2つのソリッドなボックスがあります。穴は番号で識別し、ソリッドなボックスに付いているラベルはその内容〈値 | セマンティクス〉です。穴は内容〈中身〉を持ちませんが、境界は持ちます。境界上にはプロファイル情報が乗っています。上の図の穴 1 （1 しかないが）のプロファイルは $`(A, B)\to…

…re}〉には、複圏〈オペラッド〉、多圏、モジュラーオペラッドなどがあります。これらの代数系は、「射」「セル」「オペレーション〈オペレーター〉」「辺」「ボックス」「テンソル」などと呼ばれるモノの集りです。それらのモノには境界プロファイル〈boundary profile〉が決まっています。「射／セル／オペレーション〈オペレーター〉／辺／ボックス／テンソル」の境界プロファイルは、「対象／型／ソート／色／頂点」などと呼ばれるモノの有限コレクションです。では、有限コレクションとは何で…

…使ってみては？ あるいは、既に小さい骨格が使われているかも知れない。 前層やインデックス付き圏を見たら、すぐにグロタンディーク構成しよう。グロタンディーク構成の平坦化圏やファイバー付き圏を使ったほうが見やすいことも多い。 二種類の射があるように思えたら、二重圏あるいは二重圏類似構造が存在するかも。 三種類の射があるように思えたら、三重圏あるいは三重圏類似構造が存在するかも。 オペラッド構造が見つかるといいことあるよ。見つけよう。 モナドが見つかるといいことあるよ。見つけよう。

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

…ています。複グラフはオペラッド〈複圏〉の台です。一般化ハイパーグラフに関して語る場合でも、圏の用語法やオペラッドの用語法が混じってしまいます。異なる典型事例や異なるメンタルモデルに由来する用語・記号がゴチャ混ぜになるので注意が必要です。 一般化ハイパーグラフ 圏 オペラッド〈複圏〉 頂点 対象 色 頂点の集合 対象の集合 色の集合 プロファイル・コンストラクタ（一般論） 集合の平方（具体例） リスト構成と直積構成（具体例） 辺〈ハイパー辺〉 射 オペレーション〈オペレーター〉…

…と圏になります。同様に、反射的複グラフからは複圏〈multicategory | オペラッド | operad〉、反射的多グラフからは多圏〈polycategory〉が構成できます。一般化反射的グラフを定義して、その上に結合的単位的演算〈associative unital operation〉を載せる方法は圏の概念を拡張する際に使えます。特に、米田テンソル計算（「オプティックの圏とコエンドと米田テンソル計算」参照）のような古典テンソル計算の拡張を定義する道具になるでしょう。

複圏〈オペラッド〉はその下部構造に複グラフを持ちます。導出システム〈演繹系〉は、概念的には複グラフそのものです。複グラフを依存型理論で利用したいとき、複グラフにも依存性を導入する必要があります。この記事で、依存性を持つ複グラフを導入します。$` \newcommand{\mrm}[1]{ \mathrm{#1} } %\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} %\newcomm…

…出システムは、複圏〈オペラッド〉と密接に関係があります。導出システムの代わりに、複圏が対象であるような圏をまずは考えてみます。複圏のあいだの射は、通常の準同型射ではなくて、もっとゆるい概念であるプレ準同型射とします。複圏〈オペラッド〉を対象として、複圏のあいだのプレ準同型射を射とする圏が、導出システムの記述と分析にふさわしい気がします。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}[1]{ \mathcal{#…

…ねません。 演繹系とオペラッド 演繹系と閉包系 ここでは、演繹系を導出系〈derivation system〉と呼んでおきます。つまらないリネームですが、つまらないこと（言葉の僅かな違い）に影響を受ける人もいるので*1。「4つの calculus」は「4つの導出系」と言い換えられます。「4つの計算系」、「4つの演繹系」、「4つの証明系」と言っても同じです -- こういうのが無駄なバリエーションなわけですけどね(苦笑)。4つの導出系の概要は： 通常関数計算： 型付きラムダ計算の…

…より演繹系（ある種のオペラッド）のほうが現実的かも知れません。π-インスティチューションの概念（以下の過去記事参照）を、コンテキスト／指標の圏の上で再定義できそうです。 演繹系と閉包系 ダラッっと依存型理論・インスティチューション アブラムスキー達の仕様構造（「ホーア論理の圏論的な定式化」参照）も、コンテキスト／指標の圏に取り込めるかも知れません。この記事では、指標にモデル圏を対応させる関手についてはまったく触れてません。インスティチューション理論の主役はモデルのほうです。指…

…元シーケントは複圏〈オペラッド〉で解釈できます。左辺リストは複圏の対象のリスト、右辺は複圏の対象、シーケント全体は複射と解釈します。左単元シーケント〈left singleton sequent〉は次の形です。$`\quad A \Ent (B_1, \cdots, B_n)`$左単元シーケントは、余複圏（複圏の双対概念）で解釈できます。左辺は余複圏の対象、右辺リストは余複圏の対象のリスト、シーケント全体は余複射ですね。前節で出した多圏、この節で出した複圏／余複圏は、モノイド…

… 演繹系（「演繹系とオペラッド」参照）における、構文的対象の導出可能性〈derivability〉の（メタレベルの）宣言 意味論的構造（例：インスティチューション）における、構文的対象の妥当性〈validity〉の（メタレベルの）宣言 4番の意味でターンスタイルを使うのは見たことないですが、ないとも言い切れません。プロファイル宣言は、圏論の意味での射の域・余域の仕様です。高次圏〈n-圏〉の高次射〈k-射〉、複圏〈オペラッド〉の複射、多圏の多射のプロファイルもあります。構文的対…

…る演繹系（「演繹系とオペラッド」参照）に対するメタレベルの導出可能性には、ターンスタイルではなくて '$`\Vvdash`$' を使う。 依存関数の宣言でもなく、構文的な宣言でもなく、導出可能性でもない意味で使う場合は、なんか別な記法を使う。ターンスタイルの流用はやめる。 カンマのオーバーロード回避の案カンマは、構文定義の際のリスト処理の演算記号として使われます。区切り記号としてのカンマと紛らわしくて僕は不快です。また、シグマ型を構成する演算記号としても使われます。 リスト処…