التوحيد (علوم الحاسوب)

من الناحية الرسمية، يفترض نهج التوحيد

• مجموعة لانهائية${\displaystyle V}$من المتغيرات . ولتوحيد الرتبة الأعلى، من الملائم اختيار${\displaystyle V}$منفصلة عن مجموعة متغيرات الحدود ذات الحد اللامدا .
• مجموعة${\displaystyle T}$من الشروط بحيث${\displaystyle V\subseteq T}$لتحقيق التوحيد من الدرجة الأولى،${\displaystyle T}$عادةً ما تكون مجموعة الحدود من الدرجة الأولى (الحدود المبنية من رموز المتغيرات والدوال). بالنسبة للتوحيد من الدرجات الأعلى${\displaystyle T}$يتكون من حدود من الدرجة الأولى وحدود لامدا (حدود تحتوي على بعض المتغيرات ذات الرتبة الأعلى).
• رسم الخرائط${\displaystyle {\text{vars}}\colon T\rightarrow }$${\displaystyle \mathbb {P} }$${\displaystyle (V)}$، وتخصيص لكل مصطلح${\displaystyle t}$المجموعة${\displaystyle {\text{vars}}(t)\subsetneq V}$من المتغيرات الحرة التي تحدث في${\displaystyle t}$.
• نظرية أو علاقة تكافؤ${\displaystyle \equiv }$على${\displaystyle T}$، مما يشير إلى المصطلحات التي تُعتبر متساوية. بالنسبة للتوحيد من الدرجة الأولى E،${\displaystyle \equiv }$يعكس ذلك المعرفة الأساسية حول رموز وظائف معينة؛ على سبيل المثال، إذا${\displaystyle \oplus }$تعتبر عملية تبادلية،${\displaystyle t\equiv u}$لو${\displaystyle u}$نتائج من${\displaystyle t}$عن طريق تبديل وسائط${\displaystyle \oplus }$في بعض (وربما جميع) الحالات. ^{[ ملاحظة 1 ]} في الحالة الأكثر شيوعًا، وهي انعدام المعرفة الأساسية تمامًا، تُعتبر المصطلحات المتطابقة حرفيًا أو نحويًا فقط متساوية. في هذه الحالة، يُطلق على ≡ اسم النظرية الحرة (لأنها كائن حر )، أو النظرية الفارغة (لأن مجموعة الجمل المعادلة ، أو المعرفة الأساسية، فارغة)، أو نظرية الدوال غير المفسرة (لأن التوحيد يتم على المصطلحات غير المفسرة )، أو نظرية المُنشئات (لأن جميع رموز الدوال تُنشئ مصطلحات البيانات فقط، بدلًا من العمل عليها). بالنسبة للتوحيد من الرتبة الأعلى، عادةً${\displaystyle t\equiv u}$لو${\displaystyle t}$و${\displaystyle 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 ↦ (أي قيمة) }.

الاستبدال هو عملية ربط${\displaystyle \sigma :V\rightarrow T}$من المتغيرات إلى الحدود؛ الترميز${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$يشير إلى عملية استبدال لكل متغير${\displaystyle x_{i}}$إلى المصطلح${\displaystyle t_{i}}$، ل${\displaystyle i=1,...,k}$وكل متغير آخر لنفسه؛${\displaystyle x_{i}}$يجب أن تكون متميزة ثنائياً. تطبيق هذا الاستبدال على مصطلح${\displaystyle t}$تُكتب في صيغة لاحقة على النحو التالي:${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$ويعني ذلك استبدال كل ظهور لكل متغير (في آن واحد).${\displaystyle x_{i}}$في المصطلح${\displaystyle t}$بواسطة${\displaystyle t_{i}}$النتيجة${\displaystyle t\tau }$تطبيق الاستبدال${\displaystyle \tau }$إلى مصطلح${\displaystyle t}$يُطلق عليه مثال على هذا المصطلح${\displaystyle t}$كمثال من الدرجة الأولى، بتطبيق الاستبدال { x ↦ h ( a , y ), z ↦ b } على الحد

	${\displaystyle f(}$	${\displaystyle {\textbf {x}}}$	${\displaystyle ,a,g()}$	${\displaystyle {\textbf {z}}}$	${\displaystyle ),y)}$
العائد
	${\displaystyle f(}$	${\displaystyle {\textbf {h}}({\textbf {a}},{\textbf {y}})}$	${\displaystyle ,a,g()}$	${\displaystyle {\textbf {b}}}$	${\displaystyle ),y).}$

