लैम्ब्डा कैलकुलस

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

लैम्ब्डा गणना (कैलकुलस) में लैम्ब्डा पद का निर्माण और उन पर कलन संक्रिया करना सम्मिलित है। लैम्ब्डा गणना के सबसे सामान्य रूप में, केवल निम्नलिखित नियमों का उपयोग करके पद बनाए जाते हैं:

• $x$ -चर, एक वर्ण या शृंखला एक पैरामीटर या गणितीय/तार्किक मान का प्रतिनिधित्व करता है।
• ${\textstyle (\lambda x.M)}$ – अमूर्तता, फलन परिभाषा (${\textstyle M}$ लैम्ब्डा शब्द है)। चर ${\textstyle x}$ व्यंजक में बंध जाता है।
• $(M\ N)$ - अनुप्रयोग, फलन ${\textstyle M}$ को एक तर्क पर प्रयुक्त करने के लिए${\textstyle N}$. ${\textstyle M}$ और ${\textstyle N}$ लैम्ब्डा शर्तें हैं।

न्यूनीकरण संक्रिया में सम्मिलित हैं:

• ${\textstyle (\lambda x.M[x])\rightarrow (\lambda y.M[y])}$ - α-रूपांतरण, व्यंजक में बद्ध चरों का नाम परिवर्तित करना। नाम संघट्‍टन से शून्यकरण के लिए उपयोग किया जाता है।
• ${\textstyle ((\lambda x.M)\ E)\rightarrow (M[x:=E])}$ - β-अवनति, अमूर्त के समूह में तर्क व्यंजक के साथ बद्ध चर को परिवर्तित करना।

यदि डी ब्रुइज़न अनुक्रमण का उपयोग किया जाता है, तो α-रूपांतरण की आवश्यकता नहीं है क्योंकि कोई नाम संघट्‍टन नहीं होगा। यदि न्यूनीकरण के चरणों का पुनरावृत्त प्रयोग अंततः समाप्त हो जाता है, तो चर्च-रॉसर प्रमेय द्वारा यह एक β-सामान्य रूप उत्पन्न करेगा।

एक सार्वभौमिक लैम्ब्डा फलन का उपयोग करते समय चर नामों की आवश्यकता नहीं होती है, जैसे कि आयोटा और बिन्दु, जो किसी भी फलन गतिविधि को विभिन्न संयोजनों में स्वयं कॉल करके बना सकता है।

स्पष्टीकरण और अनुप्रयोग

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

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

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

इतिहास

लैम्ब्डा गणना को गणितज्ञ अलोंजो चर्च द्वारा 1930 के दशक में गणित की नींव की जांच के एक भाग के रूप में प्रस्तुत किया गया था। मूल प्रणाली को 1935 में संगति के रूप में दिखाया गया था जब स्टीफन क्लेन और जे.बी. रोसेर ने क्लेन-रोसेर विरोधाभास विकसित किया था।

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

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

लैम्ब्डा प्रतीक की उत्पत्ति

चर्च द्वारा ग्रीक अक्षर लैम्ब्डा (λ) के उपयोग के कारण पर कुछ अनिश्चितता है क्योंकि लैम्ब्डा कैलकुस (गणना) में फलन-अमूर्तता के लिए अंकन संभव्यता चर्च द्वारा विरोधाभास स्पष्टीकरण के कारण हो सकता है। कार्डोन और हिंडले (2006) के अनुसार:

हालांकि, चर्च ने "λ" संकेतन क्यों चयन किया? [1964 में हेराल्ड डिक्सन को एक अप्रकाशित पत्र] में उन्होंने स्पष्ट रूप से कहा कि यह व्हाइटहेड और रसेल द्वारा वर्ग-अमूर्तता के लिए उपयोग किए जाने वाले "${\hat {x}}$" अंकन से आया है। "${\hat {x}}$" को पहले "$\land x$" को संशोधित करके वर्ग-अमूर्तता से फलन-अमूर्तता को अलग करने के लिए, ''$\land$'' को " से "λ" मे परिवर्तित किया जाता है।

इस उत्पत्ति को [रोसर, 1984, पृष्ठ 338] में भी बताया गया था। दूसरी ओर, अपने बाद के वर्षों में चर्च ने दो जांचकर्ताओं को बताया कि चयन अधिक आकस्मिक था: एक प्रतीक की आवश्यकता थी और λ चयन किया गया।

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

प्रिय प्रोफेसर चर्च,

रसेल के पास आईओटा संक्रियक था, हिल्बर्ट के पास एप्सिलॉन संक्रियक था। आपने अपने संक्रियक के लिए लैम्ब्डा क्यों चुना?

स्कॉट के अनुसार, चर्च की पूरी प्रतिक्रिया में पोस्टकार्ड को निम्नलिखित टिप्पणी "एनी, मीनी, मिनी, मो" के साथ वापस करना सम्मिलित था।

अनौपचारिक विवरण

कारण

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

$\operatorname {square\_sum} (x,y)=x^{2}+y^{2}$

के रूप में अस्पष्ट रूप में पुनः लिखा जा सकता है

$(x,y)\mapsto x^{2}+y^{2}$

(जिसे टपल के रूप में पढ़ा जाता है x और y मानचित्रित है ${\textstyle x^{2}+y^{2}}$) इसी प्रकार, फलन

$\operatorname {id} (x)=x$

के रूप में अस्पष्ट रूप में पुनः लिखा जा सकता है

$x\mapsto x$

जहां इनपुट को केवल उसी के लिए प्रतिचित्र किया जाता है।

दूसरा सरलीकरण यह है कि लैम्ब्डा गणना केवल एक इनपुट के फलनों का उपयोग करता है। एक सामान्य फलन जिसमें दो इनपुट की आवश्यकता होती है, उदाहरण के लिए ${\textstyle \operatorname {square\_sum} }$ फलन, एक समतुल्य फलन में पुनः काम किया जा सकता है जो एकल इनपुट को स्वीकार करता है, और आउटपुट के रूप में एक और फलन देता है, जो बदले में एकल इनपुट स्वीकार करता है। उदाहरण के लिए,

$(x,y)\mapsto x^{2}+y^{2}$

में पुन: फलन किया जा सकता है

$x\mapsto (y\mapsto x^{2}+y^{2})$

यह विधि, जिसे विच्छेदन के रूप में जाना जाता है, एक ऐसे फलन (फलन) को रूपांतरित करती है जो एक तर्क के साथ प्रत्येक फलन की श्रृंखला में कई तर्कों को लेता है।

कार्यात्मक अनुप्रयोग ${\textstyle \operatorname {square\_sum} }$ तर्कों के लिए फलन (5, 2), एक बार में प्राप्त होता है

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\textstyle =29}$,

जबकि विच्छेदन संस्करण के मूल्यांकन के लिए एक और चरण की आवश्यकता है

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$ // आंतरिक व्यंजक में 5 के साथ x की परिभाषा का प्रयोग किया गया है। यह β-अवनति जैसा है।

${\textstyle =5^{2}+2^{2}}$ // की परिभाषा $y$ का प्रयोग $2$ के साथ किया जाता है पुनः, β-अवनति के समान।

${\textstyle =29}$

समान परिणाम पर पहुंचने के लिए।

लैम्ब्डा गणना

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

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

लैम्ब्डा शर्तें

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

निम्नलिखित तीन नियम एक आगमनात्मक परिभाषा देते हैं जिसे सभी वाक्यगत रूप से मान्य लैम्ब्डा पदों के निर्माण के लिए प्रयुक्त किया जा सकता है:

• चर x अपने आप में एक वैध लैम्ब्डा पद है।
• यदि t एक लैम्ब्डा पद है, और x एक चर है, तो $(\lambda x.t)$ एक लैम्ब्डा पद है (जिसे अमूर्त कहा जाता है);
• यदि t और s लैम्ब्डा पद हैं, फिर $(t$  $s)$ एक लैम्ब्डा पद है (जिसे अनुप्रयोग कहा जाता है)।

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

