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

लॉजिक और कंप्यूटर विज्ञान में यूनिफिकेशन सिंबॉलिक एक्सप्रेशन (गणित) के बीच समीकरणों को हल करने की कलनविधि प्रक्रिया का उपयोग किया जाता है। उदाहरण के लिए 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$ शब्दों या एक्सप्रेशन का. समीकरण सेट या यूनिफिकेशन समस्या में किन एक्सप्रेशन या शब्दों को घटित होने की अनुमति दी जाती है और किस एक्सप्रेशन को समान माना जाता है, इसके आधार पर यूनिफिकेशन के रूप में कई ढांचे प्रतिष्ठित हैं। यदि उच्च-क्रम वाले चर अर्थात फलन (गणित) का प्रतिनिधित्व करने वाले चर, को एक एक्सप्रेशन में अनुमति दी जाती है, तो प्रक्रिया को 'उच्च-क्रम एकीकरण' कहा जाता है, अन्यथा 'प्रथम-क्रम एकीकरण' का रूप कहा जाता है। यदि प्रत्येक समीकरण के दोनों पक्षों को वस्तुतः समान बनाने के लिए किसी सलूशन की आवश्यकता होती है, तो प्रक्रिया को 'वाक्यविन्यास' या 'मुक्त एकीकरण' कहा जाता है, अन्यथा सिमेंटिक या 'समीकरणात्मक यूनिफिकेशन या ई-यूनिफिकेशन या यूनिफिकेशन मॉड्यूलो सिद्धांत कहा जाता है।

यदि प्रत्येक समीकरण का दाहिना भाग बंद है, को E मुक्त चर नहीं है, तो समस्या को पैटर्न मिलान कहा जाता है। प्रत्येक समीकरण के बाईं ओर चर के साथ पैटर्न का रूप कहा जाता है।

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

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

• एक अनंत समुच्चय $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.
• 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:

• ए कोलमेरौएर (1982). के.एल. क्लार्क; एस.-ए. टार्नलुंड (eds.). प्रोलॉग और अनंत पेड़. अकादमिक प्रेस.
• Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). प्रोक. इंट. कॉन्फ़. पांचवीं पीढ़ी के कंप्यूटर सिस्टम पर. pp. 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	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
• क्रमविनिमेय वलय

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

यदि 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.