स्पष्ट प्रतिस्थापन: Difference between revisions

From Vigyanwiki
(Created page with "{{Technical|date=May 2023}} {{merge to|Lambda calculus|discuss=talk:Explicit substitution|date=May 2023}} कंप्यूटर विज्ञान में, ल...")
 
No edit summary
Line 1: Line 1:
{{Technical|date=May 2023}}
कंप्यूटर विज्ञान में, लैम्ब्डा कैलकुली को स्पष्ट प्रतिस्थापन कहा जाता है यदि वे प्रतिस्थापन की प्रक्रिया की औपचारिकता पर विशेष ध्यान देते हैं। यह मानक लैम्ब्डा कैलकुलस के विपरीत है जहां बीटा कमिया द्वारा प्रतिस्थापन एक अंतर्निहित विधि से किया जाता है जो कैलकुलस के अंदर व्यक्त नहीं किया जाता है; ऐसी अंतर्निहित गणनाओं में "ताज़गी" स्थितियाँ त्रुटियों का एक प्रसिद्द स्रोत हैं। यह अवधारणा अलग-अलग क्षेत्रों में बड़ी संख्या में प्रकाशित पत्रों में दिखाई दी है जैसे कि अमूर्त मशीनों में तर्क और प्रतीकात्मक गणना का अनुमान लगाया गया है।
{{merge to|Lambda calculus|discuss=talk:Explicit substitution|date=May 2023}}


[[कंप्यूटर विज्ञान]] में, [[लैम्ब्डा कैलकुलस]] को स्पष्ट प्रतिस्थापन कहा जाता है यदि वे चर के प्रतिस्थापन की प्रक्रिया की औपचारिकता पर विशेष ध्यान देते हैं। यह मानक लैम्ब्डा कैलकुलस के विपरीत है जहां बीटा कटौती द्वारा प्रतिस्थापन एक अंतर्निहित तरीके से किया जाता है जो कैलकुलस के भीतर व्यक्त नहीं किया जाता है; ऐसी अंतर्निहित गणनाओं में ताजगी की स्थितियाँ त्रुटियों का एक कुख्यात स्रोत हैं।<ref>{{cite journal |last1=Clouston |first1=Ranald |last2=Bizjak |first2=Aleš |last3=Grathwohl |first3=Hans |last4=Birkedal |first4=Lars |title=The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |journal=Logical Methods in Computer Science |date=27 April 2017 |volume=12 |issue=3 |page=36 |doi=10.2168/LMCS-12(3:7)2016 |arxiv=1606.09455 }}</ref> यह अवधारणा विभिन्न क्षेत्रों में बड़ी संख्या में प्रकाशित पत्रों में दिखाई दी है, जैसे कि [[अमूर्त मशीन]]ें, [[विधेय तर्क]] और [[प्रतीकात्मक गणना]]।
== अवलोकन ==


== सिंहावलोकन ==
स्पष्ट प्रतिस्थापन के साथ लैम्ब्डा कैलकुलस का एक सरल उदाहरण "λx" है, जो लैम्ब्डा कैलकुलस में शब्द का एक नया रूप जोड़ता है, अर्थात् फॉर्म M⟨x:=N⟩, जिसमें लिखा है "M जहां x को N द्वारा प्रतिस्थापित किया जाता है " . (नए शब्द का अर्थ कई प्रोग्रामिंग भाषाओं में m में समान्य मुहावरे x:=N के समान है।) λx को निम्नलिखित पुनर्लेखन नियमों के साथ लिखा जा सकता है:
 
स्पष्ट प्रतिस्थापन के साथ लैम्ब्डा कैलकुलस का एक सरल उदाहरण λx है, जो लैम्ब्डा कैलकुलस में शब्द का एक नया रूप जोड़ता है, अर्थात् फॉर्म M〈x:=N〉, जो M पढ़ता है जहां x को N द्वारा प्रतिस्थापित किया जाएगा। (नए शब्द का अर्थ कई प्रोग्रामिंग भाषाओं में एम में आम मुहावरे x:=N ​​के समान है।) λx को निम्नलिखित [[पुनर्लेखन]] नियमों के साथ लिखा जा सकता है:
# (λx.M) N → M〈x:=N〉
# (λx.M) N → M〈x:=N〉
# x〈x:=N〉 → N
# x〈x:=N〉 → N
Line 13: Line 10:
# (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y और x N में मुक्त नहीं हैं)
# (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y और x N में मुक्त नहीं हैं)


प्रतिस्थापन को स्पष्ट करते हुए, यह सूत्रीकरण अभी भी लैम्ब्डा कैलकुलस चर सम्मेलन की जटिलता को बरकरार रखता है, यह सुनिश्चित करने के लिए कि अंतिम नियम पर (x≠y और x N में मुक्त नहीं है) स्थिति को लागू करने से पहले हमेशा संतुष्ट किया जाता है, कमी के दौरान चर के मनमाने ढंग से नाम बदलने की आवश्यकता होती है। नियम। इसलिए स्पष्ट प्रतिस्थापन की कई गणनाएँ तथाकथित नाम-मुक्त [[ब्राउन इंडेक्स]] नोटेशन का उपयोग करके परिवर्तनीय नामों से पूरी तरह बचती हैं।
प्रतिस्थापन को स्पष्ट करते हुए यह सूत्रीकरण अभी भी लैम्ब्डा कैलकुलस चर सम्मेलन की जटिलता को बनाय रखता है, यह सुनिश्चित करने के लिए कि अंतिम नियम पर (x≠y और x N में मुक्त नहीं है) स्थिति को प्रयुक्त करने से पहले सदैव संतुष्ट किया जाता है, कमी के समय चर के इच्छानुसार  से नाम बदलने की आवश्यकता होती है।नियम प्रयुक्त करने से पहले सदैव संतुष्ट रहें। इसलिए स्पष्ट प्रतिस्थापन की कई गणनाएँ तथाकथित "नाम-मुक्त" डी ब्रुइज़न इंडेक्स नोटेशन का उपयोग करके परिवर्तनीय नामों से पूरी तरह बचती हैं।


== इतिहास ==
== इतिहास ==


