सार पुनर्लेखन प्रणाली

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

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

परिभाषा

एक अमूर्त ह्रासीकरण प्रणाली (एआरएस) वस्तुओं और नियमों के एक सेट को निर्दिष्ट करने के बारे में सबसे सामान्य (एकआयामी) धारणा है जिसे उन्हें बदलने के लिए लागू किया जा सकता है। हाल ही में, लेखक अमूर्त पुनर्लेखन प्रणाली शब्द का भी उपयोग करते हैं। (पुनर्लेखन के अतिरिक्त यहां शब्द कटौती के लिए प्राथमिकता एआरएस के विशिष्टीकरण वाले प्रणाली के नामों में पुनर्लेखन के समान उपयोग से विचलन का गठन करती है। क्योंकि ह्रासीकरण शब्द अधिक विशिष्ट प्रणालियों के नामों में प्रकट नहीं होता है, पुराने पाठों में ह्रासीकरण प्रणाली एआरएस का पर्याय है।) एआरएस एक सेट (गणित) है, जिसके तत्वों को सामान्यत: ऑब्जेक्ट कहा जाता है, पर एक द्विआधारी वर्णन के साथ, पारंपरिक रूप से → दर्शाया जाता है, और 'ह्रासीकरण वर्णन' कहा जाता है, वर्णन को फिर से लिखेंया बस ह्रासीकरण.कटौती का उपयोग करने वाली यह (प्रमाणित) शब्दावली थोड़ी भ्रामक है, क्योंकि वर्णन आवश्यक रूप से वस्तुओं के कुछ माप को कम नहीं कर रहा है। कुछ संदर्भों में नियमों के कुछ उपसमुच्चयों के बीच अंतर करना फायदेमंद हो सकता है, अर्थात ह्रासीकरण वर्णन के कुछ उपसमुच्चय →, उदाहरण के लिए संपूर्ण ह्रासीकरण वर्णन में साहचर्यता और क्रमविनिमेयता नियम सम्मलित हो सकते हैं। परिणाम स्वरुप, कुछ लेखक ह्रासीकरण वर्णन को परिभाषित करते हैं → कुछ वर्णनों के अनुक्रमित संघ के रूप में; उदाहरण के लिए यदि ${\rightarrow _{1}\cup \rightarrow _{2}}={\rightarrow }$, प्रयुक्त संकेतन (ए, →) है₁, →₂) है।

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

उदाहरण 1

मान लीजिए कि वस्तुओं का सेट T = {a, b, c} है और द्विआधारी वर्णन नियम a → b, b → a, a → c, और b → c द्वारा दिया गया है। ध्यान दें कि c प्राप्त करने के लिए इन नियमों को a और b दोनों पर लागू किया जा सकता है। इसके अतिरिक्त, इसे और अधिक परिवर्तित करने के लिए c पर कुछ भी लागू नहीं किया जा सकता है। ऐसी गुण स्पष्ट रूप से महत्वपूर्ण है।

बुनियादी धारणाएँ

पहले कुछ बुनियादी धारणाओं और संकेतनों को परिभाषित करें।

• ${\stackrel {+}{\rightarrow }}$ का सकर्मक समापन है $\rightarrow$.
• ${\stackrel {*}{\rightarrow }}$ का प्रतिवर्ती सकर्मक समापन है $\rightarrow$, अर्थात का सकर्मक समापन $(\rightarrow )\cup (=)$, जहां = पहचान वर्णन है. समान रूप से, ${\stackrel {*}{\rightarrow }}$ सबसे छोटा पूर्व आदेश युक्त है $\rightarrow$.
• $\leftrightarrow$ का सममित समापन है $\rightarrow$, वह है, $(\rightarrow )\cup (\rightarrow )^{-1}$ अर्थात वर्णन का मिलन → इसके विपरीत वर्णन के साथ।
• ${\stackrel {*}{\leftrightarrow }}$ का प्रतिवर्ती सकर्मक सममित समापन है $\rightarrow$, अर्थात का सकर्मक समापन $(\leftrightarrow )\cup (=)$. समान रूप से, ${\stackrel {*}{\leftrightarrow }}$ सबसे छोटा समतुल्य वर्णन है $\rightarrow$.

सामान्य रूप

Main article: सामान्य रूप (अमूर्त पुनर्लेखन)

A में कोई वस्तु x को आबिंदुकोची कहा जाता है यदि A और में कोई अन्य y सम्मलित हो $x\rightarrow y$; अन्यथा इसे अनाबिन्दुकोची या सामान्य रूप कहा जाता है। एक वस्तु y को x का सामान्य रूप कहा जाता है यदि $x{\stackrel {*}{\rightarrow }}y$ और y अपरिवर्तनीय है. यदि x का एक अद्वितीय सामान्य रूप है, तो इसे सामान्यत: इससे दर्शाया जाता है $x\downarrow$. उपरोक्त उदाहरण 1 में, c एक सामान्य रूप है, और $c=a\downarrow =b\downarrow$. यदि प्रत्येक वस्तु का कम से कम एक सामान्य रूप है, तो एआरएस को सामान्यीकरण कहा जाता है।

