संप्रवाह (सार पुनर्लेखन)

चित्र.1: संगम नाम संगम से प्रेरित है, जिसका अर्थ है दो जल निकायों का मिलन।

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

प्रेरक उदाहरण

प्रारंभिक अंकगणित के सामान्य नियम एक अमूर्त पुनर्लेखन प्रणाली बनाते हैं।

उदाहरण के लिए, अभिव्यक्ति (11 + 9) × (2 + 4) का मूल्यांकन बाएं या दाएं कोष्ठक से शुरू करके किया जा सकता है; हालाँकि, दोनों ही मामलों में अंततः एक ही परिणाम प्राप्त होता है। यदि प्रत्येक अंकगणितीय अभिव्यक्ति कटौती रणनीति की परवाह किए बिना एक ही परिणाम का मूल्यांकन करती है, तो अंकगणितीय पुनर्लेखन प्रणाली को ग्राउंड-कंफ्लुएंट कहा जाता है। पुनर्लेखन प्रणाली के विवरण के आधार पर अंकगणितीय पुनर्लेखन प्रणालियाँ संगम या केवल जमीनी-संगम हो सकती हैं।^[1] प्रत्येक Group_(गणित) तत्व के Group_(mathematics)#Definition के व्युत्क्रम के बराबर होने के निम्नलिखित प्रमाण से एक दूसरा, अधिक सारगर्भित उदाहरण प्राप्त किया जाता है:^[2]

Group axioms
A1	1 ⋅ a	= a
A2	a⁻¹ ⋅ a	= 1
A3	(a ⋅ b) ⋅ c	= a ⋅ (b ⋅ c)

Proof of R4: a⁻¹⋅(a⋅b) = b
	a⁻¹ ⋅ (a ⋅ b)
=	(a⁻¹ ⋅ a) ⋅ b	by A3(r)
=	1 ⋅ b	by A2
=	b	by A1

Proof of R6: (a⁻¹)⁻¹ ⋅ 1 = a
	(a⁻¹)⁻¹ ⋅ 1
=	(a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ a)	by A2(r)
=	a	by R4

Proof of **R10**: (a⁻¹)⁻¹ ⋅ b = a ⋅ b
	(a⁻¹)⁻¹ ⋅ b
=	(a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ (a ⋅ b))	by R4(r)
=	a ⋅ b	by R4

Proof of **R11**: a ⋅ 1 = a
	a ⋅ 1
=	(a⁻¹)⁻¹ ⋅ 1	by R10(r)
=	a	by R6

Proof of **R12**: (a⁻¹)⁻¹ = a
	(a⁻¹)⁻¹
=	(a⁻¹)⁻¹ ⋅ 1	by R11(r)
=	a	by R6

यह प्रमाण दिए गए समूह स्वयंसिद्ध A1-A3 से शुरू होता है, और पांच प्रस्ताव R4, R6, R10, R11 और R12 स्थापित करता है, उनमें से प्रत्येक कुछ पहले वाले का उपयोग करता है, और R12 मुख्य प्रमेय है। कुछ प्रमाणों के लिए गैर-स्पष्ट, या यहां तक कि रचनात्मक, चरणों की आवश्यकता होती है, जैसे स्वयंसिद्ध A2 को उल्टा लागू करना, जिससे 1 को फिर से लिखना⁻¹ ⋅ a R6 के प्रमाण के पहले चरण में। शब्द पुनर्लेखन के सिद्धांत को विकसित करने की ऐतिहासिक प्रेरणाओं में से एक ऐसे कदमों की आवश्यकता से बचना था, जिन्हें एक अनुभवहीन मानव के लिए खोजना मुश्किल है, कंप्यूटर प्रोग्राम की तो बात ही छोड़ दें।^{[citation needed]}.

