パラメータ付き指標／セオリー（仕様モジュール）とCafeOBJのprotected importって同じような気がする。インポートって余スパンで説明されるような。

ゴグエン／マルコルム／ケンプ（Joseph Goguen, Grant Malcolm, Tom Kemp）の"A Hidden Herbrand Theorem"(1998)とビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）の"On Observability and Reachability "を読み比べてみた。 Observational Logi…

普通、指標はグラフとみなせる。グラフや圏の用語と記法を拝借しよう。指標Σに対して、ソートsからソートtへの演算記号の全体をΣ(s, t)と書く。Σ(s, t)は集合。ただし、(s, t)≠(s', t')でもΣ(s, t)∩Σ(s', t') = 空 は仮定しない（オーバーロード許可）。Σ(s,…

プログラミング言語をひとつ与えることは、結局は指標を与えることと同じで、問題は指標から自由圏を作る一種の閉包演算<->のほうだな。どのような種類の自由圏（エルブラン圏、項集合）を与えるかがプログラミング言語構文の特徴付けになる。閉包演算<->は…

指標圏に境界概念とグルーイングを導入して、コボルディズム的な二重圏だと考える。インスティチューションをこの二重圏の上で定義する。すると、Mod、Sen、Spec、Theo（Sen上に作る順序集合）なども拡張されるだろう。さらに、証明系ProofやプログラムProg…

待てよ、前のエントリーと同じこと、スペクトルとモデルの関係について以前書いたのだった。 「コンパクト空間と論理／モデル論」 「仕様技術への道 -- インスティチューションを縮めてみる」 ある形式系が採用している論理が古典論理なら、そのリンデンバウ…

指標を単なる有向グラフと考えるのはとてもいいとわかってきた。等式的セオリーまず、等式的セオリーとグラフのあいだには次の関係がある。 指標 圏の生成グラフ ソート 対象の生成集合 関数記号 射の生成集合 項形成規則 自由構成 項 射 等式系 グラフの（…

関手圏によるモデル圏構成、代入系の圏 - 檜山正幸のキマイラ飼育記 メモ編 指標と関手モデル - 檜山正幸のキマイラ飼育記 メモ編 ソートと演算記号の分類 - 檜山正幸のキマイラ飼育記 メモ編 System(Γ, Σ)の具体例：翻訳系 - 檜山正幸のキマイラ飼育記 メモ…

忘却関手、具象圏、構成関手 - 檜山正幸のキマイラ飼育記 メモ編、一般忘却関手 - 檜山正幸のキマイラ飼育記 メモ編 の続き。普遍的な忘却先(?)としてSetを考える（これも相対化できるが、キリがないから止める）。圏BとCは、標準的（canonical）な忘却関手U…

あっと忘れた、忘却関手概念をもう少し広くしておかないとダメだ。JSLat（ジョイン半束）とAbMon（アーベルモノイド）のように、セオリーが事実上同じってことがあるので、セオリー間の射（翻訳）を定義しないとダメだわ。インスティチューションを使わない…

昨日： 表層的な現象が見えているけど、背後にある仕掛けがわかんない状態はイライラするね。もうヤメタ、、、、って止めないけど。 あいかわらずイライラ。が、わかることだけ記録しておくしかない、クッソー。とりあえず、Σを普通の多ソート指標とする。つ…

インスティチューションのSen(Σ)上にムーア閉包作用素が存在している状況を考える。参考： 抽象証明系 - 檜山正幸のキマイラ飼育記 メモ編 Moore閉包から抽象証明系 - 檜山正幸のキマイラ飼育記 メモ編 証明系付きインスティチューション - 檜山正幸のキマイ…

Lawvere流セオリー - 檜山正幸のキマイラ飼育記 メモ編の話を少し整理する。ソート付きの指標Σは、ソートを頂点、演算記号を辺とするグラフ（またはハイパーグラフ）とみなせる。FreeCat(Σ)を、Σから作られた圏とする。グラフの圏と圏の圏において、Graph(Σ,…

現象をモデル化した構造は複雑なんじゃなかろうか。ここで、“複雑”とは、規模が大きくて階層的で有機的に絡み合っているということ。so-called“複雑系”の「複雑」とは違う。例えば、代数系を公理化したとき、等式が50も100も出てくると、とても単純な系とは…

Bidoit、Hennicker、Kurz等が、指標に現れるソートや演算（operation）の記号を分類している。彼らは、天下りにコンストラクター記号Consとオブザーバー（観測子）記号Obsを与える。Cons∩Obs = 空 だと思うが、明示的な記述はなんか見あたらない。とりあえず…

以前、Pow(Sen(-))という関手をindexed categoryだとみなして、それを平坦化してSpecを定義した。SystemはSpec上で定義した方が自然だろうから、Γ、Σは指標じゃなくて仕様だとしてSystem(Γ, Σ)は「Γを満たす実装を渡されてΣを満たすような実装」となる。Prog…

とにかくメモ、しゃべるようにメモじゃ。インスティチューションのMod関手を一般化したい。指標Σ、Γと指標射φがあるとき、Mod(φ): Mod(Γ)→Mod(Σ) となるが通常のMod関手だが、Modを2引数Mod(Γ, Σ)にしたいのだが、混乱をさけるため2引数のバージョンはSystem…

疲れた、ヘロヘロだ。朦朧状態。インスティチューションIの上のプログラムの圏Progは、|Prog| = |Sign|であり、自然な埋め込み Sign ⊆ Progがある。つまり、SignがProgの広大部分圏で入っている。[追記]自然な埋め込みがあるのではなくて、埋め込みの族があ…

インスティチューションの元祖Goguen先生の奥様（Ryokoさん）にコメントいただいちゃったよー。→http://d.hatena.ne.jp/m-hiyama/20060119#c1143599637 Joseph Goguenの妻のRyoko Goguenです。この度は、主人の研究について、記載していただき誠に有難うござ…

ついで(?)だから、命題論理も書いてしまえ。Bを有限集合と単射の圏だとする、これが指標圏。X∈|B|のとき、Xは命題変数の集合だとみなす。Ω={true, false}を2値のブール代数として、多項式インスティチューションと同じようにして簡易インスティチューション…

多項式インスティチューションは簡易インスティチューションの簡単な例だと思う。似たような例に命題論理のインスティチューションがある。が、もっと簡単な例がある。Pow*、Pow*をそれぞれ、共変と反変のベキ関手だとする。Pow*(f)をf*、Pow*(f)をf*と略記…

思わぬところでインスティチューションに出会うことがある。多項式インスティチューションは典型的なインスティチューションではないが、「こんなところにも」という例にはなる。それに説明が簡単だし。以下で、インスティチューションの単純化である簡易イ…

[追記 date="2006-03-04"]文言、わずかに手直しをした。[/追記]本編のコレとかでは、簡単なインスティチューションの例を提供しようとしている。インスティチューションの定義くらいは仮定して、本編の例が実際にインスティチューションの例になっていること…

インスティチューションがあって、Σ∈|Sign|ごとに、証明可能性“|-”が付いているとする。A⊆Sen(Σ)、b∈Sen(Σ)に対して、A|-b は、Aを仮定してbが証明できること。|-を拡張して、A|-Bが定義できる。「A|-B ならば A|⇒B」が健全性。ここで、A|⇒B は、BがAの帰結…

インスティチューションにプログラム（のソースコード）とプログラム証明を入れる準備。Pインスティチューションとは、(Sign, Mod, Sen, Prog, PMod, |=)であり、ProgとPModを除くとインスティチューション、Sign⊆Progであり、iが包含として、i;PMod = Mod。…

http://d.hatena.ne.jp/m-hiyama/20060119/1137641539の「モゴモゴな話」に書いた件でメモ：少し分かってきた（かな？）。まず、関連するエントリーは： http://d.hatena.ne.jp/m-hiyama/20050716/1121499351 http://d.hatena.ne.jp/m-hiyama/20050719/11217…

そういえば、インスティチューションの具体例って書いたことない。お決まりの、フラグ、カウンタ、スタック。代数だと、半群、モノイド、線形空間（または加群）。多項式全体もうまいことインスティチューションになる。あと、なんか面白い例はないかいな。…

証明系を抽象化する目的は、証明系をインスティチューションに組み込みたいから。Moore閉包を使う定式化もいいのだけど、集合に対する関係|-を基本とすることにする。A|-Bのインフォーマルな意味は、「Aの論理式を全部仮定すれば、Bのどの論理式でも証明でき…