टर्मिनेशन एनालिसिस

void f(int n) { while (n > 1) if (n % 2 == 0) n = n / 2; else n = 3 * n + 1; }

2021 तक, यह अभी भी अज्ञात है चाहे यह C-प्रोग्राम हर इनपुट के लिए समाप्त; कोलात्ज़ अनुमान देखें।

कंप्यूटर विज्ञान में, टर्मिनेशन विश्लेषण प्रोग्राम विश्लेषण है जो यह निर्धारित करने का प्रयास करता है कि किसी दिए गए कंप्यूटर प्रोग्राम का मूल्यांकन 'प्रत्येक' इनपुट के लिए रुकता है या नहीं रुकता है। इसका अर्थ यह निर्धारित करना है कि क्या इनपुट प्रोग्राम टोटल फंक्शन की गणना करता है।

यह हाल्टिंग समस्या से निकटता से संबंधित है, जो यह निर्धारित करना है कि क्या एक दिया गया प्रोग्राम दिए गए इनपुट के लिए रुकता है और यह अनिर्णीत समस्या है। टर्मिनेशन विश्लेषण हाल्टिंग समस्या: ट्यूरिंग मशीनों के प्रतिरूप में टर्मिनेशन विश्लेषण से भी अधिक कठिन है, कम्प्यूटेशनल कार्यों को लागू करने वाले कार्यक्रमों के प्रतिरूप के रूप में यह निश्चित करने का लक्ष्य होगा कि दी गई ट्यूरिंग मशीन कुल ट्यूरिंग मशीन है, और यह समस्या अंकगणितीय पदानुक्रम के $\Pi _{2}^{0}$ स्तर पर है और इस प्रकार हाल्टिंग समस्या की तुलना में अधिक कठिन है।

अब इस प्रश्न के रूप में कि क्या एक संगणनीय कार्य अर्ध-निर्णायक नहीं कुल है, प्रत्येक ध्वनि टर्मिनेशन विश्लेषक (अर्थात् एक गैर-टर्मिनेशन कार्यक्रम के लिए एक सकारात्मक उत्तर कभी नहीं दिया जाता है) अधूरा है, अर्थात असीमित रूप से समाप्त होने वाले कई कार्यक्रमों के लिए टर्मिनेशन का निर्धारण करने में विफल होना चाहिए, या तो हमेशा के लिए दौड़कर या अनिश्चित उत्तर के साथ रुक कर।

टर्मिनेशन प्रमाण

टर्मिनेशन प्रमाण एक प्रकार का गणितीय प्रमाण है जो औपचारिक सत्यापन में महत्वपूर्ण भूमिका निभाता है क्योंकि कलन विधि की कुल शुद्धता टर्मिनेशन पर निर्भर करती है।

टर्मिनेशन प्रमाण के निर्माण के लिए एक सरल, सामान्य विधि में कलन विधि के प्रत्येक चरण के साथ एक 'माप' को जोड़ना सम्मिलित है। माप एक विधिवत प्रमाणन के क्षेत्र से लिया जाता है, जैसे कि क्रमिक संख्याओं से लिया जाता है। यदि कलन विधि के हर संभव चरण के साथ संबंध के अनुसार माप घटता है, तो इसे समाप्त होना चाहिए, क्योंकि एक अच्छी तरह से स्थापित संबंध के संबंध में कोई अनंत अवरोही श्रृंखला नहीं है।

कुछ प्रकार के टर्मिनेशन विश्लेषण स्वचालित रूप से टर्मिनेशन प्रमाण के अस्तित्व को उत्पन्न या प्रभावित कर सकते हैं।

उदाहरण

एक प्रोग्रामिंग भाषा निर्माण का एक उदाहरण प्रोग्राम लूप है जो समाप्त हो भी सकता है और नहीं भी हो सकता है, क्योंकि उन्हें बार-बार चलाया जा सकता है। सामान्यतः डाटा प्रासेसिंग कलन विधि में पाए जाने वाले प्रतिकूल (डिजिटल) का उपयोग करके कार्यान्वित किए गए लूप सामान्यतः समाप्त हो जाएंगे, जो नीचे स्यूडोकोड उदाहरण द्वारा प्रदर्शित किया गया है:

i := 0
 loop until i = SIZE_OF_DATA
    process_data(data[i])) // process the data chunk at position i
 i := i + 1 // move to the next chunk of data to be pressed
   