यदि कोई टर्म_रीराइटिंग#टर्म_रीराइटिंग_सिस्टम संगम और रीराइटिंग#टर्मिनेशन है, तो दो अभिव्यक्तियों (जिसे शब्द (तर्क) भी कहा जाता है) एस और टी के बीच समानता साबित करने के लिए एक सीधी विधि मौजूद है। : एस से शुरू करते हुए समानताएं लागू करें^{[note 1]} जब तक संभव हो बाएँ से दाएँ, अंततः एक शब्द s' प्राप्त करना। इसी प्रकार t से एक पद t' प्राप्त करें। यदि दोनों पद s′ और t′ वस्तुतः सहमत हैं, तो s और t (आश्चर्यजनक रूप से नहीं) समान साबित होते हैं। इससे भी महत्वपूर्ण बात यह है कि यदि वे असहमत हैं, तो s और t बराबर नहीं हो सकते। अर्थात्, किन्हीं दो पदों s और t को बिल्कुल समान सिद्ध किया जा सकता है, ऐसा उस विधि द्वारा किया जा सकता है।

उस विधि की सफलता एक निश्चित परिष्कृत क्रम पर निर्भर नहीं करती है जिसमें पुनर्लेखन नियमों को लागू करना है, क्योंकि 'संगम' यह सुनिश्चित करता है कि नियम अनुप्रयोगों का कोई भी अनुक्रम अंततः एक ही परिणाम देगा (जबकि समाप्ति संपत्ति यह सुनिश्चित करती है कि कोई भी अनुक्रम अंततः पहुंचेगा) बिल्कुल अंत)। इसलिए, यदि कुछ समीकरण सिद्धांत के लिए एक संगम और समाप्ति शब्द पुनर्लेखन प्रणाली प्रदान की जा सकती है,^{[note 2]} समानता शब्द का प्रमाण प्रस्तुत करने के लिए थोड़ी सी भी रचनात्मकता की आवश्यकता नहीं है; इसलिए वह कार्य कंप्यूटर प्रोग्राम के लिए उत्तरदायी हो जाता है। आधुनिक दृष्टिकोण शब्द पुनर्लेखन प्रणालियों के बजाय अधिक सामान्य अमूर्त पुनर्लेखन प्रणालियों को संभालते हैं; उत्तरार्द्ध पूर्व का एक विशेष मामला है।

सामान्य मामला और सिद्धांत

चित्र.2: इस चित्र में,

a

दोनों को कम कर देता है

b

या

c

शून्य या अधिक पुनर्लेखन चरणों में (तारांकन द्वारा चिह्नित)। पुनर्लेखन संबंध को संगमित करने के लिए, दोनों को बदले में कुछ सामान्य तक कम करना होगा

d

.

एक पुनर्लेखन प्रणाली को एक निर्देशित ग्राफ के रूप में व्यक्त किया जा सकता है जिसमें नोड्स अभिव्यक्तियों का प्रतिनिधित्व करते हैं और किनारे पुनर्लेखन का प्रतिनिधित्व करते हैं। इसलिए, उदाहरण के लिए, यदि अभिव्यक्ति a को b में दोबारा लिखा जा सकता है, तो हम कहते हैं कि b, a का एक छोटा रूप है (वैकल्पिक रूप से, a, b को कम करता है, या a, b का विस्तार है)। इसे तीर संकेतन का उपयोग करके दर्शाया गया है; a → b इंगित करता है कि a, b में कम हो जाता है। सहज रूप से, इसका मतलब है कि संबंधित ग्राफ़ में ए से बी तक एक निर्देशित किनारा है।

यदि दो ग्राफ नोड्स c और d के बीच एक पथ है, तो यह एक कमी अनुक्रम बनाता है। इसलिए, उदाहरण के लिए, यदि c → c′ → c′′ → ... → d′ → d, तो हम c लिख सकते हैं ∗→ डी, सी से डी तक कमी अनुक्रम के अस्तित्व को दर्शाता है। औपचारिक रूप से, ∗→ → का क्लोजर (गणित)#बाइनरी रिलेशन क्लोजर|रिफ्लेक्सिव-ट्रांजिटिव क्लोजर है। पिछले पैराग्राफ से उदाहरण का उपयोग करते हुए, हमारे पास (11+9)×(2+4) → 20×(2+4) और 20×(2+4) → 20×6 है, इसलिए (11+9)×( 2+4) ∗→ 20×6.

