संप्रवाह (सार पुनर्लेखन): Difference between revisions

Latest revision as of 10:06, 18 July 2023

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

@@ Line 1: / Line 1: @@
-[[Image:Koblenz im Buga-Jahr 2011 - Deutsches Eck 01.jpg|thumb|चित्र.1: ''संप्रवाह'' नाम संप्रवाह से प्रेरित है, जिसका अर्थ है दो जल निकायों का मिलन।]]कंप्यूटर विज्ञान में, संप्रवाह [[पुनर्लेखन]] प्रणालियों का एक गुण है, जो बताता है कि समान परिणाम प्राप्त करने के लिए ऐसी प्रणाली में किन शब्दों को एक से अधिक विधियों से पुनर्लेखन किया जा सकता है। यह आलेख एक [[अमूर्त पुनर्लेखन प्रणाली]] की सबसे अमूर्त समायोजन में गुणों का वर्णन करता है।
+[[Image:Koblenz im Buga-Jahr 2011 - Deutsches Eck 01.jpg|thumb|चित्र.1: ''संप्रवाह'' नाम संप्रवाह से प्रेरित है, जिसका अर्थ है दो जल निकायों का मिलन।]]कंप्यूटर विज्ञान में, संप्रवाह [[पुनर्लेखन]] पुनर्लेखन प्रणालियों का एक गुण है, जो बताता है कि समान परिणाम प्राप्त करने के लिए ऐसी प्रणाली में किन शब्दों को एक से अधिक विधियों से पुनः लिखा जा सकता है। यह आलेख एक [[अमूर्त पुनर्लेखन प्रणाली|संक्षिप्त पुनर्लेखन प्रणाली]]  की सबसे संक्षिप्त समायोजन में गुणों का वर्णन करता है।
-== प्रेरक उदाहरण ==
+== अभिप्रेरक उदाहरण ==
-[[File:Confluence example expression.svg|right]]प्राथमिक गणित के सामान्य नियम एक अभिकलन प्रणाली बनाते हैं। उदाहरण के लिए, व्यंजक (11 + 9) × (2 + 4) को बाईं या दाईं व्यंजक से प्रारंभ करके मूल्यांकन किया जा सकता है; यद्यपि, दोनों स्थितियों में अंततः एक ही परिणाम प्राप्त होता है। यदि प्रत्येक गणितीय अभिव्यक्ति को छोटा करने की रणनीति के बाद भी समान परिणाम मिलता है, तो उस गणित अभिव्यक्ति प्रणाली को क्षेत्र-संप्रवाह कहा जाता है। पुनर्लेखन प्रणाली के विवरण के आधार पर अंकगणितीय पुनर्लेखन प्रणालियाँ संप्रवाह या गणितीय अभिव्यक्ति प्रणाली संप्रवाह हो सकता है, इस परिवर्तन प्रणाली के विवरणों पर निर्भर करता है।
+[[File:Confluence example expression.svg|right]]प्रारंभिक अंकगणित के सामान्य नियम एक संक्षिप्त पुनर्लेखन प्रणाली बनाते हैं। उदाहरण के लिए, अभिव्यक्ति (11 + 9) × (2 + 4) का मूल्यांकन बाएं या दाएं कोष्ठक से प्रारंभ करके किया जा सकता है; यद्यपि, दोनों ही स्थितियों में अंततः एक ही परिणाम प्राप्त होता है। यदि प्रत्येक गणितीय अभिव्यक्ति को छोटा करने की रणनीति के बाद भी समान परिणाम मिलता है, तो उस गणित अभिव्यक्ति प्रणाली को क्षेत्र-संप्रवाह कहा जाता है। पुनर्लेखन प्रणाली के विवरण के आधार पर अंकगणितीय पुनर्लेखन प्रणालियाँ संप्रवाह या गणितीय अभिव्यक्ति प्रणाली संप्रवाह हो सकता है, इस परिवर्तन प्रणाली के विवरणों पर निर्भर करता है।
-प्रत्येक समूह तत्व के व्युत्क्रम के व्युत्क्रम के बराबर होने के निम्नलिखित प्रमाण से एक दूसरा, अधिक अमूर्त उदाहरण प्राप्त होता है:<ref>{{cite book| title=कटौती प्रणाली| year=1992| page=291| publisher=Oldenbourg| editor=K. H. Bläsius and H.-J. Bürckert}} Here: p.134; axiom and proposition names follow the original text</ref>
+प्रत्येक समूह तत्व के व्युत्क्रम के व्युत्क्रम के बराबर होने के निम्नलिखित प्रमाण से एक दूसरा, अधिक संक्षिप्त उदाहरण प्राप्त होता है:<ref>{{cite book| title=कटौती प्रणाली| year=1992| page=291| publisher=Oldenbourg| editor=K. H. Bläsius and H.-J. Bürckert}} Here: p.134; axiom and proposition names follow the original text</ref>
 {| style="border: 1px solid grey; float: left; margin: 1em 1em;"
 |+ समूह स्वयंसिद्ध
@@ Line 62: / Line 62: @@
 | = || ''a'' || by R6
 |}
