एकीकरण (कंप्यूटर विज्ञान): Difference between revisions
No edit summary |
No edit summary |
||
Line 9: | Line 9: | ||
उच्च-क्रम एकीकरण का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है, उदाहरण के लिए इसाबेल और [[बारह|ट्वेल्व]] और उच्च-क्रम एकीकरण के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग [[लैम्डैप्रोलॉग]], के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न अभिव्यंजक के रूप में होते हैं, फिर भी उनकी संबद्ध एकीकरण प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम एकीकरण के रूप में निकट बनाए रखती है। | उच्च-क्रम एकीकरण का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है, उदाहरण के लिए इसाबेल और [[बारह|ट्वेल्व]] और उच्च-क्रम एकीकरण के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग [[लैम्डैप्रोलॉग]], के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न अभिव्यंजक के रूप में होते हैं, फिर भी उनकी संबद्ध एकीकरण प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम एकीकरण के रूप में निकट बनाए रखती है। | ||
==औपचारिक | =='''औपचारिक लैंग्वेज'''== | ||
एकीकरण समस्या एक सीमित समुच्चय के रूप में है {{math|1=''E''={{mset| ''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}}} समीकरणों को हल करना है, जहाँ {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub>}} सेट में हैं <math>T</math> शब्दों या अभिव्यक्तियों का. समीकरण सेट या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति दी जाती है और किस अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात [[फ़ंक्शन (गणित)|फलन (गणित)]] का प्रतिनिधित्व करने वाले चर, को एक अभिव्यक्ति में अनुमति दी जाती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है, अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई-एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है। | एकीकरण समस्या एक सीमित समुच्चय के रूप में है {{math|1=''E''={{mset| ''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}}} समीकरणों को हल करना है, जहाँ {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub>}} सेट में हैं <math>T</math> शब्दों या अभिव्यक्तियों का. समीकरण सेट या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति दी जाती है और किस अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात [[फ़ंक्शन (गणित)|फलन (गणित)]] का प्रतिनिधित्व करने वाले चर, को एक अभिव्यक्ति में अनुमति दी जाती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है, अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई-एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है। | ||
यदि प्रत्येक समीकरण का दाहिना भाग बंद है, को E मुक्त चर नहीं है, तो समस्या को पैटर्न मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर चर के साथ पैटर्न का रूप कहा जाता है।<ref>{{cite book |last1=Dowek |first1=Gilles |title=स्वचालित तर्क की पुस्तिका|date=1 January 2001 |publisher=Elsevier Science Publishers B. V. |isbn=978-0-444-50812-6 |pages=1009–1062 |url=http://www.lsv.fr/~dowek/Publi/unification.ps |chapter=Higher-order unification and matching}}</ref> | यदि प्रत्येक समीकरण का दाहिना भाग बंद है, को E मुक्त चर नहीं है, तो समस्या को पैटर्न मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर चर के साथ पैटर्न का रूप कहा जाता है।<ref>{{cite book |last1=Dowek |first1=Gilles |title=स्वचालित तर्क की पुस्तिका|date=1 January 2001 |publisher=Elsevier Science Publishers B. V. |isbn=978-0-444-50812-6 |pages=1009–1062 |url=http://www.lsv.fr/~dowek/Publi/unification.ps |chapter=Higher-order unification and matching}}</ref> | ||
===आवश्यकताएँ=== | ==='''आवश्यकताएँ'''=== | ||
औपचारिक रूप से, एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है | औपचारिक रूप से, एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है | ||
* एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है <math>V</math> [[लैम्ब्डा-टर्म बाध्य चर]] के सेट से भिन्न हो गया है। | * एक अनंत समुच्चय <math>V</math> चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है <math>V</math> [[लैम्ब्डा-टर्म बाध्य चर]] के सेट से भिन्न हो गया है। | ||
Line 25: | Line 25: | ||
उच्च-क्रम एकीकरण के उदाहरण के रूप में एकल सेट { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक समाधान के रूप में है {x ↦ a, y ↦ (पहचान फलन) }; दूसरा है { y ↦ (निरंतर फलन प्रत्येक मान को a पर मैप करता है), x ↦ (को E भी मान) } होता है। | उच्च-क्रम एकीकरण के उदाहरण के रूप में एकल सेट { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक समाधान के रूप में है {x ↦ a, y ↦ (पहचान फलन) }; दूसरा है { y ↦ (निरंतर फलन प्रत्येक मान को a पर मैप करता है), x ↦ (को E भी मान) } होता है। | ||
===प्रतिस्थापन=== | ==='''प्रतिस्थापन'''=== | ||
{{main|Substitution (logic)}} | {{main|Substitution (logic)}} | ||
प्रतिस्थापन एक मानचित्रण है <math>\sigma: V\rightarrow T</math> चर से पदों तक; संकेतन <math> \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}</math> प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है <math>x_i</math> पद के लिए <math>t_i</math>, के लिए <math>i=1,...,k</math>, और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर लागू करना <math>t</math> [[ उपसर्ग संकेतन ]] में इस प्रकार लिखा गया है <math>t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}</math>; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना <math>x_i</math> अवधि में <math>t</math> द्वारा <math>t_i</math>. परिणाम <math>t\tau</math> प्रतिस्थापन लागू करने का <math>\tau</math> एक पद के लिए <math>t</math> उस पद का उदाहरण कहा जाता है <math>t</math>. | प्रतिस्थापन एक मानचित्रण है <math>\sigma: V\rightarrow T</math> चर से पदों तक; संकेतन <math> \{x_1\mapsto t_1, ..., x_k \mapsto t_k\}</math> प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है <math>x_i</math> पद के लिए <math>t_i</math>, के लिए <math>i=1,...,k</math>, और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर लागू करना <math>t</math> [[ उपसर्ग संकेतन ]] में इस प्रकार लिखा गया है <math>t \{x_1 \mapsto t_1, ..., x_k \mapsto t_k\}</math>; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना <math>x_i</math> अवधि में <math>t</math> द्वारा <math>t_i</math>. परिणाम <math>t\tau</math> प्रतिस्थापन लागू करने का <math>\tau</math> एक पद के लिए <math>t</math> उस पद का उदाहरण कहा जाता है <math>t</math>. | ||
Line 49: | Line 49: | ||
|} | |} | ||
===सामान्यीकरण, विशेषज्ञता=== | ==='''सामान्यीकरण, विशेषज्ञता'''=== | ||
यदि एक शब्द <math>t</math> एक पद के समतुल्य एक उदाहरण है <math>u</math>, अर्थात्, यदि <math>t\sigma \equiv u</math> कुछ प्रतिस्थापन के लिए <math>\sigma</math>, तब <math>t</math> से अधिक सामान्य कहा जाता है <math>u</math>, और <math>u</math> से अधिक विशेष कहा जाता है, या उसमें सम्मिलित किया जाता है, <math>t</math>. उदाहरण के लिए, <math>x\oplus a</math> से अधिक सामान्य है <math>a\oplus b</math> यदि ⊕ क्रमविनिमेय संपत्ति है, तब से <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>. | यदि एक शब्द <math>t</math> एक पद के समतुल्य एक उदाहरण है <math>u</math>, अर्थात्, यदि <math>t\sigma \equiv u</math> कुछ प्रतिस्थापन के लिए <math>\sigma</math>, तब <math>t</math> से अधिक सामान्य कहा जाता है <math>u</math>, और <math>u</math> से अधिक विशेष कहा जाता है, या उसमें सम्मिलित किया जाता है, <math>t</math>. उदाहरण के लिए, <math>x\oplus a</math> से अधिक सामान्य है <math>a\oplus b</math> यदि ⊕ क्रमविनिमेय संपत्ति है, तब से <math>(x\oplus a) \{x\mapsto b\} = b\oplus a\equiv a\oplus b</math>. | ||
Line 74: | Line 74: | ||
<math>f(x, y) \tau = f(y, y)</math>.<ref>{{cite book |last1=Apt |first1=Krzysztof R. |title=लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक|date=1997 |publisher=Prentice Hall |location=London Munich |isbn=013230368X |edition=1. publ |url=https://homepages.cwi.nl/~apt/book.ps|p=24}}</ref><nowiki>}} के रूप में होता है.</nowiki> | <math>f(x, y) \tau = f(y, y)</math>.<ref>{{cite book |last1=Apt |first1=Krzysztof R. |title=लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक|date=1997 |publisher=Prentice Hall |location=London Munich |isbn=013230368X |edition=1. publ |url=https://homepages.cwi.nl/~apt/book.ps|p=24}}</ref><nowiki>}} के रूप में होता है.</nowiki> | ||
===समाधान सेट=== | ==='''समाधान सेट'''=== | ||
एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक समाधान है यदि {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} के लिए <math>i = 1, ..., n</math>. ऐसे प्रतिस्थापन को Eका एकीकरणकर्ता भी कहा जाता है। | एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक समाधान है यदि {{math|''l''<sub>''i''</sub>σ ≡ ''r''<sub>''i''</sub>σ}} के लिए <math>i = 1, ..., n</math>. ऐसे प्रतिस्थापन को Eका एकीकरणकर्ता भी कहा जाता है। | ||
Line 84: | Line 84: | ||
समुच्चय ''S'' को न्यूनतम कहा जाता है यदि इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन सेट में शून्य, एक, परिमित रूप से कई या अनंत रूप से कई सदस्य हो सकते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्णतया भी उपलब्ध नहीं हो सकते हैं।<ref>{{cite journal|first1=François|last1=Fages|first2=Gérard|last2=Huet|title=समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट|journal=Theoretical Computer Science|volume=43|pages=189–200|year=1986|doi=10.1016/0304-3975(86)90175-1|doi-access=free}}</ref> इस प्रकार, सामान्यतः, एकीकरण एल्गोरिदम पूर्ण सेट के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम हो भी सकता है और नहीं भी हो सकते है, चूंकि अधिकांश एल्गोरिदम जब संभव हो तो निरर्थक एकीकरणकर्ताओं से बचते हैं।<ref name="Vukmirovic" />प्रथम-क्रम वाक्यात्मक एकीकरण के लिए, मार्टेली और मोंटानारी<ref name="Martelli.Montanari.1982">{{cite journal|first1=Alberto|last1=Martelli|first2=Ugo|last2=Montanari|title=एक कुशल एकीकरण एल्गोरिदम|journal=ACM Trans. Program. Lang. Syst.|volume=4|number=2|pages=258–282|date=Apr 1982|doi=10.1145/357162.357169|s2cid=10921306}}</ref> एक एल्गोरिदम दिया जाता है, जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन सेट के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है। | समुच्चय ''S'' को न्यूनतम कहा जाता है यदि इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन सेट में शून्य, एक, परिमित रूप से कई या अनंत रूप से कई सदस्य हो सकते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्णतया भी उपलब्ध नहीं हो सकते हैं।<ref>{{cite journal|first1=François|last1=Fages|first2=Gérard|last2=Huet|title=समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट|journal=Theoretical Computer Science|volume=43|pages=189–200|year=1986|doi=10.1016/0304-3975(86)90175-1|doi-access=free}}</ref> इस प्रकार, सामान्यतः, एकीकरण एल्गोरिदम पूर्ण सेट के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम हो भी सकता है और नहीं भी हो सकते है, चूंकि अधिकांश एल्गोरिदम जब संभव हो तो निरर्थक एकीकरणकर्ताओं से बचते हैं।<ref name="Vukmirovic" />प्रथम-क्रम वाक्यात्मक एकीकरण के लिए, मार्टेली और मोंटानारी<ref name="Martelli.Montanari.1982">{{cite journal|first1=Alberto|last1=Martelli|first2=Ugo|last2=Montanari|title=एक कुशल एकीकरण एल्गोरिदम|journal=ACM Trans. Program. Lang. Syst.|volume=4|number=2|pages=258–282|date=Apr 1982|doi=10.1145/357162.357169|s2cid=10921306}}</ref> एक एल्गोरिदम दिया जाता है, जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन सेट के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है। | ||
==प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण== | =='''प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण'''== | ||
[[File:Triangle diagram of syntactic unification svg.svg|thumb|वाक्यविन्यास की दृष्टि से एकीकृत शब्दों का योजनाबद्ध त्रिभुज आरेख टी<sub>1</sub> और टी<sub>2</sub> एक प्रतिस्थापन द्वारा पी]]प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है। | [[File:Triangle diagram of syntactic unification svg.svg|thumb|वाक्यविन्यास की दृष्टि से एकीकृत शब्दों का योजनाबद्ध त्रिभुज आरेख टी<sub>1</sub> और टी<sub>2</sub> एक प्रतिस्थापन द्वारा पी]]प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है। | ||
यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)<sub>''n''</sub> n-ary फलन प्रतीकों का और ≡ वाक्यात्मक समानता पर आधारित है। | यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)<sub>''n''</sub> n-ary फलन प्रतीकों का और ≡ वाक्यात्मक समानता पर आधारित है। | ||
Line 125: | Line 125: | ||
एक अन्य उदाहरण के रूप में, समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई समाधान नहीं है, क्योंकि बाएं और दाएं तरफ लागू कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मक रूप से भिन्न होते हैं। | एक अन्य उदाहरण के रूप में, समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई समाधान नहीं है, क्योंकि बाएं और दाएं तरफ लागू कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मक रूप से भिन्न होते हैं। | ||
===एक एकीकरण एल्गोरिथ्म=== | ==='''एक एकीकरण एल्गोरिथ्म'''=== | ||
{{Quote box|title=Robinson's 1965 unification algorithm | {{Quote box|title=Robinson's 1965 unification algorithm | ||
|quote={{hidden begin}} | |quote={{hidden begin}} | ||
Line 214: | Line 214: | ||
====चेक होता है==== | ===='''चेक होता है'''==== | ||
{{main|Occurs check}} | {{main|Occurs check}} | ||
एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के समाधान के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है. | एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के समाधान के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है. | ||
Line 224: | Line 224: | ||
सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का #एकीकरण के रूप में देख़ते है। | सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का #एकीकरण के रूप में देख़ते है। | ||
====समाप्ति का प्रमाण==== | ===='''समाप्ति का प्रमाण'''==== | ||
एल्गोरिथम की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> | एल्गोरिथम की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें <math>\langle n_{var}, n_{lhs}, n_{eqn}\rangle</math> | ||
Line 243: | Line 243: | ||
[[कॉनर मैकब्राइड]] देखते हैं<ref>{{cite journal|last=McBride|first=Conor|title=संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> [[एपिग्राम (प्रोग्रामिंग भाषा)|एपिग्राम (प्रोग्रामिंग लैंग्वेज)]] जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण एल्गोरिदम को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है। | [[कॉनर मैकब्राइड]] देखते हैं<ref>{{cite journal|last=McBride|first=Conor|title=संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण|journal=Journal of Functional Programming|date=October 2003|volume=13|issue=6|pages=1061–1076|doi=10.1017/S0956796803004957|url=http://strictlypositive.org/unify.ps.gz|access-date=30 March 2012|issn=0956-7968|citeseerx=10.1.1.25.1516|s2cid=43523380 }}</ref> [[एपिग्राम (प्रोग्रामिंग भाषा)|एपिग्राम (प्रोग्रामिंग लैंग्वेज)]] जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण एल्गोरिदम को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है। | ||
===प्रथम-क्रम शब्दों के वाक्यात्मक एकीकरण के उदाहरण=== | ==='''प्रथम-क्रम शब्दों के वाक्यात्मक एकीकरण के उदाहरण'''=== | ||
प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है। | प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है। | ||
Line 287: | Line 287: | ||
[[File:Unification exponential blow-up svg.svg|thumb|अपने कम से कम सामान्य उदाहरण के लिए तेजी से बड़े पेड़ वाले दो शब्द। इसका निर्देशित चक्रीय आलेख प्रतिनिधित्व (सबसे दाहिना, नारंगी भाग) अभी भी रैखिक बनावट का है।]]टर्म (तर्क)#शब्दों के साथ संचालन की वाक्यात्मक प्रथम-क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता {{mvar|n}} के रूप में बनावट हो सकता है {{math|2<sup>''n''</sup>}}. उदाहरण के लिए समस्या {{tmath| (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) }} में सबसे सामान्य एकीकरणकर्ता है' {{tmath| \{ z \mapsto a, y \mapsto a*a, x \mapsto (a*a)*(a*a), w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण एल्गोरिदम पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।{{refn|e.g. Paterson, Wegman (1978),<ref name="Paterson.Wegman.1978"/> sect.2, p.159}} | [[File:Unification exponential blow-up svg.svg|thumb|अपने कम से कम सामान्य उदाहरण के लिए तेजी से बड़े पेड़ वाले दो शब्द। इसका निर्देशित चक्रीय आलेख प्रतिनिधित्व (सबसे दाहिना, नारंगी भाग) अभी भी रैखिक बनावट का है।]]टर्म (तर्क)#शब्दों के साथ संचालन की वाक्यात्मक प्रथम-क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता {{mvar|n}} के रूप में बनावट हो सकता है {{math|2<sup>''n''</sup>}}. उदाहरण के लिए समस्या {{tmath| (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) }} में सबसे सामान्य एकीकरणकर्ता है' {{tmath| \{ z \mapsto a, y \mapsto a*a, x \mapsto (a*a)*(a*a), w \mapsto ((a*a)*(a*a))*((a*a)*(a*a)) \} }}, सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण एल्गोरिदम पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।{{refn|e.g. Paterson, Wegman (1978),<ref name="Paterson.Wegman.1978"/> sect.2, p.159}} | ||
===अनुप्रयोग: तर्क प्रोग्रामिंग में एकीकरण=== | ==='''अनुप्रयोग: तर्क प्रोग्रामिंग में एकीकरण'''=== | ||
एकीकरण की अवधारणा तर्क प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे [[प्रोलॉग]] लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है <code>=</code> लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है <code>=</code>अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है <code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>. प्रकार अनुमान एल्गोरिदम सामान्यतः एकीकरण पर आधारित होते हैं। | एकीकरण की अवधारणा तर्क प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे [[प्रोलॉग]] लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है <code>=</code> लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है <code>=</code>अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है <code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>. प्रकार अनुमान एल्गोरिदम सामान्यतः एकीकरण पर आधारित होते हैं। | ||
Line 295: | Line 295: | ||
# इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है। | # इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है। | ||
=== अनुप्रयोग: प्रकार अनुमान === | === '''अनुप्रयोग: प्रकार अनुमान''' === | ||
कार्यात्मक लैंग्वेज [[हास्केल (प्रोग्रामिंग भाषा)|हास्केल (प्रोग्रामिंग लैंग्वेज)]] और [[एमएल (प्रोग्रामिंग भाषा)|एमएल (प्रोग्रामिंग लैंग्वेज)]] सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन | कार्यात्मक लैंग्वेज [[हास्केल (प्रोग्रामिंग भाषा)|हास्केल (प्रोग्रामिंग लैंग्वेज)]] और [[एमएल (प्रोग्रामिंग भाषा)|एमएल (प्रोग्रामिंग लैंग्वेज)]] सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल अभिव्यक्ति <code>ट्रू : ['x', 'y', 'z']</code> सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन <code>(:)</code> प्रकार का है <code>a -> [a] -> [a]</code>, और पहले तर्क के लिए<code>ट्रू</code>बहुरूपी प्रकार चर <code>a</code> के साथ एकाकार होना होगा <code>ट्रू</code>का प्रकार <code>बूल</code>. दूसरा तर्क, <code>['x', 'y', 'z']</code>, प्रकार का है <code>[चार]</code>, लेकिन <code>a</code> दोनों नहीं हो सकते <code>बूल</code> और<code>चार</code> एक ही समय पर होते है. | ||
प्रोलॉग के प्रकार अनुमान के लिए एक एल्गोरिदम दिया जा सकता है: | प्रोलॉग के प्रकार अनुमान के लिए एक एल्गोरिदम दिया जा सकता है: | ||
Line 308: | Line 308: | ||
ध्यान दें कि प्रथम-क्रम तर्क की शब्दावली में, एक परमाणु एक मूल प्रस्ताव है और प्रोलॉग शब्द के समान एकीकृत है। | ध्यान दें कि प्रथम-क्रम तर्क की शब्दावली में, एक परमाणु एक मूल प्रस्ताव है और प्रोलॉग शब्द के समान एकीकृत है। | ||
=== अनुप्रयोग: फ़ीचर संरचना एकीकरण === | === '''अनुप्रयोग: फ़ीचर संरचना एकीकरण''' === | ||
{{see also|Feature structure}} | {{see also|Feature structure}} | ||
अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।<ref>Jonathan Calder, Mike Reape, and Hank Zeevat,, [https://www.aclweb.org/anthology/E89-1032 An algorithm for generation in unification categorial grammar]. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.</ref><ref>Graeme Hirst and David St-Onge, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.8426] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.</ref> | अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।<ref>Jonathan Calder, Mike Reape, and Hank Zeevat,, [https://www.aclweb.org/anthology/E89-1032 An algorithm for generation in unification categorial grammar]. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.</ref><ref>Graeme Hirst and David St-Onge, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.8426] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.</ref> | ||
==क्रमानुसार एकीकरण== | =='''क्रमानुसार एकीकरण'''== | ||
[[क्रमबद्ध तर्क]] प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s<sub>2</sub>, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में तर्क करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है। | [[क्रमबद्ध तर्क]] प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s<sub>2</sub>, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में तर्क करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है। | ||
Line 332: | Line 332: | ||
उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक संपत्ति घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है। | उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक संपत्ति घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है। | ||
==अनंत पदों का एकीकरण== | =='''अनंत पदों का एकीकरण'''== | ||
{{expand section|date=December 2021}} | {{expand section|date=December 2021}} | ||
अनंत पेड़ों पर पृष्ठभूमि: | अनंत पेड़ों पर पृष्ठभूमि: | ||
Line 346: | Line 346: | ||
* {{cite journal|author1=Francis Giannesini |author2=Jacques Cohen | title=प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर| journal=Journal of Logic Programming| year=1984| volume=1|issue=3 | pages=253–265| doi=10.1016/0743-1066(84)90013-X| doi-access=free}} | * {{cite journal|author1=Francis Giannesini |author2=Jacques Cohen | title=प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर| journal=Journal of Logic Programming| year=1984| volume=1|issue=3 | pages=253–265| doi=10.1016/0743-1066(84)90013-X| doi-access=free}} | ||
==ई-एकीकरण== | =='''ई-एकीकरण'''== | ||
ई-एकीकरण [[समीकरण]] के दिए गए सेट का समाधान खोजने की समस्या है. | ई-एकीकरण [[समीकरण]] के दिए गए सेट का समाधान खोजने की समस्या है. | ||
Line 366: | Line 366: | ||
चूंकि यदि {{tmath|*}} क्रमविनिमेय माना जाता है, | चूंकि यदि {{tmath|*}} क्रमविनिमेय माना जाता है, | ||
फिर प्रतिस्थापन {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} उपरोक्त समीकरण को हल करता है, | फिर प्रतिस्थापन {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} उपरोक्त समीकरण को हल करता है, | ||
Line 377: | Line 378: | ||
| {{tmath|b * a}} | | {{tmath|b * a}} | ||
| | | | ||
| | | प्रतिस्थापन आवेदन द्वारा | ||
|- | |- | ||
| {{=}} | | {{=}} | ||
| {{tmath|a * b}} | | {{tmath|a * b}} | ||
| | | | ||
| | | की क्रमपरिवर्तनशीलता द्वारा {{tmath|*}} | ||
|- | |- | ||
| {{=}} | | {{=}} | ||
| {{tmath|y * b}} | | {{tmath|y * b}} | ||
| {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} | | {{math|{{mset|''x'' ↦ ''b'', ''y'' ↦ ''a''}}}} | ||
| | | (विपरीत) प्रतिस्थापन आवेदन द्वारा | ||
|} | |} | ||
पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है {{tmath|*}} सार्वभौम समानता द्वारा{{tmath|1=u * v = v * u}} सभी के लिए {{math|''u'', ''v''}} . | पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है {{tmath|*}} सार्वभौम समानता द्वारा{{tmath|1=u * v = v * u}} सभी के लिए {{math|''u'', ''v''}} . |
Revision as of 14:21, 29 July 2023
तर्क और कंप्यूटर विज्ञान में, एकीकरण प्रतीकात्मक अभिव्यक्ति (गणित) के बीच समीकरणों को हल करने की एक एल्गोरिथम प्रक्रिया का रूप है। उदाहरण के लिए, चर के रूप में x,y,z का उपयोग करते हुए, एकल समीकरण सेट { cons(x,cons(x,nil)) = cons(2,y) } एक वाक्यात्मक प्रथम-क्रम एकीकरण समस्या के रूप में है, जिसके पास प्रतिस्थापन {x ↦ 2, y ↦ cons(2,nil) } का एकमात्र समाधान होता है।
एकीकरण एल्गोरिथ्म की खोज सबसे पहले जैक्स हेरब्रांड ने की थी,[1][2][3] जबकि पहली औपचारिक जांच का श्रेय जॉन एलन रॉबिन्सन के रूप में दिया जाता है,[4][5] जिन्होंने प्रथम-क्रम तर्क के लिए अपने समाधान (तर्क) प्रक्रिया के बुनियादी निर्माण खंड के रूप में प्रथम-क्रम वाक्यात्मक एकीकरण का उपयोग किया जाता है, स्वचालित तर्क प्रौद्योगिकी में एक बड़ा कदम के रूप में आगे बढ़ाया जाता है, क्योंकि इसने संयोजन विस्फोट के एक स्रोत को समाप्त कर दिया था: यह संयोजन के रूप में एक स्रोत बन गया था। आज स्वचालित तर्क अभी भी एकीकरण का मुख्य अनुप्रयोग क्षेत्र का रूप है।
वाक्यात्मक प्रथम-क्रम एकीकरण का उपयोग तर्क प्रोग्रामिंग और प्रोग्रामिंग लैंग्वेज प्रकार प्रणाली कार्यान्वयन के रूप में किया जाता है, विशेष रूप से हिंडले-मिलनर आधारित प्रकार अनुमान एल्गोरिदम के रूप में होता है।
सिमेंटिक एकीकरण का उपयोग एसएमटी सॉल्वर्स, शब्द पुनर्लेखन एल्गोरिदम और क्रिप्टोआलेख़िक प्रोटोकॉल विश्लेषण के रूप में किया जाता है।
उच्च-क्रम एकीकरण का उपयोग प्रूफ़ सहायकों के रूप में किया जाता है, उदाहरण के लिए इसाबेल और ट्वेल्व और उच्च-क्रम एकीकरण के प्रतिबंधित रूपों का उपयोग कुछ प्रोग्रामिंग लैंग्वेज कार्यान्वयन के रूप में किया जाता है, चूकि कुछ प्रोग्रामिंग लैम्डैप्रोलॉग, के सीमित रूपों का उपयोग किया जाता है, क्योंकि उच्च-क्रम पैटर्न अभिव्यंजक के रूप में होते हैं, फिर भी उनकी संबद्ध एकीकरण प्रक्रिया सैद्धांतिक गुणों को प्रथम-क्रम एकीकरण के रूप में निकट बनाए रखती है।
औपचारिक लैंग्वेज
एकीकरण समस्या एक सीमित समुच्चय के रूप में है E={ l1 ≐ r1, ..., ln ≐ rn } समीकरणों को हल करना है, जहाँ li, ri सेट में हैं शब्दों या अभिव्यक्तियों का. समीकरण सेट या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति दी जाती है और किस अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात फलन (गणित) का प्रतिनिधित्व करने वाले चर, को एक अभिव्यक्ति में अनुमति दी जाती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है, अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई-एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है।
यदि प्रत्येक समीकरण का दाहिना भाग बंद है, को E मुक्त चर नहीं है, तो समस्या को पैटर्न मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर चर के साथ पैटर्न का रूप कहा जाता है।[6]
आवश्यकताएँ
औपचारिक रूप से, एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है
- एक अनंत समुच्चय चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है लैम्ब्डा-टर्म बाध्य चर के सेट से भिन्न हो गया है।
- एक सेट ऐसे शब्दों का . प्रथम-क्रम एकीकरण के लिए, सामान्यतः प्रथम-क्रम शब्दों चर और फलन प्रतीकों से निर्मित शब्द का सेट होता है। उच्च-क्रम एकीकरण के लिए इसमें प्रथम-क्रम वाले शब्द और लैम्ब्डा शब्द कुछ उच्च-क्रम वाले चर वाले शब्द के रूप में सम्मिलित होते हैं।
- एक मैपिंग संस्करण: पावर सेट|, प्रत्येक पद को निर्दिष्ट करना सेट में होने वाले मुक्त चर के रूप में होता है.
- एक सिद्धांत या तुल्यता संबंध पर , यह दर्शाता है कि कौन से पद समान माने जाते हैं। प्रथम-क्रम ई-एकीकरण के लिए, कुछ फलन प्रतीकों के बारे में पृष्ठभूमि ज्ञान को दर्शाता है; उदाहरण के लिए, यदि क्रमविनिमेय माना जाता है, यदि वहां से परिणाम मिले के तर्कों की अदला-बदली करके कुछ संभवतः सभी घटनाओं पर। [note 1] सबसे विशिष्ट स्थिति में जब कोई पृष्ठभूमि ज्ञान नहीं होता है, तो मात्र शाब्दिक रूप से या वाक्यात्मक रूप से समान शब्दों को समान माना जाता है। इस स्थिति में ≡ को मुक्त सिद्धांत कहा जाता है, क्योंकि यह एक स्वतंत्र वस्तु के रूप में है, खाली सिद्धांत क्योंकि समीकरण वाक्य (गणितीय तर्क) का सेट या पृष्ठभूमि ज्ञान के रूप में खाली है), अव्याख्यायित कार्यों का सिद्धांत पर किया जाता है, क्योंकि एकीकरण अनिर्वचनीय शब्द (तर्क)) या बीजगणितीय विनिर्देश के सिद्धांत के रूप में किया जाता है, क्योंकि सभी फलन प्रतीक मात्र उन पर काम करने के अतिरिक्त डेटा शब्द के रूप में बनाते हैं। सामान्यतः उच्च-क्रम एकीकरण के लिए यदि और अल्फ़ा समतुल्य होता है.
शब्दों और सिद्धांत का सेट समाधानों के सेट को कैसे प्रभावित करता है, इसके उदाहरण के रूप में वाक्यात्मक प्रथम-क्रम एकीकरण समस्या { y = cons(2,y) } का परिमित शब्दों के सेट पर कोई समाधान नहीं है। चूंकि, ट्री सेट सिद्धांत शर्तों के सेट पर इसका एकल समाधान के रूप में { y ↦ cons(2,cons(2,cons(2,...)) } होता है। इसी प्रकार सिमेंटिक प्रथम-क्रम एकीकरण समस्या { a⋅x = x⋅a } में फॉर्म का प्रत्येक प्रतिस्थापन { x ↦ a⋅...⋅a } एक अर्धसमूह में समाधान के रूप में होता है, अर्थात यदि (⋅) को साहचर्य माना जाता है, लेकिन वही समस्या जिसे एबेलियन समूह में देखा जाता है, जहां (⋅) को क्रमविनिमेय भी माना जाता है, समाधान के रूप में कोई भी प्रतिस्थापन होता है।
उच्च-क्रम एकीकरण के उदाहरण के रूप में एकल सेट { a = y(x) } एक वाक्यात्मक दूसरे क्रम की एकीकरण समस्या के रूप में होता है, क्योंकि y एक फलन चर है। एक समाधान के रूप में है {x ↦ a, y ↦ (पहचान फलन) }; दूसरा है { y ↦ (निरंतर फलन प्रत्येक मान को a पर मैप करता है), x ↦ (को E भी मान) } होता है।
प्रतिस्थापन
प्रतिस्थापन एक मानचित्रण है चर से पदों तक; संकेतन प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है पद के लिए , के लिए , और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर लागू करना उपसर्ग संकेतन में इस प्रकार लिखा गया है ; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना अवधि में द्वारा . परिणाम प्रतिस्थापन लागू करने का एक पद के लिए उस पद का उदाहरण कहा जाता है .
प्रथम-क्रम उदाहरण के रूप में प्रतिस्थापन लागू करना { x ↦ h(a,y), z ↦ b }शब्द के लिए होता है.
yields | |||||
सामान्यीकरण, विशेषज्ञता
यदि एक शब्द एक पद के समतुल्य एक उदाहरण है , अर्थात्, यदि कुछ प्रतिस्थापन के लिए , तब से अधिक सामान्य कहा जाता है , और से अधिक विशेष कहा जाता है, या उसमें सम्मिलित किया जाता है, . उदाहरण के लिए, से अधिक सामान्य है यदि ⊕ क्रमविनिमेय संपत्ति है, तब से .
यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी वाक्यात्मक संरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।
उदाहरण के लिए,
का एक प्रकार होता है
,
जब से
इसलिए पश्चात वाला शब्द पहले वाले की तुलना में उचित रूप से अधिक विशेष होता है।
मनमानी के लिए , एक शब्द संरचनात्मक रूप से भिन्न शब्द की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकता है।
उदाहरण के लिए, यदि ⊕ निष्क्रिय है, अर्थात यदि सदैव , फिर पद से अधिक सामान्य है ,[note 2] और इसके विपरीत,[note 3] यद्यपि और भिन्न-भिन्न संरचना के हैं.
एक प्रतिस्थापन प्रतिस्थापन से अधिक विशेष होता है या उसमें सम्मिलित होता है यदि द्वारा सम्मिलित किया गया है प्रत्येक पद के लिए . हम भी यही कहते हैं से अधिक सामान्य है . अधिक औपचारिक रूप से, एक गैर-रिक्त अनंत सेट लें सहायक चर जैसे कि को E समीकरण नहीं एकीकरण समस्या में चर के रूप में सम्मिलित हैं . फिर एक प्रतिस्थापन किसी अन्य प्रतिस्थापन द्वारा सम्मिलित किया गया है यदि कोई प्रतिस्थापन है ऐसा कि सभी शर्तों के लिए , .[7]उदाहरण के लिए द्वारा सम्मिलित किया गया है , का उपयोग करना , लेकिन
में सम्मिलित नहीं है , जैसा का उदाहरण नहीं है
.[8]}} के रूप में होता है.
समाधान सेट
एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक समाधान है यदि liσ ≡ riσ के लिए . ऐसे प्रतिस्थापन को Eका एकीकरणकर्ता भी कहा जाता है।
उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {x ⊕ a ≐ a ⊕ x } के समाधान हैं {x ↦ a' '}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, आदि ,जबकि समस्या { x ⊕ a ≐ a } का कोई समाधान नहीं होता है।
दी गई एकीकरण समस्या E के लिए, एकीकरणकर्ताओं के एक सेट S को पूर्ण कहा जाता है यदि प्रत्येक समाधान प्रतिस्थापन को एस में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन सेट निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का सेट लेकिन कुछ रूपरेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण यह निर्धारित करने की समस्या कि क्या को E के रूप में समाधान उपलब्ध है, अर्थात क्या पूर्ण प्रतिस्थापन सेट गैर होता रिक्त है, अनिर्णीत रूप में है।
समुच्चय S को न्यूनतम कहा जाता है यदि इसका कोई भी सदस्य दूसरे को सम्मिलित नहीं करता है। रूपरेखा के आधार पर एक पूर्ण और न्यूनतम प्रतिस्थापन सेट में शून्य, एक, परिमित रूप से कई या अनंत रूप से कई सदस्य हो सकते हैं या अनावश्यक सदस्यों की अनंत श्रृंखला के कारण पूर्णतया भी उपलब्ध नहीं हो सकते हैं।[9] इस प्रकार, सामान्यतः, एकीकरण एल्गोरिदम पूर्ण सेट के एक सीमित सन्निकटन की गणना करते हैं, जो न्यूनतम हो भी सकता है और नहीं भी हो सकते है, चूंकि अधिकांश एल्गोरिदम जब संभव हो तो निरर्थक एकीकरणकर्ताओं से बचते हैं।[7]प्रथम-क्रम वाक्यात्मक एकीकरण के लिए, मार्टेली और मोंटानारी[10] एक एल्गोरिदम दिया जाता है, जो अघुलनशीलता की रिपोर्ट करता है या एकल यूनिफायर की गणना करता है जो स्वयं एक पूर्ण और न्यूनतम प्रतिस्थापन सेट के रूप में बनाता है, जिसे सबसे सामान्य यूनिफायर कहा जाता है।
प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण
प्रथम-क्रम शब्दों का वाक्यात्मक एकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।
यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)n n-ary फलन प्रतीकों का और ≡ वाक्यात्मक समानता पर आधारित है।
इस ढांचे में, प्रत्येक समाधान योग्य एकीकरण समस्या {l1 ≐ r1, ..., ln ≐ rn} के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, एकल (गणित) समाधान सेट है {σ}.
इसके सदस्य σ को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) का रूप कहा जाता है।
जब एमजीयू लागू किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद वाक्यात्मक रूप से समतुल्य हो जाते हैं। l1σ = r1σ ∧ ... ∧ lnσ = rnσ.
समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है[note 4] एमजीयू द्वारा σ.
एमजीयू वेरिएंट तक अद्वितीय है: यदि एस1 और एस2 दोनों एक ही वाक्यात्मक एकीकरण समस्या के पूर्ण और न्यूनतम समाधान सेट हैं, तो S1 = { σ1 } और S2 = { σ2 } कुछ प्रतिस्थापनों के लिए σ1 और σ2, और xσ1 का एक प्रकार है xσ2 समस्या में आने वाले प्रत्येक चर x के लिए।
उदाहरण के लिए, एकीकरण समस्या { x ≐ z, y ≐ f(x) } में एक एकीकृतकर्ता है { x ↦ z, y ↦ f(z) }, क्योंकि
x { x ↦ z, y ↦ f(z) } = z = z { x ↦ z, y ↦ f(z) } , and y { x ↦ z, y ↦ f(z) } = f(z) = f(x) { x ↦ z, y ↦ f(z) } .
यह सबसे सामान्य एकीकरणकर्ता के रूप में है
समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { x ↦ f(x1), y ↦ f(f(x1)), z ↦ f(x1) }, { x ↦ f(f(x1)), y ↦ f(f(f(x1))), z ↦ f(f(x1)) }, और इसी प्रकार ऐसे अपरिमित रूप से अनेक एकीकरणकर्ता के रूप में हैं।
एक अन्य उदाहरण के रूप में, समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई समाधान नहीं है, क्योंकि बाएं और दाएं तरफ लागू कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मक रूप से भिन्न होते हैं।
एक एकीकरण एल्गोरिथ्म
Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically.[11] For a set T of terms, its disagreement path p is the lexicographically least path where two member terms of T differ. Its disagreement set is the set of subterms starting at p, formally: { t|p : }.[12]
Algorithm:[13]
Given a set T of terms to be unified
Let initially be the identity substitution
do forever
if is a singleton set then
return
fi
let D be the disagreement set of
let s, t be the two lexicographically least terms in D
if s is not a variable or s occurs in t then
return "NONUNIFIABLE"
fi
done
रॉबिन्सन (1965) द्वारा दिया गया पहला एल्गोरिदम अधिक अप्रभावी था; cf डिब्बा।
निम्नलिखित तेज़ एल्गोरिदम की उत्पत्ति मार्टेली, मोंटानारी (1982) के रूप में हुई थी।[note 5]
यह पेपर एक कुशल वाक्यात्मक एकीकरण एल्गोरिदम खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है,[14][15][16][17][18][19] और बताता है, कि रैखिक-समय एल्गोरिदम की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।[16]और पैटरसन, वेगमैन (1976,[20] 1978[17]).[note 6] का रूप होता है.
एक परिमित समुच्चय दिया गया है संभावित समीकरणों का रूप होता है. ,
एल्गोरिथ्म इसे फॉर्म के समीकरणों के समतुल्य सेट में बदलने के लिए नियम लागू करता है
{ x1 ≐ u1, ..., xm ≐ um }
कहां x1, ..., xm भिन्न-भिन्न चर हैं औरu1, ..., um ऐसे पद हैं जिनमें x में से कोई भी नहीं हैi.
इस फॉर्म के एक सेट को प्रतिस्थापन के रूप में पढ़ा जा सकता है।
यदि कोई समाधान नहीं है तो एल्गोरिथ्म ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।
समस्या G में चर x की सभी घटनाओं को पद t से प्रतिस्थापित करने की क्रिया को G {x ↦ t} दर्शाया गया है।
सरलता के लिए, स्थिर प्रतीकों को शून्य तर्क वाले फलन प्रतीकों के रूप में माना जाता है।
delete decompose if or conflict swap if and eliminate[note 7] if check
चेक होता है
एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के समाधान के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है.
जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के सेट में समीकरण x ≐ f(..., x, ...) का कोई समाधान नहीं है; इसलिए उन्मूलन नियम मात्र तभी लागू किया जा सकता है यदि x ∉ वार्स(t)।
चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, एल्गोरिथम को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग सिस्टम में होता है।
सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का #एकीकरण के रूप में देख़ते है।
समाप्ति का प्रमाण
एल्गोरिथम की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें
जहाँ nvar समीकरण सेट में एक से अधिक बार आने वाले चरों की संख्या है, nlhs फलन प्रतीकों और स्थिरांकों की संख्या होती है'
संभावित समीकरणों के बाईं ओर और neqn समीकरणों की संख्या के रूप में है.
जब नियम उन्मूलन लागू किया जाता है, nvar घट जाती है, क्योंकि G से x हटा दिया जाता है और मात्र { x ≐ t } में रखा जाता है।
कोई अन्य नियम लागू करने से कभी वृद्धि नहीं हो सकती nvar दोबारा होता है ।
जब नियम विघटित, संघर्ष, या अदला-बदली लागू के रूप में किया जाता है, nlhs कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।
बाकी किसी भी नियम को लागू करने से डिलीट या चेक नहीं बढ़ सकेगा nlhs, लेकिन घट जाती है neqn.
इसलिए किसी भी नियम को लागू करने से तीन गुना कम हो जाता है शब्दकोषीय क्रम के संबंध में जो मात्र सीमित संख्या में ही संभव है।
कॉनर मैकब्राइड देखते हैं[21] एपिग्राम (प्रोग्रामिंग लैंग्वेज) जैसी आश्रित रूप से टाइप की गई लैंग्वेज में एकीकरण जिस संरचना का उपयोग करता है, उसे व्यक्त करके रॉबिन्सन के एकीकरण एल्गोरिदम को चर की संख्या पर पुनरावर्ती बनाया जा सकता है, जिस स्थिति में एक भिन्न समाप्ति प्रमाण अनावश्यक हो जाता है।
प्रथम-क्रम शब्दों के वाक्यात्मक एकीकरण के उदाहरण
प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।
गणितीय संकेतन के लिए, x,y,z को चर के रूप में, f,g को फलन प्रतीकों के रूप में, और a,b को स्थिरांक के रूप में उपयोग किया जाता है।
प्रकल संकेतन | गणितीय संकेतन | एकताकारी प्रतिस्थापन | निरूपण |
---|---|---|---|
a = a |
{ a = a } | {} | सफल होता है. (टॉटोलॉजी) |
a = b |
{ a = b } | ⊥ | a और b मेल नहीं खाते |
X = X |
{ x = x } | {} | सफल होता है. (टॉटोलॉजी) |
a = X |
{ a = x } | { x ↦ a } | x स्थिरांक के साथ एकीकृत है a |
X = Y |
{ x = y } | { x ↦ y } | x और y उपनाम हैं |
f(a,X) = f(a,b) |
{ f(a,x) = f(a,b) } | { x ↦ b } | फलन और स्थिरांक प्रतीक मेल खाते हैं, x स्थिरांक b के साथ एकीकृत है |
f(a) = g(a) |
{ f(a) = g(a) } | ⊥ | f औरg मेल नहीं खाते
|
f(X) = f(Y) |
{ f(x) = f(y) } | { x ↦ y } | x और y उपनाम हैं |
f(X) = g(Y) |
{ f(x) = g(y) } | ⊥ | f औरg मेल नहीं खाते
|
f(X) = f(Y,Z) |
{ f(x) = f(y,z) } | ⊥ | विफल रहता है.f फलन प्रतीकों में अलग-अलग योग्यताएं होती हैं
|
f(g(X)) = f(Y) |
{ f(g(x)) = f(y) } | { y ↦ g(x) } | y को पद के साथ एकीकृत करता है |
f(g(X),X) = f(Y,a) |
{ f(g(x),x) = f(y,a) } | { x ↦ a, y ↦ g(a) } | x को स्थिरांक a के साथ और y को पद के साथ एकीकृत करता है |
X = f(X) |
{ x = f(x) } | should be ⊥ | प्रथम-क्रम तर्क और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ (होता है चेक द्वारा लागू)।
पारंपरिक प्रोलॉग और प्रोलॉग II में |
X = Y, Y = a |
{ x = y, y = a } | { x ↦ a, y ↦ a } | x और y दोनों स्थिरांक a के साथ एकीकृत हैं |
a = Y, X = Y |
{ a = y, x = y } | { x ↦ a, y ↦ a } | जैसा कि ऊपर बताया गया है (सेट में समीकरणों का क्रम मायने नहीं रखता) |
X = a, b = X |
{ x = a, b = x } | ⊥ | विफल रहता है. a और b मेल नहीं खाते हैं, इसलिए X को दोनों के साथ एकीकृत नहीं किया जा सकता है |
टर्म (तर्क)#शब्दों के साथ संचालन की वाक्यात्मक प्रथम-क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता n के रूप में बनावट हो सकता है 2n. उदाहरण के लिए समस्या में सबसे सामान्य एकीकरणकर्ता है' , सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण एल्गोरिदम पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।[22]
अनुप्रयोग: तर्क प्रोग्रामिंग में एकीकरण
एकीकरण की अवधारणा तर्क प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे प्रोलॉग लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है =
लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है =
अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है +
, -
, *
, /
. प्रकार अनुमान एल्गोरिदम सामान्यतः एकीकरण पर आधारित होते हैं।
प्रोलॉग में:
- एक चर (प्रोग्रामिंग) जो अनइंस्टेंटिफाइड है—अर्थात् इस पर कोई पिछला एकीकरण नहीं किया गया था - इसे एक परमाणु, एक शब्द या किसी अन्य असंतुलित चर के साथ एकीकृत किया जा सकता है, इस प्रकार प्रभावी रूप से इसका उपनाम बन जाता है। कई आधुनिक प्रोलॉग बोलियों और प्रथम-क्रम तर्क में एक चर को उस शब्द के साथ एकीकृत नहीं किया जा सकता है जिसमें वह सम्मिलित है; यह तथाकथित घटित जाँच है।
- दो परमाणु तभी एकीकृत हो सकते हैं जब वे समान हों जाते है।
- इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है।
अनुप्रयोग: प्रकार अनुमान
कार्यात्मक लैंग्वेज हास्केल (प्रोग्रामिंग लैंग्वेज) और एमएल (प्रोग्रामिंग लैंग्वेज) सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल अभिव्यक्ति ट्रू : ['x', 'y', 'z']
सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन (:)
प्रकार का है a -> [a] -> [a]
, और पहले तर्क के लिएट्रू
बहुरूपी प्रकार चर a
के साथ एकाकार होना होगा ट्रू
का प्रकार बूल
. दूसरा तर्क, ['x', 'y', 'z']
, प्रकार का है [चार]
, लेकिन a
दोनों नहीं हो सकते बूल
औरचार
एक ही समय पर होते है.
प्रोलॉग के प्रकार अनुमान के लिए एक एल्गोरिदम दिया जा सकता है:
- कोई भी प्रकार का चर किसी भी प्रकार की अभिव्यक्ति के साथ एकीकृत होता है और उस अभिव्यक्ति के लिए त्वरित होता है। एक विशिष्ट सिद्धांत इस नियम को घटित जाँच के साथ प्रतिबंधित कर सकता है।
- दो प्रकार के स्थिरांक तभी एकीकृत होते हैं जब वे एक ही प्रकार के हों जाते है।
- दो प्रकार के निर्माण मात्र तभी एकीकृत होते हैं जब वे एक ही प्रकार के कंस्ट्रक्टर के अनुप्रयोग होते हैं और उनके सभी घटक प्रकार पुनरावर्ती रूप से एकीकृत होते हैं।
इसकी घोषणात्मक प्रकृति के कारण एकीकरण के अनुक्रम में क्रम (सामान्यतः) महत्वहीन है।
ध्यान दें कि प्रथम-क्रम तर्क की शब्दावली में, एक परमाणु एक मूल प्रस्ताव है और प्रोलॉग शब्द के समान एकीकृत है।
अनुप्रयोग: फ़ीचर संरचना एकीकरण
अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।[23][24]
क्रमानुसार एकीकरण
क्रमबद्ध तर्क प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s2, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में तर्क करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है।
उदाहरण के लिए एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की तरह है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवर लोडिंग कहा जाता है, प्रोग्रामिंग लैंग्वेज में ओवरलोडिंग के समान हो जाता है.
क्रिस्टोफ़ वाल्थर ने क्रम-क्रमबद्ध तर्क में शब्दों के लिए एक एकीकरण एल्गोरिथ्म दिया जाता है, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती हैs1, s2 उनका प्रतिच्छेदन s1 ∩ s2 घोषित किया जाना भी है : यदि x1 और x2 सॉर्ट का एक चर हैs1,और s2, क्रमशः, समीकरण x1 ≐ x2 समाधान के रूप में है {x1 = x, x2 = x }, जहां x: s1 ∩ s2.
[25]इस एल्गोरिदम को क्लॉज-आधारित स्वचालित प्रमेय कहावत में सम्मिलित करने के पश्चात, वह एक बेंचमार्क समस्या को क्रम-क्रमबद्ध तर्क में अनुवाद करके हल कर सकता है, जिससे इसे परिमाण के क्रम में उबाला जा सकता है, क्योंकि कई यूनरी विधेय प्रकार में बदल जाते हैं।
पैरामीट्रिक बहुरूपता की अनुमति देने के लिए स्मोल्का ने क्रम-क्रमबद्ध तर्क को सामान्यीकृत किया जाता है।
[26]उनके ढांचे में उप-घोषणाएँ सम्मिश्र प्रकार की अभिव्यक्तियों के लिए प्रचारित की जाती हैं।
एक प्रोग्रामिंग उदाहरण के रूप में एक पैरामीट्रिक सॉर्ट सूची (X) घोषित की जा सकती है (टेम्प्लेट (C++)# फलन टेम्पलेट्स |C++ टेम्प्लेट में X एक प्रकार का पैरामीटर है), और एक सबसॉर्ट घोषणा से int ⊆ संबंध सूची फ़्लोट करें (int ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।
श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध तर्क को सामान्यीकृत किया। [27] उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक संपत्ति घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है।
अनंत पदों का एकीकरण
This section needs expansion. You can help by adding to it. (December 2021) |
अनंत पेड़ों पर पृष्ठभूमि:
- B. Courcelle (1983). "अनंत वृक्षों के मौलिक गुण". Theoret. Comput. Sci. 25 (2): 95–169. doi:10.1016/0304-3975(83)90059-2.
- Michael J. Maher (Jul 1988). "Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees". प्रोक. आईईईई तीसरा वार्षिक संगोष्ठी। कंप्यूटर विज्ञान में तर्क पर, एडिनबर्ग. pp. 348–357.
- Joxan Jaffar; Peter J. Stuckey (1986). "अनंत वृक्ष तर्क प्रोग्रामिंग के शब्दार्थ". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.
एकीकरण एल्गोरिथ्म, प्रोलॉग II:
- A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). प्रोलॉग और अनंत पेड़. Academic Press.
- Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). प्रोक. इंट. कॉन्फ़. पांचवीं पीढ़ी के कंप्यूटर सिस्टम पर. pp. 85–99.
अनुप्रयोग:
- Francis Giannesini; Jacques Cohen (1984). "प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर". Journal of Logic Programming. 1 (3): 253–265. doi:10.1016/0743-1066(84)90013-X.
ई-एकीकरण
ई-एकीकरण समीकरण के दिए गए सेट का समाधान खोजने की समस्या है.
कुछ समीकरणात्मक पृष्ठभूमि ज्ञान E को ध्यान में रखते हुए।
उत्तरार्द्ध को सार्वभौमिक समानता के एक सेट के रूप में दिया गया है।
कुछ विशेष सेट E के लिए समीकरण हल करने वाले एल्गोरिदम (उर्फ ई-एकीकरण एल्गोरिदम) तैयार किए गए हैं;
दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई एल्गोरिदम उपलब्ध नहीं हो सकता है।
उदाहरण के लिए, यदि a और b विशिष्ट स्थिरांक हैं,
समीकरण का कोई समाधान नहीं है.
विशुद्ध वाक्यात्मक एकीकरण में संबंध हो जाता है
जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है .
चूंकि यदि क्रमविनिमेय माना जाता है,
फिर प्रतिस्थापन {x ↦ b, y ↦ a} उपरोक्त समीकरण को हल करता है,
जब से,
{x ↦ b, y ↦ a} = प्रतिस्थापन आवेदन द्वारा = की क्रमपरिवर्तनशीलता द्वारा = {x ↦ b, y ↦ a} (विपरीत) प्रतिस्थापन आवेदन द्वारा
पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है सार्वभौम समानता द्वारा सभी के लिए u, v .
विशेष पृष्ठभूमि ज्ञान सेट E
∀ u,v,w: | = | A | Associativity of | ||
∀ u,v: | = | C | Commutativity of | ||
∀ u,v,w: | = | Dl | Left distributivity of over | ||
∀ u,v,w: | = | Dr | Right distributivity of over | ||
∀ u: | = | u | I | Idempotence of | |
∀ u: | = | u | Nl | Left neutral element n with respect to | |
∀ u: | = | u | Nr | Right neutral element n with respect to |
ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए निर्णायक होता है, यदि इसके लिए एक एकीकरण एल्गोरिदम तैयार किया गया है, जो किसी भी इनपुट समस्या के लिए समाप्त हो जाता है।
ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए अर्ध-निर्णायक है, यदि इसके लिए एक एकीकरण एल्गोरिदम तैयार किया गया है, जो किसी भी हल करने योग्य इनपुट समस्या के लिए समाप्त हो जाता है, लेकिन एक अघुलनशील इनपुट समस्या के समाधान के लिए निरंतर के लिए खोज जारी रख सकता है।
निम्नलिखित सिद्धांतों के लिए 'एकीकरण निर्णायक है':
- 'A[28]
- A,C[29]
- A,C,I[30]
- A,C,Nl[note 8][30]*A,I[31]
- A,Nl,Nr (मोनॉइड)[32]
- C[33]
- बूलियन रिंग[34][35]
- एबेलियन समूह, यदि हस्ताक्षर को मनमाने ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)[36]
- क्रिपके शब्दार्थ#पत्राचार और पूर्णता मोडल बीजगणित[37]
निम्नलिखित सिद्धांतों के लिए एकीकरण अर्ध-निर्णायक है:
- A,Dl,Dr[38]
- A,C,Dl[note 8][39]
- क्रमविनिमेय वलय[36]
एकतरफा पैरामोड्यूलेशन
यदि E के लिए एक अभिसरण शब्द पुनर्लेखन प्रणाली आर उपलब्ध है,
'एकतरफा पैरामोड्यूलेशन' एल्गोरिदम[40]
दिए गए समीकरणों के सभी समाधानों के रूप में गिनने के लिए उपयोग किया जा सकता है।
G ∪ { f(s1,...,sn) ≐ f(t1,...,tn) } | ; S | ⇒ | G ∪ { s1 ≐ t1, ..., sn ≐ tn } | ; S | decompose | |
G ∪ { x ≐ t } | ; S | ⇒ | G { x ↦ t } | ; S{x↦t} ∪ {x↦t} | if the variable x doesn't occur in t | eliminate |
G ∪ { f(s1,...,sn) ≐ t } | ; S | ⇒ | G ∪ { s1 ≐ u1, ..., sn ≐ un, r ≐ t } | ; S | if f(u1,...,un) → r is a rule from R | mutate |
G ∪ { f(s1,...,sn) ≐ y } | ; S | ⇒ | G ∪ { s1 ≐ y1, ..., sn ≐ yn, y ≐ f(y1,...,yn) } | ; S | if y1,...,yn are new variables | imitate |
G से प्रारंभ करके हल की जाने वाली एकीकरण समस्या और S पहचान प्रतिस्थापन है, नियमों को गैर-नियतात्मक रूप से लागू किया जाता है, जब तक कि खाली सेट वास्तविक G के रूप में प्रकट नहीं होता है, इस स्थिति में वास्तविक S एक एकीकृत प्रतिस्थापन है। आदेश के आधार पर पैरामॉड्यूलेशन नियम लागू होते हैं, G से वास्तविक समीकरण की पसंद पर और R की पसंद पर'के नियमों में परिवर्तन, विभिन्न संगणना पथ संभव हैं। मात्र कुछ ही समाधान की ओर ले जाते हैं, जबकि अन्य G ≠ {} पर समाप्त होते हैं, जहां कोई और नियम लागू नहीं होता है. (जैसे G = { f(...) ≐ g(...) })।
1 | app(nil,z) | → z |
2 | app(x.y,z) | → x.app(y,z) |
उदाहरण के लिए एक शब्द रीराइट सिस्टम R का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए cons(x,y) को इन्फ़िक्स नोटेशन में x.y के रूप में लिखा जाता है; जैसे ऐप(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil सूचियों a.b.nil और c.d.nil के संयोजन को प्रदर्शित करता है, पुनर्लेखन नियम 2 का उपयोग करते हुए, 2, और 1. R के अनुरूप समीकरण सिद्धांत E, R का सर्वांगसम समापन है, दोनों को शर्तों पर द्विआधारी संबंध के रूप में देखा जाता है।
उदाहरण के लिए, ऐप(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ ऐप(a.b.c.d.nil,nil)। पैरामोड्यूलेशन एल्गोरिदम उदाहरण R के साथ दिए जाने पर उस E के संबंध में समीकरणों के समाधान की गणना करता है।
एकीकरण समस्या {app(x,app(y,x)) ≐ a.a.nil } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; v2, v3, ... इस उद्देश्य के लिए कंप्यूटर-जनित परिवर्तनीय नाम हैं। प्रत्येक पंक्ति में, G से चुना गया समीकरण लाल रंग में हाइलाइट किया गया है। हर बार जब उत्परिवर्तित नियम लागू किया जाता है, तो चुने गए पुनर्लेखन नियम (1 या 2) को कोष्ठक में दर्शाया जाता है। अंतिम पंक्ति से एकीकृत प्रतिस्थापन S = {y ↦ nil, x ↦ a.nil } प्राप्त किया जा सकता है। वास्तव में,
ऐप(x,ऐप(y,x)) {y↦nil, x↦ a.nil } = ऐप(a.nil,app(nil,a.nil)) ≡ ऐप(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil दी गई समस्या का समाधान करता है।
दूसरा सफल संगणना पथ, जिसे mutate(1), mutate(2), mutate(2), mutate(1) चुनकर प्राप्त किया जा सकता है, प्रतिस्थापन की ओर ले जाता है S = { y ↦ a.a.nil, x ↦ nil }; यह यहां नहीं दिखाया गया है. कोई अन्य मार्ग सफलता की ओर नहीं ले जाता।
Used rule | G | S | |
---|---|---|---|
{ app(x,app(y,x)) ≐ a.a.nil } | {} | ||
mutate(2) | ⇒ | { x ≐ v2.v3, app(y,x) ≐ v4, v2.app(v3,v4) ≐ a.a.nil } | {} |
decompose | ⇒ | { x ≐ v2.v3, app(y,x) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil } | {} |
eliminate | ⇒ | { app(y,v2.v3) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil } | { x ↦ v2.v3 } |
eliminate | ⇒ | { app(y,a.v3) ≐ v4, app(v3,v4) ≐ a.nil } | { x ↦ a.v3 } |
mutate(1) | ⇒ | { y ≐ nil, a.v3 ≐ v5, v5 ≐ v4, app(v3,v4) ≐ a.nil } | { x ↦ a.v3 } |
eliminate | ⇒ | { y ≐ nil, a.v3 ≐ v4, app(v3,v4) ≐ a.nil } | { x ↦ a.v3 } |
eliminate | ⇒ | { a.v3 ≐ v4, app(v3,v4) ≐ a.nil } | { y ↦ nil, x ↦ a.v3 } |
mutate(1) | ⇒ | { a.v3 ≐ v4, v3 ≐ nil, v4 ≐ v6, v6 ≐ a.nil } | { y ↦ nil, x ↦ a.v3 } |
eliminate | ⇒ | { a.v3 ≐ v4, v3 ≐ nil, v4 ≐ a.nil } | { y ↦ nil, x ↦ a.v3 } |
eliminate | ⇒ | { a.nil ≐ v4, v4 ≐ a.nil } | { y ↦ nil, x ↦ a.nil } |
eliminate | ⇒ | { a.nil ≐ a.nil } | { y ↦ nil, x ↦ a.nil } |
decompose | ⇒ | { a ≐ a, nil ≐ nil } | { y ↦ nil, x ↦ a.nil } |
decompose | ⇒ | { nil ≐ nil } | { y ↦ nil, x ↦ a.nil } |
decompose | ⇒ | {} | { y ↦ nil, x ↦ a.nil } |
संकुचन
यदि R, E के लिए एक अभिसारी पद पुनर्लेखन प्रणाली है,
पिछले अनुभाग के लिए एक दृष्टिकोण विकल्प में 'संकीर्ण चरणों' का क्रमिक अनुप्रयोग सम्मिलित है;
यह अंततः किसी दिए गए समीकरण के सभी समाधानों की गणना करेगा।
एक संकीर्ण चरण (cf. चित्र) के रूप में सम्मिलित है
- वर्तमान पद का एक गैर-परिवर्तनीय उपपद चुनना है,
- आर से एक नियम के बाईं ओर इसे वाक्यात्मक रूप से एकीकृत करना, और
- तात्कालिक नियम के दाहिने हाथ को तात्कालिक शब्द में बदलना होता है।
औपचारिक रूप से, यदि l → r आर से पुनर्लेखन नियम की एक पुनर्नामित प्रति है, जिसमें शब्द एस और उपपद के साथ कोई चर समान नहीं है s|p एक चर नहीं है और इसके साथ एकीकृत किया जा सकता है l प्रथम-क्रम शब्दों के #सिंटैक्टिक एकीकरण के माध्यम से σ, तब s को इस शब्द तक सीमित किया जा सकता है t = sσ[rσ]p, अर्थात पद के लिए sσ, पी पर सबटर्म के साथ टर्म (लॉजिक)#ऑपरेशन्स विद टर्म्स बाय rσ. वह स्थिति जिसमें s को t तक सीमित किया जा सकता है, सामान्यतः s ↝ t के रूप में निरूपित की जाती है।
सहज रूप से, संकीर्ण चरणों का एक क्रम टी1 ↝ टी2 ↝ ... ↝ टीn इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है1 → टी2 → ... → टीn, लेकिन प्रारंभिक पद t के साथ1 प्रत्येक प्रयुक्त नियम को लागू करने के लिए आवश्यकतानुसार इसे और अधिक त्वरित किया जा रहा है।
- एकतरफा पैरामॉड्यूलेशन उदाहरण पैरामॉड्यूलेशन गणना निम्नलिखित संकीर्ण अनुक्रम से मेल खाती है (↓ यहां तात्कालिकता का संकेत है):
app( | x | ,app(y, | x | )) | |||||||||||||
↓ | ↓ | x ↦ v2.v3 | |||||||||||||||
app( | v2.v3 | ,app(y, | v2.v3 | )) | → | v2.app(v3,app( | y | ,v2.v3)) | |||||||||
↓ | y ↦ nil | ||||||||||||||||
v2.app(v3,app( | nil | ,v2.v3)) | → | v2.app( | v3 | ,v2. | v3 | ) | |||||||||
↓ | ↓ | v3 ↦ nil | |||||||||||||||
v2.app( | nil | ,v2. | nil | ) | → | v2.v2.nil |
अंतिम पद, वी2।में2.nil को मूल दाहिनी ओर के शब्द a.a.nil के साथ वाक्यात्मक रूप से एकीकृत किया जा सकता है।
सिकुड़ती लेम्मा[41] यह सुनिश्चित करता है कि जब भी किसी शब्द के उदाहरण को एक अभिसरण शब्द पुनर्लेखन प्रणाली द्वारा किसी शब्द t में फिर से लिखा जा सकता है, तो s और t को संकुचित किया जा सकता है और एक शब्द में फिर से लिखा जा सकता है s′ और t′, क्रमशः, ऐसे कि t′ का एक उदाहरण है s′.
औपचारिक रूप से: जब भी sσ t कुछ प्रतिस्थापन के लिए σ रखता है, तो वहां शर्तें उपलब्ध हैं s′, t′ ऐसा है कि s s′ और t t′ और s′ τ = t′ कुछ प्रतिस्थापन के लिए τ.
उच्च-क्रम एकीकरण
कई अनुप्रयोगों के लिए प्रथम-क्रम शब्दों के अतिरिक्त टाइप किए गए लैम्ब्डा-शब्दों के एकीकरण पर विचार करने की आवश्यकता होती है। इस प्रकार के एकीकरण को अधिकांशतः उच्च-क्रम एकीकरण कहा जाता है। उच्च-क्रम एकीकरण अनिर्णीत समस्या है,[42][43][44] और ऐसी एकीकरण समस्याओं में अधिकांश सामान्य एकीकरणकर्ता नहीं होते हैं। उदाहरण के लिए, एकीकरण समस्या { f(a,b,a) ≐ d(b,a,c) }, जहां एकमात्र चर f है, में है
समाधान {f ↦ λx.λy.λz. d(y,x,c) }, {f ↦ λx.λy.λz. d(y,z,c) }, {f ↦ λx.λy.λz. d(y,a,c) }, {f ↦ λx.λy.λz. डी(बी,x,सी) },
{f ↦ λx.λy.λz. d(b,z,c) } और {f ↦ λx.λy.λz. डी(बी,ए,सी) }. उच्च-क्रम एकीकरण की एक अच्छी प्रकार से अध्ययन की गई शाखा αβη रूपांतरणों द्वारा निर्धारित समानता को सरल रूप से टाइप किए गए लैम्ब्डा शब्दों मॉड्यूलो को एकीकृत करने की समस्या है। जेरार्ड ह्यूएट ने एक अर्ध-निर्णायक (पूर्व)एकीकरण एल्गोरिदम दिया[45] जो एकीकरणकर्ताओं के समष्टि की व्यवस्थित खोज की अनुमति देता है (मार्टेली-मोंटानारी के एकीकरण एल्गोरिदम को सामान्यीकृत करना)[10]उच्च-क्रम वाले चर वाले शब्दों के नियमों के साथ) जो व्यवहार में पर्याप्त रूप से अच्छी प्रकार से काम करता प्रतीत होता है। Huet[46] और गाइल्स डोवेक[47] इस विषय पर सर्वेक्षण करते हुए लेख लिखे हैं।
उच्च-क्रम एकीकरण के कई उपसमूह अच्छी प्रकार से व्यवहार किए जाते हैं, जिसमें वे निर्णय लेने योग्य होते हैं और हल करने योग्य समस्याओं के लिए सबसे सामान्य एकीकरणकर्ता होते हैं। ऐसा एक उपसमुच्चय पहले वर्णित प्रथम-क्रम पद है। डेल मिलर के कारण उच्च-क्रम पैटर्न एकीकरण,[48] ऐसा ही एक और उपसमुच्चय है। उच्च-क्रम तर्क प्रोग्रामिंग लैंग्वेजएं λप्रोलॉग और ट्वेल्फ़ पूर्ण उच्च-क्रम एकीकरण से मात्र पैटर्न खंड को लागू करने के लिए स्विच कर चुकी हैं; आश्चर्यजनक रूप से पैटर्न एकीकरण लगभग सभी कार्यक्रमों के लिए पर्याप्त है, यदि प्रत्येक गैर-पैटर्न एकीकरण समस्या को तब तक निलंबित कर दिया जाता है जब तक कि अगला प्रतिस्थापन एकीकरण को पैटर्न खंड में नहीं डाल देता। पैटर्न एकीकरण का एक सुपरसेट जिसे फलन -एज़-कंस्ट्रक्टर्स एकीकरण कहा जाता है, भी अच्छी प्रकार से व्यवहार किया जाता है।[49] ज़िपरपोज़िशन प्रमेय कहावत में एक एल्गोरिदम है जो इन अच्छे व्यवहार वाले उपसमुच्चय को पूर्ण उच्च-क्रम एकीकरण एल्गोरिदम में एकीकृत करता है।[7]
अभिकलनात्मक लैंग्वेज विज्ञान में अण्डाकार निर्माण के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम एकीकरण का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है like(j, m) ∧ R(p) और आर का मान (दीर्घवृत्त का अर्थपूर्ण प्रतिनिधित्व) समीकरण द्वारा निर्धारित किया जाता है like(j, m) = R(j) . ऐसे समीकरणों को हल करने की प्रक्रिया को उच्च-क्रम एकीकरण कहा जाता है।[50]
वेन स्नाइडर ने उच्च-क्रम एकीकरण और ई-एकीकरण दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।[51]
यह भी देखें
- पुनर्लेखन
- स्वीकार्य नियम
- लैम्ब्डा कैलकुलस में स्पष्ट प्रतिस्थापन
- गणितीय समीकरण हल करना
- डिस-यूनिफिकेशन (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: प्रतीकात्मक अभिव्यक्ति के बीच असमानताओं को हल करना
- एंटी-यूनिफिकेशन (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
- सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में एकीकरण और जुड़ने के रूप में विरोधी एकीकरण होता है
- ओन्टोलॉजी संरेखण (शब्दार्थ तुल्यता के साथ एकीकरण का उपयोग करें)
टिप्पणियाँ
- ↑ E.g. a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a
- ↑ since
- ↑ since z {z ↦ x ⊕ y} = x ⊕ y
- ↑ formally: each unifier τ satisfies ∀x: xτ = (xσ)ρ for some substitution ρ
- ↑ Alg.1, p.261. Their rule (a) corresponds to rule swap here, (b) to delete, (c) to both decompose and conflict, and (d) to both eliminate and check.
- ↑ Independent discovery is stated in Martelli, Montanari (1982),[10] sect.1, p.259. Paterson's and Wegman's journal paper[17] is dated 1978; however, the journal publisher received it in Sep.1976.
- ↑ Although the rule keeps x ≐ t in G, it cannot loop forever since its precondition x∈vars(G) is invalidated by its first application. More generally, the algorithm is guaranteed to terminate always, see below.
- ↑ 8.0 8.1 in the presence of equality C, equalities Nl and Nr are equivalent, similar for Dl and Dr
संदर्भ
- ↑ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
- ↑ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). एक तर्कशास्त्री के रूप में जैक्स हेरब्रांड पर व्याख्यान (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56
- ↑ Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97
- ↑ 4.0 4.1 4.2 4.3 J.A. Robinson (Jan 1965). "संकल्प सिद्धांत पर आधारित एक मशीन-उन्मुख तर्क". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32
- ↑ J.A. Robinson (1971). "Computational logic: The unification computation". Machine Intelligence. 6: 63–72.
- ↑ Dowek, Gilles (1 January 2001). "Higher-order unification and matching". स्वचालित तर्क की पुस्तिका. Elsevier Science Publishers B. V. pp. 1009–1062. ISBN 978-0-444-50812-6.
- ↑ 7.0 7.1 7.2 Vukmirović, Petar; Bentkamp, Alexander; Nummelin, Visa (14 December 2021). "कुशल पूर्ण उच्च-क्रम एकीकरण". Logical Methods in Computer Science. 17 (4): 6919. doi:10.46298/lmcs-17(4:18)2021.
- ↑ Apt, Krzysztof R. (1997). लॉजिक प्रोग्रामिंग से लेकर प्रोलॉग तक (1. publ ed.). London Munich: Prentice Hall. p. 24. ISBN 013230368X.
- ↑ Fages, François; Huet, Gérard (1986). "समीकरण सिद्धांतों में यूनिफायर और मैचर्स का पूरा सेट". Theoretical Computer Science. 43: 189–200. doi:10.1016/0304-3975(86)90175-1.
- ↑ 10.0 10.1 10.2 Martelli, Alberto; Montanari, Ugo (Apr 1982). "एक कुशल एकीकरण एल्गोरिदम". ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169. S2CID 10921306.
- ↑ Robinson (1965);[4] nr.2.5, 2.14, p.25
- ↑ Robinson (1965);[4] nr.5.6, p.32
- ↑ Robinson (1965);[4] nr.5.8, p.32
- ↑ Lewis Denver Baxter (Feb 1976). एक व्यावहारिक रूप से रैखिक एकीकरण एल्गोरिदम (PDF) (Res. Report). Vol. CS-76-13. Univ. of Waterloo, Ontario.
- ↑ Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (These d'etat). Universite de Paris VII.
- ↑ 16.0 16.1 Alberto Martelli & Ugo Montanari (Jul 1976). Unification in linear time and space: A structured presentation (Internal Note). Vol. IEI-B76-16. Consiglio Nazionale delle Ricerche, Pisa. Archived from the original on 2015-01-15.
- ↑ 17.0 17.1 17.2 17.3 Michael Stewart Paterson and M.N. Wegman (Apr 1978). "रैखिक एकीकरण". J. Comput. Syst. Sci. 16 (2): 158–167. doi:10.1016/0022-0000(78)90043-0.
- ↑ J.A. Robinson (Jan 1976). "Fast unification". In Woodrow W. Bledsoe, Michael M. Richter (ed.). प्रोक. प्रमेय सिद्ध करने की कार्यशाला ओबेरवुल्फ़च. Oberwolfach Workshop Report. Vol. 1976/3.[permanent dead link]
- ↑ M. Venturini-Zilli (Oct 1975). "प्रथम-क्रम अभिव्यक्तियों के लिए एकीकरण एल्गोरिथ्म की जटिलता". Calcolo. 12 (4): 361–372. doi:10.1007/BF02575754. S2CID 189789152.
- ↑ Paterson, M.S.; Wegman, M.N. (May 1976). Chandra, Ashok K.; Wotschke, Detlef; Friedman, Emily P.; Harrison, Michael A. (eds.). रैखिक एकीकरण. Proceedings of the eighth annual ACM Symposium on Theory of Computing (STOC). ACM. pp. 181–186. doi:10.1145/800113.803646.
- ↑ McBride, Conor (October 2003). "संरचनात्मक प्रत्यावर्तन द्वारा प्रथम-क्रम एकीकरण". Journal of Functional Programming. 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516. doi:10.1017/S0956796803004957. ISSN 0956-7968. S2CID 43523380. Retrieved 30 March 2012.
- ↑ e.g. Paterson, Wegman (1978),[17] sect.2, p.159
- ↑ Jonathan Calder, Mike Reape, and Hank Zeevat,, An algorithm for generation in unification categorial grammar. In Proceedings of the 4th Conference of the European Chapter of the Association for Computational Linguistics, pages 233-240, Manchester, England (10–12 April), University of Manchester Institute of Science and Technology, 1989.
- ↑ Graeme Hirst and David St-Onge, [1] Lexical chains as representations of context for the detection and correction of malapropisms, 1998.
- ↑ Walther, Christoph (1985). "कई-क्रमबद्ध रिज़ॉल्यूशन द्वारा शुबर्ट के स्टीमरोलर का एक यांत्रिक समाधान" (PDF). Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3. Archived from the original (PDF) on 2011-07-08. Retrieved 2013-06-28.
- ↑ Smolka, Gert (Nov 1988). पॉलिमॉर्फिकली ऑर्डर-सॉर्टेड प्रकारों के साथ लॉजिक प्रोग्रामिंग (PDF). Int. Workshop Algebraic and Logic Programming. LNCS. Vol. 343. Springer. pp. 53–70. doi:10.1007/3-540-50667-5_58.
- ↑ Schmidt-Schauß, Manfred (Apr 1988). टर्म घोषणाओं के साथ ऑर्डर-सॉर्टेड लॉजिक के कम्प्यूटेशनल पहलू. Lecture Notes in Artificial Intelligence (LNAI). Vol. 395. Springer.
- ↑ Gordon D. Plotkin, Lattice Theoretic Properties of Subsumption, Memorandum MIP-R-77, Univ. Edinburgh, Jun 1970
- ↑ Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, J. Assoc. Comput. Mach., vol.28, no.3, pp. 423–434, 1981
- ↑ 30.0 30.1 F. Fages, Associative-Commutative Unification, J. Symbolic Comput., vol.3, no.3, pp. 257–275, 1987
- ↑ Franz Baader, Unification in Idempotent Semigroups is of Type Zero, J. Automat. Reasoning, vol.2, no.3, 1986
- ↑ J. Makanin, The Problem of Solvability of Equations in a Free Semi-Group, Akad. Nauk SSSR, vol.233, no.2, 1977
- ↑ F. Fages (1987). "साहचर्य-अनुकरणीय एकीकरण" (PDF). J. Symbolic Comput. 3 (3): 257–275. doi:10.1016/s0747-7171(87)80004-4.
- ↑ Martin, U., Nipkow, T. (1986). "Unification in Boolean Rings". In Jörg H. Siekmann (ed.). Proc. 8th CADE. LNCS. Vol. 230. Springer. pp. 506–513.
{{cite book}}
: CS1 maint: multiple names: authors list (link) - ↑ A. Boudet; J.P. Jouannaud; M. Schmidt-Schauß (1989). "बूलियन रिंग्स और एबेलियन समूहों का एकीकरण". Journal of Symbolic Computation. 8 (5): 449–477. doi:10.1016/s0747-7171(89)80054-9.
- ↑ 36.0 36.1 Baader and Snyder (2001), p. 486.
- ↑ F. Baader and S. Ghilardi, Unification in modal and description logics, Logic Journal of the IGPL 19 (2011), no. 6, pp. 705–730.
- ↑ P. Szabo, Unifikationstheorie erster Ordnung (First Order Unification Theory), Thesis, Univ. Karlsruhe, West Germany, 1982
- ↑ Jörg H. Siekmann, Universal Unification, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984
- ↑ N. Dershowitz and G. Sivakumar, Solving Goals in Equational Languages, Proc. 1st Int. Workshop on Conditional Term Rewriting Systems, Springer LNCS vol.308, pp. 45–55, 1988
- ↑ Fay (1979). "First-Order Unification in an Equational Theory". Proc. 4th Workshop on Automated Deduction. pp. 161–167.
- ↑ 42.0 42.1 Warren D. Goldfarb (1981). "द्वितीय-क्रम एकीकरण समस्या की अनिर्णयता". TCS. 13 (2): 225–230. doi:10.1016/0304-3975(81)90040-2.
- ↑ Gérard P. Huet (1973). "तीसरे क्रम के तर्क में एकीकरण की अनिश्चितता". Information and Control. 22 (3): 257–267. doi:10.1016/S0019-9958(73)90301-X.
- ↑ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
- ↑ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
- ↑ Gérard Huet: Higher Order Unification 30 Years Later
- ↑ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009–1062
- ↑ Miller, Dale (1991). "लैम्ब्डा-एब्स्ट्रैक्शन, फंक्शन वेरिएबल्स और सरल एकीकरण के साथ एक लॉजिक प्रोग्रामिंग भाषा" (PDF). Journal of Logic and Computation. 1 (4): 497–536. doi:10.1093/logcom/1.4.497.
- ↑ Libal, Tomer; Miller, Dale (May 2022). "Functions-as-constructors higher-order unification: extended pattern unification". Annals of Mathematics and Artificial Intelligence. 90 (5): 455–479. doi:10.1007/s10472-021-09774-y.
- ↑ Gardent, Claire; Kohlhase, Michael; Konrad, Karsten (1997). "A Multi-Level, Higher-Order Unification Approach to Ellipsis". Submitted to European Association for Computational Linguistics (EACL). CiteSeerX 10.1.1.55.9018.
- ↑ Wayne Snyder (Jul 1990). "Higher order E-unification". प्रोक. स्वचालित कटौती पर 10वां सम्मेलन. LNAI. Vol. 449. Springer. pp. 573–587.
अग्रिम पठन
- Franz Baader and Wayne Snyder (2001). "Unification Theory" Archived 2015-06-08 at the Wayback Machine. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers.[dead link]
- Gilles Dowek (2001). "Higher-order Unification and Matching". In Handbook of Automated Reasoning.
- Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
- Franz Baader and Jörg H. Siekmann (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming.
- Jean-Pierre Jouannaud and Claude Kirchner (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In Computational Logic: Essays in Honor of Alan Robinson.
- Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, volume B Formal Models and Semantics, Elsevier, 1990, pp. 243–320
- Jörg H. Siekmann (1990). "Unification Theory". In Claude Kirchner (editor) Unification. Academic Press.
- Kevin Knight (Mar 1989). "Unification: A Multidisciplinary Survey" (PDF). ACM Computing Surveys. 21 (1): 93–124. CiteSeerX 10.1.1.64.8967. doi:10.1145/62029.62030. S2CID 14619034.
- Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
- Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). "A short survey on the state of the art in matching and unification problems". ACM SIGSAM Bulletin. 13 (2): 14–20. doi:10.1145/1089208.1089210. S2CID 17033087.
- Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.