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

गणितीय तर्क और सैद्धांतिक कंप्यूटर विज्ञान में, एक अमूर्त पुनर्लेखन प्रणाली (भी (अमूर्त) कमी प्रणाली या अमूर्त पुनर्लेखन प्रणाली; संक्षिप्त एआरएस) एक औपचारिकता (गणित) है जो पुनर्लेखन प्रणालियों की सर्वोत्कृष्ट धारणा और गुणों को पकड़ती है। अपने सरलतम रूप में, एआरएस बस एक सेट (गणित) (वस्तुओं का) है जो एक द्विआधारी संबंध के साथ है, जिसे पारंपरिक रूप से दर्शाया जाता है $\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: Normal form (abstract rewriting)

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: Confluence (abstract rewriting)

ऐसा कहा जाता है कि एक एआरएस के पास चर्च-रोसेर संपत्ति होती है यदि और केवल यदि $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 तक एकल चरण में कमी से भिन्न है।
• स्थानीय रूप से संगम यदि और केवल यदि ए में सभी डब्ल्यू, एक्स और वाई के लिए, $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$हालांकि सिस्टम सामान्य हो रहा है। एक संगम और समाप्ति ARS को कैनोनिकल कहा जाता है, या अभिसारी. अभिसरण एआरएस में, प्रत्येक वस्तु का एक अद्वितीय सामान्य रूप होता है। लेकिन प्रत्येक तत्व के लिए एक अद्वितीय सामान्य अस्तित्व के लिए सिस्टम का संगम और सामान्य होना पर्याप्त है, जैसा कि उदाहरण 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.