सहसंयोजन

This article is about कंप्यूटर विज्ञान. For एब्स्ट्रेक्ट बीजगणित में शब्द, see वलय का परिवर्तन. For चिकित्सा और एनेस्थेसिया में इस शब्द का उपयोग, see coinduction (anaesthetics).

कंप्यूटर विज्ञान में, सहसंयोजन समवर्ती इंटरैक्टिंग ऑब्जेक्ट (कंप्यूटिंग) के सिस्टम के गुणों को परिभाषित करने और सिद्ध करने की तकनीक है।

सहसंयोजन संरचनात्मक प्रेरण का गणितीय द्वैत (श्रेणी सिद्धांत) है। संयोगात्मक रूप से परिभाषित प्रकारों को कोडाटा के रूप में जाना जाता है और सामान्यतः अनंतता डेटा संरचनाएं होती हैं, जैसे स्ट्रीम (कंप्यूटिंग) होती हैं।।

एक परिभाषा या विनिर्देश (कंप्यूटिंग) के रूप में, सहसंयोजन वर्णन करता है कि किसी वस्तु को कैसे देखा जा सकता है, तोड़ा जा सकता है या सरल वस्तुओं में नष्ट किया जा सकता है। प्रमाण (गणित) तकनीक के रूप में, इसका उपयोग यह दिखाने के लिए किया जा सकता है कि समीकरण ऐसे विनिर्देश के सभी संभावित कार्यान्वयन (कंप्यूटिंग) से संतुष्ट है।

कोडाटा उत्पन्न करने और उसमें परिवर्तन करने के लिए, सामान्यतः लेजी मूल्यांकन के साथ, कोरकर्शन फ़ंक्शंस का उपयोग किया जाता है। अनौपचारिक रूप से, प्रत्येक प्रेरणिक कंस्ट्रक्टर पर पैटर्न-मिलान द्वारा फ़ंक्शन को परिभाषित करने के अतिरिक्त, प्रत्येक डिस्ट्रक्टर या सुपरवाइज़र को फ़ंक्शन परिणाम पर परिभाषित किया जाता है।

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

विवरण

प्रेरण के सिद्धांत और सह-आगमन के सिद्धांत दोनों का संक्षिप्त विवरण दिया गया है। चूँकि यह लेख मुख्य रूप से प्रेरण से संबंधित नहीं है, फिर भी उनके कुछ सीमा तक सामान्यीकृत रूपों पर एक साथ विचार करना उपयोगी है। इस प्रकार सिद्धांतों को बताने के लिए कुछ प्रारंभिक बातों की आवश्यकता होती है।

प्रारंभिक

मान लीजिए कि $U$ एक समुच्चय है और $F$ एक मोनोटोन फलन $2^{U}\rightarrow 2^{U}$ है, अर्थात:

$X\subseteq Y\Rightarrow F(X)\subseteq F(Y)$

जब तक अन्यथा न कहा जाए, $F$ को एकसमान माना जाएगा।

X, F-संवृत है यदि $F(X)\subseteq X$

यदि X, F-संगत है $X\subseteq F(X)$

$X=F(X)$

इन शब्दों को निम्नलिखित विधि से सामान्यतः समझा जा सकता है। मान लीजिए कि $X$ अभिकथनों का एक सेट है, और $F(X)$ वह ऑपरेशन है जो $X$ के निहितार्थ लेता है। तब $X$ 𝐹-संवृत है जब आप पहले से बताए गए निष्कर्ष से अधिक निष्कर्ष नहीं निकाल सकते हैं, जबकि $X$ 𝐹-संगत है जब आपके सभी प्रमाण अन्य प्रमाणों द्वारा समर्थित हैं (अर्थात कोई "गैर-𝐹-तार्किक धारणाएं नहीं हैं")।

नैस्टर-टार्स्की प्रमेय हमें बताता है कि $F$ का सबसे कम निश्चित-बिंदु (जिसे $\mu F$ दर्शाया गया है) सभी $F$-संवृत सेटों के प्रतिच्छेदन द्वारा दिया जाता है, जबकि सबसे बड़ा निश्चित-बिंदु (जिसे $\nu F$ दर्शाया गया है) सभी F- के मिलन द्वारा दिया जाता है। सुसंगत सेट अब हम प्रेरण और सह-आगमन के सिद्धांतों को बता सकते हैं।

परिभाषा

प्रेरण का सिद्धांत यदि $X$ F-संवृत है तो $\mu F\subseteq X$

सह-आगमन का सिद्धांत यदि $X$, F-संगत है तो $X\subseteq \nu F$

