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

From Vigyanwiki

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

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

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

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

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

आधुनिक क्रमदेशन भाषाओं के लिए वस्त्वर्थक अर्थविज्ञान विकसित किया गया है जो समवर्ती कंप्यूटिंग और अपवाद संचालन जैसी क्षमताओं का उपयोग करते हैं, उदाहरण के लिए, समवर्ती ML,[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) के लिए n+1 कॉल की आवश्यकता होती है। सीमा में हमें संपूर्ण फलन से अपने कार्यछेत्र में हर जगह परिभाषित मिलता है।

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

 int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n)
{
  if (n == 0) then return 1;
  else if (fprev = lookup(factorial_less_defined, n-1)) then
    return n * fprev;
  else
    return NOT_DEFINED;
}

Map<int,int> F(Map<int,int> factorial_less_defined)
{ 
  Map<int,int> new_factorial = Map.empty();
  for (int n in all<int>()) {
    if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED)
      new_factorial.put(n, f);
  }
  return new_factorial;
}

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

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

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

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

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

गैर-नियतात्मक क्रमादेशों के वस्त्वर्थक अर्थविज्ञान

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

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


संगामिति का वस्त्वर्थक अर्थविज्ञान

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

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


स्तिथि का वस्त्वर्थक शब्दार्थ

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

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


डेटा प्रकार के वस्त्वर्थ

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

datatype list = Cons of nat * list | Empty

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

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

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

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

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

datatype α list = Cons of α * α list | Empty

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

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

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


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

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


अनुक्रमिकता का वस्त्वर्थक अर्थविज्ञान

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

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

स्रोत-से-स्रोत अनुवाद के रूप में वस्त्वर्थक अर्थविज्ञान

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

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


अमूर्तता

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

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

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

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

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


संरचना

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

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

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

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

वास्तव में, यह संरचनागत निरूपण शब्दार्थ के लिए एक सामान्य योजना है। यहां कार्यछेत्र और निरंतर कार्यों के बारे में कुछ विशेष नहीं है। कोई इसके स्थान पर एक अलग श्रेणी (गणित) के साथ काम कर सकता है। उदाहरण के लिए, खेल शब्दार्थ में, खेलों की श्रेणी में वस्तुओं के रूप में खेल और आकारिकी के रूप में रणनीतियाँ होती हैं: हम प्रकारों को खेलों के रूप में और क्रमादेशों को रणनीतियों के रूप में व्याख्या कर सकते हैं। सामान्य पुनरावर्तन के बिना एक सरल भाषा के लिए हम सम्मुच्चय की श्रेणी के साथ काम कर सकते हैं। अनुषंगी प्रभाव वाली भाषा के लिए, हम क्लेस्ली श्रेणी में एक एकसंयुज के लिए काम कर सकते हैं। स्थिति के साथ भाषा के लिए, हम प्रकार्यक श्रेणी में काम कर सकते हैं। रॉबिन मिलनर ने वस्तुओं के रूप में अंतरापृष्ठ और आकारिकी के रूप में द्विरेखांकन के साथ एक श्रेणी में काम करके प्रतिरूपण स्थान और परस्परक्रिया की वकालत की है।[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


बाहरी संबंध