…6-06(日曜)）、インスティチューション理論についてほんの少しだけ説明しました（チアガールズの説明のほうが長かった気がする）。インスティチューションについては、「キマイラ飼育記」の初期の頃からチョコチョコ触れています。 「インスティチューション」の検索結果 インスティチューションに関する資料として、僕が最初に思い浮かべるのはゴグエン〈Joseph Goguen〉による次のページです。 https://cseweb.ucsd.edu/~goguen/projs/inst.ht…

…Burstall〉のインスティチューション〈institutions〉や、ローヴェア〈William Lawvere〉のハイパードクトリン〈hyperdoctrine〉との関連もありそうです。インスティチューション／ハイパードクトリンからの知見を、ベイズ論理／ベイズ計算に活かせるかも知れません。例えば、「順序集合のカン拡張と特徴述語論理」の手法で限量子を定義できそうな気がします。ベイズ確率論の新しい風を感じたい人、従来の理論にモヤモヤを感じている人は、ジェイコブス・スタイル（…

…理の圏論的な定式化 インスティチューションとホーア論理 というわけで、クリーネ代数／テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を与えてくれます。これが、クリーネ代数／テスト付きクリーネ代数に興味を持つ（ひとつの、しかし大きな）動機です。クリーネ代数とは何かクリーネ代数を一言でいえば、アフィン線形不動点方程式を扱うための代数系です。となると、アフィン線形不動点方程式とは何か、から説明を始めるべきでしょう。…

…scu〉のエッセイ「インスティチューション、中観派、一般モデル理論〈Institutions, Madhyamaka, and Universal Model Theory〉」を紹介しました。中観派〈ちゅうがんは〉は大乗仏教の学派です。ダイアコネスクは、中観派思想を熱心に勉強した上で、それがインスティチューション／一般モデル理論／圏論などと同じ発想だと言っています。でも僕は、仏教は何も知らない（勉強する気もない）ので、ほんとのところ「同じ発想」かどうかは分かりません。確信がな…

…デルのスキーマの圏、インスティチューションの指標圏に相当します。二項関手 E:Quivop×Cat→Cat を次のように定義します。 E(X, C) := [X◇, C] ここで、[-, -]は圏Catの内部ホム、つまり関手圏です。Xは箙ですが、X◇は圏なので、関手圏[X◇, C]を作れます。Eは、s:X→Y in Quiv に対してはsの前結合で反変的に、H:C→D に対してはHの後結合で共変的になります。E(X, C)は、関手データモデルのデータベース状態〈データベース・…

…そのテの知識がないと理解できないことが残念な点です。特定分野の予備知識を要求しない事例があるといいんですが … 何かあったら教えてください。 *1:とある圏の終対象または始対象の議論なのに、あえて「普遍」とか難しげな言葉を使う理由が分かりません。 *2:「ケンロニスト」はbonotakeさんによる造語 *3:"migration"の訳語は「転送」「移動」「移送」とかもあるでしょう。 *4:インスティチューション理論では、リダクト関手〈reduct functor〉と呼びます。

…と複雑な構造（たぶんインスティチューション）が現れます。また、条件分岐や繰り返しの制御構造を入れれば、それも複雑さにつながります。オモチャでない実用的プログラミング言語の意味論が随分と複雑そうなことは想像できるでしょう。しかし、その複雑さのなかに面白くて深い構造が潜んでいると期待もできるのです。 *1:0は自然数に含めます。 *2:valが何でもいいときは、違うリテラルが同じ値を指すことがあり、また、リテラルでは表現できない値も存在します。リテラルで表現できなくても、リテラル…

…いて書かれています。インスティチューションについての解説があります。例えば、大乗仏教中観派の話の予備知識が得られます。 Stochastic Integration with Jumps Stochastic Integration with Jumps (Encyclopedia of Mathematics and its Applications)作者: Klaus Bichteler出版社/メーカー: Cambridge University Press発売日: 20…

…クのエッセイの主題はインスティチューション（Institutions）と一般モデル理論（Universal Model Theory）です。ダイアコネスクはこの分野における第一人者なので、その主題的内容は完全に信用できるものです。となると、“欺瞞”かどうかの分かれ目は、この主題に対して仏教や中観派を持ち出すのが適切なのか？ 仏教／中観派に関する理解が行き届いているのか？ あたりでしょう。しかし、仏教がうんぬんなんて、僕には全く判断できません。とりあえず、仏教／中観派に関するダ…

