یکسان سازی

wiki: کامپیوتر است. برای ایدهٔ جهانی یکسان سازی، globalization را ببینید.برای موارد دیگر،Unification (disambiguation) را ببینید.
تعریف یکسان سازی برای منطق نوع اول
یکسان سازی در برنامه نویسی منطقی و تئوری نوع
یکسان سازی نوع بالاتر
مثال هایی از یکسان سازی
هم چنین ببینید
یادداشت ها
مرجع ها
در منطق ریاضی، مخصوصاً آنچه در علم کامپیوتر به کار می رود، اتحاد رابطه یا جمله نوعی الحاق(در معنی شبکه)، با توجه به یک نوع تخصصی، می باشد. به معنای دیگر، ما یک preorder را روی یک سری از روابط در نظر می گیریم، مثلاً t* ≤ t یعنی اینکه t* از t گرفته شده، به وسیلهٔ جانشانی برخی رابطه (ها) برای یک یا تعداد بیشتری از متغیرهای آزاد در t. اتحاد u از s و t، در صورت وجود، یک رابطه است که برای هردوی t و s یک مثال جانشانی به شمار می رود. اگر هر مثال جانشانی از s و t یک مثال برای u هم باشد، u اتحاد کمین نامیده می شود.برای مثال، در مورد چندجمله ای ها، X 2 {\displaystyle X2} و Y 3 {\displaystyle Y3} می توانند به صورت Z 6 {\displaystyle Z6} متحد شوند، اگر X را Z 3 {\displaystyle Z3} و Y را Z 2 {\displaystyle Z2} بگیریم.
محتوا
بگذارید p و q جملاتی در منطق نوع اول باشند.UNIFY (p، q) = U where subst (U،p) = subst (U،q)هرجا subst(U،p) باشد یعنی نتیجهٔ به کارگیری U جانشانی روی جملهٔ p. بنابراین U متحدکنندهٔ p و q نامیده می شود. یکسان سازی نتیجهٔ به کارگیری از U برای هردوی p و q است.فرض کنید L مجموعه ایی از جملات باشد، برای مثال L = {p،q}. یک متحدکنندهٔ U، عمومی ترین متحدکننده نامیده می شود اگر برای تمام متحدکننده های U' از L، یک جایگزین s وجود داشته باشد کهsubst(U'،L) = subst(s،subst(U،L)).