インスティチューション

グロタンディーク同型

次の同型が成立する。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$$`\prod_{i \in I} {\bf Set}[X, A[i] ] \cong {\bf Bun}[I](X \times I, \sum_I A[\bullet]) \\ \cong {\bf Fam}[I](\mrm{K}^X_I, A[\bullet]) `$名前だ…

2-コンテナとインスティチューション

まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…

BLit と MathBLit

モットー writing is programming (writing as programming) documents should be formally verified ブリットとは: BLit = Web Literature Web上で利用できる、関連する文書達のアーカイブネットワーク マスブリットとは: MathBLit = Mathematics Web L…

関手インステチューション

「インスティチューション+関手意味論」のフレームワーク、なんか名前を付けないと呼びようがない。そのまんまだけど、関手インスティチューションとか。関手インスティチューションの構成素は: 指標の圏、具体的に構成される 指標の圏のinclusive構造 代…

フラグメントによる論理条件

$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$$`\mrm{Ext}(\Sigma)`$ は拡張指標(派生指標)の全体。すると、$`\quad \Gamma \in \mrm{Ext}(\Sigma) \…

インスティチューションに対する不満

$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$ 証明の定式化が欠けている。→ πインスティチューション 非論理的指標部分と論理条件が分離されている。…

2005年7月の課題

課題と参考文献: インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩:変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩:有限変換キューと半…

ドクトリンの定式化

ドクトリンは、ドミニオンを支配〈ドミネイト〉する構造として存在する。“指標の圏”達のタワーをバックボーンタワー〈ユグドラシル〉と呼ぶ。ドミニオンの構成素: 自由忘却随伴系 ターゲット代数 上位レイヤーのドミニオンを次のように書く。 自由忘却随伴…

混乱の原因と課題

可換モナドとラックス・モノイド・モナド(動機も少し) - 檜山正幸のキマイラ飼育記 (はてなBlog) 指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。ストリング図の併置は直…

関手インスティチューションと様々な圏

次の概念が識別されてないと曖昧模糊になる。 具象圏のベース圏 モデルの圏(関手圏)のターゲット圏〈モデルのアビタベース〉 関手インスティチューション〈functorial institution〉のアンビエント圏〈ターゲット圏のアビタ〉 相対モナド(言語モナド)の…

Σ-項

Σを指標として、Σはメタ指標Σ'の配下〈governed by〉にあるとする。Σで導入(新規に定義)された記号を使って書かれた構文的対象物〈syntactic object〉をΣ-項と呼ぶ。Σ-項は、ΣのΣ'による自由閉包〈free closure〉の要素になる。Σ-項に対する演算は、Σ'によ…

セオリーとインスティチューション

n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編に書いてあることが我ながら凄いな。なんで気付いたのだ?最近とは用語法・記法が違うので対応表。 過去 最近 Σk kΣ Ak kA k-Spef[-] (-)-kSig k-Mod[-] (-)-kAlg Ck なし Ck…

状態述語随伴とインスティチューション

プログラムfを状態変換子とみたものを f*、プログラムfを述語換子とみたものを f* とすると: < x | f*(q)> = < f*(x) | q> が成立するのではないか、これはインスティチューションの充足関係 x |= f*(q) ⇔ f*(x) |= q と同じではないか。つまり、 状態変換…