सांकेतिक शब्दार्थ: Difference between revisions

From Vigyanwiki
(Created page with "{{short description|Study of programming languages via mathematical objects}} {{Semantics}} कंप्यूटर विज्ञान में, सांकेति...")
 
(TEXT)
Line 1: Line 1:
{{short description|Study of programming languages via mathematical objects}}
{{short description|Study of programming languages via mathematical objects}}
{{Semantics}}
{{Semantics}}
[[कंप्यूटर विज्ञान]] में, सांकेतिक शब्दार्थ (शुरुआत में गणितीय शब्दार्थ या स्कॉट-स्ट्रैची शब्दार्थ के रूप में जाना जाता है) [[गणितीय वस्तु]]ओं का निर्माण करके [[प्रोग्रामिंग भाषा]]ओं के अर्थों को औपचारिक रूप देने का एक दृष्टिकोण है (जिसे 'डीनोटेशन' कहा जाता है) जो [[अभिव्यक्ति (कंप्यूटर विज्ञान)]] के अर्थों का वर्णन करता है। भाषाओं से। [[प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ]] प्रदान करने वाले अन्य दृष्टिकोणों में [[स्वयंसिद्ध शब्दार्थ]] और [[परिचालन शब्दार्थ]] शामिल हैं।
[[कंप्यूटर विज्ञान]] में, वस्त्वर्थक अर्थविज्ञान (प्रारम्भ में गणितीय शब्दार्थ या स्कॉट-स्ट्रैची शब्दार्थ के रूप में जाना जाता है) [[गणितीय वस्तु]]ओं का निर्माण करके [[प्रोग्रामिंग भाषा|क्रमदेशन भाषा]]ओं के अर्थों को औपचारिक रूप देने का एक दृष्टिकोण है (जिसे 'संकेतार्थ' कहा जाता है) जो [[अभिव्यक्ति (कंप्यूटर विज्ञान)]] के अर्थों का वर्णन करता है। भाषाओं से। [[प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ|क्रमदेशन भाषाओं के औपचारिक शब्दार्थ]] प्रदान करने वाले अन्य दृष्टिकोणों में [[स्वयंसिद्ध शब्दार्थ]] और [[परिचालन शब्दार्थ]] सम्मिलित हैं।