إذا كان المصطلح${\displaystyle t}$له مثال مكافئ لمصطلح${\displaystyle u}$أي إذا${\displaystyle t\sigma \equiv u}$لبعض الاستبدال${\displaystyle \sigma }$، ثم${\displaystyle t}$يُطلق عليه اسم أكثر عمومية من${\displaystyle u}$، و${\displaystyle u}$يُطلق عليه اسم أكثر خصوصية من، أو مُندمج في،${\displaystyle t}$. على سبيل المثال،${\displaystyle x\oplus a}$هو أكثر عمومية من${\displaystyle a\oplus b}$إذا كانت ⊕ تبديلية ، فعندئذٍ${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$.

إذا كانت علامة ≡ تمثل التطابق الحرفي (النحوي) بين المصطلحات، فقد يكون مصطلح ما أكثر عمومية وخصوصية من مصطلح آخر فقط إذا اختلف المصطلحان في أسماء متغيراتهما فقط، وليس في بنيتهما النحوية؛ وتُسمى هذه المصطلحات متغيرات ، أو إعادة تسمية لبعضها البعض. على سبيل المثال، ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ هو شكل مختلف من ${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$، منذ $${\displaystyle 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})}$$ و $${\displaystyle 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}).}$$ لكن،${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ليس نوعًا مختلفًا من${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$بما أنه لا يمكن لأي استبدال أن يحول الحد الأخير إلى الحد الأول، فإن الحد الأخير بالتالي أكثر خصوصية من الحد الأول.

لـ${\displaystyle \equiv }$قد يكون المصطلح أكثر عمومية وخصوصية من مصطلح مختلف بنيويًا. على سبيل المثال، إذا كان ⊕ متطابقًا ، أي إذا كان دائمًا${\displaystyle x\oplus x\equiv x}$ثم المصطلح${\displaystyle x\oplus y}$هو أكثر عمومية من${\displaystyle z}$، ^{[ ملاحظة 2 ]} والعكس صحيح، ^{[ ملاحظة 3 ]} على الرغم من${\displaystyle x\oplus y}$و${\displaystyle z}$لها بنية مختلفة.

استبدال${\displaystyle \sigma }$أكثر خصوصية من البديل أو يندرج تحته${\displaystyle \tau }$لو${\displaystyle t\sigma }$يتم تضمينها بواسطة${\displaystyle t\tau }$لكل فصل دراسي${\displaystyle t}$ونقول أيضاً أن${\displaystyle \tau }$هو أكثر عمومية من${\displaystyle \sigma }$بصورة أكثر رسمية، خذ مجموعة غير فارغة لا نهائية${\displaystyle V}$من المتغيرات المساعدة بحيث لا توجد معادلة${\displaystyle l_{i}\doteq r_{i}}$تتضمن مسألة التوحيد متغيرات من${\displaystyle V}$ثم استبدال${\displaystyle \sigma }$يتم تضمينها بواسطة بديل آخر${\displaystyle \tau }$في حالة وجود بديل${\displaystyle \theta }$بحيث يكون ذلك لجميع الحدود${\displaystyle X\notin V}$،${\displaystyle X\sigma \equiv X\tau \theta }$[ ^{2 ] على} سبيل المثال${\displaystyle \{x\mapsto a,y\mapsto a\}}$يتم تضمينها بواسطة${\displaystyle \tau =\{x\mapsto y\}}$، استخدام${\displaystyle \theta =\{y\mapsto a\}}$، لكن ${\displaystyle \sigma =\{x\mapsto a\}}$لا يتم تضمينها بواسطة${\displaystyle \tau =\{x\mapsto y\}}$، مثل${\displaystyle f(x,y)\sigma =f(a,y)}$لا يُعد مثالاً على ${\displaystyle f(x,y)\tau =f(y,y)}$[ ^{3 ]​}

يُعدّ الاستبدال σ حلاً لمسألة التوحيد E إذا كان l _i σ ≡ r _i σ لـ${\displaystyle i=1,...,n}$يُطلق على هذا الاستبدال أيضًا اسم موحد E. على سبيل المثال، إذا كانت ⊕ تجميعية ، فإن مسألة التوحيد { x ⊕ a ≐ a ⊕ x } لها الحلول { x ↦ a }، { x ↦ a ⊕ a }، { x ↦ a ⊕ a ⊕ a }، إلخ، بينما المسألة { x ⊕ a ≐ a } ليس لها حل.

بالنسبة لمسألة توحيد معينة E ، تُسمى مجموعة S من الموحدات كاملة إذا تم تضمين كل استبدال حل بواسطة استبدال ما في S. توجد دائمًا مجموعة استبدال كاملة (على سبيل المثال، مجموعة جميع الحلول)، ولكن في بعض الأطر (مثل التوحيد غير المقيد من الرتبة العليا) تكون مشكلة تحديد ما إذا كان هناك أي حل موجود (أي ما إذا كانت مجموعة الاستبدال الكاملة غير فارغة) غير قابلة للتقرير.

تُسمى المجموعة S مجموعةً دنيا إذا لم يكن أيٌّ من عناصرها يشمل عنصرًا آخر. وبحسب الإطار، قد تحتوي مجموعة الاستبدال الكاملة والدنيا على صفر، أو عنصر واحد، أو عدد محدود، أو عدد لا نهائي من العناصر، أو قد لا توجد أصلًا بسبب سلسلة لا نهائية من العناصر الزائدة. ^{[ 4 ]} لذا، تُحسب خوارزميات التوحيد عمومًا تقريبًا محدودًا للمجموعة الكاملة، والذي قد يكون دنيا أو لا، مع أن معظم الخوارزميات تتجنب الموحدات الزائدة قدر الإمكان. ^{[ 2 ]} بالنسبة للتوحيد النحوي من الدرجة الأولى، قدّم مارتيلي ومونتاني ^{[ 5 ]} خوارزمية تُبلغ عن عدم إمكانية الحل أو تحسب موحدًا واحدًا يُشكّل بحد ذاته مجموعة استبدال كاملة ودنيا، ويُسمى الموحد الأكثر عمومية .

ناقش جاك هيربراند المفاهيم الأساسية للتوحيد ورسم مخططًا لخوارزمية في عام 1930. ^{[ 9 ] [ 10 ] [ 11 ]} لكن معظم المؤلفين ينسبون أول خوارزمية توحيد إلى جون آلان روبنسون (انظر المربع). ^{[ 12 ] [ 13 ] [ ملاحظة 5 ]} اتسمت خوارزمية روبنسون بسلوك أسي في أسوأ الحالات من حيث الوقت والمساحة. ^{[ 11 ] [ 15 ]} وقد اقترح العديد من المؤلفين خوارزميات توحيد أكثر كفاءة. ^{[ 16 ]} تم اكتشاف خوارزميات ذات أداء خطي في أسوأ الحالات بشكل مستقل من قبل مارتيلي ومونتانياري (1976) وباترسون وويغمان ( 1976 ) [ ملاحظة ^{6 ] .} يستخدم بادر وسنايدر (2001) تقنية مشابهة لتقنية باترسون-ويغمان، وبالتالي فهو خطي، ^{[ 17 ]} ولكنه، كمعظم خوارزميات التوحيد الخطية، أبطأ من نسخة روبنسون عند استخدام مدخلات صغيرة الحجم نظرًا لتكاليف المعالجة المسبقة للمدخلات والمعالجة اللاحقة للمخرجات، مثل إنشاء تمثيل DAG . يتميز دي شامبو (2022) أيضًا بتعقيد خطي بالنسبة لحجم المدخلات، ولكنه ينافس خوارزمية روبنسون عند استخدام مدخلات صغيرة الحجم. ويتحقق تحسين السرعة باستخدام تمثيل كائني التوجه لحساب المسند، مما يغني عن الحاجة إلى المعالجة المسبقة واللاحقة، ويجعل الكائنات المتغيرة مسؤولة عن إنشاء الاستبدال ومعالجة التداخل. يزعم دي شامبو أن القدرة على إضافة وظائف إلى حساب المسندات المُمثلة ككائنات برمجية توفر فرصًا لتحسين عمليات منطقية أخرى أيضًا. ^{[ 15 ]}

تُعرض الخوارزمية التالية بشكل شائع، وهي مأخوذة من مارتيلي ومونتانياري (1982) . ^{[ ملاحظة 7 ]} بالنظر إلى مجموعة منتهية${\displaystyle 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 . يمكن قراءة مجموعة من هذا الشكل على أنها استبدال. إذا لم يكن هناك حل، تتوقف الخوارزمية بالرمز ⊥؛ يستخدم مؤلفون آخرون الرمز "Ω" أو " فشل " في هذه الحالة. يُرمز لعملية استبدال جميع حالات المتغير x في المسألة G بالحد t بالرمز G { x ↦ t }. ولتبسيط الأمر، تُعتبر الرموز الثابتة رموز دوال ذات وسائط صفرية.

${\displaystyle G\cup \{t\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G}$			يمسح
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}}$			تحلل
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	لو${\displaystyle f\neq g}$أو${\displaystyle k\neq m}$		صراع
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq x\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$			تبديل
${\displaystyle G\cup \{x\doteq t\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}$	لو${\displaystyle x\not \in {\text{vars}}(t)}$و${\displaystyle x\in {\text{vars}}(G)}$		حذف [ ملاحظة 8 ]
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$	${\displaystyle \Rightarrow }$	${\displaystyle \bot }$	لو${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k}))}$		يفحص

