डिडक्टिव लैम्ब्डा कैलकुलस: Difference between revisions

Revision as of 23:57, 14 July 2023

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

इतिहास

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

हास्केल करी ने 1941 में अनुमानात्मक (प्रमाणिक) संक्रमणीय तर्कशास्त्र का अध्ययन किया। संक्रमणीय तर्कशास्त्र लैम्बडा कैलकुलस से गहरे रूप से संबंधित है, और इन्हीं में वही पराधिकरण मौजूद हैं।

बाद में लैम्बडा कैलकुलस को प्रोग्रामिंग भाषा की परिभाषा के रूप में पुनर्जीवित किया गया था।

परिचय

लैम्ब्डा कैलकुलस फंक्शनल प्रोग्रामिंग भाषाओं के विकास के लिए मॉडल और प्रेरणा है। इन भाषाओं में लैम्बडा अभिव्यक्ति को प्रदर्शित किया जाता है और इसे फंक्शनों के अनुप्रयोग के साथ और प्रकार के साथ उपयोग किया जाता है।

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

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

शब्दावली

इस चर्चा के लिए, लैम्बडा अभिव्यक्ति को गणित में अतिरिक्त ऑपरेटर के रूप में जोड़ा जाता है। बूलियन बीजगणित और वास्तविक संख्या जैसे सामान्य डोमेन उपलब्ध रहेंगे। इन डोमेनों पर गणितीय समानता लागू होगी। इस परिभाषा से कौन सी समस्याएं उत्पन्न होती हैं, इसे देखना है।

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

निम्नलिखित तालिका संक्षेप करती है;

नाम	नोटेशन
लैम्ब्डा अमूर्तन.	$\lambda v.y$
फ़ंक्शन f से x तक का अनुप्रयोग	$f\ x$
a को b से गुणा करना	$a\cdot b$
मान लीजिए x में y है	$\operatorname {let} x\operatorname {in} y$
गणितीय समानता	$m=n$
बीटा कम करने योग्य समानता	$m\ {\underset {\beta }{=}}\ n$

गणित के रूप में लैम्ब्डा कैलकुलस की व्याख्या

गणितीय व्याख्या में, लैम्बडा शब्द मानों को प्रतिष्ठित करते हैं। एटा और बीटा संक्षेपण यानी संकलन और प्रमाणिक स्थान बदलने वाली कदम हैं जो अभिव्यक्तियों के मानों को परिवर्तित नहीं करते हैं:

\operatorname {eta-reduct} [X]=X

\operatorname {beta-reduct} [X]=X

गणित के रूप में एटा कमी

ईटा-संक्षेपण की परिभाषा है,

x\not \in \operatorname {FV} (f)\to \operatorname {eta-reduct} [\lambda x.(f\ x)]=f

गणितीय व्याख्या में,

\operatorname {eta-reduct} [X]=X

f को चर मानते हुए,

\lambda x.(f\ x)=f

या देने से

$f\ x=y$

f\ x=y\iff f=\lambda x.y

यह परिभाषा समीकरण में f के लिए $\lambda x.y$ को परिभाषित करती है, जो समीकरण में समाधान है,

f\ x=y

गणित के रूप में बीटा कमी

बीटा-संक्षेपण का परिभाषित होता है,

\operatorname {beta-reduct} [(\lambda x.b)\ z]=b[x:=z]

और के रूप में,

\operatorname {beta-reduct} [X]=X

तो,

(\lambda x.b)\ z=b[x:=z]

यह नियम सार्वभौमिक परिमाणीकरण चर के सार्वभौमिक तात्कालिकता द्वारा निहित है। यदि,

\forall x:f\ x=y

तो $f\ z$ व्यक्ति y का अभिव्यक्ति है जिसमें य नियतित चर x के रूप में इंस्टेंटिएशन होती है।

f\ z=y[x:=z]

इसलिए,

(\lambda x.y)\ z=y[x:=z]

बीटा-संक्षेपण ईटा-संक्षेपण से सूचित होता है, इसलिए दो परिभाषाओं के बीच कोई विरोध नहीं है।

द्विसंयोजकता के सिद्धांत के साथ असंगति

चलिए z बूलियन बीजगणित (संरचना) है; तब हम बिना किसी समाधान वाला समीकरण बना सकते हैं,

z=\neg z

इस समीकरण को पुनरावृत्ति द्वारा हल करने के लिए, हम नया फ़ंक्शन $f$ पेश करते हैं जिसे निम्न रूप में परिभाषित किया जाता है,

f\ n=\neg (n\ n)

यहाँ $n$ परस्पर अवलंबी चर है जो पुनरावृत्ति मान को धारण करने के लिए है। (हम इसे लेते हैं कि $\neg$ अभी भी बूलियन लौटाता है, यदि इसे गैर-बूलियन तर्क दिया जाए।) इटा-संक्षेपण द्वारा, हम प्राप्त करते हैं,

f=\lambda x.\neg (x\ x)

और तब,

{\begin{aligned}f\ f&=(\lambda x.\neg (x\ x))(\lambda x.\neg (x\ x))\\&=\neg ((\lambda x.\neg (x\ x))(\lambda x.\neg (x\ x)))\\&=\neg (f\ f)\end{aligned}}

तब $f f$ न तो सच है और न ही झूठ है, और जैसा कि $f f$ बूलियन मान है (किसी भी $x$ पर, $f$ बूलियन $\neg (x\ x)$ लौटाता है ) है, तो हम देखते हैं कि $f f$ न तो सच है और न ही झूठ है; यह इसका भी प्रदर्शन करता है कि नकारात्मकता गैर-तार्किक मानों पर लागू किए जाने पर कम सार्थक होती है।

गहन बनाम विस्तारित समानता

लैम्बडा कैलकुलस को प्रमाणात्मक प्रणाली के रूप में व्याख्या करने के लिए एक और कठिनाई यह है कि मानों को लैम्बडा शब्दों के रूप में प्रतिष्ठित कैसे किया जाए, जो कि फ़ंक्शन को प्रतिष्ठित करते हैं। अनवर्णित लैम्बडा कैलकुलस को लैम्बडा शब्द परिवर्तनों के द्वारा क्रियान्वित किया जाता है, जब तक शब्द साधारित रूप में नहीं हो जाता है। भावनात्मक व्याख्या में^[5]^[6] समानता की मानिक व्याख्या है कि एकैम्बडा शब्द को साधारित रूप में परिवर्तित करना, वह लैम्बडा शब्द का मान है।

इस व्याख्या में, लैम्बडा अभिव्यक्ति की पहचान उसकी संरचना के रूप में होती है। दो लैम्बडा शब्द समान होते हैं यदि वे अल्फा परिवर्तनीय हैं।

फ़ंक्शन की समानता की व्याख्यात्मक परिभाषा है कि दो फ़ंक्शन समान होते हैं यदि वे समान मैपिंग करते हैं:

f=g\iff (\forall xf\ x=g\ x)

इसका तरीका यह है कि व्याख्यात्मक समानता फ़ंक्शनों की समानता का वर्णन करती है, जबकि भावनात्मक समानता फ़ंक्शन के अमल की समानता का वर्णन करती है।

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

उदाहरण

अंकगणित में, वितरण का नियम इसे सिद्धांत रूप में कहता है कि $2*(r+s)=2*r+2*s$ . अंकगणित के चर्च एनकोडिंग का उपयोग करके, इसके दोनों पक्षों को लैम्बडा शब्दों के रूप में प्रदर्शित किया जा सकता है।

इस प्रकार, वितरण का नियम यह कहता है कि दो फ़ंक्शन,

\lambda r.\lambda s.2*(r+s)=\lambda r.\lambda s.2*r+2*s

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

