सांकेतिक शब्दार्थ

From Vigyanwiki
Revision as of 16:10, 17 February 2023 by alpha>Indicwiki (Created page with "{{short description|Study of programming languages via mathematical objects}} {{Semantics}} कंप्यूटर विज्ञान में, सांकेति...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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

मोटे तौर पर बोलना, अर्थ संबंधी शब्दार्थ गणितीय वस्तुओं को खोजने से संबंधित है जिसे डोमेन सिद्धांत कहा जाता है जो दर्शाता है कि कार्यक्रम क्या करते हैं। उदाहरण के लिए, प्रोग्राम (या प्रोग्राम वाक्यांश) को आंशिक कार्यों द्वारा दर्शाया जा सकता है[1][2] या खेल सिद्धांत द्वारा[3] पर्यावरण और व्यवस्था के बीच।

सांकेतिक शब्दार्थ का एक महत्वपूर्ण सिद्धांत यह है कि शब्दार्थ रचनात्मक होना चाहिए: एक कार्यक्रम वाक्यांश का अर्थ उसके वाक्यांश के अर्थों से बनाया जाना चाहिए।

ऐतिहासिक विकास

1970 के दशक की शुरुआत में प्रकाशित क्रिस्टोफर स्ट्रेची और दाना स्कॉट के काम में सांकेतिक शब्दार्थ की उत्पत्ति हुई।[1][2]जैसा कि मूल रूप से स्ट्रैची और स्कॉट द्वारा विकसित किया गया था, सांकेतिक शब्दार्थ ने एक कंप्यूटर प्रोग्राम का अर्थ एक फ़ंक्शन (गणित) के रूप में प्रदान किया जो इनपुट को आउटपुट में मैप करता है।[2]पुनरावर्तन कार्यक्रमों को अर्थ देने के लिए, स्कॉट ने डोमेन सिद्धांत के बीच स्कॉट निरंतरता के साथ काम करने का प्रस्ताव दिया, विशेष रूप से आंशिक आदेशों को पूरा किया। जैसा कि नीचे वर्णित किया गया है, प्रोग्रामिंग भाषाओं के पहलुओं जैसे अनुक्रमिकता, डेनोटेशनल सिमेंटिक्स#डिनोटेशनल सिमेंटिक्स ऑफ कॉन्करेंसी, गैर नियतात्मक एल्गोरिथम|नॉन-डेटर्मिनिज्म और स्थानीय राज्य के लिए उपयुक्त डेनोटेशनल सिमेंटिक्स की जांच में काम जारी है।

आधुनिक प्रोग्रामिंग भाषाओं के लिए सांकेतिक शब्दार्थ विकसित किया गया है जो समवर्ती कंप्यूटिंग और अपवाद संचालन जैसी क्षमताओं का उपयोग करते हैं, उदाहरण के लिए, समवर्ती एमएल,[4] अनुक्रमिक प्रक्रियाओं का संचार करना,[5] और हास्केल (प्रोग्रामिंग भाषा)[6] इन भाषाओं का शब्दार्थ रचनागत है जिसमें एक वाक्यांश का अर्थ उसके उपवाक्यों के अर्थ पर निर्भर करता है। उदाहरण के लिए, अनुप्रयोगी प्रोग्रामिंग भाषा f(E1,E2) का अर्थ इसके उपवाक्यों f, E1 और E2 के शब्दार्थ के संदर्भ में परिभाषित किया गया है। एक आधुनिक प्रोग्रामिंग भाषा में, E1 और E2 का समवर्ती मूल्यांकन किया जा सकता है और उनमें से एक का निष्पादन ऑब्जेक्ट (कंप्यूटर विज्ञान) के माध्यम से बातचीत करके दूसरे को प्रभावित कर सकता है, जिससे उनके अर्थ एक दूसरे के संदर्भ में परिभाषित हो सकते हैं। इसके अलावा, E1 या E2 एक अपवाद फेंक सकते हैं जो दूसरे के निष्पादन को निरस्त (कंप्यूटिंग) कर सकता है। नीचे दिए गए खंड इन आधुनिक प्रोग्रामिंग भाषाओं के शब्दार्थ के विशेष मामलों का वर्णन करते हैं।

पुनरावर्ती कार्यक्रमों का अर्थ

डेनोटेशनल सिमेंटिक्स को एक प्रोग्राम वाक्यांश के रूप में एक वातावरण से एक फ़ंक्शन के रूप में (इसके मुक्त चर के वर्तमान मूल्यों को धारण करते हुए) इसके निरूपण के रूप में वर्णित किया गया है। उदाहरण के लिए, मुहावरा n*m एक ऐसे वातावरण के साथ प्रदान किए जाने पर एक संकेत उत्पन्न करता है जो इसके दो मुक्त चर के लिए बाध्यकारी है: n और m. अगर पर्यावरण में n मान 3 और है m का मान 5 है, तो निरूपण 15 है।[2]

एक फ़ंक्शन को तर्क और संबंधित परिणाम मानों के क्रमबद्ध जोड़े के सेट के रूप में प्रदर्शित किया जा सकता है। उदाहरण के लिए, सेट {(0,1), (4,3)} तर्क 0 के लिए परिणाम 1 के साथ एक फ़ंक्शन को दर्शाता है, तर्क 4 के लिए परिणाम 3, और अन्यथा अपरिभाषित।

उदाहरण के लिए कारख़ाने का फ़ंक्शन पर विचार करें, जिसे पुनरावर्ती रूप से परिभाषित किया जा सकता है: <वाक्यविन्यास प्रकाश लैंग = सी> इंट फैक्टोरियल (इंट एन) { अगर (एन == 0) तो 1 लौटें; अन्यथा वापसी n * भाज्य (n-1); }</syntaxhighlight>

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

औपचारिक रूप से हम प्रत्येक सन्निकटन को एक आंशिक फलन के रूप में प्रतिरूपित करते हैं . हमारा सन्निकटन तब बार-बार एक फ़ंक्शन को लागू कर रहा है जो एक अधिक परिभाषित आंशिक फैक्टोरियल फ़ंक्शन को लागू करता है, अर्थात , खाली फ़ंक्शन (खाली सेट) से शुरू होता है। F को कोड में निम्नानुसार परिभाषित किया जा सकता है (उपयोग करके Map<int,int> के लिए ): <वाक्यविन्यास लैंग = सीपीपी> int factorial_nonrecursive (नक्शा <int, int> factorial_less_defined, int n) {

 अगर (एन == 0) तो वापसी 1;
 और अगर (fprev = लुकअप (फैक्टोरियल_लेस_डिफाइन्ड, एन -1)) तो
   वापसी n * fprev;
 अन्य
   वापसी NOT_DEFINED;

}

मानचित्र <int, int> F (नक्शा <int, int> factorial_less_defined) {

 मानचित्र <int, int> new_फैक्टोरियल = मानचित्र खाली ();
 for (int n in all<int>()) {
   अगर (f = factorial_nonrecursive (फैक्टोरियल_लेस_डिफ़ाइंड, n)! = NOT_DEFINED)
     new_फैक्टोरियल.पुट (एन, एफ);
 }
 नया_फैक्टोरियल लौटें;

} </वाक्यविन्यास हाइलाइट>

तब हम संकेतन F का परिचय दे सकते हैंn पुनरावृत्त फ़ंक्शन को इंगित करने के लिए।

  • एफ0({}) पूरी तरह से अपरिभाषित आंशिक कार्य है, जिसे सेट {} के रूप में दर्शाया गया है;
  • एफ1({}) आंशिक फ़ंक्शन है जिसे सेट {(0,1)} के रूप में दर्शाया गया है: इसे 0 पर परिभाषित किया गया है, 1 होना है, और कहीं और अपरिभाषित है;
  • एफ5({}) आंशिक फ़ंक्शन है जिसे सेट {(0,1), (1,1), (2,2), (3,6), (4,24)} के रूप में दर्शाया गया है: यह तर्क 0,1,2,3,4 के लिए परिभाषित किया गया है।

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

इस मामले में, निश्चित बिंदु इस श्रृंखला की सबसे कम ऊपरी सीमा है, जो पूर्ण है factorial कार्य, जिसे संघ (सेट सिद्धांत) के रूप में व्यक्त किया जा सकता है

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

गैर-नियतात्मक कार्यक्रमों के सांकेतिक शब्दार्थ

शक्ति डोमेन की अवधारणा को गैर-नियतात्मक अनुक्रमिक कार्यक्रमों के लिए एक सांकेतिक शब्दार्थ देने के लिए विकसित किया गया है। पावर-डोमेन कन्स्ट्रक्टर के लिए पी लिखना, डोमेन पी (डी) डी द्वारा निरूपित प्रकार के गैर-नियतात्मक संगणनाओं का डोमेन है।

गैर-नियतत्ववाद के डोमेन-सैद्धांतिक मॉडल में निष्पक्षता और अबाधित गैर-नियतत्ववाद के साथ कठिनाइयां हैं।[7]


संगामिति का सांकेतिक शब्दार्थ

कई शोधकर्ताओं ने तर्क दिया है कि ऊपर दिए गए डोमेन-सैद्धांतिक मॉडल कॉन्करेंसी (कंप्यूटर विज्ञान) के अधिक सामान्य मामले के लिए पर्याप्त नहीं हैं। इस कारण विभिन्न संगामिति (कंप्यूटर विज्ञान)#मॉडल पेश किए गए हैं। 1980 के दशक की शुरुआत में, लोगों ने समवर्ती भाषाओं के लिए शब्दार्थ देने के लिए सांकेतिक शब्दार्थ की शैली का उपयोग करना शुरू किया। उदाहरणों में अभिनेता मॉडल #क्लिंजर.27एस मॉडल|विल क्लिंजर का अभिनेता मॉडल के साथ काम करना शामिल है; इवेंट स्ट्रक्चर्स और पेट्री नेट के साथ ग्लिन विंस्केल का काम;[8] और फ्रांसेज़, होरे, लेहमन, और डी रोवर (1979) द्वारा सीएसपी के लिए ट्रेस शब्दार्थ पर काम।[9] पूछताछ की ये सभी पंक्तियां जांच के अधीन हैं (उदाहरण के लिए सीएसपी के लिए विभिन्न डेनोटेशनल मॉडल देखें[5]).

हाल ही में, विंस्केल और अन्य ने संगति के लिए एक डोमेन सिद्धांत के रूप में प्रोफेसरों की श्रेणी का प्रस्ताव दिया है।[10][11]


राज्य का सांकेतिक शब्दार्थ

राज्य (जैसे कि एक ढेर) और सरल अनिवार्य प्रोग्रामिंग को ऊपर वर्णित अर्थ विज्ञान में सीधे तौर पर प्रतिरूपित किया जा सकता है। नीचे दिए गए सभी सांकेतिक शब्दार्थ#पाठ्यपुस्तकों में विवरण है। मुख्य विचार राज्यों के कुछ डोमेन पर आंशिक कार्य के रूप में कमांड पर विचार करना है। इसका मतलबx:=3तब वह कार्य है जो राज्य को राज्य में ले जाता है 3 को सौंपना x. अनुक्रमण ऑपरेटर;कार्यों की संरचना द्वारा निरूपित किया जाता है। फिक्स्ड-पॉइंट कंस्ट्रक्शन का उपयोग तब लूपिंग कंस्ट्रक्शन को शब्दार्थ देने के लिए किया जाता है, जैसेwhile.

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


डेटा प्रकार के संकेत

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

datatype list = nat * list | खाली

यह खंड केवल कार्यात्मक डेटा संरचनाओं से संबंधित है जो बदल नहीं सकते हैं। परंपरागत अनिवार्य प्रोग्रामिंग भाषाएं आमतौर पर ऐसी पुनरावर्ती सूची के तत्वों को बदलने की अनुमति देती हैं।

एक अन्य उदाहरण के लिए: अनटाइप्ड लैम्ब्डा कैलकुलस के डिनोटेशन का प्रकार है

डेटाटाइप D = D of (D  D)

डोमेन समीकरणों को हल करने की समस्या उन डोमेन को खोजने से संबंधित है जो इस प्रकार के डेटाटाइप्स को मॉडल करते हैं। एक दृष्टिकोण, मोटे तौर पर बोलना, सभी डोमेन के संग्रह को एक डोमेन के रूप में मानना ​​​​है, और फिर वहाँ पुनरावर्ती परिभाषा को हल करना है। नीचे दी गई पाठ्यपुस्तकें अधिक विवरण देती हैं।

बहुरूपता (कंप्यूटर विज्ञान) डेटा प्रकार हैं जिन्हें एक पैरामीटर के साथ परिभाषित किया गया है। उदाहरण के लिए, α का प्रकार listएस द्वारा परिभाषित किया गया है

datatype α लिस्ट = α * α लिस्ट के नुकसान | खाली

प्राकृतिक संख्याओं की सूची, तब, प्रकार की होती है nat list, जबकि स्ट्रिंग्स की सूचियाँ हैं string list.

कुछ शोधकर्ताओं ने बहुरूपता के डोमेन थ्योरिटिक मॉडल विकसित किए हैं। अन्य शोधकर्ताओं ने भी रचनात्मक सेट सिद्धांतों के भीतर पैरामीट्रिक बहुरूपता का मॉडल तैयार किया है। विवरण नीचे सूचीबद्ध पाठ्यपुस्तकों में पाए जाते हैं।

हाल ही के एक शोध क्षेत्र में वस्तु और वर्ग आधारित प्रोग्रामिंग भाषाओं के लिए सांकेतिक शब्दार्थ शामिल है।[14]


प्रतिबंधित जटिलता के कार्यक्रमों के लिए सांकेतिक शब्दार्थ

रेखीय तर्क पर आधारित प्रोग्रामिंग भाषाओं के विकास के बाद, रेखीय उपयोग के लिए भाषाओं को सांकेतिक शब्दार्थ दिया गया है (उदाहरण के लिए सबूत जाल, सुसंगत स्थान देखें) और बहुपद समय जटिलता भी।[15]


अनुक्रमिकता का सांकेतिक शब्दार्थ

कम्प्यूटेशनल फ़ंक्शंस के लिए अनुक्रमिक प्रोग्रामिंग लैंग्वेज प्रोग्रामिंग लैंग्वेज के लिए फुल डेनोटेशनल सिमेंटिक्स # एब्सट्रैक्शन की समस्या, लंबे समय से, डेनोटेशनल सिमेंटिक्स में एक बड़ा खुला प्रश्न था। पीसीएफ के साथ कठिनाई यह है कि यह बहुत अनुक्रमिक भाषा है। उदाहरण के लिए, PCF में तार्किक संयोजन#parallel-or|parallel-or फ़ंक्शन को परिभाषित करने का कोई तरीका नहीं है। यह इस कारण से है कि डोमेन का उपयोग करने वाला दृष्टिकोण, जैसा कि ऊपर पेश किया गया है, एक अर्थपूर्ण शब्दार्थ उत्पन्न करता है जो पूरी तरह से सार नहीं है।

यह खुला प्रश्न ज्यादातर 1990 के दशक में खेल शब्दार्थ के विकास और तार्किक संबंधों से जुड़ी तकनीकों के साथ हल किया गया था।[16] अधिक जानकारी के लिए, पीसीएफ पर पेज देखें।

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

इस संदर्भ में, सांकेतिक शब्दार्थ से धारणाएं, जैसे पूर्ण अमूर्तता, सुरक्षा चिंताओं को पूरा करने में मदद करती हैं।[17][18]


अमूर्तता

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

  1. वाक्यविन्यास स्वतंत्रता: कार्यक्रमों के अर्थों में स्रोत भाषा का वाक्य-विन्यास शामिल नहीं होना चाहिए।
  2. पर्याप्तता (या सुदृढ़ता): सभी पर्यवेक्षणीय तुल्यता कार्यक्रमों के अलग-अलग अर्थ होते हैं;
  3. पूर्ण अमूर्तता: सभी पर्यवेक्षणीय समकक्ष कार्यक्रमों में समान अर्थ होते हैं।

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

अतिरिक्त वांछनीय गुण जिन्हें हम परिचालन और सांकेतिक शब्दार्थ के बीच रखना चाहते हैं:

  1. Constructivism: रचनावाद (गणित) का संबंध इस बात से है कि क्या डोमेन तत्वों को रचनात्मक तरीकों से मौजूद दिखाया जा सकता है।
  2. निरूपण और परिचालन शब्दार्थ की स्वतंत्रता: सांकेतिक शब्दार्थ को गणितीय संरचनाओं का उपयोग करके औपचारिक रूप दिया जाना चाहिए जो एक प्रोग्रामिंग भाषा के परिचालन शब्दार्थ से स्वतंत्र हैं; हालांकि, अंतर्निहित अवधारणाएं निकटता से संबंधित हो सकती हैं। नीचे denotational semantics#Compositionality पर अनुभाग देखें।
  3. पूर्ण पूर्णता या निश्चितता: सिमेंटिक मॉडल का प्रत्येक रूपवाद एक कार्यक्रम का प्रतीक होना चाहिए।[19]


संरचना

प्रोग्रामिंग भाषाओं के सांकेतिक शब्दार्थ का एक महत्वपूर्ण पहलू संरचना है, जिसके द्वारा किसी प्रोग्राम के डिनोटेशन का निर्माण उसके भागों के डिनोटेशन से किया जाता है। उदाहरण के लिए, व्यंजक 7 + 4 पर विचार करें। इस मामले में संरचना 7 , 4 और + के अर्थों के संदर्भ में 7 + 4 के लिए एक अर्थ प्रदान करना है।

डोमेन थ्योरी में एक बुनियादी निरूपण शब्दार्थ रचनात्मक है क्योंकि इसे निम्नानुसार दिया गया है। हम कार्यक्रम के अंशों पर विचार करके शुरू करते हैं, अर्थात मुक्त चर वाले कार्यक्रम। एक टाइपिंग संदर्भ प्रत्येक मुक्त चर के लिए एक प्रकार प्रदान करता है। उदाहरण के लिए, अभिव्यक्ति में (x + y) को टाइपिंग संदर्भ में माना जा सकता है (x:nat,और:nat). अब हम निम्नलिखित योजना का उपयोग करते हुए, अंशों को प्रोग्राम करने के लिए एक सांकेतिक शब्दार्थ देते हैं।

  1. हम अपनी भाषा के प्रकार के अर्थ का वर्णन करते हुए शुरू करते हैं: प्रत्येक प्रकार का अर्थ एक डोमेन होना चाहिए। हम टाइप τ को दर्शाने वाले डोमेन के लिए 〚τ〛 लिखते हैं। उदाहरण के लिए, प्रकार का अर्थ nat प्राकृतिक संख्याओं का डोमेन होना चाहिए: 〚nat〛= .
  2. प्रकार के अर्थ से हम टाइपिंग संदर्भों के लिए एक अर्थ प्राप्त करते हैं। हमने 'एक्स' सेट किया है1:टी1,..., एक्सn:टीn〛 = 〚 वर्ग1〛× ... ×〚टीn〛। उदाहरण के लिए, 'एक्स:nat,और:nat〛= ×. एक विशेष मामले के रूप में, खाली टाइपिंग संदर्भ का अर्थ, बिना चर के, एक तत्व वाला डोमेन है, जिसे 1 दर्शाया गया है।
  3. अंत में, हमें प्रत्येक प्रोग्राम-टुकड़ा-इन-टाइपिंग-संदर्भ को एक अर्थ देना चाहिए। मान लीजिए कि पी प्रकार σ का एक प्रोग्राम टुकड़ा है, टाइपिंग संदर्भ में Γ, अक्सर Γ⊢P:σ लिखा जाता है। फिर इस प्रोग्राम-इन-टाइपिंग-संदर्भ का अर्थ एक सतत कार्य होना चाहिए 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛। उदाहरण के लिए, 〚⊢7:nat〛:1→ लगातार 7 कार्य है, जबकि 〚x:nat,और:nat⊢x+y:nat〛:× वह कार्य है जो दो संख्याओं को जोड़ता है।

अब, यौगिक व्यंजक (7+4) का अर्थ तीन कार्यों 〚⊢7 को मिलाकर निर्धारित किया जाता है:nat〛:1→, 〚⊢4:nat〛:1→, और "एक्स:nat,और:nat⊢x+y:nat〛:×.

वास्तव में, यह संरचनागत निरूपण शब्दार्थ के लिए एक सामान्य योजना है। यहां डोमेन और निरंतर कार्यों के बारे में कुछ खास नहीं है। कोई इसके बजाय एक अलग श्रेणी (गणित) के साथ काम कर सकता है। उदाहरण के लिए, खेल शब्दार्थ में, खेलों की श्रेणी में वस्तुओं के रूप में खेल और आकारिकी के रूप में रणनीतियाँ होती हैं: हम प्रकारों को खेलों के रूप में और कार्यक्रमों को रणनीतियों के रूप में व्याख्या कर सकते हैं। सामान्य पुनरावर्तन के बिना एक सरल भाषा के लिए, हम सेट की श्रेणी के साथ काम कर सकते हैं। साइड-इफेक्ट्स वाली भाषा के लिए, हम क्लेस्ली श्रेणी में एक सन्यासी के लिए काम कर सकते हैं। राज्य के साथ भाषा के लिए, हम functor श्रेणी में काम कर सकते हैं। रॉबिन मिलनर ने वस्तुओं के रूप में इंटरफेस और आकारिकी के रूप में bigraphs के साथ एक श्रेणी में काम करके मॉडलिंग स्थान और बातचीत की वकालत की है।[20]


शब्दार्थ बनाम कार्यान्वयन

डाना स्कॉट (1980) के अनुसार:[21]

सिमेंटिक्स के लिए किसी कार्यान्वयन का निर्धारण करना आवश्यक नहीं है, लेकिन उसे यह दर्शाने के लिए मानदंड प्रदान करना चाहिए कि कार्यान्वयन सही है।

क्लिंजर (1981) के अनुसार:[22]: 79 

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

कंप्यूटर विज्ञान के अन्य क्षेत्रों से कनेक्शन

डेनोटेशनल सिमेंटिक्स में कुछ काम ने डोमेन सिद्धांत के अर्थ में डोमेन के रूप में व्याख्या की है, जिसे मॉडल सिद्धांत की एक शाखा के रूप में देखा जा सकता है, जिससे प्रकार सिद्धांत और श्रेणी सिद्धांत के साथ संबंध हो सकते हैं। कंप्यूटर विज्ञान के भीतर, अमूर्त व्याख्या, कार्यक्रम सत्यापन और मॉडल जाँच के साथ संबंध हैं।

संदर्भ

  1. 1.0 1.1 Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.
  2. 2.0 2.1 2.2 2.3 Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971.
  3. Jan Jürjens. J. Games In The Semantics Of Programming Languages – An Elementary Introduction. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034
  4. John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, Lecture Notes in Computer Science, Vol. 693. 1993
  5. 5.0 5.1 A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.
  6. Simon Peyton Jones, Alastair Reid, Fergus Henderson, Tony Hoare, and Simon Marlow. "A semantics for imprecise exceptions" Conference on Programming Language Design and Implementation. 1999.
  7. Levy, Paul Blain (2007). "Amb Breaks Well-Pointedness, Ground Amb Doesn't". Electron. Notes Theor. Comput. Sci. 173: 221–239. doi:10.1016/j.entcs.2007.02.036.
  8. Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.
  9. Nissim Francez, C. A. R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. "Semantics of nondeterminism, concurrency, and communication", Journal of Computer and System Sciences. December 1979.
  10. Cattani, Gian Luca; Winskel, Glynn (2005). "Profunctors, open maps and bisimulation". Mathematical Structures in Computer Science. 15 (3): 553–614. CiteSeerX 10.1.1.111.6243. doi:10.1017/S0960129505004718. S2CID 16356708.
  11. Nygaard, Mikkel; Winskel, Glynn (2004). "Domain theory for concurrency". Theor. Comput. Sci. 316 (1–3): 153–190. doi:10.1016/j.tcs.2004.01.029.
  12. Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama. Syntactic control of interference revisited. Electron. Notes Theor. Comput. Sci. 1. 1995.
  13. Frank J. Oles. A Category-Theoretic Approach to the Semantics of Programming. PhD thesis, Syracuse University, New York, USA. 1982.
  14. Reus, Bernhard; Streicher, Thomas (2004). "Semantics and logic of object calculi". Theor. Comput. Sci. 316 (1): 191–213. doi:10.1016/j.tcs.2004.01.030.
  15. Baillot, P. (2004). "Stratified coherence spaces: a denotational semantics for Light Linear Logic". Theor. Comput. Sci. 318 (1–2): 29–55. doi:10.1016/j.tcs.2003.10.015.
  16. O'Hearn, P.W.; Riecke, J.G. (July 1995). "Kripke Logical Relations and PCF". Information and Computation. 120 (1): 107–116. doi:10.1006/inco.1995.1103. S2CID 6886529.
  17. Martin Abadi. "Protection in programming-language translations". Proc. of ICALP'98. LNCS 1443. 1998.
  18. Kennedy, Andrew (2006). "Securing the .NET programmingmodel". Theor. Comput. Sci. 364 (3): 311–7. doi:10.1016/j.tcs.2006.08.014.
  19. Curien, Pierre-Louis (2007). "Definability and Full Abstraction". Electronic Notes in Theoretical Computer Science. 172: 301–310. doi:10.1016/j.entcs.2007.02.011.
  20. Milner, Robin (2009). The Space and Motion of Communicating Agents. Cambridge University Press. ISBN 978-0-521-73833-0. 2009 draft Archived 2012-04-02 at the Wayback Machine.
  21. "What is Denotational Semantics?", MIT Laboratory for Computer Science Distinguished Lecture Series, 17 April 1980, cited in Clinger (1981).
  22. Clinger, William D. (1981). "Foundations of Actor Semantics" (PhD). Massachusetts Institute of Technology. hdl:1721.1/6935. AITR-633. {{cite journal}}: Cite journal requires |journal= (help)


अग्रिम पठन

Textbooks
Lecture notes
Other references


बाहरी संबंध