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

लैम्ब्डा गणना (जिसे λ-गणना के रूप में भी लिखा जाता है) गणितीय तर्क में एक औपचारिक प्रणाली है जो चर बंधन और प्रतिस्थापन का उपयोग करके फलन अमूर्त और अनुप्रयोग के आधार पर अभिकलन व्यक्त करती है। यह संगणना का एक सार्वभौमिक मॉडल है जिसका उपयोग किसी भी ट्यूरिंग मशीन (परिगणन युक्ति) को अनुकरण करने के लिए किया जा सकता है। इसे 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}$

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

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

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

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

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

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

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

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

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

एक सार $\lambda x.t$ एक #anonymousForm|§ अनाम फलन को दर्शाता है जो एक ही इनपुट लेता है 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, अर्थात यह कॉलिंग फलन के कार्य का प्रतिनिधित्व करता है t इनपुट पर s उत्पन्न करना $t(s)$.

परिवर्तनीय घोषणा के लैम्ब्डा गणना में कोई अवधारणा नहीं है। एक परिभाषा में जैसे $\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)$ एक्स के लिए, जबकि उदाहरण 2 है $MN$; $M$ लैम्ब्डा शब्द है $(\lambda x.x)$ इनपुट एन पर प्रयुक्त होने के लिए। दोनों उदाहरण 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$ कोई मुक्त चर नहीं है, लेकिन function $\lambda x.y$ $x$ एक मुक्त चर है, $y$.

कब्जा-परिहार प्रतिस्थापन

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

• $x[x:=r]=r$; $x$ इसके लिए प्रतिस्थापित $r$ बस है $r$
• $y[x:=r]=y$ अगर $x\neq y$; $x$ इसके लिए प्रतिस्थापित $r$ गतिविधि करते समय $y$ बस है $y$
• $(t$ $s)[x:=r]=(t[x:=r])(s[x:=r])$; प्रतिस्थापन चर के आगे के अनुप्रयोग के लिए वितरित करता है
• $(\lambda x.t)[x:=r]=\lambda x.t$; यद्यपि $x$ पर मैप किया गया है $r$, बाद में सभी की मैपिंग की $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: Lambda calculus definition

परिभाषा

लैम्ब्डा भाव से बना है:

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

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

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

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

अंकन

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

• सबसे बाहरी कोष्ठक हटा दिए जाते हैं: (एम एन) के बजाय एम एन।
• अनुप्रयोगों को सहचारी छोड़ दिया जाता है: ((एम एन) पी) के बजाय एम एन पी लिखा जा सकता है।
• जब सभी चर एकल-अक्षर वाले हों, तो अनुप्रयोगों में स्थान छोड़ा जा सकता है: MNP के बजाय MNP।
• एक अमूर्त का निकाय नियमित व्यंजक का विस्तार करता है # आलसी मिलान: λ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)।

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

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

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

कमी

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

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

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

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

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

α-रूपांतरण

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

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

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

