الدلالات الدلالية لنموذج الممثل

تحتوي البيئات على روابط المعرفات. عندما يتم إرسال رسالة بحث إلى بيئة ما تحتوي على عنوان المعرف x ، فإنها تُرجع أحدث رابط (معجمي) لـ x .

كمثال على كيفية عمل ذلك، انظر إلى تعبير لامدا <L> أدناه، الذي يُنفذ بنية بيانات شجرية عند تزويده بمعاملات لـ leftSubTree و rightSubTree . عندما تُعطى هذه الشجرة رسالة المعامل "getLeft" ، فإنها تُرجع leftSubTree ، وبالمثل، عندما تُعطى رسالة المعامل "getRight"، فإنها تُرجع rightSubTree .

λ(leftSubTree, rightSubTree) λ(رسالة) إذا كانت الرسالة تساوي "getLeft"، فسيتم استدعاء leftSubTree ، وإذا كانت تساوي "getRight"، فسيتم استدعاء rightSubTree.

لنفترض أن تعبيرًا من الشكل "(<L> 1 2)" يُرسل إليه رسالة تقييم (Eval) مع بيئة E. أحد دلالات تعبيرات التطبيق من هذا النوع هو التالي: يتم إرسال رسائل تقييم (Eval) إلى <L> و1 و 2 مع بيئة E. يرد العددان الصحيحان 1 و 2 فورًا على رسالة التقييم (Eval) بنفسيهما.

ومع ذلك، يستجيب <L> لرسالة Eval عن طريق إنشاء كائن إغلاق Actor (عملية) C له عنوان (يسمى body ) لـ <L> وعنوان (يسمى environment ) لـ E. ثم يرسل الكائن Actor "(<L> 1 2)" الرسالة [1 2] إلى C.

عندما يتلقى C الرسالة [1 2] ، فإنه ينشئ بيئة جديدة باسم الممثل F والتي تتصرف على النحو التالي:

1. عندما يتلقى رسالة بحث عن المعرّف leftSubTree ، فإنه يستجيب بالرقم 1
2. عندما يتلقى رسالة بحث عن المعرّف rightSubTree ، فإنه يستجيب بالرقم 2
3. عندما يتلقى رسالة بحث لأي مُعرّف آخر، فإنه يُعيد توجيه رسالة البحث إلى E

ثم يقوم الممثل (العملية) C بإرسال رسالة تقييم مع البيئة F إلى الممثل (العملية) التالي:

 λ(message) إذا كانت (message == "getLeft") ، فاستخدم leftSubTree ، وإذا كانت (message == "getRight") ، فاستخدم rightSubTree

كمثال آخر، لنفترض أن لدينا ممثلاً للتعبير " <التعبير ₁ > + <التعبير ₂ > " والذي يحتوي على عناوين لممثلين (عمليتين) آخرين هما <التعبير ₁ > و <التعبير ₂ > . عندما يستقبل ممثل التعبير المركب (العملية) _رسالة تقييم (Eval) تحتوي على عناوين لممثل البيئة E والعميل C ، فإنه يرسل رسائل تقييم إلى <التعبير ₁ > و <التعبير ₂ > مع البيئة E _، ويرسل إلى C ممثلاً (عملية) جديدًا هو _C0 . _عندما يستقبل C0 القيمتين N1 و N2 ، فإنه يرسل إلى C القيمة N1 + N2 . وبهذه الطريقة، توفر الدلالات الوصفية لحسابات العمليات ونموذج الممثل دلالات وصفية للتعبير " <التعبير ₁ > + <التعبير ₂ > _" من حيث دلالات <التعبير 1 _{> و} < التعبير ₂ > .

إنّ الدلالات التركيبية الدلالية المذكورة أعلاه عامة جدًا، ويمكن استخدامها في البرامج الوظيفية ، والإجرائية ، والمتزامنة ، والمنطقية ، وغيرها (انظر [Hewitt 2008a]). على سبيل المثال، فهي توفر بسهولة دلالات دلالية للبنى التي يصعب صياغتها رسميًا باستخدام مناهج أخرى مثل التأخيرات والمستقبلات .

