सहसंयोजन: Difference between revisions

Revision as of 10:08, 5 August 2023

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

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

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

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

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

विवरण

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

प्रारंभिक

मान लीजिए कि $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$ (दशमलव को दोहराते हुए देखें)।

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

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

data Stream a = S a (Stream a)

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

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

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

सेट की श्रेणी में एंडोफंक्टर $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

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

यह भी देखें

संदर्भ

↑ "Co-Logic Programming | Lambda the Ultimate".
↑ "Gopal Gupta's Home Page".
↑ "Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3". GitHub.
↑ Benjamin Pierce. "प्रकार और प्रोग्रामिंग भाषाएँ". The MIT Press.
↑ Dexter Kozen , Alexandra Silva. "प्रैक्टिकल कॉइंडक्शन". CiteSeerX 10.1.1.252.3961.
↑ Ralf Hinze (2012). "Generic Programming with Adjunctions". सामान्य और अनुक्रमित प्रोग्रामिंग. pp. 47–129. doi:10.1007/978-3-642-32202-0_2. ISBN 978-3-642-32201-3. {{cite book}}: |website= ignored (help)

अग्रिम पठन

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

[1] "Co-Logic Programming | Lambda the Ultimate".

[2] "Gopal Gupta's Home Page".

[3] "Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3". GitHub.

[4] Benjamin Pierce. "प्रकार और प्रोग्रामिंग भाषाएँ". The MIT Press.

[5] Dexter Kozen , Alexandra Silva. "प्रैक्टिकल कॉइंडक्शन". CiteSeerX 10.1.1.252.3961.

[6] Ralf Hinze (2012). "Generic Programming with Adjunctions". सामान्य और अनुक्रमित प्रोग्रामिंग. pp. 47–129. doi:10.1007/978-3-642-32202-0_2. ISBN 978-3-642-32201-3. {{cite book}}: |website= ignored (help)

[1]

[2]

[3]

[4]

[5]

[6]

@@ Line 1: / Line 1: @@
-{{about|computer science|the term in abstract algebra|Change of rings|the use of this term in medicine and anaesthesia|coinduction (anaesthetics)}}
+{{about|कंप्यूटर विज्ञान|एब्स्ट्रेक्ट बीजगणित में शब्द|वलय का परिवर्तन|चिकित्सा और एनेस्थेसिया में इस शब्द का उपयोग|coinduction (anaesthetics)}}
-[[कंप्यूटर विज्ञान]] में, सहसंयोजन समवर्ती इंटरैक्टिंग [[ऑब्जेक्ट (कंप्यूटिंग)]] के सिस्टम के गुणों को परिभाषित करने और साबित करने की तकनीक है।
+[[कंप्यूटर विज्ञान]] में, सहसंयोजन समवर्ती इंटरैक्टिंग [[ऑब्जेक्ट (कंप्यूटिंग)]] के सिस्टम के गुणों को परिभाषित करने और सिद्ध करने की तकनीक है।
-सहसंयोजन [[संरचनात्मक प्रेरण]] का [[गणित]]ीय दोहरा (श्रेणी सिद्धांत) है। संयोगात्मक रूप से परिभाषित प्रकारों को कोडाटा के रूप में जाना जाता है और आमतौर पर [[अनंतता]] [[डेटा संरचनाएं]] होती हैं, जैसे [[स्ट्रीम (कंप्यूटिंग)]]।
+सहसंयोजन [[संरचनात्मक प्रेरण]] का [[गणित|गणितीय]] द्वैत (श्रेणी सिद्धांत) है। संयोगात्मक रूप से परिभाषित प्रकारों को कोडाटा के रूप में जाना जाता है और सामान्यतः [[अनंतता]] [[डेटा संरचनाएं]] होती हैं, जैसे [[स्ट्रीम (कंप्यूटिंग)]] होती हैं।।
 एक परिभाषा या विनिर्देश (कंप्यूटिंग) के रूप में, सहसंयोजन वर्णन करता है कि किसी वस्तु को कैसे देखा जा सकता है, तोड़ा जा सकता है या सरल वस्तुओं में नष्ट किया जा सकता है। [[प्रमाण (गणित)]] तकनीक के रूप में, इसका उपयोग यह दिखाने के लिए किया जा सकता है कि समीकरण ऐसे विनिर्देश के सभी संभावित [[कार्यान्वयन (कंप्यूटिंग)]] से संतुष्ट है।
