एकीकरण (कंप्यूटर विज्ञान)

लॉजिक और कंप्यूटर विज्ञान में एकीकरण सिंबॉलिक अभिव्यक्तियों (गणित) के बीच समीकरणों को हल करने की एल्गोरिथम प्रक्रिया का उपयोग किया जाता है। उदाहरण के लिए x,y,z को चर के रूप में उपयोग करते हुए एकल समीकरण समुच्चय { cons(x,cons(x,nil)) = cons(2,y) } एक वाक्यात्मक प्रथम-क्रम एकीकरण समस्या के रूप में है, जिसके पास प्रतिस्थापन {x ↦ 2, y ↦ cons(2,nil) } का एकमात्र हल होता है।

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

फॉर्मल परिभाषा

एकीकरण समस्या हल करने के लिए समीकरणों का एक सीमित समुच्चय E={ l₁ ≐ r₁, ..., l_n ≐ r_n } के रूप में होता है, जहाँ l_i, r_i पदों या अभिव्यक्तियों के समुच्चय $T$ के रूप में होता हैं। समीकरण समुच्चय या एकीकरण समस्या में किन अभिव्यक्तियों या शब्दों को घटित होने की अनुमति होती है और किन अभिव्यक्तियों को समान माना जाता है, इसके आधार पर एकीकरण के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात फलन (गणित) का प्रतिनिधित्व करने वाले चर को एक अभिव्यक्तियों में अनुमति होती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है। अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी समाधान की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक एकीकरण या ई- एकीकरण या एकीकरण मॉड्यूलो सिद्धांत कहा जाता है।

प्रिरेक्विज़िट

फॉर्मल रूप से, एक एकीकरण दृष्टिकोण का अनुमान लगाया जाता है

• एक अनंत समुच्चय $V$ चर का. उच्च-क्रम एकीकरण के लिए, इसे चुनना सुविधाजनक है $V$ लैम्ब्डा-टर्म बाध्य चर के समुच्चय से भिन्न हो जाता है।
• एक समुच्चय $T$ ऐसे शब्दों का $V\subseteq T$. प्रथम-क्रम एकीकरण के लिए, $T$ सामान्यतः प्रथम-क्रम शब्दों चर और फलन प्रतीकों से निर्मित शब्द का समुच्चय होता है। उच्च-क्रम एकीकरण के लिए $T$ इसमें प्रथम-क्रम वाले शब्द और लैम्ब्डा शब्द कुछ उच्च-क्रम वाले चर वाले शब्द के रूप में सम्मिलित होते हैं।
• एक मैपिंग संस्करण: $T\rightarrow$ पावर समुच्चय |$\mathbb {P}$$(V)$, प्रत्येक पद को निर्दिष्ट करना $t$ समुच्चय ${\text{vars}}(t)\subsetneq V$ में होने वाले मुक्त चर के रूप में $t$ होता है.
• एक सिद्धांत या तुल्यता संबंध $\equiv$ पर $T$, यह दर्शाता है कि कौन से पद समान माने जाते हैं। प्रथम-क्रम ई- एकीकरण के लिए, $\equiv$ कुछ फलन प्रतीकों के बारे में पृष्ठभूमि ज्ञान को दर्शाता है; उदाहरण के लिए, यदि $\oplus$ क्रमविनिमेय माना जाता है, $t\equiv u$ यदि $u$ वहां से परिणाम मिले $t$ के लॉजिक ों की अदला-बदली करके $\oplus$ कुछ संभवतः सभी घटनाओं पर। सबसे विशिष्ट स्थिति में जब कोई पृष्ठभूमि ज्ञान नहीं होता है, तो मात्र शाब्दिक रूप से या वाक्यात्मकरूप से समान शब्दों को समान माना जाता है। इस स्थिति में ≡ को मुक्त सिद्धांत कहा जाता है, क्योंकि यह एक स्वतंत्र वस्तु के रूप में है, खाली सिद्धांत क्योंकि समीकरण वाक्य (गणितीय लॉजिक ) का समुच्चय या पृष्ठभूमि ज्ञान के रूप में खाली है), अव्याख्यायित कार्यों का सिद्धांत पर किया जाता है, क्योंकि एकीकरण अनिर्वचनीय शब्द (लॉजिक )) या बीजगणितीय विनिर्देश के सिद्धांत के रूप में किया जाता है, क्योंकि सभी फलन प्रतीक मात्र उन पर काम करने के अतिरिक्त डेटा शब्द के रूप में बनाते हैं। सामान्यतः उच्च-क्रम एकीकरण के लिए $t\equiv u$ यदि $t$ और $u$ अल्फ़ा समतुल्य होता है.

शब्दों और सिद्धांत का समुच्चय समाधानों के समुच्चय को कैसे प्रभावित करता है, इसके उदाहरण के रूप में वाक्यात्मकप्रथम-क्रम एकीकरण समस्या { 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 भी मान) } होता है।

प्रतिस्थापन

Main article: प्रतिस्थापन (लॉजिक)