شرح كلينجر [1981] مجال حسابات الممثل على النحو التالي:

تُشكّل مخططات أحداث الممثل المُعززة [انظر نظرية نموذج الممثل ] مجموعةً مُرتبة جزئيًا < المخططات ، ≤ >، والتي يُمكن من خلالها بناء مجال القوة P [ المخططات ] (انظر قسم الدلالات أدناه). تُمثل المخططات المُعززة سجلات حسابية جزئية تُمثل "لقطات" [بالنسبة لإطار مرجعي مُعين] لعملية حسابية في طريقها إلى الاكتمال. بالنسبة لـ x ، y ∈ المخططات ، فإن x≤y تعني أن x هي مرحلة يُمكن أن تمر بها العملية الحسابية في طريقها إلى y . تُمثل العناصر المُكتملة في المخططات العمليات الحسابية التي انتهت والعمليات الحسابية غير المُنتهية التي أصبحت لانهائية. يُمكن وصف العناصر المُكتملة بشكل تجريدي بأنها العناصر القصوى في المخططات [انظر ويليام وادج 1979]. عمليًا، العناصر المُكتملة هي تلك التي لا تحتوي على أحداث مُعلقة. بشكل بديهي، المخططات ليست كاملة ω لأنه توجد تسلسلات مُتزايدة من العمليات الحسابية الجزئية المحدودة.  

${\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}$

حيث يبقى حدثٌ ما معلقًا إلى الأبد بينما يزداد عدد الأحداث المُنجزة بلا حدود، وهو ما يتعارض مع شرط التأخير المحدود [للوصول]. لا يمكن أن يكون لمثل هذا التسلسل حدٌّ، لأن أي حدٍّ سيمثل عملية حسابية مكتملة غير منتهية لا يزال فيها حدثٌ ما معلقًا.

للتكرار، فإن مخطط مجال حدث الممثل غير مكتمل بسبب شرط تأخير الوصول المحدود، والذي يسمح بأي تأخير محدود بين حدث ما وحدث يقوم بتنشيطه ولكنه يستبعد التأخير اللانهائي.

في أطروحته للدكتوراه، أوضح ويل كلينجر كيف يتم الحصول على مجالات القوة من المجالات غير المكتملة على النحو التالي:

من مقالة حول مجالات القوة : P [D] هي مجموعة المجموعات الجزئية المغلقة تنازليًا من المجال D والتي تكون مغلقة أيضًا تحت الحدود العليا الصغرى الموجودة للمجموعات الموجهة في D. لاحظ أنه على الرغم من أن الترتيب على P [D] يُعطى بواسطة علاقة المجموعة الجزئية، فإن الحدود العليا الصغرى لا تتطابق عمومًا مع الاتحادات.

في مجال مخطط أحداث الفاعل Diagrams ، يُمثل كل عنصر من P [ Diagrams ] قائمةً بالمسارات الأولية المحتملة لعملية حسابية. وبما أن x ≤ y للعنصرين x و y في Diagrams تعني أن x جزء أولي من المسار الأولي y ، فإن اشتراط أن تكون عناصر P [ Diagrams ] مغلقةً تنازليًا له أساس منطقي واضح.

...

عادةً ما يُشترط أن يكون الترتيب الجزئي الذي يُبنى منه مجال القدرة كاملاً من النوع ω . وهناك سببان لذلك. أولهما أن معظم مجالات القدرة هي ببساطة تعميمات لمجالات استُخدمت كمجالات دلالية للبرامج التسلسلية التقليدية، وهذه المجالات كاملة جميعها بسبب الحاجة إلى حساب النقاط الثابتة في الحالة التسلسلية. أما السبب الثاني فهو أن اكتمال ω يسمح بحل معادلات المجال التكرارية التي تتضمن مجال القدرة، مثل:

${\displaystyle R\approx S\rightarrow P[S+(S\times R)]}$

