शब्द समस्या (गणित): Difference between revisions

From Vigyanwiki
No edit summary
 
Line 212: Line 212:


{{Authority control}}
{{Authority control}}
[[Category: सार बीजगणित]] [[Category: शब्दों पर कॉम्बिनेटरिक्स]] [[Category: पुनर्लेखन प्रणाली]] [[Category: कम्प्यूटेशनल समस्याएं]]


 
[[Category:Articles with hatnote templates targeting a nonexistent page]]
 
[[Category:CS1 English-language sources (en)]]
[[Category: Machine Translated Page]]
[[Category:CS1 maint]]
[[Category:CS1 русский-language sources (ru)]]
[[Category:Created On 21/03/2023]]
[[Category:Created On 21/03/2023]]
[[Category:Vigyan Ready]]
[[Category:Lua-based templates]]
[[Category:Machine Translated Page]]
[[Category:Pages with script errors]]
[[Category:Templates Vigyan Ready]]
[[Category:Templates that add a tracking category]]
[[Category:Templates that generate short descriptions]]
[[Category:Templates using TemplateData]]
[[Category:कम्प्यूटेशनल समस्याएं]]
[[Category:पुनर्लेखन प्रणाली]]
[[Category:शब्दों पर कॉम्बिनेटरिक्स]]
[[Category:सार बीजगणित]]

Latest revision as of 18:41, 21 April 2023

कम्प्यूटरीकृत गणित में शब्द समस्या यह निर्णय समस्या है कि क्या दो दिए गए भाव पुनर्लेखन पहचान (गणित) के एक समूह के संबंध में समान हैं। प्रोटोटाइपिक उदाहरण समूहों के लिए शब्द समस्या है। किन्तु कई अन्य उदाहरण भी हैं। कम्प्यूटरीकृत सिद्धांत का अच्छा परिणाम यह है कि इस प्रश्न का उत्तर देना कई महत्वपूर्ण स्थितियों में अनिर्णीत समस्या है।[1]


पृष्ठभूमि और प्रेरणा

कंप्यूटर बीजगणित में अधिकांशतः अभिव्यक्ति ट्री का उपयोग करके गणितीय अभिव्यक्तियों को एन्कोड करना चाहता है। किन्तु अधिकांशतः कई समान अभिव्यक्ति ट्री होते हैं। स्वाभाविक रूप से यह प्रश्न है कि क्या कोई एल्गोरिथम है। जो दो भावों के इनपुट के रूप में दिया गया है। यह निर्णय करता है कि क्या वे एक ही तत्व का प्रतिनिधित्व करते हैं। इस प्रकार के एल्गोरिदम को शब्द समस्या का समाधान कहा जाता है। उदाहरण के लिए, माना कि वास्तविक संख्याओं का प्रतिनिधित्व करने वाले प्रतीक हैं। तो इनपुट दिए जाने पर शब्द समस्या का एक प्रासंगिक समाधान होगा और EQUAL उत्पाद है। इसी प्रकार NOT_EQUAL से . उत्पादन करते हैं।

शब्द समस्या का सबसे सीधा एवं सरल समाधान सामान्य प्रमेय और एल्गोरिथ्म का रूप लेता है। जो प्रत्येक तत्व को भावों के समतुल्य वर्ग में नियम फॉर्म के रूप में ज्ञात एकल एन्कोडिंग में मैप करता है। शब्द समस्या तब इन सामान्य रूपों की तुलना वाक्यगत समानता करके हल की जाती है।[1] उदाहरण के लिए कोई यह सुनिश्चित कर सकता है कि का सामान्य रूप है। , , और और उन भावों को उस रूप में फिर से लिखने के लिए एक परिवर्तन प्रणाली तैयार करें। इस प्रक्रिया में यह सिद्ध करते हुए कि सभी समान भावों को उसी सामान्य रूप में फिर से लिखा जाएगा।[2] किन्तु शब्द समस्या के सभी समाधान सामान्य रूप प्रमेय का उपयोग नहीं करते हैं। ऐसे बीजीय गुण हैं, जो अप्रत्यक्ष रूप से एल्गोरिथम के प्रमाण का संकेत देते हैं।[1]

