टर्मिनेशन एनालिसिस
void f(int n) {
while (n > 1)
if (n % 2 == 0)
n = n / 2;
else
n = 3 * n + 1;
}
|
| As of 2021, it is still unknown whether this C-program terminates for every input; see Collatz conjecture. |
कंप्यूटर विज्ञान में, समाप्ति विश्लेषण प्रोग्राम विश्लेषण है जो यह निर्धारित करने का प्रयास करता है कि किसी दिए गए कंप्यूटर प्रोग्राम का मूल्यांकन 'प्रत्येक' इनपुट के लिए रुकता है या नहीं। इसका मतलब यह निर्धारित करना है कि क्या इनपुट प्रोग्राम टोटल फंक्शन की गणना करता है।
यह हाल्टिंग समस्या से निकटता से संबंधित है, जो यह निर्धारित करना है कि क्या एक दिया गया प्रोग्राम दिए गए इनपुट के लिए रुकता है और जो अनिर्णीत समस्या है। टर्मिनेशन विश्लेषण हाल्टिंग समस्या से भी अधिक कठिन है: ट्यूरिंग मशीनों के मॉडल में टर्मिनेशन विश्लेषण, कम्प्यूटेशनल कार्यों को लागू करने वाले कार्यक्रमों के मॉडल के रूप में यह तय करने का लक्ष्य होगा कि दी गई ट्यूरिंग मशीन कुल ट्यूरिंग मशीन है, और यह समस्या है स्तर पर अंकगणितीय पदानुक्रम का और इस प्रकार हाल्टिंग समस्या की तुलना में सख्ती से अधिक कठिन है।
अब इस प्रश्न के रूप में कि क्या एक संगणनीय कार्य कुल है, निर्णायकता (तर्क) नहीं है | अर्ध-निर्णायक,[1] प्रत्येक ध्वनि समाप्ति विश्लेषक (अर्थात् एक गैर-समाप्ति कार्यक्रम के लिए एक सकारात्मक उत्तर कभी नहीं दिया जाता है) अधूरा है, अर्थात असीमित रूप से समाप्त होने वाले कई कार्यक्रमों के लिए समाप्ति का निर्धारण करने में विफल होना चाहिए, या तो हमेशा के लिए चल रहा है या अनिश्चित उत्तर के साथ रुक रहा है।
समाप्ति प्रमाण
समाप्ति प्रमाण एक प्रकार का गणितीय प्रमाण है जो औपचारिक सत्यापन में महत्वपूर्ण भूमिका निभाता है क्योंकि कलन विधि की कुल शुद्धता समाप्ति पर निर्भर करती है।
समाप्ति प्रमाण के निर्माण के लिए एक सरल, सामान्य विधि में एल्गोरिथम के प्रत्येक चरण के साथ एक 'माप' को जोड़ना शामिल है। माप एक अच्छी तरह से स्थापित संबंध के क्षेत्र से लिया जाता है, जैसे कि क्रमिक संख्याओं से। यदि एल्गोरिथम के हर संभव चरण के साथ संबंध के अनुसार माप घटता है, तो इसे समाप्त होना चाहिए, क्योंकि एक अच्छी तरह से स्थापित संबंध के संबंध में कोई अनंत अवरोही श्रृंखला नहीं है।
कुछ प्रकार के समाप्ति विश्लेषण स्वचालित रूप से समाप्ति प्रमाण के अस्तित्व को उत्पन्न या प्रभावित कर सकते हैं।
उदाहरण
एक प्रोग्रामिंग भाषा निर्माण का एक उदाहरण जो समाप्त हो भी सकता है और नहीं भी हो सकता है एक प्रोग्राम लूप है, क्योंकि उन्हें बार-बार चलाया जा सकता है। आमतौर पर डाटा प्रासेसिंग एल्गोरिदम में पाए जाने वाले काउंटर (डिजिटल) का उपयोग करके कार्यान्वित किए गए लूप आमतौर पर समाप्त हो जाएंगे, जो नीचे स्यूडोकोड उदाहरण द्वारा प्रदर्शित किया गया है:
मैं := 0
i = SIZE_OF_DATA तक लूप करें
process_data(data[i])) // डेटा खंड को स्थिति i पर संसाधित करें
i := i + 1 // संसाधित किए जाने वाले डेटा के अगले भाग पर जाएं
यदि SIZE_OF_DATA का मान गैर-ऋणात्मक, निश्चित और परिमित है, तो लूप अंततः समाप्त हो जाएगा, यह मानते हुए कि process_data भी समाप्त हो जाता है।
कुछ लूपों को मानव निरीक्षण के माध्यम से हमेशा समाप्त या कभी समाप्त नहीं दिखाया जा सकता है। उदाहरण के लिए, निम्नलिखित लूप, सिद्धांत रूप में, कभी नहीं रुकेगा। हालांकि, अंकगणितीय अतिप्रवाह के कारण भौतिक मशीन पर निष्पादित होने पर यह रुक सकता है: या तो अपवाद से निपटने या काउंटर को नकारात्मक मूल्य पर लपेटने और लूप की स्थिति को पूरा करने में सक्षम बनाता है।
मैं: = 1
i = 0 तक लूप करें
मैं: = मैं + 1
समाप्ति विश्लेषण में कोई अज्ञात इनपुट के आधार पर किसी प्रोग्राम के समाप्ति व्यवहार को निर्धारित करने का भी प्रयास कर सकता है। निम्न उदाहरण इस समस्या को दर्शाता है।
मैं: = 1
लूप तक मैं = अज्ञात
मैं: = मैं + 1
यहां लूप कंडीशन को कुछ मान UNKNOWN का उपयोग करके परिभाषित किया गया है, जहां UNKNOWN का मान ज्ञात नहीं है (उदाहरण के लिए प्रोग्राम निष्पादित होने पर उपयोगकर्ता के इनपुट द्वारा परिभाषित)। यहाँ समाप्ति विश्लेषण को UNKNOWN के सभी संभावित मूल्यों को ध्यान में रखना चाहिए और पता लगाना चाहिए कि UNKNOWN = 0 के संभावित मामले में (जैसा कि मूल उदाहरण में है) समापन नहीं दिखाया जा सकता है।
हालांकि, यह निर्धारित करने के लिए कोई सामान्य प्रक्रिया नहीं है कि क्या लूपिंग निर्देशों वाली अभिव्यक्ति बंद हो जाएगी, भले ही मनुष्यों को निरीक्षण का कार्य सौंपा गया हो। इसका सैद्धांतिक कारण हॉल्टिंग प्रॉब्लम की अनिर्णयता है: कुछ एल्गोरिथम मौजूद नहीं हो सकते हैं जो यह निर्धारित करता है कि क्या कोई दिया गया प्रोग्राम बहुत से संगणना चरणों के बाद बंद हो जाता है।
अभ्यास में कोई समाप्ति (या गैर-समाप्ति) दिखाने में विफल रहता है क्योंकि प्रत्येक एल्गोरिदम किसी दिए गए कार्यक्रम से प्रासंगिक जानकारी निकालने में सक्षम होने के तरीकों के सीमित सेट के साथ काम करता है। एक विधि यह देख सकती है कि कुछ लूप स्थिति के संबंध में चर कैसे बदलते हैं (संभवतः उस लूप के लिए समाप्ति दिखा रहा है), अन्य विधियां प्रोग्राम की गणना को कुछ गणितीय निर्माण में बदलने की कोशिश कर सकती हैं और उस पर काम कर सकती हैं, संभवतः समापन व्यवहार के बारे में जानकारी प्राप्त करना इस गणितीय मॉडल के कुछ गुण। लेकिन क्योंकि प्रत्येक विधि केवल (गैर) समाप्ति के कुछ विशिष्ट कारणों को देखने में सक्षम है, ऐसे तरीकों के संयोजन के माध्यम से भी (गैर) समाप्ति के सभी संभावित कारणों को कवर नहीं किया जा सकता है।[citation needed]
पुनरावर्तन (कंप्यूटर विज्ञान) और लूप अभिव्यक्ति में समान हैं; लूप से जुड़ी कोई भी अभिव्यक्ति रिकर्सन का उपयोग करके लिखी जा सकती है, और इसके विपरीत। इस प्रकार पुनरावर्तन समाप्ति भी सामान्य रूप से अनिर्णीत है। सामान्य उपयोग में पाई जाने वाली अधिकांश पुनरावर्ती अभिव्यक्तियाँ (अर्थात पैथोलॉजिकल (गणित) नहीं) को विभिन्न माध्यमों से समाप्त करने के लिए दिखाया जा सकता है, आमतौर पर अभिव्यक्ति की परिभाषा के आधार पर। उदाहरण के तौर पर, नीचे कारख़ाने का फ़ंक्शन के लिए पुनरावर्ती अभिव्यक्ति में फ़ंक्शन तर्क हमेशा 1 से घट जाएगा; प्राकृतिक संख्याओं की सुव्यवस्थित संपत्ति द्वारा, तर्क अंततः 1 तक पहुंच जाएगा और पुनरावर्तन समाप्त हो जाएगा।
फ़ंक्शन फैक्टोरियल (प्राकृतिक संख्या के रूप में तर्क)
अगर तर्क = 0 या तर्क = 1
वापसी मूल्य 1
अन्यथा
वापसी तर्क * भाज्य (तर्क - 1)
आश्रित प्रकार
निर्भर रूप से टाइप की Agda (प्रोग्रामिंग भाषा) और कोक और एग्डा (प्रोग्रामिंग लैंग्वेज) जैसी थ्योरम प्रोविंग सिस्टम में टर्मिनेशन चेक बहुत महत्वपूर्ण है। ये प्रणालियाँ कार्यक्रमों और प्रमाणों के बीच करी-हावर्ड समरूपता का उपयोग करती हैं। आगमनात्मक रूप से परिभाषित डेटा प्रकारों के प्रमाण पारंपरिक रूप से प्रेरण सिद्धांतों का उपयोग करके वर्णित किए गए थे। हालांकि, यह बाद में पाया गया कि पैटर्न मिलान के साथ एक पुनरावर्ती परिभाषित फ़ंक्शन के माध्यम से एक कार्यक्रम का वर्णन सीधे प्रेरण सिद्धांतों का उपयोग करने की तुलना में अधिक प्राकृतिक तरीका है। दुर्भाग्य से, गैर-टर्मिनेटिंग परिभाषाओं की अनुमति देने से प्रकार के सिद्धांतों में तार्किक असंगति होती है[citation needed], यही वजह है कि Agda (प्रोग्रामिंग लैंग्वेज) और Coq में टर्मिनेशन चेकर्स बिल्ट-इन हैं।
आकार प्रकार
आश्रित रूप से टाइप की गई प्रोग्रामिंग भाषाओं में समाप्ति जाँच के तरीकों में से एक आकार प्रकार है। मुख्य विचार उन प्रकारों को एनोटेट करना है जिन पर हम आकार एनोटेशन के साथ पुनरावर्ती कर सकते हैं और केवल छोटे तर्कों पर पुनरावर्ती कॉल की अनुमति दे सकते हैं। Agda (प्रोग्रामिंग भाषा) में सिंटैक्टिक एक्सटेंशन के रूप में आकार प्रकार लागू किए जाते हैं।
वर्तमान शोध
कई शोध दल हैं जो नए तरीकों पर काम करते हैं जो समाप्ति (गैर) दिखा सकते हैं। कई शोधकर्ता इन विधियों को कार्यक्रमों में शामिल करते हैं[2] जो स्वचालित रूप से समाप्ति व्यवहार का विश्लेषण करने का प्रयास करते हैं (इसलिए मानव संपर्क के बिना)। अनुसंधान का एक सतत पहलू वास्तविक विश्व प्रोग्रामिंग भाषाओं में लिखे गए कार्यक्रमों के समाप्ति व्यवहार का विश्लेषण करने के लिए मौजूदा तरीकों का उपयोग करने की अनुमति देना है। हास्केल (प्रोग्रामिंग भाषा), मरकरी (प्रोग्रामिंग भाषा) और प्रोलॉग जैसी घोषणात्मक भाषाओं के लिए, कई परिणाम मौजूद हैं[3][4][5] (मुख्य रूप से इन भाषाओं की मजबूत गणितीय पृष्ठभूमि के कारण)। अनुसंधान समुदाय सी और जावा जैसी अनिवार्य भाषाओं में लिखे गए कार्यक्रमों के समाप्ति व्यवहार का विश्लेषण करने के लिए नए तरीकों पर भी काम करता है।
हॉल्टिंग प्रॉब्लम की अनिश्चितता के कारण इस क्षेत्र में अनुसंधान पूर्णता तक नहीं पहुँच सकता है। कोई हमेशा नए तरीकों के बारे में सोच सकता है जो समाप्ति के नए (जटिल) कारण ढूंढता है।
यह भी देखें
- जटिलता विश्लेषण - समाप्त करने के लिए आवश्यक समय का अनुमान लगाने की समस्या
- लूप वेरिएंट
- कुल कार्यात्मक प्रोग्रामिंग - एक प्रोग्रामिंग प्रतिमान जो कार्यक्रमों की श्रेणी को उन तक सीमित करता है जो सिद्ध रूप से समाप्त हो रहे हैं
- वाल्थर रिकर्सन
संदर्भ
- ↑ Rogers, Jr., Hartley (1988). पुनरावर्ती कार्यों और प्रभावी संगणनीयता का सिद्धांत।. Cambridge (MA), London (England): The MIT Press. p. 476. ISBN 0-262-68052-1.
- ↑ Tools at termination-portal.org
- ↑ Giesl, J. and Swiderski, S. and Schneider-Kamp, P. and Thiemann, R. Pfenning, F. (ed.). Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages (invited lecture) (postscript). Term Rewriting and Applications, 17th Int. Conf., RTA-06. LNCS. Vol. 4098. pp. 297–312. (link: springerlink.com).
{{cite conference}}: CS1 maint: uses authors parameter (link) - ↑ Compiler options for termination analysis in Mercury
- ↑ http://verify.rwth-aachen.de/giesl/papers/lopstr07-distribute.pdf[bare URL PDF]
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
