संचालनात्मक शब्दार्थ: Difference between revisions

Revision as of 16:15, 5 August 2023

ऑपरेशनल सेमेन्टिक्स औपचारिक लैंगवेज सेमेन्टिक्स (कंप्यूटर विज्ञान) की श्रेणी है जिसमें कंप्यूटर प्रोग्राम के कुछ वांछित गुण, जैसे शुद्धता, सुरक्षा या संरक्षा, को उसके शब्दों में गणितीय अर्थ जोड़ने के अतिरिक्त उसके निष्पादन एवं प्रक्रियाओं के विषय में तार्किक बयानों से प्रमाण बनाकर सत्यापित किया जाता है। ऑपरेशनल सिमेंटिक्स को दो श्रेणियों में वर्गीकृत किया गया है: संरचनात्मक ऑपरेशनल सिमेंटिक्स (या छोटे-चरण वाले सिमेंटिक्स) औपचारिक रूप से वर्णन करते हैं कि कंप्यूटर-आधारित सिस्टम में गणना के व्यक्तिगत चरण कैसे होते हैं; विपक्षी प्राकृतिक सिमेंटिक्स (या बड़े-चरण वाले सिमेंटिक्स) द्वारा वर्णन किया जाता है कि निष्पादन के समग्र परिणाम कैसे प्राप्त होते हैं। प्रोग्रामिंग लैंगवेजो का औपचारिक सिमेंटिक्स प्रदान करने के अन्य उपायों में स्वयंसिद्ध सिमेंटिक्स एवं सांकेतिक सिमेंटिक्स सम्मिलित हैं।

प्रोग्रामिंग लैंगवेज के लिए परिचालन सिमेंटिक्स यह बताता है कि वैध प्रोग्राम को कम्प्यूटेशनल चरणों के अनुक्रम के रूप में कैसे समझा जाता है। ये अनुक्रम तब प्रोग्राम का अर्थ हैं। कार्यात्मक प्रोग्रामिंग के संदर्भ में, समापन अनुक्रम में अंतिम चरण प्रोग्राम का मान लौटाता है। सामान्यतः ही प्रोग्राम के लिए कई रिटर्न मान हो सकते हैं, क्योंकि प्रोग्राम अन्य-नियतात्मक एल्गोरिथ्म हो सकता है, एवं यहां तक कि नियतात्मक प्रोग्राम के लिए कई गणना अनुक्रम भी हो सकते हैं क्योंकि सिमेंटिक्स यह निर्दिष्ट नहीं कर सकता है कि संचालन का कौन सा क्रम उस मूल्य पर आता है।

शायद परिचालन सिमेंटिक्स का प्रथम औपचारिक अवतार लिस्प (प्रोग्रामिंग लैंगवेज) के सिमेंटिक्स को परिभाषित करने के लिए लैम्ब्डा कैलकुलस का उपयोग था।^[1] एसईसीडी मशीन की परंपरा में सार मशीन भी निकटता से संबंधित हैं।

इतिहास

ALGOL 68 के सिमेंटिक्स को परिभाषित करने में प्रथम बार परिचालन सिमेंटिक्स की अवधारणा का उपयोग किया गया था। निम्नलिखित कथन संशोधित ALGOL 68 रिपोर्ट का उद्धरण है:

सख्त लैंगवेज में किसी प्रोग्राम का अर्थ काल्पनिक कंप्यूटर के संदर्भ में समझाया गया है जो उस प्रोग्राम के विस्तार को बनाने वाली क्रियाओं का समूह निष्पादित करता है।

ऑपरेशनल सिमेंटिक्स शब्द का इसके वर्तमान अर्थ में प्रथम उपयोग दाना स्कॉट (plotkin04) को दिया गया है।औपचारिक सिमेंटिक्स विज्ञान पर स्कॉट के मौलिक पेपर का उद्धरण इस प्रकार है, जिसमें उन्होंने सिमेंटिक्स के परिचालन पहलुओं का उल्लेख किया है।

सिमेंटिक्स के प्रति अधिक 'सार' एवं 'स्वच्छ' दृष्टिकोण का लक्ष्य रखना बहुत उचित विषय है, किन्तु यदि योजना उचित होनी है, तो परिचालन पहलुओं को पूर्ण रूप से अस्वीकार नहीं किया जा सकता है।

दृष्टिकोण

गॉर्डन प्लॉटकिन ने स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स, मैथ्यू फेलिसेन एवं रॉबर्ट हीब ने कमी सिमेंटिक्स,^[2] एवं गाइल्स कहन ने प्राकृतिक सिमेंटिक्स का प्रारम्भ किया था।

लघु-चरण सिमेंटिक्स

स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स

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

