Institution Begriffserklärung

Copyright © Shutterstock/Gorodenkoff

Was ist eine Institution?

Der Begriff Institution wurde Ende der 1970er Jahre von den Herren Joseph Goguen und Rod Burstall entwickelt. Diese Bezeichnung versucht, das Wesentliche eines logischen Systems einzufangen.

Die Verwendung einer Institution ermöglicht die Entwicklung von Konzepten für Spezifikationssprachen (zum Beispiel Strukturierung von Spezifikationen, Parametrisierung, Implementierung, Verfeinerung, Entwicklung), Korrekturkalküle und sogar Tools, die völlig unabhängig vom zugrunde liegenden logischen System liegen. Es gibt auch Morphismen, die es ermöglichen, logische Systeme zu verknüpfen und zu übersetzen. Wichtige Anwendungen hierfür sind die Weiterverwendung der logischen Struktur, heterogene Spezifikation und Kombination von Logiken.

Die Verbreitung der Institution-Modelltheorie hat verschiedene Begriffe und Ergebnisse der Modelltheorie verallgemeinert und die Institution selbst hat den Fortschritt der universellen Logik beeinflusst.

Definition einer Institution

Die Theorie der Institution nimmt nichts über die Natur des logischen Systems an. Das heißt, Modelle und Sätze können beliebige Objekte sein. Die einzige Annahme ist, dass es eine Zufriedenheitsbeziehung zwischen Modellen und Sätzen gibt, die aussagt, ob ein Satz in einem Modell enthalten ist oder nicht. Zufriedenheit ist von Tarskis Wahrheitsdefinition inspiriert, kann aber tatsächlich jede binäre Beziehung sein. Ein entscheidendes Merkmal einer Institution besteht nun darin, dass Modelle, Sätze und deren Zufriedenheit immer als in einem bestimmten Vokabular oder Kontext (als Signatur genannt) bezeichnet werden, da sie (nicht logische) Symbole definieren, die in Sätzen verwendet werden können und die interpretiert werden müssen in Modellen.

Darüber hinaus erlauben Signaturmorphismen das Erweitern von Signaturen, Ändern der Notation und so weiter. Über Signaturen und Signaturmorphismen wird nichts angenommen, außer dass sie zusammengesetzt werden. Dies entspricht einer Kategorie von Signaturen und Morphismen. Schließlich wird angenommen, dass die Signaturmorphismen dazu führen, dass Sätze und Modelle so übersetzt werden, dass die Zufriedenheit erhalten bleibt. Während die Sätze zusammen mit Signaturmorphismen übersetzt werden, werden Modelle gegen Signaturmorphismen übersetzt (oder besser: reduziert).

Die Signatur kann auf ein Modell der (kleineren) Quellensignatur reduziert werden, indem nur einige Komponenten des Modells vergessen werden.

Beispiele

FAQ