कर्ता मॉडल सिद्धांत

From Vigyanwiki

सैद्धांतिक कंप्यूटर विज्ञान में, कर्ता मॉडल सिद्धांत (एक्टर मॉडल थ्योरी) कर्ता मॉडल के लिए सैद्धांतिक मुद्दों से संबंधित है।

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

घटनाक्रम और उनके आदेश

कर्ता की परिभाषा से, यह देखा जा सकता है कि कई घटनाएँ घटित होती हैं: सीमित निर्णय, कर्ताओं का निर्माण, संदेश भेजना, संदेश प्राप्त करना, और यह निर्धारित करना कि प्राप्त अगले संदेश का जवाब कैसे दिया जाए।

हालाँकि, यह लेख केवल उन इवेंट पर केंद्रित है जो कर्ता को भेजे गए संदेश का आगमन हैं।

यह लेख हेविट [2006] में प्रकाशित परिणामों पर रिपोर्ट करता है।

गणनीयता का नियम: अधिक से अधिक संख्या में कई घटनाएँ होती हैं।

सक्रियण आदेश

सक्रियण आदेश (-≈→) मौलिक क्रम है जो एक इवेंट को दूसरे को सक्रिय करता है (किसी इवेंट से किसी इवेंट को सक्रिय करने वाले संदेश में ऊर्जा प्रवाह होना चाहिए)।

  • ऊर्जा के संचरण के कारण, सक्रियण क्रम सामान्य सापेक्षता अपरिवर्तनीय (भौतिकी) है; यानी सभी इवेंट के लिए e1.e2, यदि e1 -≈→ e2, तो e1 का समय सभी पर्यवेक्षकों के संदर्भ के सापेक्षतावादी फ्रेम में e2 के समय से पहले होता है।
  • एक्टिवेशन ऑर्डरिंग के लिए सख्त आकस्मिकता का नियम: किसी भी इवेंट के लिए e -≈→ e नहीं करता है।
  • एक्टिवेशन ऑर्डरिंग में परिमित पूर्वनिर्धारण का नियम: सभी इवेंट के लिए e1 सेट {e|e -≈→ e1} परिमित है।

आगमन आदेश

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

  • क्योंकि कर्ता के आगमन आदेश की सभी घटनाएँ x की विश्व रेखा पर होती हैं, x, कर्ता का आगमन क्रम सापेक्ष रूप से अपरिवर्तनीय है। यानी सभी कर्ताओं x और घटनाएँ e1.e2, के लिए, यदि e1 -x→ e2, तो e1 का समय सभी पर्यवेक्षकों के संदर्भ के सापेक्ष फ्रेम में e2 के समय से पहले होता है।
  • आगमन आदेश में परिमित पूर्वनिर्धारण का नियम: सभी इवेंट e1 और कर्ता x के लिए सेट {e|e -x→ e1} परिमित है।

संयुक्त आदेश

संयुक्त आदेश ( → द्वारा चिह्नित) को सक्रियण आदेश के सकर्मक समापन और सभी कर्ताओं के आगमन क्रम के रूप में परिभाषित किया गया है।

  • संयुक्त क्रम सापेक्षतावादी रूप से अपरिवर्तनीय है क्योंकि यह सापेक्षिक रूप से अपरिवर्तनीय क्रमों का सकर्मक समापन है। यानी, सभी इवेंट के लिए e1.e2, यदि e1→e2, तब e1 का समय सभी पर्यवेक्षकों के संदर्भ के सापेक्षतावादी फ्रेम में e2 के समय से पहले आता है।
  • संयुक्त आदेश के लिए सख्त आकस्मिकता का नियम: किसी भी इवेंट के लिए e→e नहीं होता है।

परिभाषा के अनुसार संयुक्त क्रम स्पष्ट रूप से सकर्मक है।

[बेकर और हेविट 197?] में, यह अनुमान लगाया गया था कि उपरोक्त नियम में निम्नलिखित नियम सम्मिलित हो सकते हैं:

संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला का नियम: संयुक्त क्रम में दो इवेंट के बीच इवेंट की कोई अनंत श्रृंखला (यानी, रैखिक रूप से आदेशित सेट) नहीं हैं →।

संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला के नियम की स्वतंत्रता

हालाँकि, [क्लिंगर 1981] ने आश्चर्यजनक रूप से यह सिद्ध कर दिया कि संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला का नियम पिछले नियम से स्वतंत्र है, अर्थात,

प्रमेय. संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला का नियम पहले बताए गए नियम का पालन नहीं करता है।

प्रमाण. यह दिखाने के लिए पर्याप्त है कि कर्ता संगणना है जो पहले बताए गए नियम को संतुष्ट करती है लेकिन संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला के नियम का उल्लंघन करती है।

संगणना पर विचार करें जो तब प्रारंभ होती है जब कर्ता को प्रारंभिक Start संदेश भेजा जाता है जिसके कारण यह निम्नलिखित क्रियाएं करता है
  1. एक नए कर्ता ग्रीटर1 बनाएं जिसे ग्रीटर1 के पते के साथSayHelloTo संदेश भेजा जाता है:
  2. संदेश के पहले अक्षर भेजें Again ग्रीटर के पते के साथ1: तत्पश्चात् आद्याक्षर का व्यवहार प्राप्त होने पर इस प्रकार है Again पते के साथ संदेश ग्रीटेरी (जिसे हम इवेंट कहेंगे Againi):
  3. नए कर्ता ग्रीटरi+1बनाएँ जिसे संदेश SayHelloTo ग्रीटरi के पते के साथ भेजा जाता है
  4. ग्रीटर i+1 Again संदेश को आद्याक्षर भेजें स्पष्ट रूप से आरंभिक संदेश Again भेजने की गणना कभी समाप्त नहीं होती है।
प्रत्येक कर्ता का व्यवहार ग्रीटरi इस प्रकार है:
* जब यह संदेश प्राप्त करता है SayHelloTo ग्रीटर i-1 के पते के साथ (जिसे हम इवेंट कहेंगे SayHelloToi), यह भेजता है Hello ग्रीटरi-1 को संदेश:
  • जब यह प्राप्त करता है Hello संदेश (जिसे हम ईवेंट कहेंगे Helloi), यह कुछ नहीं करता है।
अब ऐसा हो सकता है Helloi -GreeteriSayHelloToi हर बार और इसलिए HelloiSayHelloToi.
Againi -≈→ Againi+1 हर बार भी और इसलिए AgainiAgaini+1
इसके अतिरिक्त संयुक्त आदेश के लिए सख्त आकस्मिकता के नियम से पहले बताए गए सभी नियम संतुष्ट हैं।
चूंकि, संयुक्त क्रम में इवेंट की अनंत संख्या हो सकती है Again1 और SayHelloTo1 निम्नलिखित नुसार:
Again1→...→Againi→......→HelloiSayHelloToi→...→Hello1SayHelloTo1

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

विच्छेद का नियम

संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला का नियम निम्नलिखित नियम से निकटता से संबंधित है:

विच्छेद का नियम: सभी इवेंट के लिए e1 और e2, सेट {e|e1→e→e2} परिमित है।

वास्तव में पिछले दो नियम को समकक्ष दिखाया गया है:

प्रमेय [क्लिंजर 1981]. पृथकता का नियम संयुक्त क्रम में इवेंट के बीच परिमित श्रृंखला के नियम के बराबर है (पसंद के स्वयंसिद्ध का उपयोग किए बिना।)

असततता का नियम ज़ेनो मशीन को नियमबद्ध करता है और पेट्री नेट पर परिणामों से संबंधित है [बेस्ट एट अल. 1984, 1987]।

असततता के नियम का अर्थ है असीमित अनिर्धारणवाद का गुण। संयुक्त आदेश का उपयोग [क्लिंगर 1981] द्वारा कर्ताओं के सांकेतिक मॉडल के निर्माण में किया जाता है (सांकेतिक शब्दार्थ देखें)।

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

