تحليل الإنهاء

📅 آخر تحديث: ٢ أغسطس ٢٠٢٦
✍️ نُشر في: ٢ أغسطس ٢٠٢٦
📷 يحتوي على 1 صور
الموسوعة الحرة
دالة f ( n ): طالما n > 1 : إذا كان n % 2 == 0 : n = n / 2 وإلا : n = 3 * n + 1
اعتبارًا من عام 2026، لا يزال من غير المعروف ما إذا كان برنامج بايثون هذا ينتهي لكل إدخال عدد صحيح؛ انظر تخمين كولاتز .

في علم الحاسوب ، يُعد تحليل الإنهاء تحليلاً للبرنامج يهدف إلى تحديد ما إذا كان تقييم برنامج معين يتوقف عند كل مُدخل. وهذا يعني تحديد ما إذا كان البرنامج المُدخل يُحسب دالة كاملة .

يرتبط هذا ارتباطًا وثيقًا بمشكلة التوقف ، وهي تحديد ما إذا كان برنامج معين سيتوقف عند إدخال معين ، وهي مشكلة غير قابلة للحسم . يُعد تحليل الإنهاء أكثر صعوبة من مشكلة التوقف: ففي نموذج آلات تورينج ، كنموذج للبرامج التي تُنفذ وظائف قابلة للحساب، يهدف تحليل الإنهاء إلى تحديد ما إذا كانت آلة تورينج معينة هي آلة تورينج كلية ، وهذه المشكلة على مستوىΠ20{\displaystyle \Pi _{2}^{0}}من التسلسل الهرمي الحسابي، وبالتالي فهو أصعب بكثير من مشكلة التوقف.

الآن بما أن السؤال عما إذا كانت الدالة القابلة للحساب كلية ليس شبه قابل للتقرير ، [ 1 ] فإن كل محلل إنهاء سليم (أي لا يتم إعطاء إجابة إيجابية لبرنامج غير منتهٍ) يكون غير مكتمل ، أي يجب أن يفشل في تحديد الإنهاء لعدد لا نهائي من البرامج المنتهية، إما عن طريق التشغيل إلى الأبد أو التوقف بإجابة غير محددة.

مقاوم للإنهاء

يُعد برهان الإنهاء نوعًا من البراهين الرياضية التي تلعب دورًا حاسمًا في التحقق الرسمي لأن الصحة الكاملة للخوارزمية تعتمد على الإنهاء .

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

يمكن لبعض أنواع تحليل الإنهاء أن تولد تلقائيًا أو تشير ضمنيًا إلى وجود دليل على الإنهاء.

مثال

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

i := 0 كرر حتى i = SIZE_OF_DATA process_data(data[i])) // معالجة جزء البيانات في الموضع i i := i + 1 // الانتقال إلى جزء البيانات التالي المراد معالجته

إذا كانت قيمة SIZE_OF_DATA غير سالبة وثابتة ومحدودة، فستنتهي الحلقة في النهاية، بافتراض أن process_data تنتهي أيضًا.

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

i := 1 كرر حتى i = 0 i := i + 1

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

i := 1 كرر حتى i = غير معروف i := i + 1

هنا، يُعرَّف شرط الحلقة باستخدام قيمة غير معروفة (UNKNOWN)، حيث تكون قيمة هذه القيمة غير معروفة (على سبيل المثال، يتم تحديدها من خلال إدخال المستخدم عند تنفيذ البرنامج). يجب أن يأخذ تحليل الإنهاء في الاعتبار جميع القيم الممكنة لـ UNKNOWN، وأن يكتشف أنه في حالة UNKNOWN = 0 (كما في المثال الأصلي)، لا يمكن إظهار الإنهاء.

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

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

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

دالة حساب المضروب (الوسيط كعدد طبيعي) إذا كان الوسيط = 0 أو الوسيط = 1 ، تُرجع 1، وإلا تُرجع الوسيط * مضروب(الوسيط - 1)

الأنواع التابعة

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

أنواع بأحجام مختلفة

إحدى طرق التحقق من الإنهاء في لغات البرمجة المعتمدة على الأنواع هي الأنواع المُصغَّرة. الفكرة الأساسية هي إضافة تعليقات توضيحية للأنواع التي يمكننا استدعاء الدوال عليها بشكل متكرر، والسماح بالاستدعاءات المتكررة فقط على الوسائط الأصغر. تُطبَّق الأنواع المُصغَّرة في لغة أغدا كامتداد نحوي.

البحوث الحالية

هناك العديد من فرق البحث التي تعمل على تطوير أساليب جديدة لكشف حالات إنهاء البرامج (أو عدم إنهائها). يدمج العديد من الباحثين هذه الأساليب في برامج [ 2 ] تحاول تحليل سلوك الإنهاء تلقائيًا (دون تدخل بشري). يتمثل أحد جوانب البحث المستمرة في تمكين استخدام الأساليب الحالية لتحليل سلوك إنهاء البرامج المكتوبة بلغات برمجة "واقعية". بالنسبة للغات التصريحية مثل هاسكل وميركوري وبرولوج ، توجد نتائج عديدة [ 3 ] [ 4 ] [ 5 ] (وذلك أساسًا بسبب الأساس الرياضي المتين لهذه اللغات). كما يعمل مجتمع البحث على تطوير أساليب جديدة لتحليل سلوك إنهاء البرامج المكتوبة بلغات إجرائية مثل سي وجافا.

انظر أيضاً

مراجع

  1. ↑ روجرز الابن، هارتلي (1988). نظرية الدوال التكرارية والحوسبة الفعالة . كامبريدج (ماساتشوستس)، لندن (إنجلترا): مطبعة معهد ماساتشوستس للتكنولوجيا. ص  476. ISBN 0-262-68052-1.
  2. ↑ "التصنيف: أدوات - Termination-Portal.org" . termination-portal.org .
  3. ↑ جيسل، ج.؛ سويدرسكي، س.؛ شنايدر-كامب، ب.؛ ثيمان، ر.؛ بفينينغ، ف. (محررون). تحليل الإنهاء الآلي للغة هاسكل: من إعادة كتابة المصطلحات إلى لغات البرمجة (محاضرة مدعوة) (ملحق) . إعادة كتابة المصطلحات وتطبيقاتها، المؤتمر الدولي السابع عشر، RTA-06. سلسلة محاضرات في علوم الحاسوب. المجلد 4098. الصفحات 297-312 . (الرابط: springerlink.com ).  
  4. ↑ خيارات المُترجم لتحليل الإنهاء في ميركوري
  5. ↑ نغوين، مان ثانغ؛ جيسل، يورغن؛ شنايدر-كامب، بيتر؛ دي شري، داني. "تحليل إنهاء البرامج المنطقية بناءً على مخططات التبعية" ( ملف PDF) . verify.rwth-aachen.de

تشمل الأبحاث المتعلقة بتحليل إنهاء البرامج الآلي ما يلي:

تتضمن أوصاف أنظمة أدوات تحليل الإنهاء الآلي ما يلي: