स्पष्ट प्रतिस्थापन
कंप्यूटर विज्ञान में, लैम्ब्डा कैलकुली को स्पष्ट प्रतिस्थापन कहा जाता है यदि वे प्रतिस्थापन की प्रक्रिया की औपचारिकता पर विशेष ध्यान देते हैं। यह मानक लैम्ब्डा कैलकुलस के विपरीत है जहां बीटा कमिया द्वारा प्रतिस्थापन एक अंतर्निहित विधि से किया जाता है जो कैलकुलस के अंदर व्यक्त नहीं किया जाता है; ऐसी अंतर्निहित गणनाओं में "ताज़गी" स्थितियाँ त्रुटियों का एक प्रसिद्द स्रोत हैं। यह अवधारणा अलग-अलग क्षेत्रों में बड़ी संख्या में प्रकाशित पत्रों में दिखाई दी है जैसे कि अमूर्त मशीनों में तर्क और प्रतीकात्मक गणना का अनुमान लगाया गया है।
अवलोकन
स्पष्ट प्रतिस्थापन के साथ लैम्ब्डा कैलकुलस का एक सरल उदाहरण "λx" है, जो लैम्ब्डा कैलकुलस में शब्द का एक नया रूप जोड़ता है, अर्थात् फॉर्म M⟨x:=N⟩, जिसमें लिखा है "M जहां x को N द्वारा प्रतिस्थापित किया जाता है " . (नए शब्द का अर्थ कई प्रोग्रामिंग भाषाओं में m में समान्य मुहावरे 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〉) (M2〈x:=N〉)
- (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y और x N में मुक्त नहीं हैं)
प्रतिस्थापन को स्पष्ट करते हुए यह सूत्रीकरण अभी भी लैम्ब्डा कैलकुलस चर सम्मेलन की जटिलता को बनाय रखता है, यह सुनिश्चित करने के लिए कि अंतिम नियम पर (x≠y और x N में मुक्त नहीं है) स्थिति को प्रयुक्त करने से पहले सदैव संतुष्ट किया जाता है, कमी के समय चर के इच्छानुसार से नाम बदलने की आवश्यकता होती है।नियम प्रयुक्त करने से पहले सदैव संतुष्ट रहें। इसलिए स्पष्ट प्रतिस्थापन की कई गणनाएँ तथाकथित "नाम-मुक्त" डी ब्रुइज़न इंडेक्स नोटेशन का उपयोग करके परिवर्तनीय नामों से पूरी तरह बचती हैं।
इतिहास
कॉम्बिनेटरी लॉजिक पर करी की पुस्तक की प्रस्तावना में स्पष्ट प्रतिस्थापनों का चित्रण किया गया था[1] और उदाहरण के लिए, ऑटोमैथ द्वारा उपयोग की गई एक 'कार्यान्वयन चाल' से विकसित हुआ, और लैम्ब्डा कैलकुलस और पुनर्लेखन सिद्धांत में एक सम्मानजनक वाक्यविन्यास सिद्धांत बन गया था। चूँकि इसकी उत्पत्ति वास्तव में निकोलस गोवर्ट डी ब्रुइज़न से हुई थी,[2] एक विशिष्ट कैलकुलस का विचार जहां प्रतिस्थापन वस्तु भाषा का भाग है,और न कि अनौपचारिक मेटा-सिद्धांत का, पारंपरिक रूप से मार्टिन आपश्चात्, लुका कार्डेली, क्यूरियन और लेवी को श्रेय दिया जाता है। उनका मौलिक पेपर[3] λσ कैलकुलस पर बताया गया है कि प्रतिस्थापन से निपटने के समय लैम्ब्डा कैलकुलस के कार्यान्वयन को बहुत सावधान रहने की आवश्यकता है। संरचना-साझाकरण के लिए परिष्कृत तंत्र के बिना, प्रतिस्थापन आकार में विस्फोट का कारण बन सकता है, और इसलिए, वास्तव में, प्रतिस्थापन में देरी होती है और स्पष्ट रूप से अंकित की जाती है। इससे सिद्धांत और कार्यान्वयन के बीच पत्राचार अत्यधिक गैर-तुच्छ हो जाता है और कार्यान्वयन की शुद्धता स्थापित करना कठिन हो सकता है। एक समाधान यह है कि प्रतिस्थापनों को कलन का भाग बनाया जाए, अथार्त स्पष्ट प्रतिस्थापनों का कलन रखा जाता है।
चूँकि एक बार प्रतिस्थापन को स्पष्ट कर दिया गया है, तो प्रतिस्थापन के मूल गुण अर्थ संबंधी से वाक्यात्मक गुणों में बदल जाते हैं। एक सबसे महत्वपूर्ण उदाहरण "प्रतिस्थापन लेम्मा" है जो λx के अंकन के साथ बन जाता है
- (M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (जहाँ x≠y और x मुक्त P नहीं हैं )
मेलियस के कारण एक आश्चर्यजनक प्रति-उदाहरण,[4] दर्शाता है कि जिस तरह से यह नियम स्पष्ट प्रतिस्थापनों की मूल गणना में एन्कोड किया गया है वह शसक्त सामान्यीकरण नहीं है। इसके पश्चात् स्पष्ट प्रतिस्थापन कैलकुली के वाक्य-विन्यास गुणों के बीच सर्वोत्तम समझौता करने का प्रयाश करते हुए अनेक कैलकुली का वर्णन किया गया था।[5][6][7]
यह भी देखें
- संयोजन तर्क
- प्रतिस्थापन उदाहरण
संदर्भ
- ↑ 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)