कॉम्बिनेटरी लॉजिक पर करी की पुस्तक की प्रस्तावना में स्पष्ट प्रतिस्थापनों का चित्रण किया गया था<ref>{{cite book|last1=Curry|first1=Haskell|last2=Feys|first2=Robert|title=कॉम्बिनेटरी लॉजिक वॉल्यूम I|year=1958|publisher=North-Holland Publishing Company|location=Amsterdam}}</ref>
कॉम्बिनेटरी लॉजिक पर करी की पुस्तक की प्रस्तावना में स्पष्ट प्रतिस्थापनों का चित्रण किया गया था<ref>{{cite book|last1=Curry|first1=Haskell|last2=Feys|first2=Robert|title=कॉम्बिनेटरी लॉजिक वॉल्यूम I|year=1958|publisher=North-Holland Publishing Company|location=Amsterdam}}</ref> और उदाहरण के लिए, [[ खुद ब खुद | ऑटोमैथ]] द्वारा उपयोग की गई एक 'कार्यान्वयन चाल' से विकसित हुआ, और लैम्ब्डा कैलकुलस और पुनर्लेखन सिद्धांत में एक सम्मानजनक वाक्यविन्यास सिद्धांत बन गया था। चूँकि  इसकी उत्पत्ति वास्तव में [[निकोलस गोवर्ट डी ब्रुइज़न]] से हुई थी,<ref>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. </ref> एक विशिष्ट कैलकुलस का विचार जहां प्रतिस्थापन वस्तु भाषा का भाग है,और  न कि अनौपचारिक मेटा-सिद्धांत का, पारंपरिक रूप से [[मार्टिन आबादी|मार्टिन आपश्चात् ी]], [[लुका कार्डेली]], क्यूरियन और लेवी को श्रेय दिया जाता है। उनका मौलिक पेपर<ref>M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375&ndash;416.</ref> λσ कैलकुलस पर बताया गया है कि प्रतिस्थापन से निपटने के समय लैम्ब्डा कैलकुलस के कार्यान्वयन को बहुत सावधान रहने की आवश्यकता है। संरचना-साझाकरण के लिए परिष्कृत तंत्र के बिना, प्रतिस्थापन आकार में विस्फोट का कारण बन सकता है, और इसलिए, वास्तव में, प्रतिस्थापन में देरी होती है और स्पष्ट रूप से अंकित की जाती है। इससे सिद्धांत और कार्यान्वयन के बीच पत्राचार अत्यधिक गैर-तुच्छ हो जाता है और कार्यान्वयन की शुद्धता स्थापित करना कठिन हो सकता है। एक समाधान यह है कि प्रतिस्थापनों को कलन का भाग बनाया जाए, अथार्त स्पष्ट प्रतिस्थापनों का कलन रखा जाता है।
और उदाहरण के लिए, [[ खुद ब खुद ]] द्वारा उपयोग की गई एक 'कार्यान्वयन चाल' से विकसित हुआ, और लैम्ब्डा कैलकुलस और पुनर्लेखन सिद्धांत में एक सम्मानजनक वाक्यविन्यास सिद्धांत बन गया। हालाँकि इसकी उत्पत्ति वास्तव में [[निकोलस गोवर्ट डी ब्रुइज़न]] से हुई थी,<ref>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. </ref> एक विशिष्ट कैलकुलस का विचार जहां प्रतिस्थापन वस्तु भाषा का हिस्सा है, न कि अनौपचारिक मेटा-सिद्धांत का, पारंपरिक रूप से [[मार्टिन आबादी]], [[लुका कार्डेली]], क्यूरियन और लेवी को श्रेय दिया जाता है। उनका मौलिक पेपर<ref>M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375&ndash;416.</ref> λσ कैलकुलस पर बताया गया है कि प्रतिस्थापन से निपटने के दौरान लैम्ब्डा कैलकुलस के कार्यान्वयन को बहुत सावधान रहने की आवश्यकता है। संरचना-साझाकरण के लिए परिष्कृत तंत्र के बिना, प्रतिस्थापन आकार में विस्फोट का कारण बन सकता है, और इसलिए, व्यवहार में, प्रतिस्थापन में देरी होती है और स्पष्ट रूप से दर्ज की जाती है। इससे सिद्धांत और कार्यान्वयन के बीच पत्राचार अत्यधिक गैर-तुच्छ हो जाता है और कार्यान्वयन की शुद्धता स्थापित करना कठिन हो सकता है। एक समाधान यह है कि प्रतिस्थापनों को कलन का हिस्सा बनाया जाए, यानी स्पष्ट प्रतिस्थापनों का कलन रखा जाए।
 
