セオリー論
括弧に入れたものは、あまり興味を持たれてない。 一般 述語論理 データベース 遷移系 線形代数 指標 集合 スキーマ＠グラフ アルファベット 生成集合〈基底〉 指標の圏 集合圏 グラフの圏 集合圏 集合圏 コンビネーション 要素 カラムパス 字のストリング …
ゴチャゴチャとメモ。指標の同義語類義語 シグネチャ＠ML インターフェイス＠オブジェクト指向言語 コンセプト＠C++ 型クラス＠Haskell 型クラス＠Coq モジュール＠Objファミリー 手続きの同義語類義語 ファンクタ＠ML アダプター＠デザインパターン 型パラ…
強モナド (T, μ, η, s)/C が構文的だとは： 基礎圏 C は挿入的余デカルト・モノイド圏 モナドは強度 s とその余強度〈右強度〉に対して可換モナド モナド単位は、Cの挿入。 挿入的モノイド圏〈insertive monoidal category〉とは： 挿入〈insertion〉の圏と…
線形代数 セオリー論 事例1：遷移系 事例2：階層構造 基底 指標 集合＝アルファベット 単純DAG＝ハッセ図 基底の要素 記号セル 要素＝文字 アロー、辺 線形結合 コンビネーション 文字列＝ストリング パス 自由ベクトル空間 セオリー 自由モノイド 自由やせ…
Graphvis Online digraph { rankdir = BT subgraph cluster_msyn { MetaSig } subgraph cluster_syn { Sig } subgraph cluster_msem { MetaClass Amb[label="Amb/Def"] MetaTarg Amb -> MetaClass[label="class-of"] Amb -> MetaTarg[label="habitat-of"] Me…
コンテナスキーマの形状と位置集合〈set of positions〉の組 を仮にテンプレートと呼ぶと。以下は同義語。 コンテナスキーマのテンプレート 変数出現を持つ式と変数出現の集合 変数出現を持つ項と変数出現の集合 形状がストリング図のときは、ストリング図と…
記号＝シンボル＝文字＝名前＝ラベル 代入＝割り当て 具体物＝具体値＝モデル＝値 次の正規表現はすべて同じ意味 {記号 | シンボル | 文字 | 名前 | ラベル}に{具体物 | 具体値 | モデル | 値}を{代入する | 割り当てる} {記号 | シンボル | 文字 | 名前 | …
Twitterでつぶやいていた内容の一部をメモにしておこう。無名指標と入れ子指標無名指標または指標リテラルは、sig {...} の形で書く。 sig { sort U operation e:ε → U operation m:(U, U) → U }これはモノイド指標（monoidal signature、「モノイドの指標」…
定義1： 論理式の集合（生成系） 定義2： 演繹閉な論理式の集合（順序閉包） 定義3： 証明〈推論規則〉の集合（生成系） 定義4： リーズニング閉な証明〈推論規則〉の集合（リーズニング閉包＝圏） 定義5： 生成系を持つ圏 定義5'： 指標〈生成系〉を持つ圏 …
暫定案、後で修正。日本語だと複数形がないので、複数形の代わりに「ナントカセット」とする。 セオリー論 プログラミング 論理 ストリング図 指標 インターフェイス 推論規則セット スパイダーセット〈アイコンパレット〉 ソート 型 命題 ワイヤー（のラベ…
実体〈entity | thing | stuff〉に対して、そのアビタ（直接的）とアビタベース（間接的）の区別がついてなかったのではないか？ アビタは型インスタンスの型クラスと言っていいが、アビタベースはベース型クラスとは違う概念。 アビタベース＝“指標のターゲ…
関手インスティチューションと様々な圏 - (新) 檜山正幸のキマイラ飼育記 メモ編 のセッティングで話をする。Sをグラフ（あるいはコンピュータッド）と見た指標の圏で、射はプレーンな（モナドで拡張してない）射とする。Sはアンビエント圏への埋め込み J:S→…
次の概念が識別されてないと曖昧模糊になる。 具象圏のベース圏 モデルの圏（関手圏）のターゲット圏〈モデルのアビタベース〉 関手インスティチューション〈functorial institution〉のアンビエント圏〈ターゲット圏のアビタ〉 相対モナド（言語モナド）の…
CがB上の具象圏〈concrete category〉であるとき、Bはベース圏〈base category〉、具象構造を構成している関手 U:B→B をベーシング関手〈basing functor〉と呼ぶことにする。忘却関手と呼ぶのをやめる！U:C→B, V:B→A が2つの具象圏のとき、ベーシング関手を…
セオリー論 その他 指標 インターフェイス インハビタント インスタンス、構造、モデル、代数 アビタ クラス、型クラス、モデル・代数の圏 アビタベース クラスのベースクラス、モデルのターゲット圏 全体構造はインスティチューションのなかでしか理解でき…
スタッフ〈stuff〉はモノ〈thing〉とか構成素〈constituent〉と同じ。構造は、スタッフと性質からなる。性質は公理で定義される。性質を持つ⇔公理を満たす、性質を持つ⇔定理を満たす。公理は条件〈condition〉制約〈constraint | 拘束〉ともいう。忘却関手は…
セオリーのタワーが安定するという言い方をしてきた。 デカルト・タワーを求めて - 檜山正幸のキマイラ飼育記 (はてなBlog) 安定でもいいが循環的〈circulative〉が良さそう、メタ循環的という言葉は既にあるし、僕も使っている。ただし、メタ循環的は meta-…
等式的延長〈equational prolongation〉について述べる。Xを集合として、Δ(X) をXの対角集合とする。Δ(X) X 。Δk(X) を次のように帰納的に定義する。 Δ0 := X Δk+1 := {(x, y)∈Δk(X)×Δk(X) | x = y} 特に、 Δ1 := {(x, y)∈Δ0(X)×Δ0(X) | x = y} = Δ(X) ik:Δk…
球体的n-マグマを使うアプローチは、次の状況で使う。 構成的 v.s. 非構成的 →構成的 組み合わせ的 v.s. 非組み合わせ的 →組み合わせ的 形状 →球体 次元の上限 →有限 マグマ演算〈magma operation〉＝結合〈composition〉が定義されている。Xはn次元球体的集…
Σを指標として、Σはメタ指標Σ'の配下〈governed by〉にあるとする。Σで導入（新規に定義）された記号を使って書かれた構文的対象物〈syntactic object〉をΣ-項と呼ぶ。Σ-項は、ΣのΣ'による自由閉包〈free closure〉の要素になる。Σ-項に対する演算は、Σ'によ…
適宜追加予定。 名前 使ったことがある 恒等関手 I, IdC, J モノイド積 , P, Y, × 単位射 i, J, I 単位対象 I, 1, 1 自明圏 I, I 自明集合 1, 1 自明アトム *, 0 対角 Δ, δ 潰し関手 K, !' 射影 π1, Π1, proj1 2-圏の恒等 IDK 恒等自然変換 IDF, ιF 自明厳密…
マイクロコスモス原理関係記事： デカルト圏、こんな定義もあります - 檜山正幸のキマイラ飼育記 (はてなBlog) http://m-hiyama.hatenablog.com/entry/20111124/1322100492 マイクロコスモ原理の恐怖 - 檜山正幸のキマイラ飼育記 (はてなBlog) http://m-hiya…
階数 r を横に、縦に次元・弱性 ν を取って、圏論的実体の表。 r = 0 r = 1 r = 2 宇宙 U0 U1 U2 ν = 0 Set SET SET ν = 1 Cat CAT CAT ν = s2 s2-Cat s2-CAT s2-CAT ν = w2 Bicat BICAT BICAT truncation は、Cat↓1 など、prolongation Set↑2 など。Set↓0 =…
考える素材に。不完全。 レベル 0 1 2 3 典型圏 10-Cat#0 21-Cat#1 22-Cat#2 23-Cat#3 別名 Set CAT CAT 一般圏 C 対象変数 A C 対象定数 1 I, Set I, CAT CAT 射変数 f F 射定数 !A , Δ, Π × 2-射変数 なし α, β 2-射定数 なし !, δ, π 実際に使う予定の記…
デカルト・モノイド圏は、デカルト・モノイド圏のなかで定義される。 外のCAT 定義されるC I in CAT 1 in C ★ in CAT ☆ in CAT I~:★→CAT in CAT 1~:☆→C in CAT (-×-):CAT×CAT in CAT P:C×C→C in CAT <-, ->:CAT∧CAT in CAT Q:C∧C→C in CAT Δ::CAT^⇒Δ*P:CAT→C…
次の理論達はすべて表層理論だ。 共変微分（コジュール接続）の理論 主接続（カルタン接続）の理論 エーレスマン接続の理論 平行移動の理論 背後にあるウル理論〈Ur-theory〉（原理論、理論のイデア）は 接続のウル理論 「接続」という概念的実体（イデア）…
横と縦があるので、 縦方向の列＝ピア〈pier〉（peerではない！） 横方向＝フロア フロアの数＝ストーリー 次のように呼ぶのが良さそう。∈0 は「対象として所属する」。 指標Σ ∈0 リテラチャーL ターゲット圏C ∈0 アンビエントA 指標とターゲット圏から決ま…
次の列がある。 Set = Total ⊆ Partial ⊆ ND Totalは双デカルトな半環圏、NDはテンソル半加法圏、Partialはその中間のなにか。これは、ND上に積み上がった3段のパレスになっている。フレイド圏 J:C→D も埋め込みJで C⊆D と考えれば二段のパレスだ。どうもパ…
パレス、使える！ - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。デカルト作用圏（例えば、デカルト作用圏が面白い - 檜山正幸のキマイラ飼育記 (はてなBlog)）の純部分圏は、やはりパレスの例になっている。フレイド圏ももちろんそうだ。パレスの例は： …
n段のパレス - (新) 檜山正幸のキマイラ飼育記 メモ編 いったん気付いてしまうと、これは使える感じ。非関手／非自然変換の手法と相性がいい。圏論的モダリティも、パレスを作る手法と解釈できる。テンソル計算では、次のようなパレスが使える。 複線形写像…
