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

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

كمثال بسيط، سننظر في جزء من دلالات لغة برمجة بسيطة؛ توجد أمثلة توضيحية مناسبة في بلوتكين 81 وهينيسي 90 ، وكتب أخرى.${\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}$".

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

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

2.${\displaystyle {\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 }}}$

3.${\displaystyle {\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}}$.

إذا كان لدينا أيضًا تعبيرات منطقية على مستوى الولاية، مرتبة حسب${\displaystyle B}$ثم يمكننا تحديد دلالات أمر while : ${\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 ( بلوتكين 81 ) بأكثر من 1000 استشهاد وفقًا لموقع CiteSeer.مما يجعله أحد أكثر التقارير الفنية استشهاداً في علوم الحاسوب .

تُعدّ دلالات الاختزال عرضًا بديلًا للدلالات التشغيلية. طُبّقت أفكارها الأساسية لأول مرة على متغيرات حساب لامدا الوظيفية البحتة ، سواءً بالاسم أو بالقيمة، على يد غوردون بلوتكين عام 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 ]}

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