प्रतिस्थापन एक मानचित्रण है $\sigma :V\rightarrow T$ चर से पदों तक; संकेतन $\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ प्रत्येक चर के रूप में प्रतिस्थापन मानचित्रण को संदर्भित करता है $x_{i}$ पद के लिए $t_{i}$, के लिए $i=1,...,k$, और प्रत्येक अन्य चर स्वयं के लिए होता है। उस प्रतिस्थापन को किसी पद पर प्रयुक्त करना $t$ उपसर्ग संकेतन में इस प्रकार लिखा गया है $t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$; इसका अर्थ है (एक साथ) प्रत्येक चर की प्रत्येक घटना को प्रतिस्थापित करना $x_{i}$ अवधि में $t$ द्वारा $t_{i}$. परिणाम $t\tau$ प्रतिस्थापन प्रयुक्त करने का $\tau$ एक पद के लिए $t$ उस पद का उदाहरण कहा जाता है $t$.

प्रथम-क्रम उदाहरण के रूप में प्रतिस्थापन प्रयुक्त करना { x ↦ h(a,y), z ↦ b }शब्द के लिए होता है.

	$f($	${\textbf {x}}$	$,a,g($	${\textbf {z}}$	$),y)$
yields
	$f($	${\textbf {h}}({\textbf {a}},{\textbf {y}})$	$,a,g($	${\textbf {b}}$	$),y).$

सामान्यीकरण, विशेषज्ञता

यदि एक शब्द $t$ एक पद के समतुल्य एक उदाहरण है $u$, अर्थात्, यदि $t\sigma \equiv u$ कुछ प्रतिस्थापन के लिए $\sigma$, तब $t$ से अधिक सामान्य कहा जाता है $u$, और $u$ से अधिक विशेष कहा जाता है, या उसमें सम्मिलित किया जाता है, $t$. उदाहरण के लिए, $x\oplus a$ से अधिक सामान्य है $a\oplus b$ यदि ⊕ क्रमविनिमेय संपत्ति है, तब से $(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$.

यदि ≡ शब्दों की शाब्दिक वाक्यविन्यास के रूप में पहचान है, तो एक शब्द दूसरे की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकते है, यदि दोनों शब्द मात्र उनके परिवर्तनीय नामों में भिन्न हों न कि उनकी वाक्यात्मकसंरचना में ऐसे शब्दों को परिवर्त या एक-दूसरे का नाम बदलना कहा जाता है।

उदाहरण के लिए,

$f(x_{1},a,g(z_{1}),y_{1})$

का एक प्रकार होता है

$f(x_{2},a,g(z_{2}),y_{2})$,

जब से

$$f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})$$

और

$$f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).$$

चूंकि, $f(x_{1},a,g(z_{1}),y_{1})$ का एक प्रकार नहीं है $f(x_{2},a,g(x_{2}),x_{2})$, क्योंकि कोई भी प्रतिस्थापन पश्चात वाले पद को पहले वाले में नहीं बदल सकता है।

इसलिए पश्चात वाला शब्द पहले वाले की तुलना में उचित रूप से अधिक विशेष होता है।

यादृच्छिक के लिए $\equiv$, एक शब्द संरचनात्मक रूप से भिन्न शब्द की तुलना में अधिक सामान्य और अधिक विशेष दोनों हो सकता है।

उदाहरण के लिए, यदि ⊕ निष्क्रिय है, अर्थात यदि सदैव $x\oplus x\equiv x$, फिर पद $x\oplus y$ से अधिक सामान्य है $z$, और इसके विपरीत, यद्यपि $x\oplus y$ और $z$ भिन्न-भिन्न संरचना के हैं.

एक प्रतिस्थापन $\sigma$ प्रतिस्थापन से अधिक विशेष होता है या उसमें सम्मिलित होता है $\tau$ यदि $t\sigma$ द्वारा सम्मिलित किया गया है $t\tau$ प्रत्येक पद के लिए $t$. हम भी यही कहते हैं $\tau$ से अधिक सामान्य है $\sigma$. अधिक फॉर्मल रूप से, एक गैर-रिक्त अनंत समुच्चय लें $V$ सहायक चर जैसे कि को E समीकरण नहीं $l_{i}\doteq r_{i}$ एकीकरण समस्या में चर के रूप में सम्मिलित हैं $V$. फिर एक प्रतिस्थापन $\sigma$ किसी अन्य प्रतिस्थापन द्वारा सम्मिलित किया गया है $\tau$ यदि कोई प्रतिस्थापन है $\theta$ ऐसा कि सभी शर्तों के लिए $X\notin V$, $X\sigma \equiv X\tau \theta$.उदाहरण के लिए $\{x\mapsto a,y\mapsto a\}$ द्वारा सम्मिलित किया गया है $\tau =\{x\mapsto y\}$, का उपयोग करना $\theta =\{y\mapsto a\}$, लेकिन

$\sigma =\{x\mapsto a\}$ में सम्मिलित नहीं है $\tau =\{x\mapsto y\}$, जैसा $f(x,y)\sigma =f(a,y)$ का उदाहरण नहीं है

$f(x,y)\tau =f(y,y)$.}} के रूप में होता है.

हल समुच्चय

एक प्रतिस्थापन σ एकीकरण समस्या E के रूप में एक हल है यदि l_iσ ≡ r_iσ के लिए $i=1,...,n$. ऐसे प्रतिस्थापन को E का एकीकरण कर्ता भी कहा जाता है।

उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {x ⊕ a ≐ a ⊕ x } के हल हैं {x ↦ a' '}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, आदि ,जबकि समस्या { x ⊕ a ≐ a } का कोई हल नहीं होता है।

