संचालनात्मक शब्दार्थ

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

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

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

इतिहास

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

<ब्लॉककोट> सख्त लैंगवेज में किसी प्रोग्राम का अर्थ काल्पनिक कंप्यूटर के संदर्भ में समझाया गया है जो उस प्रोग्रामके विस्तार को बनाने वाली क्रियाओं का समूह निष्पादित करता है। (#एल्गोल68, धारा 2) </ब्लॉककोट>

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

<ब्लॉककोट> अधिक 'सार' एवं 'स्वच्छ' दृष्टिकोण का लक्ष्य रखना बहुत अच्छी बात है शब्दार्थ, लेकिन यदि योजना अच्छी होनी है, तो परिचालन संबंधी पहलू नहीं हो सकते पूरी तरह से नजरअंदाज किया जाए. (#स्कॉट70) </ब्लॉककोट>

दृष्टिकोण

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

लघु-चरण शब्दार्थ

संरचनात्मक परिचालन शब्दार्थ

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

सरल उदाहरण के लिए, हम साधारण प्रोग्रामिंग लैंगवेज के शब्दार्थ के भाग पर विचार करते हैं; #plotkin81 एवं #hennessybook, एवं अन्य पाठ्यपुस्तकों में उचित चित्रण दिए गए हैं। होने देना $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}}$ अनौपचारिक रूप से, पहला नियम कहता है कि, यदि प्रोग्राम $C_{1}$ राज्य में $s$ अवस्था में समाप्त होता है $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}}$ ऐसी परिलैंगवेज कार्यक्रमों के व्यवहार के औपचारिक विश्लेषण की अनुमति देती है, कार्यक्रमों के बीच संबंध (गणित) के अध्ययन की अनुमति देती है। महत्वपूर्ण संबंधों में अनुकरण पूर्वआदेश एवं द्विसिमुलेशन शामिल हैं। ये Concurrency (कंप्यूटर विज्ञान) के संदर्भ में विशेष रूप से उपयोगी हैं।

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

न्यूनीकरण शब्दार्थ

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

$\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) ल-चरण संबंध के ट्रांजिटिव-रिफ्लेक्टिव क्लोजर के लिए करी-फ़े मानकीकरण लेम्मा, जो मूल्यांकन फ़ंक्शन में गैर-नियतात्मक खोज को नियतात्मक बाएं-सबसे / सबसे बाहरी खोज से बदल देता है। फ़ेलिसेन ने दिखाया कि इस कलन के अनिवार्य विस्तार इन प्रमेयों को संतुष्ट करते हैं। इन प्रमेयों का परिणाम यह है कि समीकरण सिद्धांत - सममित-संक्रमणीय-प्रतिवर्ती समापन - इन लैंगवेजओं के लिए ठोस तर्क सिद्धांत है। हालाँकि, व्यवहार में, कटौती शब्दार्थ के अधिकांश अनुप्रयोग कैलकुलस से दूर हो जाते हैं एवं केवल मानक कटौती (एवं मूल्यांकनकर्ता जो इससे प्राप्त किया जा सकता है) का उपयोग करते हैं।

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

बड़ा कदम शब्दार्थ

प्राकृतिक शब्दार्थ

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

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

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

तुलना

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

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

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

यह भी देखें

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

अग्रिम पठन

• 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])
• Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. available online.

बाहरी संबंध

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