जबकि शब्द समस्या पूछती है कि क्या स्थिरांक (गणित) वाले दो शब्द समान हैं। शब्द समस्या का एक उचित विस्तार, जिसे एकीकरण (कंप्यूटर विज्ञान) के रूप में जाना जाता है, पूछता है कि क्या दो शब्द वेरिएबल (गणित) वाले ऐसे उदाहरण हैं। जो बराबर हैं या दूसरे शब्दों में समीकरण हैं। एक सामान्य उदाहरण के रूप में पूर्णांक बीजगणितीय गुणों में शब्द समस्या है। पूर्णांक समूह ℤ है।

जबकि एक ही समूह में एकीकरण की समस्या है। चूंकि पूर्व नियम ℤ में बराबर होती हैं। बाद की समस्या में प्रतिस्थापन (तर्क) एक समाधान के रूप में होता है।

इतिहास

शब्द समस्या के सबसे गहन अध्ययन वाले स्थितियों में से एक सेमीग्रुप और समूह (गणित) के सिद्धांत में है। नोविकोव-बूने सिद्धांत से संबंधित कागज की एक समयरेखा इस प्रकार है:[3][4]

  • 1910: एक्सल थू ने पेड़ जैसी संरचनाओं पर शब्द पुनर्लेखन की एक सामान्य समस्या पेश की। वह कहते हैं कि "सबसे सामान्य स्थितियों में इस समस्या का समाधान संभवतः अनगिनत कठिनाइयों से जुड़ा हो सकता है"।
  • 1911: मैक्स डेह्न ने अंतिम रूप से प्रस्तुत समूहों के लिए शब्द समस्या प्रस्तुत की।
  • 1912: डेन के एल्गोरिथ्म को प्रस्तुत करता है और यह सिद्ध करता है कि यह 2 से अधिक या उसके बराबर जीनस के बंद उन्मुख द्वि-आयामी कई गुना के मौलिक समूहों के लिए शब्द समस्या को हल करता है। बाद के लेखकों ने समूह सैद्धांतिक निर्णय समस्याओं की एक विस्तृत श्रृंखला के लिए इसे अधिक विस्तारित किया है।
  • 1914: एक्सल थू ने सूक्ष्म रूप से प्रस्तुत अर्धसमूहों के लिए शब्द समस्या प्रस्तुत की।
  • 1930 - 1938: चर्च-ट्यूरिंग थीसिस उभरती है। संगणनीयता और अनिर्वचनीयता की औपचारिक धारणाओं को परिभाषित करती है।
  • 1947: एमिल पोस्ट और एंड्री मार्कोव जूनियर स्वतंत्र रूप से अघुलनशील शब्द समस्या के साथ सूक्ष्म रूप से प्रस्तुत अर्धसमूहों का निर्माण करते हैं। पोस्ट का निर्माण ट्यूरिंग मशीनों पर किया गया है। जबकि मार्कोव पोस्ट के सामान्य प्रणाली का उपयोग करता है।
  • 1950: पोस्ट के निर्माण को आगे बढ़ाकर एलन ट्यूरिंग दिखाते हैं कि नष्ट किए गए सेमीग्रुप्स के लिए शब्द समस्या अघुलनशील है। प्रमाणन का पालन करना कठिन है। किन्तु समूहों के लिए शब्द समस्या में एक महत्वपूर्ण मोड़ है।
  • 1955: प्योत्र नोविकोव ने पहला प्रकाशित प्रमाण दिया कि ट्यूरिंग के नष्ट करने के सेमीग्रुप परिणाम का उपयोग करते हुए समूहों के लिए शब्द समस्या अघुलनशील है। प्रमाण में ब्रिटन के लेम्मा के बराबर एक "प्रिंसिपल लेम्मा" है।
  • 1954 - 1957: पोस्ट के सेमीग्रुप निर्माण का उपयोग करते हुए विलियम बून स्वतंत्र रूप से समूहों के लिए शब्द समस्या को हल करने योग्य नहीं दिखाते हैं।
  • 1957 - 1958: जॉन ब्रिटन ने एक और प्रमाण दिया कि समूहों के लिए शब्द समस्या अघुलनशील है। जो ट्यूरिंग के निरस्तीकरण सेमिग्रुप परिणाम और ब्रिटन के कुछ पहले के काम पर आधारित है। [20] ब्रिटन के लेम्मा का एक प्रारंभिक संस्करण प्रकट होता है।
  • 1958 - 1959: बूने ने अपने निर्माण का एक सरलीकृत संस्करण प्रकाशित किया।
  • 1961: ग्राहम हिगमैन, हिगमैन के एम्बेडिंग प्रमेय के साथ अंतिम रूप से प्रस्तुत समूहों के उपसमूहों की विशेषता बताता है। समूह सिद्धांत के साथ पुनरावर्तन सिद्धांत को अप्रत्याशित उपायों से जोड़ता है और शब्द समस्या की असम्बद्धता का एक बहुत अलग प्रमाण देता है।
  • 1961 - 1963: ब्रिटन ने बूने के 1959 के प्रमाण का एक बहुत ही सरलीकृत संस्करण प्रस्तुत किया कि समूहों के लिए शब्द समस्या हल नहीं हो सकती है। यह एक समूह-सैद्धांतिक दृष्टिकोण का उपयोग करता है, विशेष रूप से ब्रिटन की लेम्मा में। इस प्रमाण का उपयोग स्नातक पाठ्यक्रम में किया गया है। चूंकि अधिक आधुनिक और संघनित प्रमाण उपस्थित हैं।
  • 1977: गेन्नेडी माकानिन ने सिद्ध किया कि मुक्त मोनोइड्स पर समीकरणों का अस्तित्व सिद्धांत हल करने योग्य है।

