संस्थान (कंप्यूटर विज्ञान)

इंस्टिट्यूशन की धारणा जोसेफ गोगुएन और रॉड बर्स्टल द्वारा 1970 के दशक के अंत में "कंप्यूटर विज्ञान में प्रयुक्त लॉजिकल सिस्टम के बीच जनसंख्या विस्फोट" से निपटने के लिए बनाई गई थी। यह धारणा लॉजिकल सिस्टम की "अनौपचारिक" अवधारणा को औपचारिक बनाने का प्रयास करती है।

इंस्टीट्यूशन का उपयोग विनिर्देशन लैंग्वेज (जैसे विशिष्टताओं की संरचना, मानकीकरण, कार्यान्वयन, शोधन और विकास), प्रमाण कैल्कुली, और यहां तक ​​​​कि अंतर्निहित लॉजिकल सिस्टम से पूरी तरह से स्वतंत्र उपकरणों की अवधारणाओं को विकसित करना संभव बनाता है। ऐसी आकृतियाँ भी हैं जो लॉजिकल सिस्टम को जोड़ने और अनुवाद करने की अनुमति देती हैं। इसके महत्वपूर्ण अनुप्रयोग हैं इसके महत्वपूर्ण अनुप्रयोग लॉजिकल संरचना (जिसे उधार भी कहा जाता है) और विषम विनिर्देश और लॉजिक का संयोजन का पुन: उपयोग है।

संस्थागत मॉडल सिद्धांत के प्रसार ने मॉडल सिद्धांत की विभिन्न धारणाओं और परिणामों को सामान्यीकृत किया है, और इंस्टीट्यूशन ने स्वयं यूनीवर्सल लॉजिक की प्रगति को प्रभावित किया है।

परिभाषा

इंस्टीट्यूशन का सिद्धांत लॉजिकल सिस्टम की प्रकृति के बारे में कुछ भी नहीं मानता है। अर्थात्, व्याख्या (लॉजिक) और वाक्य (गणितीय लॉजिक) अनैतिक वस्तुएं हो सकती हैं; एकमात्र धारणा यह है कि मॉडल और वाक्यों के मध्य संतुष्टि संबंध है, जो बताता है कि कोई वाक्य मॉडल में फिट बैठता है या नहीं। संतुष्टि टी-स्कीमा या टार्स्की की सत्य परिभाषा से प्रेरित है, किन्तु वास्तव में यह कोई भी बायनरी संबंध हो सकता है।

इंस्टीट्यूशन की महत्वपूर्ण विशेषता यह है कि मॉडल, वाक्य और उनकी संतुष्टि को सदैव कुछ शब्दावली या संदर्भ (जिसे सिग्नेचर (लॉजिक) कहा जाता है) में रहने वाला माना जाता है जो (गैर-लॉजिक) प्रतीकों को परिभाषित करता है जिनका उपयोग वाक्यों में किया जा सकता है और जिन्हें मॉडल में व्याख्या करने की आवश्यकता होती है। इसके अतिरिक्क्त, सिग्नेचर मोरफोलॉजि सिग्नेचर का विस्तार करने, नोटेशन परिवर्तित करने आदि की अनुमति देती है। सिग्नेचर और सिग्नेचर मोरफोलॉजि के बारे में कुछ भी नहीं माना गया है, अतिरिक्त इसके कि सिग्नेचर मोरफोलॉजि की रचना की जा सकती है; यह होने के सामान है

सिग्नेचर और मोरफोलॉजि की श्रेणी (गणित) अंत में, यह माना जाता है कि सिग्नेचर मोरफोलॉजि वाक्यों और मॉडलों के अनुवाद को इस तरह से आगे बढ़ाती है कि संतुष्टि संरक्षित रहती है। जबकि वाक्यों को सिग्नेचर मोरफोलॉजि के साथ अनुवादित किया जाता है (रूपवाद के साथ प्रतीकों को प्रतिस्थापित करने के बारे में सोचें), सिग्नेचर मोरफोलॉजि के विरुद्ध मॉडल का अनुवाद किया जाता है (या उत्तम: कम किया जाता है)। उदाहरण के लिए, सिग्नेचर एक्सटेंशन के स्थिति में, मॉडल के कुछ अवयवो को भूलकर (बड़े) लक्ष्य सिग्नेचर के मॉडल को (छोटे) स्रोत सिग्नेचर के मॉडल में कम किया जा सकता है।

मन लीजिए $\mathbf {Cat} ^{\mathrm {op} }$ लघु श्रेणियों की श्रेणी के विपरीत श्रेणी को निरूपित करें। इंस्टिट्यूशन औपचारिक रूप से सम्मिलित होती है

