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

…す。より具体的な話は次の機会とします。 *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つ…

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

自分で参照する都合で小さなリンク集を作った； 僕の興味はたぶん次のようなキーワードで示せるのでしょう。 メイヤー 「本文」「目次」 ホーア「本文」「目次」 型理論 「本文」「目次」 インスティチューション 「本文」「目次」 シーケント 「本文」「目次」 仕様記述 「本文」「目次」 次の2つの語は一般的過ぎるかも。ヒットが多すぎる。 論理 「本文」「目次」 ラムダ 「本文」「目次」

…れることがあります。インスティチューションでは、指標と指標射からなるベース圏の上にモデル圏が森の木のように“生えた”構造を考えます。メイヤー代数もメイヤー指標で定義可能です。集合圏で考えることにすれば、メイヤー指標は、1つの隠蔽ソート（hidden sort）を持つ隠蔽指標（hidden signature）です。次のものから構成されます。 Commandを表す記号の集合C Queryを表す記号の集合Q、各記号qには値のソートVqが割り当てられている CもQも無限集合でもかま…

…だいぶ違うでしょう。インスティチューション・ベースならCategories-as-Typesと考えるべきかもしれません。とりあえずここでは、Sets-as-Types（型とは集合なり）に限定することにします。「型とはなにか？」を固定してもまだ問題があります。型に関する議論には、プログラミング言語の概念、論理の概念、集合論の概念（Sets-as-Typesのとき）、そして型理論固有の概念が登場します。同じ、またはほとんど同じ概念にたくさんの用語が対応しています。同義語なのか、微…

…性の関数とは関係（relation）と言っても同じです。そして、関数や関係の背後にはSetやRelのような圏があります。圏Setや圏Relと、伴意順序のような順序を一緒に扱えないでしょうか？ そのひとつの候補が順序付き関係の圏ORelです。もちろん、インスティチューションやインデックス付き圏や構文生成モナドなどの他の方法もありますが、ホーアセオリーと順序付きの圏は割と相性が良さそうです。 *1:セオリーは、ホーア論理に特有のものではなくて、論理一般に関して定義できる概念です。

「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。 ホーア論理の圏論的な定式化 真偽構造が付いた圏 -- ホーア論理のために 「インデックス付き圏のフビニ／グロタンディーク同値」では、入れ子になったインデックス付き圏を持ち出しました。入れ子のインデックス付き圏の動機は「大量のモナド類似物（monad-like entities）を一挙に扱う方法」だと書きました。実は、「インスティチュ…

…様技術への道 -- インスティチューションを縮めてみる」とか、「古典論理は可換環論なんだよ」なんかがあります。これらも、マジメに書いてあるみたい。そういえば、「古典論理は可換環論なんだよ」には、「当方記事には過ぎた続編」をtri_iroさんに書いていただきました。「イデアルと論理 番外の補足：ベキ等元と連結性」と「“古典論理＝可換環論”の計算と種明かし」も関連記事です。以上に挙げた記事は、「論理は位相や代数とも関係するんだぜー」みたいなハナシ。そして、「論理も位相も代数も計算…

…な定式化」において、インスティチューションとホーア論理を一緒にしたようなナニカができないかなぁ、とか言ったので、もう少し考えてみることにします。ただし、最初のステップだけで、インスティチューションを使う段階には至ってません。僕がやりたいことは、「拡張されたホーア論理」の意味論を構成することですが、とりあえず意味論の舞台となる構造を作ることにします。真偽値という概念を圏論的に扱いやすい形にしたモノです。内容： 圏の上に真偽値を乗せる 真偽構造のあいだの準同型 具体的な真偽構造付…

…ーバーライドなしの）継承 MethodS→MethodT となっています。それから以上の定式化は、状態空間とメソッドのモデルとしては直接的・直感的なものだと思います。多くの現実の実装が採用している方式と同じで、メソッドはthisとかselfとかの暗黙の引数を持つことにより実現されます。大域関数はthisの値がvoidであるメソッドとみなされます。この定式化と、インスティチューション、ホーアトリプル、余代数などの関係を考えてみると面白いかも（あるいは面白くないかも）しれません。

インスティチューションは重要だと思っているのですが、このブログでまとまった記述をしたことはありません。じゃ、まとまったものを書くのか -- 書きません(苦笑)。まとまりのない断片的なことを書きます。インスティチューションはインデックス付き圏です。ベースの圏（インデックスの圏）は指標圏（category of signatures）と呼ばれ、標準的な記法では Sig と書きます。指標 Σ∈|Sig| ごとにモデル圏 Mod[Σ] が対応して、Σ |→ Mod[Σ] がインデック…