हालाँकि, एक बार प्रतिस्थापन को स्पष्ट कर दिया गया है, तो प्रतिस्थापन के मूल गुण अर्थ संबंधी से वाक्यात्मक गुणों में बदल जाते हैं। एक सबसे महत्वपूर्ण उदाहरण प्रतिस्थापन लेम्मा है, जो λx के अंकन के साथ बन जाता है
* (M〈x:=N〉)〈y:=P〉 = (M〈y:=P〉)〈x:=(N〈y:=P〉)〉 (जहाँ x≠y और x मुक्त नहीं हैं पी)
मेलियस के कारण एक आश्चर्यजनक प्रति-उदाहरण,<ref>P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328&ndash;334</ref> दर्शाता है कि जिस तरह से यह नियम स्पष्ट प्रतिस्थापनों की मूल गणना में एन्कोड किया गया है वह [[मजबूत सामान्यीकरण]] नहीं है। इसके बाद, स्पष्ट प्रतिस्थापन कैलकुली के वाक्य-विन्यास गुणों के बीच सर्वोत्तम समझौता करने की कोशिश करते हुए अनेक कैलकुली का वर्णन किया गया।<ref>P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60&ndash;69.</ref><ref>K. H. Rose, Explicit Substitution &ndash; Tutorial & Survey, BRICS LS-96-3, September 1996 ([http://www.brics.dk/LS/96/3/BRICS-LS-96-3.ps.gz ps.gz]).</ref><ref>Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)</ref>
 


चूँकि  एक बार प्रतिस्थापन को स्पष्ट कर दिया गया है, तो प्रतिस्थापन के मूल गुण अर्थ संबंधी से वाक्यात्मक गुणों में बदल जाते हैं। एक सबसे महत्वपूर्ण उदाहरण "प्रतिस्थापन लेम्मा" है जो λx के अंकन के साथ बन जाता है
** (M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (जहाँ x≠y और x मुक्त P नहीं हैं )
मेलियस के कारण एक आश्चर्यजनक प्रति-उदाहरण,<ref>P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328&ndash;334</ref> दर्शाता है कि जिस तरह से यह नियम स्पष्ट प्रतिस्थापनों की मूल गणना में एन्कोड किया गया है वह [[मजबूत सामान्यीकरण|शसक्त सामान्यीकरण]] नहीं है। इसके पश्चात् स्पष्ट प्रतिस्थापन कैलकुली के वाक्य-विन्यास गुणों के बीच सर्वोत्तम समझौता करने का प्रयाश करते हुए अनेक कैलकुली का वर्णन किया गया था।<ref>P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60&ndash;69.</ref><ref>K. H. Rose, Explicit Substitution &ndash; Tutorial & Survey, BRICS LS-96-3, September 1996 ([http://www.brics.dk/LS/96/3/BRICS-LS-96-3.ps.gz ps.gz]).</ref><ref>Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)</ref>
== यह भी देखें ==
== यह भी देखें ==
* संयोजन तर्क
* संयोजन तर्क

Revision as of 09:54, 15 July 2023

कंप्यूटर विज्ञान में, लैम्ब्डा कैलकुली को स्पष्ट प्रतिस्थापन कहा जाता है यदि वे प्रतिस्थापन की प्रक्रिया की औपचारिकता पर विशेष ध्यान देते हैं। यह मानक लैम्ब्डा कैलकुलस के विपरीत है जहां बीटा कमिया द्वारा प्रतिस्थापन एक अंतर्निहित विधि से किया जाता है जो कैलकुलस के अंदर व्यक्त नहीं किया जाता है; ऐसी अंतर्निहित गणनाओं में "ताज़गी" स्थितियाँ त्रुटियों का एक प्रसिद्द स्रोत हैं। यह अवधारणा अलग-अलग क्षेत्रों में बड़ी संख्या में प्रकाशित पत्रों में दिखाई दी है जैसे कि अमूर्त मशीनों में तर्क और प्रतीकात्मक गणना का अनुमान लगाया गया है।

अवलोकन

स्पष्ट प्रतिस्थापन के साथ लैम्ब्डा कैलकुलस का एक सरल उदाहरण "λx" है, जो लैम्ब्डा कैलकुलस में शब्द का एक नया रूप जोड़ता है, अर्थात् फॉर्म M⟨x:=N⟩, जिसमें लिखा है "M जहां x को N द्वारा प्रतिस्थापित किया जाता है " . (नए शब्द का अर्थ कई प्रोग्रामिंग भाषाओं में m में समान्य मुहावरे x:=N के समान है।) λx को निम्नलिखित पुनर्लेखन नियमों के साथ लिखा जा सकता है:

  1. (λx.M) N → M〈x:=N〉
  2. x〈x:=N〉 → N
  3. x〈y:=N〉 → x (x≠y)
  4. (एम1M2) 〈x:=N〉 → (एम1〈x:=N〉) (एम2〈x:=N〉)
  5. (λ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]

यह भी देखें

संदर्भ

  1. ↑ Curry, Haskell; Feys, Robert (1958). कॉम्बिनेटरी लॉजिक वॉल्यूम I. Amsterdam: North-Holland Publishing Company.
  2. ↑ 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.
  3. ↑ M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375–416.
  4. ↑ P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328–334
  5. ↑ P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60–69.
  6. ↑ K. H. Rose, Explicit Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 (ps.gz).
  7. ↑ Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=स्पष्ट_प्रतिस्थापन&oldid=224223’