…インスタンス -- 一般関手モデル 一般関手モデル：「圏の表示」の圏 Quivを箙の圏とします（既に出てきました）。Quivには始対象・直和・余等値核〈余イコライザー〉を定義できます。終対象・直積も定義できるので、モノイド積として直積を選びます。これにより、Quivは有限余完備でモノイド積を持つ圏となります。このQuivが、関手データモデルのスキーマの圏、インスティチューションの指標圏に相当します。二項関手 E:Quivop×Cat→Cat を次のように定義します。 E(X,…

…表現可能関手の話題 一般関手モデル：インスタンスの余タプリングと貼り合わせ カリー／ハワード対応の新しい仲間 独身男性にもコウノトリはモナドを運んでくるのか カン拡張っぽいアレコレ データベースとカン拡張と思い出 *1:[追記]もちろん、整理すればシッチャカメッチャカなんてことはありません。断片的な情報を脈絡なく収集すると、シッチャカメッチャカな印象を受けるであろう、ということです。[/追記] *2:カン拡張の定義が何種類かあります。そのことは、nLabエントリー https…

…頂点です。詳しくは「一般関手モデル：相対スキーマと相対インスタンス」を参照してください。伝統的オートマトンの場合は、可視部分グラフは2個の頂点{0, 2}からなる離散グラフ（辺はない）で、K(0) = 1, K(2) = B で定義される K:{0, 2}→|Set| を固定化関手と思ってもかまいません。これから考える指標グラフΦには、開始頂点族Sと識別頂点族Dが組み込まれているとして、Φ = (Φ, S, D) のように記します（記号の乱用）。また、固定化関手Kも入れた (…

…記事に書きました。 一般関手モデル：インスティチューションとの関係 Alloyとの類似性に関して言えば、「Alloyを理屈っぽく考えてみようと思う」で次のように書いたことがあります。 関手データモデルとAlloyは、かなり親和性が高いんじゃないか、と感じるのです。[...snip...]また、関手データモデルを理解する道具としてAlloyが役に立つとも言えます。 これはつまり、AlloyのモデルとFQL／OPLのモデルは似てるってことです。今ではFQL／OPLが使えるので、関…

…となります。Sch を指標圏とみなしたインスティチューションの構造が入ります（「一般関手モデル：インスティチューションとの関係」参照）。また、DB:Sch→CAT は、導来子（derivator）とみなせそうです（グロタンディークの導来子の条件を多少弱める必要があるかも知れませんが）。と、なにやら関手圏がやたらに出てきます。関手圏て、現象を記述する基本的な言葉なのかもなー、と思ったりします。 *1:状態遷移系とオートマトンはほとんど同義語で、あまり厳密な区別はないと思います。

…組みを提供します。「一般関手モデル：相対スキーマと相対インスタンス」は、この話題を扱っています。関手（ファンクトリアル）データモデルの上に構築された新しい問い合わせ理論は、その一部が実装されるだけでも、データ処理の面目を一新しそうです。 Database queries and constraints via lifting problems (http://arxiv.org/abs/1202.2591) スピヴァック理論を既存理論と対比してみるのはもう終わりにします。それ…

「一般関手モデル：インスティチューションとの関係」にて： 実際のところ、特別に一般化する必要性は薄いですね、スピヴァック理論が既に十分に一般的に作られているので。 強いて一般化する点を挙げてみます。アンビエント圏をSet以外に取り替えることは既にスピヴァックがやっているので、アンビエント圏は関手モデルのパラメータです。スキーマ全体の圏Schも色々と動かせるのでパラメータなんですが、今のところスピヴァックは Sch⊆Cat を仮定しているように見受けられます。まー、スピヴァック…

一般関手モデルは、スピヴァックの関手データモデルをデータベース以外にも適用する試みです。とはいえ実際のところ、特別に一般化する必要性は薄いですね、スピヴァック理論が既に十分に一般的に作られているので。今回の話も二番煎じで、関手データモデルがインスティチューションを定義することは既にスピヴァックが示しています。この事実を、観点と記述スタイルを若干変えて説明してみます。内容： 言葉と記号の約束 だいたいのところ（概要） 有向グラフに対する圏的演繹系とグラフ制約の圏 Pathモナド…

[追記 date="2024-04-18"]（11年以上の時を経て）用語法はだいぶ変わっています。 この記事 10年後 圏の表示の圏 Prs 形状の圏、または指標の圏 圏の表示（Prs の対象） 1-コンピュータッド ドクトリン（Sch） ？ アンビエント圏（Set） ターゲット圏 「アンビエント」の意味・使用法は変わっています。ターゲット圏（この記事の“アンビエント圏”）が所属する2-圏がアンビエントです。今の場合、ターゲット圏（この記事の“アンビエント圏”）が $`{\b…

…インスタンス -- 一般関手モデル 一般関手モデル：インスタンスのモノイド積とテンソル積 Schを“圏の圏”として、ドクトリンと呼びます。ドクトリンの対象 S, T などがスキーマであり、個々のスキーマは圏です。スキーマのあいだの関手 σ:S→T はドクトリンの射（σ∈Mor(Sch)）ですが、σをスキーマ準同型射（あるいは単にスキーマ準同型）、スキーマ射などと呼びます。ドクトリンと呼ぶ圏の射が、対象であるスキーマのあいだの準同型射なので注意してください。スキーマ射は、ときに…

「一般関手モデル：インスタンスの余タプリングと貼り合わせ」の続き。「一般関手モデル」というタイトルの記事は、スピヴァック理論それ自体の解説じゃなくて、スピヴァックに触発されて僕が考えたことのメモです。関手モデルでは、スキーマが圏なので、スキーマ全体の圏は“圏の圏”です。「スキーマの圏」という言葉は曖昧で紛らわしいです。スキーマ全体の圏はなんか別な呼び名を与えておいたほうがいいでしょう。ベック（Jon Beck）によるドクトリン（doctrine）という言葉があります。ある種の…

…インスタンス -- 一般関手モデル」に書いた“スピヴァックの処方箋”に従うと、考えるスキーマの全体である“圏の圏”Schとアンビエント圏Cを決めると、グロタンディーク構成により圏のファイブレーション ∫(s∈Sch | [s, C]) → Sch ができるのでした。以下、平坦化された圏 ∫(s∈Sch | [s, C]) を単にInstと書くことにします。Instの対象は、スキーマSとその上のインスタンス F:S→C の組 (S, F) です。Instの射 (S, F)→(T…

…連するエントリー： 一般関手モデル：インスタンスの余タプリングと貼り合わせ 一般関手モデル：インスタンスのモノイド積とテンソル積 一般関手モデル：相対スキーマと相対インスタンス 一般関手モデル：「圏の表示」の圏 一般関手モデル：インスティチューションとの関係 一般関手モデル：どこを一般化？ *1:ほんとにCatの部分圏でなくても、Catの部分圏に圏同値となる圏ならかまいません。 *2:これは、インスティチューション理論の習慣を採用しました。スキーマと、インスティチューションの…