अमूर्तता $\lambda x.t$ § अज्ञात फलन को दर्शाता है जो एकल इनपुट x लेता है और t देता है। उदाहरण के लिए, $\lambda x.x^{2}+2$ फलन के लिए एक अमूर्तता है $f(x)=x^{2}+2$ शब्द का उपयोग करके $x^{2}+2$ के लिए t नाम $f(x)$ अमूर्तता का उपयोग करते समय अनावश्यक है। $(\lambda x.t)$ चर x पद t मे परिबद्ध करता है। अमूर्त के साथ एक फलन की परिभाषा केवल फलन को स्थापित करती है, लेकिन इसे प्रयुक्त नहीं करती है।

अनुप्रयोग $t$ इनपुट $s$ के लिए फलन के अनुप्रयोग का प्रतिनिधित्व करता है अर्थात $t(s)$ उत्पन्न करने के लिए इनपुट s पर फलन t को कॉल करने के लिए फलन का प्रतिनिधित्व करता है।

परिवर्तनीय घोषणा के लैम्ब्डा गणना में कोई अवधारणा नहीं है। एक परिभाषा में जैसे $\lambda x.x+y$ (अर्थात $f(x)=x+y$), लैम्ब्डा गणना में y एक चर है जिसे अभी तक परिभाषित नहीं किया गया है। अमूर्त $\lambda x.x+y$ सिमेन्टिक रूप से मान्य है, और एक ऐसे फलन का प्रतिनिधित्व करता है जो y इनपुट को अभी तक अज्ञात में जोड़ता है।

कोष्ठक का उपयोग किया जा सकता है और शर्तों को स्पष्ट करने के लिए इसकी आवश्यकता हो सकती है। उदाहरण के लिए,

1. $\lambda x.((\lambda x.x)x)$ जो $\lambda x.B$ के प्रारूप मे है- एक अमूर्त, और
2. $((\lambda x.x)x)$ जो $MN$ के प्रारूप मे है- अनुप्रयोग। उदाहरण 1 और 2 अलग-अलग पदों को दर्शाते हैं; हालाँकि उदाहरण 1 एक फलन परिभाषा है, जबकि उदाहरण 2 अनुप्रयोग है।

यहाँ, उदाहरण 1 एक फलन को परिभाषित करता है $\lambda x.B$, जहां $B$ है $((\lambda x.x)x)$, अनुप्रयोग करने का परिणाम $(\lambda x.x)$ x के लिए, जबकि उदाहरण 2 $MN$ है; $M$ लैम्ब्डा पद $(\lambda x.x)$ है। इनपुट N पर प्रयुक्त किया जाना चाहिए। उदाहरण 1 और 2 सर्वसमिका फलन $\lambda x.x$ का मूल्यांकन करेंगे।

फलन जो फलन पर प्रवर्तित करते

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

उदाहरण के लिए, $\lambda x.x$ सर्वसमिका फलन का प्रतिनिधित्व करता है, $x\mapsto x$, और $(\lambda x.x)y$ प्रयुक्त किए गए $y$ सर्वसमिका फलन का प्रतिनिधित्व करता है इसके अतिरिक्त $(\lambda x.y)$ स्थिर फलन का प्रतिनिधित्व करता है $x\mapsto y$, वह फलन जो सदैव $y$ देता है, फिर इनपुट कोई भी हो। लैम्ब्डा गणना में, फलन अनुप्रयोग को बायाँ साहचर्य के रूप में माना जाता है, ताकि $stx$ का तात्पर्य $(st)x$ हो।

समतुल्यता और अवनति की कई धारणाएँ हैं जो लैम्ब्डा पदों को समतुल्य लैम्ब्डा पदों में कम करने की स्वीकृति देती हैं।

अल्फा समानता

समानता का एक मूल रूप, जिसे लैम्ब्डा पदों पर परिभाषित किया जा सकता है, अल्फा समानता है। यह अंतर्ज्ञान को प्रग्रहण है कि एक बाध्य चर का विशेष विकल्प, एक अमूर्तता में, (सामान्य रूप से) कोई अंतर नहीं है। उदाहरण के लिए, $\lambda x.x$ और $\lambda y.y$ अल्फा-समतुल्य लैम्ब्डा पद हैं, और वे दोनों एक ही फलन (सर्वसमिका फलन) का प्रतिनिधित्व करते हैं। शर्तें $x$ और $y$ अल्फा-समतुल्य नहीं हैं, क्योंकि वे एक अमूर्तता में परिबद्ध नहीं हैं। कई प्रस्तुतियों में, अल्फा-समतुल्य लैम्ब्डा पदों की सर्वसमिका करना सामान्य है।

β-अवनति को परिभाषित करने में सक्षम होने के लिए निम्नलिखित परिभाषाएँ आवश्यक हैं:

मुक्त चर

मुक्त चर एक पद के वे चर हैं जो एक अमूर्तता से परिबद्ध नहीं हैं। किसी व्यंजक के मुक्त चरों के समुच्चय को आगमनात्मक रूप से परिभाषित किया जाता है:

• $x$ के मुक्त चर सिर्फ $x$
• $\lambda x.t$ के मुक्त चर का समुच्चय सिद्धांत के $t$ मुक्त चरों का समुच्चय है, लेकिन $x$ को दिया गया
• $t$ $s$ के मुक्त चर का समुच्चय सिद्धांत $t$ के मुक्त चरों के समुच्चय है और $s$ के मुक्त चर का समुच्चय का संयोजन है।

उदाहरण के लिए, सर्वसमिका का प्रतिनिधित्व करने वाला लैम्ब्डा पद $\lambda x.x$ कोई मुक्त चर नहीं है, लेकिन फलन $\lambda x.y$ $x$ एक मुक्त चर $y$ है।

प्रग्रहण-परिहरण प्रतिस्थापन

एक मुक्त चर के प्रग्रहण से शून्यकरण के लिए चर में एक व्यवस्थित परिवर्तन एक कार्यात्मक प्रोग्रामिंग भाषा में त्रुटि का परिचय दे सकता है, जहां फलन प्रथम श्रेणी के स्थानिक हैं।

मान लीजिए $t$, $s$ और $r$ लैम्ब्डा पद हैं और $x$ और $y$ चर हैं। अंकन $t[x:=r]$ का प्रतिस्थापन दर्शाता है $r$ के लिए $x$ में $t$ प्रग्रहण से शून्यकरण के तरीके में। इसे इस प्रकार परिभाषित किया गया है:

• $x[x:=r]=r$; $r$ के स्थान पर $x$ सिर्फ $r$ है,
• $y[x:=r]=y$ यदि $x\neq y$; $r$इसके लिए प्रतिस्थापित $y$ गतिविधि करते समय $x$ सिर्फ $y$ है,
• $(t$ $s)[x:=r]=(t[x:=r])(s[x:=r])$; प्रतिस्थापन चर के आगे के अनुप्रयोग के लिए वितरित करता है
• $(\lambda x.t)[x:=r]=\lambda x.t$; $r$ यद्यपि $x$ पर प्रतिचित्रित किया गया है, बाद मे सभी $x$ को $t$ लैम्ब्डा फलन $(\lambda x.t)$ नहीं बदलेगा
• $(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])$ यदि $x\neq y$ और $y$ $r$ के मुक्त चरों में नहीं है $y$ चर $r$ के लिए भिन्न कहा जाता है।