दी गई एकीकरण समस्या E के लिए, एकीकरण कर्ताओं के एक समुच्चय S को पूर्ण कहा जाता है यदि प्रत्येक हल प्रतिस्थापन को एस में कुछ प्रतिस्थापन द्वारा समाहित किया जाता है। एक पूर्ण प्रतिस्थापन समुच्चय निरंतर उपलब्ध होता है, उदाहरण के लिए सभी समाधानों का समुच्चय लेकिन कुछ रूपरेखाओं में जैसे कि अप्रतिबंधित उच्च-क्रम एकीकरण में यह निर्धारित करने की समस्या होती है कि क्या पूर्ण प्रतिस्थापन समुच्चय गैर रिक्त अनिर्णीत रूप में होता है।

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

प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण

प्रतिस्थापन σ द्वारा टर्म t1 और t2 को वाक्यात्मकरूप से एकीकृत करने का योजनाबद्ध त्रिभुज आरेख है

प्रथम-क्रम शब्दों का वाक्यात्मकएकीकरण सबसे व्यापक रूप से उपयोग किया जाने वाला एकीकरण ढांचा है।

यह प्रथम-क्रम के पदों के समुच्चय T के रूप में आधारित है, (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)_n n-ary फलन प्रतीकों का और ≡ वाक्यात्मकसमानता पर आधारित है।

इस ढांचे में, प्रत्येक हल योग्य एकीकरण समस्या {l₁ ≐ r₁, ..., l_n ≐ r_n} के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, एकल (गणित) हल समुच्चय है {σ}.

इसके सदस्य σ को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) का रूप कहा जाता है।

जब एमजीयू प्रयुक्त किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद वाक्यात्मकरूप से समतुल्य हो जाते हैं। l₁σ = r₁σ ∧ ... ∧ l_nσ = r_nσ.

समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है एमजीयू द्वारा σ.

एमजीयू वेरिएंट तक अद्वितीय है: यदि एस₁ और एस₂ दोनों एक ही वाक्यात्मकएकीकरण समस्या के पूर्ण और न्यूनतम हल समुच्चय हैं, तो S₁ = { σ₁ } और S₂ = { σ₂ } कुछ प्रतिस्थापनों के लिए σ₁ और σ₂, और xσ₁ का एक प्रकार है xσ₂ समस्या में आने वाले प्रत्येक चर 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(x₁), y ↦ f(f(x₁)), z ↦ f(x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) }, और इसी प्रकार ऐसे अपरिमित रूप से अनेक एकीकरणकर्ता के रूप में हैं।

एक अन्य उदाहरण के रूप में, समस्या g(x,x) ≐ f(y) का शाब्दिक पहचान होने के संबंध में कोई हल नहीं है, क्योंकि बाएं और दाएं तरफ प्रयुक्त कोई भी प्रतिस्थापन क्रमशः सबसे बाहरी g और f को बनाए रखेगा, और विभिन्न बाहरीतम फलन प्रतीकों वाले शब्द वाक्यात्मकरूप से भिन्न होते हैं।

एक एकीकरण कलन विधि

Robinson's 1965 unification algorithm

Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically. 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 : $t\in T$ }.

Algorithm:
Given a set T of terms to be unified
Let $\sigma$ initially be the identity substitution
do forever
    if $T\sigma$ is a singleton set then
        return $\sigma$
    fi
    let D be the disagreement set of $T\sigma$
    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
    $\sigma :=\sigma \{s\mapsto t\}$
done

रॉबिन्सन (1965) द्वारा दिया गया पहला एल्गोरिथम अधिक अप्रभावी था; cf डिब्बा।

निम्नलिखित तेज़ एल्गोरिथम की उत्पत्ति मार्टेली, मोंटानारी (1982) के रूप में हुई थी।

यह पेपर एक कुशल वाक्यात्मकएकीकरण एल्गोरिथम खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है, और बताता है, कि रैखिक-समय एल्गोरिथम की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।और पैटरसन, वेगमैन (1976, 1978). का रूप होता है.

एक परिमित समुच्चय दिया गया है $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$ संभावित समीकरणों का रूप होता है. ,

एल्गोरिथम इसे फॉर्म के समीकरणों के समतुल्य समुच्चय में बदलने के लिए नियम प्रयुक्त करता है

{ x₁ ≐ u₁, ..., x_m ≐ u_m }

कहां x₁, ..., x_m भिन्न-भिन्न चर हैं औरu₁, ..., u_m ऐसे पद हैं जिनमें x में से कोई भी नहीं है_i.

इस फॉर्म के एक समुच्चय को प्रतिस्थापन के रूप में पढ़ा जा सकता है।

यदि कोई हल नहीं है तो एल्गोरिथम ⊥ के साथ समाप्त हो जाता है; अन्य लेखक Ω , {} के रूप में उपयोग करते हैं या उस स्थिति में विफल हो जाते हैं।

समस्या G में चर x की सभी घटनाओं को पद t से प्रतिस्थापित करने की क्रिया को G {x ↦ t} दर्शाया गया है।

सरलता के लिए, स्थिर प्रतीकों को शून्य लॉजिक वाले फलन प्रतीकों के रूप में माना जाता है।