في اصطلاحات لغة برولوج النحوية، يُعتبر الرمز الذي يبدأ بحرف كبير اسم متغير، بينما يُعتبر الرمز الذي يبدأ بحرف صغير رمز دالة. وتُستخدم الفاصلة كعامل منطقي "و" . أما في الترميز الرياضي ، فتُستخدم x وy وz كمتغيرات، و f وg كرموز دوال، و a وb كثوابت.

تدوين برولوج	الترميز الرياضي	الاستبدال الموحد	توضيح
a = a	{ a = a }	{}	ينجح. ( تكرار )
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 مع المصطلح ⁠${\displaystyle g(x)}$⁠
f(g(X),X) = f(Y,a)	{ f ( g ( x ), x ) = f ( y , a ) }	{ x ↦ a , y ↦ g ( a ) }	يوحد x مع الثابت a ، و y مع الحد ⁠${\displaystyle g(a)}$⁠
X = f(X)	{ x = f ( x ) }	يجب أن يكون ⊥	تُرجع ⊥ في منطق الدرجة الأولى والعديد من لهجات برولوج الحديثة (يتم فرضها بواسطة فحص الأحداث ). ينجح في لغة برولوج التقليدية وفي برولوج 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 حجم يساوي 2n . على سبيل المثال، المسألة ^⁠${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$يمتلك أكثر الموحدين عمومية${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}}$انظر الصورة. لتجنب التعقيد الزمني الأسي الناتج عن هذا التضخم، تعمل خوارزميات التوحيد المتقدمة على الرسوم البيانية الموجهة غير الدورية (DAGs) بدلاً من الأشجار. ^{[ 19 ]}