चर्चा

जैसा कि कहा गया है, सिद्धांत कुछ सीमा तक अपारदर्शी हैं, किन्तु निम्नलिखित विधि से उपयोगी विधि से सोचा जा सकता है। मान लीजिए आप $\mu F$ की प्रोपर्टी सिद्ध करना चाहते हैं। प्रेरण के सिद्धांत के अनुसार, यह एक 𝐹-संवृत सेट $x$ प्रदर्शित करने के लिए पर्याप्त है जिसके लिए प्रोपर्टी धारण करती है। जैसे, मान लीजिए आप यह दिखाना चाहते हैं कि $x\in \nu F$ फिर यह एक 𝐹-संगत सेट प्रदर्शित करने के लिए पर्याप्त है जिसका $x$ को सदस्य माना जाता है।

उदाहरण

डेटा प्रकार के सेट को परिभाषित करना

डेटाटाइप के निम्नलिखित व्याकरण पर विचार करें:

$T=\bot \;|\;\top \;|\;T\times T$

अर्थात्, प्रकारों के सेट में "निचला प्रकार" $\bot$, "शीर्ष प्रकार" $\top$, और (गैर-समरूप) सूचियाँ सम्मिलित हैं। इन प्रकारों को $\Sigma =\{\bot ,\top ,\times \}$ अक्षर के ऊपर तारों से पहचाना जा सकता है। मान लीजिए $\Sigma ^{*}$ पर सभी स्ट्रिंग्स $\Sigma$ को दर्शाता है। $F:2^{\Sigma ^{*}}\rightarrow 2^{\Sigma ^{*}}$ फ़ंक्शन पर विचार करें

$F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}$

इस संदर्भ में, $x\times y$ का अर्थ है "स्ट्रिंग $x$, प्रतीक $\times$ और स्ट्रिंग $y$ का संयोजन" अब हमें अपने डेटाटाइप्स के सेट को $F$ के फिक्सपॉइंट के रूप में परिभाषित करना चाहिए, किन्तु यह मायने रखता है कि हम सबसे कम या सबसे बड़ा फिक्सपॉइंट लेते हैं या नहीं है।

मान लीजिए कि हम डेटाटाइप्स के अपने सेट के रूप में $\mu F$ लेते हैं। प्रेरण के सिद्धांत का उपयोग करके, हम निम्नलिखित प्रमाण को सिद्ध कर सकते हैं:

$\mu F$ में सभी डेटाटाइप सीमित हैं

इस निष्कर्ष पर पहुंचने के लिए $\Sigma$ पर सभी परिमित स्ट्रिंग्स के सेट पर विचार करें। स्पष्ट रूप से $F$ एक अनंत स्ट्रिंग उत्पन्न नहीं कर सकता है, इसलिए यह पता चलता है कि यह सेट F-संवृत है और निष्कर्ष इस प्रकार है।

अब मान लीजिए कि हम डेटाटाइप्स के अपने सेट के रूप में $\nu F$ लेते हैं। हम निम्नलिखित प्रमाण को सिद्ध करने के लिए सह-आगमन के सिद्धांत का उपयोग करना चाहेंगे:

प्ररूप $\bot \times \bot \times \cdots \in \nu F$

यहाँ $\bot \times \bot \times \cdots$ सभी $\bot$ से युक्त अनंत सूची को दर्शाता है। सहसंयोजन के सिद्धांत का उपयोग करने के लिए, सेट पर विचार करें:

$\{\bot \times \bot \times \cdots \}$

यह सेट 𝐹-संगत हो जाता है, और इसलिए $\bot \times \bot \times \cdots \in \nu F$ यह उस संदिग्ध कथन पर निर्भर करता है

$\bot \times \bot \times \cdots =\bot \times \bot \times \cdots \times \bot \times \bot \times \cdots$

इसका औपचारिक औचित्य तकनीकी है और स्ट्रिंग्स को अनुक्रम के रूप में व्याख्या करने पर निर्भर करता है, अर्थात $\mathbb {N} \rightarrow \Sigma$ से कार्य करता है। सामान्यतः, यह तर्क उस तर्क के समान है जो $0.{\bar {0}}1=0$ (दशमलव को दोहराते हुए देखें)।

प्रोग्रामिंग लैंग्वेज में सहवर्ती डेटाप्रकार

स्ट्रीम (कंप्यूटिंग) की निम्नलिखित परिभाषा पर विचार करें:

data Stream a = S a (Stream a)

-- Stream "destructors"
head (S a astream) = a
tail (S a astream) = astream

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