स्टैटिक नाम संकल्प (प्रोग्रामिंग भाषाएं) में, α-रूपांतरण का उपयोग नाम रिज़ॉल्यूशन (प्रोग्रामिंग लैंग्वेज) को सामान्य बनाने के लिए किया जा सकता है, यह सुनिश्चित करके कि कोई वैरिएबल नाम चर शैडोइंग एक युक्त गुंजाइश (प्रोग्रामिंग) में नहीं है (देखें नाम रिज़ॉल्यूशन (प्रोग्रामिंग लैंग्वेज)#Alpha रीनेमिंग नाम संकल्प तुच्छ बनाने के लिए | α-नाम बदलने के लिए नाम संकल्प तुच्छ बनाने के लिए)।

डी ब्रुइज़न इंडेक्स अंकन में, कोई भी दो α-समतुल्य शब्द वाक्यगत रूप से समान हैं।

प्रतिस्थापन

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

एक्स [एक्स: = एन] = एन

y[x := N] = y, यदि x ≠ y

(एम₁ M₂) [एक्स: = एन] = एम₁[एक्स:= एन] एम₂[एक्स := एन]

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

(λy.M)[x := N] = λy.(M[x := N]), यदि x ≠ y और y ∉ FV(N) देखें #मुक्त और बाध्य चर

एक अमूर्त में स्थानापन्न करने के लिए, कभी-कभी व्यंजक को α-रूपांतरित करना आवश्यक होता है। उदाहरण के लिए, यह (λ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: Normalization property (abstract rewriting)

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

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

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

एन्कोडिंग डेटाटाइप्स

Main articles: Church encoding and Mogensen–Scott encoding

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

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

0 := λf.λx.x

1 := λf.λx.f x

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

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

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

0 := λfx.x

1 := λfx.f x

2 := λfx.f (f x)

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

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

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

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

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

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

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 जोड़ी encapsulates (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)

एक लिंक की गई सूची को खाली सूची के लिए या तो शून्य के रूप में परिभाषित किया जा सकता है, या 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 एम में मतलब एन (कुछ स्पष्ट लैम्ब्डा-पद) (एक और लैम्ब्डा-पद, मुख्य कार्यक्रम), कोई कह सकता है

(λf.M) एन

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

let f =N in एम

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

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

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

Main article: Fixed-point combinator

See also: SKI combinator calculus § Self-application and recursion

प्रत्यावर्तन फलन का उपयोग करके फलन की परिभाषा है। लैम्ब्डा गणना इसे सीधे तौर पर कुछ अन्य अंकन के रूप में व्यक्त नहीं कर सकता है: लैम्ब्डा गणना में सभी फलन अस्पष्ट हैं, इसलिए हम लैम्ब्डा शब्द के अंदर उसी मान को परिभाषित करने वाले मान का उल्लेख नहीं कर सकते हैं। हालांकि, लैम्ब्डा व्यंजक को अपने तर्क मान के रूप में प्राप्त करने की व्यवस्था करके अभी भी रिकर्सन प्राप्त किया जा सकता है, उदाहरण के लिए (λ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 फॉर्म कंप्लीट कॉम्बिनेटर गणना सिस्टम जो किसी भी लैम्ब्डा पद को व्यक्त कर सकता है - देखें

1. अमूर्त उन्मूलन। Ω है UU, या YI, सबसे छोटा शब्द जिसका कोई सामान्य रूप नहीं है। Y मानक है और परिभाषित #Y है, और इसे इस रूप में भी परिभाषित किया जा सकता है Y=BU(CBU), ताकि Yf=f(Yf). TRUE और FALSE परिभाषित #तर्क और विधेय को आमतौर पर संक्षिप्त किया जाता है T और F.

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

Main article: Combinatory logic § Completeness of the S-K basis

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

टी(x, x) := मैं

टी(x, एन) := 'के' एन अगर x एन में मुक्त नहीं है।

टी(x, एम एन) := 'एस' टी (x, एम) टी (x, एन)

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

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

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

Main article: Typed lambda calculus

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

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

कटौती रणनीतियाँ

Main article: Reduction strategy § Lambda calculus

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

सामान्य क्रम

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

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

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

पूर्ण β-कटौती

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

लैम्ब्डा सार के तहत दुर्बल कमी की रणनीति कम नहीं होती है:

मूल्य से कॉल करें

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

नाम से बुलाओ

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

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

इष्टतम कमी

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

आवश्यकता के अनुसार कॉल करें

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

कम्प्यूटेबिलिटी

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

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

जटिलता

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

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

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

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

अनाम कार्य

Main article: Anonymous function

उदाहरण के लिए, पायथन (प्रोग्रामिंग भाषा) में स्क्वायर फलन को लैम्ब्डा व्यंजक के रूप में निम्नानुसार व्यक्त किया जा सकता है: <वाक्यविन्यास लैंग = पायथन> (लैम्ब्डा एक्स: एक्स ** 2) </वाक्यविन्यास हाइलाइट>

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

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

समानांतरवाद और संगामिति

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

अर्थ

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

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

रूपांतर और विस्तार

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

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

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

• बाइनरी लैम्ब्डा गणना - बाइनरी I/O के साथ लैम्ब्डा गणना का एक संस्करण, शब्दों का एक बाइनरी एन्कोडिंग और एक निर्दिष्ट यूनिवर्सल मशीन।
• लैम्ब्डा-इन गणना - शास्त्रीय तर्क के इलाज के लिए लैम्ब्डा गणना का विस्तार

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

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

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

• संयोजन तर्क - चर के बिना गणितीय तर्क के लिए एक अंकन
• SKI कॉम्बिनेटर गणना - #S, #K और #I कॉम्बिनेटर पर आधारित एक संगणनात्मक सिस्टम, लैम्ब्डा गणना के बराबर, लेकिन चर सब्स्टीट्यूशन के बिना रिड्यूसिबल

यह भी देखें

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

अग्रिम पठन

• 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