機関（コンピュータサイエンス）

制度の概念は、1970年代後半にジョセフ・ゴーゲンとロッド・バーストールによって、「コンピュータサイエンスで使用される論理システムの人口爆発」に対処するために作成されました。この概念は、論理システムの「非公式な」概念を「形式化」しようとします。^[1]

制度を利用することで、仕様言語の概念（仕様の構造化、パラメータ化、実装、改良、開発など）、証明計算、さらにはツールを、基礎となる論理システムから完全に独立した方法で開発することが可能になります。論理システムを関連付けたり変換したりできるモルフィズムもあります。この重要な用途は、論理構造の再利用（借用とも呼ばれる）、異種仕様、および論理の組み合わせです。

制度モデル理論の普及により、モデル理論の様々な概念や結果が一般化され、制度自体が普遍論理の進歩に影響を与えてきた。^{[2] [3]}

制度理論は、論理システムの性質について何も仮定しません。つまり、モデルと文は任意のオブジェクトである可能性があります。唯一の仮定は、モデルと文の間に満足関係があり、文がモデルで成り立つかどうかを示すことです。満足はタルスキの真理定義に触発されていますが、実際には任意の二項関係である可能性があります。制度の重要な特徴は、モデル、文、およびそれらの満足が、文で使用される可能性があり、モデルで解釈される必要がある (非論理) 記号を定義する何らかの語彙またはコンテキスト (シグネチャと呼ばれる) に存在すると常に見なされることです 。さらに、シグネチャ射により、シグネチャを拡張したり、表記を変更したりすることができます。シグネチャ射が構成できることを除いて、シグネチャとシグネチャ射については何も仮定されていません。これは、シグネチャと射のカテゴリを持つことに相当します。最後に、シグネチャ射は、満足度が保持される方法で文とモデルの翻訳につながると想定されます。文章は署名モルフィズムに沿って翻訳されますが (モルフィズムに沿ってシンボルが置き換えられると考えてください)、モデルは署名モルフィズムに対して翻訳されます (または、より正確には、縮小されます) 。たとえば、署名拡張の場合、(より大きな) ターゲット署名のモデルは、モデルのいくつかのコンポーネントを忘れるだけで、(より小さな) ソース署名のモデルに縮小される場合があります。

を小カテゴリのカテゴリの反対を表すものとする。制度は形式的には ${\displaystyle \mathbf {猫} ^{\mathrm {op} }}$

• 署名のカテゴリ、​ ${\displaystyle \mathbf {符号} }$
• 各署名 に対して文の集合を与え、各 署名射に対して文の翻訳写像 を与える関手。ここで、 は次のように書かれることが多い。${\displaystyle {\mathit {Sen}}\colon \mathbf {Sign} \to }$ ${\displaystyle \mathbf {集合} }$${\displaystyle \Sigma }$ ${\displaystyle {\mathit {セン}}(\Sigma )}$${\displaystyle \sigma \colon \Sigma \to \Sigma '}$ ${\displaystyle {\mathit {Sen}}(\sigma )\colon {\mathit {Sen}}(\Sigma )\to {\mathit {Sen}}(\Sigma ')}$${\displaystyle {\mathit {Sen}}(\sigma )(\varphi )}$${\displaystyle \sigma (\varphi )}$
• 各シグネチャ に対してモデルのカテゴリを与える関数、および各シグネチャ射に対して縮約関数を与える関数。 ここで、 は次のように記述されることが多い。${\displaystyle \mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }}$${\displaystyle \Sigma }$ ${\displaystyle \mathbf {Mod} (\Sigma )}$${\displaystyle \sigma \colon \Sigma \to \Sigma '}$ ${\displaystyle \mathbf {Mod} (\sigma )\colon \mathbf {Mod} (\Sigma ')\to \mathbf {Mod} (\Sigma )}$${\displaystyle \mathbf {Mod} (\sigma )(M')}$${\displaystyle M'|_{\sigma }}$
• それぞれに対する満足度関係 、${\displaystyle {\models _{\Sigma }}\subseteq |{\mathbf {Mod} (\Sigma )|\times {\mathit {Sen}}(\Sigma )}}$${\displaystyle \Sigma \in \mathbf {Sign} }$

の各 に対して、次の満足条件 が成立します。 ${\displaystyle \sigma \colon \Sigma \to \Sigma '}$${\displaystyle \mathbf {Sign} }$

$${\displaystyle M'\models _{\Sigma '}\sigma (\varphi )\quad {\text{if and only if}}\quad M'|_{\sigma }\models _{\Sigma }\varphi }$$

それぞれおよび。 ${\displaystyle M'\in \mathbf {Mod} (\Sigma ')}$${\displaystyle \varphi \in {\mathit {Sen}}(\Sigma )}$

満足条件は、表記の変更（およびコンテキストの拡大や除算）によっても真実が不変であることを表します。

厳密に言えば、モデル関数はすべての大きなカテゴリの「カテゴリ」で終わります。

• 共通の論理
• 共通代数仕様言語(CASL)
• 一階論理
• 高階論理
• 直観主義論理
• 様相論理
• 命題論理
• 時間的論理
• ウェブオントロジー言語(OWL)

• 抽象モデル理論
• 制度モデル理論
• 普遍的な論理

• JA Goguen、RM Burstall (1984)、「Introducing institutions」、E. Clarke、D. Kozen (編)、『Logics of Programs: Proceedings of the Logics of Programming Workshop 1983』、Lecture Notes in Computer Science、vol. 164、Springer、ベルリン、ドイツ、pp. 221–256、doi :10.1007/3-540-12896-4_366、ISBN 978-3-540-12896-0これは制度理論に関する最初の出版物であり、GoguenとBurstall（1992）の予備版でした。
• J. Meseguer (1989)、「一般論理」、H.-D. Ebbinghaus、J. Fernandez-Prida、M. Garrido、D. Lascar、M. Rodriquez Artalejo (編)、『Logic Colloquium '87: Proceedings of the Colloquium held in Granada, Spain』、第 129 巻、Elservier、pp. 274–307
• JAゴグエン; G. Rosu (2002)、「Institution morphisms」、Formal Aspects of Computing、13 (3–5): 274–307、doi : 10.1007/s001650200013、S2CID  5687318
• D. サンネラ、A. タルレッキ (1988)、「任意の制度における仕様」、情報と計算、76 (2–3): 165–210、doi : 10.1016/0890-5401(88)90008-9
• R. Diaconescu (2008)、制度に依存しないモデル理論、ビルクハウザー、バーゼル

• ラズヴァン・ディアコネスク、「制度理論」、インターネット哲学百科事典、2021年1月31日閲覧
• Joseph Goguen (2006)、Institutions、カリフォルニア大学サンディエゴ校、 2021 年1 月 31 日取得
• 形式主義、論理、制度 - 関連付け、翻訳、構造化。膨大な参考文献が含まれています。
• Răzvan Diaconescu、Selected Publications、ルーマニア科学アカデミー数学研究所シミオン・ストイロウ研究所、 2021年1月31日閲覧制度モデル理論に関する最近の研究が含まれています。