यदि डेटा के आकार का मान गैर-ऋणात्मक, निश्चित और परिमित है, तो लूप अंततः समाप्त हो जाएगा, यह मानते हुए कि विधि_आँकड़े भी समाप्त हो जाते हैं।

कुछ लूपों को मानव निरीक्षण के माध्यम से हमेशा समाप्त या कभी समाप्त नहीं दिखाया जा सकता है। उदाहरण के लिए, निम्नलिखित लूप, सिद्धांत रूप में, कभी नहीं रुकेगा। हालांकि, अंकगणितीय अतिप्रवाह के कारण भौतिक मशीन पर निष्पादित होने पर यह रुक सकता है: या तो अपवाद से निपटने या काउंटर को नकारात्मक मूल्य पर लपेटने और लूप की स्थिति को पूरा करने में सक्षम बनाता है।

i := 1

loop until i = 0
    i := i + 1

टर्मिनेशन विश्लेषण में कोई अज्ञात इनपुट के आधार पर किसी प्रोग्राम के टर्मिनेशन व्यवहार को निर्धारित करने का भी प्रयास कर सकता है। निम्न उदाहरण इस समस्या को दर्शाता है।

i := 1
loop until i = UNKNOWN
i := i + 1    

यहां लूप कंडीशन को कुछ मान अननोनका उपयोग करके परिभाषित किया गया है, जहां अननोनका मान ज्ञात नहीं है (उदाहरण के लिए प्रोग्राम निष्पादित होने पर उपयोगकर्ता के इनपुट द्वारा परिभाषित)। यहाँ टर्मिनेशन विश्लेषण को अननोन के सभी संभावित मूल्यों को ध्यान में रखना चाहिए और पता लगाना चाहिए कि अननोन= 0 के संभावित स्तिथि में (जैसा कि मूल उदाहरण में है) समापन नहीं दिखाया जा सकता है।

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

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

पुनरावर्तन (कंप्यूटर विज्ञान) और लूप अभिव्यक्ति में समान हैं; लूप से जुड़ी कोई भी अभिव्यक्ति रिकर्सन का उपयोग करके लिखी जा सकती है, और इसके विपरीत। इस प्रकार पुनरावर्तन टर्मिनेशन भी सामान्य रूप से अनिर्णीत है। सामान्य उपयोग में पाई जाने वाली अधिकांश पुनरावर्ती अभिव्यक्तियाँ (अर्थात पैथोलॉजिकल (गणित) नहीं) को सामान्यतः अभिव्यक्ति की परिभाषा के आधार पर विभिन्न माध्यमों से समाप्त करने के लिए दिखाया जा सकता है। उदाहरण के लिए, नीचे क्रमगुणित प्रणाली के लिए पुनरावर्ती अभिव्यक्ति में प्रणाली तर्क हमेशा 1 से घट जाएगा; प्राकृतिक संख्याओं की सुव्यवस्थित संपत्ति द्वारा, तर्क अंततः 1 तक पहुंच जाएगा और पुनरावर्तन समाप्त हो जाएगा।

function factorial (argument as natural number)
   if argument = 0 or argument = 1
        return 1
    otherwise
        return argument * factorial(argument - 1)

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

आकार प्रकार

आश्रित रूप से टाइप की गई प्रोग्रामिंग भाषाओं में टर्मिनेशन जाँच के तरीकों में से एक आकार प्रकार है। मुख्य विचार उन प्रकारों को टिप्पणी करना है जिन पर हम आकार एनोटेशन के साथ पुनरावर्ती कर सकते हैं और केवल छोटे तर्कों पर पुनरावर्ती कॉल की अनुमति दे सकते हैं। एग्डा (प्रोग्रामिंग भाषा) में वाक्यात्मक विस्तारण के रूप में आकार प्रकार लागू किए जाते हैं।

वर्तमान शोध

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

हॉल्टिंग समस्या की अनिश्चितता के कारण इस क्षेत्र में अनुसंधान पूर्णता तक नहीं पहुँच सकता है। कोई हमेशा नए तरीकों के बारे में सोच सकता है जो टर्मिनेशन के नए (जटिल) कारण ढूंढता है।

यह भी देखें