सेमी-थ्यू प्रणाली के लिए शब्द समस्या

स्ट्रिंग पुनर्लेखन प्रणाली (सेमी-थ्यू प्रणाली या सेमीग्रुप) के लिए एक्सेसिबिलिटी समस्या निम्नानुसार बताई जा सकती है: एक सेमी-थ्यू प्रणाली दिया गया और दो शब्द (तार) में बदलकर से नियम संचालित करें। ध्यान दें कि यहाँ पुनर्लेखन एक ओर है। शब्द समस्या सममित पुनर्लेखन संबंधों अर्थात् थ्यू प्रणाली के लिए अभिगम्यता समस्या है।[5]

अभिगम्यता और शब्द समस्याएँ अनिर्णीत समस्याएँ हैं, अर्थात इस समस्या को हल करने के लिए कोई सामान्य एल्गोरिद्म नहीं है।[6] यह तब भी होता है, जब हम प्रणाली को सीमित प्रस्तुतियों तक सीमित करते हैं, अर्थात् प्रतीकों का एक सीमित समूह और उन प्रतीकों पर संबंधों का एक सीमित समूह[5]यहां तक ​​​​कि निचले शब्दों तक सीमित शब्द समस्या भी निश्चित रूप से प्रस्तुत अर्धसमूहों के लिए निर्णायक नहीं है।[7][8]


समूहों के लिए शब्द समस्या

समूह G के लिए प्रस्तुति दी। शब्द समस्या निर्णय लेने की एल्गोरिथम समस्या है। जो S में इनपुट दो शब्दों के रूप में दी गई है। क्या वे G के समान तत्व का प्रतिनिधित्व करते हैं। शब्द समस्या 1911 में मैक्स डेहन द्वारा प्रस्तावित समूहों के लिए तीन एल्गोरिथम समस्याओं में से एक है। यह 1955 में पीटर नोविकोव द्वारा दिखाया गया था कि एक सूक्ष्म रूप से प्रस्तुत समूह G उपस्थित है। जैसे कि G के लिए शब्द समस्या अनिर्णीत समस्या है।[9]


कॉम्बिनेटरियल कैलकुलस और लैम्ब्डा कैलकुलस में वर्ड प्रॉब्लम =

सबसे प्रारम्भिकप्रमाणों में से एक है कि एक शब्द समस्या अनिर्णीत है। जो संयोजन तर्क के लिए थी। कॉम्बिनेटर के दो तार कब बराबर होते हैं? क्योंकि कॉम्बिनेटर सभी संभव ट्यूरिंग मशीनों को एनकोड करते हैं और दो ट्यूरिंग मशीनों की समानता अनिर्णीत है। यह इस प्रकार है कि कॉम्बिनेटर के दो स्ट्रिंग्स की समानता अनिर्णीत है। 1936 में अलोंजो चर्च ने इसका अवलोकन किया।[10]