\begin{aligned} λ r . λ s . mult 2 (plus r s) & = λ r . λ s . plus (mult 2 r) (mult 2 s) \\ λ r . λ s . (λ m . λ n . λ f . m (n f)) (λ f . λ x . f (f x)) ((λ m . λ n . λ f . λ x . m f (n f x)) r s) & = λ r . λ s . (λ m . λ n . λ f . λ x . m f (n f x)) ((λ m . λ n . λ f . m (n f)) (λ f . λ x . f (f x)) r) ((λ m . λ n . λ f . m (n f)) \end{aligned}

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

यदि, सभी लैम्ब्डा-अभिव्यक्तियों $t$ के लिए हमारे पास $f\ t\ {\underset {\beta }{=}}\ g\ t$ , हो, तो $f\ {\underset {\beta }{=}}\ g$ होता है।

हमारी स्थिति में, "सभी लैम्ब्डा-अभिव्यक्तियों" का अर्थ होता है "सभी चर्च अंकगणित", इसलिए यह प्रामाणिक अर्थ में भी ओमेगा-नियम होता है। ध्यान दें कि ओमेगा-नियम ईटा-नियम की प्राथमिकता को दिखाता है, क्योंकि $f\ t\ {\underset {\beta }{=}}\ (\lambda x.f\ x)\ t$ दायरिकरणीय घटना के बाद दाईं ओर अंकित होता है।

सैद्धांतिक डोमेन सेट करें

लैम्बडा अवचलन स्वीकार किया जाता है कि लैम्बडा अवचलन फ़ंक्शन की फ़ंक्शन होती है। प्राकृतिक कदम यह है कि लैम्बडा अवचलन के लिए डोमेन को सेट के रूप में परिभाषित किया जाए, जो सभी फ़ंक्शनों का सेट होता है।

डोमेन D से रेंज R तक सभी फ़ंक्शंस का सेट K निम्न में दिया गया है:

f\in K\iff (\forall x:x\in D\implies f\ x\in R)

तब (काल्पनिक) सभी फ़ंक्शनों के सेट की परिभाषा F में दी गई है:

f\in F\iff (\forall x:x\in F\implies f\ x\in F)

यह परिभाषा किसी अभिलक्षणिक सेट सिद्धांत में रचना नहीं की जा सकती है; और यह नाइव समीकरण, यदि इसे सेट सिद्धांत में लिखा जा सकता है, तो इसका कोई समाधान नहीं होता है।

अब लैम्बडा कैलकुलस को बीटा घटना और ईटा घटना द्वारा परिभाषित किया जाता है। समानता को परिभाषित करने के रूप में घटना का व्याख्यान एक निहित डोमेन के लिए देता है। नियम हैं:

प्रत्येक लैम्ब्डा एब्स्ट्रैक्शन का मान होता है।
लैम्बडा पद का बीटा घटना ही मान होता है
लैम्बडा पद का ईटा घटना ही मान होता है।
अल्फा परिवर्तनीय लैम्बडा पद समान होते हैं।
[यदि ओमेगा-नियम मौजूद है] "ओमेगा-समान" लैम्बडा पद समान होते हैं।
यदि दो लैम्बडा पदों को उपरोक्त नियमों द्वारा समान नहीं किया जा सकता है, तो वे समान नहीं होते हैं।

यदि दो लैम्ब्डा पदों को सामान्य रूप में घटाया जा सकता है तो चर्च-रोसेर प्रमेय का उपयोग यह दिखाने के लिए किया जा सकता है कि वे समान हैं यदि उनके सामान्य रूप अल्फा परिवर्तनीय हैं।

यदि दोनों पदों में से एक या दोनों ही साधारित रूप में नहीं हैं, तो समानता की असंभवता दिखाती है कि सामान्यतः दो लैम्बडा पदों के बीच समानता निर्धारित करने के लिए कोई एल्गोरिदम नहीं होता है। इससे सामान्यतः लैम्बडा कैलकुलस डोमेन के विभिन्न तत्वों को जानना असंभव हो जाता है।

उदाहरण: कोई समाधान नहीं → एक समाधान

उदाहरण के रूप में समीकरण $x=\neg x$ को चर्च एन्कोडिंग का उपयोग करके और करी के Y कॉम्बिनेटर का उपयोग करके कोड किया जा सकता है:

\operatorname {not} _{1}=\lambda p.\lambda a.\lambda b.p\ b\ a

(\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))(\lambda p.\lambda a.\lambda b.p\ b\ a)

और यह पुनरावर्तन है,

(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))

(\lambda p.\lambda a.\lambda b.p\ b\ a)\ ((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))

\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a

...

\lambda a.\lambda b.(\lambda a.\lambda b.((\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x)))\ b\ a)\ b\ a