सरल उदाहरण के लिए, हम साधारण प्रोग्रामिंग लैंगवेज के सिमेंटिक्स के भाग पर विचार करते हैं; plotkin81 एवं hennessy90, एवं अन्य पाठ्यपुस्तकों में उचित चित्रण दिए गए हैं। $C_{1},C_{2}$ लैंगवेज के प्रोग्रामों की रेंज, एवं विभिन्न अवस्थाओं $s$ में सीमा होती है। यदि हमारे पास अभिव्यक्तियाँ (क्रमानुसार $E$ ), मान ( $V$ ) एवं स्थान ( $L$ ) हैं, तो मेमोरी अपडेट कमांड में सिमेंटिक्स

${\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}$ होता है। अनौपचारिक रूप से, नियम कहता है कि यदि अभिव्यक्ति $E$ अवस्था $s$ में मूल्य $V$ कम कर देता है, तत्पश्चात प्रोग्राम $L:=E$ अवस्था $s$ को असाइनमेंट $L=V$ के साथ अद्यतन करता है।

अनुक्रमण का सिमेंटिक्स निम्नलिखित तीन नियमों द्वारा दिया जा सकता है:

${\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}$ अनौपचारिक रूप से, प्रथम नियम कहता है कि यदि अवस्था $s$ में प्रोग्राम $C_{1}$ अवस्था $s'$ में समाप्त होता है, तत्पश्चात प्रोग्राम $C_{1};C_{2}$ अवस्था $s$ में प्रोग्राम $C_{2}$ अवस्था में $s'$ में कमी आएगी। (आप इसे औपचारिकता के रूप में सोच सकते हैं, $C_{1}$ , एवं तत्पश्चात $C_{2}$ परिणामी मेमोरी स्टोर का उपयोग करना कर सकते हैं।) दूसरा नियम यही कहता है, यदि प्रोग्राम $C_{1}$ अवस्था $s$ में प्रोग्राम $C_{1}'$ अवस्था $s'$ के साथ कम कर सकते हैं, तत्पश्चात प्रोग्राम $C_{1};C_{2}$ अवस्था $s$ में प्रोग्राम $C_{1}';C_{2}$ अवस्था $s'$ में कमी आएगी, आप इसे अनुकूलन कंपाइलर के लिए सिद्धांत को औपचारिक बनाने के रूप में सोच सकते हैं: "आपको परिवर्तन करने की अनुमति है जैसे कि यह $C_{1}$ अकेले ही हो, भले ही यह किसी प्रोग्राम का प्रथम भाग ही क्यों न हो।"

सिमेंटिक्स संरचनात्मक है, क्योंकि अनुक्रमिक प्रोग्राम $C_{1};C_{2}$ , $C_{1}$ एवं $C_{2}$ के अर्थ से परिभाषित किया गया है।

यदि हमारे पास अवस्था पर बूलियन अभिव्यक्तियाँ भी हैं, तो सीमा से अधिक $B$ , तो हम while कमांड के सिमेंटिक्स को परिभाषित कर सकते हैं: ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$ ऐसी परिभाषा प्रोग्रामों के व्यवहार के औपचारिक विश्लेषण की अनुमति देती है, प्रोग्रामों के मध्य संबंध के अध्ययन की अनुमति देती है। महत्वपूर्ण संबंधों में अनुकरण पूर्वआदेश एवं द्विसिमुलेशन सम्मिलित हैं। ये समवर्ती सिद्धांत के संदर्भ में विशेष रूप से उपयोगी हैं।

इसके सहज स्वरूप एवं अनुसरण करने में सरल संरचना के लिए धन्यवाद, एसओएस ने लोकप्रियता प्राप्त की है एवं परिभाषित करने में यह वास्तविक मानक बन गया है। परिचालन सिमेंटिक्स सफलता के संकेत के रूप में, मूल रिपोर्ट (तथाकथित आरहूस रिपोर्ट) CiteSeer [1] के अनुसार 1000 से अधिक उद्धरण आकर्षित किए हैं। इसे कंप्यूटर विज्ञान में सर्वाधिक उद्धृत प्रौद्योगिकी रिपोर्टों में से एक बना दिया गया है।

रिडक्शन सिमेंटिक्स

रिडक्शन सिमेंटिक्स परिचालन सिमेंटिक्स की वैकल्पिक प्रस्तुति है। इसके मुख्य विचारों को प्रथम बार 1975 में गॉर्डन प्लॉटकिन द्वारा लैम्ब्डा कैलकुलस के नाम एवं कॉल द्वारा मूल्य वेरिएंट के अनुसार पूर्ण रूप से कार्यात्मक कॉल पर प्रस्तुत किया गया था।^[3] एवं अपने 1987 के शोध प्रबंध में मैथियास फेलिसेन द्वारा अनिवार्य विशेषताओं के साथ उच्च-क्रम कार्यात्मक लैंगवेजों के लिए सामान्यीकृत किया गया।^[4] इस विधि को 1992 में मैथियास फेलिसेन एवं रॉबर्ट हीब द्वारा नियंत्रण प्रवाह एवं प्रोग्राम समष्टि के लिए पूर्ण समीकरण सिद्धांत में विस्तारित किया गया था।^[2]वाक्यांश "रिडक्शन सिमेंटिक्स" प्रथम बार फेलिसेन एवं फ्रीडमैन द्वारा PARLE 1987 के पेपर में गढ़ा गया था।^[5]रिडक्शन सिमेंटिक्स को कमी नियमों के सेट के रूप में दिया गया है, जिनमें से प्रत्येक संभावित कमी चरण को निर्दिष्ट करता है। उदाहरण के लिए, निम्नलिखित न्यूनीकरण नियम में कहा गया है कि असाइनमेंट स्टेटमेंट को कम किया जा सकता है यदि वह अपने परिवर्तनीय घोषणा के ठीक बगल में बैठता है:

$\mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e$ असाइनमेंट स्टेटमेंट को ऐसी समष्टि में लाने के लिए इसे फ़ंक्शन एप्लिकेशन एवं असाइनमेंट स्टेटमेंट के दाईं ओर के माध्यम से "बबल अप" किया जाता है जब तक कि यह उचित बिंदु तक नहीं पहुंच जाता है। हस्तक्षेप करने के पश्चात से $\mathbf {let}$ अभिव्यक्ति भिन्न-भिन्न वेरिएंट घोषित कर सकती है, कैलकुलस भी $\mathbf {let}$ भाव के लिए एक्सट्रूज़न नियम की मांग करता है। रिडक्शन सिमेंटिक्स के अधिकांश प्रकाशित उपयोग मूल्यांकन संदर्भों की सुविधा के साथ ऐसे "बबल नियमों" को परिभाषित करते हैं। उदाहरण के लिए, मूल्य लैंगवेज द्वारा साधारण कॉल में मूल्यांकन संदर्भों का व्याकरण इस प्रकार दिया जा सकता है,

$E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e$ जहाँ $e$ अभिव्यक्ति को दर्शाता है एवं $v$ पूर्ण रूप से कम किए गए मूल्यों को दर्शाता है। प्रत्येक मूल्यांकन संदर्भ में छेद $[\,]$ सम्मिलित होता है जिसमें शब्द को कैप्वेरिएंटिंग फैशन में प्लग किया गया है। संदर्भ का आकार इस छेद से इंगित करता है कि कहां कमी हो सकती है। मूल्यांकन संदर्भों की सहायता से "बुलबुले" का वर्णन करने के लिए, एकल सिद्धांत पर्याप्त है:

$E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}$ यह एकल न्यूनीकरण नियम असाइनमेंट स्टेटमेंट के लिए फेलिसेन एवं हिएब के लैम्ब्डा कैलकुलस से लिफ्ट नियम है। मूल्यांकन संदर्भ इस नियम को कुछ शर्तों तक सीमित रखते हैं, किन्तु यह लैम्ब्डा सहित किसी भी अवधि में स्वतंत्र रूप से प्रस्तुत होता है।

प्लॉटकिन के पश्चात, न्यूनीकरण नियमों के सेट से प्राप्त कैलकुलस की उपयोगिता दिखाते हुए (1) चरण संबंध के लिए वेरिएंट्च-रोसेर लेम्मा की मांग की जाती है, जो मूल्यांकन फ़ंक्शन को प्रेरित करता है, एवं (2) चरण संबंध के ट्रांजिटिव-रिफ्लेक्टिव क्लोजर के लिए करी-फ़े मानकीकरण लेम्मा, जो मूल्यांकन फ़ंक्शन में अन्य-नियतात्मक शोध को नियतात्मक बाएं-सबसे बाहरी शोध से परिवर्तित कर देता है। फ़ेलिसेन ने दिखाया कि इस कलन के अनिवार्य विस्तार इन प्रमेयों को संतुष्ट करते हैं। इन प्रमेयों का परिणाम यह है कि समीकरण सिद्धांत - सममित-संक्रमणीय-प्रतिवर्ती समापन इन लैंगवेजों के लिए ठोस तर्क सिद्धांत है। चूँकि, व्यवहार में, रिडक्शन सिमेंटिक्स के अधिकांश अनुप्रयोग कैलकुलस से दूर हो जाते हैं एवं केवल मानक न्यूनीकरण (एवं मूल्यांकनकर्ता जो इससे प्राप्त किया जा सकता है) का उपयोग करते हैं।

रिडक्शन सिमेंटिक्स विशेष रूप से उपयोगी होते हैं, जिससे सरली से मूल्यांकन संदर्भ अवस्था या असामान्य नियंत्रण संरचनाओं (उदाहरण के लिए, प्रथम श्रेणी निरंतरता) को प्रारूप कर सकते हैं। इसके अतिरिक्त, वस्तु उन्मुख लैंगवेजों^[6] अनुबंध, अपवाद, वायदा, कॉल-बाय-नीड एवं कई अन्य लैंगवेज सुविधाओं को प्रारूप करने के लिए रिडक्शन सिमेंटिक्स का उपयोग किया गया है। रिडक्शन सिमेंटिक्स विज्ञान का संपूर्ण, आधुनिक उपचार जो ऐसे कई अनुप्रयोगों पर विस्तार से वेरिएंट्चा करता है, पीएलटी रेडेक्स के साथ सिमेंटिक्स इंजीनियरिंग में मैथियास फेलिसेन, रॉबर्ट ब्रूस फाइंडलर एवं मैथ्यू फ़्लैट द्वारा दिया गया है।^[7]