والذي يُحدد نطاق الافتراضات [غوردون بلوتكين 1976]. مع ذلك، يُمكن تعريف نطاقات القوة لأي نطاق كان. علاوة على ذلك، فإن نطاق قوة أي نطاق هو في جوهره نطاق قوة اكتماله ω، لذا يُمكن حل المعادلات التكرارية التي تتضمن نطاق قوة نطاق غير مكتمل، شريطة أن تكون النطاقات التي تُطبق عليها المُنشئات المعتادة (+، ×، →، و*) مكتملة ω. يُصادف أن تعريف دلالات الممثل كما في كلينجر [1981] لا يتطلب حل أي معادلات تكرارية تتضمن نطاق القوة.

باختصار، لا توجد عوائق تقنية أمام بناء نطاقات القوة من نطاقات غير مكتملة. ولكن لماذا قد يرغب المرء في القيام بذلك؟

في علم الدلالة السلوكية ، الذي طورته إيرين غريف ، يُعرَّف البرنامج بأنه تحديد للحسابات التي يمكن للبرنامج تنفيذها. وتُمثَّل هذه الحسابات رسميًا بواسطة مخططات أحداث الفاعلين. وقد حددت غريف مخططات الأحداث باستخدام بديهيات سببية تحكم سلوكيات الفاعلين الأفراد [غريف 1975].

قدم هنري بيكر مترجمًا غير حتمي يقوم بتوليد جداول زمنية فورية يتم ربطها بعد ذلك بمخططات الأحداث. واقترح أنه يمكن تعريف مترجم حتمي مماثل يعمل على مجموعات من الجداول الزمنية الفورية باستخدام دلالات مجال القوة [بيكر 1978].

تُعدّ الدلالات المُقدّمة في [كلينجر 1981] صيغةً من دلالات السلوك. يُشير البرنامج إلى مجموعة من مخططات أحداث الفاعلين. تُعرَّف هذه المجموعة امتدادياً باستخدام دلالات مجال القوة، بدلاً من تعريفها قصدياً باستخدام البديهيات السببية. تُعرَّف سلوكيات الفاعلين الفردية وظيفياً. ومع ذلك، فقد تبيّن أن مجموعة مخططات أحداث الفاعلين الناتجة تتكوّن تحديداً من تلك المخططات التي تُحقّق البديهيات السببية التي تُعبّر عن السلوكيات الوظيفية للفاعلين. وبالتالي، فإن دلالات السلوك عند غريف متوافقة مع دلالات مجال القوة الدلالية.

قدّمت جداول بيكر الآنية مفهوم الأحداث المعلقة ، التي تمثل الرسائل في طريقها إلى وجهاتها. يجب أن يصبح كل حدث معلق حدث وصول فعلي (متحقق) عاجلاً أم آجلاً، وهو شرط يُشار إليه بالتأخير المحدود . يساعد تعزيز مخططات أحداث الممثل بمجموعات من الأحداث المعلقة على التعبير عن خاصية التأخير المحدود، وهي سمة مميزة للتزامن الحقيقي [شوارتز 1979].

في أطروحته التي قدمها عام 1981، أوضح كلينجر كيف تشكل العمليات الحسابية المتسلسلة مجالاً فرعياً من العمليات الحسابية المتزامنة:

بدلاً من البدء بدلالات البرامج المتسلسلة ثم محاولة توسيعها للتزامن، فإن دلالات الممثل تنظر إلى التزامن على أنه أساسي وتحصل على دلالات البرامج المتسلسلة كحالة خاصة.

...

قد يبدو وجود متتابعات متزايدة بدون حدود عليا دنيا غريبًا على من اعتادوا التفكير في دلالات البرامج المتسلسلة. ولعل من المفيد الإشارة إلى أن جميع المتتابعات المتزايدة الناتجة عن البرامج المتسلسلة لها حدود عليا دنيا. في الواقع، تُشكل العمليات الحسابية الجزئية التي يمكن إنتاجها بواسطة الحساب المتسلسل مجالًا فرعيًا كاملًا من نوع ω ضمن مجال مخططات حسابات الممثل . وفيما يلي برهان غير رسمي.

