الدلالات التعيينية

في علوم الكمبيوتر، الدلالات الإشارية (Denotational Semantics) (التي كانت تُعرف في البداية بالدلالات الرياضية أو دلالات سكوت-ستراشي) هي مقاربة لـإضفاء الطابع الرسمي على معاني لغات البرمجة. يتم ذلك عن طريق بناء كائنات رياضية(تُسمى الدلالات) تُوصف معاني التعبيرات من اللغات. تتضمن الأساليب الأخرى التي توفر الدلالات الرسمية للغات البرمجة الدلالات البديهية (Axiomatic Semantics) والدلالات التشغيلية (Operational Semantics).

بشكل عام، تهتم الدلالات الدلالية بإيجاد كائنات رياضية تُسمى المجالات(domains)، والتي تمثل ما تفعله البرامج. على سبيل المثال، قد يتم تمثيل البرامج (أو عبارات البرامج) بواسطة وظائف جزئية (partial functions) أو بواسطة ألعاب(games) بين البيئة والنظام.^[1]

أحد المبادئ المهمة في الدلالات الدلالية هو أن الدلالات يجب أن تكون تركيبية (compositional): أي أن معنى (دلالة) عبارة البرنامج يجب أن يُبنى من معاني (دلالات) العبارات الفرعية المكونة لها.

التطور التاريخي

نشأت الدلالات الدلالية في أعمال كريستوفر ستراتشي (Christopher Strachey) ودانا سكوت (Dana Scott) التي نُشرت في أوائل سبعينيات القرن العشرين. كما تم تطويرها في الأصل بواسطة ستراتشي وسكوت، فقد قدمت الدلالات الدلالية معنى برنامج الكمبيوتر كدالة تقوم بربط المدخلات بالمخرجات.

ولإعطاء معانٍ للبرامج المُعرّفة بشكل متكرر، اقترح سكوت العمل مع الدوال المستمرة (continuous functions) بين المجالات (domains)، وتحديدًا الطلبات الجزئية الكاملة (complete partial orders). استمر العمل في التحقيق في الدلالات الإشارية المناسبة لجوانب لغات البرمجة مثل: التسلسل،والتزامن وعدم التحديد والحالة المحلية.

معاني البرامج التكرارية

تُحدِّد الدلالات الدلالية (Denotational Semantics) معنى أي عبارة برمجية كدالة تأخذ البيئة (environment)—التي تتضمن قيم المتغيرات الحرة—وتُعيد دلالتها. على سبيل المثال، التعبير n * m ينتج دلالة محددة عند تزويده ببيئة تربط قيمًا للمتغيرين n وm. فإذا كانت قيمة n في البيئة 3 وm 5، فإن الدلالة الناتجة ستكون 15.

يمكن تمثيل الدالة كمجموعة من الأزواج المرتبة التي تتكون من الحجج وقيم النتائج المقابلة. على سبيل المثال، تشير المجموعة {(0,1),(4,3)} إلى دالة تكون نتيجتها 1 عندما تكون الحجة 0، ونتيجتها 3 عندما تكون الحجة 4، وتكون غير محددة بخلاف ذلك.

على سبيل المثال، لننظر إلى الدالة العامِلية (factorial function)، والتي يمكن تعريفها بشكل متكرر (recursively) على النحو التالي:

int factorial(int n) { if (n == 0) then return 1; else return n * factorial(n-1); }

لإضفاء معنى على هذا التعريف المتكرر، تُبنى الدلالة كـحد للتقريبات. يقيّد كل تقريب عدد استدعاءات العامل. نبدأ في البداية بدون أي استدعاءات، وبالتالي لا يتم تعريف أي شيء. في التقريب التالي، يمكننا إضافة الزوج المرتب (0,1)، حيث لا يتطلب ذلك استدعاء العامل مرة أخرى. وبالمثل، يمكننا إضافة (1,1)، (2,2)، وهكذا، بإضافة زوج واحد لكل تقريب متتالٍ. يعود السبب في ذلك إلى أن حساب العامل n يتطلب n+1 استدعاءات. في النهاية، نحصل على دالة كلية من N إلى N، معرفة في كل مكان ضمن نطاقها.