يُعدّ مفهوم التوحيد أحد الأفكار الرئيسية في البرمجة المنطقية . وبالتحديد، يُمثّل التوحيد لبنة أساسية في عملية الاستدلال ، وهي قاعدة استدلال لتحديد مدى إمكانية تحقيق الصيغ. في لغة برولوج ، يُشير رمز المساواة =إلى التوحيد النحوي من الدرجة الأولى. وهو يُمثّل آلية ربط محتويات المتغيرات، ويمكن اعتباره نوعًا من التعيين لمرة واحدة.

في لغة البرولوج:

1. يمكن توحيد متغير مع ثابت أو حد أو متغير آخر، ليصبح بذلك بديلاً عنه. في العديد من لهجات لغة برولوج الحديثة وفي منطق الرتبة الأولى ، لا يمكن توحيد متغير مع حد يحتويه؛ وهذا ما يُعرف بفحص التكرار .
2. لا يمكن توحيد ثابتين إلا إذا كانا متطابقين.
3. وبالمثل، يمكن توحيد حد مع حد آخر إذا كانت رموز الدالة العليا وعدد معاملات الحدين متطابقة، وإذا أمكن توحيد المعاملات في آن واحد. لاحظ أن هذا سلوك تكراري.
4. معظم العمليات، بما في ذلك +، -، ، *، /، لا يتم تقييمها بواسطة =. لذا، على سبيل المثال 1+2 = 3، لا يمكن تحقيق لأنها مختلفة نحويًا. يُدخل استخدام قيود الحساب الصحيح #=شكلاً من أشكال التوحيد E الذي يتم فيه تفسير هذه العمليات وتقييمها. ^{[ 20 ]}

