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

चित्र.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

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