लूप वैरिएंट

कंप्यूटर विज्ञान में, एक लूप वेरिएंट, एक कंप्यूटर प्रोग्राम के स्टेट स्पेस पर परिभाषित एक गणितीय फ़ंक्शन है, जिसका मान एक निश्चित रूप से कम होता है, जो कुछ इनवेरिएंट स्थितियों के तहत एक समय लूप की गणना द्वारा अच्छी तरह से स्थापित संबंध के संबंध में एक निश्चित रूप से कम होता है, जिससे यह समाप्त हो जाता है। एक लूप वेरिएंट जिसकी सीमा ऋणेतर  पूर्णांक तक सीमित है, एक बाउंड फ़ंक्शन के रूप में भी जाना जाता है, क्योंकि इस स्थिति में यह एक लूप के पुनरावृत्तियों की संख्या पर एक छोटी ऊपरी सीमा प्रदान करता है। हालांकि, एक लूप वेरिएंट ट्रांसफिनाइट हो सकता है, और इस प्रकार आवश्यक रूप से पूर्णांक मूल्यों तक सीमित नहीं है।

एक अच्छी तरह से स्थापित संबंध अपने डोमेन के प्रत्येक गैर-रिक्त उपसमुच्चय के न्यूनतम तत्व के अस्तित्व की विशेषता है। वेरिएंट का अस्तित्व अच्छी तरह से स्थापित अवतरण द्वारा एक कंप्यूटर प्रोग्राम में एक समय के लूप की समाप्ति को सिद्ध करता है। एक अच्छी तरह से स्थापित संबंध की एक बुनियादी गुण यह है कि इसमें अनंत अवरोही श्रृंखला नहीं हैं। इसलिए एक लूप जिसमें एक प्रकार होता है, वह पुनरावृत्तियों की एक सीमित संख्या के बाद समाप्त हो जाता है, जब तक कि उसकी बॉडी हर बार समाप्त हो जाती है।

एक while लूप, या, अधिक सामान्यतः, एक कंप्यूटर प्रोग्राम जिसमें while लूप हो सकता है, पूरी तरह से सही कहा जाता है यदि यह आंशिक रूप से सही है और समाप्त हो जाता है।

पूर्ण सत्यता के लिए अनुमान का नियम

कुछ समय की समाप्ति के लिए अनुमान के नियम को औपचारिक रूप से बताने के लिए हमने ऊपर प्रदर्शित किया है, याद करें कि फ्लॉयड-होयर लॉजिक में, एक समय लूप की आंशिक शुद्धता व्यक्त करने का नियम है:

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

जहां I इनवेरिएंट है, C स्टेट है, और S लूप का मुख्य भाग है। पूर्ण सत्यता व्यक्त करने के लिए, हम इसके स्पेस पर लिखते हैं:

${\frac {<{\text{ is well-founded}},\;[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 लूप जो समाप्त होता है (इसके इनवेरिएंट को देखते हुए) का एक प्रकार होता है। इसे सिद्ध करने के लिए मान लीजिए कि लूप

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

इनवेरिएंट I दिए जाने पर समाप्त हो जाता है, जहां हमारे पास पूर्ण यथार्थता का दृढ़ कथन है

$[I\land C]\;S\;[I].$

स्टेट स्पेस Σ पर "सक्सेसर" संबंध पर विचार करें स्टेटमेंट S के निष्पादन से प्रेरित एक स्टेट से जो इनवेरिएंट I और कंडीशन C दोनों को संतुष्ट करता है। यही है, हम कहते हैं कि एक स्टेट σ ′ σ का "सक्सेसर" है यदि और केवल यदि

• I और C दोनों स्टेट σ में ट्रू हैं, और
• σ′ वह स्टेट है जो स्टेट σ में कथन S के निष्पादन के परिणामस्वरूप उत्पन्न होती है।

हमने ध्यान दिया कि $\sigma '\neq \sigma ,$ अन्यथा लूप समाप्त होने में विफल रहेगा।

इसके बाद सक्सेसर संबंध के प्रतिवर्ती, सकर्मक समापन पर विचार करें। इस पुनरावृत्ति को कॉल करें: हम कहते हैं कि एक स्टेट σ′ का पुनरावृत्त है σ या तो $\sigma '=\sigma ,$ अथवा एक परिमित शृंखला $\sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}$है। ऐसा है कि $\sigma _{0}=\sigma ,$ $\sigma _{n}=\sigma '$ और $\sigma _{i+1}$ का सक्सेसर $\sigma _{i};$ सभी के लिए $0\leq i<n.$I, है।

हम ध्यान दें कि यदि σ और σ′ दो अलग-अलग स्टेट हैं, और σ′ का पुनरावृत्त σ है, तब σ का पुनरावृत्त σ′, फिर से नहीं हो सकता, अन्यथा लूप समाप्त होने में विफल रहेगा। दूसरे शब्दों में, पुनरावृत्ति प्रतिसममिति है, और इस प्रकार, एक आंशिक क्रम है।

अब, चूंकि लूप इनवेरिएंट I दिए गए चरणों की एक सीमित संख्या के बाद समाप्त हो जाता है, और किसी भी स्टेट का तब तक कोई सक्सेसर नहीं होता जब तक I उस स्टेट में ट्रू है, हम यह निष्कर्ष निकालते हैं कि प्रत्येक स्टेट में केवल सीमित रूप से कई पुनरावृत्तियाँ होती हैं, पुनरावृत्ति के संबंध में प्रत्येक अवरोही श्रृंखला में केवल सीमित रूप से कई अलग-अलग मान होते हैं, और इस प्रकार कोई अनंत अवरोही श्रृंखला नहीं होती है, अर्थात लूप पुनरावृत्ति अवरोही श्रृंखला की स्टेट को संतुष्ट करती है।

इसलिए - विकल्प के स्वयंसिद्ध सिद्धांत को मानते हुए - "सक्सेसर" संबंध जिसे हमने मूल रूप से लूप के लिए परिभाषित किया था, स्टेट स्पेस Σ पर अच्छी तरह से स्थापित है, क्योंकि यह सख्त (अप्रतिवर्ती) है और "पुनरावृत्त" संबंध में निहित है। इस प्रकार इस स्टेट स्पेस पर पहचान फ़ंक्शन while लूप के लिए एक प्रकार है, जैसा कि हमने दिखाया है कि स्टेट को प्रबलता से कम होना चाहिए - एक "सक्सेसर" और एक "पुनरावृत्त" के रूप में - हर बार जब शरीर एस को इनवेरिएंट I और स्टेट C को देखते हुए निष्पादित किया जाता है।

इसके अतिरिक्त, हम गणना के तर्क से दिखा सकते हैं कि किसी भी प्रकार का एक्सिस्टेंस ω₁ में एक प्रकार के एक्सिस्टेंस का तात्पर्य है, पहला असंख्य क्रमसूचक, यानी,

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

इसका कारण यह है कि एक सीमित इनपुट से चरणों की एक सीमित संख्या में एक सीमित कंप्यूटर प्रोग्राम द्वारा पहुंच योग्य सभी स्टेट का संग्रह गणनीय रूप से अनंत है, और ω₁ गणनीय सेटों पर सभी अच्छी तरह से क्रम प्रकारों की गणना है।

व्यावहारिक दृष्टिकोण

व्यवहार में, लूप वेरिएंट को प्रायः ऋणेत्तर पूर्णांक के रूप में लिया जाता है, या यहां तक ​​कि ऐसा होना भी आवश्यक है, लेकिन यह आवश्यकता कि प्रत्येक लूप में एक पूर्णांक वेरिएंट होता है, एक प्रोग्रामिंग भाषा से असीमित पुनरावृत्ति की अभिव्यंजक शक्ति को हटा देता है। जब तक ऐसी (औपचारिक रूप से सत्यापित) भाषा किसी अन्य समान रूप से निर्माण जैसे कि पुनरावर्ती फ़ंक्शन कॉल के लिए समाप्ति के एक अनंत प्रमाण की अनुमति नहीं देती है, यह अब पूर्ण μ-पुनरावृत्ति में सक्षम नहीं है, बल्कि केवल आदिम पुनरावर्तन में सक्षम है। एकरमैन का फ़ंक्शन एक पुनरावर्ती फ़ंक्शन का विहित उदाहरण है जिसकी गणना पूर्णांक संस्करण वाले लूप में नहीं की जा सकती है।

हालाँकि, उनकी कम्प्यूटेशनल जटिलता के संदर्भ में, जो कार्य आदिम पुनरावर्ती नहीं हैं, वे सामान्यतः ट्रैक्टेबल माने जाने वाले दायरे से बहुत दूर हैं। घातांक के साधारण स्थिति को भी एक आदिम पुनरावर्ती फ़ंक्शन के रूप में ध्यान में रखते हुए, और यह कि आदिम पुनरावर्ती कार्यों की संरचना आदिम पुनरावर्ती है, कोई यह देखना प्रारम्भ कर सकता है कि एक आदिम पुनरावर्ती फ़ंक्शन कितनी तेज़ी से बढ़ सकता है। और कोई भी फ़ंक्शन जिसकी गणना ट्यूरिंग मशीन द्वारा एक आदिम पुनरावर्ती फ़ंक्शन द्वारा बंधे हुए समय में की जा सकती है, वह स्वयं आदिम पुनरावर्ती है। इसलिए पूर्ण μ-पुनरावर्तन के लिए एक व्यावहारिक उपयोग की कल्पना करना मुश्किल है जहां आदिम पुनरावर्तन काम नहीं करेगा, विशेष रूप से चूंकि पूर्व को बाद वाले द्वारा अत्यधिक लंबे समय तक चलने के लिए अनुकरण किया जा सकता है।

और किसी भी स्थिति में, कर्ट गोडेल की पहली अपूर्णता प्रमेय और रुकने की समस्या का अर्थ यह है कि ऐसे लूप हैं जो हमेशा समाप्त हो जाते हैं लेकिन ऐसा करने के लिए सिद्ध नहीं किए जा सकते हैं; इस प्रकार यह अपरिहार्य है कि समाप्ति के औपचारिक प्रमाण के लिए किसी भी आवश्यकता से प्रोग्रामिंग भाषा की अभिव्यंजक शक्ति कम हो जानी चाहिए। जबकि हमने दिखाया है कि समाप्त होने वाले प्रत्येक लूप का एक प्रकार होता है, इसका मतलब यह नहीं है कि लूप पुनरावृत्ति की अच्छी तरह से नींव सिद्ध की जा सकती है।

उदाहरण

यहां एक उदाहरण दिया गया है, C-जैसे स्यूडोकोड में, थोड़ी देर के लूप में शेष पुनरावृत्तियों की संख्या पर कुछ ऊपरी सीमा से गणना की गई पूर्णांक संस्करण हालाँकि, C अभिव्यक्तियों के मूल्यांकन में नकारात्मक प्रभाव की अनुमति देता है, जो कंप्यूटर प्रोग्राम को औपचारिक रूप से सत्यापित करने के दृष्टिकोण से अस्वीकार्य है।

/** condition-variable, which is changed in procedure S() **/
bool C;
/** function, which computes a loop iteration bound without side effects **/
inline unsigned int getBound();

/** body of loop must not alter V **/ 
inline void S(); 

int main() {
    unsigned int V = getBound(); /* set variant equal to bound */
    assert(I); /* loop invariant */
    while (C) {
        assert(V > 0); /* this assertion is the variant's raison d'être (reason of existence) */
        S(); /* call the body */
        V = min(getBound(), V - 1); /* variant must decrease by at least one */
    };
    assert(I && !C); /* invariant is still true and condition is false */

    return 0;
};

फिर एक गैर-पूर्णांक संस्करण (नॉन-इन्टिजर वेरिएंट) पर भी विचार क्यों करें?

एक गैर-पूर्णांक या ट्रांसफ़िनिट वेरिएंट पर भी विचार क्यों करें? यह प्रश्न इसलिए उठाया गया है क्योंकि सभी व्यावहारिक उदाहरणों में जहां हम यह सिद्ध करना चाहते हैं कि एक फंक्शन समाप्त हो जाता है, हम यह भी सिद्ध करना चाहते हैं कि यह उचित समय में समाप्त हो जाता है। वहाँ कम से कम दो संभावनाएँ हैं:

• लूप के पुनरावृत्तियों की संख्या पर ऊपरी सीमा पहली जगह में समाप्ति सिद्ध करने पर सशर्त हो सकती है। यह वांछनीय हो सकता है कि तीनों गुणों को अलग-अलग (या उत्तरोत्तर) सिद्ध किया जाए
  • आंशिक यथार्थता,
  • समाप्ति, और
  • कार्यकारी समय

• व्यापकता: ट्रांसफ़िनिट वेरिएंट पर विचार करने से एक वेरिएंट के अस्तित्व के संदर्भ में थोड़ी देर के लिए समाप्ति के सभी संभावित प्रमाण देखने की अनुमति मिलती है।

यह भी देखें

• व्हाइल लूप
• लूप इंवरिएंट
• ट्रांसफाइनाइट इंडकशन
• डेसेंडिंग चेन कंडीशन
• लार्ज सोँटाबले ऑर्डिनल
• करेक्टनेस (कंप्यूटर साइंस)
• वीकेस्ट-प्रीकंडिशन्स ऑफ़ व्हाइल लूप