الدلالات التشغيلية

الدلالات
لغوي منطقي
الحقول الفرعية حسابي المعجمية ( علم المفردات )​ إحصائية هيكلي المواضيع تحليل التركيب السياق (استخدام اللغة) نظرية النموذج الأولي ديناميكيات القوة الميزة الدلالية الفجوة الدلالية نظرية الأوصاف تحليل كامن حسابي التعلم الآلي التطبيقات نظام الملفات الدلالي سطح مكتب دلالي المطابقة الدلالية التحليل الدلالي التشابه الدلالي استعلام دلالي الويب الدلالي ويكي الدلالة
دلالات لغات البرمجة
أنواع فعل جبري بديهي تصنيفي التزامن معلم ب لعبة تشغيلية المسند التحويلي نظرية التفسير المجرد الرسم البياني الدلالي المجرد
لغة علم اللغة
ف ت هـ

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

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

ربما كان أول تجسيد رسمي للدلالات التشغيلية هو استخدام حساب لامدا لتحديد دلالات لغة ليسب . ^{[1] كما أن} الآلات المجردة في تقليد آلة SECD وثيقة الصلة أيضًا.

تم استخدام مفهوم الدلالات التشغيلية لأول مرة في تحديد دلالات AlGOL 68. العبارة التالية هي اقتباس من تقرير ALGOL 68 المنقح:

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

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

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

قدم جوردون بلوتكين الدلالات البنيوية التشغيلية، وماتياس فيليزن وروبرت هيب الدلالات الاختزالية، ^[2] وجيلز كان الدلالات الطبيعية.

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

على سبيل المثال البسيط، نأخذ في الاعتبار جزءًا من دلالات لغة برمجة بسيطة؛ وتوجد أمثلة توضيحية مناسبة في Plotkin81 وHennessy90، وكتب مدرسية أخرى. لنفترض أن range يغطي برامج اللغة، ولنفترض أن range يغطي الحالات (على سبيل المثال، الوظائف من مواقع الذاكرة إلى القيم). إذا كان لدينا تعبيرات (محددة بـ )، وvalues ​​( ) وlocations ( )، فإن أمر تحديث الذاكرة سيكون له دلالات: ${\displaystyle C_{1},C_{2}}$${\displaystyle s}$${\displaystyle E}$${\displaystyle V}$${\displaystyle L}$

${\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}$

بشكل غير رسمي، تنص القاعدة على أنه " إذا تم تقليص التعبير في الحالة إلى قيمة ، فسيقوم البرنامج بتحديث الحالة بالتعيين ". ${\displaystyle E}$${\displaystyle s}$${\displaystyle V}$${\displaystyle L:=E}$${\displaystyle s}$${\displaystyle L=V}$

يمكن إعطاء دلالات التسلسل من خلال القواعد الثلاث التالية:

