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

चित्र.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" में परिवर्तित करके R6 के प्रणाम के पहले चरण में लेखन होता है। शब्द पुनर्लेखन के सिद्धांत को विकसित करने की ऐतिहासिक प्रेरणाओं में से एक ऐसे चरणों की आवश्यकता से बचना था, जिन्हें एक अनुभवहीन मानव के लिए खोजना मुश्किल है, कंप्यूटर प्रोग्राम की तो बात ही छोड़ दें।

यदि एक शब्द पुनर्लेखन प्रणाली संप्रवाह और समाप्ति है, तो दो अभिव्यक्तियों s और t के बीच समानता सिद्ध करने के लिए एक सीधी विधि उपस्थित है: s से प्रारंभ करके, जब तक संभव हो बाएं से दाएं समानता लागू करें, अंततः एक पद s' प्राप्त किया जा सकता है। इसी प्रकार t से एक पद t' प्राप्त करें। यदि दोनों पद s′ और t′ वस्तुतः सहमत हैं, तो s और t समान सिद्ध होते हैं। इससे भी महत्वपूर्ण बात यह है कि यदि वे असहमत हैं, तो s और t बराबर नहीं हो सकते। अर्थात्, किन्हीं दो पदों s और t को बिल्कुल समान सिद्ध किया जा सकता है, ऐसा उस विधि द्वारा किया जा सकता है।

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

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

चित्र.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, y के लिए $x\mathbin {\downarrow } y$ होता है। अलोंजो चर्च और जे. बार्कले रोसेर ने 1936 में प्रस्तुत किया कि लैम्ब्डा कैलकुलस में यह गुण होता है;^[4] ^[5] लैम्बडा कैलकुलस के इस गुणधर्म को जानने के लिए यह तथ्य भी चर्च-रॉसर का सिद्धांत के रूप में जाना जाता है।चर्च-रॉसर गुणधर्म वाली एक पुनर्लेखन प्रणाली में, शब्द समस्या को एक सामान्य उत्तर की खोज में कम किया जा सकता है। चर्च-रॉसर प्रणाली में, एक वस्तु की अधिकतम एक साधारित रूप होता है; अर्थात यदि एक वस्तु का साधारित रूप मौजूद है, तो वह एकद्वितीय होता है, लेकिन यह मौजूद नहीं हो सकता है। उदाहरण के लिए, लैम्बडा कैलकुलस में अभिव्यक्ति (λx.xx)(λx.xx) का कोई साधारित रूप नहीं है क्योंकि इसके अनंत β-पुनर्निर्माणों का एक अनंत अनुक्रम होता है (λx.xx)(λx.xx) → (λx.xx) (λx.xx) →अनुक्रम होता है। ^[6]

एक पुनर्लेखन प्रणाली चर्च-रॉसर गुणधर्म का धारण करती है यदि और केवल यदि वह संयोजक है।[8] इस समानता के कारण, साहित्य में परिभाषाओं में बहुत सी विविधता होती है। उदाहरण के लिए, "टेरेसी" में चर्च-रॉसर गुणधर्म और संयोजन को समानार्थी और इस परिभाषा के तत्व समान होने के रूप में परिभाषित किया जाता है; यहां परिभाषित चर्च-रॉसर गुणधर्म को अनदेखा किया गया है, परंतु इसे एक समकोणी गुणधर्म के रूप में दिया गया है; और यह अन्य ग्रंथों से विचलन सोच समझ कर किया गया है। ^[7]

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

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

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

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

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

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

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

जब किसी ग्रोबनर बेसिस के साथ काम किया जाता है, तब आदेशग्रस्त प्रणाली के रूप में आदेश के अधीन विभाजन के पुनर्निर्माण को संघटनीय पुनर्लेखन प्रणाली कहा जाता है।
मात्सुमोटो का सिद्धांत ब्रेड संबंधों की संप्रवाह से आता है।
चर्च-रॉसर के सिद्धांत के अनुसंक्षिप्त , लैम्बडा-अभिव्यक्तियों का बीटा-पुनर्निर्माण संयोज्य होता है।

यह भी देखें

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

संदर्भ

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.
↑ 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.

[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

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

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

[5] Baader and Nipkow, p. 9

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

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

[3]

[4]

[5]

[6]

[7]

Anonymous

Search

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

Namespaces

More

Page actions

Contents

अभिप्रेरक उदाहरण