نُنمذج كل تقريب رياضيًا كدالة جزئية $\mathbb {N} \rightharpoonup \mathbb {N}$ . بعد ذلك، يقوم نموذجنا بتطبيق دالة $F:(\mathbb {N} \rightharpoonup \mathbb {N} )\to (\mathbb {N} \rightharpoonup \mathbb {N} )$ بشكل متكرر، تبدأ من الدالة الفارغة (الوظيفة الفارغة). تعمل هذه الدالة على "إنشاء دالة عاملية جزئية أكثر تحديدًا" في كل تكرار.

↑ 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

int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n) {

if (n == 0) then return 1;

else if (fprev = lookup(factorial_less_defined, n-1)) then

return n * fprev;

else

return NOT_DEFINED;

}

Map<int,int> F(Map<int,int> factorial_less_defined)

{

Map<int,int> new_factorial = Map.empty();

for (int n in all<int>()) {

if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED)

new_factorial.put(n, f);

}

return new_factorial;

}

بعد ذلك، يمكننا استخدام الرمز Fn للإشارة إلى الدالة F المطبقة n مرة .

F ⁰ ({}) هي الدالة الجزئية غير المعرفة تمامًا، والممثلة بالمجموعة {}؛
F ¹ ({}) هي الدالة الجزئية الممثلة كمجموعة {(0,1)}: يتم تعريفها عند 0، لتكون 1، وغير معرفة في أي مكان آخر؛
F ⁵ ({}) هي الدالة الجزئية الممثلة كمجموعة {(0,1)، (1,1)، (2,2)، (3,6)، (4,24)}: يتم تعريفها للحجج 0،1،2،3،4.

تبني هذه العملية التكرارية سلسلة من الدوال الجزئية من N إلى N. تُشكّل هذه الدوال الجزئية ترتيبًا جزئيًا مكتملًا للسلسلة باستخدام العلاقة ⊆ كترتيب. علاوة على ذلك، تُعدّ هذه العملية التكرارية لتقريبات أفضل لدالة العامل بمثابة تخطيط توسعي (يُسمى أيضًا تخطيطًا تقدميًا)، وذلك لأن كل $F^{i}\leq F^{i+1}$ باستخدام ⊆ كترتيب. وبالتالي، وبموجب نظرية النقطة الثابتة (وبالتحديد نظرية بورباكي-ويت)، توجد نقطة ثابتة لهذه العملية التكرارية.

في هذه الحالة، تُعتبر النقطة الثابتة هي الحد الأعلى الأصغر لهذه السلسلة، وهي تمثل الدالة العاملية (factorial) الكاملة، والتي يمكن التعبير عنها كالِاتحاد (union) لجميع التقريبات.

\bigcup _{i\in \mathbb {N} }F^{i}(\{\}).

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

الدلالات الدلالية للبرامج غير الحتمية

لقد تم تطوير مفهوم مجالات القوة (Power Domains) لتقديم دلالات دلالية للبرامج المتسلسلة غير الحتمية (nondeterministic). عند استخدام الرمز P للإشارة إلى مُنشئ مجال القوة، فإن المجال P(D) يُمثل مجال الحسابات غير الحتمية من النوع الذي يُرمز إليه بالرمز D.

تُظهر نماذج نظرية المجال (Domain Theory) التي تتناول حالات وعدم التحديد (nondeterminism) تحديات مرتبطة بمفهومي العدالة (fairness) وعدم التحديد (indeterminacy).^[1]

الدلالات الدلالية للتزامن

لقد زعم العديد من الباحثين أن النماذج النظرية للمجال المذكورة أعلاه غير كافية للحالة الأكثر عمومية للحوسبة المتزامنة (concurrent computing). لهذا السبب، تم تقديم نماذج جديدة ومتنوعة.^[2]

في أوائل الثمانينيات، بدأ استخدام أسلوب الدلالات الإشارية (Denotational Semantics) لتحديد دلالات اللغات المتزامنة. تشمل الأمثلة على هذا التوجه:^[3]

عمل ويل كلينجر مع نموذج الممثل.
عمل غلين وينسكيل مع هياكل الأحداث وشبكات بتري (Petri nets).
العمل الذي قام به فرانسيس، هوار، ليمان، ودي روفر (1979) حول دلالات التتبع لـ CSP (Communicating Sequential Processes).^[4]

تظل جميع خطوط البحث هذه قيد التحقيق والتطوير (على سبيل المثال، انظر النماذج الدلالية المختلفة لـ CSP).

مؤخرًا، اقترح وينسكيل وآخرون فئة المتحولات اللحظية (Event Structures) كنظرية مجال للتزامن.^[5]^[6]