${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

بشكل غير رسمي، تنص القاعدة الأولى على أنه إذا انتهى البرنامج في الحالة في الحالة ، فإن البرنامج في الحالة سيُختزل إلى البرنامج في الحالة . (يمكنك التفكير في هذا على أنه إضفاء الطابع الرسمي على "يمكنك تشغيل ، ثم تشغيل باستخدام مخزن الذاكرة الناتج.) تنص القاعدة الثانية على أنه إذا كان البرنامج في الحالة يمكن اختزاله إلى البرنامج الذي يحتوي على الحالة ، فإن البرنامج في الحالة سيُختزل إلى البرنامج في الحالة . (يمكنك التفكير في هذا على أنه إضفاء الطابع الرسمي على مبدأ المترجم الأمثل: "يُسمح لك بالتحويل كما لو كان مستقلاً، حتى لو كان مجرد الجزء الأول من البرنامج.") الدلالات هيكلية، لأن معنى البرنامج المتسلسل ، يتم تعريفه من خلال معنى ومعنى . ${\displaystyle C_{1}}$${\displaystyle s}$${\displaystyle s'}$${\displaystyle C_{1};C_{2}}$${\displaystyle s}$${\displaystyle C_{2}}$${\displaystyle s'}$${\displaystyle C_{1}}$${\displaystyle C_{2}}$${\displaystyle C_{1}}$${\displaystyle s}$${\displaystyle C_{1}'}$${\displaystyle s'}$${\displaystyle C_{1};C_{2}}$${\displaystyle s}$${\displaystyle C_{1}';C_{2}}$${\displaystyle s'}$${\displaystyle C_{1}}$${\displaystyle C_{1};C_{2}}$${\displaystyle C_{1}}$${\displaystyle C_{2}}$

إذا كان لدينا أيضًا تعبيرات منطقية على الحالة، والتي يتراوح نطاقها بواسطة ، فيمكننا تحديد دلالات أمر while : ${\displaystyle B}$${\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}}$

يسمح هذا التعريف بإجراء تحليل رسمي لسلوك البرامج، مما يسمح بدراسة العلاقات بين البرامج. تشمل العلاقات المهمة ترتيبات المحاكاة المسبقة والمحاكاة الثنائية . وهي مفيدة بشكل خاص في سياق نظرية التزامن .

بفضل مظهرها البديهي وبنيتها سهلة المتابعة، اكتسبت SOS شعبية كبيرة وأصبحت معيارًا فعليًا في تحديد الدلالات التشغيلية. وكدليل على النجاح، اجتذب التقرير الأصلي (ما يسمى بتقرير آرهوس) حول SOS (Plotkin81) أكثر من 1000 استشهاد وفقًا لـ CiteSeer [1]، مما يجعله أحد أكثر التقارير الفنية استشهادًا في علوم الكمبيوتر .

الدلالات الاختزالية هي عرض بديل للدلالات التشغيلية. تم تطبيق أفكارها الرئيسية لأول مرة على المتغيرات الوظيفية البحتة للاستدعاء بالاسم والاستدعاء بالقيمة لحساب لامدا بواسطة جوردون بلوتكين في عام 1975 ^[3] وتم تعميمها على اللغات الوظيفية ذات الترتيب الأعلى مع ميزات الأمر بواسطة ماثياس فيليسين في أطروحته عام 1987. ^[4] تم تطوير الطريقة بشكل أكبر بواسطة ماثياس فيليسين وروبرت هيب في عام 1992 في نظرية معادلة كاملة للتحكم والحالة . [ 2 ] ^تم صياغة عبارة "دلالات الاختزال" نفسها لأول مرة بواسطة فيليسين ودانييل ب. فريدمان في ورقة بحثية في PARLE عام 1987. ^[5]

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

${\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e}$

للحصول على عبارة تعيين في مثل هذا الموضع، يتم "تجميعها" من خلال تطبيقات الوظائف والجانب الأيمن من عبارات التعيين حتى تصل إلى النقطة المناسبة. نظرًا لأن التعبيرات المتداخلة قد تعلن عن متغيرات مميزة، فإن حساب التفاضل والتكامل يتطلب أيضًا قاعدة إخراج للتعبيرات. تحدد معظم الاستخدامات المنشورة لدلالات الاختزال مثل هذه "قواعد الفقاعة" مع ملاءمة سياقات التقييم. على سبيل المثال، يمكن إعطاء قواعد سياقات التقييم في لغة استدعاء بسيطة بالقيمة على النحو التالي${\displaystyle \mathbf {let} }$${\displaystyle \mathbf {let} }$

${\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e}$

حيث تشير إلى تعبيرات عشوائية وتشير إلى قيم مخفضة بالكامل. يتضمن كل سياق تقييمي ثقبًا واحدًا فقط يتم فيه إدخال مصطلح بطريقة التقاط. يشير شكل السياق من خلال هذه الثقب إلى المكان الذي قد يحدث فيه الاختزال. لوصف "الفقاعات" بمساعدة سياقات التقييم، يكفي بديهية واحدة: ${\displaystyle e}$${\displaystyle v}$${\displaystyle [\,]}$

${\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}}$

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

وعلى غرار بلوتكين، فإن إظهار فائدة حساب التفاضل والتكامل المشتق من مجموعة من قواعد الاختزال يتطلب (1) مبرهنة تشيرش-روسر للعلاقة ذات الخطوة الواحدة، والتي تحث على دالة تقييم، و(2) مبرهنة كاري-فاي للتوحيد القياسي للإغلاق المتعدي الانعكاسي للعلاقة ذات الخطوة الواحدة، والذي يحل محل البحث غير الحتمي في دالة التقييم ببحث حتمي في أقصى اليسار/الخارج. وقد أظهر فيليزن أن الامتدادات الإلزامية لهذا الحساب تلبي هذه النظريات. وتتمثل عواقب هذه النظريات في أن النظرية المعادلة - الإغلاق المتعدي الانعكاسي المتماثل - هي مبدأ منطقي سليم لهذه اللغات. ومع ذلك، في الممارسة العملية، تستغني معظم تطبيقات دلالات الاختزال عن الحساب وتستخدم الاختزال القياسي فقط (والمقيِّم الذي يمكن اشتقاقه منه).