इसी प्रकार (अनटाइप्ड) लैम्ब्डा कैलकुलस में अनिवार्य रूप से एक ही समस्या है। दो अलग-अलग लैम्ब्डा एक्सप्रेशन दिए गए हैं। कोई एल्गोरिथ्म नहीं है, जो यह बता सके कि वे समकक्ष हैं या नहीं। लैम्ब्डा कैलकुलस तुल्यता की अनिश्चितता लैम्ब्डा कैलकुस के कई टाइप किए गए रूपों के लिए सामान्य रूपों की तुलना करके समानता निर्णायक है।

सार पुनर्लेखन प्रणाली के लिए शब्द समस्या

शब्द समस्या को हल करना: यदि निर्धारित करना सामान्यतः अनुमानी खोज की आवश्यकता होती है। (लाल, हरा), निर्णय लेते समय (ग्रे) सीधा है।

सार पुनर्लेखन प्रणाली (एआरएस) के लिए शब्द समस्या अधिक संक्षिप्त है। दी गई वस्तुएँ x और y के अंतर्गत वे समतुल्य हैं ?[7] एआरएस के लिए शब्द समस्या सामान्य रूप से अनिर्णीत समस्या है। चूंकि विशिष्ट स्थितियों में शब्द समस्या के लिए एक संगणनीय कार्य समाधान है। जहाँ प्रत्येक वस्तु एक विशिष्ट सामान्य रूप में चरणों की एक सीमित संख्या में घट जाती है (अर्थात प्रणाली अभिसारी है)। दो वस्तुएँ समतुल्य हैं। यदि और केवल यदि वे एक ही सामान्य रूप में कम हो जाते हैं।[11]

नुथ-बेंडिक्स पूर्णता एल्गोरिथम का उपयोग समीकरणों के एक समूह को अभिसरण शब्द पुनर्लेखन प्रणाली में बदलने के लिए किया जा सकता है।

सार्वभौमिक बीजगणित में शब्द समस्या

सार्वभौमिक बीजगणित में बीजीय संरचनाओं का अध्ययन करता है। जिसमें एक जनरेटिंग समूह A, परिमित एरिटी (सामान्यतः बाइनरी ऑपरेशंस) के A पर संचालन का एक संग्रह होता है और पहचान का एक परिमित समूह होता है। जिसे इन ऑपरेशनों को पूरा करना चाहिए। एक बीजगणित के लिए शब्द समस्या तब निर्धारित करने के लिए है। दो भाव (शब्द) दिए गए हैं, जिनमें जनरेटर और संचालन सम्मिलित है। फिर वे बीजगणित मॉड्यूलो के समान तत्व का प्रतिनिधित्व करते हों। समूहों और अर्धसमूहों के लिए शब्द समस्याओं को बीजगणित के लिए शब्द समस्याओं के रूप में अभिव्यक्त किया जा सकता है।[1]

मुक्त हेटिंग बीजगणित पर शब्द समस्या कठिन है।[12] एकमात्र ज्ञात परिणाम यह है कि एक जनरेटर पर मुफ्त हेटिंग बीजगणित अनंत है और यह कि एक जनरेटर पर मुक्त पूर्ण हेटिंग बीजगणित उपस्थित है (और मुक्त हेटिंग बीजगणित की तुलना में एक और तत्व है)।

मुक्त जालक के लिए शब्द समस्या

उदाहरण की गणना xz ~ xz∧(xy)
xz∧(xy) ~ xz
5 के द्वारा तब से xz ~ xz
1के द्वारा तब से xz = xz
 
 
xz ~ xz∧(xy)
7 के द्वारा तब से xz ~ xz और xz ~ xy
1 के द्वारा तब से xz = xz 6 के द्वारा तब से xz ~ x
5 के द्वारा तब से x ~ x
1 के द्वारा तब से x = x

मुक्त जालक और अधिक सामान्यतःमुक्त जालक (आदेश) पर शब्द समस्या का एक निर्णायक समाधान है। बाउंडेड लैटिस दो बाइनरी ऑपरेशंस ∨ और ∧ और दो स्थिरांक (शून्य संचालन) 0 और 1 के साथ बीजगणितीय संरचनाएं हैं। सभी अच्छी प्रकार से गठित शब्द (लॉजिक) का समूह जो दिए गए समूह से तत्वों पर इन ऑपरेशंस का उपयोग करके तैयार किया जा सकता है। जेनरेटर X को W(X) कहा जाएगा। शब्दों के इस समूह में कई अभिव्यक्तियां होती हैं जो प्रत्येक जालक में समान मूल्यों को दर्शाती हैं। उदाहरण के लिए यदि a, X का कोई अवयव है। तो a ∨ 1 = 1 और a∧ 1 =a मुक्त परिबद्ध जालक के लिए शब्द समस्या यह निर्धारित करने की समस्या है कि W(X) के इन तत्वों में से कौन सा तत्व मुक्त बाध्य जालक FX में समान तत्व को दर्शाता है और इसलिए प्रत्येक बाध्य जालक में उपस्थित होगा।

