लैम्डा कैलकुलस और कार्यात्मक मॉडल

लैम्डा कैलकुलस एक न्यूनतम औपचारिक प्रणाली है जिसमें सब कुछ एक फलन होता है और संगणना प्रतिस्थापन द्वारा आगे बढ़ती है, जो प्रभावी संगणना का एक प्रारंभिक मॉडल और कार्यात्मक प्रोग्रामिंग का सैद्धांतिक मूल दोनों प्रदान करती है।

Definition

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

Scope

यह विषय लैम्डा पदों के सिंटैक्स, संगणना को संचालित करने वाले न्यूनीकरण नियमों, चर्च-रॉसर संगामी गुण (Church–Rosser confluence property), निश्चित-बिंदु संयोजकों (fixed-point combinators) के माध्यम से डेटा और पुनरावर्तन (recursion) के एन्कोडिंग, कैलकुलस की ट्यूरिंग-पूर्णता (Turing-completeness), और संगणना को तर्क से जोड़ने वाले टाइप किए गए वेरिएंट को शामिल करता है।

Core questions

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

Key theories

चर्च-रॉसर प्रमेय

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

ट्यूरिंग-पूर्णता और निश्चित बिंदु

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

करी-हावर्ड पत्राचार

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

Clinical relevance

लैम्डा कैलकुलस लिस्प, हास्केल और एमएल जैसी कार्यात्मक प्रोग्रामिंग भाषाओं, आधुनिक भाषाओं में त्रुटियों को पकड़ने वाली प्रकार प्रणालियों (type systems), और प्रूफ असिस्टेंट (proof assistants) का आधार है जहाँ करी-हावर्ड पत्राचार (Curry–Howard correspondence) कार्यक्रमों और गणितीय प्रमाणों को एक ही तंत्र द्वारा जांचने की अनुमति देता है।

History

चर्च ने 1930 के दशक में तर्क और संगणना के आधार के रूप में लैम्डा कैलकुलस की शुरुआत की, और रॉसर के साथ इसकी संगामिता (confluence) को सिद्ध किया। यद्यपि मूल तार्किक प्रणाली असंगत थी, संगणनात्मक मूल फला-फूला, और 1960 के दशक से इसने कार्यात्मक प्रोग्रामिंग को आकार दिया और, करी-हावर्ड पत्राचार के माध्यम से, प्रमाणों और कार्यक्रमों के बीच संबंध स्थापित किया।

Key figures

• Alonzo Church
• Haskell Curry
• J. Barkley Rosser
• William Alvin Howard

Seminal works

• church1936
• barendregt1984

Frequently asked questions

केवल फलनों वाली प्रणाली संख्याओं के साथ गणना कैसे कर सकती है?

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

लैम्डा कैलकुलस और प्रोग्रामिंग के बीच क्या संबंध है?

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