बड़ा चरण सिमेंटिक्स

प्राकृतिक सिमेंटिक्स

बिग-स्टेप स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स को प्राकृतिक सिमेंटिक्स, रिलेशनल सिमेंटिक्स एवं मूल्यांकन सिमेंटिक्स के नाम से भी जाना जाता है।^[8] मिनी-एमएल, एमएल (प्रोग्रामिंग लैंगवेज) की शुद्ध लैंगवेज प्रस्तुत करते समय गाइल्स काह्न द्वारा बिग-स्टेप ऑपरेशनल सिमेंटिक्स को प्राकृतिक सिमेंटिक्स के नाम से प्रस्तुत किया गया था।

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

बड़ा चरण सिमेंटिक्स डिवाइड एंड कांकेर विधि से वर्णन करता है कि कैसे लैंगवेज निर्माण के अंतिम मूल्यांकन परिणाम उनके वाक्यात्मक समकक्षों (उपअभिव्यक्ति, उपकथन, आदि) के मूल्यांकन परिणामों को मिलाकर प्राप्त किए जा सकते हैं।

अपेक्षा

छोटे-चरण एवं बड़े-चरण वाले सिमेंटिक्स के मध्य कई अंतर हैं जो प्रभावित करते हैं कि प्रोग्रामिंग लैंगवेज के सिमेंटिक्स को निर्दिष्ट करने के लिए कोई दूसरा अधिक उपयुक्त आधार बनाता है या नहीं बनाता है।

बड़े-चरण वाले सिमेंटिक्स प्रायः सरल होते हैं (कम अनुमान नियमों की आवश्यकता होती है) एवं प्रायः सीधे लैंगवेज के लिए दुभाषिया के कुशल कार्यान्वयन के अनुरूप होते हैं (इसलिए कहन उन्हें प्राकृतिक कहते हैं।) दोनों सरल प्रमाणों की ओर ले जा सकते हैं, उदाहरण के लिए जब कुछ प्रोग्राम परिवर्तन के अंतर्गत शुद्धता के संरक्षण को प्रमाणित किया जाता है।^[9]बड़े-चरण वाले सिमेंटिक्स की मुख्य हानि यह है कि अन्य-समाप्ति विचलन गणनाओं में कोई अनुमान वृक्ष नहीं होता है, जिससे ऐसी गणनाओं के विषय में गुणों को बताना एवं प्रमाणित करना असंभव हो जाता है।^[9]

छोटे-चरण वाले सिमेंटिक्स विवरण एवं मूल्यांकन के क्रम पर अधिक नियंत्रण देते हैं। इंस्ट्रुमेंटेड ऑपरेशनल सिमेंटिक्स के विषय में, यह ऑपरेशनल सिमेंटिक्स को ट्रैक करने एवं सिमेंटिस्ट को लैंगवेज के रन-टाइम व्यवहार के विषय में अधिक त्रुटिहीन प्रमेयों को बताने एवं प्रमाणित करने की अनुमति देता है। परिचालन सिमेंटिक्स के विरुद्ध प्रकार की सिस्टम की प्रकार की सुदृढ़ता प्रमाणित करते समय ये गुण छोटे-चरण के सिमेंटिक्स को अधिक सुविधाजनक बनाते हैं।^[9]

यह भी देखें

बीजगणितीय सिमेंटिक्स (कंप्यूटर विज्ञान)
स्वयंसिद्ध सिमेंटिक्स
सांकेतिक सिमेंटिक्स
प्रोग्रामिंग लैंगवेजों का औपचारिक सिमेंटिक्स

संदर्भ

↑ McCarthy, John. "प्रतीकात्मक अभिव्यक्तियों के पुनरावर्ती कार्य और मशीन द्वारा उनकी गणना, भाग I". Archived from the original on 2013-10-04. Retrieved 2006-10-13.
↑ ^2.0 ^2.1 Felleisen, M.; Hieb, R. (1992). "अनुक्रमिक नियंत्रण और राज्य के वाक्यात्मक सिद्धांतों पर संशोधित रिपोर्ट". Theoretical Computer Science. 103 (2): 235–271. doi:10.1016/0304-3975(92)90014-7.
↑ Plotkin, Gordon (1975). "Call-by-name, call-by-value and the λ-calculus" (PDF). Theoretical Computer Science. 1 (2): 125–159. doi:10.1016/0304-3975(75)90017-1. Retrieved July 22, 2021.
↑ Felleisen, Matthias (1987). The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (PhD). Indiana University. Retrieved July 22, 2021.
↑ Felleisen, Matthias; Friedman, Daniel P. (1987). "अनिवार्य उच्च-क्रम भाषाओं के लिए एक न्यूनीकरण शब्दार्थ". Proceedings of the Parallel Architectures and Languages Europe. International Conference on Parallel Architectures and Languages Europe. Vol. 1. Springer-Verlag. pp. 206–223. doi:10.1007/3-540-17945-3_12.
↑ Abadi, M.; Cardelli, L. (8 September 2012). वस्तुओं का एक सिद्धांत. ISBN 9781441985989.
↑ Felleisen, Matthias; Findler, Robert Bruce; Flatt, Matthew (2009). पीएलटी रिडेक्स के साथ सिमेंटिक्स इंजीनियरिंग. The MIT Press. ISBN 978-0-262-06275-6.
↑ University of Illinois CS422
↑ ^9.0 ^9.1 ^9.2 Xavier Leroy. "Coinductive big-step operational semantics".

