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

कंप्यूटर विज्ञान में उपयोग की जाने वाली लॉजिकल सिस्टम के बीच जनसंख्या विस्फोट से सामना करने के लिए, संस्था की धारणा 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 )$ के रूप में लिखा गया है $\sigma (\varphi )$,
• एक पदाधिकारी $\mathbf {Mod} \colon \mathbf {Sign} \to \mathbf {Cat} ^{\mathrm {op} }$ प्रत्येक हस्ताक्षर के लिए देना $\Sigma$, मॉडलों की श्रेणी $\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 )$.

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

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

संस्थानों के उदाहरण

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

यह भी देखें

• सार मॉडल सिद्धांत
• संस्थागत मॉडल सिद्धांत
• सार्वभौमिक तर्क

अग्रिम पठन

• 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.