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

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

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

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

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

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

यह लेख हेविट [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. एक नए अभिनेता का अभिवादन करें₁जिसे संदेश भेजा जाता है SayHelloTo ग्रीटर के पते के साथ₁:#संदेश के पहले अक्षर भेजें Again ग्रीटर के पते के साथ₁: इसके बाद आद्याक्षर का व्यवहार एक प्राप्त होने पर इस प्रकार है Again पता अभिनंदन के साथ संदेश_i(जिसे हम घटना कहेंगे Againi):
2. एक नए अभिनेता का अभिवादन करें_i+1जिसे संदेश भेजा जाता है SayHelloTo अभिनंदनकर्ता के पते के साथ_i:#संदेश के पहले अक्षर भेजें Again ग्रीटर के पते के साथ_i+1:जाहिर है प्रारंभिक भेजने की गणना ही Again संदेश कभी समाप्त नहीं होते।

प्रत्येक अभिनेता का व्यवहार अभिनंदनकर्ता_iइस प्रकार है:

* जब यह एक संदेश प्राप्त करता है SayHelloTo अभिनंदनकर्ता के पते के साथ_i-1(जिसे हम घटना कहेंगे SayHelloToi), यह एक भेजता है Hello ग्रीटर को संदेश_i-1: * जब यह एक प्राप्त करता है Hello संदेश (जिसे हम ईवेंट कहेंगे Helloi), यह कुछ नहीं करता है।

अब ऐसा हो सकता है Helloi -Greeteri→ SayHelloToi हर बार और इसलिए Helloi→SayHelloToi.

भी Againi -≈→ Againi+1 हर बार और इसलिए Againi → Againi+1.

इसके अलावा संयुक्त आदेश के लिए सख्त आकस्मिकता के कानून से पहले बताए गए सभी कानून संतुष्ट हैं।

हालांकि, संयुक्त क्रम में घटनाओं की एक अनंत संख्या हो सकती है Again1 और SayHelloTo1 निम्नलिखित नुसार:

Again1→...→Againi→...$\infty$...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

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

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

संयुक्त क्रम में घटनाओं के बीच परिमित जंजीरों का नियम निम्नलिखित कानून से निकटता से संबंधित है:

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

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

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

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

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

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

क्लिंजर [1981] ने एक्टर मॉडल#क्लिंजर.27एस मॉडल के एक डेनोटेशनल शब्दार्थ के निर्माण के लिए ऊपर वर्णित अभिनेता इवेंट मॉडल का उपयोग किया। इसके बाद हेविट [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.