क्लिंजर [1981] ने पावर डोमेन का उपयोग करने वाले कर्ताओं के लिए डेनोटेशनल मॉडल बनाने के लिए ऊपर वर्णित अभिनेता इवेंट मॉडल का उपयोग किया है। बाद में हेविट [2006] ने आरेखों को आगमन समय के साथ संवर्धित किया जिससे कि तकनीकी रूप से सरल निरूपण मॉडल का निर्माण किया जा सके जिसे समझना आसान है।

यह भी देखें

संदर्भ

  • Carl Hewitt, et al. Actor Induction and Meta-evaluation Conference Record of ACM Symposium on Principles of Programming Languages, January 1974.
  • Irene Greif. Semantics of Communicating Parallel Processes MIT EECS Doctoral Dissertation. August 1975.
  • Edsger Dijkstra. A discipline of programming Prentice Hall. 1976.
  • Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
  • Henry Baker and Carl Hewitt The Incremental Garbage Collection of Processes Proceedings of the Symposium on Artificial Intelligence Programming Languages. SIGPLAN Notices 12, August 1977.
  • Carl Hewitt and Henry Baker Laws for Communicating Parallel Processes IFIP-77, August 1977.
  • Aki Yonezawa Specification and Verification Techniques for Parallel Programs Based on Message Passing Semantics MIT EECS Doctoral Dissertation. December 1977.
  • Peter Bishop Very Large Address Space Modularly Extensible Computer Systems MIT EECS Doctoral Dissertation. June 1977.
  • Carl Hewitt. Viewing Control Structures as Patterns of Passing Messages Journal of Artificial Intelligence. June 1977.
  • Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
  • Carl Hewitt and Russ Atkinson. Specification and Proof Techniques for Serializers IEEE Journal on Software Engineering. January 1979.
  • Carl Hewitt, Beppe Attardi, and Henry Lieberman. Delegation in Message Passing Proceedings of First International Conference on Distributed Systems Huntsville, AL. October 1979.
  • Russ Atkinson. Automatic Verification of Serializers MIT Doctoral Dissertation. June, 1980.
  • Bill Kornfeld and Carl Hewitt. The Scientific Community Metaphor IEEE Transactions on Systems, Man, and Cybernetics. January 1981.
  • Gerry Barber. Reasoning about Change in Knowledgeable Office Systems MIT EECS Doctoral Dissertation. August 1981.
  • Bill Kornfeld. Parallelism in Problem Solving MIT EECS Doctoral Dissertation. August 1981.
  • Will Clinger. Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation. June 1981.
  • Eike Best. Concurrent Behaviour: Sequences, Processes and Axioms Lecture Notes in Computer Science Vol.197 1984.
  • Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems Doctoral Dissertation. 1986.
  • Eike Best and R.Devillers. Sequential and Concurrent Behaviour in Petri Net Theory Theoretical Computer Science Vol.55/1. 1987.
  • Gul Agha, Ian Mason, Scott Smith, and Carolyn Talcott. A Foundation for Actor Computation Journal of Functional Programming January 1993.
  • Satoshi Matsuoka and Akinori Yonezawa. Analysis of inheritance anomaly in object-oriented concurrent programming languages in Research directions in concurrent object-oriented programming. 1993.
  • Jayadev Misra. A Logic for concurrent programming: Safety Journal of Computer Software Engineering. 1995.
  • Luca de Alfaro, Zohar Manna, Henry Sipma and Tomás Uribe. Visual Verification of Reactive Systems TACAS 1997.
  • Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
  • Giuseppe Milicia and Vladimiro Sassone. The Inheritance Anomaly: Ten Years After Proceedings of the 2004 ACM Symposium on Applied Computing (SAC), Nicosia, Cyprus, March 14–17, 2004.
  • Petrus Potgieter. Zeno machines and hypercomputation 2005
  • Carl Hewitt What is Commitment?Physical, Organizational, and Social COINS@AAMAS. 2006.