…へ 伴意から含意へ インスティチューション論理／モデル論をベースとした仕様技術といえば、現状利用できる最も便利な枠組みはインスティチューション（Institution）だろう。以下に、キマイラ・サイトの記事からインスティチューションに関する注釈を引用する： インスティチューションは、（僕は読んでないけど）Joseph Goguen & Rod Burstall "Institutions: Abstract model theory for specification and…

…だ。[蛇足] もし、インスティチューション（institution）を知っているなら、指標（signature）Σを1つ固定してモデル圏Mod=ModΣと文集合Sen=SenΣを考えれば、M、N∈Obj(Mod)に対して同値関係≡を定義できることを確認できるだろう。つまり、空間X=XΣはインスティチューションに対して定義できる。Σ |→ XΣ は関手に拡張できて、これは指標圏から位相空間の圏への関手になる。（細部をチェックしてないから、まちがっていたらゴメンね。）論理式が定義…

…は意訳しているが）をインスティチューション（institutions）で扱いたいのだ。Aを入力、Bを出力、Xを状態空間とするtransducerはf:A×X→B×X in Set で記述できる。transducerの圏は、SetからのCirc構成で、feedback付き圏になる。このままではtracedにならないが、タイミング（フィードバックの遅れ）をうまく処理すれば、たぶんtracedになる。さらにInt構成すれば、コンパクト閉圏になるはず。transducerの圏は、二圏…

…en program σ:Σ→Σ'からinduceされるreduct functor Mod(Σ')→Mod(Σ) も自然なものに思える。もとの指標圏Signから作ったKleisli圏の射の向きを逆向き（opposite）にするかどうかで、またまた悩む！ あーーー、向きや符号はいつもいつも悩みの種だぁ。が、作ったKleisli圏が有限余完備なら、そこでさらにCospan構成をすれば、かなり使いやすいインスティチューションが得られそうだ。って、ホントに作れるかどうかわからんが。

…しい!。具体的には、インスティチューション(Sign, Sen, Mod, |=)の指標圏Signが有限余完備な状況を考える。Maude（http://maude.cs.uiuc.edu/）やCASL（http://www.cofi.info/CASL.html）でも、この状況は仮定している。この状況で、Signがプアなとき、Sign上のモナドLを使ってSignを拡張したいことがあるのだ。そもそもインスティチューション自体をKleisli圏まで持ち上げなくてはならないのだが、…

… 次の2箇所でchimairaサイトに好意的な言及をしていただいております。 http://mag.autumn.org/Content.modf?id=20050127163831 : 「正気の試み」は「狂気の沙汰」の婉曲表現ですね。 http://aquamarine.c.oka-pu.ac.jp/weblog/archives/2005/01/post_2.html : ソフトウェア工学の本で、圏やインスティチューションに触れているのは、松本先生のアノ本以外知りません。