$G\cup \{t\doteq t\}$	$\Rightarrow$	$G$		delete
$G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}$	$\Rightarrow$	$G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}$		decompose
$G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}$	$\Rightarrow$	$\bot$	if $f\neq g$ or $k\neq m$	conflict
$G\cup \{f(s_{0},...,s_{k})\doteq x\}$	$\Rightarrow$	$G\cup \{x\doteq f(s_{0},...,s_{k})\}$		swap
$G\cup \{x\doteq t\}$	$\Rightarrow$	$G\{x\mapsto t\}\cup \{x\doteq t\}$	if $x\not \in {\text{vars}}(t)$ and $x\in {\text{vars}}(G)$	eliminate
$G\cup \{x\doteq f(s_{0},...,s_{k})\}$	$\Rightarrow$	$\bot$	if $x\in {\text{vars}}(f(s_{0},...,s_{k}))$	check

ओक्कुर चेक

Main article: ओक्कुर चेक

एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के हल के रूप में एक अनंत पद की ओर ले जाता है, क्योंकि x स्वयं के एक उपपद के रूप में घटित होता है

जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के समुच्चय में समीकरण x ≐ f(..., x, ...) का कोई हल नहीं है; इसलिए उन्मूलन नियम मात्र तभी प्रयुक्त किया जा सकता है यदि x ∉ वार्स(t)।

चूँकि वह अतिरिक्त जाँच जिसे 'एक्सेस चेक' कहा जाता है, एल्गोरिथम को धीमा कर देती है, इसलिए इसे छोड़ दिया जाता है, उदाहरण के लिए अधिकांश प्रोलॉग प्रणाली में होता है।

सैद्धांतिक दृष्टिकोण से, चेक को छोड़ना अनंत पेड़ों पर समीकरणों को हल करने के समतुल्य है, नीचे अनंत पदों का # एकीकरण के रूप में देख़ते है।

समाप्ति का प्रमाण

एल्गोरिथम की समाप्ति के प्रमाण के लिए ट्रिपल पर विचार करें $\langle n_{var},n_{lhs},n_{eqn}\rangle$

जहाँ n_var समीकरण समुच्चय में एक से अधिक बार आने वाले चरों की संख्या है, n_lhs फलन प्रतीकों और स्थिरांकों की संख्या होती है'

संभावित समीकरणों के बाईं ओर और n_eqn समीकरणों की संख्या के रूप में है.

जब नियम उन्मूलन प्रयुक्त किया जाता है, n_var घट जाती है, क्योंकि G से x हटा दिया जाता है और मात्र { x ≐ t } में रखा जाता है।

कोई अन्य नियम प्रयुक्त करने से कभी वृद्धि नहीं हो सकती n_var दोबारा होता है ।

जब नियम विघटित, संघर्ष, या अदला-बदली प्रयुक्त के रूप में किया जाता है, n_lhs कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी f गायब हो जाता है।

बाकी किसी भी नियम को प्रयुक्त करने से डिलीट या चेक नहीं बढ़ सकेगा n_lhs, लेकिन घट जाती है n_eqn.

इसलिए किसी भी नियम को प्रयुक्त करने से तीन गुना कम हो जाता है $\langle n_{var},n_{lhs},n_{eqn}\rangle$ शब्दकोषीय क्रम के संबंध में जो मात्र सीमित संख्या में ही संभव है।

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

प्रथम-क्रम शब्दों के वाक्यात्मकएकीकरण के उदाहरण

प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपर केस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है. वह एक फलन प्रतीक है, अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है।