इसकी स्थापना से संगम को इस प्रकार परिभाषित किया जा सकता है। a ∈ S को संगम माना जाता है यदि सभी जोड़ियों के लिए b, c ∈ S ऐसा हो कि a ∗→ बी और ए ∗→ सी, बी के साथ एक डी ∈ एस मौजूद है ∗→डी और सी ∗→ डी (निरूपित) $b\mathbin {\downarrow } c$ ). यदि प्रत्येक a ∈ S संगम है, तो हम कहते हैं कि → संगम है। दाईं ओर दिखाए गए चित्र के आकार के बाद, इस संपत्ति को कभी-कभी हीरे की संपत्ति भी कहा जाता है। कुछ लेखक हर जगह एकल कटौती के साथ आरेख के एक प्रकार के लिए हीरा संपत्ति शब्द को आरक्षित रखते हैं; अर्थात्, जब भी a → b और a → c, वहाँ a d का अस्तित्व इस प्रकार होना चाहिए कि b → d और c → d। सिंगल-रिडक्शन वेरिएंट मल्टी-रिडक्शन वेरिएंट की तुलना में अधिक मजबूत है।

भूमि संगम

एक शब्द पुनर्लेखन प्रणाली ग्राउंड कंफ्लुएंट होती है यदि प्रत्येक जमीनी अवधि कंफ्लुएंट हो, अर्थात प्रत्येक शब्द बिना चर के हो।^[3]

स्थानीय संगम

चित्र.3: चक्रीय, स्थानीय रूप से संगमित, लेकिन विश्व स्तर पर संगमित पुनर्लेखन प्रणाली नहीं^[4]

चित्र.4: अनंत गैर-चक्रीय, स्थानीय रूप से-संगम, लेकिन विश्व स्तर पर मिश्रित पुनर्लेखन प्रणाली नहीं^[4]

एक तत्व a ∈ S को स्थानीय रूप से (या कमजोर रूप से) संगम कहा जाता है यदि सभी b, c ∈ S के लिए a → b और a → c के साथ d ∈ S मौजूद हो ∗→डी और सी ∗→ डी। यदि प्रत्येक ∈ S स्थानीय रूप से संगम है, तो → को स्थानीय रूप से (या कमजोर रूप से) संगम कहा जाता है, या कमजोर चर्च-रोसेर संपत्ति वाला कहा जाता है। यह संगम से भिन्न है क्योंकि बी और सी को एक चरण में ए से कम किया जाना चाहिए। इसके अनुरूप, संगम को कभी-कभी वैश्विक संगम भी कहा जाता है।

रिश्ता ∗→, कटौती अनुक्रमों के लिए एक संकेतन के रूप में पेश किया गया, इसे अपने आप में एक पुनर्लेखन प्रणाली के रूप में देखा जा सकता है, जिसका संबंध → का क्लोजर_(गणित)#बाइनरी रिलेशन क्लोजर|रिफ्लेक्टिव-ट्रांजिटिव क्लोजर है। चूँकि कमी अनुक्रमों का एक क्रम फिर से एक कमी अनुक्रम है (या, समतुल्य रूप से, चूंकि रिफ्लेक्सिव-ट्रांजिटिव क्लोजर बनाना निष्क्रियता#यूनरी ऑपरेशन है), ∗∗→ = ∗→. इससे यह निष्कर्ष निकलता है कि → संगम है यदि और केवल यदि ∗→ स्थानीय रूप से संगम है।

एक पुनर्लेखन प्रणाली (वैश्विक स्तर पर) मिश्रित हुए बिना भी स्थानीय रूप से संगमित हो सकती है। उदाहरण चित्र 3 और 4 में दिखाए गए हैं। हालाँकि, न्यूमैन की लेम्मा बताती है कि यदि स्थानीय रूप से संगम पुनर्लेखन प्रणाली में कोई अनंत कमी अनुक्रम नहीं है (जिस स्थिति में इसे समाप्त या दृढ़ता से सामान्यीकृत कहा जाता है), तो यह विश्व स्तर पर संगम है।

चर्च-रोसेर संपत्ति