... (बीटा और फिर ईटा कमी)

(\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))\ (\lambda x.(\lambda p.\lambda a.\lambda b.p\ b\ a)\ (x\ x))

यह पहली पंक्ति है और यह अनंतिक्रिया अवधि तक पुनरावृत्ति होगा। यह अभिव्यक्ति कभी साधारित रूप तक कम नहीं होती है। हालांकि, घटना में सम्मलित हर लैम्बडा पद एक ही मान को प्रतिष्ठित करता है। यह मान ट्रू या फॉल्स के एनकोडिंग से अलग होता है। यह बूलियन डोमेन का हिस्सा नहीं है, लेकिन यह लैम्बडा कैलकुलस डोमेन में मौजूद होता है।

उदाहरण: एकाधिक समाधान → एक समाधान

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

इस एनकोडिंग का उपयोग करके,

x^{2}=n\Rightarrow x={\frac {n}{x}}\Rightarrow f\ x={\frac {n}{x}}\land Y\ f=x

विभाजन के कार्यान्वयन का उपयोग करते हुए,

Y(\operatorname {divide} n)

यदि n शून्य के समान नहीं है, तो हस्ताक्षरित संख्याओं के डोमेन में दो मानों का प्रतिनिधित्व करता है। हालाँकि यह लैम्ब्डा अभिव्यक्ति है इसलिए लैम्ब्डा कैलकुलस डोमेन में इसका केवल मान होता है। इस लैम्बडा शब्द का बीटा संकुचन कभी साधारित रूप नहीं प्राप्त करता है। हालाँकि यह मान का प्रतिनिधित्व करता है, इसलिए लैम्ब्डा कैलकुलस डोमेन में एकल मान हस्ताक्षरित संख्या डोमेन में मानों का प्रतिनिधित्व करता है।

यह भी देखें

लैम्ब्डा कैलकुलस
आओ अभिव्यक्ति
चर्च एन्कोडिंग

संदर्भ

↑ Church, A. (1932). "तर्क की नींव के लिए अभिधारणाओं का एक सेट". Annals of Mathematics. Series 2. 33 (2): 346–366. doi:10.2307/1968337. JSTOR 1968337.
↑ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
↑ Kleene, S. C. & Rosser, J. B. (1935). "कुछ औपचारिक तर्कों की असंगति". Annals of Mathematics. 36 (3): 630–636. doi:10.2307/1968646. JSTOR 1968646.
↑ Curry, Haskell B. (1942). "कुछ औपचारिक तर्क की असंगति". The Journal of Symbolic Logic. 7 (3): 115–117. doi:10.2307/2269292. JSTOR 2269292. S2CID 121991184.
↑ Selinger, Peter. "Lecture Notes on Lambda Calculus (PDF)" (PDF). p. 6.
↑ "The Lambda Calculus". Lambda calculus – intensionality. Stanford. 2021. p. 1.2 Intensionality.

[1] Church, A. (1932). "तर्क की नींव के लिए अभिधारणाओं का एक सेट". Annals of Mathematics. Series 2. 33 (2): 346–366. doi:10.2307/1968337. JSTOR 1968337.

[2] For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).

[3] Kleene, S. C. & Rosser, J. B. (1935). "कुछ औपचारिक तर्कों की असंगति". Annals of Mathematics. 36 (3): 630–636. doi:10.2307/1968646. JSTOR 1968646.

[4] Curry, Haskell B. (1942). "कुछ औपचारिक तर्क की असंगति". The Journal of Symbolic Logic. 7 (3): 115–117. doi:10.2307/2269292. JSTOR 2269292. S2CID 121991184.

[5] Selinger, Peter. "Lecture Notes on Lambda Calculus (PDF)" (PDF). p. 6.

[6] "The Lambda Calculus". Lambda calculus – intensionality. Stanford. 2021. p. 1.2 Intensionality.

[1]

[2]

[3]

[4]

[5]

[6]

Anonymous

Search

डिडक्टिव लैम्ब्डा कैलकुलस: Difference between revisions

Namespaces

More

Page actions

Revision as of 23:57, 14 July 2023

Contents

इतिहास

परिचय

शब्दावली