الدلالات الدلالية للحالة

يمكن نمذجة ميزات الحالة (مثل الكومة - heap) والميزات الإلزامية البسيطة مباشرةً ضمن الدلالات الدلالية الموضحة أعلاه. الفكرة الأساسية هي اعتبار الأمر كدالة جزئية في بعض مجالات الحالات (state domains). على سبيل المثال، معنى الأمر x := 3 هو الدالة التي تُحوّل حالة معينة إلى حالة جديدة يتم فيها تعيين القيمة 3 للمتغير x. يُشار إلى عامل التسلسل ؛ بتركيب الدوال. بعد ذلك، تُستخدم بناءات النقطة الثابتة لإعطاء دلالات للبناءات المتكررة، مثل while (حلقة التكرار).

تزداد الأمور تعقيدًا عند نمذجة البرامج التي تتضمن المتغيرات المحلية (local variables). أحد الأساليب المتبعة لمعالجة ذلك هو عدم الاعتماد على المجالات بشكل مباشر، بل تفسير الأنواع كـمحولات (functors) من فئة معينة من العوالم إلى فئة من المجالات. بعد ذلك، ^[7] تُشار البرامج من خلال الدوال المستمرة الطبيعية بين هذه الدوال.^[8]

دلالات أنواع البيانات

تسمح العديد من لغات البرمجة للمستخدمين بتعريف أنواع البيانات المتكررة (Recursive Data Types). على سبيل المثال، يمكن تحديد نوع قوائم الأرقام عن طريق:

datatype list = Cons of nat * list | Empty يتناول هذا القسم فقط هياكل البيانات الوظيفية التي لا يمكن تغييرها. تجدر الإشارة إلى أن لغات البرمجة الإلزامية التقليدية تسمح عادةً بتعديل عناصر هذه القائمة المتكررة.

كمثال آخر: نوع الدلالات لحساب لامدا (lambda calculus) غير المكتوب هو:

datatype D = D of (D → D) تتعلق مشكلة حل معادلات المجال (Domain Equations) بإيجاد المجالات التي تُنمذج هذه الأنواع من أنواع البيانات. أحد الأساليب، بشكل تقريبي، هو اعتبار مجموعة كل المجالات مجالًا بحد ذاته، ثم حل التعريف المتكرر هناك.

أنواع البيانات المتعددة الأشكال (Polymorphic Data Types) هي أنواع بيانات تُعرّف باستخدام معامل (parameter). على سبيل المثال، يُعرّف نوع list α بواسطة:

datatype α list = Cons of α * α list | Empty وبالتالي، فإن قوائم الأعداد الطبيعية تكون من نوع nat list، في حين أن قوائم السلاسل تكون من نوع string list.

قام بعض الباحثين بتطوير نماذج نظرية المجال (Domain Theory) للتعدد الأشكال (polymorphism). كما قام باحثون آخرون بوضع نماذج للتعدد الأشكال البارامترية (parametric polymorphism) ضمن نظريات المجموعات البنائية.

شمل مجال بحثي حديث الدلالات الدلالية (Denotational Semantics) للغات البرمجة القائمة على الكائنات (Objects) والفئات (Classes).^[9]

الدلالات الدلالية للبرامج ذات التعقيد المحدود

بعد تطوير لغات البرمجة القائمة على المنطق الخطي (Linear Logic)، تم إعطاء الدلالات الدلالية لهذه اللغات لاستخدامها الخطي (انظر على سبيل المثال شبكات الإثبات - Proof Nets ومساحات التماسك - Coherence Spaces) وكذلك لتعقيد الوقت متعدد الحدود.^[10]

الدلالات الدلالية للتسلسل

ظلت مشكلة التجريد الكامل للغة البرمجة التسلسلية PCF، لفترة طويلة، سؤالًا مفتوحًا رئيسيًا في مجال الدلالات الدلالية. تكمن الصعوبة في لغة PCF في أنها لغة تسلسلية للغاية؛ فعلى سبيل المثال، لا توجد طريقة لتحديد الدالة parallel-or فيها. ولهذا السبب، فإن النهج الذي يستخدم المجالات، كما قُدم أعلاه، يؤدي إلى دلالات دلالية ليست مجردة تمامًا.

