💻 computer science

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library

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

المؤلفون الأصليون: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

نُشر 2026-02-18

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أن لديك آلة ضخمة ومعقدة — مثل شخصية في لعبة فيديو، أو نظام إشارات مرور، أو مكنسة روبوتية. أنت تريد أن تعرف: "كيف تتصرف هذه الآلة؟" و "هل تتصرف تماماً بنفس الطريقة التي تتصرف بها تلك الآلة الأخرى؟"

في علوم الحاسوب، نستخدم إطار عمل يسمى نظام الانتقال المسمى (LTS) لرسم خريطة لكل حركة ممكنة يمكن للآلة القيام بها. فكر في الـ LTS كأنه كتاب "اختر مغامرتك الخاصة" ضخم ومتفرع، حيث كل صفحة تمثل حالة، وكل سهم يمثل حركة مصحوبة بتسمية (مثل "اضغط ابدأ"، "تحرك يساراً"، أو "أرسل رسالة").

الورقة البحثية التي تسأل عنها تتعلق ببناء قاعدة قواعد عالمية (تسمى منطق هينيسي-ميلنر، أو HML) لوصف هذه الآلات، وإثبات أن هذه القاعدة دقيقة تماماً.

إليك تفصيل عملهم باستخدام تشبيهات بسيطة:

١. المشكلة: "هل هاتان الآلتان توأمان؟"

تخيل أن لديك روبوتين، الروبوت أ و الروبوت ب.

الروبوت أ يمكنه الضغط على زر والانتقال إلى غرفة بها قطة.
الروبوت ب يمكنه الضغط على زر والانتقال إلى غرفة بها كلب.

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

يستخدم علماء الحاسوب المحاكاة المتشابهة (Bisimulation). هذا يشبه "اختبار المرآة". إذا قام الروبوت (أ) بحركة، يجب على الروبوت (ب) أن يكون قادراً على القيام بحركة مطابقة تؤدي إلى حالة تبدو جيدة بنفس القدر. إذا استطاعا الاستمرار في محاكاة بعضهما البعض للأبد، فهما "متشابهان بالتبعية" (توأمان).

٢. الحل: "لغة المنطق" (HML)

ابتكر المؤلفون لغة خاصة (HML) لوصف هذه الآلات. بدلاً من قول "الروبوت أ يذهب إلى غرفة القطة"، يستخدمون جملًا منطقية مثل:

"المعين" ( $\langle \mu \rangle$ ): "من الممكن الضغط على الزر $\mu$ والوصول إلى حالة تكون فيها $\phi$ صحيحة." (مثل قول: "هناك مسار للوصول إلى الكنز.")
"الصندوق" ( $[\mu]$ ): "مهما كان شكل الضغط على الزر $\mu$ ، يجب أن ينتهي بك الأمر في حالة تكون فيها $\phi$ صحيحة." (مثل قول: "كل المسارات تؤدي إلى الأمان.")

لقد بنوا هذه اللغة داخل Lean، وهو أداة قوية تعمل بمثابة معلم رياضيات صارم للغاية. يقوم Lean بفحص كل خطوة من خطوات منطقهم لضمان عدم وجود أخطاء.

٣. الإنجاز الكبير: "نظرية المرآة"

الجزء الأكثر شهرة في عملهم هو إثبات نظرية هينيسي-ميلنر.

فكر في الأمر بهذه الطريقة:

المحاكاة المتشابهة (Bisimulation) هي التحقق مما إذا كانت الآلتان تتحركان في تزامن مثالي جسدياً.
تكافؤ النظرية (Theory Equivalence) هي التحقق مما إذا كانت الآلتان تجيبان بـ "نعم" على نفس قائمة الأسئلة في لغة المنطق الخاصة بنا.

لقد أثبت المؤلفون حقيقة سحرية: بالنسبة للآلات التي لا تملك احتمالات تفرع لانهائية (تسمى "محدودة الصورة")، فإن هذين الفحصين متطابقان.

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

٤. لماذا تهم هذه الورقة البحثية (جزء CSLib)

قبل هذا، كان الناس يكتبون أكواداً للتحقق من هذه الأشياء، لكنها كانت غالباً غير منظمة، أو مخصصة لنوع معين من الروبوتات، أو يصعب إعادة استخدامها.

بنى المؤلفون هذا المنطق كـ مكتبة (صندوق أدوات) تسمى CSLib.

