लूप वैरिएंट

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

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

एक 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 और शर्त सी.

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

$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;
};

एक गैर-पूर्णांक वेरिएंट पर भी विचार क्यों करें?

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

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

यह भी देखें

• घुमाव के दौरान
• लूप इनवेरिएंट
• ट्रांसफिनिट इंडक्शन
• अवरोही श्रृंखला स्टेट
• बड़ा गणनीय क्रमसूचक
• शुद्धता (कंप्यूटर विज्ञान)
• Predicate_transformer_semantics#While_loop | जबकि लूप की सबसे कमजोर पूर्व शर्ते