تعد دلالات الاختزال مفيدة بشكل خاص نظرًا لسهولة نمذجة سياقات التقييم لحالة أو بنيات التحكم غير العادية (على سبيل المثال، الاستمرارية من الدرجة الأولى ). بالإضافة إلى ذلك، تم استخدام دلالات الاختزال لنمذجة اللغات الموجهة للكائنات ، ^[6] وأنظمة العقود ، والاستثناءات، والمستقبلات، والاستدعاء حسب الحاجة، والعديد من ميزات اللغة الأخرى. يقدم ماثياس فيليزن وروبرت بروس فيندلر وماثيو فلات معالجة شاملة وحديثة لدلالات الاختزال التي تناقش العديد من هذه التطبيقات بالتفصيل في هندسة الدلالات مع PLT Redex . ^[7]

تُعرف الدلالات التشغيلية البنيوية ذات الخطوة الكبيرة أيضًا باسم الدلالات الطبيعية والدلالات العلائقية ودلالات التقييم . ^[8] تم تقديم الدلالات التشغيلية ذات الخطوة الكبيرة تحت اسم الدلالات الطبيعية بواسطة جيلز كان عند تقديم Mini-ML، وهي لهجة نقية من ML .

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

يصف علم الدلالات ذو الخطوة الكبيرة بطريقة تقسيم وغزو كيف يمكن الحصول على نتائج التقييم النهائية لهياكل اللغة من خلال الجمع بين نتائج تقييم نظيراتها النحوية (التعبيرات الفرعية، والعبارات الفرعية، وما إلى ذلك).

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

تتمتع دلالات الخطوة الكبيرة بميزة كونها غالبًا ما تكون أبسط (تحتاج إلى قواعد استدلال أقل) وغالبًا ما تتوافق بشكل مباشر مع تنفيذ فعال لمترجم للغة (ومن هنا أطلق عليها كاهن اسم "طبيعية"). يمكن أن يؤدي كلاهما إلى إثباتات أبسط، على سبيل المثال عند إثبات الحفاظ على الصحة في ظل بعض تحويلات البرنامج . ^[10]

العيب الرئيسي لدلالات الخطوة الكبيرة هو أن العمليات الحسابية غير المنتهية ( المتباعدة ) لا تحتوي على شجرة استدلال، مما يجعل من المستحيل تحديد وإثبات خصائص مثل هذه العمليات الحسابية. ^[10]

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

• الدلالات الجبرية
• الدلالات البديهية
• الدلالات الإشارية
• الدلالات الرسمية للغات البرمجة

• جيلز كاهن . "الدلالات الطبيعية". وقائع الندوة السنوية الرابعة حول الجوانب النظرية لعلوم الكمبيوتر . دار نشر سبرينغر. لندن. 1987.
• جوردون د. بلوتكين. نهج هيكلي للدلالات التشغيلية. (1981) Tech. Rep. DAIMI FN-19، قسم علوم الكمبيوتر، جامعة آرهوس، آرهوس، الدنمارك. (أعيد طبعه مع التصحيحات في J. Log. Algebr. Program. 60-61: 17-139 (2004)، طبعة أولية).
• جوردون د. بلوتكين. أصول الدلالات التشغيلية البنيوية. مجلة الجبر اللوجيستية. 60-61:3-15، 2004. (طبعة أولية).
• دانا إس سكوت. مخطط لنظرية حسابية رياضية، مجموعة أبحاث البرمجة، دراسة تقنية PRG-2، جامعة أكسفورد، 1970.
• أدريان فان فيجنجاردن وآخرون. تقرير منقح عن اللغة الخوارزمية ALGOL 68 . إيفيب. 1968. ([2] ^{[ الرابط الميت الدائم ]} )
• ماثيو هينيسي . دلالات لغات البرمجة. وايلي، 1990. متاح على الإنترنت.

• الوسائط المتعلقة بالدلالات التشغيلية في ويكيميديا ​​كومنز