تم حل هذا السؤال المفتوح إلى حد كبير في تسعينيات القرن العشرين مع تطوير دلالات الألعاب(Game Semantics) وأيضًا باستخدام التقنيات التي تتضمن العلاقات المنطقية (Logical Relations). لمزيد من التفاصيل، يمكنك مراجعة الصفحة الخاصة بـ PCF.^[11]

الدلالات الدلالية كترجمة من مصدر إلى مصدر

من المفيد غالبًا ترجمة لغة برمجة إلى أخرى. على سبيل المثال، يمكن تحويل لغة برمجة متزامنة إلى حساب العمليات (process calculus)، أو لغة برمجة عالية المستوى إلى رمز ثنائي (binary code). في الواقع، يمكن النظر إلى الدلالات الدلالية التقليدية كطريقة لتفسير لغات البرمجة ضمن "اللغة الداخلية" لفئة المجالات.

في هذا السياق، تساهم المفاهيم المستمدة من الدلالات الدلالية، مثل التجريد الكامل (Full Abstraction)، في معالجة المخاوف الأمنية.^[12]

التجريد

غالبًا ما يُعتبر من المهم ربط الدلالات الدلالية (Denotational Semantics) بـبالدلالات التشغيلية (Operational Semantics). يكتسب هذا الارتباط أهمية خاصة عندما تكون الدلالات الدلالية رياضية ومجردة إلى حد ما، بينما تكون الدلالات التشغيلية أكثر واقعية أو أقرب إلى الحدس الحسابي.

غالبًا ما تكون الخصائص التالية للدلالات الدلالية موضع اهتمام:

استقلال بناء الجملة : لا ينبغي أن تتضمن دلالات البرامج بناء جملة اللغة المصدر.
الكفاية (أو السلامة) : جميع البرامج المتميزة التي يمكن ملاحظتها لها دلالات مميزة؛
التجريد الكامل : جميع البرامج المكافئة من الناحية الرصدية لها دلالات متساوية.

بالنسبة للدلالات في الأسلوب التقليدي، يمكن فهم الكفاية (adequacy) والتجريد الكامل (full abstraction) تقريبًا على أنهما الشرط الذي ينص على أن "التكافؤ التشغيلي يتطابق مع المساواة الدلالية".

أما بالنسبة للدلالات الدلالية في النماذج الأكثر قصدية (intentional models)، مثل ننموذج الممثل (Actor model) وحساب العملية (process calculus)، فهناك مفاهيم مختلفة للتكافؤ داخل كل نموذج، وبالتالي فإن مفهومي الكفاية والتجريد الكامل هما موضع نقاش، ويصعب تحديدهما.كما يمكن أن يصبح البناء الرياضي للدلالات التشغيلية والدلالات الإشارية متقاربين للغاية.

بالإضافة إلى العلاقة بين الدلالات التشغيلية والدلالية، قد نرغب في أن تتسم هذه الدلالات ببعض الخصائص المرغوبة، مثل:

البنائية : تهتم البنائية بمعرفة ما إذا كان من الممكن إثبات وجود عناصر المجال من خلال الأساليب البناءة.
استقلال الدلالات الإشارية والتشغيلية : ينبغي صياغة الدلالات الإشارية باستخدام هياكل رياضية مستقلة عن الدلالات التشغيلية للغة البرمجة؛ ومع ذلك، يمكن أن تكون المفاهيم الأساسية مرتبطة ارتباطًا وثيقًا. انظر القسم الخاص بالتكوين أدناه.
الاكتمال الكامل أو القدرة على التعريف : يجب أن يكون كل شكل من أشكال النموذج الدلالي بمثابة دلالة على برنامج.^[13]

التركيبية

أحد الجوانب المهمة للدلالات الدلالية للغات البرمجة هو التركيب (Compositionality). يعني هذا أن دلالة البرنامج تُبنى من دلالات أجزائه. على سبيل المثال، عند النظر إلى التعبير "7 + 4"، فإن التركيب يتجلى في تحديد معنى هذا التعبير بناءً على معاني الأجزاء المكونة له: "7"، "4"، وعامل التشغيل "+".

إن الدلالات الإشارية الأساسية في نظرية المجال هي تركيبية لأنها تُعطى على النحو التالي:

نبدأ بالنظر إلى أجزاء البرنامج (program fragments)، أي البرامج التي تحتوي على متغيرات حرة. يُعيّن سياق الكتابة نوعًا لكل متغير حر. على سبيل المثال، في التعبير (x + y)، يمكن اعتباره ضمن سياق كتابة حيث x وy من النوع nat (عدد طبيعي).

