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

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

इतिहास

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

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

परिचय

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

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

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

शब्दावली

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

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

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

Name	Notation
Lambda abstraction.	$\lambda v.y$
Application of the function f to x	$f\ x$
Multiplication of a by b	$a\cdot b$
Let x in y	$\operatorname {let} x\operatorname {in} y$
Mathematical equality	$m=n$
Beta reducible equality	$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$

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

$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$ परिमाणित चर x के साथ अभिव्यक्ति y है जिसे z के रूप में त्वरित किया गया है।

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