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

तर्क और कंप्यूटर विज्ञान में, एकीकरण प्रतीकात्मक अभिव्यक्ति (गणित) के बीच समीकरणों को हल करने की एक एल्गोरिथम प्रक्रिया का रूप है। उदाहरण के लिए, चर के रूप में 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 ↦ (कोई भी मान) } होता है।

प्रतिस्थापन

Main article: Substitution (logic)

प्रतिस्थापन एक मानचित्रण है $\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$ सहायक चर जैसे कि कोई समीकरण नहीं $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)$.}}</ref>

समाधान सेट

एक प्रतिस्थापन σ एकीकरण समस्या ई का एक समाधान है यदि l_iσ ≡ r_iσ के लिए $i=1,...,n$. ऐसे प्रतिस्थापन को ई का एकीकरणकर्ता भी कहा जाता है। उदाहरण के लिए, यदि ⊕ साहचर्य है, तो एकीकरण समस्या {x ⊕ a ≐ a ⊕ x } के समाधान हैं {x ↦ a' '}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a}, आदि ., जबकि समस्या { x ⊕ a ≐ a } का कोई समाधान नहीं है।

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

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

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

वाक्यविन्यास की दृष्टि से एकीकृत शब्दों का योजनाबद्ध त्रिभुज आरेख टी₁ और टी₂ एक प्रतिस्थापन द्वारा पी

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

यह प्रथम-क्रम के पदों के समुच्चय T पर आधारित है (चरों के कुछ दिए गए समुच्चय V, स्थिरांकों के C और F पर)_n n-ary फलन प्रतीकों का) और ≡ वाक्यगत समानता पर है। इस ढांचे में, प्रत्येक समाधान योग्य एकीकरण समस्या {l₁ ≐ r₁, ..., l_n ≐ r_n} के पास पूर्ण, और स्पष्ट रूप से न्यूनतम, एकल (गणित) समाधान सेट है {σ}. इसके सदस्य σ को समस्या का सबसे सामान्य एकीकरणकर्ता (एमजीयू) कहा जाता है। जब एमजीयू लागू किया जाता है तो प्रत्येक संभावित समीकरण के बायीं और दायीं ओर के पद वाक्यात्मक रूप से समतुल्य हो जाते हैं। l₁σ = r₁σ ∧ ... ∧ l_nσ = r_nσ. समस्या का कोई भी एकीकरणकर्ता समाहित हो जाता है एमजीयू द्वारा σ. एमजीयू वेरिएंट तक अद्वितीय है: यदि एस₁ और एस₂ दोनों एक ही वाक्यात्मक एकीकरण समस्या के पूर्ण और न्यूनतम समाधान सेट हैं, तो एस₁ = {पी₁ } और एस₂ = {पी₂ } कुछ प्रतिस्थापनों के लिए σ₁ और σ₂, और 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) }	.

यह सबसे सामान्य एकीकरणकर्ता भी है। समान समस्या के लिए अन्य एकीकरणकर्ता हैं, उदा. { एक्स ↦ एफ(एक्स₁), 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) द्वारा दिया गया पहला एल्गोरिदम अधिक अप्रभावी था; सी एफ डिब्बा। निम्नलिखित तेज़ एल्गोरिदम की उत्पत्ति मार्टेली, मोंटानारी (1982) से हुई। यह पेपर एक कुशल वाक्यात्मक एकीकरण एल्गोरिदम खोजने के पिछले प्रयासों को भी सूचीबद्ध करता है, और बताता है कि रैखिक-समय एल्गोरिदम की खोज मार्टेली, मोंटानारी (1976) द्वारा स्वतंत्र रूप से की गई थी।और पैटरसन, वेगमैन (1976, 1978).

एक परिमित समुच्चय दिया गया है $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$ संभावित समीकरणों का, एल्गोरिथ्म इसे फॉर्म के समीकरणों के समतुल्य सेट में बदलने के लिए नियम लागू करता है { एक्स₁ ≐ यू₁, ..., एक्स_m ≐ यू_m } कहां एक्स₁, ..., एक्स_m भिन्न-भिन्न चर हैं और यू₁, ..., में_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: Occurs check

