लैम्ब्डा कैलकुलस गणितीय तर्क में एक औपचारिक प्रणाली है जो अमूर्त-आधारित गणनाओं को व्यक्त करने और बाध्यकारी और चर प्रतिस्थापन का उपयोग करके कार्यों को लागू करने के लिए है। यह एक सार्वभौमिक मॉडल है जिसे किसी भी ट्यूरिंग मशीन के डिजाइन पर लागू किया जा सकता है। लैम्ब्डा कैलकुलस की शुरुआत 1930 के दशक में एक प्रसिद्ध गणितज्ञ चर्च ने की थी।
सिस्टम में लैम्ब्डा सदस्यों का निर्माण और उन पर कमी संचालन करना शामिल है।
स्पष्टीकरण और अनुप्रयोग
ग्रीक अक्षर लैम्ब्डा (λ) का प्रयोग लैम्ब्डा एक्सप्रेशन और लैम्ब्डा शब्दों में एक फंक्शन में एक वेरिएबल के बंधन को दर्शाने के लिए किया जाता है।
लैम्ब्डा कैलकुलस को अनटाइप या टाइप किया जा सकता है। पहले संस्करण में, फ़ंक्शंस का उपयोग केवल तभी किया जा सकता है जब वे इस प्रकार का डेटा प्राप्त करने में सक्षम हों। टाइप किए गए लैम्ब्डा कैलकुली कमजोर हैं, एक छोटे मूल्य को व्यक्त कर सकते हैं। लेकिन, दूसरी ओर, वे आपको और बातें साबित करने की अनुमति देते हैं।
मजबूत लैम्ब्डा कैलकुलस प्रमेयों को सिद्ध करने का अवसर दिए बिना वैज्ञानिकों की इच्छा अधिक करने की इच्छा है।
सिस्टम में गणित, दर्शन, भाषा विज्ञान और कंप्यूटर विज्ञान के कई अलग-अलग क्षेत्रों में अनुप्रयोग हैं। सबसे पहले, लैम्ब्डा कैलकुलस एक कलन है जिसने प्रोग्रामिंग भाषाओं के सिद्धांत के विकास में महत्वपूर्ण भूमिका निभाई है। यह कार्यात्मक निर्माण की शैली है जिसे सिस्टम लागू करते हैं। वे इन श्रेणियों के सिद्धांत में शोध का एक गर्म विषय भी हैं।
डमी के लिए
लैम्ब्डा कैलकुलस को गणितज्ञ अलोंजो चर्च ने 1930 के दशक में विज्ञान की नींव में अपने शोध के हिस्से के रूप में पेश किया था। मूल प्रणाली को 1935 में तार्किक रूप से असंगत दिखाया गया था जब स्टीफन क्लेन और जे.बी. रॉसर ने क्लेन-रॉसर विरोधाभास विकसित किया था।
बाद में, 1936 में, चर्च ने केवल उसी भाग को प्रकाशित किया जो गणना के लिए प्रासंगिक है, जिसे अब अनटाइप्ड लैम्ब्डा कैलकुलस कहा जाता है। 1940 में उन्होंने एक कमजोर लेकिन तार्किक रूप से सुसंगत सिद्धांत भी पेश किया जिसे प्राइम टाइप सिस्टम के रूप में जाना जाता है। अपने काम में, उन्होंने पूरे सिद्धांत को सरल शब्दों में समझाया, इसलिए यह कहा जा सकता है कि चर्च ने डमी के लिए कैलकुलस लैम्ब्डा प्रकाशित किया।
1960 के दशक तक, जब प्रोग्रामिंग भाषाओं से इसका संबंध स्पष्ट हो गया, तो सिर्फ एक औपचारिकता थी। प्राकृतिक भाषा के शब्दार्थ में रिचर्ड मोंटेग्यू और अन्य भाषाविदों के अनुप्रयोगों के लिए धन्यवाद, कैलकुलस ने भाषा विज्ञान और कंप्यूटर विज्ञान दोनों में जगह बना ली है।
प्रतीक की उत्पत्ति
लैम्ब्डा एक शब्द या संक्षिप्त नाम के लिए खड़ा नहीं है, यह रसेल के प्रधान गणित में एक संदर्भ से आता है जिसके बाद दो टाइपोग्राफिक परिवर्तन होते हैं। संकेतन उदाहरण: f (y)=2y + 1 के साथ एक फ़ंक्शन f के लिए 2ŷ + 1 है। और यहां हम इनपुट चर को लेबल करने के लिए y के ऊपर एक कैरेट ("टोपी") का उपयोग करते हैं।
चर्च मूल रूप से समान प्रतीकों का उपयोग करने का इरादा रखता था, लेकिन टाइपसेटर अक्षरों के ऊपर "टोपी" चिह्न लगाने में असमर्थ थे। तो इसके बजाय उन्होंने इसे मूल रूप से "/\y.2y+1" के रूप में मुद्रित किया। संपादन की अगली कड़ी में, टाइपिस्टों ने "/ \" को एक समान दिखने वाले वर्ण से बदल दिया।
लैम्ब्डा कैलकुलस का परिचय
सिस्टम में शब्दों की एक भाषा होती है, जिसे एक निश्चित औपचारिक सिंटैक्स द्वारा चुना जाता है, और परिवर्तन नियमों का एक सेट जो उन्हें हेरफेर करने की अनुमति देता है। अंतिम बिंदु को एक समीकरण सिद्धांत या एक परिचालन परिभाषा के रूप में माना जा सकता है।
लैम्ब्डा कैलकुलस में सभी फंक्शन गुमनाम होते हैं, जिसका अर्थ है कि उनके नाम नहीं हैं। वे केवल एक इनपुट चर लेते हैं, और कई चर के साथ भूखंडों को लागू करने के लिए करी का उपयोग किया जाता है।
लैम्ब्डा शब्द
कैलकुलस सिंटैक्स कुछ अभिव्यक्तियों को मान्य और अन्य को अमान्य के रूप में परिभाषित करता है। जैसे वर्णों के विभिन्न तार मान्य C प्रोग्राम हैं और कुछ नहीं हैं। लैम्ब्डा कैलकुलस की वास्तविक अभिव्यक्ति को "लैम्ब्डा टर्म" कहा जाता है।
निम्नलिखित तीन नियम एक आगमनात्मक परिभाषा प्रदान करते हैं जो हो सकता हैसभी वाक्यात्मक रूप से मान्य अवधारणाओं के निर्माण के लिए लागू करें:
x चर अपने आप में एक वैध लैम्ब्डा शब्द है:
- यदि T, LT है और x अस्थिर है, तो (lambda xt) को एब्स्ट्रैक्शन कहा जाता है।
- यदि T और s अवधारणाएँ हैं, तो (TS) को एक अनुप्रयोग कहा जाता है।
और कुछ नहीं एक लैम्ब्डा टर्म है। इस प्रकार, एक अवधारणा तभी मान्य होती है जब और केवल इन तीन नियमों के बार-बार आवेदन द्वारा प्राप्त की जा सकती है। हालांकि, कुछ कोष्ठक अन्य मानदंडों के अनुसार छोड़े जा सकते हैं।
परिभाषा
लैम्ब्डा एक्सप्रेशन से मिलकर बनता है:
- चर वी 1, वी 2, …, वी एन, …
- अमूर्तता के प्रतीक 'λ' और बिंदु '।
- कोष्ठक ()।
सेट Λ को आगमनात्मक रूप से परिभाषित किया जा सकता है:
- यदि x एक चर है, तो x;
- x स्थिर नहीं है और M ∈, तब (λx. M);
- एम, एन, फिर (एमएन).
पदनाम
लैम्ब्डा के भावों के अंकन को साफ रखने के लिए, निम्नलिखित सम्मेलनों का आमतौर पर उपयोग किया जाता है:
- बाहरी कोष्ठक छोड़े गए: (MN) के बजाय MN।
- आवेदनों को साहचर्य माना जाता है: कोई ((MN) P) के बजाय MNP लिख सकता है।
- अमूर्तता का शरीर आगे दाईं ओर फैला हुआ है: λx. MN का अर्थ है λx। (एमएन), नहीं (λx.एम) एन.
- एब्स्ट्रैक्शन का क्रम कम हो गया है: x.λy.λz. N λxyz. N हो सकता है।
मुक्त और बाध्य चर
ऑपरेटर λ अपने गैर-स्थिरांक को अमूर्तता के शरीर में कहीं भी जोड़ता है। वेरिएबल जो स्कोप में आते हैं बाउंड कहलाते हैं। व्यंजक में x. एम, एक्स भाग को अक्सर बाइंडर के रूप में जाना जाता है। मानो यह इशारा करते हुए कि चर X x से M के योग के साथ एक समूह बन जाते हैं। अन्य सभी अस्थिर को मुक्त कहा जाता है।
उदाहरण के लिए, व्यंजक में y. x x y, y - बाध्य अस्थाई, और x - मुक्त। और यह भी ध्यान देने योग्य है कि चर को इसके "निकटतम" अमूर्तता द्वारा समूहीकृत किया गया है। निम्नलिखित उदाहरण में, लैम्ब्डा कैलकुलस समाधान को x की एकल घटना द्वारा दर्शाया गया है, जो दूसरे पद से संबंधित है:
λ एक्स. वाई (λ एक्स। जेड एक्स)
मुक्त चर के सेट एम को एफवी (एम) के रूप में दर्शाया गया है और इसे शब्दों की संरचना पर रिकर्सन द्वारा परिभाषित किया गया है:
- FV (x)={x}, जहां x एक चर है।
- FV (λx. M)=FV (M) {x}।
- एफवी (एमएन)=एफवी (एम) ∪ एफवी (एन)।
ऐसे सूत्र जिसमें मुक्त चर नहीं होते हैं, बंद कहलाते हैं। क्लोज्ड लैम्ब्डा एक्सप्रेशन को कॉम्बिनेटर के रूप में भी जाना जाता है और कॉम्बिनेटरियल लॉजिक में शब्दों के बराबर हैं।
संक्षिप्त नाम
लैम्ब्डा के भावों का अर्थ इस बात से निर्धारित होता है कि उन्हें कैसे छोटा किया जा सकता है।
कटाई तीन प्रकार की होती है:
- α-रूपांतरण: बाध्य चर (अल्फा) बदलना।
- β-कमी: उनके तर्कों (बीटा) के लिए कार्य लागू करना।
- η-रूपांतरण: विस्तार की धारणा को शामिल करता है।
यहाँ भी हैहम परिणामी तुल्यता के बारे में बात कर रहे हैं: दो व्यंजक β-समतुल्य होते हैं यदि उन्हें एक ही घटक में β-रूपांतरित किया जा सकता है, और α / η-तुल्यता को समान रूप से परिभाषित किया जाता है।
रिड्यूसेबल टर्नओवर के लिए संक्षिप्त शब्द रेडेक्स, उप-विषयों को संदर्भित करता है जिसे नियमों में से एक द्वारा कम किया जा सकता है। डमी के लिए लैम्ब्डा कैलकुलस, उदाहरण:
(λ x. M) एन, एम में एक्स के साथ एन को प्रतिस्थापित करने के लिए अभिव्यक्ति में बीटा रेडेक्स है। जिस घटक को रेडेक्स कम करता है उसे रिडक्ट कहा जाता है। कमी (λ x. M) N, M है [x:=N]।
यदि M में x मुक्त नहीं है, तो x. एम एक्स रेगुलेटर एम के साथ एम-रेडेक्स भी।
α-परिवर्तन
अल्फा नाम आपको बाध्य चर के नाम बदलने की अनुमति देता है। उदाहरण के लिए, एक्स। x y दे सकता है। वाई केवल अल्फा रूपांतरण में भिन्न होने वाले शब्दों को α-समतुल्य कहा जाता है। अक्सर, लैम्ब्डा कैलकुलस का उपयोग करते समय, α-समकक्षों को पारस्परिक माना जाता है।
अल्फा रूपांतरण के लिए सटीक नियम पूरी तरह से तुच्छ नहीं हैं। सबसे पहले, इस एब्स्ट्रैक्शन के साथ, केवल उन्हीं वेरिएबल्स का नाम बदला जाता है जो एक ही सिस्टम से जुड़े होते हैं। उदाहरण के लिए, अल्फा ट्रांसफॉर्म λ x.λ x। x y.λ x तक ले जा सकता है। x, लेकिन इससे y.λx.y नहीं हो सकता है, बाद वाले का मूल अर्थ से भिन्न अर्थ है। यह चर छायांकन प्रोग्रामिंग की अवधारणा के अनुरूप है।
दूसरा, एक अल्फा ट्रांसफॉर्म संभव नहीं है अगर इसके परिणामस्वरूप एक गैर-स्थायी अन्य अमूर्तता द्वारा कब्जा कर लिया जाएगा। उदाहरण के लिए, यदि आप x.λ y में x को y से प्रतिस्थापित करते हैं। एक्स, तो आप प्राप्त कर सकते हैंy.λy. आप, जो बिल्कुल समान नहीं है।
स्थिर दायरे वाली प्रोग्रामिंग भाषाओं में, नाम समाधान को सरल बनाने के लिए अल्फा रूपांतरण का उपयोग किया जा सकता है। साथ ही, इस बात का ध्यान रखते हुए कि एक चर की अवधारणा युक्त क्षेत्र में पदनाम को मुखौटा नहीं बनाती है।
डी ब्रुने इंडेक्स नोटेशन में, कोई भी दो अल्फा-समतुल्य शब्द वाक्य-रचना की दृष्टि से समान हैं।
प्रतिस्थापन
ई द्वारा लिखे गए परिवर्तन [वी:=आर] वेरिएबल वी के सभी मुक्त घटनाओं को एक्सप्रेशन ई में टर्नओवर आर के साथ प्रतिस्थापित करने की प्रक्रिया है। λ के संदर्भ में प्रतिस्थापन को रिकर्सन के लैम्ब्डा द्वारा परिभाषित किया गया है अवधारणा संरचना पर कलन इस प्रकार है (नोट: x और y - केवल चर, और M और N - कोई -अभिव्यक्ति)।
x [एक्स:=एन] ≡ एन
y [x:=N] y अगर x y
(एम 1 एम 2) [एक्स:=एन] ≡ (एम 1 [एक्स:=एन]) (एम 2 [एक्स:=एन])
(λ x. M) [x:=N] x. M
(λ वाई.एम) [एक्स:=एन] वाई λ वाई। (एम [एक्स:=एन]) अगर एक्स ≠ वाई, बशर्ते कि वाई एफवी (एन)।
एक लैम्ब्डा एब्स्ट्रैक्शन में प्रतिस्थापन के लिए, कभी-कभी एक एक्सप्रेशन को α-transform करना आवश्यक होता है। उदाहरण के लिए, यह सच नहीं है कि (λ x. Y) [y:=x] का परिणाम (λ x. X) होता है क्योंकि प्रतिस्थापित x मुक्त होना चाहिए था, लेकिन अंत में बाध्य होना चाहिए था। इस मामले में सही प्रतिस्थापन (λ z. X) α-तुल्यता तक है। ध्यान दें कि प्रतिस्थापन विशिष्ट रूप से लैम्ब्डा तक परिभाषित है।
β-कमी
बीटा कमी किसी फ़ंक्शन को लागू करने के विचार को दर्शाती है। बीटा-रिडक्टिव को शब्दों में परिभाषित किया गया हैप्रतिस्थापन: ((एक्स वी। ई) ई ') ई है [वी:=ई']।
उदाहरण के लिए, कुछ एन्कोडिंग 2, 7, × मानते हुए, निम्नलिखित β-कमी है: ((λ n. N × 2) 7) → 7 × 2.
बीटा कमी को करी-हावर्ड समरूपता के माध्यम से प्राकृतिक कटौती के तहत स्थानीय रिड्यूसिबिलिटी की अवधारणा के समान देखा जा सकता है।
η-रूपांतरण
यह रूपांतरण विस्तार के विचार को व्यक्त करता है, जो इस संदर्भ में है कि दो कार्य समान होते हैं जब वे सभी तर्कों के लिए समान परिणाम देते हैं। यह रूपांतरण x के बीच आदान-प्रदान करता है। (F x) और f जब भी x f में मुक्त नहीं लगता है।
इस क्रिया को करी-हावर्ड समरूपता के माध्यम से प्राकृतिक कटौती में स्थानीय पूर्णता की अवधारणा के समान माना जा सकता है।
सामान्य रूप और संलयन
बिना टाइप किए गए लैम्ब्डा कैलकुलस के लिए, β-कमी नियम आम तौर पर न तो मजबूत होता है और न ही कमजोर सामान्यीकरण।
फिर भी, यह दिखाया जा सकता है कि α-रूपांतरण से पहले चलने पर β-कमी विलीन हो जाती है (यानी, दो सामान्य रूपों को समान माना जा सकता है यदि एक α-परिवर्तन एक से दूसरे में संभव है)।
इसलिए, दृढ़ता से सामान्य करने वाले शब्दों और कमजोर समायोजन वाले शब्दों दोनों का एक ही सामान्य रूप है। पहली शर्तों के लिए, किसी भी कमी की रणनीति को एक विशिष्ट कॉन्फ़िगरेशन में परिणाम की गारंटी दी जाती है। जबकि परिस्थितियों को कमजोर रूप से सामान्य करने के लिए, कुछ कमी रणनीतियों को यह नहीं मिल सकता है।
अतिरिक्त प्रोग्रामिंग तरीके
लैम्ब्डा कैलकुलस के लिए बहुत सारे सृजन मुहावरे हैं। उनमें से कई मूल रूप से एक प्रोग्रामिंग भाषा के शब्दार्थ के आधार के रूप में सिस्टम का उपयोग करने के संदर्भ में विकसित किए गए थे, उन्हें प्रभावी रूप से निम्न-स्तरीय निर्माण के रूप में लागू किया गया था। चूंकि कुछ शैलियों में एक लैम्ब्डा कैलकुस (या कुछ बहुत समान) एक स्निपेट के रूप में शामिल है, इसलिए इन तकनीकों को व्यावहारिक निर्माण में भी उपयोग किया जाता है, लेकिन फिर उन्हें अस्पष्ट या विदेशी माना जा सकता है।
नामित स्थिरांक
लैम्ब्डा कैलकुलस में, एक पुस्तकालय पहले से परिभाषित कार्यों के एक सेट का रूप लेता है, जहां शब्द केवल ठोस स्थिरांक होते हैं। शुद्ध कैलकुस में नामित अपरिवर्तनीय की कोई अवधारणा नहीं है क्योंकि सभी परमाणु लैम्ब्डा शब्द चर हैं। लेकिन शरीर में उस अस्थिर को बांधने के लिए लैम्ब्डा एब्स्ट्रैक्शन का उपयोग करके, और उस एब्स्ट्रैक्शन को इच्छित परिभाषा में लागू करने के लिए, परिवर्तनशील को स्थिरांक के नाम के रूप में ले कर उनकी नकल भी की जा सकती है। इसलिए यदि आप N में M का प्रतिनिधित्व करने के लिए f का उपयोग करते हैं, तो आप कह सकते हैं
(λ f. N) एम.
लेखक अक्सर एक वाक्यात्मक अवधारणा का परिचय देते हैं जैसे कि चीजों को अधिक सहज तरीके से लिखने की अनुमति दें।
f=M से N
ऐसी परिभाषाओं को जंजीर बनाकर, कोई लैम्ब्डा कैलकुलस "प्रोग्राम" को शून्य या अधिक फ़ंक्शन परिभाषाओं के रूप में लिख सकता है, जिसके बाद एक लैम्ब्डा सदस्य उन परिभाषाओं का उपयोग कर सकता है जो प्रोग्राम का बड़ा हिस्सा बनाते हैं।
इस let की एक उल्लेखनीय सीमा यह है कि f नाम M में परिभाषित नहीं है,चूंकि एम लैम्ब्डा एब्स्ट्रैक्शन एफ के बाध्यकारी दायरे से बाहर है। इसका मतलब है कि एक पुनरावर्ती फ़ंक्शन विशेषता का उपयोग M के साथ let के रूप में नहीं किया जा सकता है। अधिक उन्नत letrec सिंटैक्स, जो आपको इस शैली में पुनरावर्ती फ़ंक्शन परिभाषाएँ लिखने की अनुमति देता है, इसके बजाय निश्चित-बिंदु संयोजक का उपयोग करता है।
मुद्रित एनालॉग
यह प्रकार एक टाइप की गई औपचारिकता है जो एक अनाम फ़ंक्शन एब्स्ट्रैक्शन का प्रतिनिधित्व करने के लिए एक प्रतीक का उपयोग करता है। इस संदर्भ में, प्रकार आमतौर पर एक वाक्यात्मक प्रकृति की वस्तुएं होती हैं जिन्हें लैम्ब्डा शब्दों को सौंपा जाता है। सटीक प्रकृति प्रश्न में कलन पर निर्भर करती है। एक निश्चित दृष्टिकोण से, टाइप किए गए LI को बिना टाइप किए गए LI के शोधन के रूप में माना जा सकता है। लेकिन दूसरी ओर, उन्हें एक अधिक मौलिक सिद्धांत भी माना जा सकता है, और अनटाइप्ड लैम्ब्डा कैलकुलस केवल एक प्रकार के साथ एक विशेष मामला है।
टाइप्ड LI प्रोग्रामिंग लैंग्वेज की नींव है और ML और हास्केल जैसी कार्यात्मक भाषाओं की रीढ़ है। और, अधिक परोक्ष रूप से, सृजन की अनिवार्य शैलियाँ। टाइप लैम्ब्डा कैलकुली प्रोग्रामिंग भाषाओं के लिए टाइप सिस्टम के विकास में महत्वपूर्ण भूमिका निभाते हैं। यहां, टाइपेबिलिटी आमतौर पर प्रोग्राम के वांछित गुणों को कैप्चर करती है, उदाहरण के लिए, इससे मेमोरी एक्सेस उल्लंघन नहीं होगा।
टाइप किए गए लैम्ब्डा कैलकुली करी-हावर्ड आइसोमोर्फिज्म के माध्यम से गणितीय तर्क और प्रमाण सिद्धांत से निकटता से संबंधित हैं, और इसे श्रेणी वर्गों की आंतरिक भाषा के रूप में माना जा सकता है, उदाहरण के लिए, जोबस कार्टेशियन क्लोजर की शैली है।