-<nowiki>:</nowiki>  यह प्रम ,यह प्रमाण माने गए समूह अभियोग A1-A3 से प्रारंभ होता है और पांच प्रस्तावनाएं R4, R6, R10, R11 और R12 स्थापित करता है, हर एक प्रस्तावना में पहले कुछ का उपयोग करता है, और R12 मुख्य प्रमाण होता है। कुछ प्रमाणों के लिए गैर-स्पष्ट या पुनः सृजनात्मक चरणों की आवश्यकता होती है, जैसे कि स्‍वयंसिद्ध A2 को उत्क्रम करके, पहले चरण में "1" को "a−1 ⋅ a" में पुनःलेखित करना। तर्कात्मक पुनःलेखन के सिद्धांत के विकास के ऐतिहासिक प्रेरणाओं में से एक यह थी कि ऐसे चरणों की आवश्यकता से बचा जा सके, जो अनुभवहीन मानव द्वारा ढूंढना कठिन होता है, और वह भी कंप्यूटर प्रोग्राम द्वारा कहीं अधिक कठिन होता है।
-यदि कोई टर्म_रीराइटिंग#टर्म_रीराइटिंग_सिस्टम संप्रवाह और ''रीराइटिंग#टर्मिनेशन'' है, तो दो अभिव्यक्तियों (जिसे ''[[ शब्द (तर्क) ]]'' भी कहा जाता है) ''एस'' और ''टी'' के बीच समानता साबित करने के लिए एक सीधी विधि मौजूद है। :
-''एस'' से शुरू करते हुए समानताएं लागू करें<ref group=note>then called ''rewrite rules'' to emphasize their left-to-right orientation</ref> जब तक संभव हो बाएँ से दाएँ, अंततः एक शब्द s' प्राप्त करना।
-इसी प्रकार t से एक पद t' प्राप्त करें।
-यदि दोनों पद s′ और t′ वस्तुतः सहमत हैं, तो s और t (आश्चर्यजनक रूप से नहीं) समान साबित होते हैं।
-इससे भी महत्वपूर्ण बात यह है कि यदि वे असहमत हैं, तो s और t बराबर नहीं हो सकते।
-अर्थात्, किन्हीं दो पदों s और t को बिल्कुल समान सिद्ध किया जा सकता है, ऐसा उस विधि द्वारा किया जा सकता है।
-उस विधि की सफलता एक निश्चित परिष्कृत क्रम पर निर्भर नहीं करती है जिसमें पुनर्लेखन नियमों को लागू करना है, क्योंकि 'संप्रवाह' यह सुनिश्चित करता है कि नियम अनुप्रयोगों का कोई भी अनुक्रम अंततः एक ही परिणाम देगा (जबकि समाप्ति संपत्ति यह सुनिश्चित करती है कि कोई भी अनुक्रम अंततः पहुंचेगा) बिल्कुल अंत)। इसलिए, यदि कुछ [[समीकरण सिद्धांत]] के लिए एक संप्रवाह और समाप्ति शब्द पुनर्लेखन प्रणाली प्रदान की जा सकती है,<ref group=note>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 [[Word problem (mathematics)#Example: A term rewriting system to decide the word problem in the free group|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''<sup>−1</sup>)<sup>−1</sup>⋅1 to obtain the term ''a''; no other rules are applicable.</ref> समानता शब्द का प्रमाण प्रस्तुत करने के लिए थोड़ी सी भी रचनात्मकता की आवश्यकता नहीं है; इसलिए वह कार्य कंप्यूटर प्रोग्राम के लिए उत्तरदायी हो जाता है। आधुनिक दृष्टिकोण शब्द पुनर्लेखन प्रणालियों के बजाय अधिक सामान्य अमूर्त पुनर्लेखन प्रणालियों को संभालते हैं; उत्तरार्द्ध पूर्व का एक विशेष मामला है।
-== सामान्य मामला और सिद्धांत ==
-[[Image:Confluence.svg|right|200px|thumb|चित्र.2: इस चित्र में, {{mvar|a}} दोनों को कम कर देता है {{mvar|b}} या {{mvar|c}} शून्य या अधिक पुनर्लेखन चरणों में (तारांकन द्वारा चिह्नित)। पुनर्लेखन संबंध को संप्रवाहित करने के लिए, दोनों को बदले में कुछ सामान्य तक कम करना होगा {{mvar|d}}.]]एक पुनर्लेखन प्रणाली को एक [[निर्देशित ग्राफ]] के रूप में व्यक्त किया जा सकता है जिसमें नोड्स अभिव्यक्तियों का प्रतिनिधित्व करते हैं और किनारे पुनर्लेखन का प्रतिनिधित्व करते हैं। इसलिए, उदाहरण के लिए, यदि अभिव्यक्ति a को b में दोबारा लिखा जा सकता है, तो हम कहते हैं कि b, a का एक छोटा रूप है (वैकल्पिक रूप से, a, b को कम करता है, या a, b का विस्तार है)। इसे तीर संकेतन का उपयोग करके दर्शाया गया है; a → b इंगित करता है कि a, b में कम हो जाता है। सहज रूप से, इसका मतलब है कि संबंधित ग्राफ़ में ए से बी तक एक निर्देशित किनारा है।
-यदि दो ग्राफ नोड्स c और d के बीच एक पथ है, तो यह एक कमी अनुक्रम बनाता है। इसलिए, उदाहरण के लिए, यदि c → c′ → c′′ → ... → d′ → d, तो हम c लिख सकते हैं {{overset|∗|→}} डी, सी से डी तक कमी अनुक्रम के अस्तित्व को दर्शाता है। औपचारिक रूप से, {{overset|∗|→}} → का क्लोजर (गणित)#बाइनरी रिलेशन क्लोजर|रिफ्लेक्सिव-ट्रांजिटिव क्लोजर है। पिछले पैराग्राफ से उदाहरण का उपयोग करते हुए, हमारे पास (11+9)×(2+4) → 20×(2+4) और 20×(2+4) → 20×6 है, इसलिए (11+9)×( 2+4) {{overset|∗|→}} 20×6.
-इसकी स्थापना से संप्रवाह को इस प्रकार परिभाषित किया जा सकता है। a ∈ S को संप्रवाह माना जाता है यदि सभी जोड़ियों के लिए b, c ∈ S ऐसा हो कि a {{overset|∗|→}} बी और ए {{overset|∗|→}} सी, बी के साथ एक डी ∈ एस मौजूद है {{overset|∗|→}}डी और सी {{overset|∗|→}} डी (निरूपित) <math>b \mathbin\downarrow c</math>). यदि प्रत्येक a ∈ S संप्रवाह है, तो हम कहते हैं कि → संप्रवाह है। दाईं ओर दिखाए गए चित्र के आकार के बाद, इस संपत्ति को कभी-कभी हीरे की संपत्ति भी कहा जाता है। कुछ लेखक हर जगह एकल कटौती के साथ आरेख के एक प्रकार के लिए हीरा संपत्ति शब्द को आरक्षित रखते हैं; अर्थात्, जब भी a → b और a → c, वहाँ a d का अस्तित्व इस प्रकार होना चाहिए कि b → d और c → d। सिंगल-रिडक्शन वेरिएंट मल्टी-रिडक्शन वेरिएंट की तुलना में अधिक मजबूत है।
+यह प्रणाम दिए गए समूह के अभिगम 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 को बिल्कुल समान सिद्ध किया जा सकता है, ऐसा उस विधि द्वारा किया जा सकता है।
+उस विधि की सफलता एक निश्चित परिष्कृत क्रम पर निर्भर नहीं करता है जिसमें पुनर्लेखन नियमों को लागू करना है, क्योंकि संप्रवाह यह सुनिश्चित करता है कि नियम अनुप्रयोगों का कोई भी अनुक्रम अंततः एक ही परिणाम देगा जबकि समाप्ति संपत्ति यह सुनिश्चित करता है कि कोई भी अनुक्रम अंततः अंत तक पहुंच सकता है। इसलिए, यदि कुछ समीकरण सिद्धांत के लिए एक संप्रवाह और समाप्ति शब्द पुनर्लेखन प्रणाली प्रदान की जा सकती है, शब्द समानता का प्रमाण देने के लिए थोड़ी सी भी रचनात्मकता की आवश्यकता नहीं है; इसलिए वह कार्य कंप्यूटर प्रोग्राम के लिए उत्तरदायी हो जाता है। आधुनिक दृष्टिकोण शब्द पुनर्लेखन प्रणालियों के अतिरिक्त अधिक सामान्य संक्षेप पुनर्लेखन प्रणालियों को नियंत्रित करते है जो उत्तरार्द्ध पूर्व का एक विशेष स्थिति है।
+== सामान्य स्थिति और सिद्धांत ==
+[[Image:Confluence.svg|right|200px|thumb|चित्र.2: इस चित्र में, {{mvar|a}} दोनों को कम कर देता है {{mvar|b}} या {{mvar|c}} शून्य या अधिक पुनर्लेखन चरणों में (तारांकन द्वारा चिह्नित)। पुनर्लेखन संबंध को संप्रवाहित करने के लिए, दोनों को बदले में कुछ सामान्य तक कम करना होगा {{mvar|d}}.]]एक पुनर्लेखन प्रणाली को एक [[निर्देशित ग्राफ|निर्देशित आरेख]] के रूप में व्यक्त किया जा सकता है जिसमें नोड्स अभिव्यक्तियों का प्रतिनिधित्व करते हैं और किनारे पुनर्लेखन का प्रतिनिधित्व करते हैं। इसलिए, उदाहरण के लिए, यदि अभिव्यक्ति a को b में पुनर्लेखित किया जा सकता है तो हम कहते हैं कि b, a का एक छोटा रूप है। इसे तीर संकेतन का उपयोग करके दर्शाया गया है; a → b इंगित करता है कि a, b में कम हो जाता है। सहज रूप से, इसका अर्थ है कि संबंधित आरेख में a से b तक एक निर्देशित किनारा है।
+यदि दो आरेख नोड c और d के बीच एक पथ होती है, तो यह एक पुनर्निर्माण अनुक्रम बनाती है। इसलिए, उदाहरण के लिए, यदि c → c′ → c′′ → ... → d′ → d, होता है, तो हम  ''c'',{{overset|∗|→}}''d'', लिख सकते है जिससे c से d तक एक पुनर्निर्माण अनुक्रम की उपस्थिति का संकेत मिलता है। औपचारिक रूप से, {{overset|∗|→}} → का प्रतिदीप्त-संचारिक संघटन" होता है जो पिछले पैराग्राफ में दिए गए उदाहरण का उपयोग करते हुए, हमारे  (11+9)×(2+4) → 20×(2+4) और 20×(2+4) → 20×6 है, इसलिए (11+9)×( 2+4) {{overset|∗|→}} 20×6.होता है।
+इसके आधार पर, संयोजन निम्नलिखित रूप में परिभाषित की जा सकती है: S में विद्यमान ऐसे सभी जोड़ों के लिए a {{overset|∗|→}} b और a {{overset|∗|→}} c , की स्थिति मे जहां  b, c ∈ S हैं, एक ऐसा d ∈ S उपस्थित होता है  जिसके लिए b{{overset|∗|→}}d और c  {{overset|∗|→}} d होता है, इसे  <math>b \mathbin\downarrow c</math> द्वारा निरूपित किया जाता है।
+यदि प्रत्येक a ∈ S संप्रवाह है, तो हम कहते हैं कि → संप्रवाह है। दाईं ओर दिखाए गए चित्र के आकार के बाद, इस गुण को कभी-कभी मणि गुण भी कहा जाता है। कुछ लेखक शब्द "मणि गुण" को एक ऐसे आरेख के लिए सुरक्षित रखते हैं जिसमें हर जगह एकांशित घटाने होते हैं; अर्थात, जब भी a → b और a → c होता है, तो b → d और c → d जैसा d उपस्थित होता है। एकल-परिवर्तन विभिन्न बहु-संक्षिप्ति परिवर्त के सापेक्ष में अधिक सामथर्यवान होता है।
 ===भूमि संप्रवाह ===
-एक शब्द पुनर्लेखन प्रणाली ग्राउंड कंफ्लुएंट होती है यदि प्रत्येक [[ जमीनी अवधि ]] कंफ्लुएंट हो, अर्थात प्रत्येक शब्द बिना चर के हो।<ref>{{cite book |last1=Robinson |first1=Alan J. A. |last2=Voronkov |first2=Andrei |title=स्वचालित तर्क की पुस्तिका|date=5 July 2001 |publisher=Gulf Professional Publishing |isbn=978-0-444-82949-8 |page=560 |url=https://books.google.com/books?id=X3z8ujBRgmEC&dq=ground%20confluent&pg=PA560 |language=en}}</ref>
+शब्द पुनर्लेखन प्रणाली "भूमि संप्रवाह" होती है जब हर भूमिका शब्द संप्रवाहक होता है, अर्थात जब कोई भी चर चक्र के बिना शब्द संयोजित होता है।<ref>{{cite book |last1=Robinson |first1=Alan J. A. |last2=Voronkov |first2=Andrei |title=स्वचालित तर्क की पुस्तिका|date=5 July 2001 |publisher=Gulf Professional Publishing |isbn=978-0-444-82949-8 |page=560 |url=https://books.google.com/books?id=X3z8ujBRgmEC&dq=ground%20confluent&pg=PA560 |language=en}}</ref>
@@ Line 91: / Line 98: @@
 [[File:Cyclic_locally,_but_not_globally_confluent_rewrite_system.png|thumb|चित्र.3: चक्रीय, स्थानीय रूप से संप्रवाहित, लेकिन विश्व स्तर पर संप्रवाहित पुनर्लेखन प्रणाली नहीं<ref name="Dershowitz.Jouannaud.1990.Fig2">{{cite book | isbn=0-444-88074-7 | editor=Jan van Leeuwen | title=औपचारिक मॉडल और शब्दार्थ| publisher=Elsevier | series=Handbook of Theoretical Computer Science | volume=B | year=1990 | author=N. Dershowitz and J.-P. Jouannaud | contribution=Rewrite Systems | pages=243&ndash;320}} Here: p.268, Fig.2a+b.</ref>]]
-[[File:Non-cyclic locally, but not globally confluent rewrite system.gif|thumb|चित्र.4: अनंत गैर-चक्रीय, स्थानीय रूप से-संप्रवाह, लेकिन विश्व स्तर पर मिश्रित पुनर्लेखन प्रणाली नहीं<ref name="Dershowitz.Jouannaud.1990.Fig2"/>]]एक तत्व a ∈ S को स्थानीय रूप से (या कमजोर रूप से) संप्रवाह कहा जाता है यदि सभी b, c ∈ S के लिए a → b और a → c के साथ d ∈ S मौजूद हो {{overset|∗|→}}डी और सी {{overset|∗|→}} डी। यदि प्रत्येक ∈ S स्थानीय रूप से संप्रवाह है, तो → को स्थानीय रूप से (या कमजोर रूप से) संप्रवाह कहा जाता है, या कमजोर चर्च-रोसेर संपत्ति वाला कहा जाता है। यह संप्रवाह से भिन्न है क्योंकि बी और सी को एक चरण में ए से कम किया जाना चाहिए। इसके अनुरूप, संप्रवाह को कभी-कभी वैश्विक संप्रवाह भी कहा जाता है।
+[[File:Non-cyclic locally, but not globally confluent rewrite system.gif|thumb|चित्र.4: अनंत गैर-चक्रीय, स्थानीय रूप से-संप्रवाह, लेकिन विश्व स्तर पर मिश्रित पुनर्लेखन प्रणाली नहीं<ref name="Dershowitz.Jouannaud.1990.Fig2"/>]]एक तत्व a ∈ S को स्थानीय रूप से संप्रवाह कहा जाता है यदि सभी b, c ∈ S के लिए a → b और a → c के साथ d ∈ S उपस्थित हो {{overset|∗|→}}d और c {{overset|∗|→}} d होता है। यदि प्रत्येक a ∈ S स्थानीय रूप से संप्रवाह है, तो → को स्थानीय रूप से संप्रवाह कहा जाता है, यह संप्रवाह से भिन्न होता है क्योंकि  b और c को एक चरण में a से कम किया जाता है। इसके अनुरूप, संप्रवाह को कभी-कभी वैश्विक संप्रवाह भी कहा जाता है।
+संबंध {{overset|∗|→}}, पुनर्निर्माण अनुक्रमों के लिए प्रदर्शन के रूप में प्रस्तुत किए जाने पर,को अपने अधिकार में एक पुनर्लेखन प्रणाली के रूप में देखा जा सकता है, जिसका संबंध → प्रतिदीप्त-संचारिक संघटन" होता है।
-रिश्ता {{overset|∗|→}}, कटौती अनुक्रमों के लिए एक संकेतन के रूप में पेश किया गया, इसे अपने आप में एक पुनर्लेखन प्रणाली के रूप में देखा जा सकता है, जिसका संबंध → का क्लोजर_(गणित)#बाइनरी रिलेशन क्लोजर|रिफ्लेक्टिव-ट्रांजिटिव क्लोजर है। चूँकि कमी अनुक्रमों का एक क्रम फिर से एक कमी अनुक्रम है (या, समतुल्य रूप से, चूंकि रिफ्लेक्सिव-ट्रांजिटिव क्लोजर बनाना निष्क्रियता#यूनरी ऑपरेशन है), {{overset|∗|{{overset|∗|→}}}} = {{overset|∗|→}}. इससे यह निष्कर्ष निकलता है कि → संप्रवाह है यदि और केवल यदि {{overset|∗|→}} स्थानीय रूप से संप्रवाह है।
+क्योंकि पुनर्निर्माण अनुक्रमों की एक अनुक्रमिकता पुनः से एक पुनर्निर्माण अनुक्रम है या समान रूप से, क्योंकि प्रतिदीप्त-संचारिक समापन का गठन स्वचालित होता है, {{overset|∗|{{overset|∗|→}}}} = {{overset|∗|→}}. इससे यह निष्कर्ष निकलता है कि → संप्रवाह है यदि और केवल यदि {{overset|∗|→}} स्थानीय रूप से संप्रवाह है।
-एक पुनर्लेखन प्रणाली (वैश्विक स्तर पर) मिश्रित हुए बिना भी स्थानीय रूप से संप्रवाहित हो सकती है। उदाहरण चित्र 3 और 4 में दिखाए गए हैं। हालाँकि, न्यूमैन की लेम्मा बताती है कि यदि स्थानीय रूप से संप्रवाह पुनर्लेखन प्रणाली में कोई अनंत कमी अनुक्रम नहीं है (जिस स्थिति में इसे समाप्त या दृढ़ता से सामान्यीकृत कहा जाता है), तो यह विश्व स्तर पर संप्रवाह है।
+एक पुनर्लेखन प्रणाली स्थानिक रूप से संयोजक होने के अतिरिक्त   संयोजक नहीं हो सकती है। उदाहरण चित्र 3 और 4 में दिखाए गए हैं। यद्यपि, , न्यूमैन का लेमा कहता है कि यदि एक स्थानिक रूप से संयोजक पुनर्लेखन प्रणाली में कोई अनंत पुनर्निर्माण अनुक्रम नहीं होता है तो यह वैश्विक रूप से संप्रवाह होता है।
-=== चर्च-रोसेर संपत्ति ===
+=== चर्च-रोसेर गुण ===
+यदि एक पुनर्लेखन प्रणाली को "चर्च-रॉसर गुण" होता है, तो केवल तभी जब <math>x \stackrel{*}{\leftrightarrow} y</math> होता है तो सभी वस्तुएं x, y के लिए <math>x\mathbin\downarrow y</math> होता है।   [[अलोंजो चर्च]] और जे. बार्कले रोसेर ने 1936 में प्रस्तुत किया कि [[लैम्ब्डा कैलकुलस]] में यह गुण होता है;<ref>Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans.
+AMS, 39:472-482, 1936</ref> <ref>Baader and Nipkow, p. 9</ref> लैम्बडा कैलकुलस के इस गुणधर्म को जानने के लिए यह तथ्य भी चर्च-रॉसर का सिद्धांत के रूप में जाना जाता है।चर्च-रॉसर गुणधर्म वाली एक पुनर्लेखन प्रणाली में, शब्द समस्या को एक सामान्य उत्तर की खोज में कम किया जा सकता है। चर्च-रॉसर प्रणाली में, एक वस्तु की अधिकतम एक साधारित रूप होता है; अर्थात यदि एक वस्तु का साधारित रूप मौजूद है, तो वह एकद्वितीय होता है, लेकिन यह मौजूद नहीं हो सकता है। उदाहरण के लिए, लैम्बडा कैलकुलस में अभिव्यक्ति (λx.xx)(λx.xx) का कोई साधारित रूप नहीं है क्योंकि इसके अनंत β-पुनर्निर्माणों का एक अनंत अनुक्रम होता है (λx.xx)(λx.xx) → (λx.xx)  (λx.xx) →अनुक्रम होता है। <ref>{{cite book |last1=Cooper |first1=S. B. |title=कम्प्यूटेबिलिटी सिद्धांत|date=2004 |publisher=Chapman & Hall/CRC |location=Boca Raton |isbn=1584882379 |page=184}}</ref>
+एक पुनर्लेखन प्रणाली चर्च-रॉसर गुणधर्म का धारण करती है यदि और केवल यदि वह संयोजक है।[8] इस समानता के कारण, साहित्य में परिभाषाओं में बहुत सी विविधता होती है। उदाहरण के लिए, "टेरेसी" में चर्च-रॉसर गुणधर्म और संयोजन को समानार्थी और इस परिभाषा के तत्व समान होने के रूप में परिभाषित किया जाता है; यहां परिभाषित चर्च-रॉसर गुणधर्म को अनदेखा किया गया है, परंतु इसे एक समकोणी गुणधर्म के रूप में दिया गया है; और यह अन्य ग्रंथों से विचलन सोच समझ कर किया गया है। <ref>Marc Bezem, [[Jan Willem Klop]], Roel de Vrijer ("Terese"), ''Term rewriting systems'', Cambridge University Press, 2003, {{ISBN|0-521-39115-6}}, Here: p.11</ref>
-ऐसा कहा जाता है कि एक पुनर्लेखन प्रणाली के पास चर्च-रोसेर संपत्ति होती है यदि और केवल यदि <math>x \stackrel{*}{\leftrightarrow} y</math> तात्पर्य <math>x\mathbin\downarrow y</math> सभी वस्तुओं x, y के लिए। [[अलोंजो चर्च]] और जे. बार्कले रोसेर ने 1936 में साबित किया कि [[लैम्ब्डा कैलकुलस]] में यह गुण है;<ref>Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans.
-AMS, 39:472-482, 1936</ref> इसलिए संपत्ति का नाम.<ref>Baader and Nipkow, p. 9</ref> (यह तथ्य कि लैम्ब्डा कैलकुलस में यह संपत्ति है, इसे चर्च-रोसेर प्रमेय के रूप में भी जाना जाता है।) चर्च-रोसेर संपत्ति के साथ एक पुनर्लेखन प्रणाली में शब्द समस्या को एक सामान्य उत्तराधिकारी की खोज तक कम किया जा सकता है। चर्च-रोसेर प्रणाली में, एक वस्तु का अधिकतम एक सामान्य रूप (अमूर्त पुनर्लेखन) होता है; अर्थात् किसी वस्तु का सामान्य रूप यदि अस्तित्व में है तो अद्वितीय है, लेकिन यह अस्तित्व में नहीं भी हो सकता है। उदाहरण के लिए लैम्ब्डा कैलकुलस में, अभिव्यक्ति (λx.xx)(λx.xx) का कोई सामान्य रूप नहीं है क्योंकि β-कटौती (λx.xx)(λx.xx) → (λx.xx) का एक अनंत अनुक्रम मौजूद है। (λx.xx) → ...<ref>{{cite book |last1=Cooper |first1=S. B. |title=कम्प्यूटेबिलिटी सिद्धांत|date=2004 |publisher=Chapman & Hall/CRC |location=Boca Raton |isbn=1584882379 |page=184}}</ref>
-एक पुनर्लेखन प्रणाली के पास चर्च-रोसेर संपत्ति होती है यदि और केवल यदि यह संप्रवाह है।<ref>Baader and Nipkow, p. 11</ref> इस समानता के कारण, साहित्य में परिभाषाओं में काफी भिन्नता पाई जाती है। उदाहरण के लिए, टेरेसी में चर्च-रोसेर संपत्ति और संप्रवाह को यहां प्रस्तुत संप्रवाह की परिभाषा के पर्यायवाची और समान के रूप में परिभाषित किया गया है; चर्च-रोसेर जैसा कि यहां परिभाषित है, अज्ञात है, लेकिन इसे समकक्ष संपत्ति के रूप में दिया गया है; अन्य ग्रंथों से यह विचलन जानबूझकर किया गया है।<ref>Marc Bezem, [[Jan Willem Klop]], Roel de Vrijer ("Terese"), ''Term rewriting systems'', Cambridge University Press, 2003, {{ISBN|0-521-39115-6}}, Here: p.11</ref>
 === अर्ध-संप्रवाह ===
-स्थानीय संप्रवाह की परिभाषा वैश्विक संप्रवाह से भिन्न है जिसमें केवल एक पुनर्लेखन चरण में दिए गए तत्व से प्राप्त तत्वों पर विचार किया जाता है। एक चरण में एक तत्व तक पहुंचने और एक मनमाना अनुक्रम द्वारा पहुंचे दूसरे तत्व पर विचार करके, हम अर्ध-संप्रवाह की मध्यवर्ती अवधारणा पर पहुंचते हैं: ए ∈ एस को अर्ध-संप्रवाह कहा जाता है यदि सभी बी के लिए, सी ∈ एस → के साथ बी और ए {{overset|∗|→}} c में b के साथ d ∈ S मौजूद है {{overset|∗|→}}डी और सी {{overset|∗|→}} डी; यदि प्रत्येक a ∈ S अर्ध-संप्रवाह है, तो हम कहते हैं कि → अर्ध-संप्रवाह है।
+स्थानीय संप्रवाह की परिभाषा वैश्विक संप्रवाह से भिन्न है जिसमें केवल एक पुनर्लेखन चरण में दिए गए तत्व से प्राप्त तत्वों पर विचार किया जाता है। एक चरण में एक तत्व तक पहुंचने और एक मनमाना अनुक्रम द्वारा पहुंचे दूसरे तत्व पर विचार करके, हम अर्ध-संप्रवाह की मध्यवर्ती अवधारणा पर पहुंचते हैं: a ∈ s के लिए यदि ऐसे सभी यदि सभी होते हैं जिनके साथ, a {{overset|∗|→}} b और a {{overset|∗|→}}c होता है, तो ऐसा d ∈ S उपस्थित होता है जिसके लिए b {{overset|∗|→}}d और c {{overset|∗|→}} d होता है यदि प्रत्येक a ∈ S अर्ध-संप्रवाह है, तो हम कहते हैं कि यह → अर्ध-संप्रवाह है।
-एक अर्ध-संप्रवाह तत्व को मिला हुआ होने की आवश्यकता नहीं है, लेकिन एक अर्ध-संप्रवाह पुनर्लेखन प्रणाली आवश्यक रूप से संप्रवाह है, और एक संप्रवाह प्रणाली तुच्छ रूप से अर्ध-संप्रवाह है।
+एक अर्ध-संप्रवाह तत्व को मिला हुआ होने की आवश्यकता नहीं है, लेकिन एक अर्ध-संप्रवाह पुनर्लेखन प्रणाली आवश्यक रूप से संप्रवाह है, और एक संप्रवाह प्रणाली स्वचालित रूप से आर्ध-संप्रवाह होती है।।
 === प्रबल संप्रवाह ===
-मजबूत संप्रवाह स्थानीय संप्रवाह पर एक और भिन्नता है जो हमें यह निष्कर्ष निकालने की अनुमति देता है कि एक पुनर्लेखन प्रणाली विश्व स्तर पर संप्रवाह है। एक तत्व a ∈ S को दृढ़ता से मिला हुआ कहा जाता है यदि सभी b, c ∈ S के लिए a → b और a → c के साथ d ∈ S मौजूद हो {{overset|∗|→}} d और या तो c → d या c = d; यदि प्रत्येक a ∈ S दृढ़ता से मिला हुआ है, तो हम कहते हैं कि → दृढ़ता से मिला हुआ है।
+प्रबल संप्रवाह स्थानीय संप्रवाह पर एक और भिन्नता है जो हमें यह निष्कर्ष निकालने की अनुमति देता है कि एक पुनर्लेखन प्रणाली विश्व स्तर पर संप्रवाह है। यदि a ∈ S के लिए b, c ∈ S के साथ  a → b और a → c होता है तो d ∈ S उपस्थित होता है जिसके लिए b  {{overset|∗|→}} d होता है और या तो  c → d या c = d होता है यदि प्रत्येक a ∈ S को प्रबल संप्रवाह कहा जाता है।
-एक संप्रवाह तत्व को दृढ़ता से मिला हुआ होने की आवश्यकता नहीं है, लेकिन एक दृढ़ता से मिला हुआ पुनर्लेखन प्रणाली आवश्यक रूप से संप्रवाह है।
+एक संप्रवाह तत्व को दृढ़ता से मिला हुआ होने की आवश्यकता नहीं है, परंतु दृढ़ता से मिला हुआ पुनर्लेखन प्रणाली आवश्यक रूप से संप्रवाह है।
 == संप्रवाह प्रणालियों के उदाहरण ==
-* [[बहुपद]] मॉड्यूलो का न्यूनीकरण एक [[आदर्श (रिंग सिद्धांत)]] एक संप्रवाह पुनर्लेखन प्रणाली है, बशर्ते कोई ग्रोबनर आधार के साथ काम करे।
+* जब किसी ग्रोबनर बेसिस के साथ काम किया जाता है, तब आदेशग्रस्त प्रणाली के रूप में आदेश के अधीन विभाजन के पुनर्निर्माण को संघटनीय पुनर्लेखन प्रणाली कहा जाता है।
-* मात्सुमोतो का प्रमेय (समूह सिद्धांत)|मात्सुमोतो का प्रमेय ब्रैड संबंधों के संप्रवाह से आता है।
+* मात्सुमोटो का सिद्धांत ब्रेड संबंधों की संप्रवाह से आता है।
-* λ-शब्दों की β-कमी चर्च-रोसेर प्रमेय से मिलती है।
+* चर्च-रॉसर के सिद्धांत के अनुसंक्षिप्त  , लैम्बडा-अभिव्यक्तियों का बीटा-पुनर्निर्माण संयोज्य होता है।
 == यह भी देखें ==
 * [[अभिसरण (तर्क)]]
 * [[क्रिटिकल जोड़ी (तर्क)]]
-* सामान्य रूप (सार पुनर्लेखन)
+* सामान्य रूप (संक्षिप्त   पुनर्लेखन)
 == टिप्पणियाँ ==
@@ Line 140: / Line 151: @@
 {{Authority control}}
-{{DEFAULTSORT:Confluence (Abstract Rewriting)}}[[Category: पुनर्लेखन प्रणाली]]
+{{DEFAULTSORT:Confluence (Abstract Rewriting)}}
-[[Category: Machine Translated Page]]
+[[Category:CS1 English-language sources (en)]]
-[[Category:Created On 30/06/2023]]
+[[Category:Created On 30/06/2023|Confluence (Abstract Rewriting)]]
+[[Category:Machine Translated Page|Confluence (Abstract Rewriting)]]
+[[Category:Pages with script errors|Confluence (Abstract Rewriting)]]
+[[Category:Templates Vigyan Ready|Confluence (Abstract Rewriting)]]
+[[Category:पुनर्लेखन प्रणाली|Confluence (Abstract Rewriting)]]

Anonymous

Search

संप्रवाह (सार पुनर्लेखन): Difference between revisions

Namespaces

More

Page actions

Latest revision as of 10:06, 18 July 2023

Contents

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