セオリー論
以前にも書いたが、包含的圏〈inclusive category〉は、 Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 包含系は： Grot…
次の記事の内容を今の言葉で書き直す。 n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編 セオリーとインスティチューション - (新) 檜山正幸のキマイラ飼育記 メモ編
指標と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog) パート分けと多パート指標〈multipart signature〉は、テレスコープで解釈できる。法則パートを定義できれば、有法則指標と無法則指標の概念も定義できる。$`(S \sqsubseteq T)`$ のとき、$`S`$ が無法…
$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$ $`\cat{Sign}`$ 指標の圏 $`\cat{Alg}`$ 代数の圏 $`\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}`$ 自由忘却随伴系 $`J:\ca…
https://www.win.tue.nl/automath/archive/pdf/aut103.pdf Telescopic mappings in typed lambda calculus by N.G. de Bruijn ド・ブラウンのテレスコープ https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanのテレス…
相対指標と利用法 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$指標の圏は $`\cat{Sign}`$ と書く。指標はローマン体大文字。指標…
基本的道具は： Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 特に、"3 Inclusive Institutions" 。$`\newcommand{\cat…
https://m-hiyama-memo.hatenablog.jp/entry/20171209/1512807104 からコピー 用語法、表記法 オペレーター | オペレータ | 演算子 | 作用素 | コンビネータ | コンビネーター コンストラクタ | コンストラクター | 構成子 | 構築子 | 生成子 例 トレースオ…
Σ〈$`\Sigma`$〉なんらかの意味の指標、D〈$`D`$〉はドクトリンだとして、$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{ \text{ in } } \newcommand{\mrm}[1]{ \mathrm{#1} } %`$$`\quad \cat{C} = \mrm{Th}^D(\Sigma)`$とする。$`\cat{E}`$ を同…
フラットコンステレーション＝ストリング図テンプレート⊇ワイヤリング図 ソリッドディスク＝ストリング図⊇無ノード・ワイヤリング図＝スパイダー図 外サークル＝ストリング図のキャンバス境界 内サークル達＝ストリング図テンプレートのスロット境界達 中間…
右の欄はローヴェアの代数セオリー。 アリーナ コンステレーション 代数指標 カローラ テンプレート オペレーション アリーナ テンプレートキット 指標 ツリー コンステレーション 項 フォレスト コンステレーションキット 割り当て〈代入〉系 リーフ スロッ…
次のような対応があると思う。 テレスコープ ←→ フォレスト テレスコープのシグマ構成圏の対象 ←→ フォレストのパス テレスコープのシグマ構成圏の対象集合 ←→ フォレストのパス集合 テレスコープに関して、レベルk（k - 0, 1, ...）のベース圏を考える。レ…
カリー同型とフビニ定理は切っても切れない。フビニ定理は、カリー同型で互いに移る高階関数と多変数関数の積分が一致することを主張している。同様に、依存カリー同型と依存フビニ定理は切っても切れない。依存フビニ定理は、カリー同型で互いに移る高階依…
カリー同型は、複関数〈multifunction | 多重関数 | 多変数関数〉と高階関数〈higher-order function〉との1：1対応を与える。同様に、依存カリー同型は、依存複関数と依存高階関数のあいだの対応を与える。さらに、関数を関手に一般化するると、依存複関手…
テレスコープとグロタンディーク構成とグロタンディーク／フビニの定理の関係：indexed thing = indexed family of things を単にファミリーと呼ぶ。インデックス付き圏もファミリーになる。テレスコープはファミリーに関して定義できる。テレスコープの第1…
Wikipediaに ニコラース・ホーヴァート・ド・ブラウン という項目があるので、「ド・ブラウン」にする。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1} } %`$Automathの論文 "Telescopic mappings in typed lambda calculus" by N.…
コンテナ〈ファミリー〉の演算と特別な射： {{ディリクレ}?{テンソル}?}!積 $`\otimes`$ ： コンテナ＆レンズ演算〈(0 | 1)-オペレーター〉、遷移系の演算とも考えられる。 ジョイン $`\triangleleft, \triangleright`$ ： 遷移系の演算、遷移系だけ考えると…
k-オペレータはk-射に作用するオペレータ、関手は (0 | 1)-オペレータ。 絵図要素 圏論 射の次元 ワイヤー 対象 Cの0-射 ノード 射 Cの1-射 ボックス 1-オペレータ Cの射ではない 細いストライプ 0-オペレータ Cの射ではない ストライプ 関手 Cの射ではない …
公理系を演繹的に拡大するメカニズムの定式化に： 閉包システム〈closure system〉 単純伴意システム〈simple entailment sysmte〉 バンチ伴意システム〈bunched entailment sysmte〉 双対バンチ伴意システム〈dual bunched entailment sysmte〉 伴意関係を …
構文は： law 2-ラベル :: 閉じた論理式または variable 変数の型宣言 law 2-ラベル :: 自由変数を含む論理式法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。事例： signature LawlessMonoid within Set { sort U operation e: 1 → U ope…
指標 $`\Sigma`$ の文法 $`G`$ によるセオリー $`\mathrm{Th}^G(\Sigma)`$ は $`G`$-代数構造を持つ。もし、ドクトリンが無法則指標ならば、文法に含まれるコネクティブはドクトリン指標のラベルで、コネクティブ記号自体が$`G`$-代数構造の演算記号に使える…
ストレージの日本語は「格納器」にするかな。格納器には次がある。 ファイルシステム ： ファイル名／パス名がキー 各種データベース ： IDフィールドの値がキー プログラミング言語が管理するメモリー空間 ： ハッシュマップ／ディクショナリのキーがキー …
基本はフローグラフだな。フローグラフは集合圏上のモナドになる。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in }} \newcommand{\twoto}{\Rightarrow} \newcommand{\Id}{\mathrm{Id}} %`$ $`\mrm{FlGrph}:{\bf Set} \to {\bf Set}\In {\…
セオリー論 Tenjin 0-ラベル ターム, トピック 0-指標 トピック 0-コンビネーション シナリオ〈フローグラフ〉 0-手続き パッケージ〈ライブラリ〉 ターム／トピックを格納するコンテナがノート〈記述子〉／記事で、その物理的実体は： 記事の実体はMarkdown…
$`\newcommand{\mrm}[1]{ \mathrm{#1} }% \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\ClassOf}{\Keyword{ClassOf } }% \newcommand{\Things}{\Keyword{ Things} } %`$関係圏を2-圏のインスタンスとみ…
ドクトリンは、ドミニオンを支配〈ドミネイト〉する構造として存在する。“指標の圏”達のタワーをバックボーンタワー〈ユグドラシル〉と呼ぶ。ドミニオンの構成素： 自由忘却随伴系 ターゲット代数 上位レイヤーのドミニオンを次のように書く。 自由忘却随伴…
可換モナドとラックス・モノイド・モナド（動機も少し） - 檜山正幸のキマイラ飼育記 (はてなBlog) 指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。ストリング図の併置は直…
まとめておく。 一般 線形代数 遷移系（モノイド） DB（圏） 述語論理 左域 C Set Set Graph Set 右域 D Vect Mon Cat Set 左関手 F FreeVect FreeMon FreeCat Id 右関手 U ForgetVect ForgetMon ForgetCat Id 線形代数はドミニオン意味パートが面白くない。…
一般 線形代数 モノイド 圏 左域 C Set Set Graph 右域 D Vect Mon Cat 左関手 F FreeVect FreeMon FreeCat 右関手 U ForgetVect ForgetMon ForgetCat 単位 η linEmbed monEmbed catEmbed 余単位 ε linCalc monCalc catCalc モナド M LinComb MonComb CatCom…
「k-項のあいだの等式＝恒等(k + 1)-射」と考える。「等式は恒等射」主義。すべての次元に渡って等式を集めることは、すべての次元に渡って恒等射を集めること。できた恒等射の圏は無限次元圏だが、すべての次元でやせた無限次元圏。一般的に、両端＝境界を…