शाब्दिक समस्या का समाधान इस प्रकार किया जा सकता है कि एक संबंध ≤~ W(X) पर w ≤ समूह करके ~ v गणितीय आगमन को परिभाषित किया जा सकता है। यदि और केवल यदि निम्न में से कोई एक धारण करता है:

  1.   w = v (इसे उस स्थिति तक सीमित रखा जा सकता है। जहां w और v X के अवयव हैं),
  2.   w = 0,
  3.   v = 1,
  4.   w = w1w2 और दोनों w1~ v और w2~ v पकड़ती है।
  5.   w = w1w2 और या w1~ v या w2~ v पकड़ती है।
  6.   v = v1v2 और या w~ v1 या w~ v2 पकड़ती है।
  7.  v = v1v2 और दोनों w~ v1 और w~ v2 पकड़ती है।

यह एक पूर्व आदेश ≤ W(X) पर परिभाषित करता है। इसलिए एक तुल्यता संबंध को w ~ v द्वारा परिभाषित किया जा सकता है। जब w~ v and v~ w तब कोई यह दिखा सकता है कि आंशिक रूप से आदेशित भागफल समुच्चय 'W'(X)/~ मुक्त परिबद्ध जालक FX है।[13][14] W(X)/~ के समतुल्य वर्ग सभी शब्दों w और v के साथ w~ v और v~ w के समुच्चय हैं। 'W'(X) में दो सुगठित शब्द v और w प्रत्येक बंधे हुए जालक में समान मान को दर्शाते हैं। यदि और केवल यदि w~ v और v~ w उपरोक्त आगमनात्मक परिभाषा का उपयोग करके बाद की स्थितियों को प्रभावी ढंग से तैयार किया जा सकता है। सारणी यह दिखाने के लिए एक उदाहरण संगणना दिखाती है कि x∧z और x∧z∧(x∨y) शब्द प्रत्येक बंधे हुए जालक में समान मान को दर्शाते हैं। जालक के स्थितियों ऊपर के निर्माण में, जो बंधे नहीं हैं, नियम 2 और 3 को छोड़कर ≤~ उसी प्रकार से व्यवहार किया जाता है।


उदाहरण: मुक्त समूह में शब्द समस्या निर्धारित करने के लिए एक शब्द पुनर्लेखन प्रणाली

[15]

ब्लासियस और बर्कर्ट समूहों के लिए एक स्वयंसिद्ध समूह पर नुथ-बेंडिक्स एल्गोरिथम प्रदर्शित करें।

एल्गोरिथ्म एक संगम (सार पुनर्लेखन) और सार पुनर्लेखन प्रणाली समाप्ति और अभिसरण पुनर्लेखन प्रणाली शब्द पुनर्लेखन प्रणाली उत्पन्न करता है। जो प्रत्येक शब्द को एक अद्वितीय सामान्य रूप (सार पुनर्लेखन) में बदल देता है।[16] पुनर्लेखन नियमों को अस्पष्ट रूप से क्रमांकित किया गया है क्योंकि कुछ नियम नष्ट हो गए थे और एल्गोरिथम रन के समय हटा दिए गए थे।

दो शब्दों की समानता स्वयंसिद्धों से होती है। यदि और केवल यदि दोनों शब्दों को शाब्दिक रूप से समान सामान्य रूप में रूपांतरित किया जाता है। उदाहरण के लिए, नियम

, और

समान सामान्य रूप साझा करें अर्थात। । इसलिए दोनों शब्द प्रत्येक समूह में समान हैं।

एक अन्य उदाहरण के रूप में शब्द और सामान्य रूप क्रमश और , है । चूँकि सामान्य रूप वस्तुतः भिन्न होते हैं। मूल शब्द प्रत्येक समूह में समान नहीं हो सकते। वास्तविक रूप में वे सामान्यतःएबेलियन समूह गैर-एबेलियन समूहों में भिन्न होते हैं।