गणितीय संकेतन के लिए, 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 को पद के साथ एकीकृत करता है $g(x)$
f(g(X),X) = f(Y,a)	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	x को स्थिरांक a के साथ और y को पद के साथ एकीकृत करता है $g(a)$
X = f(X)	{ x = f(x) }	should be ⊥	प्रथम-क्रम लॉजिक और कई आधुनिक प्रोलॉग बोलियों में रिटर्न ⊥ ओक्कुर चेक द्वारा प्रयुक्त होता है। पारंपरिक प्रोलॉग और प्रोलॉग II मेंxको अनंत पद के साथ एकीकृत करने में सफलता मिलती हैx=f(f(f(f(...)))).
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 के रूप में बनावट हो सकता है 2ⁿ. उदाहरण के लिए समस्या $(((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))$ में सबसे सामान्य एकीकरणकर्ता है' $\{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}$, सीf. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय जटिलता से बचने के लिए उन्नत एकीकरण एल्गोरिथम पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।

अनुप्रयोग: लॉजिक प्रोग्रामिंग में एकीकरण

एकीकरण की अवधारणा लॉजिक प्रोग्रामिंग के पीछे मुख्य विचारों में से एक है, जिसे प्रोलॉग लैंग्वेज के माध्यम से जाना जाता है। यह चर की सामग्री को बांधने के तंत्र का प्रतिनिधित्व करता है और इसे एक प्रकार के एक बार के असाइनमेंट के रूप में देखा जा सकता है। प्रोलॉग में इस ऑपरेशन को समानता प्रतीक द्वारा दर्शाया जाता है = लेकिन चर को इंस्टेंटिएट करते समय भी किया जाता है (नीचे देखें)। समानता चिन्ह के प्रयोग से इसका प्रयोग अन्य लैंग्वेज में भी किया जाता है =अपितु कई ऑपरेशनों के संयोजन में भी सम्मिलित होता है +, -, *, /. प्रकार अनुमान एल्गोरिथम सामान्यतः एकीकरण पर आधारित होते हैं।

प्रोलॉग में:

1. एक चर (प्रोग्रामिंग) जो अनइंस्टेंटिफाइड है—अर्थात् इस पर कोई पिछला एकीकरण नहीं किया गया था - इसे एक परमाणु, एक शब्द या किसी अन्य असंतुलित चर के साथ एकीकृत किया जा सकता है, इस प्रकार प्रभावी रूप से इसका अलियास बन जाता है। कई आधुनिक प्रोलॉग बोलियों और प्रथम-क्रम लॉजिक में एक चर को उस शब्द के साथ एकीकृत नहीं किया जा सकता है जिसमें वह सम्मिलित है; यह तथाकथित घटित जाँच है।
2. दो परमाणु तभी एकीकृत हो सकते हैं जब वे समान हों जाते है।
3. इसी प्रकार, एक पद को दूसरे पद के साथ एकीकृत किया जा सकता है यदि पदों के शीर्ष फलन प्रतीक और गुणधर्म समान हैं और यदि मापदंडों को एक साथ एकीकृत किया जा सकता है। ध्यान दें कि यह एक पुनरावर्ती व्यवहार है।

अनुप्रयोग: प्रकार अनुमान

कार्यात्मक लैंग्वेज हास्केल (प्रोग्रामिंग लैंग्वेज) और एमएल (प्रोग्रामिंग लैंग्वेज) सहित हिंडले-मिलनर प्रकार प्रणाली पर आधारित प्रकार प्रणालियों वाली लैंग्वेज के लिए प्रकार अनुमान के समय एकीकरण का उपयोग किया जाता है। एक ओर प्रोग्रामर को प्रत्येक फलन के लिए प्रकार की जानकारी प्रदान करने की आवश्यकता नहीं होती है, दूसरी ओर इसका उपयोग टाइपिंग त्रुटियों का पता लगाने के लिए किया जाता है। हास्केल अभिव्यक्तियों ट्रू  : ['x', 'y', 'z'] सही ढंग से टाइप नहीं किया गया है. सूची निर्माण फलन (:) प्रकार का है a -> [a] -> [a], और पहले लॉजिक के लिएट्रूबहुरूपी प्रकार चर a के साथ एकाकार होना होगा ट्रूका प्रकार बूल. दूसरा लॉजिक , ['x', 'y', 'z'], प्रकार का है [चार], लेकिन a दोनों नहीं हो सकते बूल औरचार एक ही समय पर होते है.

प्रोलॉग के प्रकार अनुमान के लिए एक एल्गोरिथम दिया जा सकता है:

1. कोई भी प्रकार का चर किसी भी प्रकार की अभिव्यक्तियों के साथ एकीकृत होता है और उस अभिव्यक्तियों के लिए त्वरित होता है। एक विशिष्ट सिद्धांत इस नियम को घटित जाँच के साथ प्रतिबंधित कर सकता है।
2. दो प्रकार के स्थिरांक तभी एकीकृत होते हैं जब वे एक ही प्रकार के हों जाते है।
3. दो प्रकार के निर्माण मात्र तभी एकीकृत होते हैं जब वे एक ही प्रकार के कंस्ट्रक्टर के अनुप्रयोग होते हैं और उनके सभी घटक प्रकार पुनरावर्ती रूप से एकीकृत होते हैं।

इसकी घोषणात्मक प्रकृति के कारण एकीकरण के अनुक्रम में क्रम (सामान्यतः) महत्वहीन है।

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

अनुप्रयोग: फ़ीचर संरचना एकीकरण

See also: फ़ीचर संरचना

अभिकलनात्मक लैंग्वेज विज्ञान के विभिन्न अनुसंधान क्षेत्रों में एकीकरण के रूप में उपयोग किया गया है।

क्रमानुसार एकीकरण

क्रमबद्ध लॉजिक प्रत्येक पद के लिए एक सॉर्ट या प्रकार निर्दिष्ट करने और एक सॉर्ट s1 घोषित करने की अनुमति देता है, दूसरे प्रकार का एक उपवर्ग s₂, घोषित करने की अनुमति देता है, जिसे आमतौर पर s1 ⊆ s2 के रूप में लिखा जाता है। उदाहरण के लिए जैविक प्राणियों के बारे में लॉजिक करते समय एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग के रूप में घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है।

उदाहरण के लिए एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की तरह है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवर लोडिंग कहा जाता है, प्रोग्रामिंग लैंग्वेज में ओवरलोडिंग के समान हो जाता है.

क्रिस्टोफ़ वाल्थर ने क्रम-क्रमबद्ध लॉजिक में शब्दों के लिए एक एकीकरण एल्गोरिथम दिया जाता है, जिसके लिए किन्हीं दो घोषित प्रकारों की आवश्यकता होती हैs₁, s₂ उनका प्रतिच्छेदन s₁ ∩ s₂ घोषित किया जाना भी है : यदि x₁ और x₂ सॉर्ट का एक चर हैs₁,और s₂, क्रमशः, समीकरण x₁ ≐ x₂ हल के रूप में है {x₁ = x, x₂ = x }, जहां x: s₁ ∩ s₂.

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

पैरामीट्रिक बहुरूपता की अनुमति देने के लिए स्मोल्का ने क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया जाता है।

उनके ढांचे में उप-घोषणाएँ सम्मिश्र प्रकार की अभिव्यक्तियों के लिए प्रचारित की जाती हैं।

एक प्रोग्रामिंग उदाहरण के रूप में एक पैरामीट्रिक सॉर्ट सूची (X) घोषित की जा सकती है (टेम्प्लेट (C++)# फलन टेम्पलेट्स |C++ टेम्प्लेट में X एक प्रकार का पैरामीटर है), और एक सबसॉर्ट घोषणा से int ⊆ संबंध सूची फ़्लोट करें (int ) ⊆ सूची (फ्लोट) का स्वचालित रूप से अनुमान लगाया जाता है, जिसका अर्थ है कि पूर्णांकों की प्रत्येक सूची भी फ्लोट्स की एक सूची है।

श्मिट-शाउß ने शब्द घोषणाओं की अनुमति देने के लिए क्रम-क्रमबद्ध लॉजिक को सामान्यीकृत किया। उदाहरण के तौर पर, उपवर्ग घोषणाओं को सम ⊆ int और विषम ⊆ int मानते हुए, एक शब्द घोषणा जैसे ∀ i : int। (i + i): पूर्णांक जोड़ की एक संपत्ति घोषित करने की भी अनुमति देता है जिसे सामान्य ओवरलोडिंग द्वारा व्यक्त नहीं किया जा सकता है।

अनंत पदों का एकीकरण

अनंत पेड़ों पर पृष्ठभूमि:

• बी कौरसेल (1983). "अनंत ट्री के मौलिक गुण". सैद्धांतिक संगणना विज्ञान. 25 (2): 95–169. doi:10.1016/0304-3975(83)90059-2.
• माइकल जे. महर (जुलाई 1988)"परिमित, तर्कसंगत और अनंत पेड़ों के बीजगणित के पूर्ण स्वयंसिद्ध!"प्रोक. आईईईई तीसरा वार्षिक संगोष्ठी पर कंप्यूटर विज्ञान में तर्क, एडिनबर्ग.पृ. 348-357
• Joxan Jaffar; Peter J. Stuckey (1986). "अनंत वृक्ष तर्क प्रोग्रामिंग के शब्दार्थ". Theoretical Computer Science. 46: 141–158. doi:10.1016/0304-3975(86)90027-7.

एकीकरण कलन विधि , प्रोलॉग II:

• ए कोलमेरौएर (1982). के.एल. क्लार्क; एस.-ए. टार्नलुंड (eds.). प्रोलॉग और अनंत पेड़. अकादमिक प्रेस.
• एलेन कोलम्योर (1984)"परिमित और अनंत पेड़ों पर समीकरण और असमानताएं"आईसीयू (एडी) में प्रक्रिया समझौता। पांचवीं पीढ़ी कंप्यूटर सिस्टम पर पृ. 85-99 अनुप्रयोग।

• फ्रांसिस जियानेसिनी; जैक्स कोहेन (1984). "प्रोलॉग के अनंत पेड़ों का उपयोग करके पार्सर जेनरेशन और व्याकरण हेरफेर". जर्नल ऑफ़ लॉजिक प्रोग्रामिंग. 1 (3): 253–265. doi:10.1016/0743-1066(84)90013-X.

ई-एकीकरण

ई- एकीकरण समीकरण के दिए गए समुच्चय का हल खोजने की समस्या है.

कुछ समीकरणात्मक पृष्ठभूमि ज्ञान E को ध्यान में रखते हुए।

उत्तरार्द्ध को सार्वभौमिक समानता के एक समुच्चय के रूप में दिया गया है।

कुछ विशेष समुच्चय E के लिए समीकरण हल करने वाले एल्गोरिथम (उर्फ ई- एकीकरण एल्गोरिदम) तैयार किए गए हैं;

दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई एल्गोरिथम उपलब्ध नहीं हो सकता है।

उदाहरण के लिए, यदि a और b विशिष्ट स्थिरांक हैं,

समीकरण $x*a\doteq y*b$ का कोई हल नहीं है.

विशुद्ध वाक्यात्मकएकीकरण में संबंध हो जाता है

जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है $*$.

चूंकि यदि $*$ क्रमविनिमेय माना जाता है,

फिर प्रतिस्थापन {x ↦ b, y ↦ a} उपरोक्त समीकरण को हल करता है,

जब से,

	$x*a$	{x ↦ b, y ↦ a}
=	$b*a$		प्रतिस्थापन अनुप्रयोग द्वारा
=	$a*b$		की क्रमपरिवर्तनशीलता द्वारा $*$
=	$y*b$	{x ↦ b, y ↦ a}	(विपरीत) प्रतिस्थापन अनुप्रयोग द्वारा

पृष्ठभूमि ज्ञान E की क्रम परिवर्तनशीलता बता सकता है $*$ सार्वभौम समानता द्वारा$u*v=v*u$ सभी के लिए u, v .

विशेष पृष्ठभूमि ज्ञान समुच्चय E

Used naming conventions

∀ u,v,w:	$u*(v*w)$	=	$(u*v)*w$	A	की संबद्धता $*$
∀ u,v:	$u*v$	=	$v*u$	C	की क्रमपरिवर्तनशीलता $*$
∀ u,v,w:	$u*(v+w)$	=	$u*v+u*w$	Dl	का वाम वितरण ∗ ऊपर +
∀ u,v,w:	$(v+w)*u$	=	$v*u+w*u$	Dr	का सही वितरण ∗ ऊपर +
∀ u:	$u*u$	=	u	I	नपुंसकताof $*$
∀ u:	$n*u$	=	u	Nl	के संबंध में तटस्थ तत्व n छोड़ दिया $*$
∀ u:	$u*n$	=	u	Nr	के संबंध में सही तटस्थ तत्व n ** $*$

ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए निर्णायक होता है, यदि इसके लिए एक एकीकरण एल्गोरिथम तैयार किया गया है, जो किसी भी इनपुट समस्या के लिए समाप्त हो जाता है।

ऐसा कहा जाता है कि एकीकरण एक सिद्धांत के लिए अर्ध-निर्णायक है, यदि इसके लिए एक एकीकरण एल्गोरिथम तैयार किया गया है, जो किसी भी हल करने योग्य इनपुट समस्या के लिए समाप्त हो जाता है, लेकिन एक अघुलनशील इनपुट समस्या के हल के लिए निरंतर के लिए खोज जारी रख सकता है।

निम्नलिखित सिद्धांतों के लिए ' एकीकरण निर्णायक है':

• 'A
• A,C
• A,C,I
• A,C,N_l*A,I
• A,N_l,N_r (मोनॉइड)
• C
• बूलियन रिंग
• एबेलियन समूह, यदि हस्ताक्षर को यादृच्छिक ढंग से अतिरिक्त प्रतीकों द्वारा विस्तारित किया गया हो (लेकिन स्वयंसिद्ध नहीं)
• क्रिपके शब्दार्थ#पत्राचार और पूर्णता मोडल बीजगणित

निम्नलिखित सिद्धांतों के लिए एकीकरण अर्ध-निर्णायक है:

• A,D_l,D_r
• A,C,D_l
• क्रमविनिमेय वलय

एकतरफा पैरामोड्यूलेशन

यदि E के लिए एक अभिसरण शब्द पुनर्लेखन प्रणाली आर उपलब्ध है,

'एकतरफा पैरामोड्यूलेशन' एल्गोरिदम

दिए गए समीकरणों के सभी समाधानों के रूप में गिनने के लिए उपयोग किया जा सकता है।

एकतरफ़ा पैरामॉड्यूलेशन नियम

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(...) })।