التشبيه: تخيل أن الباحثين السابقين صنعوا مفتاح ربط مخصصاً لمسمار محدد. أما المؤلفون فقد صنعوا مجموعة مقابس عالمية عالية الجودة تناسب أي مسمار.
إعادة الاستخدام: نظرًا لأنهم بنوا هذا ضمن "مكتبة علوم الحاسوب في Lean"، يمكن لأي شخص آخر يعمل على الأتمتة، أو بروتوكولات الاتصال، أو التحقق من البرمجيات، أن يأخذ هذا الصندوق ويستخدمه فوراً. ليس عليهم إعادة اختراع العجلة.
الأتمتة: استخدموا تكتيكاً خاصاً يسمى grind (فكر فيه كـ "ممحاة سحرية" أو "طيار آلي") الذي يحل تلقائياً البراهين الرياضية المملة والمتكررة، مما يسم يسمح للباحثين بالتركيز على الأفكار الكبرى.

الملخص

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

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

بناءً على ورقة "منطق هينيسي-ميلنر في مكتبة CSLib، مكتبة علوم الحاسوب لـ Lean"، إليك ملخص تقني مفصل يغطي المشكلة، والمنهجية، والمساهمات، والنتائج، والأهمية.

١. بيان المشكلة

تُعد أنظمة الانتقال المسمّاة (LTSs) الإطار القياسي لتحديد السلوك التشغيلي للأنظمة الحسابية (مثل حساب العمليات، والبروتوكولات، والأتمتة). ومنطق هينيسي-ميلنر (HML) هو منطق جهوي أساسي يُستخدم للاستدلال على هذه الأنظمة. وتتمثل أهم خصائصه في "مبرهنة هينيسي-ميلنر"، التي تثبت أنه بالنسبة لأنظمة LTS ذات "الصور المحدودة" (image-finite)، يكون حالتان متماثلتين في التماثل القوي (strongly bisimilar) إذا وفقط إذا استوفتا نفس المجموعة من قضايا منطق HML (تكافؤ النظرية).

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

نقص في العمومية على مستوى المكتبة: تركز المعالجات الميكانيكية الموجودة في مبرهنات النظريات غالبًا على تنويعات محددة من HML أو أنواع محددة من LTSs بدلاً من كونها مكون مكتبة عام وقابل لإعادة الاستخدام.
التجزئة: هناك حاجة إلى صياغة موحدة وعالية الجودة ضمن مكتبة علوم الحاسوب لـ Lean (CSLib) تتكامل بسلاسة مع نظريات علوم الحاسوب الأخرى (مثل الأتمتة وحساب العمليات) المعرفة في نفس النظام البيئي.

٢. المنهجية

قام المؤلفون بتطوير صياغة لمنطق HML باستخدام Lean 4، مصممة خصيصًا للتكامل مع CSLib و Mathlib (المكتبة الرياضية لـ Lean). وتؤكد منهجيتهم على:

التصميم البارامتري: التعريفات متعددة الأكوان (universe-polymorphic) وبارامترية على أنواع عشوائية للحالات وتسميات الانتقال. يضمن ذلك تطبيق المنطق على أي نظام يتم نمذجته كـ LTS داخل المكتبة.
التكامل مع البنية التحتية القائمة: تستفيد الصياغة من تعريفات CSLib الحالية لأنظمة LTS والتماثل (bisimilarity)، مما يتجنب التكرار.
الأتمتة: تعتمد البراهين بشكل كبير على أتمتة Lean، وتحديدًا تكتيك grind للتعامل مع الالتزامات البرهانية المتكررة المتعلقة بعمليات المجموع والهياكل الاستقرائية.
نهج الدلالات المزدوج: قام المؤلفون بصياغة كل من علاقة الإرضاء الاستقرائية (الدلالات التشغيلية) والدلالات التفسيرية (mapping propositions to sets of states) لإثبات تكافؤهما.

٣. المساهمات الرئيسية

تقدم الورقة ثلاث مساهمات رئيسية:

أ. صياغة المكونات الأساسية لـ HML

عرف المؤلفون المكونات التالية كبنى Lean قابلة لإعادة الاستخدام:
١. بناء الجمل (Syntax): نوع استقرائي لقضايا HML يتضمن true و false والاقتران (∧) والاتحاد (∨) والنمط الماسي (⟨µ⟩) والنمط الصندوقي ([µ]). وقد اعتمدوا نسخة لا تحتوي على نفي صريح في البناء (باستخدام false بدلاً منه) لتبسيط تعريف الإرضاء، مع استعادة النفي عبر دالة مشتقة.
٢. علاقة الإرضاء (Satisfies): تعريف استقرائي يحدد متى يستوفي حال ما قضية ما بناءً على علاقة الانتقال.
٣. الدلالات التفسيرية: دالة تربط كل قضية بمجموعة الحالات التي تستوفيها.
٤. تكافؤ النظرية: تعريف ينص على أن حالتين متكافئتان إذا استوفتا نفس مجموعة القضايا بالضبط.