कोलजेब्रा में 𝐹-कोलजेब्रा के साथ संबंध

सेट की श्रेणी में एंडोफंक्टर $F$ पर विचार करें:

$F(x)=A\times x$

$F(f)=\langle \mathrm {id} _{A},f\rangle$

अंतिम 𝐹-कोलजेब्रा $\nu F$ के साथ निम्नलिखित मोर्फिस्म जुड़ा हुआ है

$\mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F$

यह संबंधित मोर्फिस्म $F(\nu F)$ के साथ एक और कोलजेब्रा $F(\mathrm {out} )$ को प्रेरित करता है। क्योंकि $\nu F$ अंतिम है, एक अद्वितीय मोर्फिस्म है

${\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F$

ऐसा है कि

$\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)$

रचना ${\overline {F(\mathrm {out} )}}\circ \mathrm {out}$ एक और एफ-कोलजेब्रा समरूपता $\nu F\rightarrow \nu F$ प्रेरित करती है। चूँकि $\nu F$ अंतिम है, यह समरूपता अद्वितीय है और इसलिए $\mathrm {id} _{\nu F}$ है। कुल मिलाकर हमारे पास है:

${\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}$

$\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}$

यह समरूपता $\nu F\simeq F(\nu F)$ का साक्षी है, जो स्पष्ट शब्दों में संकेत करता है कि $\nu F$ $F$ का एक निश्चित बिंदु है और अंकन को उचित ठहराता है।

अंतिम कोलजेब्रा के रूप में स्ट्रीम करें

हम दिखाएंगे कि

Stream A

फ़ैक्टर $F(x)=A\times x$ का अंतिम कोलजेब्रा है। निम्नलिखित कार्यान्वयन पर विचार करें:

out astream = (head astream, tail astream)
out' (a, astream) = S a astream

इन्हें सरलता से परस्पर विपरीत देखा जा सकता है, जिससे समरूपता देखी जा सकती है। अधिक विवरण के लिए संदर्भ देखें.

गणितीय प्रेरण के साथ संबंध

हम प्रदर्शित करेंगे कि कैसे प्रेरण का सिद्धांत गणितीय प्रेरण को समाहित करता है। माना $P$ प्राकृतिक संख्याओं का कुछ गुण है। हम गणितीय प्रेरण की निम्नलिखित परिभाषा लेंगे:

$P(0)\land (P(n)\Rightarrow P(n+1))\Rightarrow P(\mathbb {N} )$

अब फ़ंक्शन $F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }$ पर विचार करें

$F(X)=\{0\}\cup \{x+1:x\in X\}$

यह देखना कठिन नहीं होना चाहिए $\mu F=\mathbb {N}$. इसलिए, प्रेरण के सिद्धांत के अनुसार, यदि हम $\mathbb {N}$ के कुछ गुण $P$ को सिद्ध करना चाहते हैं, तो यह दिखाना पर्याप्त है कि $P$, F-संवृत है। विस्तार से, हमें चाहिए:

$F(P)\subseteq P$

वह है,

$\{0\}\cup \{x+1:x\in P\}\subseteq P$

जैसा कि कहा गया है, यह पूर्णतः गणितीय प्रेरण है।

यह भी देखें

• 𝐹-कोलजेब्रा
• कोरकर्शन
• द्विसिमुलेशन
• एनामोर्फिज्म
• कुल कार्यात्मक प्रोग्रामिंग

अग्रिम पठन

Textbooks

• Davide Sangiorgi (2012). Introduction to Bisimulation and Coinduction. Cambridge University Press.
• Davide Sangiorgi and Jan Rutten (2011). Advanced Topics in Bisimulation and Coinduction. Cambridge University Press.

Introductory texts

• Andrew D. Gordon (1994). "A Tutorial on Co-induction and Functional Programming". 1994. pp. 78–95. CiteSeerX 10.1.1.37.3914. — mathematically oriented description
• Bart Jacobs and Jan Rutten (1997). A Tutorial on (Co)Algebras and (Co)Induction (alternate link) — describes induction and coinduction simultaneously
• Eduardo Giménez and Pierre Castéran (2007). "A Tutorial on [Co-]Inductive Types in Coq"
• Coinduction — short introduction

History

• Davide Sangiorgi. "On the Origins of Bisimulation and Coinduction", ACM Transactions on Programming Languages and Systems, Vol. 31, Nb 4, Mai 2009.

Miscellaneous

• Co-Logic Programming: Extending Logic Programming with Coinduction — describes the co-logic programming paradigm