अग्रिम पठन

Gilles Kahn. "Natural Semantics". Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science. Springer-Verlag. London. 1987.
Gordon D. Plotkin. A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), preprint).
Gordon D. Plotkin. The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. (preprint).
Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
Adriaan van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ([2]^{[permanent dead link]})
Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. available online.

बाहरी संबंध

Media related to संचालनात्मक शब्दार्थ at Wikimedia Commons

[1] McCarthy, John. "प्रतीकात्मक अभिव्यक्तियों के पुनरावर्ती कार्य और मशीन द्वारा उनकी गणना, भाग I". Archived from the original on 2013-10-04. Retrieved 2006-10-13.

[felleisen-hieb-92-2] 2.0 ^2.1 Felleisen, M.; Hieb, R. (1992). "अनुक्रमिक नियंत्रण और राज्य के वाक्यात्मक सिद्धांतों पर संशोधित रिपोर्ट". Theoretical Computer Science. 103 (2): 235–271. doi:10.1016/0304-3975(92)90014-7.

[3] Plotkin, Gordon (1975). "Call-by-name, call-by-value and the λ-calculus" (PDF). Theoretical Computer Science. 1 (2): 125–159. doi:10.1016/0304-3975(75)90017-1. Retrieved July 22, 2021.

[4] Felleisen, Matthias (1987). The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages (PDF) (PhD). Indiana University. Retrieved July 22, 2021.

[5] Felleisen, Matthias; Friedman, Daniel P. (1987). "अनिवार्य उच्च-क्रम भाषाओं के लिए एक न्यूनीकरण शब्दार्थ". Proceedings of the Parallel Architectures and Languages Europe. International Conference on Parallel Architectures and Languages Europe. Vol. 1. Springer-Verlag. pp. 206–223. doi:10.1007/3-540-17945-3_12.

[6] Abadi, M.; Cardelli, L. (8 September 2012). वस्तुओं का एक सिद्धांत. ISBN 9781441985989.

[7] Felleisen, Matthias; Findler, Robert Bruce; Flatt, Matthew (2009). पीएलटी रिडेक्स के साथ सिमेंटिक्स इंजीनियरिंग. The MIT Press. ISBN 978-0-262-06275-6.

[8] University of Illinois CS422

[leroy-coinductivebigstep-9] 9.0 ^9.1 ^9.2 Xavier Leroy. "Coinductive big-step operational semantics".

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

@@ Line 2: / Line 2: @@
 {{Semantics}}