تعتمد خوارزميات استنتاج الأنواع عادةً على التوحيد، وخاصةً استنتاج أنواع هيندلي-ميلنر المستخدم في لغتي البرمجة الوظيفية هاسكل و ML . على سبيل المثال، عند محاولة استنتاج نوع تعبير هاسكل ، سيستخدم المترجم نوع دالة إنشاء القائمة ، ونوع الوسيط الأول ، ونوع الوسيط الثاني . سيتم توحيد متغير النوع متعدد الأشكال مع ، وسيتم توحيد الوسيط الثاني مع . لا يمكن أن يكون كلا النوعين و في الوقت نفسه، لذلك فإن هذا التعبير غير مُحدد النوع بشكل صحيح.True : ['x']a -> [a] -> [a](:)BoolTrue[Char]['x']aBool[a][Char]aBoolChar

كما هو الحال بالنسبة للغة برولوج، يمكن تقديم خوارزمية لاستنتاج النوع:

1. أي متغير نوعي يتحد مع أي تعبير نوعي، ويتم إنشاء نسخة منه بناءً على ذلك التعبير. قد تقيد نظرية معينة هذه القاعدة بفحص حدوثها.
2. لا يتوحد نوعان ثابتان إلا إذا كانا من نفس النوع.
3. لا تتوحد بنيتان من النوع إلا إذا كانتا تطبيقين لنفس مُنشئ النوع وتتوحد جميع أنواع مكوناتهما بشكل متكرر.

تم استخدام التوحيد في مجالات بحثية مختلفة في اللغويات الحاسوبية. ^{[ 21 ] [ 22 ]}

تم استخدام اصطلاحات التسمية

∀ u , v , w :	⁠${\displaystyle u*(v*w)}$⁠	=	⁠${\displaystyle (u*v)*w}$⁠	أ	خاصية الترابط لـ${\displaystyle *}$⁠
∀ u , v :	⁠${\displaystyle u*v}$⁠	=	⁠${\displaystyle v*u}$⁠	ج	خاصية التبديل لـ${\displaystyle *}$⁠
∀ u , v , w :	⁠${\displaystyle u*(v+w)}$⁠	=	⁠${\displaystyle u*v+u*w}$⁠	دي إل	التوزيع الأيسر لـ${\displaystyle *}$انتهى​​${\displaystyle +}$⁠
∀ u , v , w :	⁠${\displaystyle (v+w)*u}$⁠	=	⁠${\displaystyle v*u+w*u}$⁠	دكتور​	التوزيع الأيمن لـ${\displaystyle *}$انتهى​​${\displaystyle +}$⁠
∀ u :	⁠${\displaystyle u*u}$⁠	=	u	أنا	خاصية التكرار لـ${\displaystyle *}$⁠
∀ u :	⁠${\displaystyle n*u}$⁠	=	u	هولندا​	العنصر المحايد الأيسر n بالنسبة إلى ⁠${\displaystyle *}$⁠
∀ u :	⁠${\displaystyle u*n}$⁠	=	u	رقم ر	العنصر المحايد الأيمن n بالنسبة إلى${\displaystyle *}$⁠

