डिडक्टिव लैम्ब्डा कैलकुलस

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

इतिहास

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

हास्केल करी ने 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 न तो सच है और न ही झूठ है; यह इसका भी प्रदर्शन करता है कि नकारात्मकता गैर-तार्किक मानों पर लागू किए जाने पर कम सार्थक होती है।

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

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

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

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

$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$

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

$f\ t\ {\underset {\beta }{=}}\ g\ t$