ऐसा कहा जाता है कि एक पुनर्लेखन प्रणाली के पास चर्च-रोसेर संपत्ति होती है यदि और केवल यदि $x{\stackrel {*}{\leftrightarrow }}y$ तात्पर्य $x\mathbin {\downarrow } y$ सभी वस्तुओं x, y के लिए। अलोंजो चर्च और जे. बार्कले रोसेर ने 1936 में साबित किया कि लैम्ब्डा कैलकुलस में यह गुण है;^[5] इसलिए संपत्ति का नाम.^[6] (यह तथ्य कि लैम्ब्डा कैलकुलस में यह संपत्ति है, इसे चर्च-रोसेर प्रमेय के रूप में भी जाना जाता है।) चर्च-रोसेर संपत्ति के साथ एक पुनर्लेखन प्रणाली में शब्द समस्या को एक सामान्य उत्तराधिकारी की खोज तक कम किया जा सकता है। चर्च-रोसेर प्रणाली में, एक वस्तु का अधिकतम एक सामान्य रूप (अमूर्त पुनर्लेखन) होता है; अर्थात् किसी वस्तु का सामान्य रूप यदि अस्तित्व में है तो अद्वितीय है, लेकिन यह अस्तित्व में नहीं भी हो सकता है। उदाहरण के लिए लैम्ब्डा कैलकुलस में, अभिव्यक्ति (λx.xx)(λx.xx) का कोई सामान्य रूप नहीं है क्योंकि β-कटौती (λx.xx)(λx.xx) → (λx.xx) का एक अनंत अनुक्रम मौजूद है। (λx.xx) → ...^[7] एक पुनर्लेखन प्रणाली के पास चर्च-रोसेर संपत्ति होती है यदि और केवल यदि यह संगम है।^[8] इस समानता के कारण, साहित्य में परिभाषाओं में काफी भिन्नता पाई जाती है। उदाहरण के लिए, टेरेसी में चर्च-रोसेर संपत्ति और संगम को यहां प्रस्तुत संगम की परिभाषा के पर्यायवाची और समान के रूप में परिभाषित किया गया है; चर्च-रोसेर जैसा कि यहां परिभाषित है, अज्ञात है, लेकिन इसे समकक्ष संपत्ति के रूप में दिया गया है; अन्य ग्रंथों से यह विचलन जानबूझकर किया गया है।^[9]

अर्ध-संगम

स्थानीय संगम की परिभाषा वैश्विक संगम से भिन्न है जिसमें केवल एक पुनर्लेखन चरण में दिए गए तत्व से प्राप्त तत्वों पर विचार किया जाता है। एक चरण में एक तत्व तक पहुंचने और एक मनमाना अनुक्रम द्वारा पहुंचे दूसरे तत्व पर विचार करके, हम अर्ध-संगम की मध्यवर्ती अवधारणा पर पहुंचते हैं: ए ∈ एस को अर्ध-संगम कहा जाता है यदि सभी बी के लिए, सी ∈ एस → के साथ बी और ए ∗→ c में b के साथ d ∈ S मौजूद है ∗→डी और सी ∗→ डी; यदि प्रत्येक a ∈ S अर्ध-संगम है, तो हम कहते हैं कि → अर्ध-संगम है।

एक अर्ध-संगम तत्व को मिला हुआ होने की आवश्यकता नहीं है, लेकिन एक अर्ध-संगम पुनर्लेखन प्रणाली आवश्यक रूप से संगम है, और एक संगम प्रणाली तुच्छ रूप से अर्ध-संगम है।

प्रबल संगम

मजबूत संगम स्थानीय संगम पर एक और भिन्नता है जो हमें यह निष्कर्ष निकालने की अनुमति देता है कि एक पुनर्लेखन प्रणाली विश्व स्तर पर संगम है। एक तत्व a ∈ S को दृढ़ता से मिला हुआ कहा जाता है यदि सभी b, c ∈ S के लिए a → b और a → c के साथ d ∈ S मौजूद हो ∗→ d और या तो c → d या c = d; यदि प्रत्येक a ∈ S दृढ़ता से मिला हुआ है, तो हम कहते हैं कि → दृढ़ता से मिला हुआ है।