سنقدم الآن دلالات دلالية لأجزاء البرنامج، باستخدام المخطط التالي:

نبدأ بوصف معنى أنواع لغتنا: يجب أن يكون معنى كل نوع مجالًا. نكتب 〚τ〛 للمجال الذي يشير إلى النوع τ. على سبيل المثال، يجب أن يكون معنى النوع nat مجال الأعداد الطبيعية: 〚 nat 〛= $\mathbb {N}$ _⊥ .
ومن معنى الأنواع نشتق معنى لسياقات الكتابة. لقد وضعنا 〚 x ₁ :τ ₁ ،... , x _n :τ _n 〛 = 〚 τ ₁ 〛× ... ×〚τ _n〛 . على سبيل المثال، 〚x : nat ، y : nat 〛= $\mathbb {N}$ _⊥ × $\mathbb {N}$ _⊥ . كحالة خاصة، فإن معنى سياق الكتابة الفارغ، بدون متغيرات، هو المجال الذي يحتوي على عنصر واحد، يُشار إليه بالرقم 1.
أخيرًا، يجب علينا إعطاء معنى لكل جزء من البرنامج في سياق الكتابة. افترض أن P هو جزء برنامج من النوع σ، في سياق الكتابة Γ، والذي يُكتب عادةً Γ⊢ P :σ. ثم يجب أن يكون معنى هذا البرنامج في سياق الكتابة دالة مستمرة 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛. على سبيل المثال، 〚⊢7: nat 〛:1→ $\mathbb {N}$ _⊥ هي الدالة "7" باستمرار، بينما 〚 x : nat ، y : nat ⊢ x + y : nat 〛: $\mathbb {N}$ _⊥ × $\mathbb {N}$ _⊥ → $\mathbb {N}$ _⊥ هي الدالة التي تقوم بجمع عددين.

الآن، يتم تحديد معنى التعبير المركب (7+4) من خلال تكوين الدوال الثلاث:

〚⊢7:nat〛:1→ $\mathbb {N}$ _⊥, 〚⊢4:nat〛:1→ $\mathbb {N}$ _⊥, and 〚x:nat,y:nat⊢x+y:nat〛: $\mathbb {N}$ _⊥× $\mathbb {N}$ _⊥→ $\mathbb {N}$ _⊥

في الواقع، هذا هو مخطط عام للدلالات التركيبية (Compositional Semantics). لا يوجد شيء محدد حول المجالات والوظائف المستمرة هنا؛ يمكنك العمل مع فئة مختلفة بدلاً من ذلك.

على سبيل المثال:

في دلالات الألعاب (Game Semantics)، تشتمل فئة الألعاب على الألعاب كـ"أشياء" والاستراتيجيات كـ"أشكال"؛ يمكننا تفسير الأنواع على أنها ألعاب، والبرامج على أنها استراتيجيات.
بالنسبة للغة بسيطة بدون تكرار عام، يمكننا أن نكتفي بـفئة المجموعات والوظائف (Category of Sets and Functions).
بالنسبة للغة ذات آثار جانبية (side effects)، يمكننا العمل في فئة Kleisli لموناد (Kleisli category for a monad).
بالنسبة للغة ذات حالة (state)، يمكننا العمل في فئة الدالة (functor category).
وقد دافع ميلنر(Milner) عن نمذجة الموقع والتفاعل من خلال العمل في فئة ذات واجهات (interfaces) كـ"أشياء" ومخططات ثنائية (diagrams) كـ"أشكال".^[14]

الدلالات مقابل التنفيذ

وفقًا لدانا سكوت (1980):

ليس من الضروري أن تحدد الدلالات التنفيذ، ولكن يجب أن توفر معايير لإظهار أن التنفيذ صحيح.

وفقًا لكلينجر (1981):^[15] ^:79

ومع ذلك، عادةً ما يتم تفسير الدلالات الرسمية للغة البرمجة التسلسلية التقليدية في حد ذاتها لتوفير تنفيذ (غير فعال) للغة. ومع ذلك، لا يلزم الدلالات الرسمية دائمًا توفير مثل هذا التنفيذ، والاعتقاد بأن الدلالات يجب أن توفر تنفيذًا يؤدي إلى ارتباك حول الدلالات الرسمية للغات المتزامنة. يصبح هذا الارتباك واضحًا بشكل مؤلم عندما يقال إن وجود عدم التحديد غير المحدود في دلالات لغة البرمجة يعني ضمناً أن لغة البرمجة لا يمكن تنفيذها.