मोटे तौर पर बोलना, अर्थ संबंधी शब्दार्थ गणितीय वस्तुओं को खोजने से संबंधित है जिसे [[डोमेन सिद्धांत]] कहा जाता है जो दर्शाता है कि कार्यक्रम क्या करते हैं। उदाहरण के लिए, प्रोग्राम (या प्रोग्राम वाक्यांश) को आंशिक कार्यों द्वारा दर्शाया जा सकता है<ref name="ropas.snu.ac.kr">Dana S. Scott. [https://ropas.snu.ac.kr/~kwang/520/readings/sco70.pdf Outline of a mathematical theory of computation]. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.</ref><ref name="Research Group Technical Monograph 1971">[[Dana Scott]] and [[Christopher Strachey]]. ''Toward a mathematical semantics for computer languages'' Oxford Programming Research Group Technical Monograph. PRG-6.  1971.</ref> या [[खेल सिद्धांत]] द्वारा<ref>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 https://doi.org/10.1023/A:1020883810034]</ref> पर्यावरण और व्यवस्था के बीच।
मोटे तौर पर बोलना, अर्थ संबंधी शब्दार्थ गणितीय वस्तुओं को खोजने से संबंधित है जिसे [[डोमेन सिद्धांत|कार्यक्षेत्र सिद्धांत]] कहा जाता है जो दर्शाता है कि क्रमादेश क्या करते हैं। उदाहरण के लिए, क्रमादेश (या क्रमादेश वाक्यांश) को पर्यावरण और व्यवस्था के बीच आंशिक कार्यों द्वारा या [[खेल सिद्धांत]] द्वारा दर्शाया जा सकता है।<ref name="ropas.snu.ac.kr">Dana S. Scott. [https://ropas.snu.ac.kr/~kwang/520/readings/sco70.pdf Outline of a mathematical theory of computation]. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.</ref><ref name="Research Group Technical Monograph 1971">[[Dana Scott]] and [[Christopher Strachey]]. ''Toward a mathematical semantics for computer languages'' Oxford Programming Research Group Technical Monograph. PRG-6.  1971.</ref> <ref>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 https://doi.org/10.1023/A:1020883810034]</ref>


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


== ऐतिहासिक विकास ==
== ऐतिहासिक विकास ==
1970 के दशक की शुरुआत में प्रकाशित [[क्रिस्टोफर स्ट्रेची]] और [[दाना स्कॉट]] के काम में सांकेतिक शब्दार्थ की उत्पत्ति हुई।<ref name="ropas.snu.ac.kr"/><ref name="Research Group Technical Monograph 1971"/>जैसा कि मूल रूप से स्ट्रैची और स्कॉट द्वारा विकसित किया गया था, सांकेतिक शब्दार्थ ने एक कंप्यूटर प्रोग्राम का अर्थ एक फ़ंक्शन (गणित) के रूप में प्रदान किया जो इनपुट को आउटपुट में मैप करता है।<ref name="Research Group Technical Monograph 1971"/>पुनरावर्तन कार्यक्रमों को अर्थ देने के लिए, स्कॉट ने डोमेन सिद्धांत के बीच [[स्कॉट निरंतरता]] के साथ काम करने का प्रस्ताव दिया, विशेष रूप से आंशिक आदेशों को पूरा किया। जैसा कि नीचे वर्णित किया गया है, प्रोग्रामिंग भाषाओं के पहलुओं जैसे अनुक्रमिकता, डेनोटेशनल सिमेंटिक्स#डिनोटेशनल सिमेंटिक्स ऑफ कॉन्करेंसी, [[गैर नियतात्मक एल्गोरिथम]]|नॉन-डेटर्मिनिज्म और [[स्थानीय राज्य]] के लिए उपयुक्त डेनोटेशनल सिमेंटिक्स की जांच में काम जारी है।
1970 के दशक की प्रारम्भ में प्रकाशित [[क्रिस्टोफर स्ट्रेची]] और [[दाना स्कॉट]] के काम में वस्त्वर्थक अर्थविज्ञान की उत्पत्ति हुई।<ref name="ropas.snu.ac.kr"/><ref name="Research Group Technical Monograph 1971"/> जैसा कि मूल रूप से स्ट्रैची और स्कॉट द्वारा विकसित किया गया था, वस्त्वर्थक अर्थविज्ञान ने एक कंप्यूटर क्रमादेश का अर्थ एक फलन (गणित) के रूप में प्रदान किया जो इनपुट को आउटपुट में मानचित्र करता है।<ref name="Research Group Technical Monograph 1971"/> पुनरावर्तन क्रमादेशों को अर्थ देने के लिए, स्कॉट ने कार्यछेत्र सिद्धांत के बीच [[स्कॉट निरंतरता]] के साथ काम करने का प्रस्ताव दिया, विशेष रूप से आंशिक आदेशों को पूरा किया। जैसा कि नीचे वर्णित किया गया है, क्रमदेशन भाषाओं के पहलुओं जैसे अनुक्रमिकता, संगामिति का वस्त्वर्थक अर्थविज्ञान, [[गैर नियतात्मक एल्गोरिथम|गैर नियतात्मक कलन विधि]], अनिर्धारिता और [[स्थानीय राज्य|स्थानीय स्तिथि]] के लिए उपयुक्त वस्त्वर्थक अर्थविज्ञान की जांच में काम जारी है।


आधुनिक प्रोग्रामिंग भाषाओं के लिए सांकेतिक शब्दार्थ विकसित किया गया है जो [[समवर्ती कंप्यूटिंग]] और अपवाद संचालन जैसी क्षमताओं का उपयोग करते हैं, उदाहरण के लिए, [[समवर्ती एमएल]],<ref>John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, ''[[Lecture Notes in Computer Science]]'', Vol. 693. 1993</ref> [[अनुक्रमिक प्रक्रियाओं का संचार करना]],<ref name=Roscoe>[[A. W. Roscoe]]. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.</ref> और [[हास्केल (प्रोग्रामिंग भाषा)]]।<ref>[[Simon Peyton Jones]], Alastair Reid, Fergus Henderson, [[Tony Hoare]], and Simon Marlow. "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.1525&rep=rep1&type=pdf A semantics for imprecise exceptions]" Conference on Programming Language Design and Implementation. 1999.</ref> इन भाषाओं का शब्दार्थ रचनागत है जिसमें एक वाक्यांश का अर्थ उसके उपवाक्यों के अर्थ पर निर्भर करता है। उदाहरण के लिए, [[अनुप्रयोगी प्रोग्रामिंग भाषा]] f(E1,E2) का अर्थ इसके उपवाक्यों f, E1 और E2 के शब्दार्थ के संदर्भ में परिभाषित किया गया है। एक आधुनिक प्रोग्रामिंग भाषा में, E1 और E2 का समवर्ती मूल्यांकन किया जा सकता है और उनमें से एक का निष्पादन ऑब्जेक्ट (कंप्यूटर विज्ञान) के माध्यम से बातचीत करके दूसरे को प्रभावित कर सकता है, जिससे उनके अर्थ एक दूसरे के संदर्भ में परिभाषित हो सकते हैं। इसके अलावा, E1 या E2 एक अपवाद फेंक सकते हैं जो दूसरे के निष्पादन को निरस्त (कंप्यूटिंग) कर सकता है। नीचे दिए गए खंड इन आधुनिक प्रोग्रामिंग भाषाओं के शब्दार्थ के विशेष मामलों का वर्णन करते हैं।
आधुनिक क्रमदेशन भाषाओं के लिए वस्त्वर्थक अर्थविज्ञान विकसित किया गया है जो [[समवर्ती कंप्यूटिंग]] और अपवाद संचालन जैसी क्षमताओं का उपयोग करते हैं, उदाहरण के लिए, [[समवर्ती एमएल|समवर्ती ML]],<ref>John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, ''[[Lecture Notes in Computer Science]]'', Vol. 693. 1993</ref> [[अनुक्रमिक प्रक्रियाओं का संचार करना]],<ref name=Roscoe>[[A. W. Roscoe]]. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.</ref> और [[हास्केल (प्रोग्रामिंग भाषा)|हास्केल (क्रमदेशन भाषा)]]।<ref>[[Simon Peyton Jones]], Alastair Reid, Fergus Henderson, [[Tony Hoare]], and Simon Marlow. "[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.1525&rep=rep1&type=pdf A semantics for imprecise exceptions]" Conference on Programming Language Design and Implementation. 1999.</ref> इन भाषाओं का शब्दार्थ रचनागत है जिसमें एक वाक्यांश का अर्थ उसके उपवाक्यों के अर्थ पर निर्भर करता है। उदाहरण के लिए, [[अनुप्रयोगी प्रोग्रामिंग भाषा|अनुप्रयोगी क्रमदेशन भाषा]] f(E1,E2) का अर्थ इसके उपवाक्यों f, E1 और E2 के शब्दार्थ के संदर्भ में परिभाषित किया गया है। एक आधुनिक क्रमदेशन भाषा में, E1 और E2 का समवर्ती मूल्यांकन किया जा सकता है और उनमें से एक का निष्पादन वस्तु (कंप्यूटर विज्ञान) के माध्यम से बातचीत करके दूसरे को प्रभावित कर सकता है, जिससे उनके अर्थ एक दूसरे के संदर्भ में परिभाषित हो सकते हैं। इसके अतिरिक्त, E1 या E2 एक अपवाद निकाल सकते हैं जो दूसरे के निष्पादन को निरस्त (कंप्यूटिंग) कर सकता है। नीचे दिए गए खंड इन आधुनिक क्रमदेशन भाषाओं के शब्दार्थ के विशेष स्तिथियों का वर्णन करते हैं।


=== पुनरावर्ती कार्यक्रमों का अर्थ ===
=== पुनरावर्ती क्रमादेशों का अर्थ ===
डेनोटेशनल सिमेंटिक्स को एक प्रोग्राम वाक्यांश के रूप में एक वातावरण से एक फ़ंक्शन के रूप में (इसके मुक्त चर के वर्तमान मूल्यों को धारण करते हुए) इसके निरूपण के रूप में वर्णित किया गया है। उदाहरण के लिए, मुहावरा {{code|n*m}} एक ऐसे वातावरण के साथ प्रदान किए जाने पर एक संकेत उत्पन्न करता है जो इसके दो मुक्त चर के लिए बाध्यकारी है: {{code|n}} और {{code|m}}. अगर पर्यावरण में {{code|n}} मान 3 और है {{code|m}} का मान 5 है, तो निरूपण 15 है।<ref name="Research Group Technical Monograph 1971"/>
वस्त्वर्थक अर्थविज्ञान को एक क्रमादेश वाक्यांश के रूप में एक वातावरण से एक फलन के रूप में (इसके मुक्त चर के वर्तमान मूल्यों को धारण करते हुए) इसके निरूपण के रूप में वर्णित किया गया है। उदाहरण के लिए, मुहावरा {{code|n*m}} एक ऐसे वातावरण के साथ प्रदान किए जाने पर एक संकेत उत्पन्न करता है जो इसके दो मुक्त चर {{code|n}}और{{code|m}}के लिए बाध्यकारी है। अगर पर्यावरण में {{code|n}} मान 3 है और {{code|m}} का मान 5 है, तो निरूपण 15 है।<ref name="Research Group Technical Monograph 1971"/>


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


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


इस पुनरावर्ती परिभाषा के लिए एक अर्थ प्रदान करने के लिए, निरूपण को सन्निकटन की सीमा के रूप में बनाया गया है, जहाँ प्रत्येक सन्निकटन फैक्टोरियल के लिए कॉल की संख्या को सीमित करता है। शुरुआत में, हम बिना कॉल के शुरू करते हैं - इसलिए कुछ भी परिभाषित नहीं है। अगले सन्निकटन में, हम [[क्रमित युग्म]] (0,1) जोड़ सकते हैं, क्योंकि इसके लिए फिर से फैक्टोरियल बुलाने की आवश्यकता नहीं है। इसी तरह हम (1,1), (2,2), आदि जोड़ सकते हैं, प्रत्येक क्रमिक सन्निकटन में एक जोड़ी जोड़ सकते हैं क्योंकि कंप्यूटिंग फैक्टोरियल (एन) के लिए n+1 कॉल की आवश्यकता होती है। लिमिट में हमें [[कुल समारोह]] मिलता है <math>\mathbb{N}</math> को <math>\mathbb{N}</math> अपने डोमेन में हर जगह परिभाषित।
<वाक्यविन्यास प्रकाश लैंग = सी> इंट क्रमगुणित (इंट एन) { अगर (एन == 0) तो 1 लौटें; अन्यथा वापसी n * भाज्य (n-1); }<nowiki></syntaxhighlight></nowiki>
 
इस पुनरावर्ती परिभाषा के लिए एक अर्थ प्रदान करने के लिए, निरूपण को सन्निकटन की सीमा के रूप में बनाया गया है, जहाँ प्रत्येक सन्निकटन क्रमगुणित के लिए कॉल की संख्या को सीमित करता है। प्रारम्भ में, हम बिना कॉल के प्रारम्भ करते हैं - इसलिए कुछ भी परिभाषित नहीं होता है। अगले सन्निकटन में, हम [[क्रमित युग्म]] (0,1) जोड़ सकते हैं, क्योंकि इसके लिए फिर से क्रमगुणित बुलाने की आवश्यकता नहीं है। इसी तरह हम (1,1), (2,2), आदि जोड़ सकते हैं, प्रत्येक क्रमिक सन्निकटन में एक जोड़ी जोड़ सकते हैं क्योंकि कंप्यूटिंग क्रमगुणित (n) के लिए n+1 कॉल की आवश्यकता होती है। सीमा में हमें [[कुल समारोह|संपूर्ण फलन]] <math>\mathbb{N}</math> से <math>\mathbb{N}</math> अपने कार्यछेत्र में हर जगह परिभाषित मिलता है।
 
औपचारिक रूप से हम प्रत्येक सन्निकटन को एक आंशिक फलन <math>\N \rightharpoonup \N</math> के रूप में प्रतिरूपित करते हैं। हमारा सन्निकटन तब बार-बार एक फलन को लागू कर रहा है जो एक अधिक परिभाषित आंशिक क्रमगुणित फलन को लागू करता है, अर्थात <math>F : (\N \rightharpoonup \N) \to (\N \rightharpoonup \N) </math>, खाली फलन (खाली सम्मुच्चय) से प्रारम्भ होता है। F को कूट में निम्नानुसार परिभाषित '''किया जा सकता''' है (उपयोग करके <code>Map<int,int></code>  <math>\N \rightharpoonup \N</math> के लिए):


औपचारिक रूप से हम प्रत्येक सन्निकटन को एक आंशिक फलन के रूप में प्रतिरूपित करते हैं  <math>\N \rightharpoonup \N</math>. हमारा सन्निकटन तब बार-बार एक फ़ंक्शन को लागू कर रहा है जो एक अधिक परिभाषित आंशिक फैक्टोरियल फ़ंक्शन को लागू करता है, अर्थात <math>F : (\N \rightharpoonup \N) \to (\N \rightharpoonup \N) </math>, खाली फ़ंक्शन (खाली सेट) से शुरू होता है। F को कोड में निम्नानुसार परिभाषित किया जा सकता है (उपयोग करके <code>Map<int,int></code> के लिए  <math>\N \rightharpoonup \N</math>):
<वाक्यविन्यास लैंग = सीपीपी>
<वाक्यविन्यास लैंग = सीपीपी>
int factorial_nonrecursive (नक्शा <int, int> factorial_less_defined, int n)
int factorial_nonrecursive (नक्शा <int, int> factorial_less_defined, int n)
{
{
   अगर (एन == 0) तो वापसी 1;
   अगर (एन == 0) तो वापसी 1;
   और अगर (fprev = लुकअप (फैक्टोरियल_लेस_डिफाइन्ड, एन -1)) तो
   और अगर (fprev = लुकअप (क्रमगुणित_लेस_डिफाइन्ड, एन -1)) तो
     वापसी n * fprev;
     वापसी n * fprev;
   अन्य
   अन्य
Line 35: Line 37:
मानचित्र <int, int> F (नक्शा <int, int> factorial_less_defined)
मानचित्र <int, int> F (नक्शा <int, int> factorial_less_defined)
{
{
   मानचित्र <int, int> new_फैक्टोरियल = मानचित्र खाली ();
   मानचित्र <int, int> new_क्रमगुणित = मानचित्र खाली ();
   for (int n in all<int>()) {
   for (int n in all<int>()) {
     अगर (f = factorial_nonrecursive (फैक्टोरियल_लेस_डिफ़ाइंड, n)! = NOT_DEFINED)
     अगर (f = factorial_nonrecursive (क्रमगुणित_लेस_डिफ़ाइंड, n)! = NOT_DEFINED)
       new_फैक्टोरियल.पुट (एन, एफ);
       new_क्रमगुणित.पुट (एन, एफ);
   }
   }
   नया_फैक्टोरियल लौटें;
   नया_क्रमगुणित लौटें;
}
}
</वाक्यविन्यास हाइलाइट>
</वाक्यविन्यास हाइलाइट>


तब हम संकेतन F का परिचय दे सकते हैं<sup>n</sup> पुनरावृत्त फ़ंक्शन को इंगित करने के लिए।
तब हम संकेतन F का परिचय दे सकते हैं<sup>n</sup> पुनरावृत्त फलन को इंगित करने के लिए।
* एफ<sup>0</sup>({}) पूरी तरह से अपरिभाषित आंशिक कार्य है, जिसे सेट {} के रूप में दर्शाया गया है;
* एफ<sup>0</sup>({}) पूरी तरह से अपरिभाषित आंशिक कार्य है, जिसे सम्मुच्चय {} के रूप में दर्शाया गया है;
* एफ<sup>1</sup>({}) आंशिक फ़ंक्शन है जिसे सेट {(0,1)} के रूप में दर्शाया गया है: इसे 0 पर परिभाषित किया गया है, 1 होना है, और कहीं और अपरिभाषित है;
* एफ<sup>1</sup>({}) आंशिक फलन है जिसे सम्मुच्चय {(0,1)} के रूप में दर्शाया गया है: इसे 0 पर परिभाषित किया गया है, 1 होना है, और कहीं और अपरिभाषित है;
* एफ<sup>5</sup>({}) आंशिक फ़ंक्शन है जिसे सेट {(0,1), (1,1), (2,2), (3,6), (4,24)} के रूप में दर्शाया गया है: यह तर्क 0,1,2,3,4 के लिए परिभाषित किया गया है।
* एफ<sup>5</sup>({}) आंशिक फलन है जिसे सम्मुच्चय {(0,1), (1,1), (2,2), (3,6), (4,24)} के रूप में दर्शाया गया है: यह तर्क 0,1,2,3,4 के लिए परिभाषित किया गया है।


यह पुनरावृत्त प्रक्रिया आंशिक कार्यों के अनुक्रम का निर्माण करती है <math>\mathbb{N}</math> को <math>\mathbb{N}</math>. आंशिक फ़ंक्शन ⊆ को क्रम के रूप में उपयोग करके एक [[श्रृंखला-पूर्ण आंशिक क्रम]] बनाते हैं। इसके अलावा, फैक्टोरियल फ़ंक्शन के बेहतर सन्निकटन की यह पुनरावृत्त प्रक्रिया एक विस्तृत (जिसे प्रगतिशील भी कहा जाता है) मैपिंग बनाती है क्योंकि प्रत्येक <math>F^i\le F^{i+1}</math> आदेश के रूप में ⊆ का उपयोग करना। तो एक [[निश्चित-बिंदु प्रमेय]] (विशेष रूप से बोरबाकी-विट प्रमेय) द्वारा, इस पुनरावृत्त प्रक्रिया के लिए एक निश्चित बिंदु मौजूद है।
यह पुनरावृत्त प्रक्रिया आंशिक कार्यों के अनुक्रम का निर्माण करती है <math>\mathbb{N}</math> को <math>\mathbb{N}</math>. आंशिक फलन ⊆ को क्रम के रूप में उपयोग करके एक [[श्रृंखला-पूर्ण आंशिक क्रम]] बनाते हैं। इसके अलावा, क्रमगुणित फलन के बेहतर सन्निकटन की यह पुनरावृत्त प्रक्रिया एक विस्तृत (जिसे प्रगतिशील भी कहा जाता है) मानचित्रिंग बनाती है क्योंकि प्रत्येक <math>F^i\le F^{i+1}</math> आदेश के रूप में ⊆ का उपयोग करना। तो एक [[निश्चित-बिंदु प्रमेय]] (विशेष रूप से बोरबाकी-विट प्रमेय) द्वारा, इस पुनरावृत्त प्रक्रिया के लिए एक निश्चित बिंदु मौजूद है।


इस मामले में, निश्चित बिंदु इस श्रृंखला की सबसे कम ऊपरी सीमा है, जो पूर्ण है {{code|factorial}} कार्य, जिसे [[संघ (सेट सिद्धांत)]] के रूप में व्यक्त किया जा सकता है
इस मामले में, निश्चित बिंदु इस श्रृंखला की सबसे कम ऊपरी सीमा है, जो पूर्ण है {{code|factorial}} कार्य, जिसे [[संघ (सेट सिद्धांत)|संघ (सम्मुच्चय सिद्धांत)]] के रूप में व्यक्त किया जा सकता है
:<math>\bigcup_{i \in \mathbb N} F^i(\{\}). </math>
:<math>\bigcup_{i \in \mathbb N} F^i(\{\}). </math>
हमने पाया निश्चित बिंदु एफ का सबसे कम निश्चित बिंदु है, क्योंकि हमारी पुनरावृत्ति डोमेन में सबसे छोटे तत्व (खाली सेट) से शुरू हुई थी। इसे सिद्ध करने के लिए हमें एक अधिक जटिल निश्चित बिंदु प्रमेय की आवश्यकता है जैसे कि नास्टर-टार्स्की प्रमेय।
हमने पाया निश्चित बिंदु एफ का सबसे कम निश्चित बिंदु है, क्योंकि हमारी पुनरावृत्ति कार्यछेत्र में सबसे छोटे तत्व (खाली सम्मुच्चय) से प्रारम्भ हुई थी। इसे सिद्ध करने के लिए हमें एक अधिक जटिल निश्चित बिंदु प्रमेय की आवश्यकता है जैसे कि नास्टर-टार्स्की प्रमेय।


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


गैर-नियतत्ववाद के डोमेन-सैद्धांतिक मॉडल में निष्पक्षता और अबाधित गैर-नियतत्ववाद के साथ कठिनाइयां हैं।<ref>{{cite journal |first=Paul Blain |last=Levy |title=Amb Breaks Well-Pointedness, Ground Amb Doesn't |journal=Electron. Notes Theor. Comput. Sci. |volume=173 |pages=221–239 |year=2007 |doi=10.1016/j.entcs.2007.02.036 |doi-access=free }}</ref>
गैर-नियतत्ववाद के कार्यछेत्र-सैद्धांतिक मॉडल में निष्पक्षता और अबाधित गैर-नियतत्ववाद के साथ कठिनाइयां हैं।<ref>{{cite journal |first=Paul Blain |last=Levy |title=Amb Breaks Well-Pointedness, Ground Amb Doesn't |journal=Electron. Notes Theor. Comput. Sci. |volume=173 |pages=221–239 |year=2007 |doi=10.1016/j.entcs.2007.02.036 |doi-access=free }}</ref>




=== संगामिति का सांकेतिक शब्दार्थ ===
=== संगामिति का वस्त्वर्थक अर्थविज्ञान ===
कई शोधकर्ताओं ने तर्क दिया है कि ऊपर दिए गए डोमेन-सैद्धांतिक मॉडल कॉन्करेंसी (कंप्यूटर विज्ञान) के अधिक सामान्य मामले के लिए पर्याप्त नहीं हैं। इस कारण विभिन्न संगामिति (कंप्यूटर विज्ञान)#मॉडल पेश किए गए हैं। 1980 के दशक की शुरुआत में, लोगों ने समवर्ती भाषाओं के लिए शब्दार्थ देने के लिए सांकेतिक शब्दार्थ की शैली का उपयोग करना शुरू किया। उदाहरणों में अभिनेता मॉडल #क्लिंजर.27एस मॉडल|विल क्लिंजर का अभिनेता मॉडल के साथ काम करना शामिल है; इवेंट स्ट्रक्चर्स और [[पेट्री नेट]] के साथ ग्लिन विंस्केल का काम;<ref>''[https://www.cl.cam.ac.uk/~gw104/eventStructures82.pdf Event Structure Semantics for CCS and Related Languages]''. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.</ref> और फ्रांसेज़, होरे, लेहमन, और डी रोवर (1979) द्वारा सीएसपी के लिए ट्रेस शब्दार्थ पर काम।<ref>[[Nissim Francez]], [[C. A. R. Hoare]], Daniel Lehmann, and [[Willem-Paul de Roever]].  "[https://dspace.library.uu.nl/bitstream/handle/1874/24888/francez_79_Semantics+of+nondeterminism.pdf?sequence=1 Semantics of nondeterminism, concurrency, and communication]", ''Journal of Computer and System Sciences''.  December 1979.</ref> पूछताछ की ये सभी पंक्तियां जांच के अधीन हैं (उदाहरण के लिए सीएसपी के लिए विभिन्न डेनोटेशनल मॉडल देखें<ref name=Roscoe/>).
कई शोधकर्ताओं ने तर्क दिया है कि ऊपर दिए गए कार्यछेत्र-सैद्धांतिक मॉडल कॉन्करेंसी (कंप्यूटर विज्ञान) के अधिक सामान्य मामले के लिए पर्याप्त नहीं हैं। इस कारण विभिन्न संगामिति (कंप्यूटर विज्ञान)#मॉडल पेश किए गए हैं। 1980 के दशक की प्रारम्भ में, लोगों ने समवर्ती भाषाओं के लिए शब्दार्थ देने के लिए वस्त्वर्थक अर्थविज्ञान की शैली का उपयोग करना प्रारम्भ किया। उदाहरणों में अभिनेता मॉडल #क्लिंजर.27एस मॉडल|विल क्लिंजर का अभिनेता मॉडल के साथ काम करना सम्मिलित है; इवेंट स्ट्रक्चर्स और [[पेट्री नेट]] के साथ ग्लिन विंस्केल का काम;<ref>''[https://www.cl.cam.ac.uk/~gw104/eventStructures82.pdf Event Structure Semantics for CCS and Related Languages]''. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.</ref> और फ्रांसेज़, होरे, लेहमन, और डी रोवर (1979) द्वारा सीएसपी के लिए ट्रेस शब्दार्थ पर काम।<ref>[[Nissim Francez]], [[C. A. R. Hoare]], Daniel Lehmann, and [[Willem-Paul de Roever]].  "[https://dspace.library.uu.nl/bitstream/handle/1874/24888/francez_79_Semantics+of+nondeterminism.pdf?sequence=1 Semantics of nondeterminism, concurrency, and communication]", ''Journal of Computer and System Sciences''.  December 1979.</ref> पूछताछ की ये सभी पंक्तियां जांच के अधीन हैं (उदाहरण के लिए सीएसपी के लिए विभिन्न डेनोटेशनल मॉडल देखें<ref name=Roscoe/>).


हाल ही में, विंस्केल और अन्य ने संगति के लिए एक डोमेन सिद्धांत के रूप में प्रोफेसरों की श्रेणी का प्रस्ताव दिया है।<ref>{{cite journal |first1=Gian Luca |last1=Cattani |first2=Glynn |last2=Winskel |title=Profunctors, open maps and bisimulation |journal=Mathematical Structures in Computer Science |volume=15 |issue=3 |pages=553–614 |year=2005 |doi= 10.1017/S0960129505004718|citeseerx=10.1.1.111.6243 |s2cid=16356708 }}</ref><ref>{{cite journal |first1=Mikkel |last1=Nygaard |first2=Glynn |last2=Winskel |title=Domain theory for concurrency |journal=Theor. Comput. Sci. |volume=316 |issue=1–3 |pages=153–190 |year=2004 |doi=10.1016/j.tcs.2004.01.029 |doi-access=free }}</ref>
हाल ही में, विंस्केल और अन्य ने संगति के लिए एक कार्यछेत्र सिद्धांत के रूप में प्रोफेसरों की श्रेणी का प्रस्ताव दिया है।<ref>{{cite journal |first1=Gian Luca |last1=Cattani |first2=Glynn |last2=Winskel |title=Profunctors, open maps and bisimulation |journal=Mathematical Structures in Computer Science |volume=15 |issue=3 |pages=553–614 |year=2005 |doi= 10.1017/S0960129505004718|citeseerx=10.1.1.111.6243 |s2cid=16356708 }}</ref><ref>{{cite journal |first1=Mikkel |last1=Nygaard |first2=Glynn |last2=Winskel |title=Domain theory for concurrency |journal=Theor. Comput. Sci. |volume=316 |issue=1–3 |pages=153–190 |year=2004 |doi=10.1016/j.tcs.2004.01.029 |doi-access=free }}</ref>




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


स्थानीय चरों के साथ मॉडलिंग कार्यक्रमों में चीजें अधिक कठिन हो जाती हैं। एक दृष्टिकोण अब डोमेन के साथ काम नहीं करना है, बल्कि दुनिया की कुछ श्रेणी से लेकर डोमेन की श्रेणी तक [[ऑपरेटर]] के रूप में प्रकारों की व्याख्या करना है। कार्यक्रमों को तब इन फ़ैक्टरों के बीच [[प्राकृतिक परिवर्तन]] निरंतर कार्यों द्वारा निरूपित किया जाता है।<ref>[[Peter W. O'Hearn]], John Power, [[Robert D. Tennent]], Makoto Takeyama. Syntactic control of interference revisited. ''Electron. Notes Theor. Comput. Sci.'' 1. 1995.</ref><ref>Frank J. Oles. ''A Category-Theoretic Approach to the Semantics of Programming''. PhD thesis, [[Syracuse University]], New York, USA. 1982.</ref>
स्थानीय चरों के साथ मॉडलिंग क्रमादेशों में चीजें अधिक कठिन हो जाती हैं। एक दृष्टिकोण अब कार्यछेत्र के साथ काम नहीं करना है, बल्कि दुनिया की कुछ श्रेणी से लेकर कार्यछेत्र की श्रेणी तक [[ऑपरेटर]] के रूप में प्रकारों की व्याख्या करना है। क्रमादेशों को तब इन फ़ैक्टरों के बीच [[प्राकृतिक परिवर्तन]] निरंतर कार्यों द्वारा निरूपित किया जाता है।<ref>[[Peter W. O'Hearn]], John Power, [[Robert D. Tennent]], Makoto Takeyama. Syntactic control of interference revisited. ''Electron. Notes Theor. Comput. Sci.'' 1. 1995.</ref><ref>Frank J. Oles. ''A Category-Theoretic Approach to the Semantics of Programming''. PhD thesis, [[Syracuse University]], New York, USA. 1982.</ref>




=== डेटा प्रकार के संकेत ===
=== डेटा प्रकार के संकेत ===
कई प्रोग्रामिंग भाषाएँ उपयोगकर्ताओं को [[पुनरावर्ती डेटा प्रकार]]ों को परिभाषित करने की अनुमति देती हैं। उदाहरण के लिए, संख्याओं की सूचियों के प्रकार को किसके द्वारा निर्दिष्ट किया जा सकता है
कई क्रमदेशन भाषाएँ उपयोगकर्ताओं को [[पुनरावर्ती डेटा प्रकार]]ों को परिभाषित करने की अनुमति देती हैं। उदाहरण के लिए, संख्याओं की सूचियों के प्रकार को किसके द्वारा निर्दिष्ट किया जा सकता है
<syntaxhighlight lang=sml>datatype list = nat * list | खाली</syntaxhighlight>
<syntaxhighlight lang=sml>datatype list = nat * list | खाली</syntaxhighlight>
यह खंड केवल कार्यात्मक डेटा संरचनाओं से संबंधित है जो बदल नहीं सकते हैं। परंपरागत अनिवार्य प्रोग्रामिंग भाषाएं आमतौर पर ऐसी पुनरावर्ती सूची के तत्वों को बदलने की अनुमति देती हैं।
यह खंड केवल कार्यात्मक डेटा संरचनाओं से संबंधित है जो बदल नहीं सकते हैं। परंपरागत अनिवार्य क्रमदेशन भाषाएं आमतौर पर ऐसी पुनरावर्ती सूची के तत्वों को बदलने की अनुमति देती हैं।


एक अन्य उदाहरण के लिए: [[अनटाइप्ड लैम्ब्डा कैलकुलस]] के डिनोटेशन का प्रकार है
एक अन्य उदाहरण के लिए: [[अनटाइप्ड लैम्ब्डा कैलकुलस]] के डिनोटेशन का प्रकार है
<syntaxhighlight lang=sml>डेटाटाइप D = D of (D → D)</syntaxhighlight>
<syntaxhighlight lang=sml>डेटाटाइप D = D of (D → D)</syntaxhighlight>
डोमेन समीकरणों को हल करने की समस्या उन डोमेन को खोजने से संबंधित है जो इस प्रकार के डेटाटाइप्स को मॉडल करते हैं। एक दृष्टिकोण, मोटे तौर पर बोलना, सभी डोमेन के संग्रह को एक डोमेन के रूप में मानना ​​​​है, और फिर वहाँ पुनरावर्ती परिभाषा को हल करना है। नीचे दी गई पाठ्यपुस्तकें अधिक विवरण देती हैं।
कार्यछेत्र समीकरणों को हल करने की समस्या उन कार्यछेत्र को खोजने से संबंधित है जो इस प्रकार के डेटाटाइप्स को मॉडल करते हैं। एक दृष्टिकोण, मोटे तौर पर बोलना, सभी कार्यछेत्र के संग्रह को एक कार्यछेत्र के रूप में मानना ​​​​है, और फिर वहाँ पुनरावर्ती परिभाषा को हल करना है। नीचे दी गई पाठ्यपुस्तकें अधिक विवरण देती हैं।


[[बहुरूपता (कंप्यूटर विज्ञान)]] डेटा प्रकार हैं जिन्हें एक पैरामीटर के साथ परिभाषित किया गया है। उदाहरण के लिए, α का प्रकार {{code|list}}एस द्वारा परिभाषित किया गया है
[[बहुरूपता (कंप्यूटर विज्ञान)]] डेटा प्रकार हैं जिन्हें एक पैरामीटर के साथ परिभाषित किया गया है। उदाहरण के लिए, α का प्रकार {{code|list}}एस द्वारा परिभाषित किया गया है
Line 86: Line 88:
प्राकृतिक संख्याओं की सूची, तब, प्रकार की होती है {{code|nat list}}, जबकि स्ट्रिंग्स की सूचियाँ हैं {{code|string list}}.
प्राकृतिक संख्याओं की सूची, तब, प्रकार की होती है {{code|nat list}}, जबकि स्ट्रिंग्स की सूचियाँ हैं {{code|string list}}.


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


हाल ही के एक शोध क्षेत्र में वस्तु और वर्ग आधारित प्रोग्रामिंग भाषाओं के लिए सांकेतिक शब्दार्थ शामिल है।<ref>{{cite journal |first1=Bernhard |last1=Reus |first2=Thomas |last2=Streicher |title=Semantics and logic of object calculi |journal=Theor. Comput. Sci. |volume=316|issue=1 |pages=191–213 |year=2004 |doi=10.1016/j.tcs.2004.01.030 |doi-access=free }}</ref>
हाल ही के एक शोध क्षेत्र में वस्तु और वर्ग आधारित क्रमदेशन भाषाओं के लिए वस्त्वर्थक अर्थविज्ञान सम्मिलित है।<ref>{{cite journal |first1=Bernhard |last1=Reus |first2=Thomas |last2=Streicher |title=Semantics and logic of object calculi |journal=Theor. Comput. Sci. |volume=316|issue=1 |pages=191–213 |year=2004 |doi=10.1016/j.tcs.2004.01.030 |doi-access=free }}</ref>




===प्रतिबंधित जटिलता के कार्यक्रमों के लिए सांकेतिक शब्दार्थ ===
===प्रतिबंधित जटिलता के क्रमादेशों के लिए वस्त्वर्थक अर्थविज्ञान ===
रेखीय तर्क पर आधारित प्रोग्रामिंग भाषाओं के विकास के बाद, रेखीय उपयोग के लिए भाषाओं को सांकेतिक शब्दार्थ दिया गया है (उदाहरण के लिए [[सबूत जाल]], [[सुसंगत स्थान]] देखें) और बहुपद समय जटिलता भी।<ref>{{cite journal |first=P. |last=Baillot |title=Stratified coherence spaces: a denotational semantics for Light Linear Logic |journal=Theor. Comput. Sci. |volume=318 |issue=1–2 |pages=29–55 |year=2004 |doi=10.1016/j.tcs.2003.10.015 |doi-access=free }}</ref>
रेखीय तर्क पर आधारित क्रमदेशन भाषाओं के विकास के बाद, रेखीय उपयोग के लिए भाषाओं को वस्त्वर्थक अर्थविज्ञान दिया गया है (उदाहरण के लिए [[सबूत जाल]], [[सुसंगत स्थान]] देखें) और बहुपद समय जटिलता भी।<ref>{{cite journal |first=P. |last=Baillot |title=Stratified coherence spaces: a denotational semantics for Light Linear Logic |journal=Theor. Comput. Sci. |volume=318 |issue=1–2 |pages=29–55 |year=2004 |doi=10.1016/j.tcs.2003.10.015 |doi-access=free }}</ref>




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


यह खुला प्रश्न ज्यादातर 1990 के दशक में [[खेल शब्दार्थ]] के विकास और [[तार्किक संबंध]]ों से जुड़ी तकनीकों के साथ हल किया गया था।<ref>{{cite journal |first1=P.W. |last1=O'Hearn |first2=J.G. |last2=Riecke |title=Kripke Logical Relations and PCF |journal=Information and Computation |volume=120 |issue=1 |pages=107–116 |date=July 1995 |doi=10.1006/inco.1995.1103 |s2cid=6886529 |url=https://surface.syr.edu/lcsmith_other/3 |doi-access=free }}</ref> अधिक जानकारी के लिए, पीसीएफ पर पेज देखें।
यह खुला प्रश्न ज्यादातर 1990 के दशक में [[खेल शब्दार्थ]] के विकास और [[तार्किक संबंध]]ों से जुड़ी तकनीकों के साथ हल किया गया था।<ref>{{cite journal |first1=P.W. |last1=O'Hearn |first2=J.G. |last2=Riecke |title=Kripke Logical Relations and PCF |journal=Information and Computation |volume=120 |issue=1 |pages=107–116 |date=July 1995 |doi=10.1006/inco.1995.1103 |s2cid=6886529 |url=https://surface.syr.edu/lcsmith_other/3 |doi-access=free }}</ref> अधिक जानकारी के लिए, पीसीएफ पर पेज देखें।


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


इस संदर्भ में, सांकेतिक शब्दार्थ से धारणाएं, जैसे पूर्ण अमूर्तता, सुरक्षा चिंताओं को पूरा करने में मदद करती हैं।<ref>Martin Abadi. "Protection in programming-language translations". ''Proc. of ICALP'98''. LNCS 1443. 1998.</ref><ref>{{cite journal |first=Andrew |last=Kennedy |title=Securing the .NET programmingmodel |journal=Theor. Comput. Sci. |volume=364 |issue=3 |pages=311–7 |year=2006|doi=10.1016/j.tcs.2006.08.014 |doi-access=free }}</ref>
इस संदर्भ में, वस्त्वर्थक अर्थविज्ञान से धारणाएं, जैसे पूर्ण अमूर्तता, सुरक्षा चिंताओं को पूरा करने में मदद करती हैं।<ref>Martin Abadi. "Protection in programming-language translations". ''Proc. of ICALP'98''. LNCS 1443. 1998.</ref><ref>{{cite journal |first=Andrew |last=Kennedy |title=Securing the .NET programmingmodel |journal=Theor. Comput. Sci. |volume=364 |issue=3 |pages=311–7 |year=2006|doi=10.1016/j.tcs.2006.08.014 |doi-access=free }}</ref>




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


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


अतिरिक्त वांछनीय गुण जिन्हें हम परिचालन और सांकेतिक शब्दार्थ के बीच रखना चाहते हैं:
अतिरिक्त वांछनीय गुण जिन्हें हम परिचालन और वस्त्वर्थक अर्थविज्ञान के बीच रखना चाहते हैं:
#Constructivism: रचनावाद (गणित) का संबंध इस बात से है कि क्या डोमेन तत्वों को रचनात्मक तरीकों से मौजूद दिखाया जा सकता है।
#Constructivism: रचनावाद (गणित) का संबंध इस बात से है कि क्या कार्यछेत्र तत्वों को रचनात्मक तरीकों से मौजूद दिखाया जा सकता है।
# निरूपण और परिचालन शब्दार्थ की स्वतंत्रता: सांकेतिक शब्दार्थ को गणितीय संरचनाओं का उपयोग करके औपचारिक रूप दिया जाना चाहिए जो एक प्रोग्रामिंग भाषा के परिचालन शब्दार्थ से स्वतंत्र हैं; हालांकि, अंतर्निहित अवधारणाएं निकटता से संबंधित हो सकती हैं। नीचे denotational semantics#Compositionality पर अनुभाग देखें।
# निरूपण और परिचालन शब्दार्थ की स्वतंत्रता: वस्त्वर्थक अर्थविज्ञान को गणितीय संरचनाओं का उपयोग करके औपचारिक रूप दिया जाना चाहिए जो एक क्रमदेशन भाषा के परिचालन शब्दार्थ से स्वतंत्र हैं; हालांकि, अंतर्निहित अवधारणाएं निकटता से संबंधित हो सकती हैं। नीचे denotational semantics#Compositionality पर अनुभाग देखें।
# पूर्ण पूर्णता या निश्चितता: सिमेंटिक मॉडल का प्रत्येक रूपवाद एक कार्यक्रम का प्रतीक होना चाहिए।<ref>{{cite journal
# पूर्ण पूर्णता या निश्चितता: सिमेंटिक मॉडल का प्रत्येक रूपवाद एक क्रमादेश का प्रतीक होना चाहिए।<ref>{{cite journal
   | last = Curien
   | last = Curien
   | first = Pierre-Louis
   | first = Pierre-Louis
Line 130: Line 132:


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


डोमेन थ्योरी में एक बुनियादी निरूपण शब्दार्थ रचनात्मक है क्योंकि इसे निम्नानुसार दिया गया है। हम कार्यक्रम के अंशों पर विचार करके शुरू करते हैं, अर्थात मुक्त चर वाले कार्यक्रम। एक टाइपिंग संदर्भ प्रत्येक मुक्त चर के लिए एक प्रकार प्रदान करता है। उदाहरण के लिए, अभिव्यक्ति में (x + y) को टाइपिंग संदर्भ में माना जा सकता है (x:{{code|nat}},और:{{code|nat}}). अब हम निम्नलिखित योजना का उपयोग करते हुए, अंशों को प्रोग्राम करने के लिए एक सांकेतिक शब्दार्थ देते हैं।
कार्यछेत्र थ्योरी में एक बुनियादी निरूपण शब्दार्थ रचनात्मक है क्योंकि इसे निम्नानुसार दिया गया है। हम क्रमादेश के अंशों पर विचार करके प्रारम्भ करते हैं, अर्थात मुक्त चर वाले क्रमादेश। एक टाइपिंग संदर्भ प्रत्येक मुक्त चर के लिए एक प्रकार प्रदान करता है। उदाहरण के लिए, अभिव्यक्ति में (x + y) को टाइपिंग संदर्भ में माना जा सकता है (x:{{code|nat}},और:{{code|nat}}). अब हम निम्नलिखित योजना का उपयोग करते हुए, अंशों को क्रमादेश करने के लिए एक वस्त्वर्थक अर्थविज्ञान देते हैं।
# हम अपनी भाषा के प्रकार के अर्थ का वर्णन करते हुए शुरू करते हैं: प्रत्येक प्रकार का अर्थ एक डोमेन होना चाहिए। हम टाइप τ को दर्शाने वाले डोमेन के लिए 〚τ〛 लिखते हैं। उदाहरण के लिए, प्रकार का अर्थ {{code|nat}} प्राकृतिक संख्याओं का डोमेन होना चाहिए: 〚{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>.
# हम अपनी भाषा के प्रकार के अर्थ का वर्णन करते हुए प्रारम्भ करते हैं: प्रत्येक प्रकार का अर्थ एक कार्यछेत्र होना चाहिए। हम टाइप τ को दर्शाने वाले कार्यछेत्र के लिए 〚τ〛 लिखते हैं। उदाहरण के लिए, प्रकार का अर्थ {{code|nat}} प्राकृतिक संख्याओं का कार्यछेत्र होना चाहिए: 〚{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>.
# प्रकार के अर्थ से हम टाइपिंग संदर्भों के लिए एक अर्थ प्राप्त करते हैं। हमने 'एक्स' सेट किया है<sub>1</sub>:टी<sub>1</sub>,..., एक्स<sub>n</sub>:टी<sub>n</sub>〛 = 〚 वर्ग<sub>1</sub>〛× ... ×〚टी<sub>n</sub>〛। उदाहरण के लिए, 'एक्स:{{code|nat}},और:{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>. एक विशेष मामले के रूप में, खाली टाइपिंग संदर्भ का अर्थ, बिना चर के, एक तत्व वाला डोमेन है, जिसे 1 दर्शाया गया है।
# प्रकार के अर्थ से हम टाइपिंग संदर्भों के लिए एक अर्थ प्राप्त करते हैं। हमने 'एक्स' सम्मुच्चय किया है<sub>1</sub>:टी<sub>1</sub>,..., एक्स<sub>n</sub>:टी<sub>n</sub>〛 = 〚 वर्ग<sub>1</sub>〛× ... ×〚टी<sub>n</sub>〛। उदाहरण के लिए, 'एक्स:{{code|nat}},और:{{code|nat}}〛= <math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>. एक विशेष मामले के रूप में, खाली टाइपिंग संदर्भ का अर्थ, बिना चर के, एक तत्व वाला कार्यछेत्र है, जिसे 1 दर्शाया गया है।
# अंत में, हमें प्रत्येक प्रोग्राम-टुकड़ा-इन-टाइपिंग-संदर्भ को एक अर्थ देना चाहिए। मान लीजिए कि पी प्रकार σ का एक प्रोग्राम टुकड़ा है, टाइपिंग संदर्भ में Γ, अक्सर Γ⊢P:σ लिखा जाता है। फिर इस प्रोग्राम-इन-टाइपिंग-संदर्भ का अर्थ एक सतत कार्य होना चाहिए 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛। उदाहरण के लिए, 〚⊢7:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub> लगातार 7 कार्य है, जबकि 〚x:{{code|nat}},और:{{code|nat}}⊢x+y:{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub> वह कार्य है जो दो संख्याओं को जोड़ता है।
# अंत में, हमें प्रत्येक क्रमादेश-टुकड़ा-इन-टाइपिंग-संदर्भ को एक अर्थ देना चाहिए। मान लीजिए कि पी प्रकार σ का एक क्रमादेश टुकड़ा है, टाइपिंग संदर्भ में Γ, अक्सर Γ⊢P:σ लिखा जाता है। फिर इस क्रमादेश-इन-टाइपिंग-संदर्भ का अर्थ एक सतत कार्य होना चाहिए 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛। उदाहरण के लिए, 〚⊢7:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub> लगातार 7 कार्य है, जबकि 〚x:{{code|nat}},और:{{code|nat}}⊢x+y:{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub> वह कार्य है जो दो संख्याओं को जोड़ता है।


अब, यौगिक व्यंजक (7+4) का अर्थ तीन कार्यों 〚⊢7 को मिलाकर निर्धारित किया जाता है:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, 〚⊢4:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, और "एक्स:{{code|nat}},और:{{code|nat}}⊢x+y:{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub>.
अब, यौगिक व्यंजक (7+4) का अर्थ तीन कार्यों 〚⊢7 को मिलाकर निर्धारित किया जाता है:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, 〚⊢4:{{code|nat}}〛:1→<math>\mathbb{N}</math><sub>⊥</sub>, और "एक्स:{{code|nat}},और:{{code|nat}}⊢x+y:{{code|nat}}〛:<math>\mathbb{N}</math><sub>⊥</sub>×<math>\mathbb{N}</math><sub>⊥</sub>→<math>\mathbb{N}</math><sub>⊥</sub>.


वास्तव में, यह संरचनागत निरूपण शब्दार्थ के लिए एक सामान्य योजना है। यहां डोमेन और निरंतर कार्यों के बारे में कुछ खास नहीं है। कोई इसके बजाय एक अलग [[श्रेणी (गणित)]] के साथ काम कर सकता है। उदाहरण के लिए, खेल शब्दार्थ में, खेलों की श्रेणी में वस्तुओं के रूप में खेल और आकारिकी के रूप में रणनीतियाँ होती हैं: हम प्रकारों को खेलों के रूप में और कार्यक्रमों को रणनीतियों के रूप में व्याख्या कर सकते हैं। सामान्य पुनरावर्तन के बिना एक सरल भाषा के लिए, हम [[सेट की श्रेणी]] के साथ काम कर सकते हैं। साइड-इफेक्ट्स वाली भाषा के लिए, हम [[क्लेस्ली श्रेणी]] में एक सन्यासी के लिए काम कर सकते हैं। राज्य के साथ भाषा के लिए, हम functor श्रेणी में काम कर सकते हैं। [[रॉबिन मिलनर]] ने वस्तुओं के रूप में इंटरफेस और आकारिकी के रूप में [[bigraphs]] के साथ एक श्रेणी में काम करके मॉडलिंग स्थान और बातचीत की वकालत की है।<ref>{{cite book |first=Robin |last=Milner |title=The Space and Motion of Communicating Agents |publisher=Cambridge University Press |year=2009 |isbn=978-0-521-73833-0 }} [https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf 2009 draft] {{webarchive|url=https://web.archive.org/web/20120402095417/https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf |date=2012-04-02 }}.</ref>
वास्तव में, यह संरचनागत निरूपण शब्दार्थ के लिए एक सामान्य योजना है। यहां कार्यछेत्र और निरंतर कार्यों के बारे में कुछ खास नहीं है। कोई इसके बजाय एक अलग [[श्रेणी (गणित)]] के साथ काम कर सकता है। उदाहरण के लिए, खेल शब्दार्थ में, खेलों की श्रेणी में वस्तुओं के रूप में खेल और आकारिकी के रूप में रणनीतियाँ होती हैं: हम प्रकारों को खेलों के रूप में और क्रमादेशों को रणनीतियों के रूप में व्याख्या कर सकते हैं। सामान्य पुनरावर्तन के बिना एक सरल भाषा के लिए, हम [[सेट की श्रेणी|सम्मुच्चय की श्रेणी]] के साथ काम कर सकते हैं। साइड-इफेक्ट्स वाली भाषा के लिए, हम [[क्लेस्ली श्रेणी]] में एक सन्यासी के लिए काम कर सकते हैं। राज्य के साथ भाषा के लिए, हम functor श्रेणी में काम कर सकते हैं। [[रॉबिन मिलनर]] ने वस्तुओं के रूप में इंटरफेस और आकारिकी के रूप में [[bigraphs]] के साथ एक श्रेणी में काम करके मॉडलिंग स्थान और बातचीत की वकालत की है।<ref>{{cite book |first=Robin |last=Milner |title=The Space and Motion of Communicating Agents |publisher=Cambridge University Press |year=2009 |isbn=978-0-521-73833-0 }} [https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf 2009 draft] {{webarchive|url=https://web.archive.org/web/20120402095417/https://blog.itu.dk/SMDS-F2010/files/2010/04/milner-2009-the-space-and-motion-of-communicating-agents.pdf |date=2012-04-02 }}.</ref>




Line 147: Line 149:


क्लिंजर (1981) के अनुसार:<ref name="clinger1981">{{cite document |first=William D. |last=Clinger |title=Foundations of Actor Semantics |year=1981 |type=PhD |publisher=Massachusetts Institute of Technology |id=AITR-633 |hdl=1721.1/6935}}</ref>{{rp|79}}
क्लिंजर (1981) के अनुसार:<ref name="clinger1981">{{cite document |first=William D. |last=Clinger |title=Foundations of Actor Semantics |year=1981 |type=PhD |publisher=Massachusetts Institute of Technology |id=AITR-633 |hdl=1721.1/6935}}</ref>{{rp|79}}
: आमतौर पर, हालांकि, एक पारंपरिक अनुक्रमिक प्रोग्रामिंग भाषा के औपचारिक शब्दार्थ को भाषा के एक (अकुशल) कार्यान्वयन प्रदान करने के लिए व्याख्या की जा सकती है। एक औपचारिक शब्दार्थ को हमेशा ऐसा कार्यान्वयन प्रदान करने की आवश्यकता नहीं होती है, और यह मानने के लिए कि शब्दार्थ को एक कार्यान्वयन प्रदान करना चाहिए, समवर्ती भाषाओं के औपचारिक शब्दार्थ के बारे में भ्रम पैदा करता है। इस तरह का भ्रम स्पष्ट रूप से स्पष्ट है जब एक प्रोग्रामिंग भाषा के शब्दार्थ में अबाधित अनिर्धारणवाद की उपस्थिति का अर्थ यह है कि प्रोग्रामिंग भाषा को लागू नहीं किया जा सकता है।
: आमतौर पर, हालांकि, एक पारंपरिक अनुक्रमिक क्रमदेशन भाषा के औपचारिक शब्दार्थ को भाषा के एक (अकुशल) कार्यान्वयन प्रदान करने के लिए व्याख्या की जा सकती है। एक औपचारिक शब्दार्थ को हमेशा ऐसा कार्यान्वयन प्रदान करने की आवश्यकता नहीं होती है, और यह मानने के लिए कि शब्दार्थ को एक कार्यान्वयन प्रदान करना चाहिए, समवर्ती भाषाओं के औपचारिक शब्दार्थ के बारे में भ्रम पैदा करता है। इस तरह का भ्रम स्पष्ट रूप से स्पष्ट है जब एक क्रमदेशन भाषा के शब्दार्थ में अबाधित अनिर्धारणवाद की उपस्थिति का अर्थ यह है कि क्रमदेशन भाषा को लागू नहीं किया जा सकता है।


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


==संदर्भ==
==संदर्भ==

Revision as of 08:52, 24 February 2023

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

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


बाहरी संबंध