एक चर x को एक ऐसे पद के साथ एकीकृत करने का प्रयास जिसमें x एक सख्त उपपद x ≐ f(..., x, ...) के रूप में हो, x के समाधान के रूप में एक अनंत पद की ओर ले जाएगा, क्योंकि x स्वयं के एक उपपद के रूप में घटित होगा . जैसा कि ऊपर परिभाषित किया गया है (परिमित) प्रथम-क्रम शब्दों के सेट में, समीकरण x ≐ f(..., x, ...) का कोई समाधान नहीं है; इसलिए उन्मूलन नियम मात्र तभी लागू किया जा सकता है यदि x ∉ vars(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 कम हो जाता है, क्योंकि कम से कम बायीं ओर का सबसे बाहरी एफ गायब हो जाता है। बाकी किसी भी नियम को लागू करने से डिलीट या चेक नहीं बढ़ सकेगा n_lhs, लेकिन घट जाती है n_eqn. इसलिए, किसी भी नियम को लागू करने से तीन गुना कम हो जाता है $\langle n_{var},n_{lhs},n_{eqn}\rangle$ शब्दकोषीय क्रम के संबंध में, जो मात्र सीमित संख्या में ही संभव है।

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

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

प्रोलॉग सिंटैक्टिकल कन्वेंशन में अपरकेस अक्षर से प्रारंभ होने वाला प्रतीक एक परिवर्तनीय नाम है; एक प्रतीक जो छोटे अक्षर से प्रारंभ होता है वह एक फलन प्रतीक है; अल्पविराम का उपयोग तार्किक और ऑपरेटर के रूप में किया जाता है। गणितीय संकेतन के लिए, x,y,z को चर के रूप में, f,g को फलन प्रतीकों के रूप में, और a,b को स्थिरांक के रूप में उपयोग किया जाता है।

Prolog notation	Mathematical notation	Unifying substitution	Explanation
a = a	{ a = a }	{}	Succeeds. (tautology)
a = b	{ a = b }	⊥	a and b do not match
X = X	{ x = x }	{}	Succeeds. (tautology)
a = X	{ a = x }	{ x ↦ a }	x is unified with the constant a
X = Y	{ x = y }	{ x ↦ y }	x and y are aliased
f(a,X) = f(a,b)	{ f(a,x) = f(a,b) }	{ x ↦ b }	function and constant symbols match, x is unified with the constant b
f(a) = g(a)	{ f(a) = g(a) }	⊥	f and g do not match
f(X) = f(Y)	{ f(x) = f(y) }	{ x ↦ y }	x and y are aliased
f(X) = g(Y)	{ f(x) = g(y) }	⊥	f and g do not match
f(X) = f(Y,Z)	{ f(x) = f(y,z) }	⊥	Fails. The f function symbols have different arity
f(g(X)) = f(Y)	{ f(g(x)) = f(y) }	{ y ↦ g(x) }	Unifies y with the term $g(x)$
f(g(X),X) = f(Y,a)	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	Unifies x with constant a, and y with the term $g(a)$
X = f(X)	{ x = f(x) }	should be ⊥	Returns ⊥ in first-order logic and many modern Prolog dialects (enforced by the occurs check). Succeeds in traditional Prolog and in Prolog II, unifying x with infinite term x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y, y = a }	{ x ↦ a, y ↦ a }	Both x and y are unified with the constant a
a = Y, X = Y	{ a = y, x = y }	{ x ↦ a, y ↦ a }	As above (order of equations in set doesn't matter)
X = a, b = X	{ x = a, b = x }	⊥	Fails. a and b do not match, so x can't be unified with both

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

टर्म (तर्क)#शब्दों के साथ संचालन की वाक्यात्मक प्रथम-क्रम एकीकरण समस्या का सबसे सामान्य एकीकरणकर्ता 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))\}$, सीएफ. चित्र। इस प्रकार के विस्फोट के कारण होने वाली घातीय समय सम्मिश्रता से बचने के लिए, उन्नत एकीकरण एल्गोरिदम पेड़ों के अतिरिक्त निर्देशित एसाइक्लिक आलेख़ (डैग) पर काम करते हैं।

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

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

प्रोलॉग में:

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

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

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

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

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

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

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

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

See also: Feature structure

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

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

क्रमबद्ध तर्क प्रत्येक पद के लिए एक सॉर्ट, या प्रकार निर्दिष्ट करने और एक सॉर्ट एस घोषित करने की अनुमति देता है₁ दूसरे प्रकार का एक उपवर्ग s₂, सामान्यतः एस के रूप में लिखा जाता है₁ ⊆ एस₂. उदाहरण के लिए, जैविक प्राणियों के बारे में तर्क करते समय, एक प्रकार के कुत्ते को एक प्रकार के जानवर का उपवर्ग घोषित करना उपयोगी होता है। जहां भी किसी प्रकार के शब्द की आवश्यकता होती है, उसके समष्टि पर किसी भी प्रकार के शब्द की आपूर्ति की जा सकती है। उदाहरण के लिए, एक फलन घोषणा मां: जानवर → जानवर, और एक निरंतर घोषणा लस्सी: कुत्ता मानते हुए, मां (लस्सी) शब्द पूरी प्रकार से मान्य है और इसमें जानवर की प्रकार है। यह जानकारी प्रदान करने के लिए कि कुत्ते की माँ बदले में एक कुत्ता है, एक और घोषणा माँ: कुत्ता → कुत्ता जारी की जा सकती है; इसे फलन ओवरलोडिंग कहा जाता है, प्रोग्रामिंग भाषाओं में ओवरलोडिंग के समान।

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

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

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

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

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

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

ई-एकीकरण

ई-एकीकरण समीकरणों के दिए गए सेट का समाधान खोजने की समस्या है, कुछ समीकरणात्मक पृष्ठभूमि ज्ञान ई को ध्यान में रखते हुए। उत्तरार्द्ध को सार्वभौमिक समानता के एक सेट के रूप में दिया गया है। कुछ विशेष सेट ई के लिए, समीकरण हल करने वाले एल्गोरिदम (उर्फ ई-एकीकरण एल्गोरिदम) तैयार किए गए हैं; दूसरों के लिए यह सिद्ध हो चुका है कि ऐसा कोई एल्गोरिदम उपलब्ध नहीं हो सकता।

उदाहरण के लिए, यदि a और b विशिष्ट स्थिरांक हैं, समीकरण $x*a\doteq y*b$ का कोई समाधान नहीं है विशुद्ध वाक्यात्मक एकीकरण के संबंध में, जहां संचालक के बारे में कुछ भी पता नहीं चल पाया है $*$. चूंकि, यदि $*$ क्रमविनिमेय माना जाता है, फिर प्रतिस्थापन {x ↦ b, y ↦ a} उपरोक्त समीकरण को हल करता है, तब से

	$x*a$	{x ↦ b, y ↦ a}
=	$b*a$		by substitution application
=	$a*b$		by commutativity of $*$
=	$y*b$	{x ↦ b, y ↦ a}	by (converse) substitution application

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

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

Used naming conventions

∀ u,v,w:	$u*(v*w)$	=	$(u*v)*w$	A	Associativity of $*$
∀ u,v:	$u*v$	=	$v*u$	C	Commutativity of $*$
∀ u,v,w:	$u*(v+w)$	=	$u*v+u*w$	Dl	Left distributivity of $*$ over $+$
∀ u,v,w:	$(v+w)*u$	=	$v*u+w*u$	Dr	Right distributivity of $*$ over $+$
∀ u:	$u*u$	=	u	I	Idempotence of $*$
∀ u:	$n*u$	=	u	Nl	Left neutral element n with respect to $*$
∀ u:	$u*n$	=	u	Nr	Right neutral element n with respect to $*$

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

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

• '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
• क्रमविनिमेय वलय

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

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

One-sided paramodulation rules

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 ≠ {} पर समाप्त होते हैं जहां कोई और नियम लागू नहीं होता है (जैसे G = { f(...) ≐ g(...) })।

Example term rewrite system R

1	app(nil,z)	→ z
2	app(x.y,z)	→ x.app(y,z)

उदाहरण के लिए, एक शब्द रीराइट सिस्टम आर का उपयोग विपक्ष और शून्य से निर्मित सूचियों के परिशिष्ट ऑपरेटर को परिभाषित करने के लिए किया जाता है; जहां संक्षिप्तता के लिए 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)। पैरामोड्यूलेशन एल्गोरिदम उदाहरण आर के साथ दिए जाने पर उस ई के संबंध में समीकरणों के समाधान की गणना करता है।

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

Example unifier computation

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 }

संकुचन

पुनर्लेखन नियम का उपयोग करते हुए एकीकृत प्रतिस्थापन σ (निचली पंक्ति) के साथ, पद 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. डी(बी,एक्स,सी) }, {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.