الارتباطات بمجالات أخرى من علوم الكمبيوتر

لقد فسر بعض الباحثين في الدلالات الدلالية (denotational semantics) الأنواع باعتبارها مجالات (domains) بمعنى نظرية المجال (domain theory)، والتي يمكن اعتبارها فرعًا من نظرية النموذج (model theory)، مما يؤدي إلى ارتباطها بـنظرية النوع (type theory) ونظرية الفئة (category theory). في مجال علوم الكمبيوتر، هناك ارتباطات مع التفسير المجرد(abstract interpretation)، والتحقق من البرامج (program verification)، ووالتحقق من النموذج (model checking).

مراجع

قراءة إضافية

مراجع أخرى

روابط خارجية

الدلالات الإشارية . نظرة عامة على كتاب لويد أليسون

↑ 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.
↑ Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983. نسخة محفوظة 2024-11-18 على موقع واي باك مشين.
↑ 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. نسخة محفوظة 2024-11-17 على موقع واي باك مشين.
↑ A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.
↑ 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 (غير نشط 20 نوفمبر 2024). S2CID:16356708.{{استشهاد بدورية محكمة}}: صيانة الاستشهاد: وصلة دوي غير نشطة منذ 2024 (link)
↑ 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.
↑ Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama. Syntactic control of interference revisited. Electron. Notes Theor. Comput. Sci. 1. 1995.
↑ Frank J. Oles. A Category-Theoretic Approach to the Semantics of Programming. PhD thesis, جامعة سيراكيوز, New York, USA. 1982.
↑ 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.
↑ 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.
↑ O'Hearn، P.W.؛ Riecke، J.G. (يوليو 1995). "Kripke Logical Relations and PCF". Information and Computation. ج. 120 ع. 1: 107–116. DOI:10.1006/inco.1995.1103. S2CID:6886529. مؤرشف من الأصل في 2024-05-27.
↑ Kennedy، Andrew (2006). "Securing the .NET programmingmodel". Theor. Comput. Sci. ج. 364 ع. 3: 311–7. DOI:10.1016/j.tcs.2006.08.014.
↑ 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.
↑ Milner، Robin (2009). The Space and Motion of Communicating Agents. Cambridge University Press. ISBN:978-0-521-73833-0. 2009 draft نسخة محفوظة 2012-04-02 على موقع واي باك مشين..
↑ Clinger، William D. (مايو 1981). Foundations of Actor Semantics (PhD thesis). Massachusetts Institute of Technology. hdl:1721.1/6935. AITR-633.

[1] 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

[2] 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.

[3] Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983. نسخة محفوظة 2024-11-18 على موقع واي باك مشين.

[4] 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. نسخة محفوظة 2024-11-17 على موقع واي باك مشين.

[Roscoe2-5] A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.

[6] 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 (غير نشط 20 نوفمبر 2024). S2CID:16356708.{{استشهاد بدورية محكمة}}: صيانة الاستشهاد: وصلة دوي غير نشطة منذ 2024 (link)

[7] 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.

[8] Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama. Syntactic control of interference revisited. Electron. Notes Theor. Comput. Sci. 1. 1995.

[9] Frank J. Oles. A Category-Theoretic Approach to the Semantics of Programming. PhD thesis, جامعة سيراكيوز, New York, USA. 1982.

[10] 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.

[11] 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.

[12] O'Hearn، P.W.؛ Riecke، J.G. (يوليو 1995). "Kripke Logical Relations and PCF". Information and Computation. ج. 120 ع. 1: 107–116. DOI:10.1006/inco.1995.1103. S2CID:6886529. مؤرشف من الأصل في 2024-05-27.

[13] Kennedy، Andrew (2006). "Securing the .NET programmingmodel". Theor. Comput. Sci. ج. 364 ع. 3: 311–7. DOI:10.1016/j.tcs.2006.08.014.

[14] 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.

[15] Milner، Robin (2009). The Space and Motion of Communicating Agents. Cambridge University Press. ISBN:978-0-521-73833-0. 2009 draft نسخة محفوظة 2012-04-02 على موقع واي باك مشين..

[clinger1981-16] Clinger، William D. (مايو 1981). Foundations of Actor Semantics (PhD thesis). Massachusetts Institute of Technology. hdl:1721.1/6935. AITR-633.

[1]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]