-कोडाटा उत्पन्न करने और उसमें हेरफेर करने के लिए, आमतौर पर [[आलसी मूल्यांकन]] के साथ, [[corecursion]] फ़ंक्शंस का उपयोग किया जाता है। अनौपचारिक रूप से, प्रत्येक आगमनात्मक कंस्ट्रक्टर पर पैटर्न-मिलान द्वारा फ़ंक्शन को परिभाषित करने के बजाय, प्रत्येक डिस्ट्रक्टर या पर्यवेक्षक को फ़ंक्शन परिणाम पर परिभाषित किया जाता है।
+कोडाटा उत्पन्न करने और उसमें परिवर्तन करने के लिए, सामान्यतः [[आलसी मूल्यांकन|लेजी मूल्यांकन]] के साथ, [[corecursion|कोरकर्शन]] फ़ंक्शंस का उपयोग किया जाता है। अनौपचारिक रूप से, प्रत्येक प्रेरणिक कंस्ट्रक्टर पर पैटर्न-मिलान द्वारा फ़ंक्शन को परिभाषित करने के अतिरिक्त, प्रत्येक डिस्ट्रक्टर या सुपरवाइज़र को फ़ंक्शन परिणाम पर परिभाषित किया जाता है।
-प्रोग्रामिंग में, सह-तर्क प्रोग्रामिंग (संक्षिप्तता के लिए सह-एलपी) तर्क प्रोग्रामिंग और संयोगात्मक तर्क प्रोग्रामिंग का प्राकृतिक सामान्यीकरण है, जो बदले में तर्क प्रोग्रामिंग के अन्य विस्तारों को सामान्यीकृत करता है, जैसे कि अनंत पेड़, आलसी विधेय, और समवर्ती संचार विधेय। सह-एलपी में तर्कसंगत पेड़ों, अनंत गुणों की पुष्टि, आलसी मूल्यांकन, समवर्ती तर्क प्रोग्रामिंग, मॉडल जांच, [[द्विसमानता]] प्रमाण इत्यादि के अनुप्रयोग हैं।<ref>{{Cite web|url=http://lambda-the-ultimate.org/node/2513|title = Co-Logic Programming &#124; Lambda the Ultimate}}</ref> सह-एलपी के प्रायोगिक कार्यान्वयन [[डलास में टेक्सास विश्वविद्यालय]] से उपलब्ध हैं<ref>{{Cite web|url=http://www.utdallas.edu/~gupta/|title = Gopal Gupta's Home Page}}</ref> और [[लॉगटॉक]] में (उदाहरण के लिए देखें <ref>{{Cite web|url=https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction|title = Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3|website = [[GitHub]]}}</ref>) और [[एसडब्ल्यूआई-प्रोलॉग]]।
+प्रोग्रामिंग में, सह-लॉजिक प्रोग्रामिंग (संक्षिप्तता के लिए सह-एलपी) लॉजिक प्रोग्रामिंग और संयोगात्मक लॉजिक प्रोग्रामिंग का प्राकृतिक सामान्यीकरण है, इस प्रकार जो परिवर्तन में लॉजिक प्रोग्रामिंग के अन्य विस्तारों को सामान्यीकृत करता है, जैसे कि अनंत लेजी, लेजी विधेय, और समवर्ती संचार विधेय सह-एलपी में लॉजिकसंगत ट्री, अनंत गुणों की पुष्टि, लेजी मूल्यांकन, समवर्ती लॉजिक प्रोग्रामिंग, मॉडल जांच, [[द्विसमानता]] प्रमाण इत्यादि के अनुप्रयोग हैं।<ref>{{Cite web|url=http://lambda-the-ultimate.org/node/2513|title = Co-Logic Programming &#124; Lambda the Ultimate}}</ref> इस प्रकार सह-एलपी के प्रायोगिक कार्यान्वयन [[डलास में टेक्सास विश्वविद्यालय]] से उपलब्ध हैं <ref>{{Cite web|url=http://www.utdallas.edu/~gupta/|title = Gopal Gupta's Home Page}}</ref> और [[लॉगटॉक]] में (उदाहरण के लिए और [[एसडब्ल्यूआई-प्रोलॉग]] देखें <ref>{{Cite web|url=https://github.com/LogtalkDotOrg/logtalk3/tree/master/examples/coinduction|title = Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3|website = [[GitHub]]}}</ref>)।
 == विवरण ==
-में <ref>{{Cite web|url=https://mitpress.mit.edu/9780262303828/types-and-programming-languages/|title = प्रकार और प्रोग्रामिंग भाषाएँ|author = Benjamin Pierce|website = The MIT Press}}</ref> प्रेरण के सिद्धांत और सह-आगमन के सिद्धांत दोनों का संक्षिप्त विवरण दिया गया है। हालाँकि यह लेख मुख्य रूप से प्रेरण से संबंधित नहीं है, फिर भी उनके कुछ हद तक सामान्यीकृत रूपों पर साथ विचार करना उपयोगी है। सिद्धांतों को बताने के लिए कुछ प्रारंभिक बातों की आवश्यकता होती है।
+<ref>{{Cite web|url=https://mitpress.mit.edu/9780262303828/types-and-programming-languages/|title = प्रकार और प्रोग्रामिंग भाषाएँ|author = Benjamin Pierce|website = The MIT Press}}</ref> प्रेरण के सिद्धांत और सह-आगमन के सिद्धांत दोनों का संक्षिप्त विवरण दिया गया है। चूँकि यह लेख मुख्य रूप से प्रेरण से संबंधित नहीं है, फिर भी उनके कुछ सीमा तक सामान्यीकृत रूपों पर एक साथ विचार करना उपयोगी है। इस प्रकार सिद्धांतों को बताने के लिए कुछ प्रारंभिक बातों की आवश्यकता होती है।
 === प्रारंभिक ===
-होने देना <math>U</math> सेट हो और <math>F</math> मोनोटोनिक फ़ंक्शन बनें#क्रम सिद्धांत में <math>2^U \rightarrow 2^U</math>, वह है:
+मान लीजिए कि <math>U</math> एक समुच्चय है और <math>F</math> एक मोनोटोन फलन <math>2^U \rightarrow 2^U</math> है, अर्थात:
 : <math> X \subseteq Y \Rightarrow F(X) \subseteq F(Y) </math>
-जब तक अन्यथा न कहा जाए, <math>F</math> एकरस माना जाएगा।
+जब तक अन्यथा न कहा जाए, <math>F</math> को एकसमान माना जाएगा।
-: X, F-बंद है यदि <math>F(X) \subseteq X </math>
+:X, F-संवृत है यदि <math>F(X) \subseteq X </math>
 : यदि X, F-संगत है <math>X \subseteq F(X) </math>
 : <math>X = F(X) </math>
-इन शब्दों को निम्नलिखित तरीके से सहज रूप से समझा जा सकता है। लगता है कि <math>X</math> अभिकथनों का समूह है, और <math>F(X)</math> वह ऑपरेशन है जो इसके निहितार्थ लेता है <math>X</math>. तब <math>X</math> एफ-बंद है जब आप पहले से ही दावा किए गए से अधिक निष्कर्ष नहीं निकाल सकते हैं <math>X</math> एफ-संगत है जब आपके सभी दावे अन्य दावों द्वारा समर्थित हैं (यानी कोई गैर-एफ-तार्किक धारणाएं नहीं हैं)।
+इन शब्दों को निम्नलिखित विधि से सामान्यतः समझा जा सकता है। मान लीजिए कि <math>X</math> अभिकथनों का एक सेट है, और <math>F(X)</math> वह ऑपरेशन है जो <math>X</math> के निहितार्थ लेता है। तब <math>X</math> 𝐹-संवृत है जब आप पहले से बताए गए निष्कर्ष से अधिक निष्कर्ष नहीं निकाल सकते हैं, जबकि <math>X</math> 𝐹-संगत है जब आपके सभी प्रमाण अन्य प्रमाणों द्वारा समर्थित हैं (अर्थात कोई "गैर-𝐹-तार्किक धारणाएं नहीं हैं")।
-नैस्टर-टार्स्की प्रमेय हमें बताता है कि सबसे कम निश्चित बिंदु <math>F</math> (संकेतित <math>\mu F</math>) सभी एफ-बंद सेटों के प्रतिच्छेदन द्वारा दिया गया है, जबकि सबसे बड़ा निश्चित-बिंदु (निरूपित)। <math>\nu F</math>) सभी एफ-संगत सेटों के संघ द्वारा दिया गया है। अब हम प्रेरण और सह-आगमन के सिद्धांतों को बता सकते हैं।
+नैस्टर-टार्स्की प्रमेय हमें बताता है कि <math>F</math> का सबसे कम निश्चित-बिंदु (जिसे <math>\mu F</math> दर्शाया गया है) सभी <math>F</math>-संवृत सेटों के प्रतिच्छेदन द्वारा दिया जाता है, जबकि सबसे बड़ा निश्चित-बिंदु (जिसे <math>\nu F</math> दर्शाया गया है) सभी F- के मिलन द्वारा दिया जाता है। सुसंगत सेट अब हम प्रेरण और सह-आगमन के सिद्धांतों को बता सकते हैं।
 === परिभाषा ===
-: प्रेरण का सिद्धांत: यदि <math>X</math> तो, एफ-बंद है <math>\mu F \subseteq X</math>
+:प्रेरण का सिद्धांत यदि <math>X</math> F-संवृत है तो <math>\mu F \subseteq X</math>
-: सहसंयोजन का सिद्धांत: यदि <math>X</math> तो, F-संगत है <math>X \subseteq \nu F</math>
+सह-आगमन का सिद्धांत यदि <math>X</math>, F-संगत है तो <math>X \subseteq \nu F</math>
 ==चर्चा==
-जैसा कि कहा गया है, सिद्धांत कुछ हद तक अपारदर्शी हैं, लेकिन निम्नलिखित तरीके से उपयोगी ढंग से सोचा जा सकता है। मान लीजिए आप किसी संपत्ति को साबित करना चाहते हैं <math>\mu F</math>. प्रेरण के सिद्धांत के अनुसार, यह एफ-बंद सेट प्रदर्शित करने के लिए पर्याप्त है <math>X</math> जिसके लिए संपत्ति धारण की जाती है। वैसे, मान लीजिए आप यह दिखाना चाहते हैं <math>x \in \nu F</math>. फिर यह एफ-संगत सेट प्रदर्शित करने के लिए पर्याप्त है <math>x</math> का सदस्य माना जाता है।
+जैसा कि कहा गया है, सिद्धांत कुछ सीमा तक अपारदर्शी हैं, किन्तु निम्नलिखित विधि से उपयोगी विधि से सोचा जा सकता है। मान लीजिए आप <math>\mu F</math> की प्रोपर्टी सिद्ध करना चाहते हैं। प्रेरण के सिद्धांत के अनुसार, यह एक 𝐹-संवृत सेट <math>x</math> प्रदर्शित करने के लिए पर्याप्त है जिसके लिए प्रोपर्टी धारण करती है। जैसे, मान लीजिए आप यह दिखाना चाहते हैं कि <math>x \in \nu F</math> फिर यह एक 𝐹-संगत सेट प्रदर्शित करने के लिए पर्याप्त है जिसका <math>x</math> को सदस्य माना जाता है।
 == उदाहरण ==
@@ Line 44: / Line 46: @@
 : <math> T = \bot \;|\;\top \;|\; T \times T </math>
-अर्थात्, प्रकारों के सेट में निचला प्रकार भी शामिल है <math>\bot</math>, शीर्ष प्रकार <math>\top</math>, और (गैर-समरूप) सूचियाँ। इन प्रकारों को वर्णमाला के ऊपर तारों से पहचाना जा सकता है <math>\Sigma = \{\bot, \top, \times\}</math>. होने देना <math>\Sigma^*</math> सभी स्ट्रिंग्स को निरूपित करें <math>\Sigma</math>. फ़ंक्शन पर विचार करें <math>F: 2^{\Sigma^*} \rightarrow 2^{\Sigma^*}</math>:
+अर्थात्, प्रकारों के सेट में "निचला प्रकार" <math>\bot</math>, "शीर्ष प्रकार" <math>\top</math>, और (गैर-समरूप) सूचियाँ सम्मिलित हैं। इन प्रकारों को <math>\Sigma = \{\bot, \top, \times\}</math> अक्षर के ऊपर तारों से पहचाना जा सकता है। मान लीजिए <math>\Sigma^*</math> पर सभी स्ट्रिंग्स <math>\Sigma</math> को दर्शाता है। <math>F: 2^{\Sigma^*} \rightarrow 2^{\Sigma^*}</math> फ़ंक्शन पर विचार करें
 : <math> F(X) = \{\bot, \top\} \cup \{ x \times y : x,y \in X \} </math>
-इस संदर्भ में, <math>x \times y</math> मतलब स्ट्रिंग का संयोजन <math>x</math>, प्रतीक <math>\times</math>, और स्ट्रिंग <math>y</math>. अब हमें अपने डेटाटाइप्स के सेट को फिक्सपॉइंट के रूप में परिभाषित करना चाहिए <math>F</math>, लेकिन यह मायने रखता है कि हम सबसे कम या सबसे बड़ा फिक्सपॉइंट लेते हैं या नहीं।
+इस संदर्भ में, <math>x \times y</math> का अर्थ है "स्ट्रिंग <math>x</math>, प्रतीक <math>\times</math> और स्ट्रिंग <math>y</math> का संयोजन" अब हमें अपने डेटाटाइप्स के सेट को <math>F</math> के फिक्सपॉइंट के रूप में परिभाषित करना चाहिए, किन्तु यह मायने रखता है कि हम सबसे कम या सबसे बड़ा फिक्सपॉइंट लेते हैं या नहीं है।
-मान लीजिए हम लेते हैं <math>\mu F</math> हमारे डेटाटाइप्स के सेट के रूप में। प्रेरण के सिद्धांत का उपयोग करके, हम निम्नलिखित दावे को सिद्ध कर सकते हैं:
+मान लीजिए कि हम डेटाटाइप्स के अपने सेट के रूप में <math>\mu F</math> लेते हैं। प्रेरण के सिद्धांत का उपयोग करके, हम निम्नलिखित प्रमाण को सिद्ध कर सकते हैं:
-: सभी डेटाप्रकार <math>\mu F</math> परिमित हैं
+:<math>\mu F</math> में सभी डेटाटाइप सीमित हैं
-इस निष्कर्ष पर पहुंचने के लिए, सभी परिमित तारों के समुच्चय पर विचार करें <math>\Sigma</math>. स्पष्ट रूप से <math>F</math> अनंत स्ट्रिंग उत्पन्न नहीं कर सकता, इसलिए यह पता चला कि यह सेट एफ-बंद है और निष्कर्ष इस प्रकार है।
+इस निष्कर्ष पर पहुंचने के लिए <math>\Sigma</math> पर सभी परिमित स्ट्रिंग्स के सेट पर विचार करें। स्पष्ट रूप से <math>F</math> एक अनंत स्ट्रिंग उत्पन्न नहीं कर सकता है, इसलिए यह पता चलता है कि यह सेट F-संवृत है और निष्कर्ष इस प्रकार है।
-अब मान लीजिए कि हम लेते हैं <math>\nu F</math> हमारे डेटाटाइप्स के सेट के रूप में। हम निम्नलिखित दावे को साबित करने के लिए सह-आगमन के सिद्धांत का उपयोग करना चाहेंगे:
+अब मान लीजिए कि हम डेटाटाइप्स के अपने सेट के रूप में <math>\nu F</math> लेते हैं। हम निम्नलिखित प्रमाण को सिद्ध करने के लिए सह-आगमन के सिद्धांत का उपयोग करना चाहेंगे:
 : प्ररूप <math>\bot \times \bot \times \cdots \in \nu F</math>
-यहाँ <math>\bot \times \bot \times \cdots </math> सभी से मिलकर बनी अनंत सूची को दर्शाता है <math>\bot</math>. सहसंयोजन के सिद्धांत का उपयोग करने के लिए, सेट पर विचार करें:
+यहाँ <math>\bot \times \bot \times \cdots </math> सभी <math>\bot</math> से युक्त अनंत सूची को दर्शाता है। सहसंयोजन के सिद्धांत का उपयोग करने के लिए, सेट पर विचार करें:
 : <math> \{\bot \times \bot \times \cdots \} </math>
-यह सेट एफ-संगत हो जाता है, और इसलिए <math> \bot \times \bot \times \cdots \in \nu F </math>. ये उस संदिग्ध बयान पर निर्भर करता है
+यह सेट 𝐹-संगत हो जाता है, और इसलिए <math> \bot \times \bot \times \cdots \in \nu F </math> यह उस संदिग्ध कथन पर निर्भर करता है
 : <math> \bot \times \bot \times \cdots = \bot \times \bot \times \cdots \times \bot \times \bot \times \cdots </math>
-इसका औपचारिक औचित्य तकनीकी है और स्ट्रिंग्स को Sequence#Formal_definition_and_basic_properties के रूप में व्याख्या करने पर निर्भर करता है, यानी से कार्य करता है <math>\mathbb{N} \rightarrow \Sigma</math>. सहज रूप से, यह तर्क उस तर्क के समान है <math>0.\bar{0}1 = 0</math> (पुनरावर्ती दशमलव#Repeating_decimals_as_infinite_series देखें)।
+इसका औपचारिक औचित्य तकनीकी है और स्ट्रिंग्स को अनुक्रम के रूप में व्याख्या करने पर निर्भर करता है, अर्थात <math>\mathbb{N} \rightarrow \Sigma</math> से कार्य करता है। सामान्यतः, यह तर्क उस तर्क के समान है जो <math>0.\bar{0}1 = 0</math> (दशमलव को दोहराते हुए देखें)।
 === प्रोग्रामिंग भाषाओं में सहवर्ती डेटाप्रकार ===
-स्ट्रीम_(कंप्यूटिंग) की निम्नलिखित परिभाषा पर विचार करें:<ref>{{Cite CiteSeerX|title = प्रैक्टिकल कॉइंडक्शन|author =  Dexter Kozen , Alexandra Silva | citeseerx=10.1.1.252.3961 }}</ref>
+स्ट्रीम (कंप्यूटिंग) की निम्नलिखित परिभाषा पर विचार करें:<ref>{{Cite CiteSeerX|title = प्रैक्टिकल कॉइंडक्शन|author =  Dexter Kozen , Alexandra Silva | citeseerx=10.1.1.252.3961 }}</ref>
 <syntaxhighlight lang="haskell">
@@ Line 77: / Line 83: @@
 tail (S a astream) = astream
 </syntaxhighlight>
-यह ऐसी परिभाषा प्रतीत होती है जो गैर-अच्छी तरह से स्थापित_सेट_सिद्धांत है| अच्छी तरह से स्थापित नहीं है, लेकिन फिर भी यह प्रोग्रामिंग में उपयोगी है और इसके बारे में तर्क किया जा सकता है। किसी भी स्थिति में, स्ट्रीम तत्वों की अनंत सूची है जिसमें से आप पहले तत्व का निरीक्षण कर सकते हैं, या दूसरी स्ट्रीम प्राप्त करने के लिए तत्व को सामने रख सकते हैं।
+यह ऐसी परिभाषा प्रतीत होती है जो गैर-अच्छी तरह से स्थापित सेट सिद्धांत है | अच्छी तरह से स्थापित नहीं है, किन्तु फिर भी यह प्रोग्रामिंग में उपयोगी है और इसके बारे में लॉजिक किया जा सकता है। किसी भी स्थिति में, स्ट्रीम अवयवो की अनंत सूची है जिसमें से आप पहले अवयव का निरीक्षण कर सकते हैं, या दूसरी स्ट्रीम प्राप्त करने के लिए अवयव को सामने रख सकते हैं।
-=== [[ कोलजेब्रा में ]]|एफ-कोलजेब्रा के साथ संबंध<ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-642-32202-0_2|chapter = Generic Programming with Adjunctions|author = Ralf Hinze| title=सामान्य और अनुक्रमित प्रोग्रामिंग|website = Springer| series=Lecture Notes in Computer Science | year=2012 | volume=7470 | pages=47–129 | doi=10.1007/978-3-642-32202-0_2 | isbn=978-3-642-32201-3 }}</ref> ===
+=== [[ कोलजेब्रा में | '''कोलजेब्रा में''']] 𝐹-कोलजेब्रा के साथ संबंध<ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-642-32202-0_2|chapter = Generic Programming with Adjunctions|author = Ralf Hinze| title=सामान्य और अनुक्रमित प्रोग्रामिंग|website = Springer| series=Lecture Notes in Computer Science | year=2012 | volume=7470 | pages=47–129 | doi=10.1007/978-3-642-32202-0_2 | isbn=978-3-642-32201-3 }}</ref> ===
-फ़ंक्टर#एंडोफ़ंक्टर पर विचार करें <math>F</math> [[सेट की श्रेणी]] में:
+सेट की श्रेणी में एंडोफंक्टर <math>F</math> पर विचार करें:
 : <math>F(x) = A \times x</math>
 : <math>F(f) = \langle \mathrm{id}_A, f \rangle </math>
-अंतिम एफ-कोलजेब्रा <math>\nu F</math> इसके साथ निम्नलिखित रूपवाद जुड़ा हुआ है:
+अंतिम 𝐹-कोलजेब्रा <math>\nu F</math> के साथ निम्नलिखित मोर्फिस्म जुड़ा हुआ है
 : <math> \mathrm{out}: \nu F \rightarrow F(\nu F) = A \times \nu F </math>
-यह और कोलजेब्रा को प्रेरित करता है <math>F(\nu F)</math> संबद्ध रूपवाद के साथ <math>F(\mathrm{out})</math>. क्योंकि <math>\nu F</math> अंतिम है, अद्वितीय रूपवाद है
+यह संबंधित मोर्फिस्म <math>F(\nu F)</math> के साथ एक और कोलजेब्रा <math>F(\mathrm{out})</math> को प्रेरित करता है। क्योंकि <math>\nu F</math> अंतिम है, एक अद्वितीय मोर्फिस्म है
 : <math> \overline{F(\mathrm{out})}: F(\nu F) \rightarrow \nu F </math>
@@ Line 95: / Line 103: @@
 : <math> \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)</math>
-रचना <math>\overline{F(\mathrm{out})} \circ \mathrm{out}</math> और एफ-कोलजेब्रा समरूपता को प्रेरित करता है <math>\nu F \rightarrow \nu F</math>. तब से <math>\nu F</math> अंतिम है, यह समरूपता अद्वितीय है और इसलिए <math>\mathrm{id}_{\nu F}</math>. कुल मिलाकर हमारे पास है:
+रचना <math>\overline{F(\mathrm{out})} \circ \mathrm{out}</math> एक और एफ-कोलजेब्रा समरूपता <math>\nu F \rightarrow \nu F</math> प्रेरित करती है। चूँकि <math>\nu F</math> अंतिम है, यह समरूपता अद्वितीय है और इसलिए <math>\mathrm{id}_{\nu F}</math> है। कुल मिलाकर हमारे पास है:
 : <math> \overline{F(\mathrm{out})} \circ \mathrm{out} = \mathrm{id}_{\nu F} </math>
 : <math> \mathrm{out} \circ \overline{F(\mathrm{out})} = F\left(\overline{F(\mathrm{out})}\right) \circ \mathrm{out}) = \mathrm{id}_{F(\nu F)} </math>
-यह समरूपता का साक्षी है <math>\nu F \simeq F(\nu F)</math>, जो स्पष्ट शब्दों में इंगित करता है <math>\nu F</math> का निश्चित बिंदु है <math>F</math> और अंकन को उचित ठहराता है।
+यह समरूपता <math>\nu F \simeq F(\nu F)</math> का साक्षी है, जो स्पष्ट शब्दों में संकेत करता है कि <math>\nu F</math> <math>F</math> का एक निश्चित बिंदु है और अंकन को उचित ठहराता है।
 ==== अंतिम कोलजेब्रा के रूप में स्ट्रीम करें ====
-हम दिखाएंगे कि <pre>स्ट्रीम ए</pre> फ़नकार का अंतिम कोलजेब्रा है <math>F(x) = A \times x</math>. निम्नलिखित कार्यान्वयन पर विचार करें:
+हम दिखाएंगे कि <syntaxhighlight lang="abl">
+Stream A
+</syntaxhighlight>
+फ़ैक्टर <math>F(x) = A \times x</math> का अंतिम कोलजेब्रा है। निम्नलिखित कार्यान्वयन पर विचार करें:
 <syntaxhighlight lang="haskell">
@@ Line 109: / Line 123: @@
 out' (a, astream) = S a astream
 </syntaxhighlight>
-इन्हें आसानी से परस्पर विपरीत देखा जा सकता है, जिससे समरूपता देखी जा सकती है। अधिक विवरण के लिए संदर्भ देखें.
+इन्हें सरलता से परस्पर विपरीत देखा जा सकता है, जिससे समरूपता देखी जा सकती है। अधिक विवरण के लिए संदर्भ देखें.
 ===[[गणितीय प्रेरण]] के साथ संबंध ===
-हम प्रदर्शित करेंगे कि कैसे प्रेरण का सिद्धांत गणितीय प्रेरण को समाहित करता है।
+हम प्रदर्शित करेंगे कि कैसे प्रेरण का सिद्धांत गणितीय प्रेरण को समाहित करता है। माना <math>P</math> [[प्राकृतिक संख्या]]ओं का कुछ गुण है। हम गणितीय प्रेरण की निम्नलिखित परिभाषा लेंगे:
-होने देना <math>P</math> [[प्राकृतिक संख्या]]ओं की कुछ संपत्ति बनें। हम गणितीय प्रेरण की निम्नलिखित परिभाषा लेंगे:
 : <math>P(0) \and (P(n) \Rightarrow P(n+1)) \Rightarrow P(\mathbb{N})</math>
-अब फ़ंक्शन पर विचार करें <math>F: 2^{\mathbb{N}} \rightarrow 2^{\mathbb{N}}</math>:
+अब फ़ंक्शन <math>F: 2^{\mathbb{N}} \rightarrow 2^{\mathbb{N}}</math> पर विचार करें
 : <math>F(X) = \{0\} \cup \{x + 1 : x \in X \}</math>
-इसे देखना कठिन नहीं होना चाहिए <math>\mu F = \mathbb{N}</math>. अत: प्रेरण के सिद्धांत द्वारा यदि हम किसी गुण को सिद्ध करना चाहते हैं <math>P</math> का <math>\mathbb{N}</math>, यह दिखाने के लिए पर्याप्त है <math>P</math> एफ-बंद है. विस्तार से, हमें चाहिए:
+यह देखना कठिन नहीं होना चाहिए <math>\mu F = \mathbb{N}</math>. इसलिए, प्रेरण के सिद्धांत के अनुसार, यदि हम <math>\mathbb{N}</math> के कुछ गुण <math>P</math> को सिद्ध करना चाहते हैं, तो यह दिखाना पर्याप्त है कि <math>P</math>, F-संवृत है। विस्तार से, हमें चाहिए:
 : <math>F(P) \subseteq P</math>
 वह है,
 : <math>\{0\} \cup \{x + 1 : x \in P \} \subseteq P </math>
-जैसा कि कहा गया है, यह बिल्कुल गणितीय प्रेरण है।
+जैसा कि कहा गया है, यह पूर्णतः गणितीय प्रेरण है।
 ==यह भी देखें==
-* एफ-कोलजेब्रा
+* 𝐹-कोलजेब्रा
 * कोरकर्शन
 * [[द्विसिमुलेशन]]

Anonymous

Search

सहसंयोजन: Difference between revisions

Namespaces

More

Page actions

Revision as of 10:08, 5 August 2023

Contents

विवरण

प्रारंभिक

परिभाषा

चर्चा

उदाहरण

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

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

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

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

सहसंयोजन: Difference between revisions

Revision as of 10:08, 5 August 2023

विवरण

प्रारंभिक

परिभाषा

चर्चा

उदाहरण

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

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

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

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

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

यह भी देखें

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories

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