インスティチューションは、さまざまな型理論を統一的に扱うための便利な枠組みになります。与えられたインスティチューションをインデックス付き圏（indexed category）とみなして、グロタンディーク構成を行うことは有効なテクニックです。このテクニックの簡単な応用例を紹介します。この方法は、オブジェクト指向のクラス、抽象クラス、インターフェースなどを全部ひっくるめた型階層（type hierarchy）を作りたいときなどに使えます。Σを指標だとして、M[Σ]をモデル圏としま…

…インデックス付き圏 インスティチューション 仕様構造圏C上の仕様構造の定義は簡単です。 圏Cの対象Aごとに P(A) という集合が対応している。 圏Cの対象A, Bごとに P(A)×C(A, B)×P(B) の部分集合 H(A, B) が対応している。 P(A)は、A上のプロパティ（properties over A）の集合と呼びます。H(A, B) はホーアトリプルの集合と呼びましょう。P(-) と H(-, -) に関して次の条件を要求します。 (p, idA, p)∈H…

…ットに他ならない。 インスティチューション理論では、指標をΣと書く習慣がある。基本オペレーションの集合は指標と解釈できる。 実例を出しましょう。単純な整数変数をオブジェクトに仕立てたものをvとします。vは整数値を蓄えることができるのでストレージです。ただしvは、値がバインドされてない状態と、壊れてしまった状態を持つとします。vへの値の代入には、v.set(2) のようなsetメソッドを使い、値を未定義にするには v.unset() とします。vを壊す操作は v.destroy…

…い枠組みは？ そりゃインスティチューションでしょう。 圏論とオブジェクト指向 圏論とオブジェクト指向：資料編 自己改変コードについてはたまに考えてみるんですが、よくワカリマセン。状態空間が変化していく状況をモデル化したいなら、クリーネ圏を使えばよさそうなんですが …不純な計算や概念、多くの人が避けたり嫌ったりする計算や概念は魅力的。ただのへそ曲がりかもしんないけど、面白いんだからしょうがない。 *1:[追記]これは日本語が不正確。ほぼ書き間違っていますね。goto文を継続で解…

…category）、インスティチューション（institution）、ファイバー圏（fibred/fibered category）あたり。ステファネスク師のデカルト半環圏（Cartesian Semiringal Category）も、古典圏論の範囲では扱いがたいシロモノです。それで、何日か前からインデックス付き圏の話をはじめたのですが、毎度のことながら、定訳のない用語をどう表記するかで悩んでいます。古典圏を超える概念を扱うので、「超」とか「モドキ」の意味を持つ形容詞・副詞…

…のなかで、図式の例とインスティチューションの例は、具体例とは言いながら完全に圏を1つ固定した話ではなくて、圏の類を話題にしているので後回し。ベクトル空間の例に対してグロタンディーク構成（平坦化）を具体的に作ってみます。以下では、グロタンディーク構成で作った圏を「平坦化（した／された）圏」と呼ぶことにします。正確に言えば、インデックス付き圏（indexed category）のグロタンディーク構成からファイブレーションを忘れた圏（ファイバーバンドルで言えば全空間）が平坦化圏です…

…限倍とは限りません。インスティチューションインスティチューションがあるとして、Signを指標圏、Modをモデル関手とします。σ:Σ→Σ' を指標圏Sign内の射（指標射）だとします。インスティチューションの定義から、指標射σに対応するモデル圏のあいだの関手 σ*:Mod(Σ')→Mod(Σ) が誘導されます。この関手σ*はリダクト関手（reduct functor）と呼ばれるものです。つまり、インスティチューション構造のModは、指標圏Signをベース圏とするインデックス付き…

…とします。この記法はインスティチューションに倣いましたが、インスティチューションは出てきません。「|- A」という書き方のAを変数だと思うと、次の集合Provableが定義でます。 Provable = {A∈Sen(S) | |-S A} 左側がカラッポの「|-」の意味は、Sen(S)の部分集合だと言っていいでしょう。しかし、「A |- B」のような書き方もあります。これは、Aを仮定すればBが証明できる、という相対的証明可能性です。「A |- B」のA, Bを変数だと思うと…

…式化として、現状ではインスティチューションが一番包括的だと思います。ですが、インスティチューションの定義は「圏の圏」（あるいは圏のタバ）の形をしていて、インスティチューションのあいだの準同型を考えると「圏の圏の圏」を扱うことになります。それに、インスティチューションの準同型って概念はあんまりハッキリしてないし。僕の個人的な印象（錯覚や誤解かもしれません）では、インスティチューションは論理の双対性をうまくキャプチャできてない気がします。この感覚は、「当方記事には過ぎた続編、よみ…