• जटिलता विश्लेषण - समाप्त करने के लिए आवश्यक समय का अनुमान लगाने की समस्या
• लूप रूपांतर
• कुल कार्यात्मक प्रोग्रामिंग - एक प्रोग्रामिंग प्रतिमान जो कार्यक्रमों की श्रेणी को उन तक सीमित करता है जो सिद्ध रूप से समाप्त हो रहे हैं
• वाल्थर रिकर्सन

संदर्भ

Research papers on automated program termination analysis include:

• Christoph Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs". Proc. 9th Conference on Automated Deduction. LNAI. Vol. 310. Springer. pp. 602–621.
• Christoph Walther (1991). "On Proving the Termination of Algorithms by Machine" (PDF). Artificial Intelligence. 70 (1).
• Xi, Hongwei (1998). "Towards Automated Termination Proofs through Freezing" (PDF). In Tobias Nipkow (ed.). Rewriting Techniques and Applications, 9th Int. Conf., RTA-98. LNCS. Vol. 1379. Springer. pp. 271–285.
• Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs". In W. Bibel; P. Schmitt (eds.). Automated Deduction - A Basis for Applications (postscript). Vol. 3. Dordrecht: Kluwer Academic Publishers. pp. 135–164.
• Christoph Walther (2000). "Criteria for Termination". In S. Hölldobler (ed.). Intellectics and Computational Logic (postscript). Dordrecht: Kluwer Academic Publishers. pp. 361–386.
• Christoph Walther; Stephan Schweitzer (2005). "Automated Termination Analysis for Incompletely Defined Programs" (PDF). In Franz Baader; Andrei Voronkov (eds.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNAI. Vol. 3452. Springer. pp. 332–346.
• Adam Koprowski; Johannes Waldmann (2008). "Arctic Termination ...Below Zero". In Andrei Voronkov (ed.). Rewriting Techniques and Applications, 19th Int. Conf., RTA-08 (PDF). Lecture Notes in Computer Science. Vol. 5117. Springer. pp. 202–216. ISBN 978-3-540-70588-8.

System descriptions of automated termination analysis tools include:

• Giesl, J. (1995). "Generating Polynomial Orderings for Termination Proofs (system description)". In Hsiang, Jieh (ed.). Rewriting Techniques and Applications, 6th Int. Conf., RTA-95 (postscript). LNCS. Vol. 914. Springer. pp. 426–431.
• Ohlebusch, E.; Claves, C.; Marché, C. (2000). "TALP: A Tool for the Termination Analysis of Logic Programs (system description)". In Bachmair, Leo (ed.). Rewriting Techniques and Applications, 11th Int. Conf., RTA-00 (compressed postscript). LNCS. Vol. 1833. Springer. pp. 270–273.
• Hirokawa, N.; Middeldorp, A. (2003). "Tsukuba Termination Tool (system description)". In Nieuwenhuis, R. (ed.). Rewriting Techniques and Applications, 14th Int. Conf., RTA-03 (PDF). LNCS. Vol. 2706. Springer. pp. 311–320.
• Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S. (2004). "Automated Termination Proofs with AProVE (system description)". In van Oostrom, V. (ed.). Rewriting Techniques and Applications, 15th Int. Conf., RTA-04 (PDF). LNCS. Vol. 3091. Springer. pp. 210–220. ISBN 3-540-22153-0.
• Hirokawa, N.; Middeldorp, A. (2005). "Tyrolean Termination Tool (system description)". In Giesl, J. (ed.). Term Rewriting and Applications, 16th Int. Conf., RTA-05. LNCS. Vol. 3467. Springer. pp. 175–184. ISBN 978-3-540-25596-3.
• Koprowski, A. (2006). "TPA: Termination Proved Automatically (system description)". In Pfenning, F. (ed.). Term Rewriting and Applications, 17th Int. Conf., RTA-06. LNCS. Vol. 4098. Springer. pp. 257–266.
• Marché, C.; Zantema, H. (2007). "The Termination Competition (system description)". In Baader, F. (ed.). Term Rewriting and Applications, 18th Int. Conf., RTA-07 (PDF). LNCS. Vol. 4533. Springer. pp. 303–313.

बाहरी संबंध

• Termination Analysis of Higher-Order Functional Programs
• Termination Tools mailing list
• Termination Competition — see Marché, Zantema (2007) for a description
• Termination Portal