एक संगम तत्व को दृढ़ता से मिला हुआ होने की आवश्यकता नहीं है, लेकिन एक दृढ़ता से मिला हुआ पुनर्लेखन प्रणाली आवश्यक रूप से संगम है।

संगम प्रणालियों के उदाहरण

बहुपद मॉड्यूलो का न्यूनीकरण एक आदर्श (रिंग सिद्धांत) एक संगम पुनर्लेखन प्रणाली है, बशर्ते कोई ग्रोबनर आधार के साथ काम करे।
मात्सुमोतो का प्रमेय (समूह सिद्धांत)|मात्सुमोतो का प्रमेय ब्रैड संबंधों के संगम से आता है।
λ-शब्दों की β-कमी चर्च-रोसेर प्रमेय से मिलती है।

यह भी देखें

अभिसरण (तर्क)
क्रिटिकल जोड़ी (तर्क)
सामान्य रूप (सार पुनर्लेखन)

↑ then called rewrite rules to emphasize their left-to-right orientation
↑ The Knuth–Bendix completion algorithm can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown here, with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to the term (a⁻¹)⁻¹⋅1 to obtain the term a; no other rules are applicable.

संदर्भ

Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998

↑ Walters, H.R.; Zantema, H. (Oct 1994). "पूर्णांक अंकगणित के लिए सिस्टम को फिर से लिखें" (PDF). Utrecht University.
↑ K. H. Bläsius and H.-J. Bürckert, ed. (1992). कटौती प्रणाली. Oldenbourg. p. 291. Here: p.134; axiom and proposition names follow the original text
↑ Robinson, Alan J. A.; Voronkov, Andrei (5 July 2001). स्वचालित तर्क की पुस्तिका (in English). Gulf Professional Publishing. p. 560. ISBN 978-0-444-82949-8.
↑ ^4.0 ^4.1 N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). औपचारिक मॉडल और शब्दार्थ. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. ISBN 0-444-88074-7. Here: p.268, Fig.2a+b.
↑ Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936
↑ Baader and Nipkow, p. 9
↑ Cooper, S. B. (2004). कम्प्यूटेबिलिटी सिद्धांत. Boca Raton: Chapman & Hall/CRC. p. 184. ISBN 1584882379.
↑ Baader and Nipkow, p. 11
↑ Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003, ISBN 0-521-39115-6, Here: p.11

बाहरी संबंध

Weisstein, Eric W. "Confluent". MathWorld.

[3] then called rewrite rules to emphasize their left-to-right orientation

[4] The Knuth–Bendix completion algorithm can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown here, with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to the term (a⁻¹)⁻¹⋅1 to obtain the term a; no other rules are applicable.

[1] Walters, H.R.; Zantema, H. (Oct 1994). "पूर्णांक अंकगणित के लिए सिस्टम को फिर से लिखें" (PDF). Utrecht University.

[2] K. H. Bläsius and H.-J. Bürckert, ed. (1992). कटौती प्रणाली. Oldenbourg. p. 291. Here: p.134; axiom and proposition names follow the original text

[5] Robinson, Alan J. A.; Voronkov, Andrei (5 July 2001). स्वचालित तर्क की पुस्तिका (in English). Gulf Professional Publishing. p. 560. ISBN 978-0-444-82949-8.

[Dershowitz.Jouannaud.1990.Fig2-6] 4.0 ^4.1 N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). औपचारिक मॉडल और शब्दार्थ. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. ISBN 0-444-88074-7. Here: p.268, Fig.2a+b.

[7] Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936

[8] Baader and Nipkow, p. 9

[9] Cooper, S. B. (2004). कम्प्यूटेबिलिटी सिद्धांत. Boca Raton: Chapman & Hall/CRC. p. 184. ISBN 1584882379.

[10] Baader and Nipkow, p. 11

[11] Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003, ISBN 0-521-39115-6, Here: p.11

[1]

[2]

[note 1]

[note 2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

Anonymous

Search

संप्रवाह (सार पुनर्लेखन)

Namespaces

More

Page actions

Contents

प्रेरक उदाहरण