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

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

लैम्ब्डा कैलकुलस में #Lambda टर्म्स|§ लैम्ब्डा टर्म्स का निर्माण करना और उन पर #Reduction|§ रिडक्शन ऑपरेशन करना शामिल है। लैम्ब्डा कैलकुस के सबसे सरल रूप में, शर्तों को केवल निम्नलिखित नियमों का उपयोग करके बनाया गया है:

• $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])}$ - β-कमी, अमूर्त के शरीर में तर्क अभिव्यक्ति के साथ बाध्य चर को बदलना।

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

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

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

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

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

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

इतिहास

लैम्ब्डा कैलकुलस को गणितज्ञ अलोंजो चर्च द्वारा 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)}$ // की परिभाषा $x$ के साथ प्रयोग किया गया है $5$ आंतरिक अभिव्यक्ति में। यह β-कमी जैसा है।

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