लैम्ब्डा गणना प्रकार (टाइप लैम्ब्डा कैलकुस)

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

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

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

टाइप्ड लैम्ब्डा कैलकुली के प्रकार

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

कुछ टाइप किए गए लैम्ब्डा कैलकुली सबटाइपिंग की धारणा का परिचय देते हैं, अर्थात यदि $A$, $B$ का उपप्रकार है, तो टाइप $A$ के सभी शब्दों में भी टाइप $B$ होता है। सबटाइपिंग के साथ टाइप की गई लैम्ब्डा कैलकुली कंजंक्टिव प्रकार और सिस्टम F_<: के साथ बस टाइप की गई लैम्ब्डा कैलकुलस हैं।

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

प्रोग्रामिंग भाषाओं के लिए आवेदन

कंप्यूटर प्रोग्रामिंग में, दृढ़ता से टाइप की गई प्रोग्रामिंग भाषाओं की दिनचर्या (कार्य, प्रक्रियाएं, विधियां) टाइप किए गए लैम्ब्डा एक्सप्रेशंस के साथ निकटता से मेल खाती हैं।

यह भी देखें

• कप्पा कैलकुलस- टाइप किए गए लैम्ब्डा कैलकुलस का एक एनालॉग जिसमें उच्च-क्रम के कार्य सम्मलित नहीं हैं।

अग्रिम पठन

• Barendregt, Henk (1992). "Lambda Calculi with Types". In Abramsky, S. (ed.). Background: Computational Structures. Handbook of Logic in Computer Science. Vol. 2. Oxford University Press. pp. 117–309. ISBN 9780198537618.
• Brandl, Helmut (2022). Calculus of Constructions / Typed Lambda Calculus