Example term rewrite system R

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 } के लिए एक सफल उदाहरण गणना पथ नीचे दिखाया गया है। परिवर्तनीय नाम टकराव से बचने के लिए, नियम परिवर्तन द्वारा उनके उपयोग से पहले हर बार पुनर्लेखन नियमों का लगातार नाम बदला जाता है; v₂, v₃, ... इस उद्देश्य के लिए कंप्यूटर-जनित परिवर्तनीय नाम हैं। प्रत्येक पंक्ति में, 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 }; यह यहां नहीं दिखाया गया है. कोई अन्य मार्ग सफलता की ओर नहीं ले जाता।

उदाहरण एकीकरण अभिकलन

प्रयुक्त नियम		G	S
		{ app(x,app(y,x)) ≐ a.a.nil }	{}
म्यूटेट(2)	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2.app(v3,v4) ≐ a.a.nil }	{}
डीकोम्पोस	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{}
एलिमिनेट	⇒	{ app(y,v2.v3) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{ x ↦ v2.v3 }
एलिमिनेट	⇒	{ 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 }
एलिमिनेट	⇒	{ y ≐ nil, a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
एलिमिनेट	⇒	{ a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
म्यूटेट(1)	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ v6, v6 ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
एलिमिनेट	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
एलिमिनेट	⇒	{ a.nil ≐ v4, v4 ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
एलिमिनेट	⇒	{ a.nil ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{ a ≐ a, nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{ nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
डीकोम्पोस	⇒	{}	{ y ↦ nil, x ↦ a.nil }

संकुचन

पुनर्लेखन नियम का उपयोग करते हुए एकीकृत प्रतिस्थापन σ (निचली पंक्ति) के साथ, पद s में स्थिति p पर चरण s ↝ t को संकीर्ण करने का त्रिभुज आरेख l → r (सबसे ऊपर की कतार)

यदि R, E के लिए एक अभिसारी पद पुनर्लेखन प्रणाली है,

पिछले अनुभाग के लिए एक दृष्टिकोण विकल्प में 'संकीर्ण चरणों' का क्रमिक अनुप्रयोग सम्मिलित है;

यह अंततः किसी दिए गए समीकरण के सभी समाधानों की गणना करेगा।

एक संकीर्ण चरण (cf. चित्र) के रूप में सम्मिलित है

• वर्तमान पद का एक गैर-परिवर्तनीय उपपद चुनना है,
• आर से एक नियम के बाईं ओर इसे वाक्यात्मकरूप से एकीकृत करना, और
• तात्कालिक नियम के दाहिने हाथ को तात्कालिक शब्द में बदलना होता है।

फॉर्मल रूप से, यदि l → r आर से पुनर्लेखन नियम की एक पुनर्नामित प्रति है, जिसमें शब्द एस और उपपद के साथ कोई चर समान नहीं है s|_p एक चर नहीं है और इसके साथ एकीकृत किया जा सकता है l प्रथम-क्रम शब्दों के # वाक्यात्मकएकीकरण के माध्यम से σ, तब s को इस शब्द तक सीमित किया जा सकता है t = sσ[rσ]_p, अर्थात पद के लिए sσ, पी पर सबटर्म के साथ टर्म (लॉजिक)#ऑपरेशन्स विद टर्म्स बाय rσ. वह स्थिति जिसमें s को t तक सीमित किया जा सकता है, सामान्यतः s ↝ t के रूप में निरूपित की जाती है।

सहज रूप से, संकीर्ण चरणों का एक क्रम टी₁ ↝ टी₂ ↝ ... ↝ टी_n इसे पुनः लिखने के चरणों के अनुक्रम के रूप में सोचा जा सकता है₁ → टी₂ → ... → टी_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

अंतिम पद, वी₂।में₂.nil को मूल दाहिनी ओर के शब्द a.a.nil के साथ वाक्यात्मकरूप से एकीकृत किया जा सकता है।

सिकुड़ती लेम्मा यह सुनिश्चित करता है कि जब भी किसी शब्द के उदाहरण को एक अभिसरण शब्द पुनर्लेखन प्रणाली द्वारा किसी शब्द t में फिर से लिखा जा सकता है, तो s और t को संकुचित किया जा सकता है और एक शब्द में फिर से लिखा जा सकता है s′ और t′, क्रमशः, ऐसे कि t′ का एक उदाहरण है s′.

फॉर्मल रूप से: जब भी sσ →∗ t कुछ प्रतिस्थापन के लिए σ रखता है, तो वहां शर्तें उपलब्ध हैं s′, t′ ऐसा है कि s ↝∗ s′ और t →∗ t′ और s′ τ = t′ कुछ प्रतिस्थापन के लिए τ.

उच्च-क्रम एकीकरण

गोल्डफ़ार्ब मेंहिल्बर्ट की 10वीं समस्या को दूसरे क्रम की एकीकरणीयता, समीकरण में घटाना $X_{1}*X_{2}=X_{3}$ फलन चर के साथ चित्रित एकीकरण समस्या से मेल खाता है $F_{i}$ तदनुसार $X_{i}$ और $G$ ताजा चर.

कई अनुप्रयोगों के लिए प्रथम-क्रम शब्दों के अतिरिक्त टाइप किए गए लैम्ब्डा-शब्दों के एकीकरण पर विचार करने की आवश्यकता होती है। इस प्रकार के एकीकरण को अधिकांशतः उच्च-क्रम एकीकरण कहा जाता है। उच्च-क्रम एकीकरण अनिर्णीत समस्या है, और ऐसी एकीकरण समस्याओं में अधिकांश सामान्य एकीकरणकर्ता नहीं होते हैं। उदाहरण के लिए, एकीकरण समस्या { 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. डी(बी,ए,सी) }. उच्च-क्रम एकीकरण की एक अच्छी प्रकार से अध्ययन की गई शाखा αβη रूपांतरणों द्वारा निर्धारित समानता को सरल रूप से टाइप किए गए लैम्ब्डा शब्दों मॉड्यूलो को एकीकृत करने की समस्या है। जेरार्ड ह्यूएट ने एक अर्ध-निर्णायक (पूर्व) एकीकरण एल्गोरिथम दिया जो एकीकरणकर्ताओं के समष्टि की व्यवस्थित खोज की अनुमति देता है (मार्टेली-मोंटानारी के एकीकरण एल्गोरिथम को सामान्यीकृत करना)उच्च-क्रम वाले चर वाले शब्दों के नियमों के साथ) जो व्यवहार में पर्याप्त रूप से अच्छी प्रकार से काम करता प्रतीत होता है। Huet और गाइल्स डोवेक इस विषय पर सर्वेक्षण करते हुए लेख लिखे हैं।

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

अभिकलनात्मक लैंग्वेज विज्ञान में अण्डाकार निर्माण के सबसे प्रभावशाली सिद्धांतों में से एक यह है कि दीर्घवृत्त को मुक्त चर द्वारा दर्शाया जाता है, जिनके मान तब उच्च-क्रम एकीकरण का उपयोग करके निर्धारित किए जाते हैं। उदाहरण के लिए जॉन का अर्थपूर्ण प्रतिनिधित्व मैरी को पसंद है और पीटर को भी पसंद है like(j, m) ∧ R(p) और आर का मान (दीर्घवृत्त का अर्थपूर्ण प्रतिनिधित्व) समीकरण द्वारा निर्धारित किया जाता है like(j, m) = R(j) . ऐसे समीकरणों को हल करने की प्रक्रिया को उच्च-क्रम एकीकरण कहा जाता है।

वेन स्नाइडर ने उच्च-क्रम एकीकरण और ई- एकीकरण दोनों का सामान्यीकरण दिया, अर्थात लैम्ब्डा-शब्द मॉड्यूलो को एक समीकरण सिद्धांत को एकीकृत करने के लिए एक एल्गोरिदम।

यह भी देखें

• पुनर्लेखन
• स्वीकार्य नियम
• लैम्ब्डा कैलकुलस में स्पष्ट प्रतिस्थापन
• गणितीय समीकरण हल करना
• डिस- एकीकरण (कंप्यूटर विज्ञान)|डिस-यूनिफिकेशन: सिंबॉलिक अभिव्यक्तियों के बीच असमानताओं को हल करना
• एंटी- एकीकरण (कंप्यूटर साइंस)|एंटी-यूनिफिकेशन: दो शब्दों के कम से कम सामान्य सामान्यीकरण (एलजीजी) की गणना करना, सबसे सामान्य उदाहरण (एमजीयू) की गणना करना
• सब्समिशन जाली, एक जाली जिसमें मिलन के रूप में एकीकरण और जुड़ने के रूप में विरोधी एकीकरण होता है
• ओन्टोलॉजी संरेखण (शब्दार्थ तुल्यता के साथ एकीकरण का उपयोग करें)

अग्रिम पठन

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