本編「レコードの型階層を合理的に説明できるか」の設定でインスティチューションを作ってみる。用語や記号は本編記事に従う。指標圏フィールド名として許されるすべての名前の集合をName（無限集合と仮定）とする。Nameの有限部分集合を指標と呼ぶ。例えば…

余完備性をKleisli圏に持ち上げたい open programs open programs 再び 2005年の夏、えー、こんな昔からTermモナドがプログラムだって知っていたの、僕？ Cospan構成にも言及しているし。以上をふまえて書いた記事： ソースコードの形式化 これ↑で、「コンポ…

protecting 演算（記号）も法則（等式）も追加できない。 extending 演算は追加できるが法則は追加できない。 using 自由

プレ圏（グラフ上に部分的な圏構造）の圏をPrecatとする。さらに、プレ圏に同値関係（一般化合同）が与えられたものを(P, E)として、その全体をEPrecatとする。EPrecatは有限余完備だと期待している。EPrecatが有限余完備ならその上の余スパンの圏が作れる。…

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

どう違う？ 同じような気もするが。

だって。 Title: Observational Truth as a Categorical Modality (2002) Author: Grant Malcolm URL: http://citeseer.ist.psu.edu/573401.html 11ページ

ゴグエン／マルコルム／ケンプ（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,…

エルブラン定理関係で、結局一番短い、 Title: A Hidden Herbrand Theorem (1998) Authors: Joseph Goguen, Grant Malcolm, Tom Kemp URL: http://citeseer.ist.psu.edu/293075.html 18ページ これにした。まず、隠蔽ソートって用語はよくないと思った。これ…

フー、ここ2,3日四苦八苦していた問題にやっと目星がついた。プログラム言語をはじめとする形式言語の一般的定式化。とりあえず目標は： インスティチューション・フレンドリ 十分な一般性 形式言語系とは、組(Sign, Mod, T, ξ)であって： SignとModはインス…