जुड़ने की योग्यता

सामान्य रूपों के अस्तित्व की तुलना में एक वर्णनित, लेकिन कमजोर धारणा यह है कि दो वस्तुएं जुड़ने योग्य हैं: x और y को जुड़ने योग्य कहा जाता है यदि गुण के साथ कुछ z सम्मलित है $x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y$. इस परिभाषा से, यह स्पष्ट है कि कोई जुड़ाव वर्णन को इस प्रकार परिभाषित कर सकता है ${\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}$, जहाँ $\circ$ वर्णनों की संरचना है. जुड़ाव को सामान्यत:, कुछ हद तक भ्रामक रूप से, साथ भी दर्शाया जाता है $\downarrow$, लेकिन इस अंकन में नीचे का तीर एक द्विआधारी वर्णन है, अर्थात हम लिखते हैं $x\mathbin {\downarrow } y$ यदि x और y जुड़ने योग्य हैं।

चर्च-रोसेर गुण और संगामी की धारणाएं

Main article: संगम (अमूर्त पुनर्लेखन)

ऐसा कहा जाता है कि एक एआरएस के पास चर्च-रोसेर गुण होती है यदि और केवल यदि $x{\stackrel {*}{\leftrightarrow }}y$ तात्पर्य $x\mathbin {\downarrow } y$ सभी वस्तुओं x, y के लिए है। समान रूप से, चर्च-रोसेर गुण का अर्थ है कि प्रतिवर्ती सकर्मक सममित समापन जुड़ाव वर्णन में निहित है। अलोंजो चर्च और जे. बार्कले रोसेर ने 1936 में सिद्ध किया कि लैम्ब्डा कैलकुलस में यह गुण है; इसलिए गुण का नाम. चर्च-रोसेर गुण के साथ एआरएस में शब्द समस्या को एक साधारण आनुक्रमिक की खोज तक कम किया जा सकता है। चर्च-रोसेर प्रणाली में, किसी वस्तु का अधिकतम एक सामान्य रूप होता है; अर्थात्, यदि किसी वस्तु का अस्तित्व है तो उसका सामान्य रूप अद्वितीय है, लेकिन यह अस्तित्व में नहीं भी हो सकता है।

चर्च-रोसेर की तुलना में सरल विभिन्न गुण, इसके समतुल्य हैं। इन समकक्ष गुणों का अस्तित्व किसी को यह सिद्ध करने की अनुमति देता है कि एक प्रणाली चर्च-रोसेर है जिसमें कम काम होता है। इसके अतिरिक्त, संगामी की धारणाओं को किसी विशेष वस्तु के गुणों के रूप में परिभाषित किया जा सकता है, जो कि चर्च-रोसेर के लिए संभव नहीं है। एक एआरएस $(A,\rightarrow )$ बताया गया है।

• संगामी यदि और केवल यदि A में सभी w, x, और y के लिए, $x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y$ तात्पर्य $x\mathbin {\downarrow } y$. मोटे तौर पर, संगामी कहता है कि इससे कोई फर्क नहीं पड़ता कि दो रास्ते एक सामान्य पूर्वज (डब्ल्यू) से कैसे अलग होते हैं, रास्ते किसी साधारण आनुक्रमिक से जुड़ रहे हैं। इस धारणा को किसी विशेष वस्तु w की गुण के रूप में परिष्कृत किया जा सकता है, और यदि इसके सभी तत्व मिले हुए हैं तो प्रणाली को संगामी कहा जाता है।
• अर्ध-संगामी यदि और केवल यदि A में सभी w, x, और y के लिए, $x\leftarrow w{\stackrel {*}{\rightarrow }}y$ तात्पर्य $x\mathbin {\downarrow } y$. यह संगामी से w से x तक एकल चरण में ह्रासीकरण से भिन्न है।
• स्थानीय रूप से संगामी यदि और केवल यदि A में सभी w, x, और y के लिए, $x\leftarrow w\rightarrow y$ तात्पर्य $x\mathbin {\downarrow } y$. इस गुण को कभी-कभी कमजोर संगामी भी कहा जाता है।

स्थानीय रूप से संगामी पुनर्लेखन प्रणाली का उदाहरण जिसमें चर्च-रोसेर गुण नहीं है

प्रमेय. एआरएस के लिए निम्नलिखित तीन स्थितियाँ समतुल्य हैं: (i) इसमें चर्च-रोसेर गुण है, (ii) यह संगामी है, (iii) यह अर्ध-संगामी है।

उपसिद्धान्त. एक संगामी एआरएस में यदि $x{\stackrel {*}{\leftrightarrow }}y$ है तब

• यदि x और y दोनों सामान्य रूप हैं, तो x = y.
• यदि y एक सामान्य रूप है, तो $x{\stackrel {*}{\rightarrow }}y$.