…on 2 3 のようにします。…… …… フエーッ、こんなん、僕の欲しいオーバーロードじゃない！*2 *1:Haskellでの標準的な方法は、型クラスNumを経由して足し算モノイドと掛け算モノイドを定義するものです。 *2:例えば、掛け算でも足し算でも通用する話をするとき、演算子記号を◇とかして、(◇) = (*) か (◇) = (+) かの区別は、「話の文脈」として与えるべきなんでしょう。ここらへんをキチンと分析するなら、インスティチューション理論を使うべきかと思います。

…と置換原則 できればインスティチューションで分析したいところ。割と圏論バッキバキだったりするんだけど： 圏論とオブジェクト指向 インスティチューションと型階層 インスティチューションと Categories-as-Types インスティチューションとホーア論理 Haskellでは型同士の継承をサポートしていませんが、型クラスから型インスタンスへの継承はできるため、それを利用した多態性の実現が可能です。 「型クラスから型インスタンス」は文字通りインスタンス化であって継承とは言わ…

…ure）と呼びます。インスティチューション理論では、指標をギリシャ文字大文字で表す習慣があるので、それに従ってギリシャ文字大文字を使ったのです。Φはグラフですが、圏と同様な記法を使って、頂点の集合を|Φ|、x, y∈|Φ| に対して2頂点のあいだの辺の集合をΦ(x, y)で表します。伝統的オートマトンAに対する指標グラフΦは次の通りです。 |Φ| = {0, 1, 2} Φ(0, 1) = {i} Φ(1, 1) = Γ Φ(1, 2) = {t} それ以外のΦ(n, m)は…

… sentenceはインスティチューションの用語です。インスティチューションでは、|= をsatisfaction relationと呼びます。 動詞として、deduce, refine, infer, reasonなどもありますが、この表では使ってません。 |- を使ったjudgmentの左（premisesと書いた）はcontextということもあります。特に型理論ではcontextが多いです。 記号法／用語法だけでなく、内容的な補足をちょっとしておきます。|-, |=, …

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