يُقال إن التوحيد قابل للتقرير بالنسبة لنظرية ما، إذا وُضعت لها خوارزمية توحيد تنتهي عند أي مسألة إدخال. ويُقال إن التوحيد شبه قابل للتقرير بالنسبة لنظرية ما، إذا وُضعت لها خوارزمية توحيد تنتهي عند أي مسألة إدخال قابلة للحل ، ولكنها قد تستمر في البحث إلى ما لا نهاية عن حلول لمسألة إدخال غير قابلة للحل.

يمكن تحديد التوحيد للنظريات التالية:

• أ ^{[ 26 ]}
• أ ، ج ^{[ 27 ]}
• أ ، ج ، ي ^{[ 28 ]}
• أ ، ج ، ن _ل ^{[ ملاحظة 9 ] [ 28 ]}
• أ ، أنا ^{[ 29 ]}
• A ، N _l ، N _r (أحادي) ^{[ 30 ]}
• ج ^{[ 28 ]}
• الحلقات المنطقية ^{[ 31 ] [ 32 ]}
• المجموعات الأبيلية ، حتى لو تم توسيع التوقيع بواسطة رموز إضافية عشوائية (ولكن ليس بديهيات) ^{[ 33 ]}
• الجبر الموجه K4 ^{[ 34 ]}

التوحيد قابل للتقرير جزئياً بالنسبة للنظريات التالية:

• أ ، د _ل ، د _ر ^{[ 35 ]}
• أ ، ج ، د _ل ^{[ ملاحظة 9 ] [ 36 ]}
• الحلقات التبادلية ^{[ 33 ]}

إذا كان هناك نظام إعادة كتابة مصطلح متقارب R متاح لـ E ، فيمكن استخدام خوارزمية التعديل البارامتري أحادي الجانب ^{[ 37 ]} لحصر جميع حلول المعادلات المعطاة.

بدءًا من G باعتبارها مسألة التوحيد المراد حلها و S باعتبارها استبدال الهوية، تُطبَّق القواعد بشكل غير حتمي حتى تظهر المجموعة الفارغة كـ G الفعلية، وفي هذه الحالة تكون S الفعلية استبدالًا موحدًا. اعتمادًا على ترتيب تطبيق قواعد التعديل البارامتري، واختيار المعادلة الفعلية من G ، واختيار قواعد R في mutate ، توجد مسارات حسابية مختلفة ممكنة. بعضها فقط يؤدي إلى حل، بينما ينتهي البعض الآخر عند G ≠ {} حيث لا يمكن تطبيق أي قاعدة أخرى (مثل G = { f (...) ≐ g (...) }).