इन समानताओं के कारण, साहित्य में परिभाषाओं में काफी भिन्नता पाई जाती है। उदाहरण के लिए, टेरेसी में चर्च-रोसेर गुण और संगामी को यहां प्रस्तुत संगामी की परिभाषा के पर्यायवाची और समान के रूप में परिभाषित किया गया है; चर्च-रोसेर जैसा कि यहां परिभाषित है, अज्ञात है, लेकिन इसे समकक्ष गुण के रूप में दिया गया है; अन्य ग्रंथों से यह विचलन जानबूझकर किया गया है। उपरोक्त परिणाम के कारण, कोई व्यक्ति x के सामान्य रूप y को उस गुण के साथ एक अघुलनशील y के रूप में परिभाषित कर सकता है $x{\stackrel {*}{\leftrightarrow }}y$. किताब और ओटो में पाई गई यह परिभाषा, संगामी प्रणाली में यहां दी गई सामान्य परिभाषा के बराबर है, लेकिन गैर-संगामी एआरएस में यह अधिक समावेशी है।

दूसरी ओर, स्थानीय संगामी इस खंड में दी गई संगामी की अन्य धारणाओं के बराबर नहीं है, लेकिन यह संगामी से बिल्कुल कमजोर है। विशिष्ट प्रति उदाहरण है $\{b\rightarrow c,c\rightarrow b,b\rightarrow a,c\rightarrow d\}$, जो स्थानीय रूप से संगामी है लेकिन संगामी नहीं है (सीएफ. चित्र)।

अवसान और अभिसरण

यदि कोई अनंत श्रृंखला नहीं है तो एक अमूर्त पुनर्लेखन प्रणाली को अवसान या नोथेरियन कहा जाता है $x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots$. (यह सिर्फ इतना कह रहा है कि पुनर्लेखन वर्णन एक नोथेरियन वर्णन है।) एक अवसान एआरएस में, प्रत्येक वस्तु का कम से कम एक सामान्य रूप होता है, इस प्रकार यह सामान्य हो रहा है। इसका उलट सत्य नहीं है। उदाहरण के लिए उदाहरण 1 में, एक अनंत पुनर्लेखन श्रृंखला है $a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots$चूंकि प्रणाली सामान्य हो रही है। एक संगामी और अवसान एआरएस को कैनोनिकल कहा जाता है, या अभिसारी. अभिसरण एआरएस में, प्रत्येक वस्तु का एक अद्वितीय सामान्य रूप होता है। लेकिन प्रत्येक तत्व के लिए एक अद्वितीय सामान्य अस्तित्व के लिए प्रणाली का संगामी और सामान्य होना पर्याप्त है, जैसा कि उदाहरण 1 में देखा गया है।

प्रमेय (न्यूमैन की लेम्मा): एक अवसान एआरएस संगामी है यदि और केवल यदि यह स्थानीय रूप से संगामी है।

न्यूमैन द्वारा इस परिणाम का मूल 1942 प्रमाण बल्कि जटिल था। 1980 तक ऐसा नहीं हुआ था कि ह्यूट ने इस तथ्य का फायदा उठाते हुए एक बहुत ही सरल प्रमाण प्रकाशित किया था कि कब $\rightarrow$ समाप्त हो रहा है हम अच्छी तरह से स्थापित प्रेरण लागू कर सकते हैं।

यह भी देखें

• शब्द समस्या (गणित) - विशेष रूप से अमूर्त पुनर्लेखन प्रणाली पर अनुभाग

संदर्भ

• Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203. A textbook suitable for undergraduates.
• Nachum Dershowitz and Jean-Pierre Jouannaud Rewrite Systems, Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320. The preprint of this chapter is freely available from the authors, but it misses the figures.
• Book, Ronald V.; Otto, Friedrich (1993). "1, "Abstract reduction systems"". String-rewriting Systems. Springer. ISBN 0-387-97965-4.
• Marc Bezem; Jan Willem Klop; Roel de Vrijer; "Terese" (2003). "1". Term rewriting systems. Cambridge University Press. ISBN 0-521-39115-6. This is a comprehensive monograph. It uses, however, a fair deal of notations and definitions not commonly encountered elsewhere. For instance the Church–Rosser property is defined to be identical with confluence.
• Harrison, John (2009). "4 "Equality"". Handbook of Practical Logic and Automated Reasoning Cambridge University Press. ISBN 978-0-521-89957-4. Abstract rewriting from the practical perspective of solving problems in equational logic.
• Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797–821. Huet's paper established many of the modern concepts, results and notations.
• Sinyor, J.; "The 3x+1 Problem as a String Rewriting System", International Journal of Mathematics and Mathematical Sciences, Volume 2010 (2010), Article ID 458563, 6 pages.
• Duffy, David A. (1991). Principles of Automated Theorem Proving. Wiley.
• Church, Alonzo; Rosser, J. B. (1936). "Some Properties of Conversion". Transactions of the American Mathematical Society. 39 (3): 472–482. doi:10.2307/1989762. ISSN 0002-9947. JSTOR 1989762.