…則を使うこの方式は、インスティチューションとの対応がハッキリしていて、個人的には使いやすく感じます。アンバンドル方式アンバンドル方式で何をバラすのかというと、指標に含まれる「台集合、二項演算、単位元」を別々なパラメータとして法則を表すクラスに渡すのです。 (* === アンバンドル方式 === *) Class MonoidUnbundle {A: Set} (op: A -> A -> A) (u: A) := { (* モノイドの法則 *) assoc'': forall…

…」に分けるやり方は、インスティチューションを意識しています。Σを指標とするとき、インスティチューションではモデル圏Mod[Σ]を定義しますが、Coqの型クラスとしてのΣマグマクラスは、モデル圏 Mod[Σ]の対象類 |Mod[Σ]| = Obj(Mod[Σ]) に対応します。指標Σの論理式の集合Sen[Σ]の部分集合Aを公理として特定したとき、Aを満たすモデルの全体は|Mod[Σ]|の部分類を定義します。公理系Aを記述したCoqの型クラスが、構造の法則クラスです。法則クラスは…

…すために使おう。Σはインスティチューション理論で指標（signature）を表すために使われる記号です。指標はアルファベットの拡張概念ですから関連はあるのです。グラフ理論からすると異例の記号法ですが、Σ, Γ などで有向グラフを表します。総和記号と紛らわしいことには目をつぶります。というわけで、オートマトン F:Σ→Set のように書くことにします。値を取る圏は具体的な圏を想定しているので、Set、PtSet、Rel などが登場します。有向グラフと指標に関する用語と記号法関手…

…つからなかったので、インスティチューション理論の言葉を拝借しました。αB := αtBα と置くと、次の“指数法則”が成立します。δ = δT:T→T は単位行列だとします（遷移写像δと記号がかぶってますが、これも文脈で判断）。 α(βC) = αβC （α:S→T、β:T→U、C:U→U） δB = B B ≦ B' ならば、αB ≦ αB' これらの法則は、定義からすぐに出ます。インデックス付き圏 AutomH[-]基数条件χを固定して、MatχB を考えます。Bはブール…

…いるのでしょうか？ 超フィルターモナドを生成する随伴は位相的に構成できますが、ジリィ・モナドに対応する随伴はどういうものでしょう？論理にはモデル論（「コンパクト空間と論理／モデル論」参照）、さらにはインスティチューション（抽象モデル論）がありますが、確率におけるインスティチューションとはなんでしょうか？ それは確率遷移系の仕様記述に使えるでしょうか（「仕様技術への道 -- インスティチューションを縮めてみる」参照）。疑問符を並べただけですね。締まりがないけど、今日はコレダケ。

…す。より具体的な話は次の機会とします。 *1:構文的な観点から言うなら、自由変数を含まない論理式は「閉じた論理式」と呼ぶべきでしょう。 *2:解釈のための世界Wは固定しますが、Wを色々と動かすときもあります。インスティチューションは、解釈の世界を変えていく系統的な枠組です。 *3:例えば、モデルは順序集合や位相空間かもしれません。 *4:[追記]反例モデルを持つ命題を、「反証可能」と呼ぶようです。だけど、科学哲学で使われる印象が強いので、この言葉は僕は使わないかも。[/追記]

…イヤー指標の圏の上にインスティチューションを作るときにも利用できることを注意しておきます。もう少しCを集合圏の部分デカルト圏（終対象を含み、直積で閉じている部分圏）だとします。メイヤー対 (M, V) は、C上の両モナドを定義します。A∈|C| に対して F(A) := M×A、G(A) := V×A とすると、Mのモノイド構造からFをモナド、Vの余モノイド構造からGを余モナドとみなせます。M×(V×A) と V×(M×A) の同型から、FとGの順序を交換する自然変換も定義で…

…「名前の削減問題からインスティチューションへ」で出した掛け算の法則 mult(unit, x) == x mult(x, unit) == x mult(mult(x, y), z) == mult(x, mult(y, z)) これはモノイドの公理系です。集合ベースのモノイド（普通のモノイドです）は、集合Mと2つの関数（写像）からなる代数的構造です。2つの関数は次の形です。 u:1→M m:M×M→M ここで出てきた記号 M, 1, u, m の使い方は次のようなものです。…

…義されている式／項の変換を誘導します。同じ名前（ローカル名）をそのまま流用できないときは、系統的に名前の置き換え（リネーム）を行い、それを追跡可能にしておけば弊害を減らせます。このての話って、インスティチューションに帰着しそうですね。系統的な名前の置き換えは指標射であり、それに伴う式／項の変換は翻訳関手となります。名前付けや構文が変わっても、構文の翻訳と、対応するモデル（実装）側の変換があれば、全体として整合性は保てる、というのがインスティチューション理論の教えるところです。

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

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

…、関手データモデルがインスティチューションを定義することは既にスピヴァックが示しています。この事実を、観点と記述スタイルを若干変えて説明してみます。内容： 言葉と記号の約束 だいたいのところ（概要） 有向グラフに対する圏的演繹系とグラフ制約の圏 Pathモナドと有向グラフの圏の拡張 グロタンディーク構成による表示の圏の再現 インスティチューションの構成 関手モデルとインスティチューションの同値性 言葉と記号の約束Catは、小さい圏と関手からなる圏です。Graphは、有向グラフ…

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

…ります。圏Schは、インスティチューションにおける指標圏と同じものです。インスティチューションのモデル圏にあたるものが、インスタンスの圏 S-InstC := [S, C]（関手圏）です。このように、データベースの諸概念を直接（straightforward）に圏論でモデル化する手法が関手的データモデルです。枠組みはローヴェルやゴグエン（Goguen）のものと同じと言えますが、代数理論やインスティチューションが、データベース／データモデルの議論にこれほど直接的に適用可能である…

…様記述を付け加えるとインスティチューションが出来上がるのです。以上が、メイヤー指標の余代数意味論の大ざっぱなシナリオです。Creatorの意味論CommandとQueryだけから構成されるメイヤー指標に関しては、上記のような余代数意味論が構成できます。継承とかリスコフの置換原則なども、この枠内で説明できます。（僕が勘違いしてなければ）マイヒル／ネロードの定理も成立します。ところが、Creatorが入ると、上記のような余代数意味論からハミ出してしまうのです。先に挙げた例では3つ…

…うまく定義できれば、インスティチューションを定義できます。つまり、抽象構文記法は構文的インスティチューションの指標を記述する方法だったのです。構文構成子だけでなく、構文判定子や構文抽出子を定義し公理系を定めれば、より精密でリッチな代数構造ができて、その上に構文的操作の体系を組み立てることができます。様々な構文的操作を定義することは、代数構造の上でプログラミングする典型的な例を与えます。「代数構造（台集合と基本的な演算と法則性）の上でプログラミングする」という発想は、けっこう重…