من وجهة نظر الفاعل، تُعدّ العمليات الحسابية المتسلسلة حالة خاصة من العمليات الحسابية المتزامنة، ويمكن تمييزها من خلال مخططات الأحداث الخاصة بها. يحتوي مخطط أحداث العملية الحسابية المتسلسلة على حدث ابتدائي، ولا يُفعّل أي حدث أكثر من حدث واحد. بعبارة أخرى، يكون ترتيب التفعيل في العملية الحسابية المتسلسلة خطيًا؛ ومخطط الأحداث هو في الأساس تسلسل تنفيذ تقليدي. هذا يعني أن العناصر المحدودة للمخططات

${\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}$

جميع الأجزاء الأولية المحدودة لتسلسل تنفيذ متسلسل تحتوي على حدث معلق واحد فقط، باستثناء العنصر الأكبر المكتمل في حالة انتهاء الحساب. إحدى خصائص مجال مخططات الأحداث المعززة < Diagrams , ≤ > هي أنه إذا كان x ≤ y و x ≠ y ، فإن أحد الأحداث المعلقة لـ x يتحقق في y . بما أن كل xᵢ في هذه الحالة _يحتوي على حدث معلق واحد على الأكثر، فإن كل حدث معلق في التسلسل يتحقق. ومن ثم، فإن التسلسل  

${\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}$

يوجد حد أدنى أعلى في المخططات بما يتوافق مع الحدس.

ينطبق البرهان المذكور أعلاه على جميع البرامج التسلسلية، حتى تلك التي تحتوي على نقاط اختيار مثل الأوامر المحمية . وبالتالي، فإن دلالات الممثل تشمل البرامج التسلسلية كحالة خاصة، وتتفق مع الدلالات التقليدية لهذه البرامج.

تُنشئ الدلالات الوصفية للمخططات الزمنية مجالًا حسابيًا كاملًا من نوع ω لحسابات الممثل. في هذا المجال، لكل حدث في حساب الممثل، يوجد وقت تسليم يُمثل وقت تسليم الرسالة، بحيث يُحقق كل وقت تسليم الشروط التالية:

1. وقت التسليم هو عدد نسبي موجب لا يتطابق مع وقت تسليم أي رسالة أخرى.
2. يتجاوز وقت التسليم قيمة ثابتة δ، وهي أكبر من وقت تفعيل العملية. وسيتضح لاحقًا أن قيمة δ لا تُؤثر على العملية. بل يمكن السماح لقيمة δ بالتناقص خطيًا مع مرور الوقت لمراعاة قانون مور .

تُشكّل مخططات الأحداث الموقوتة للممثل مجموعةً مُرتبةً جزئيًا < TimedDiagrams , ≤>. تُمثّل هذه المخططات سجلات حسابية جزئية تُشير إلى "لقطات" (بالنسبة لإطار مرجعي مُحدد) لعملية حسابية في طريقها إلى الاكتمال. بالنسبة لـ d1، d2ε TimedDiagrams ، فإن d1≤d2 تعني أن d1 هي مرحلة يُمكن أن تمر بها العملية الحسابية في طريقها إلى d2. تُمثّل العناصر المُكتملة في TimedDiagrams العمليات الحسابية التي انتهت والعمليات الحسابية غير المُنتهية التي أصبحت لانهائية. يُمكن وصف العناصر المُكتملة بشكل تجريدي بأنها العناصر القصوى في TimedDiagrams . وبشكلٍ ملموس، فإن العناصر المُكتملة هي تلك التي لا تحتوي على أحداث مُعلقة.

نظرية: تُعتبر المخططات الزمنية مجالًا كاملًا من نوع ω لحسابات الممثل، أي

1. إذا كان D⊆ TimedDiagrams موجهًا، فإن الحد الأعلى الأدنى ⊔D موجود؛ علاوة على ذلك، فإن ⊔D يطيع جميع قوانين نظرية نموذج الممثل .
2. تكون العناصر المحدودة في TimedDiagrams قابلة للعد، ويكون العنصر xε TimedDiagrams محدودًا (معزولًا) إذا وفقط إذا كان D⊆ TimedDiagrams موجهًا، وكان x≤VD، يوجد dεD بحيث x≤d. بعبارة أخرى، يكون x محدودًا إذا كان لا بد من المرور عبر x للوصول إلى x أو ما فوقها عبر عملية النهاية.
3. كل عنصر من عناصر TimedDiagrams هو الحد الأعلى الأدنى لتسلسل متزايد قابل للعد من العناصر المحدودة.