على سبيل المثال، يُستخدم نظام إعادة كتابة المصطلحات R لتعريف عامل الإلحاق للقوائم المُنشأة من cons و nil ؛ حيث تُكتب cons ( x , y ) في صيغة الوسط x.y للاختصار ؛ على سبيل المثال ، app ( 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 . النظرية المعادلة E المقابلة لـ R هي الإغلاق التوافقي لـ R ، وكلاهما يُنظر إليهما كعلاقات ثنائية على المصطلحات . على سبيل المثال، app ( a . b . nil , c . d . nil ) ≡ a . b . c . d . nil ≡ app ( a . b . c . d . nil , nil ). تقوم خوارزمية التعديل البارامتري بحصر حلول المعادلات بالنسبة إلى E عند تغذيتها بالمثال R.

يُعرض أدناه مثالٌ ناجحٌ لمسار حسابي لمسألة التوحيد { app ( x , app ( y , x )) ≐ a . a . nil }. لتجنب تضارب أسماء المتغيرات، تُعاد تسمية قواعد إعادة الكتابة بشكلٍ متسقٍ في كل مرة قبل استخدامها بواسطة قاعدة mutate ؛ v ₂ ، v ₃ ، ... هي أسماء متغيرات مُولَّدة حاسوبيًا لهذا الغرض. في كل سطر، تُظلَّل المعادلة المختارة من G باللون الأحمر. في كل مرة تُطبَّق فيها قاعدة mutate ، تُشار إلى قاعدة إعادة الكتابة المختارة ( 1 أو 2 ) بين قوسين. من السطر الأخير، يُمكن الحصول على استبدال التوحيد S = { y ↦ nil , x ↦ a . nil } . في الواقع، app ( x , app ( y , x )) { y ↦ nil , x ↦ a . { } = app ( a . nil , app ( nil , a . nil )) ≡ app ( 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 }؛ لم يتم عرضه هنا. لا يوجد مسار آخر يؤدي إلى النجاح.

إذا كان R نظامًا لإعادة كتابة الحدود المتقاربة لـ E ، فإن أحد الأساليب البديلة للقسم السابق يتمثل في التطبيق المتتالي لـ " خطوات التضييق "؛ وهذا سيؤدي في النهاية إلى حصر جميع حلول المعادلة المعطاة. تتكون خطوة التضييق (انظر الصورة) من

• اختيار حد فرعي غير متغير من الحد الحالي،
• توحيدها نحويًا مع الجانب الأيسر من قاعدة من R ، و
• استبدال الجانب الأيمن من القاعدة المُطبقة في المصطلح المُطبق.

بصورة رسمية، إذا كانت l → r نسخة مُعاد تسميتها من قاعدة إعادة كتابة من R ، ولا تشترك في أي متغيرات مع الحد s ، وكان الحد الفرعي s | _p ليس متغيرًا ويمكن توحيده مع l عبر mgu σ ، فإنه يمكن تضييق s إلى الحد t = sσ [ rσ ] _p ، أي إلى الحد sσ ، مع استبدال الحد الفرعي عند p بـ rσ . يُشار عادةً إلى حالة إمكانية تضييق s إلى t بالرمز s ↝ t . وبشكل بديهي، يمكن اعتبار سلسلة خطوات التضييق t ₁ ↝ t ₂ ↝ ... ↝ t _n بمثابة سلسلة من خطوات إعادة الكتابة t ₁ → t ₂ → ... → t _n ، ولكن مع زيادة عدد مرات ظهور الحد الأولي t ₁ ، حسب الحاجة لجعل كل قاعدة من القواعد المستخدمة قابلة للتطبيق.

يتوافق حساب التعديل البارامتري المذكور أعلاه مع تسلسل التضييق التالي ("↓" يشير إلى التجسيد هنا):

يمكن توحيد المصطلح الأخير، v ₂ . v ₂ . nil، نحويًا مع المصطلح الأصلي الموجود على الجانب الأيمن a . a . nil .

تضمن اللمة التضييقية ^{[ 38 ]} أنه كلما أمكن إعادة كتابة مثال للمصطلح s إلى مصطلح t بواسطة نظام إعادة كتابة المصطلحات المتقارب، فإنه يمكن تضييق s و t وإعادة كتابتهما إلى مصطلح s ′ و t ′ على التوالي، بحيث يكون t ′ مثالًا على s ′ .

بصورة رسمية: عندما يتحقق sσ → ∗ t لبعض الاستبدال σ، فإنه توجد حدود s ′ , t ′ بحيث يكون s ↝ ∗ s ′ و t → ∗ t ′ و s ′ τ = t ′ لبعض الاستبدال τ.