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

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

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

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

प्राथमिक गणित के सामान्य नियम एक अभिकलन प्रणाली बनाते हैं। उदाहरण के लिए, व्यंजक (11 + 9) × (2 + 4) को बाईं या दाईं व्यंजक से प्रारंभ करके मूल्यांकन किया जा सकता है; यद्यपि, दोनों स्थितियों में अंततः एक ही परिणाम प्राप्त होता है। यदि प्रत्येक गणितीय अभिव्यक्ति को छोटा करने की रणनीति के बाद भी समान परिणाम मिलता है, तो उस गणित अभिव्यक्ति प्रणाली को क्षेत्र-संप्रवाह कहा जाता है। पुनर्लेखन प्रणाली के विवरण के आधार पर अंकगणितीय पुनर्लेखन प्रणालियाँ संप्रवाह या गणितीय अभिव्यक्ति प्रणाली संप्रवाह हो सकता है, इस परिवर्तन प्रणाली के विवरणों पर निर्भर करता है।

प्रत्येक समूह तत्व के व्युत्क्रम के व्युत्क्रम के बराबर होने के निम्नलिखित प्रमाण से एक दूसरा, अधिक अमूर्त उदाहरण प्राप्त होता है:^[1]

समूह स्वयंसिद्ध
A1	1 ⋅ a	= a
A2	a⁻¹ ⋅ a	= 1
A3	(a ⋅ b) ⋅ c	= a ⋅ (b ⋅ c)

R4 का प्रमाण : a⁻¹⋅(a⋅b) = b
	a⁻¹ ⋅ (a ⋅ b)
=	(a⁻¹ ⋅ a) ⋅ b	by A3(r)
=	1 ⋅ b	by A2
=	b	by A1

R6का प्रमाण: (a⁻¹)⁻¹ ⋅ 1 = a
	(a⁻¹)⁻¹ ⋅ 1
=	(a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ a)	by A2(r)
=	a	by R4

R10 का प्रमाण: (a⁻¹)⁻¹ ⋅ b = a ⋅ b
	(a⁻¹)⁻¹ ⋅ b
=	(a⁻¹)⁻¹ ⋅ (a⁻¹ ⋅ (a ⋅ b))	by R4(r)
=	a ⋅ b	by R4

R11 का प्रमाण: a ⋅ 1 = a
	a ⋅ 1
=	(a⁻¹)⁻¹ ⋅ 1	by R10(r)
=	a	by R6

R12 का प्रमाण: (a⁻¹)⁻¹ = a
	(a⁻¹)⁻¹
=	(a⁻¹)⁻¹ ⋅ 1	by R11(r)
=	a	by R6

यह प्रमाण माने गए समूह अभियोग A1-A3 से प्रारंभ होता है और पांच प्रस्तावनाएं R4, R6, R10, R11 और R12 स्थापित करता है, हर एक प्रस्तावना में पहले कुछ का उपयोग करता है, और R12 मुख्य प्रमाण होता है। कुछ प्रमाणों के लिए गैर-स्पष्ट या पुनः सृजनात्मक चरणों की आवश्यकता होती है, जैसे कि स्‍वयंसिद्ध A2 को उत्क्रम करके, पहले चरण में "1" को "a−1 ⋅ a" में पुनःलेखित करना। तर्कात्मक पुनःलेखन के सिद्धांत के विकास के ऐतिहासिक प्रेरणाओं में से एक यह थी कि ऐसे चरणों की आवश्यकता से बचा जा सके, जो अनुभवहीन मानव द्वारा ढूंढना कठिन होता है, और वह भी कंप्यूटर प्रोग्राम द्वारा कहीं अधिक कठिन होता है। यदि एक तर्कात्मक पुनर्लेखन प्रणाली संप्रवाह और समाप्ति है, तो दो अभिव्यक्तियों s और t के बीच समानता प्रमाणित करने के लिए एक सीधी विधि उपस्थित है, प्रारंभ s के साथ करें, बाएं से दाएं समानता को लागू करें जहाँ तक संभव हो, अंततः पद s' प्राप्त करें। एक ही विधि से पद t' प्राप्त करें। यदि दोनों पद s' और t' वास्तव में मेल खाते हैं, तो s और t समान सिद्ध होते हैं। अधिक महत्वपूर्ण बात यह है कि यदि वे असहमत होते हैं, तो s और t समान नहीं हो सकते हैं। अर्थात, कोई भी दो पद s और t जो किसी भी विधि से सिद्ध हो सकते हैं, उन्हें उस विधि द्वारा सिद्ध किया जा सकता है।

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

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

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

a

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

b

या

c

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

d

.

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

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

इसके आधार पर, संयोजन निम्नलिखित रूप में परिभाषित की जा सकती है: S में विद्यमान ऐसे सभी जोड़ों के लिए a ∗→ b और a ∗→ c , की स्थिति मे जहां b, c ∈ S हैं, एक ऐसा d ∈ S उपस्थित होता है जिसके लिए b∗→d और c ∗→ d होता है, इसे $b\mathbin {\downarrow } c$ द्वारा निरूपित किया जाता है।

यदि प्रत्येक a ∈ S संप्रवाह है, तो हम कहते हैं कि → संप्रवाह है। दाईं ओर दिखाए गए चित्र के आकार के बाद, इस गुण को कभी-कभी मणि गुण भी कहा जाता है। कुछ लेखक शब्द "मणि गुण" को एक ऐसे आरेख के लिए सुरक्षित रखते हैं जिसमें हर जगह एकांशित घटाने होते हैं; अर्थात, जब भी a → b और a → c होता है, तो b → d और c → d जैसा d उपस्थित होता है। एकल-परिवर्तन विभिन्न बहु-संक्षिप्ति परिवर्त के सापेक्ष में अधिक सामथर्यवान होता है।

भूमि संप्रवाह

शब्द पुनर्लेखन प्रणाली "भूमि संप्रवाह" होती है जब हर भूमिका शब्द संप्रवाहक होता है, अर्थात जब कोई भी चर चक्र के बिना शब्द संयोजित होता है।^[2]

स्थानीय संप्रवाह

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

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

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

संबंध ∗→, पुनर्निर्माण अनुक्रमों के लिए प्रदर्शन के रूप में प्रस्तुत किए जाने पर,को अपने अधिकार में एक पुनर्लेखन प्रणाली के रूप में देखा जा सकता है, जिसका संबंध → प्रतिदीप्त-संचारिक संघटन" होता है।

क्योंकि पुनर्निर्माण अनुक्रमों की एक अनुक्रमिकता पुनः से एक पुनर्निर्माण अनुक्रम है या समान रूप से, क्योंकि प्रतिदीप्त-संचारिक समापन का गठन स्वचालित होता है, ∗∗→ = ∗→. इससे यह निष्कर्ष निकलता है कि → संप्रवाह है यदि और केवल यदि ∗→ स्थानीय रूप से संप्रवाह है।

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

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

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

अर्ध-संप्रवाह

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

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

प्रबल संप्रवाह

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

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

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

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

यह भी देखें

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

↑ 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

↑ 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.
↑ ^3.0 ^3.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.

[2] 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] 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

[3] 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-4] 3.0 ^3.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.

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

[6] Baader and Nipkow, p. 9

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

[8] Baader and Nipkow, p. 11

[9] 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]

[note 1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

Anonymous

Search

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

Namespaces

More

Page actions

Contents

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