ب. الميتا-نظرية الكاملة

أثبت المؤلفون الخصائص النظرية الأساسية لـ HML:
١. التكافؤ الدلالي: إثبات أن علاقة الإرضاء الاستقرائية تتطابق مع الدلالات التفسيرية (أي $s \models \phi \iff s \in \llbracket \phi \rrbracket$ ).
٢. ثبات التماثل (Bisimulation Invariance): إثبات أنه إذا كان حالان متماثلان، فإنهما يستوفيان نفس القضايا.
٣. مبرهنة هينيسي-ميلنر: إثبات العكس: بالنسبة لأنظمة LTS ذات "الصور المحدودة"، إذا استوفى حالان نفس القضايا (تكافؤ النظرية)، فإنهما متماثلان.
* ملاحظة تقنية: يعتمد البرهان على العكس على شرط "الصور المحدودة" لتجميع كافة المشتقات الممكنة وتشكيل اتحاد منتهي لإنشاء قضية تمييز لأي زوج غير متماثل.

ج. التكامل وإعادة الاستخدام

الكود جزء من مستودع CSLib الرسمي (Cslib.Logic.HML).
يوفر واجهات برمجة تطبيقات (APIs) تسمح للمشاريع اللاحقة (مثل صياغة حساب العمليات التواصلية - CCS و نظرية الأتمتة داخل CSLib) بوراثة هذه النتائج فورًا.
أظهر المؤلفون ذلك من خلال إثبات أن تكافؤ النظرية يتطابق مع التماثل لنماذج CCS، بشرط استيفائها لشرط الصور المحدودة (على سبيل المثال، عبر التكرار المحروس).

٤. النتائج

الصحة: نجحت الصياغة في إثبات صحة الدلالات التفسيرية ومبرهنة هينيسي-ميلنر الكاملة داخل Lean 4.
نجاح الأتمتة: سمح استخدام تكتيك grind بالحل التلقائي لمعظم حالات البرهان، خاصة في براهين التكافؤ الدلالي وثبات التماثل. وكان التدخل اليدوي الوحيد المطلوب عبارة عن تلميح بسيط لحالة التماثل في النمط الماسي.
القابلية للتطبيق: تطبق المكتبة بنجاء على مكونات CSLib الموجودة. يوضح المثال المقدم أن المبرهنة العامة theoryEq_eq_bisimilarity يمكن تشغيلها مباشرة لنماذج CCS دون إعادة كتابة المنطق.

٥. الأهمية

البنية التحتية التأسيسية: يضع هذا العمل أول صياغة لمنطق جهوي في CSLib، مما يجعله نموذجًا مرجعيًا للتوسعات المستقبلية (مثل التكافؤات الضعيفة، أو معاملات النقطة الثابتة، أو المنطق المخصص لـ $\pi$ -calculus).
العمومية: على عكس الأعمال السابقة التي تستهدف حسابات محددة، فإن هذه الصياغة عامة. فهي تفصل المنطق عن تنفيذ أنظمة محددة، مما يسمح بتطبيقه على أي نظام يلتزم بواجهة LTS الخاصة بـ CSLib.
الربط بين النظرية والتطبيق: من خلال التكامل مع مكتبة مجتمعية متنامية (CSLib)، فإنه يسهل تطوير البرمجيات الموثقة والبحث في نظرية التزامن، مما يجعل النتائج الميتا-نظرية المتقدمة (مثل مبرهنة هينيسي-ميلنر) متاحة بسهولة للمطورين والباحثين الذين يستخدمون Lean.
الاتجاهات المستقبلية: يشير المؤلفون إلى أنه بينما يتعامل العمل الحالي مع التماثل القوي ومنطق HML القياسي، فإن العمل المستقبلي سيتناول التوسعات للتماثلات الضعيفة والمنطق القادر على التعامل مع المتغيرات المقيدة (وهو أمر ضروري لـ $\pi$ -calculus)، والتي تتطلب استدلالًا اسميًا أكثر تعقيدًا.

باختدال، تقدم الورقة صياغة متينة وعامة ومؤتمتة لمنطق هينيسي-ميلنر، تسد الفجوة بين نظرية التزامن المجردة وتطوير البرمجيات العملية والموثقة داخل بيئة Lean.