• التعريف: المجال <Power[ TimedDiagrams] , ⊆> هو مجموعة التواريخ الأولية الممكنة M لعملية حسابية بحيث
  1. M مغلقة من الأسفل، أي إذا كان dεM، فإن ∀d'εTimedDiagrams d'≤d ⇒ d'εM
  2. تكون المجموعة M مغلقة تحت الحدود العليا الدنيا للمجموعات الموجهة، أي إذا كانت D⊆M موجهة، فإن VDεM
• ملاحظة: على الرغم من أن Power[ TimedDiagrams ] مرتبة حسب ⊆، إلا أن الحدود لا تُعطى بواسطة U. أي،

  (∀i∈ω M _i ≤M _i+1 ) ⇒ ​​U _i∈ω M _i ⊆ ⊔ _i∈ω M _i

  على سبيل المثال، إذا كان ∀id _i ε TimedDiagrams و d _i ≤d _i+1 و M _i = {d _k | k ≤i} فإن

  {{{1}}}

• نظرية: Power [ TimedDiagrams ] هو مجال ω-كامل.

يمكن أن تتقدم عملية حساب الممثل بطرق عديدة. ليكن d مخططًا يحتوي على الحدث المجدول التالي e و X ≡ {e' | e ─≈→ _{رسالة واحدة} e'} (انظر نظرية نموذج الممثل )، يُعرَّف التدفق Flow(d) بأنه مجموعة جميع المخططات الزمنية التي تحتوي على d وامتدادات d بواسطة X بحيث

1. تم تحديد موعد وصول جميع فعاليات X حيث
2. يتم جدولة أحداث X بجميع الترتيبات الممكنة بين الأحداث المستقبلية المجدولة لـ d
3. مع مراعاة القيد المتمثل في أن كل حدث في X يتم جدولته على الأقل δ بعد e وأن كل حدث في X يتم جدولته مرة واحدة على الأقل في كل فترة δ بعد ذلك.

(تذكر أن δ هو الحد الأدنى من الوقت اللازم لتسليم الرسالة.)

Flow(d) ≡ {d} إذا كانت d كاملة.

ليكن S نظام ممثلين، ويكون التقدم _S عبارة عن خريطة

Power[ TimedDiagrams ]→Power[ TimedDiagrams ]

التقدم _S (M) ≡ U _dεM التدفق (d)

النظرية: المتتابعة _S متصلة من الدرجة ω.

أي، إذا كان ∀i M _i ⊆M _i+1 فإن التقدم _S (⊔ _iεω M _i ) = ⊔ _iεω التقدم _S (M _i )

علاوة على ذلك، فإن أصغر نقطة ثابتة للتقدم _S تُعطى بواسطة نظرية تمثيل التزامن على النحو التالي:

⊔ _iεω التقدم _S ⁱ (⊥ _S )

حيث ⊥ _S هو التكوين الأولي لـ S.

يشير الرمز Denote _S لنظام الممثل S إلى مجموعة جميع عمليات الحساب الخاصة بـ S.

عرّف التجريد الزمني للمخطط الزمني بأنه المخطط الذي تمت إزالة التعليقات الزمنية منه.

نظرية التمثيل: يُرمز إلى _{نظام الممثل S بالرمز S، وهو التجريد الزمني لـ}

⊔ _iεω التقدم _S ⁱ (⊥ _S )

إن استخدام مجال TimedDiagrams ، وهو ω-كامل، أمر مهم لأنه يوفر التعبير المباشر عن نظرية التمثيل المذكورة أعلاه لدلالات أنظمة الممثل من خلال إنشاء نقطة ثابتة دنيا بشكل مباشر.

يمكن اشتقاق معيار الاستمرارية للرسوم البيانية للدوال الذي استخدمه سكوت لتطوير الدلالات الدلالية للدوال في البداية كنتيجة لقوانين الممثل للحساب كما هو موضح في القسم التالي.