नुथ-बेंडिक्स पूर्णता में प्रयुक्त समूह अभिगृहीत
A1
A2
A3    
नुथ-बेंडिक्स पूर्णता से प्राप्त शब्द पुनर्लेखन प्रणाली
R1
R2
R3
R4
R8
R11
R12
R13
R14
R17    

यह भी देखें

संदर्भ

  1. 1.0 1.1 1.2 1.3 Evans, Trevor (1978). "शब्द की समस्याएं". Bulletin of the American Mathematical Society. 84 (5): 790. doi:10.1090/S0002-9904-1978-14516-9.
  2. Cohen, Joel S. (2002). Computer algebra and symbolic computation: elementary algorithms. Natick, Mass.: A K Peters. pp. 90–92. ISBN 1568811586.
  3. Miller, Charles F. (2014). Downey, Rod (ed.). "शब्द समस्याओं के लिए ट्यूरिंग मशीन" (PDF). Turing's Legacy: 330. doi:10.1017/CBO9781107338579.010. hdl:11343/51723. ISBN 9781107338579. Retrieved 6 December 2021.
  4. Stillwell, John (1982). "समूहों के लिए शब्द समस्या और समरूपता समस्या". Bulletin of the American Mathematical Society. 6 (1): 33–56. doi:10.1090/S0273-0979-1982-14963-1.
  5. 5.0 5.1 Matiyasevich, Yuri; Sénizergues, Géraud (January 2005). "कुछ नियमों के साथ अर्ध-थू सिस्टम के लिए निर्णय समस्याएँ". Theoretical Computer Science. 330 (1): 145–169. doi:10.1016/j.tcs.2004.09.016.
  6. Davis, Martin (1978). "What is a Computation?" (PDF). Mathematics Today Twelve Informal Essays: 257–259. doi:10.1007/978-1-4613-9435-8_10. ISBN 978-1-4613-9437-2. Retrieved 5 December 2021.
  7. 7.0 7.1 Baader, Franz; Nipkow, Tobias (5 August 1999). टर्म पुनर्लेखन और वह सब (in English). Cambridge University Press. pp. 59–60. ISBN 978-0-521-77920-3.
  8. *Matiyasevich, Yu. V. (1967). "Простые примеры неразрешимых ассоциативных исчислений" [Simple examples of undecidable associative calculi]. Doklady Akademii Nauk SSSR (in Russian). 173 (6): 1264–1266. ISSN 0869-5652.{{cite journal}}: CS1 maint: unrecognized language (link)
    • Matiyasevich, Yu. V. (1967). "Simple examples of undecidable associative calculi". Soviet Mathematics. 8 (2): 555–557. ISSN 0197-6788.
  9. Novikov, P. S. (1955). "समूह सिद्धांत में शब्द समस्या की एल्गोरिदमिक असम्बद्धता पर". Trudy Mat. Inst. Steklov (in русский). 44: 1–143.
  10. Statman, Rick (2000). "कॉम्बिनेटर्स के लिए वर्ड प्रॉब्लम पर". Rewriting Techniques and Applications. Lecture Notes in Computer Science. 1833: 203–213. doi:10.1007/10721975_14. ISBN 978-3-540-67778-9.
  11. Beke, Tibor (May 2011). "Categorification, term rewriting and the Knuth–Bendix procedure". Journal of Pure and Applied Algebra. 215 (5): 730. doi:10.1016/j.jpaa.2010.06.019.
  12. Peter T. Johnstone, Stone Spaces, (1982) Cambridge University Press, Cambridge, ISBN 0-521-23893-5. (See chapter 1, paragraph 4.11)
  13. Whitman, Philip M. (January 1941). "मुक्त जाली". The Annals of Mathematics. 42 (1): 325–329. doi:10.2307/1969001. JSTOR 1969001.
  14. Whitman, Philip M. (1942). "मुक्त जाली II". Annals of Mathematics. 43 (1): 104–115. doi:10.2307/1968883. JSTOR 1968883.
  15. K. H. Bläsius and H.-J. Bürckert, ed. (1992). कटौती प्रणाली. Oldenbourg. p. 291.; here: p.126, 134
  16. Apply rules in any order to a term, as long as possible; the result doesn't depend on the order; it is the term's normal form.