• सिग्नेचरों की श्रेणी $\mathbf {Sign}$,
• एक फ़ंक्टर ${\mathit {Sen}}\colon \mathbf {Sign} \to$ दे रहा है, प्रत्येक सिग्नेचर के लिए $\mathbf {Set}$, वाक्यों का सेट $\Sigma$, और प्रत्येक सिग्नेचर रूपवाद ${\mathit {Sen}}(\Sigma )$ के लिए, वाक्य अनुवाद मानचित्र $\sigma \colon \Sigma \to \Sigma '$, जहां अधिकांशतः ${\mathit {Sen}}(\sigma )\colon {\mathit {Sen}}(\Sigma )\to {\mathit {Sen}}(\Sigma ')$ को ${\mathit {Sen}}(\sigma )(\varphi )$ के रूप में लिखा जाता है
• एक फ़ंक्टर $\mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }$ दे रहा है, प्रत्येक सिग्नेचर के लिए $\mathbf {Mod} (\Sigma )$ मॉडल की श्रेणी $\sigma \colon \Sigma \to \Sigma '$, और प्रत्येक सिग्नेचर रूपवाद $\mathbf {Mod} (\sigma )\colon \mathbf {Mod} (\Sigma ')\to \mathbf {Mod} (\Sigma )$ के लिए, रिडक्ट फ़ंक्टर $\mathbf {Mod} (\sigma )(M')$, जहां अधिकांशतः $M'|_{\sigma }$ के रूप में लिखा जाता है
• प्रत्येक ${\models _{\Sigma }}\subseteq |{\mathbf {Mod} (\Sigma )|\times {\mathit {Sen}}(\Sigma )}$ के लिए संतुष्टि संबंध $\Sigma \in \mathbf {Sign}$

इस प्रकार कि $\sigma \colon \Sigma \to \Sigma '$ में प्रत्येक $\mathbf {Sign}$ के लिए, निम्नलिखित संतुष्टि नियम प्रयुक्त होता है:

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

प्रत्येक $M'\in \mathbf {Mod} (\Sigma ')$ और $\varphi \in {\mathit {Sen}}(\Sigma )$ के लिए

संतुष्टि की स्थिति यह व्यक्त करती है कि संकेतन के परिवर्तन के अनुसार सत्य अपरिवर्तनीय है (और संदर्भ के विस्तार या उद्धरण के अनुसार भी)।

सख्ती से कहें तो मॉडल फ़ैक्टर सभी बड़ी श्रेणियों की "श्रेणी" में समाप्त होता है।

इंस्टीट्यूशन के उदाहरण

• सामान्य लॉजिक
• सामान्य बीजीय विशिष्टता लैंग्वेज (सीएएसएल)
• प्रथम-क्रम लॉजिक
• उच्च-क्रम लॉजिक
• अंतर्ज्ञानवादी लॉजिक
• मॉडल लॉजिक
• प्रोपोज़िशनल लॉजिक
• अस्थायी लॉजिक
• वेब ओण्टोलॉजी लैंग्वेज (ओडब्ल्यूएल)

यह भी देखें

• एब्स्ट्रेक्ट मॉडल सिद्धांत
• संस्थागत मॉडल सिद्धांत
• यूनीवर्सल लॉजिक

अग्रिम पठन

• J. A. Goguen; R. M. Burstall (1984), "Introducing institutions", in E. Clarke; D. Kozen (eds.), Logics of Programs: Proceedings of the Logics of Programming Workshop 1983, Lecture Notes in Computer Science, vol. 164, Springer, Berlin, Germany, pp. 221–256, doi:10.1007/3-540-12896-4_366, ISBN 978-3-540-12896-0. This was the first publication on institution theory and the preliminary version of Goguen and Burstall (1992).
• J. Meseguer (1989), "General logics", in H.-D. Ebbinghaus; J. Fernandez-Prida; M. Garrido; D. Lascar; M. Rodriquez Artalejo (eds.), Logic Colloquium '87: Proceedings of the Colloquium held in Granada, Spain, vol. 129, Elservier, pp. 274–307
• J. A. Goguen; G. Rosu (2002), "Institution morphisms", Formal Aspects of Computing, 13 (3–5): 274–307, doi:10.1007/s001650200013, S2CID 5687318
• D. Sannella; A. Tarlecki (1988), "Specifications in an arbitrary institution", Information and Computation, 76 (2–3): 165–210, doi:10.1016/0890-5401(88)90008-9
• R. Diaconescu (2008), Institution-independent Model Theory, Birkhäuser, Basel

बाहरी संबंध

• Răzvan Diaconescu, "Institution Theory", Internet Encyclopedia of Philosophy, retrieved January 31, 2021
• Joseph Goguen (2006), Institutions, University of California, San Diego, retrieved January 31, 2021
• Formalism, Logic, Institution - Relating, Translating and Structuring. Includes large bibliography.
• Răzvan Diaconescu, Selected Publications, Simion Stoilow Institute of Mathematics of the Romanian Academy, retrieved January 31, 2021. Contains recent work on institutional model theory.