स्पष्ट प्रतिस्थापन
 | This article may be too technical for most readers to understand. (May 2023) (Learn how and when to remove this template message) |
 | It has been suggested that this article be merged into Lambda calculus. (Discuss) Proposed since May 2023. |
कंप्यूटर विज्ञान में, लैम्ब्डा कैलकुलस को स्पष्ट प्रतिस्थापन कहा जाता है यदि वे चर के प्रतिस्थापन की प्रक्रिया की औपचारिकता पर विशेष ध्यान देते हैं। यह मानक लैम्ब्डा कैलकुलस के विपरीत है जहां बीटा कटौती द्वारा प्रतिस्थापन एक अंतर्निहित तरीके से किया जाता है जो कैलकुलस के भीतर व्यक्त नहीं किया जाता है; ऐसी अंतर्निहित गणनाओं में ताजगी की स्थितियाँ त्रुटियों का एक कुख्यात स्रोत हैं।[1] यह अवधारणा विभिन्न क्षेत्रों में बड़ी संख्या में प्रकाशित पत्रों में दिखाई दी है, जैसे कि अमूर्त मशीनें, विधेय तर्क और प्रतीकात्मक गणना।
सिंहावलोकन
स्पष्ट प्रतिस्थापन के साथ लैम्ब्डा कैलकुलस का एक सरल उदाहरण λx है, जो लैम्ब्डा कैलकुलस में शब्द का एक नया रूप जोड़ता है, अर्थात् फॉर्म M〈x:=N〉, जो M पढ़ता है जहां x को N द्वारा प्रतिस्थापित किया जाएगा। (नए शब्द का अर्थ कई प्रोग्रामिंग भाषाओं में एम में आम मुहावरे x:=N के समान है।) λx को निम्नलिखित पुनर्लेखन नियमों के साथ लिखा जा सकता है:
- (λx.M) N → M〈x:=N〉
- x〈x:=N〉 → N
- x〈y:=N〉 → x (x≠y)
- (एम1M2) 〈x:=N〉 → (एम1〈x:=N〉) (एम2〈x:=N〉)
- (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y और x N में मुक्त नहीं हैं)
प्रतिस्थापन को स्पष्ट करते हुए, यह सूत्रीकरण अभी भी लैम्ब्डा कैलकुलस चर सम्मेलन की जटिलता को बरकरार रखता है, यह सुनिश्चित करने के लिए कि अंतिम नियम पर (x≠y और x N में मुक्त नहीं है) स्थिति को लागू करने से पहले हमेशा संतुष्ट किया जाता है, कमी के दौरान चर के मनमाने ढंग से नाम बदलने की आवश्यकता होती है। नियम। इसलिए स्पष्ट प्रतिस्थापन की कई गणनाएँ तथाकथित नाम-मुक्त ब्राउन इंडेक्स नोटेशन का उपयोग करके परिवर्तनीय नामों से पूरी तरह बचती हैं।
इतिहास
कॉम्बिनेटरी लॉजिक पर करी की पुस्तक की प्रस्तावना में स्पष्ट प्रतिस्थापनों का चित्रण किया गया था[2] और उदाहरण के लिए, खुद ब खुद द्वारा उपयोग की गई एक 'कार्यान्वयन चाल' से विकसित हुआ, और लैम्ब्डा कैलकुलस और पुनर्लेखन सिद्धांत में एक सम्मानजनक वाक्यविन्यास सिद्धांत बन गया। हालाँकि इसकी उत्पत्ति वास्तव में निकोलस गोवर्ट डी ब्रुइज़न से हुई थी,[3] एक विशिष्ट कैलकुलस का विचार जहां प्रतिस्थापन वस्तु भाषा का हिस्सा है, न कि अनौपचारिक मेटा-सिद्धांत का, पारंपरिक रूप से मार्टिन आबादी, लुका कार्डेली, क्यूरियन और लेवी को श्रेय दिया जाता है। उनका मौलिक पेपर[4] λσ कैलकुलस पर बताया गया है कि प्रतिस्थापन से निपटने के दौरान लैम्ब्डा कैलकुलस के कार्यान्वयन को बहुत सावधान रहने की आवश्यकता है। संरचना-साझाकरण के लिए परिष्कृत तंत्र के बिना, प्रतिस्थापन आकार में विस्फोट का कारण बन सकता है, और इसलिए, व्यवहार में, प्रतिस्थापन में देरी होती है और स्पष्ट रूप से दर्ज की जाती है। इससे सिद्धांत और कार्यान्वयन के बीच पत्राचार अत्यधिक गैर-तुच्छ हो जाता है और कार्यान्वयन की शुद्धता स्थापित करना कठिन हो सकता है। एक समाधान यह है कि प्रतिस्थापनों को कलन का हिस्सा बनाया जाए, यानी स्पष्ट प्रतिस्थापनों का कलन रखा जाए।
हालाँकि, एक बार प्रतिस्थापन को स्पष्ट कर दिया गया है, तो प्रतिस्थापन के मूल गुण अर्थ संबंधी से वाक्यात्मक गुणों में बदल जाते हैं। एक सबसे महत्वपूर्ण उदाहरण प्रतिस्थापन लेम्मा है, जो λx के अंकन के साथ बन जाता है
- (M〈x:=N〉)〈y:=P〉 = (M〈y:=P〉)〈x:=(N〈y:=P〉)〉 (जहाँ x≠y और x मुक्त नहीं हैं पी)
मेलियस के कारण एक आश्चर्यजनक प्रति-उदाहरण,[5] दर्शाता है कि जिस तरह से यह नियम स्पष्ट प्रतिस्थापनों की मूल गणना में एन्कोड किया गया है वह मजबूत सामान्यीकरण नहीं है। इसके बाद, स्पष्ट प्रतिस्थापन कैलकुली के वाक्य-विन्यास गुणों के बीच सर्वोत्तम समझौता करने की कोशिश करते हुए अनेक कैलकुली का वर्णन किया गया।[6][7][8]
यह भी देखें
- संयोजन तर्क
- प्रतिस्थापन उदाहरण
संदर्भ
- ↑ Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans; Birkedal, Lars (27 April 2017). "The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types". Logical Methods in Computer Science. 12 (3): 36. arXiv:1606.09455. doi:10.2168/LMCS-12(3:7)2016.
- ↑ Curry, Haskell; Feys, Robert (1958). कॉम्बिनेटरी लॉजिक वॉल्यूम I. Amsterdam: North-Holland Publishing Company.
- ↑ N. G. de Bruijn: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technological University Eindhoven, Netherlands, Department of Mathematics, (1978), (TH-Report), Number 78-WSK-03.
- ↑ M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375–416.
- ↑ P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328–334
- ↑ P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60–69.
- ↑ K. H. Rose, Explicit Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 (ps.gz).
- ↑ Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)
