علم الدلالة (لغات البرمجة)

في نظرية لغات البرمجة ، تُعرف الدلالات بأنها الدراسة المنطقية الرياضية الدقيقة لمعاني لغات البرمجة . ^{[ 1 ]} تُسند الدلالات معنى حسابيًا للسلاسل النصية الصحيحة في بنية لغة البرمجة . وهي وثيقة الصلة بدلالات البراهين الرياضية ، وغالبًا ما تتداخل معها .

يصف علم الدلالة العمليات التي يتبعها الحاسوب عند تنفيذ برنامج بلغة برمجة محددة. ويمكن تحقيق ذلك من خلال وصف العلاقة بين مدخلات ومخرجات البرنامج، أو تقديم شرح لكيفية تنفيذ البرنامج على منصة معينة ، مما يُنشئ نموذجًا للحوسبة .

في عام 1967، نشر روبرت دبليو فلويد بحثًا بعنوان "إسناد معانٍ للبرامج "؛ وكان هدفه الرئيسي "وضع معيار صارم لإثباتات برامج الحاسوب، بما في ذلك إثباتات الصحة والتكافؤ والإنهاء". ^{[ 2 ] [ 3 ]} وكتب فلويد أيضًا: ^{[ 2 ]}

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

في عام 1969، نشر توني هوار ورقة بحثية حول منطق هوار الذي استند إلى أفكار فلويد، والتي تُعرف الآن أحيانًا مجتمعة باسم الدلالات البديهية . ^{[ 4 ] [ 5 ]}

في سبعينيات القرن العشرين، ظهر مصطلحا الدلالات التشغيلية والدلالات الدلالية . ^{[ 5 ]}

يشمل مجال الدلالات الرسمية كل ما يلي:

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

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

توجد العديد من المناهج في علم الدلالة الرسمي؛ وهذه تنتمي إلى ثلاث فئات رئيسية:

• الدلالات الدلالية ^{[ 6 ]} ،حيث تُفسَّر كل عبارة في اللغة على أنها دلالة ، أي معنى مفاهيمي يمكن تصوره بشكل مجرد. غالبًا ما تكون هذه الدلالات كائنات رياضية تنتمي إلى فضاء رياضي، ولكن ليس من الضروري أن تكون كذلك. وكضرورة عملية، تُوصَف الدلالات باستخدام شكل من أشكال الترميز الرياضي، والذي يمكن بدوره صياغته كلغة وصفية دلالية. على سبيل المثال، غالبًا ما تُترجم الدلالات الدلالية للغات الوظيفية اللغة إلى نظرية المجال . كما يمكن أن تُستخدم الأوصاف الدلالية الدلالية كترجمات تركيبية من لغة برمجة إلى اللغة الوصفية الدلالية، وأن تُستخدم كأساس لتصميم المترجمات .
• الدلالات التشغيلية ، ^{[ 7 ]} حيث يتم وصف تنفيذ اللغة مباشرةً (بدلاً من الترجمة). تتوافق الدلالات التشغيلية بشكل عام مع التفسير ، على الرغم من أن "لغة التنفيذ" الخاصة بالمفسر هي عادةً صيغة رياضية. قد تُعرّف الدلالات التشغيلية آلةً مجردة (مثل آلة SECD )، وتُضفي معنىً على العبارات من خلال وصف التحولات التي تُحدثها على حالات الآلة. بدلاً من ذلك، كما هو الحال مع حساب لامدا البحت ، يمكن تعريف الدلالات التشغيلية من خلال التحويلات النحوية على عبارات اللغة نفسها.
• الدلالة البديهية ، ^{[ 8 ]} حيث يُعطى معنى للعبارات من خلال وصف البديهيات التي تنطبق عليها. لا تُميّز الدلالة البديهية بين معنى العبارة والصيغ المنطقية التي تصفها؛ فمعناها هو بالضبط ما يمكن إثباته عنها في منطق معين. المثال الكلاسيكي للدلالة البديهية هو منطق هوار .

بصرف النظر عن الاختيار بين المناهج الدلالية أو التشغيلية أو البديهية، فإن معظم الاختلافات في الأنظمة الدلالية الرسمية تنشأ من اختيار الشكلية الرياضية الداعمة.

تتضمن بعض الاختلافات في الدلالات الرسمية ما يلي:

• دلالات الفعل ^{[ 9 ]} هي نهج يحاول تقسيم الدلالات الدلالية إلى وحدات، وتقسيم عملية الصياغة الرسمية إلى طبقتين (الدلالات الكلية والجزئية) وتحديد ثلاثة كيانات دلالية مسبقًا (الأفعال والبيانات والمُنتِجات) لتبسيط المواصفات؛
• الدلالات الجبرية ^{[ 8 ]} هي شكل من أشكال الدلالات البديهية القائمة على القوانين الجبرية لوصف دلالات البرامج والاستدلال عليها بطريقة رسمية . كما أنها تدعم الدلالات الدلالية والدلالات التشغيلية ؛
• تُعرّف قواعد السمات ^{[ 10 ]} أنظمةً تحسب بشكل منهجي " البيانات الوصفية " (المسماة بالسمات ) لمختلف حالات بناء الجملة في اللغة . ويمكن فهم قواعد السمات على أنها دلالات وصفية حيث تكون اللغة الهدف هي اللغة الأصلية مُثرية بتعليقات السمات. وإلى جانب الدلالات الرسمية، استُخدمت قواعد السمات أيضًا لتوليد التعليمات البرمجية في المترجمات ، ولإثراء القواعد العادية أو الخالية من السياق بشروط حساسة للسياق .
• تستخدم الدلالات الفئوية (أو "الوظيفية") ^{[ 11 ]} نظرية الفئات كصيغة رياضية أساسية. وعادةً ما يُثبت أن الدلالات الفئوية تتوافق مع بعض الدلالات البديهية التي تُقدم عرضًا نحويًا للبنى الفئوية. كما أن الدلالات الدلالية غالبًا ما تكون أمثلة على الدلالات الفئوية العامة؛ ^{[ 12 ]}
• دلالات التزامن ^{[ 13 ]} هي مصطلح شامل لأي دلالات رسمية تصف العمليات الحسابية المتزامنة. وقد تضمنت الصيغ الرسمية المتزامنة ذات الأهمية التاريخية نموذج الممثل وحسابات العمليات ؛
• يستخدم علم دلالات الألعاب ^{[ 14 ]} استعارة مستوحاة من نظرية الألعاب ؛
• دلالات محول المسند ، ^{[ 15 ]} التي طورها إدسكار دبليو ديجكسترا ، تصف معنى جزء البرنامج على أنه الدالة التي تحول الشرط اللاحق إلى الشرط المسبق اللازم لإنشائه.

لأسبابٍ عديدة، قد يرغب المرء في وصف العلاقات بين الدلالات الرسمية المختلفة. على سبيل المثال:

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

من الممكن أيضاً ربط دلالات متعددة من خلال التجريدات عبر نظرية التفسير المجرد .

• الدلالات الحاسوبية
• الدلالات الرسمية (المنطق)
• الدلالات الرسمية (علم اللغة)
• علم الوجود
• علم الوجود (علم المعلومات)
• التكافؤ الدلالي
• التكنولوجيا الدلالية

الكتب الدراسية

• آبي، أنتوني (2004). مقدمة في لغات البرمجة . مؤرشف من الأصل بتاريخ 19-06-2015.علم الدلالة.