उदाहरण के लिए, $(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x$, और $((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y$

नवीनता की स्थिति (उसकी आवश्यकता है $y$ का मुक्त और बाध्य चर $r$ है) यह सुनिश्चित करने के लिए महत्वपूर्ण है कि प्रतिस्थापन फलनों के अर्थ को नहीं बदलता है। उदाहरण के लिए, एक प्रतिस्थापन जो नवीनता की स्थिति को अनदेखा करता है, त्रुटियों का कारण बन सकता है: $(\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x$ यह प्रतिस्थापन स्थिर फलन $\lambda x.y$ सर्वसमिका में $\lambda x.x$ प्रतिस्थापन द्वारा को परिवर्तित कर देता है।

सामान्य रूप से, नवीनता की स्थिति को पूरा करने में विफलता को उपयुक्त नए चर के साथ अल्फा-नाम द्वारा संशोधित किया जा सकता है। उदाहरण के लिए, प्रतिस्थापन की हमारी सही धारणा पर वापस स्विच करने, में $(\lambda x.y)[y:=x]$ अमूर्त का नाम बदलकर एक नए चर के साथ किया जा सकता है $z$, प्राप्त करने के लिए $(\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x$, और फलन का अर्थ प्रतिस्थापन द्वारा संरक्षित किया जा सकता है।

β-अवनति

β-अवनति नियम कहा गया है कि प्रारूप का अनुप्रयोग $(\lambda x.t)s$ अवधि तक कम कर देता है $t[x:=s]$ संकेत $(\lambda x.t)s\to t[x:=s]$ इंगित करने के लिए प्रयोग किया जाता है $(\lambda x.t)s$ β-कम होकर $t[x:=s]$ हो जाता है उदाहरण के लिए, प्रत्येक के लिए $s$, $(\lambda x.x)s\to x[x:=s]=s$ यह दर्शाता है कि $\lambda x.x$ वास्तव में सर्वसमिका है। इसी प्रकार, $(\lambda x.y)s\to y[x:=s]=y$, जो यह दर्शाता है $\lambda x.y$ एक स्थिर फलन है।

लैम्ब्डा गणना को कार्यात्मक प्रोग्रामिंग भाषा के आदर्श संस्करण के रूप में देखा जा सकता है, जैसे हास्केल (प्रोग्रामिंग भाषा) या मानक एमएल इस दृष्टि के अंतर्गत, β-अवनति एक संगणनात्मक चरण से अनुरूप है। इस चरण को अतिरिक्त β-अवनति द्वारा दोहराया जा सकता है जब तक कि कम करने के लिए कोई और अनुप्रयोग नहीं बचा है। अनटाइप्ड लैम्ब्डा कलन में, जैसा कि यहाँ प्रस्तुत किया गया है, यह कमी प्रक्रिया समाप्त नहीं हो सकती है। इंस्टेंस के लिए, पद $\Omega =(\lambda x.xx)(\lambda x.xx)$ यहाँ $(\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)$पर विचार करें, यह शब्द एक β-अवनति में स्वयं को कम कर देता है, और इसलिए कमी की प्रक्रिया कभी समाप्त नहीं होगी।

अनटाइप्ड लैम्ब्डा गणना का एक अन्य स्वरूप यह है कि यह विभिन्न प्रकार के डेटा के बीच अंतर नहीं करता है। इंस्टेंस के लिए, एक ऐसा फलन लिखना वांछनीय हो सकता है जो केवल संख्याओं पर फलन करता हो। हालांकि, अनटाइप्ड लैम्ब्डा गणना में, किसी फलन को सत्य मानों, शृंखला या अन्य गैर-संख्या वस्तुओं पर प्रयुक्त होने से रोकने का कोई तरीका नहीं है।

औपचारिक परिभाषा

Main article: लैम्ब्डा कैलकुस परिभाषा

परिभाषा

लैम्ब्डा व्यंजक से बना है:

• चर v₁, v₂, ...;
• अमूर्त प्रतीक λ (लैम्ब्डा) और . (डॉट);
• कोष्ठक ()

लैम्ब्डा व्यंजक का समुच्चय, Λ, पुनरावर्ती परिभाषा हो सकती है:

1. यदि x एक चर है, तो x ∈ Λ.
2. यदि x एक चर है और M ∈ Λ, तब (λx.M) ∈ Λ.
3. यदि M, N ∈ Λ, तब (M N) ∈ Λ.

नियम 2 के उदाहरणों को अमूर्तता के रूप में जाना जाता है और नियम 3 के उदाहरणों को अनुप्रयोग के रूप में जाना जाता है।

संकेत पद्धति

लैम्ब्डा व्यंजक के अंकन को सुव्यवस्थित रखने के लिए, सामान्य रूप से निम्नलिखित समागम प्रयुक्त की जाती हैं:

• सबसे बाहरी कोष्ठक हटा दिए जाते हैं: (M N) के अतिरिक्त M N।
• अनुप्रयोगों को साहचर्य छोड़ दिया जाता है: ((M N) P) के अतिरिक्त MNP लिखा जा सकता है।
• जब सभी चर एकल-अक्षर वाले हों, तो अनुप्रयोगों में स्थान छोड़ा जा सकता है: MNP के अतिरिक्त M N P है।
• एक अमूर्त का समूह नियमित व्यंजक का विस्तार करता है: λx.M N का अर्थ है λx.(M N) और नहीं (λx.M) N है।
• अमूर्तता का एक क्रम संकुचित होता है: λx.λy.λz.N को λxyz.N के रूप में संक्षिप्त किया गया है।

मुक्त और बाध्य चर

अमूर्तता संक्रियक, λ, अमूर्तता के समूह में जहां कहीं भी होता है, उसके चर को परिबद्ध करने के लिए कहा जाता है। अमूर्तता के विस्तार में आने वाले चर को सीमित कहा जाता है। एक व्यंजक λx.M में, भाग λx को प्रायः योजक कहा जाता है, एक संकेत के रूप में कि चर x, λx को M से जोड़कर बाध्य हो रहा है। अन्य सभी चर मुक्त कहलाते हैं। उदाहरण के लिए, व्यंजक λy.x x y में, y एक बाध्य चर है और x एक मुक्त चर है। साथ ही एक चर अपने निकटतम अमूर्तता से परिबद्ध होता है। निम्नलिखित उदाहरण में व्यंजक में x की एकल घटना दूसरे लैम्ब्डा से λx.y (λx.z x) परिबद्ध है।

एक लैम्ब्डा व्यंजक, M के मुक्त चर का समुच्चय, FV(M) के रूप में दर्शाया गया है और पदों की संरचना पर पुनरावर्तन द्वारा परिभाषित किया गया है:

1. FV(x) = {x}, जहाँ x एक चर है।
2. FV (λx.M) = FV(M) \ {x}।
3. FV(M N) = FV(M) ∪ FV(N).

एक व्यंजक जिसमें कोई मुक्त चर नहीं होता है, उसे संवृत्त कहा जाता है। संवृत्त लैम्ब्डा व्यंजक को साहचर्य के रूप में भी जाना जाता है और संयोजन तर्क में पदों के समान है।

अवनति

लैम्ब्डा व्यंजक का अर्थ इस बात से परिभाषित होता है कि व्यंजक को कैसे कम किया जा सकता है।

न्यूनीकरण तीन प्रकार की होती है:

• α- रूपांतरण: बाध्य चर परिवर्तित करना;
• β-न्यूनीकरण: फलन को उनके तर्कों पर प्रयुक्त करना;
• η-न्यूनीकरण: जो विस्तार की धारणा को दर्शाता है।

हम परिणामी तुल्यताओं के बारे में भी बात करते हैं: दो व्यंजक α-समतुल्य हैं, यदि उन्हें α-एक ही व्यंजक में परिवर्तित किया जा सकता है। β-समानता और η-समानता को इसी तरह परिभाषित किया गया है।

रेडेक्स पद, लघुकरणीय व्यंजक के लिए छोटा है, उपश्रेणी को संदर्भित करता है जिसे अवनति नियमों में से एक द्वारा कम किया जा सकता है। उदाहरण के लिए, (λx.M) N, M में x के लिए N के प्रतिस्थापन को व्यक्त करने में एक β-रेडेक्स है। एक रेडेक्स जिस व्यंजक को कम करता है उसे उसका अवनति कहा जाता है; (λx.M) N का न्यूनीकरण M[x := N] है।

यदि x, M में मुक्त नहीं है, λx.M x भी एक η-रेडेक्स है, जिसमें M की कमी है।

α-रूपांतरण

α-रूपांतरण, जिसे कभी-कभी α-नाम परिवर्तित करने के रूप में जाना जाता है, बाध्य चर नामों को परिवर्तित करने की स्वीकृति देता है। उदाहरण के लिए, λx.x का α-रूपांतरण λy.y उत्पन्न कर सकता है। वे पद जो केवल α-रूपांतरण से भिन्न होते हैं, α-समतुल्य कहलाते हैं। प्रायः, लैम्ब्डा गणना के उपयोग में, α-समतुल्य पदों को समतुल्य माना जाता है।

α-रूपांतरण के परिशुद्ध नियम पूरी तरह से साधारण नहीं हैं। सबसे पहले, जब α-एक अमूर्तता को परिवर्तित करते हैं, केवल चर घटनाएँ जिनका नाम बदला जाता है, वे हैं जो एक ही अमूर्तता के लिए बाध्य हैं। उदाहरण के लिए, λx.λx.x के α-रूपांतरण का परिणाम λy.λx.x हो सकता है, लेकिन इसका परिणाम λy.λx.y नहीं हो सकता है। उत्तरार्द्ध का मूल से अलग अर्थ है। यह चर छायाकरण की प्रोग्रामिंग धारणा के अनुरूप है।

दूसरा, α-रूपांतरण संभव नहीं है यदि इसके परिणामस्वरूप एक भिन्न अमूर्तता द्वारा एक चर पर प्रग्रहण कर लिया जाएगा। उदाहरण के लिए, यदि हम λx.λy.x में x को y से प्रतिस्थापित करते हैं, तो हमें λy.λy.y मिलता है, जो बहुत समान नहीं है।

प्रोग्रामिंग भाषाओं में स्थिर सीमा के साथ, α-रूपांतरण का उपयोग नाम विभेदन (प्रोग्रामिंग भाषा) को सामान्य बनाने के लिए किया जा सकता है, यह सुनिश्चित करके कि कोई चर नाम किसी नाम को विस्तार (प्रोग्रामिंग) में नहीं रखता है ( विभेदन को सामान्य बनाने के लिए के लिए α-नामकरण देखें)।

डी ब्रुइज़न इंडेक्स संकेतन में, कोई भी दो α-समतुल्य पद रचना दृष्टि से समान हैं।

प्रतिस्थापन

प्रतिस्थापन, लिखित M[x:= N], व्यंजक N के साथ व्यंजक M में चर x की सभी मुक्त उपस्थिति को परिवर्तित करने की प्रक्रिया है। लैम्ब्डा गणना की शर्तों पर प्रतिस्थापन को पदों की संरचना पर पुनरावर्तन द्वारा परिभाषित किया गया है, निम्नानुसार (ध्यान दें: x और y केवल चर हैं जबकि M और N कोई लैम्ब्डा व्यंजक हैं):

x[x := N] = N

y[x := N] = y, if x ≠ y

(M₁ M₂)[x := N] = M₁[x := N] M₂[x := N]

(λx.M)[x := N] = λx.M

(λy.M)[x := N] = λy.(M[x := N]), if x ≠ y and y ∉ FV(N) FV के लिए ऊपर देखें

एक अमूर्त में स्थानापन्न करने के लिए, कभी-कभी व्यंजक को α-रूपांतरित करना आवश्यक होता है। उदाहरण के लिए, यह (λx.y)[y := x] के लिए λx.x में परिणाम के लिए सही नहीं है, क्योंकि प्रतिस्थापित x मुक्त होना चाहिए था लेकिन बाध्य होने के कारण समाप्त हो गया। इस स्थिति में सही प्रतिस्थापन λz.x है, α-समानता तक है। प्रतिस्थापन को विशिष्ट रूप से α-समानता तक परिभाषित किया गया है।

β-न्यूनीकरण

β-अवनति फलन अनुप्रयोग के विचार को प्रग्रहण करती है। β-न्यूनीकरण को प्रतिस्थापन के संदर्भ में परिभाषित किया गया है: β-न्यूनीकरण (λx.M) N, M[x := N] है।

उदाहरण के लिए, 2, 7, × के कुछ एन्कोडिंग को मानते हुए, हमारे पास निम्न β-अवनति (λn.n × 2) 7 → 7 × 2 है।

β-न्यूनीकरण को करी-हावर्ड समरूपता के माध्यम से प्राकृतिक अवनति में स्थानीय न्यूनीकरण की अवधारणा के समान देखा जा सकता है।

η-न्यूनीकरण

η-न्यूनीकरण विस्तार के विचार को व्यक्त करता है, जो इस संदर्भ में है कि दो फलन समान हैं यदि और केवल यदि वे सभी तर्कों के लिए समान परिणाम देते हैं। η-अवनति λx.f x और f के बीच परिवर्तित होती है जब भी x f में मुक्त दिखाई नहीं देता है।

η-न्यूनीकरण को करी-हावर्ड समरूपता के माध्यम से प्राकृतिक अवनति में स्थानीय पूर्णता की अवधारणा के समान देखा जा सकता है।

सामान्य रूप और मेल

Main article: सामान्यीकरण गुण (अमूर्त पुनर्लेखन)

अनटाइप्ड लैम्ब्डा गणना के लिए, पुनर्लेखन प्रणाली के रूप में β-अवनति न तो दृढ़ता से सामान्यीकरण कर रही है और न ही दुर्बल रूप से सामान्यीकरण कर रही है।

हालांकि, यह दिखाया जा सकता है कि α-रूपांतरण तक काम करते समय β-अवनति मेल (अमूर्त पुनर्लेखन) है (अर्थात हम दो सामान्य रूपों को बराबर मानते हैं यदि α-एक को दूसरे में परिवर्तित करना संभव है)।

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

एन्कोडिंग डेटा प्रारूप

Main article: चर्च एन्कोडिंग और मोगेंसेन-स्कॉट एन्कोडिंग

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

लैम्ब्डा गणना में अंकगणित

लैम्ब्डा गणना में प्राकृतिक संख्याओं को परिभाषित करने के कई संभावित तरीके हैं, लेकिन अब तक सबसे सामान्य चर्च अंक हैं, जिन्हें निम्नानुसार परिभाषित किया जा सकता है:

0 := λf.λx.x

1 := λf.λx.f x

2 := λf.λx.f (f x)

3 := λf.λx.f (f (f x))

और इसीलिए संकेतन में ऊपर प्रस्तुत वैकल्पिक सिंटैक्स का उपयोग करना:

0 := λfx.x

1 := λfx.f x

2 := λfx.f (f x)

3 := λfx.f (f (f x))

एक चर्च अंक एक उच्च-क्रम फलन है यह एक एकल-तर्क फलन f लेता है, और एक और एकल-तर्क फलन देता है। चर्च अंक n एक फलन(फ़ंक्शन) है जो एक फलन f को तर्क के रूप में लेता है और f की nवे रचना को प्रतिवर्ती करता है, अर्थात फलन f जो स्वयं n बार से बना होता है। यह f⁽ⁿ⁾ को निरूपित किया गया है और वास्तव में f की n-वे पावर है (एक संक्रिया के रूप में माना जाता है); f⁽⁰⁾ को पहचान फलन के रूप में परिभाषित किया गया है। इस तरह की दोहराई गई रचनाएँ (एकल फलन f की) घातांक के नियमों का अनुसरण करती हैं, यही वजह है कि इन अंकों का उपयोग अंकगणित के लिए किया जा सकता है। (चर्च के मूल लैम्ब्डा गणना में, एक लैम्ब्डा व्यंजक के औपचारिक पैरामीटर को फलन समूह में कम से कम एक बार होने की आवश्यकता थी, जिसने 0 की उपरोक्त परिभाषा को असंभव बना दिया।)

चर्च अंक के बारे में सोचने का एक तरीका n, जो क्रमानुदेश का विश्लेषण करते समय प्रायः उपयोगी होता है, एक निर्देश 'n बार दोहराएं' के रूप में होता है। उदाहरण के लिए, का उपयोग करना PAIR और NIL नीचे परिभाषित फ़ंक्शंस, एक ऐसे फलन को परिभाषित कर सकता है जो n तत्वों की एक (लिंक्ड) सूची बनाता है जो सभी x के बराबर है, एक रिक्त सूची से प्रारंभ करते हुए 'एक और x तत्व को आगे बढ़ाएं' n बार दोहराता है। लैम्ब्डा पद है

λn.λx.n (PAIR x) NIL

जो दोहराया जा रहा है उसे अलग करके, और जिस तर्क को दोहराया जा रहा है उसे अलग-अलग करके, कई अलग-अलग प्रभावों को प्राप्त किया जा सकता है।

हम एक अनुक्रमिक फलन को परिभाषित कर सकते हैं, जो एक चर्च अंक n लेता है f का एक और अनुप्रयोग जोड़कर n + 1 और प्रतिवर्ती करता है,, जहां '(mf)x' का अर्थ है 'f' फलन 'x' पर 'm' बार प्रयुक्त होता है:

SUCC := λn.λf.λx.f (n f x)

क्योंकि m-वीं रचना f के साथ n-वीं रचना f देता है m+n-वीं रचना f, जोड़ को निम्नानुसार परिभाषित किया जा सकता है:

PLUS := λm.λn.λf.λx.m f (n f x)

PLUS दो प्राकृतिक संख्याओं को तर्क के रूप में लेने और एक प्राकृतिक संख्या वापस करने के फलन के रूप में विचार किया जा सकता है; यह सत्यापित किया जा सकता है

PLUS 2 3

और

5

β-समतुल्य लैम्ब्डा व्यंजक हैं। जोड़ने के बाद से m एक संख्या के लिए n 1 जोड़कर पूरा किया जा सकता है m बार, एक वैकल्पिक परिभाषा है:

PLUS := λm.λn.m SUCC n 

इसी प्रकार, गुणा को परिभाषित किया जा सकता है

MULT := λm.λn.λf.m (n f)वैकल्पिक

MULT := λm.λn.m (PLUS n) 0

गुणा करने के बाद से m और n जोड़ने को पुनरावर्ती के समान है n फलन m बार और फिर इसे शून्य पर प्रयुक्त करना। घातांक का चर्च अंकों में सामान्य प्रतिपादन है, अर्थात्

POW := λb.λe.e b द्वारा परिभाषित पूर्ववर्ती फलन PRED n = n − 1 एक सकारात्मक पूर्णांक के लिए n और PRED 0 = 0 अपेक्षाकृत अधिक कठिन है। सूत्र

PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

आगमनात्मक रूप से दिखा कर मान्य किया जा सकता है कि यदि T दर्शाता है (λg.λh.h (g f)), तब T⁽ⁿ⁾(λu.x) = (λh.h(f⁽ⁿ⁻¹⁾(x))) के लिए n > 0. की दो अन्य परिभाषाएँ PRED नीचे दिए गए हैं, एक तर्क और दूसरा जोड़ों का उपयोग कर रहा है। पूर्ववर्ती फलन के साथ, व्यवकलन प्रत्यक्ष है। परिभाषित

SUB := λm.λn.n PRED m,

SUB m n प्राप्त m − n जब m > n और 0 अन्यथा।

तर्क और निर्धारक

संकेत के अनुसार, निम्नलिखित दो परिभाषाओं (चर्च बूलियन्स के रूप में जाना जाता है) का उपयोग बूलियन मूल्यों के लिए किया जाता है TRUE और FALSE:

TRUE := λx.λy.x

FALSE := λx.λy.y

फिर, इन दो लैम्ब्डा पदों के साथ, हम कुछ तार्किक संक्रिया को परिभाषित कर सकते हैं (ये केवल संभव सूत्रीकरण हैं; अन्य व्यंजक समान रूप से सही हैं):

AND := λp.λq.p q p

OR := λp.λq.p p q

NOT := λp.p FALSE TRUE

IFTHENELSE := λp.λa.λb.p a b

अब हम कुछ तार्किक फलनों की गणना करने में सक्षम हैं, उदाहरण के लिए:

AND TRUE FALSE

≡ (λp.λq.p q p) TRUE FALSE →_β TRUE FALSE TRUE

≡ (λx.λy.x) FALSE TRUE →_β FALSE

और हम देखते हैं AND TRUE FALSE के बराबर है FALSE.

एक निर्धारक एक ऐसा फलन है जो एक बूलियन मान वापस करता है। सबसे मौलिक निर्धारक ISZERO है जो TRUE प्रतिवर्ती है यदि इसका तर्क चर्च अंक 0 है और FALSE यदि इसका तर्क कोई अन्य चर्च अंक है:

ISZERO := λn.n (λx.FALSE) TRUE

निम्नलिखित निर्धारक परीक्षण करता है कि क्या पहला तर्क दूसरे से कम-से-या-बराबर है:

LEQ := λm.λn.ISZERO (SUB m n),

और m = n, यदि LEQ m n और LEQ n m, संख्यात्मक समानता के लिए एक निर्धारक का निर्माण करना प्रत्यक्ष है।

निर्धारक की उपलब्धता और की उपरोक्त परिभाषा TRUE और FALSE लैम्ब्डा गणना में if-then-else पद लिखना सुविधाजनक बनाएं। उदाहरण के लिए, पूर्ववर्ती फलन को इस प्रकार परिभाषित किया जा सकता है:

PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0

जिसे आगमनात्मक रूप से दिखा कर सत्यापित किया जा सकता है n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) जोड़ n -1 के लिए फलन n > 0 है।

युग्म

एक युग्म (2-ट्यूपल) TRUE और FALSE, युग्म के लिए चर्च कोडिंग का उपयोग करके संदर्भ में परिभाषित किया जा सकता है। उदाहरण के लिए, PAIR एनकैप्सुलेट (x,y), FIRST जोड़ी का पहला तत्व देता है, और SECOND प्रतिफल देते है।

PAIR := λx.λy.λf.f x y

FIRST := λp.p TRUE

SECOND := λp.p FALSE

NIL := λx.TRUE

NULL := λp.p (λx.λy.FALSE)

एक लिंक की गई सूची को रिक्त सूची के लिए या तो NIL शून्य के रूप में परिभाषित किया जा सकता है, या PAIR और एक छोटी सूची के रूप में परिभाषित किया जा सकता है। निर्धारक NULL मूल्य के लिए NIL परीक्षण करता है। (वैकल्पिक रूप से, NIL := FALSE के साथ निर्माण l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil) स्पष्ट NULL परीक्षण की आवश्यकता को कम करता है)।

युग्म के उपयोग के एक उदाहरण के रूप में, शिफ्ट-एंड-इन्क्रीमेंट फंक्शन जो चित्रित (m, n) को (n, n + 1) के रूप में परिभाषित किया जा सकता है

Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))

जो हमें पूर्ववर्ती फलन का संभव्यता सबसे पारदर्शी संस्करण देने की स्वीकृति देता है:

PRED := λn.FIRST (n Φ (PAIR 0 0)).

अतिरिक्त प्रोग्रामिंग तकनीकें

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

नामित नियतांक

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

(λf.M) N

लेखक प्रायः उपरोक्त को अधिक सामान्य क्रम में लिखने की स्वीकृति देने के लिए सिंटैक्टिक खंड जैसे let, को प्रस्तुत करते है।

let f =N in M

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

इस let का एक उल्लेखनीय प्रतिबंध है यह कि पद f को N में परिभाषित नहीं किया जाना चाहिए, N के लिए अमूर्त परिबद्ध f के विस्तार से बाहर होना चाहिए; इसका तात्पर्य है कि एक पुनरावर्ती फलन परिभाषा का उपयोग N के रूप में नहीं किया जा सकता है let. letrec निर्माण पुनरावर्ती फलन परिभाषाएँ लिखने की स्वीकृति देगा।

पुनरावर्तन और निश्चित बिंदु

Main article: निश्चित-बिंदु संयोजक

See also: एसकेआई संयोजक कलन § स्व-अनुप्रयोग और पुनरावर्तन

पुनरावर्तन फलन का उपयोग करके फलन की परिभाषा है। लैम्ब्डा गणना इसे प्रत्यक्ष रूप से कुछ अन्य अंकन के रूप में व्यक्त नहीं कर सकता है: लैम्ब्डा गणना में सभी फलन अस्पष्ट हैं, इसलिए हम लैम्ब्डा शब्द के अंदर उसी मान को परिभाषित करने वाले मान का उल्लेख नहीं कर सकते हैं। हालांकि, लैम्ब्डा व्यंजक को अपने तर्क मान के रूप में प्राप्त करने की व्यवस्था करके अभी भी पुनरावर्तन प्राप्त किया जा सकता है, उदाहरण के लिए (λx.x x) E.

क्रमगुणित (फैक्टोरियल) फलन F(n) द्वारा पुनरावर्ती रूप से परिभाषित पर विचार करें

F(n) = 1, if n = 0; else n × F(n − 1).

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

G := λr. λn.(1, if n = 0; else n × (r r (n−1)))

साथ r r x = F x = G r x धारण करना, इसलिए r = G और

F := G G = (λx.x x) G

स्व-अनुप्रयोग यहां प्रतिकृति प्राप्त करता है, फलन की लैम्ब्डा व्यंजक को तर्क मान के रूप में अगले इन्वोकेशन पर पास करता है, इसे संदर्भित करने के लिए उपलब्ध कराता है और वहां संबोधित किया जाता है।

यह इसे हल करता है लेकिन प्रत्येक पुनरावर्ती कॉल को स्व-अनुप्रयोग के रूप में पुनः लिखने की आवश्यकता होती है। हम किसी भी पुनः लिखने की आवश्यकता के बिना एक सामान्य समाधान चाहते हैं:

G := λr. λn.(1, if n = 0; else n × (r (n−1)))

साथ r x = F x = G r x धारण करना, इसलिए r = G r =: FIX G और

F := FIX G जहां FIX g := (r where r = g r) = g (FIX g)

ताकि FIX G = G (FIX G) = (λn.(1, if n = 0; else n × ((FIX G) (n−1))))

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

वास्तव में, इसके लिए कई संभावित परिभाषाएँ हैं FIX संक्रियक, उनमें से सबसे सामान्य हैं:

Y := λg.(λx.g (x x)) (λx.g (x x))

लैम्ब्डा गणना में, Y g का निश्चित बिन्दु g है जैसा कि इसका विस्तार होता है:

Y g

(λh.(λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g)

अब, हमारे पुनरावर्ती कॉल को फैक्टोरियल फलन करने के लिए, हम सिर्फ (Y G) n, कॉल करेंगे जहां n वह संख्या है जिसके भाज्य की हम गणना कर रहे हैं। दिया गया n = 4, उदाहरण के लिए, यह देता है:

(Y G) 4

G (Y G) 4

(λr.λn.(1, if n = 0; else n × (r (n−1)))) (Y G) 4

(λn.(1, if n = 0; else n × ((Y G) (n−1)))) 4

1, if 4 = 0; else 4 × ((Y G) (4−1))

4 × (G (Y G) (4−1))

4 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (4−1))

4 × (1, if 3 = 0; else 3 × ((Y G) (3−1)))

4 × (3 × (G (Y G) (3−1)))

4 × (3 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (3−1)))