-'''ऑपरेशनल सेमेन्टिक्स''' [[औपचारिक भाषा|औपचारिक लैंगवेज]] सेमेन्टिक्स (कंप्यूटर विज्ञान) की श्रेणी है जिसमें [[कंप्यूटर प्रोग्राम]] के कुछ वांछित गुण, जैसे शुद्धता, सुरक्षा या संरक्षा, को उसके शब्दों में गणितीय अर्थ जोड़ने के अतिरिक्त उसके [[निष्पादन (कंप्यूटिंग)|निष्पादन]] एवं प्रक्रियाओं के विषय में तार्किक बयानों से [[गणितीय प्रमाण|प्रमाण]] बनाकर [[औपचारिक सत्यापन|सत्यापित]] किया जाता है। ऑपरेशनल सिमेंटिक्स को दो श्रेणियों में वर्गीकृत किया गया है: संरचनात्मक ऑपरेशनल सिमेंटिक्स (या छोटे-चरण वाले सिमेंटिक्स) औपचारिक रूप से वर्णन करते हैं कि कंप्यूटर-आधारित प्रणाली में [[गणना]] के व्यक्तिगत चरण कैसे होते हैं; विपक्षी प्राकृतिक सिमेंटिक्स (या बड़े-चरण वाले सिमेंटिक्स) द्वारा वर्णन किया जाता है कि निष्पादन के समग्र परिणाम कैसे प्राप्त होते हैं। [[प्रोग्रामिंग भाषा|प्रोग्रामिंग लैंगवेजो]] का औपचारिक सिमेंटिक्स प्रदान करने के अन्य उपायों में [[स्वयंसिद्ध शब्दार्थ|स्वयंसिद्ध सिमेंटिक्स]] एवं सांकेतिक सिमेंटिक्स सम्मिलित हैं।
+'''ऑपरेशनल सेमेन्टिक्स''' [[औपचारिक भाषा|औपचारिक लैंगवेज]] सेमेन्टिक्स (कंप्यूटर विज्ञान) की श्रेणी है जिसमें [[कंप्यूटर प्रोग्राम]] के कुछ वांछित गुण, जैसे शुद्धता, सुरक्षा या संरक्षा, को उसके शब्दों में गणितीय अर्थ जोड़ने के अतिरिक्त उसके [[निष्पादन (कंप्यूटिंग)|निष्पादन]] एवं प्रक्रियाओं के विषय में तार्किक बयानों से [[गणितीय प्रमाण|प्रमाण]] बनाकर [[औपचारिक सत्यापन|सत्यापित]] किया जाता है। ऑपरेशनल सिमेंटिक्स को दो श्रेणियों में वर्गीकृत किया गया है: संरचनात्मक ऑपरेशनल सिमेंटिक्स (या छोटे-चरण वाले सिमेंटिक्स) औपचारिक रूप से वर्णन करते हैं कि कंप्यूटर-आधारित सिस्टम में [[गणना]] के व्यक्तिगत चरण कैसे होते हैं; विपक्षी प्राकृतिक सिमेंटिक्स (या बड़े-चरण वाले सिमेंटिक्स) द्वारा वर्णन किया जाता है कि निष्पादन के समग्र परिणाम कैसे प्राप्त होते हैं। [[प्रोग्रामिंग भाषा|प्रोग्रामिंग लैंगवेजो]] का औपचारिक सिमेंटिक्स प्रदान करने के अन्य उपायों में [[स्वयंसिद्ध शब्दार्थ|स्वयंसिद्ध सिमेंटिक्स]] एवं सांकेतिक सिमेंटिक्स सम्मिलित हैं।
-प्रोग्रामिंग लैंगवेज के लिए परिचालन सिमेंटिक्स यह बताता है कि वैध प्रोग्राम को कम्प्यूटेशनल चरणों के अनुक्रम के रूप में कैसे समझा जाता है। ये अनुक्रम तब प्रोग्रामका अर्थ हैं। [[कार्यात्मक प्रोग्रामिंग]] के संदर्भ में, समापन अनुक्रम में अंतिम चरण प्रोग्राम का मान लौटाता है। सामान्यतः ही प्रोग्राम के लिए कई रिटर्न मान हो सकते हैं, क्योंकि प्रोग्राम [[गैर-नियतात्मक एल्गोरिथ्म|अन्य-नियतात्मक एल्गोरिथ्म]] हो सकता है, एवं यहां तक कि नियतात्मक प्रोग्राम के लिए कई गणना अनुक्रम भी हो सकते हैं क्योंकि सिमेंटिक्स यह निर्दिष्ट नहीं कर सकता है कि संचालन का कौन सा क्रम उस मूल्य पर आता है।
+प्रोग्रामिंग लैंगवेज के लिए परिचालन सिमेंटिक्स यह बताता है कि वैध प्रोग्राम को कम्प्यूटेशनल चरणों के अनुक्रम के रूप में कैसे समझा जाता है। ये अनुक्रम तब प्रोग्राम का अर्थ हैं। [[कार्यात्मक प्रोग्रामिंग]] के संदर्भ में, समापन अनुक्रम में अंतिम चरण प्रोग्राम का मान लौटाता है। सामान्यतः ही प्रोग्राम के लिए कई रिटर्न मान हो सकते हैं, क्योंकि प्रोग्राम [[गैर-नियतात्मक एल्गोरिथ्म|अन्य-नियतात्मक एल्गोरिथ्म]] हो सकता है, एवं यहां तक कि नियतात्मक प्रोग्राम के लिए कई गणना अनुक्रम भी हो सकते हैं क्योंकि सिमेंटिक्स यह निर्दिष्ट नहीं कर सकता है कि संचालन का कौन सा क्रम उस मूल्य पर आता है।
 शायद परिचालन सिमेंटिक्स का प्रथम औपचारिक अवतार [[लिस्प (प्रोग्रामिंग भाषा)|लिस्प (प्रोग्रामिंग लैंगवेज)]] के सिमेंटिक्स को परिभाषित करने के लिए [[लैम्ब्डा कैलकुलस]] का उपयोग था।<ref>{{Cite web |title=प्रतीकात्मक अभिव्यक्तियों के पुनरावर्ती कार्य और मशीन द्वारा उनकी गणना, भाग I|last=McCarthy |first=John |author-link=John McCarthy (computer scientist) |url=http://www-formal.stanford.edu/jmc/recursive.html |access-date=2006-10-13 |url-status=dead |archive-url=https://web.archive.org/web/20131004215327/http://www-formal.stanford.edu/jmc/recursive.html |archive-date=2013-10-04}}</ref> [[एसईसीडी मशीन]] की परंपरा में [[सार मशीन|सार]] [[एसईसीडी मशीन|मशीन]] भी निकटता से संबंधित हैं।
@@ Line 23: / Line 23: @@
 ==== स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स ====
-स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स (एसओएस, जिसे स्ट्रक्वेरिएंट्ड ऑपरेशनल सिमेंटिक्स या स्मॉल-स्टेप सिमेंटिक्स भी कहा जाता है) को गॉर्डन प्लॉटकिन ने (plotkin81) ऑपरेशनल सिमेंटिक्स को परिभाषित करने के तार्किक साधन के रूप में प्रस्तुत किया था। एसओएस के पीछे मूल विचार किसी प्रोग्राम के व्यवहार को उसके भागों के व्यवहार के संदर्भ में परिभाषित करना है, इस प्रकार संरचनात्मक, अर्थात, वाक्यविन्यास-उन्मुख एवं [[आगमनात्मक परिभाषा]], परिचालन सिमेंटिक्स पर दृष्टिकोण प्रदान करना है। एसओएस विनिर्देश [[राज्य संक्रमण प्रणाली|अवस्था संक्रमण प्रणाली]] के सेट के संदर्भ में  प्रोग्राम के व्यवहार को परिभाषित करता है। एसओएस विनिर्देश [[अनुमान नियम|अनुमान नियमों]] के सेट का रूप लेते हैं जो इसके घटकों के संक्रमण के संदर्भ में वाक्यविन्यास के समग्र भागों के वैध परिवर्तन को परिभाषित करते हैं।
+स्ट्रक्वेरिएंटल ऑपरेशनल सिमेंटिक्स (एसओएस, जिसे स्ट्रक्वेरिएंट्ड ऑपरेशनल सिमेंटिक्स या स्मॉल-स्टेप सिमेंटिक्स भी कहा जाता है) को गॉर्डन प्लॉटकिन ने (plotkin81) ऑपरेशनल सिमेंटिक्स को परिभाषित करने के तार्किक साधन के रूप में प्रस्तुत किया था। एसओएस के पीछे मूल विचार किसी प्रोग्राम के व्यवहार को उसके भागों के व्यवहार के संदर्भ में परिभाषित करना है, इस प्रकार संरचनात्मक, अर्थात, वाक्यविन्यास-उन्मुख एवं [[आगमनात्मक परिभाषा]], परिचालन सिमेंटिक्स पर दृष्टिकोण प्रदान करना है। एसओएस विनिर्देश [[राज्य संक्रमण प्रणाली|अवस्था संक्रमण सिस्टम]] के सेट के संदर्भ में प्रोग्राम के व्यवहार को परिभाषित करता है। एसओएस विनिर्देश [[अनुमान नियम|अनुमान नियमों]] के सेट का रूप लेते हैं जो इसके घटकों के संक्रमण के संदर्भ में वाक्यविन्यास के समग्र भागों के वैध परिवर्तन को परिभाषित करते हैं।
 सरल उदाहरण के लिए, हम साधारण प्रोग्रामिंग लैंगवेज के सिमेंटिक्स के भाग पर विचार करते हैं; plotkin81 एवं hennessy90, एवं अन्य पाठ्यपुस्तकों में उचित चित्रण दिए गए हैं। <math>C_1, C_2</math> लैंगवेज के प्रोग्रामों की रेंज, एवं विभिन्न अवस्थाओं <math>s</math> में सीमा होती है। यदि हमारे पास अभिव्यक्तियाँ (क्रमानुसार <math>E</math>), मान {{nobreak|(<math>V</math>)}} एवं स्थान (<math>L</math>) हैं, तो मेमोरी अपडेट कमांड में सिमेंटिक्स
@@ Line 42: / Line 42: @@
 \frac{}
 {\langle \mathbf{skip} ,s\rangle\longrightarrow s}
-</math> अनौपचारिक रूप से, प्रथम नियम कहता है कि यदि अवस्था <math>s</math> में  प्रोग्राम <math>C_1</math>अवस्था <math>s'</math> में समाप्त होता है, तत्पश्चात प्रोग्राम <math>C_1;C_2</math> अवस्था <math>s</math> में प्रोग्राम <math>C_2</math> अवस्था में <math>s'</math>में कमी आएगी। (आप इसे औपचारिकता के रूप में सोच सकते हैं, <math>C_1</math>, एवं तत्पश्चात <math>C_2</math> परिणामी मेमोरी स्टोर का उपयोग करना कर सकते हैं।) दूसरा नियम यही कहता है, यदि प्रोग्राम <math>C_1</math> अवस्था <math>s</math> में प्रोग्राम <math>C_1'</math> अवस्था के साथ <math>s'</math> को कम कर सकते हैं, तत्पश्चात प्रोग्राम <math>C_1;C_2</math> अवस्था <math>s</math> में  प्रोग्राम <math>C_1';C_2</math>अवस्था <math>s'</math> में कमी आएगी, आप इसे अनुकूलन कंपाइलर के लिए सिद्धांत को औपचारिक बनाने के रूप में सोच सकते हैं: "आपको परिवर्तन करने की अनुमति है जैसे कि यह <math>C_1</math> अकेले ही हो, भले ही यह किसी प्रोग्राम का प्रथम भाग ही क्यों न हो।"
+</math> अनौपचारिक रूप से, प्रथम नियम कहता है कि यदि अवस्था <math>s</math> में  प्रोग्राम <math>C_1</math>अवस्था <math>s'</math> में समाप्त होता है, तत्पश्चात प्रोग्राम <math>C_1;C_2</math> अवस्था <math>s</math> में प्रोग्राम <math>C_2</math> अवस्था में <math>s'</math>में कमी आएगी। (आप इसे औपचारिकता के रूप में सोच सकते हैं,  <math>C_1</math>, एवं तत्पश्चात <math>C_2</math> परिणामी मेमोरी स्टोर का उपयोग करना कर सकते हैं।) दूसरा नियम यही कहता है, यदि प्रोग्राम <math>C_1</math> अवस्था <math>s</math> में प्रोग्राम <math>C_1'</math> अवस्था <math>s'</math>के साथ कम कर सकते हैं, तत्पश्चात प्रोग्राम <math>C_1;C_2</math> अवस्था <math>s</math> में  प्रोग्राम <math>C_1';C_2</math>अवस्था <math>s'</math> में कमी आएगी, आप इसे अनुकूलन कंपाइलर के लिए सिद्धांत को औपचारिक बनाने के रूप में सोच सकते हैं: "आपको परिवर्तन करने की अनुमति है जैसे कि यह <math>C_1</math> अकेले ही हो, भले ही यह किसी प्रोग्राम का प्रथम भाग ही क्यों न हो।"
@@ Line 84: / Line 85: @@
 बड़े-चरण वाले सिमेंटिक्स प्रायः सरल होते हैं (कम अनुमान नियमों की आवश्यकता होती है) एवं प्रायः सीधे लैंगवेज के लिए दुभाषिया के कुशल कार्यान्वयन के अनुरूप होते हैं (इसलिए कहन उन्हें प्राकृतिक कहते हैं।) दोनों सरल प्रमाणों की ओर ले जा सकते हैं, उदाहरण के लिए जब कुछ [[कार्यक्रम परिवर्तन|प्रोग्राम परिवर्तन]] के अंतर्गत शुद्धता के संरक्षण को प्रमाणित किया जाता है।<ref name="leroy-coinductivebigstep">[[Xavier Leroy]]. "Coinductive big-step operational semantics".</ref>बड़े-चरण वाले सिमेंटिक्स की मुख्य हानि यह है कि अन्य-समाप्ति [[विचलन (कंप्यूटर विज्ञान)|विचलन]] गणनाओं में कोई अनुमान वृक्ष नहीं होता है, जिससे ऐसी गणनाओं के विषय में गुणों को बताना एवं प्रमाणित करना असंभव हो जाता है।<ref name="leroy-coinductivebigstep" />
-छोटे-चरण वाले सिमेंटिक्स विवरण एवं मूल्यांकन के क्रम पर अधिक नियंत्रण देते हैं। इंस्ट्रुमेंटेड ऑपरेशनल सिमेंटिक्स के विषय में, यह ऑपरेशनल सिमेंटिक्स को ट्रैक करने एवं सिमेंटिस्ट को लैंगवेज के रन-टाइम व्यवहार के विषय में अधिक त्रुटिहीन प्रमेयों को बताने एवं प्रमाणित करने की अनुमति देता है। परिचालन सिमेंटिक्स के विरुद्ध  प्रकार की प्रणाली की [[प्रकार की सुदृढ़ता]] प्रमाणित करते समय ये गुण छोटे-चरण के सिमेंटिक्स को अधिक सुविधाजनक बनाते हैं।<ref name="leroy-coinductivebigstep" />
+छोटे-चरण वाले सिमेंटिक्स विवरण एवं मूल्यांकन के क्रम पर अधिक नियंत्रण देते हैं। इंस्ट्रुमेंटेड ऑपरेशनल सिमेंटिक्स के विषय में, यह ऑपरेशनल सिमेंटिक्स को ट्रैक करने एवं सिमेंटिस्ट को लैंगवेज के रन-टाइम व्यवहार के विषय में अधिक त्रुटिहीन प्रमेयों को बताने एवं प्रमाणित करने की अनुमति देता है। परिचालन सिमेंटिक्स के विरुद्ध  प्रकार की सिस्टम की [[प्रकार की सुदृढ़ता]] प्रमाणित करते समय ये गुण छोटे-चरण के सिमेंटिक्स को अधिक सुविधाजनक बनाते हैं।<ref name="leroy-coinductivebigstep" />
 == यह भी देखें ==

Anonymous

Search

संचालनात्मक शब्दार्थ: Difference between revisions

Namespaces

More

Page actions

Revision as of 16:15, 5 August 2023

Contents

इतिहास