टाइप किया गया लैम्ब्डा कैलकुलस

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

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

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

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

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

कुछ टाइप किए गए लैम्ब्डा कैलकुली उपप्रकार की धारणा पेश करते हैं, यानी यदि $A$ का एक उपप्रकार है $B$, फिर प्रकार की सभी शर्तें $A$ प्रकार भी है $B$. उपप्रकार के साथ टाइप किया गया लैम्ब्डा कैलकुली संयोजन प्रकार और सिस्टम एफ-सब|सिस्टम एफ के साथ बस टाइप किया गया लैम्ब्डा कैलकुलस है।_<:.

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

प्रोग्रामिंग भाषाओं के लिए अनुप्रयोग

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

यह भी देखें

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

अग्रिम पठन

• 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