4 × (3 × (1, if 2 = 0; else 2 × ((Y G) (2−1))))

4 × (3 × (2 × (G (Y G) (2−1))))

4 × (3 × (2 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (2−1))))

4 × (3 × (2 × (1, if 1 = 0; else 1 × ((Y G) (1−1)))))

4 × (3 × (2 × (1 × (G (Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (1−1)))))

4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × ((Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24

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

मानक शब्द

कुछ शब्दों के सामान्यतः स्वीकृत नाम हैं:

I := λx.x

S := λx.λy.λz.x z (y z)

K := λx.λy.x

B := λx.λy.λz.x (y z)

C := λx.λy.λz.x z y

W := λx.λy.x y y

ω or Δ or U := λx.x x

Ω := ω ω

I सर्वसमिका फलन है। SK और BCKW प्रारूप पूर्ण साहचर्य गणना प्रणाली जो किसी भी लैम्ब्डा पद को व्यक्त कर सकता है -अगला भाग देखें Ω है UU, या YI, सबसे छोटा पद है जिसका कोई सामान्य रूप नहीं है। Y मानक है और परिभाषित है, और इसे Y=BU(CBU)रूप में भी परिभाषित किया जा सकता है, ताकि Yf=f(Yf)ऊपर परिभाषित TRUE और FALSE को सामान्य रूप से T और F के रूप मे संक्षिप्त किया जाता है

अमूर्त उन्मूलन

Main article: संयोजन तर्क § S-K आधार की पूर्णता

यदि N अमूर्तता के बिना एक लैम्ब्डा-पद है, लेकिन संभवतः नामित नियतांक (संयोजी तर्क) युक्त है, तो एक लैम्ब्डा-पद T (x,N) सम्मिलित है जो λx.N बराबर है लेकिन अमूर्तता का अभाव है (नामित नियतांक के भाग को छोड़कर, यदि इन्हें गैर-परमाणु माना जाता है)। इसे अज्ञात चर के रूप में भी देखा जा सकता है, क्योंकि T(x,N) x से N की सभी उपस्थिति को हटा देता है, जबकि अभी भी तर्क मानों को उन स्थितियों में प्रतिस्थापित करने की स्वीकृति है जहाँ N में x सम्मिलित है। रूपांतरण फलन T द्वारा परिभाषित किया जा सकता है:

T(x, x) := I

T(x, N) := K N if x is not free in N.

T(x, M N) := S T(x, M) T(x, N)

किसी भी स्थिति में, प्रारूप T(x,N) P प्रारंभिक साहचर्य 'I', 'K', या 'S' द्वारा तर्क P को ग्रैब से कम कर सकता है, उसी तरह जैसे β-अवनति (λx.N) P मे होगी। 'I' वह तर्क देता है। 'K' तर्क को कम कर देता है, जैसे (λx.N) करेंगे यदि x में N कोई मुक्त पद नहीं है। 'S' तर्क को अनुप्रयोग के दोनों उप-पदों पर पास करता है, और फिर पहले के परिणाम को दूसरे के परिणाम पर प्रयुक्त करता है।

संयोजक 'B' और 'C' 'S' के समान हैं, लेकिन एक अनुप्रयोग के केवल एक उपपद पर तर्क पारित करते हैं ('B' तर्क उपपद के लिए और 'C' फलन उपपद के लिए), इस प्रकार 'K' पद न हो तो x एक उपपद में उपस्थित नहीं करते है। B और C की तुलना में, एस साहचर्य वास्तव में दो कार्यात्मकताओं को जोड़ता है: तर्कों को पुनर्व्यवस्थित करना, और एक तर्क को पुनरावृत करता ताकि इसे दो समष्टि पर उपयोग किया जा सके। W संयोजक केवल बाद वाले को एसकेआई साहचर्य गणना के विकल्प के रूप में B, C, K, W प्रणाली की प्रदान करता है।

टाइप किया हुआ लैम्ब्डा गणना

Main article: टाइप लैम्ब्डा गणना

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

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

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

अवनति रणनीतियाँ

Main article: न्यूनीकरण रणनीति § लैम्ब्डा गणना

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

सामान्य क्रम

सबसे बाएँ, सबसे बाहरी रिडेक्स को सदैव पहले घटाया जाता है। यही है, जब भी संभव हो तर्कों को कम करने से पहले तर्कों को अमूर्त के समूह में प्रतिस्थापित किया जाता है।

प्रयुक्त करने का क्रम

सबसे बाएं, अंतरतम रिडेक्स को सदैव पहले घटाया जाता है। सामान्य रूप से इसका तात्पर्य है कि फलन के तर्क सदैव फलन से पहले ही कम हो जाते हैं। व्यावहारिक क्रम सदैव फलनों को सामान्य रूपों में प्रयुक्त करने का प्रयास करता है, तथापि यह संभव न हो।

पूर्ण β-अवनति

किसी भी रेडेक्स को किसी भी समय घटाया जा सकता है। इसका तात्पर्य अनिवार्य रूप से किसी विशेष कमी की योजना की कमी है समानेयता के संबंध में, सभी शर्त विवृत हैं। लैम्ब्डा अमूर्तता के अंतर्गत दुर्बल कमी की योजना कम नहीं होती है:

मान स्थगित

एक रीडेक्स केवल तभी घटाया जाता है जब उसका दाहिना हाथ एक मान (चर या अमूर्त) तक कम हो जाता है। केवल सबसे बाहरी रेडेक्स कम किए जाते हैं।

नाम स्थगित

सामान्य क्रम के रूप में, लेकिन अमूर्तता के अंदर कोई अवनति नहीं की जाती है। उदाहरण के लिए, λx.(λy.y)x इस योजना के अनुसार सामान्य रूप में है, हालांकि इसमें रेडेक्स (λy.y)x सम्मिलित है।

साझाकरण के साथ रणनीतियाँ उन संगणनाओं को कम करती हैं जो समानांतर में समान हैं:

इष्टतम अवनति

सामान्य क्रम के रूप में, लेकिन समान लेबल वाली संगणनाएँ एक साथ कम हो जाती हैं।

आवश्यकता मे स्थगित

नाम से कॉल के रूप में (इसलिए दुर्बल), लेकिन फलन अनुप्रयोग जो शब्दों को प्रतिदर्श करेंगे, इसके अतिरिक्त तर्क को नाम दें, जिसे केवल तभी कम किया जाता है जब इसकी आवश्यकता होती है।

संगणनीयता

कोई एल्गोरिथ्म नहीं है जो किसी भी दो लैम्ब्डा व्यंजक और आउटपुट को इनपुट के रूप में लेता है और TRUE या FALSE इस पर निर्भर करता है कि एक व्यंजक दूसरे को कम करती है या नहीं। अधिक परिशुद्ध रूप से, कोई भी संगणनीय फलन समस्या का निर्णय नहीं कर सकता है। यह ऐतिहासिक दृष्टि से पहली समस्या थी जिसके लिए अनिश्चयता सिद्ध की जा सकती थी। इस तरह के प्रमाण के लिए सदैव की तरह, संगणनीय का तात्पर्य गणना के किसी भी मॉडल द्वारा गणना योग्य है जो ट्यूरिंग पूर्ण है। वास्तव में संगणनीयता को लैम्ब्डा गणना के माध्यम से परिभाषित किया जा सकता है: प्राकृतिक संख्याओं का एक फलन F: 'N' → 'N' एक संगणनात्मक फलन है यदि और केवल यदि लैम्ब्डा व्यंजक f सम्मिलित है जैसे कि x, y की प्रत्येक युग्म के लिए 'N, F(x)=y यदि और केवल यदि F x =_β y, जहां x और y क्रमशः x और y के अनुरूप चर्च अंक हैं और =_β तात्पर्य β-अवनति के साथ समानता है। संगणनीयता और उनकी समानता को परिभाषित करने के अन्य दृष्टिकोणों के लिए चर्च-ट्यूरिंग अभिधारणा देखें।

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

जटिलता

लैम्ब्डा गणना के लिए संगणनात्मक जटिलता सिद्धांत की धारणा कठिन है, क्योंकि β-अवनति की कीमत इसे प्रयुक्त करने के तरीके के आधार पर भिन्न हो सकती है। परिशुद्ध होने के लिए, किसी को बाध्य चर की सभी उपस्थिति का स्थान ढूंढना चाहिए V व्यंजक में E, एक समय की कीमत का अर्थ है, या किसी को किसी तरह से मुक्त चर के समष्टि की जानकारी रखनी चाहिए, एक स्थान कीमत का अर्थ है। E में V के समष्टि के लिए एक सामान्य जाँच E की लंबाई N में O (N) है। निदेशक शृंखला एक प्रारंभिक दृष्टिकोण थे जो द्विघात समष्टि उपयोग के लिए इस समय की कीमत का उपयोग करते थे। सामान्य रूप से इससे उन प्रणालियों का अध्ययन हुआ है जो स्पष्ट प्रतिस्थापन का उपयोग करते हैं।

2014 में यह दिखाया गया था कि एक पद को कम करने के लिए सामान्य क्रम में कमी के द्वारा β-अवनति चरणों की संख्या एक उपयुक्त समय कीमत मॉडल है, अर्थात, कमी को ट्यूरिंग मशीन पर बहुपद रूप से चरणों की संख्या के अनुपात में अनुकरण किया जा सकता है। यह लंबे समय से संवृत समस्या थी, आकार विस्फोट के कारण, लैम्ब्डा पदों की स्थिति जो प्रत्येक β-अवनति के लिए आकार में तीव्रता से बढ़ता है। नियम साझा प्रतिनिधित्व के साथ काम करके परिणाम इसके आसपास हो जाता है। परिणाम स्पष्ट करता है कि लैम्ब्डा शब्द का मूल्यांकन करने के लिए आवश्यक स्थान की मात्रा कमी के समय पद के आकार के समानुपाती नहीं है। यह वर्तमान में ज्ञात नहीं है कि समष्टि जटिलता का एक अच्छा उपाय क्या होगा।

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

लैम्ब्डा गणना और प्रोग्रामिंग भाषाएं

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

अज्ञात फलन

Main article: अज्ञात फलन

उदाहरण के लिए, पायथन (प्रोग्रामिंग भाषा) में स्क्वायर फ़ंक्शन को लैम्ब्डा व्यंजक के रूप में निम्नानुसार व्यक्त किया जा सकता है:

(lambda x: x**2)

उपरोक्त उदाहरण एक व्यंजक है जो प्रथम श्रेणी के फलन का मूल्यांकन करता है। प्रतीक lambda पैरामीटर नामों की एक सूची दी गई है, एक अज्ञात फलन बनाता है, x - इस स्थिति में केवल एक तर्क, और एक व्यंजक जिसका मूल्यांकन फलन के मुख्य भाग के रूप में किया जाता है, x**2 अज्ञात फलनों को कभी-कभी लैम्ब्डा व्यंजक कहा जाता है।

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

समानता और समरूपता

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

सेमेन्टिक्स

तथ्य यह है कि लैम्ब्डा गणना पद अन्य लैम्ब्डा गणना शर्तों पर फलनों के रूप में फलन करते हैं, और यहां तक ​​​​कि स्वयं पर भी, लैम्ब्डा गणना के अर्थशास्त्र के बारे में प्रश्नों का नेतृत्व करते हैं। क्या लैम्ब्डा गणना शर्तों को सेमेन्टिक्स दिया जा सकता है? प्राकृतिक अर्थ को स्वयं के फलनों के फलन स्थान D → D के लिए एक समुच्चय D समरूप जाँचना था। हालांकि, प्रमुखता कमी के कारण कोई भी गैर- साधारण D सम्मिलित नहीं हो सकता है क्योंकि D से D के सभी फलनों के समुच्चय में D की तुलना में अधिक प्रमुखता है, जब तक कि D सिंगलटन समुच्चय न हो।

1970 के दशक में, दाना स्कॉट ने दिखाया कि यदि केवल स्कॉट निरंतरता पर विचार किया जाता है, तो आवश्यक गुण के साथ एक समुच्चय या डोमेन सिद्धांत D पाया जा सकता है, इस प्रकार लैम्ब्डा गणना के लिए एक मॉडल सिद्धांत प्रदान करता है।

इस फलन ने प्रोग्रामिंग भाषाओं के सांकेतिक सेमेन्टिक्स (अर्थ) के लिए भी आधार बनाया।

विविधताएं और विस्तार

ये एक्सटेंशन लैम्ब्डा घन में हैं:

• टाइप किया हुआ लैम्ब्डा गणना - टाइप किए गए चर (और फ़ंक्शंस) के साथ लैम्ब्डा गणना
• प्रणाली एफ - प्रारूप-चर के साथ एक टाइप किया हुआ लैम्ब्डा गणना
• निर्माण की कलन - प्रथम श्रेणी के मान के रूप में टाइप प्रणाली के साथ एक टाइप किया हुआ लैम्ब्डा गणना

ये औपचारिक प्रणालियाँ लैम्ब्डा गणना के विस्तार हैं जो लैम्ब्डा घन में नहीं हैं:

• बाइनरी लैम्ब्डा गणना - बाइनरी इनपुट/आउट्पुट के साथ लैम्ब्डा गणना का एक संस्करण, शब्दों का एक बाइनरी एन्कोडिंग और एक निर्दिष्ट सामान्य मशीन।
• लैम्ब्डा-म्यू गणना - उत्कृष्ट तर्क के संशोधन के लिए लैम्ब्डा गणना का विस्तार

ये औपचारिक प्रणालियाँ लैम्ब्डा गणना की विविधताएँ हैं:

• कप्पा गणना - लैम्ब्डा गणना का प्रथम क्रम का एनालॉग

ये औपचारिक प्रणालियाँ लैम्ब्डा गणना से संबंधित हैं:

• संयोजन तर्क - चर के बिना गणितीय तर्क के लिए एक अंकन
• एसकेआई साहचर्य गणना - S, K और I साहचर्य पर आधारित एक संगणनात्मक प्रणाली, लैम्ब्डा गणना के बराबर, लेकिन चर प्रतिस्थापन के बिना कम

यह भी देखें

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

अग्रिम पठन

• Abelson, Harold & Gerald Jay Sussman. Structure and Interpretation of Computer Programs. The MIT Press. ISBN 0-262-51087-1.
• Hendrik Pieter Barendregt Introduction to Lambda Calculus.
• Henk Barendregt, The Impact of the Lambda Calculus in Logic and Computer Science. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
• Barendregt, Hendrik Pieter, The Type Free Lambda Calculus pp1091–1132 of Handbook of Mathematical Logic, North-Holland (1977) ISBN 0-7204-2285-X
• Cardone and Hindley, 2006. History of Lambda-calculus and Combinatory Logic. In Gabbay and Woods (eds.), Handbook of the History of Logic, vol. 5. Elsevier.
• Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345–363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
• Church, Alonzo (1941). The Calculi of Lambda-Conversion. Princeton: Princeton University Press. Retrieved 2020-04-14. (ISBN 978-0-691-08394-0)
• Frink Jr., Orrin (1944). "Review: The Calculi of Lambda-Conversion by Alonzo Church" (PDF). Bull. Amer. Math. Soc. 50 (3): 169–172. doi:10.1090/s0002-9904-1944-08090-7.
• Kleene, Stephen, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp. 153–173 and 219–244. Contains the lambda calculus definitions of several familiar functions.
• Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation, Communications of the ACM, vol. 8, no. 2 (1965), pages 89–101. Available from the ACM site. A classic paper highlighting the importance of lambda calculus as a basis for programming languages.
• Larson, Jim, An Introduction to Lambda Calculus and Scheme. A gentle introduction for programmers.
• Michaelson, Greg (10 April 2013). An Introduction to Functional Programming Through Lambda Calculus (in English). Courier Corporation. ISBN 978-0-486-28029-5.
• Schalk, A. and Simmons, H. (2005) An introduction to λ-calculi and arithmetic with a decent selection of exercises. Notes for a course in the Mathematical Logic MSc at Manchester University.
• de Queiroz, Ruy J.G.B. (2008). "On Reduction Rules, Meaning-as-Use and Proof-Theoretic Semantics". Studia Logica. 90 (2): 211–247. doi:10.1007/s11225-008-9150-5. S2CID 11321602. A paper giving a formal underpinning to the idea of 'meaning-is-use' which, even if based on proofs, it is different from proof-theoretic semantics as in the Dummett–Prawitz tradition since it takes reduction as the rules giving meaning.
• Hankin, Chris, An Introduction to Lambda Calculi for Computer Scientists, ISBN 0954300653

Monographs/textbooks for graduate students

• Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry–Howard isomorphism, Elsevier, 2006, ISBN 0-444-52077-5 is a recent monograph that covers the main topics of lambda calculus from the type-free variety, to most typed lambda calculi, including more recent developments like pure type systems and the lambda cube. It does not cover subtyping extensions.
• Pierce, Benjamin (2002), Types and Programming Languages, MIT Press, ISBN 0-262-16209-1 covers lambda calculi from a practical type system perspective; some topics like dependent types are only mentioned, but subtyping is an important topic.

Documents

• Achim Jung, A Short Introduction to the Lambda Calculus-(PDF)
• Dana Scott, A timeline of lambda calculus-(PDF)
• Raúl Rojas, A Tutorial Introduction to the Lambda Calculus-(PDF)
• Peter Selinger, Lecture Notes on the Lambda Calculus-(PDF)
• Marius Buliga, Graphic lambda calculus
• Lambda Calculus as a Workflow Model by Peter Kelly, Paul Coddington, and Andrew Wendelborn; mentions graph reduction as a common means of evaluating lambda expressions and discusses the applicability of lambda calculus for distributed computing (due to the Church–Rosser property, which enables parallel graph reduction for lambda expressions).

संदर्भ

Some parts of this article are based on material from FOLDOC, used with permission.

बाहरी संबंध

• Graham Hutton, Lambda Calculus, a short (12 minutes) Computerphile video on the Lambda Calculus
• Helmut Brandl, Step by Step Introduction to Lambda Calculus
• "Lambda-calculus", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
• L. Allison, Some executable λ-calculus examples
• Georg P. Loczewski, The Lambda Calculus and A++
• Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
• Lambda Calculus Archived 2012-10-14 at the Wayback Machine on Safalra's Website Archived 2021-05-02 at the Wayback Machine
• LCI Lambda Interpreter a simple yet powerful pure calculus interpreter
• Lambda Calculus links on Lambda-the-Ultimate
• Mike Thyer, Lambda Animator, a graphical Java applet demonstrating alternative reduction strategies.
• Implementing the Lambda calculus using C++ Templates
• Shane Steinert-Threlkeld, "Lambda Calculi", Internet Encyclopedia of Philosophy
• Anton Salikhmetov, Macro Lambda Calculus