सहसंयोजन

This article is about computer science. For the term in abstract algebra, see Change of rings. For the use of this term in medicine and anaesthesia, see coinduction (anaesthetics).

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

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

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

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

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

विवरण

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

प्रारंभिक

होने देना $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$) सभी एफ-बंद सेटों के प्रतिच्छेदन द्वारा दिया गया है, जबकि सबसे बड़ा निश्चित-बिंदु (निरूपित)। $\nu F$) सभी एफ-संगत सेटों के संघ द्वारा दिया गया है। अब हम प्रेरण और सह-आगमन के सिद्धांतों को बता सकते हैं।

परिभाषा

प्रेरण का सिद्धांत: यदि $X$ तो, एफ-बंद है $\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$ एक अनंत स्ट्रिंग उत्पन्न नहीं कर सकता, इसलिए यह पता चला कि यह सेट एफ-बंद है और निष्कर्ष इस प्रकार है।

अब मान लीजिए कि हम लेते हैं $\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$

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

प्रोग्रामिंग भाषाओं में सहवर्ती डेटाप्रकार

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

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$ और अंकन को उचित ठहराता है।

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

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

स्ट्रीम ए

फ़नकार का अंतिम कोलजेब्रा है $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}$. अत: प्रेरण के सिद्धांत द्वारा यदि हम किसी गुण को सिद्ध करना चाहते हैं $P$ का $\mathbb {N}$, यह दिखाने के लिए पर्याप्त है $P$ एफ-बंद है. विस्तार से, हमें चाहिए:

$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