نسخة الحلقة

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

تتميز العلاقة المؤسسة بوجود عنصر أدنى في كل مجموعة جزئية غير فارغة من مجالها. ويُثبت وجود متغير انتهاء حلقة while في برنامج حاسوبي عن طريق النزول المؤسس . ^{[ 1 ]} من الخصائص الأساسية للعلاقة المؤسسة عدم وجود سلاسل تنازلية لانهائية . لذلك، ستنتهي الحلقة التي تحتوي على متغير بعد عدد محدود من التكرارات، طالما أن جسمها ينتهي في كل مرة.

يقال إن حلقة while، أو بشكل عام، برنامج كمبيوتر قد يحتوي على حلقات while، صحيح تمامًا إذا كان صحيحًا جزئيًا وينتهي.

من أجل صياغة قاعدة الاستدلال لإنهاء حلقة while التي أوضحناها أعلاه بشكل رسمي، تذكر أنه في منطق فلويد-هوار ، فإن قاعدة التعبير عن الصحة الجزئية لحلقة while هي:

${\displaystyle {\frac {\{I\land C\}\;S\;\{I\}}{\{I\}\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;\{I\land \lnot C\}}},}$

حيث I هو الثابت ، وC هو الشرط ، و S هو جسم الحلقة. وللتعبير عن صحة تامة، نكتب بدلاً من ذلك:

${\displaystyle {\frac {<{\text{ is wellfounded}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I]\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},}$

حيث أن V هو المتغير ، وبحسب الاصطلاح، يتم اعتبار الرمز غير المقيد z كميًا بشكل عالمي .

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

${\displaystyle {\mathtt {while}}\;C\;{\mathtt {do}}\;S}$

ينتهي الأمر بالنظر إلى الثابت I حيث لدينا تأكيد الصحة الكاملة.

${\displaystyle [I\land C]\;S\;[I].}$

لنفترض علاقة "الخلف" على فضاء الحالة Σ الناتجة عن تنفيذ العبارة S من حالة تحقق كلاً من الثابت I والشرط C. أي أننا نقول إن الحالة σ ′ هي "خلف" للحالة σ إذا وفقط إذا

• تكون العبارتان I و C صحيحتين في الحالة σ ، و
• σ ′ هي الحالة التي تنتج عن تنفيذ العبارة S في الحالة σ .

نلاحظ أن${\displaystyle \sigma '\neq \sigma ,}$وإلا فإن الحلقة ستفشل في الانتهاء.

لننتقل الآن إلى دراسة الإغلاق الانعكاسي والمتعدي لعلاقة "الخلف". لنسمي هذه العملية تكرارًا : نقول إن الحالة σ ′ هي تكرار للحالة σ إذا كان أي مما يلي صحيحًا ${\displaystyle \sigma '=\sigma ,}$أو توجد سلسلة محدودة${\displaystyle \sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}}$بحيث${\displaystyle \sigma _{0}=\sigma ,}$${\displaystyle \sigma _{n}=\sigma '}$و${\displaystyle \sigma _{i+1}}$هو "خليفة" لـ${\displaystyle \sigma _{i};}$لكل ما أنا عليه ،${\displaystyle 0\leq i<n.}$

نلاحظ أنه إذا كانت σ و σ ′ حالتين مختلفتين، وكانت σ ′ تكرارًا لـ σ ، فلا يمكن أن تكون σ تكرارًا لـ σ ′ ، وإلا فلن تنتهي الحلقة. بعبارة أخرى، التكرار غير متناظر، وبالتالي فهو ترتيب جزئي .

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

لذا، وبافتراض صحة بديهية الاختيار ، فإن علاقة "الخلف" التي عرّفناها في الأصل للحلقة تستند إلى فضاء الحالة Σ ، لأنها علاقة صارمة (غير انعكاسية) ومضمنة في علاقة "التكرار". وبالتالي، فإن دالة التطابق على فضاء الحالة هذا هي صيغة بديلة لحلقة while، حيث بيّنا أن الحالة يجب أن تتناقص بشكل صارم - كـ"خلف" و"تكرار" - في كل مرة يُنفّذ فيها الجسم S ، مع الأخذ في الاعتبار الثابت I والشرط C.

علاوة على ذلك، يمكننا أن نبين من خلال حجة العد أن وجود أي متغير يستلزم وجود متغير في ω ₁ ، وهو أول عدد ترتيبي غير قابل للعد ، أي

${\displaystyle V:\Sigma \rightarrow \omega _{1}.}$

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

عمليًا، غالبًا ما تُعتبر متغيرات الحلقات أعدادًا صحيحة غير سالبة ، أو حتى يُشترط ذلك ^{[ 2 ]،} لكن اشتراط وجود متغير عددي صحيح في كل حلقة يُفقد لغة البرمجة القدرة التعبيرية للتكرار غير المحدود . ما لم تسمح هذه اللغة (المُدققة رسميًا) بإثبات انتهاء غير محدود لبنية أخرى قوية بنفس القدر، مثل استدعاء دالة تكرارية ، فإنها تفقد القدرة على التكرار الكامل من النوع μ ، وتقتصر على التكرار الأولي . تُعد دالة أكرمان مثالًا نموذجيًا لدالة تكرارية لا يمكن حسابها في حلقة ذات متغير عددي صحيح .

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

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

/** متغير شرطي، يتم تغييره في الإجراء S() **/ bool C ; /** دالة، تحسب حد تكرار الحلقة بدون آثار جانبية **/ inline unsigned int getBound ();/** يجب ألا يُغير جسم الحلقة V **/ inline void S ();int main () { unsigned int V = getBound (); /* اجعل المتغير مساويًا للحد */ assert ( I ); /* شرط الحلقة */ while ( C ) { assert ( V > 0 ); /* هذا التأكيد هو سبب وجود المتغير */ S (); /* استدعاء جسم الحلقة */ V = ​​min ( getBound (), V - 1 ); /* يجب أن ينقص المتغير بمقدار واحد على الأقل */ }; assert ( I && ! C ); /* الشرط لا يزال صحيحًا والشرط خاطئ */return 0 ; };

• حلقة التكرار
• ثابت الحلقة
• الاستقراء المتسامي
• حالة السلسلة الهابطة
• عدد ترتيبي كبير قابل للعد
• الصحة (علوم الحاسوب)
• أضعف الشروط المسبقة لحلقة While