موضوع مقاله: همان‌سازی (علوم رایانه) | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # همان‌سازی (علوم رایانه) | مقدمه: بر اساس آنکه کدام عبارات (که ترم نامیده می‌شوند) اجازه رخداد در مجموعه معادلات را دارد (که مسئله همان‌سازی نام دارد)، و نیز بر اساس آنکه کدام عبارات‌ها معادل درنظر گرفته می‌شوند، چارچوب‌های همان‌سازی از هم متمایز می‌شوند. | ## بخش 1: همان‌سازی (علوم رایانه) | اگر متغیرهای سطح بالا، یعنی متغیرهایی که نمایش‌دهنده توابع هستند، امکان وجود در یک عبارت را داشته باشد، به این فرایند همان‌سازی سطح بالا می‌گویند، در غیر این صورت به آن همان‌سازی سطح اول می‌گویند. اگر به وجود راه‌حلی برای همان‌سازی لیترالی هر دو طرف هر معادله نیاز باشد، به این فرایند نحوی یا همان‌سازی آزاد می‌گویند، در غیر این صورت به آن معنایی، همان‌سازی معادله‌ای، یا همان‌سازی E یا همان‌سازی بر پایه نظریه می‌گویند. راه‌حل‌های مسئله همان‌سازی توسط «جایگزینی» نشان داده می‌شوند، که «جایگزینی» یک نگاشت است که یک مقدار نمادین را به هر متغیر در عبارت‌های مسئله انتساب می‌دهد. یک الگوریتم همان‌سازی باید برای یک مسئله معین یک مجموعه جایگزینی «کامل و کمینه» محاسبه کند، یعنی این مجموعه همه جواب‌ها را پوشش دهد، و نیز شامل هیچ عضو زایدی هم نیست. بر اساس چارچوب مسئله، یک «مجموعه جایگزینی کامل و کمینه» می‌تواند تعداد اعضایش حداکثر یک، حداکثر تعداد متناهی، یا احتمالاً تعداد بی‌نهایتی عضو داشته باشد، یا ممکن است اصلاً عضوی نداشته باشد. برای همان‌سازی نحوی سطح اول، مارتلی و مانتناری یک الگوریتم ارائه دادند که قابل حل نبودن را گزارش کند، یا در غیر اینصورت یک مجموعه جایگزینی منفرد کمینه و کامل را محاسبه می‌کند، که شامل عمومی‌ترین همان‌ساز است. مسئله همان‌سازی سطح اول نحوی { y = cons(2,y) } در مجموعه ترم‌های متناهی هیچ راه‌حلی ندارد. مسئله همان‌سازی سطح اول معنایی { a⋅x = x⋅a } دارای جایگزینی با فرم { x ↦ a⋅...⋅a } است، که یک راه‌حل در نیم-گروه است، یعنی اگر (.) شرکت‌پذیر درنظرگرفته شود، مسئله مشابهی در گروه آبلی دیده می‌شود، که در آن (.) جابه‌جایی‌پذیر موقعی جابه‌جایی‌پذیر است، که هر جایگزینی اصلاً یک راه‌حل نباشد. مجموعه منفرد { a = y(x) } یک مسئله همان‌سازی سطح دوم نحوی است، زیرا y یک متغیر تابعی است. | ## بخش 2: همان‌سازی (علوم رایانه) | یکسان‌سازی سطح‌اول نحوی در برنامه‌نویسی منطقی، و نیز پیاده‌سازی سامانه نوع زبان برنامه‌نویسی استفاده می‌شود، مخصوصاً در الگوریتم‌های استنتاج نوع مبتنی بر هیندلی-میلنر از آن استفاده می‌شود. از همان‌سازی نحوی در حل‌کننده‌های مسئله SMT، الگوریتم‌های بازنویسی ترم، و تحلیل پروتکل رمزنگاری استفاده می‌شود. از همان‌سازی سطح بالاتر در کمک اثبات‌گر استفاده می‌شود، مثلاً در ایزابل، و توِلف از آن استفاده می‌شود، و حالت‌های محدودتر همان‌سازی سطح بالا (همان‌سازی الگوی سطح بالا) در بعضی از پیاده‌سازی‌های زبان برنامه‌نویسی، مثل لمبداپرولوگ، استفاده شده‌است، به دلیل آنکه الگوهای سطح بالاتر قابلیت بیان بالاتری دارند، هنوز فرایند همان‌سازی مربوط به آن‌ها، ویژگی‌های نظری‌شان به همان‌سازی سطح اول نزدیک است. در منطق ریاضی، مخصوصاً آنچه در علم کامپیوتر به کار می‌رود، اتحاد رابطه یا جمله نوعی الحاق (در معنی شبکه)، با توجه به یک نوع تخصصی، می‌باشد. به معنای دیگر، ما یک preorder را روی یک سری از روابط در نظر می‌گیریم، مثلاً t* ≤ t یعنی اینکه t* از t گرفته شده، به وسیلهٔ جانشانی برخی رابطه(ها) برای یک یا تعداد بیشتری از متغیرهای آزاد در t. اتحاد u از s و t، در صورت وجود، یک رابطه است که برای هردوی t و s یک مثال جانشانی به‌شمار می‌رود. اگر هر مثال جانشانی از s و t یک مثال برای u هم باشد، u اتحاد کمین نامیده می‌شود. برای مثال، در مورد چندجمله‌ای‌ها، و می‌توانند به صورت متحد شوند، اگر X را و Y را بگیریم. یکسان‌سازی در برنامه‌نویسی منطقی و تئوری نوع مفهوم یکسان‌سازی یکی از ایده‌های مهم در ورای برنامه‌نویسی منطقی است، که با زبان Prolog به بهترین نحو شناخته شده‌است. | ## بخش 3: همان‌سازی (علوم رایانه) | این برنامه مکانیزم محصور ومنسجم کردن محتویات متغیرها را نشان می‌دهد و می‌تواند به صورت نوعی از گمارش «یک زمانی» به نمایش در آید. در پرولوگ، این عملکرد به وسیلهٔ نماد تساوی = مشخص می‌شود، اما هنگام معرفی متغیرها نیز انجام می‌شود (قسمت زیر را ببینید). هم چنین در زبان‌های دیگر با استفاده از نماد تساوی =، استفاده می‌شود، اما هم چنین در رابطه با خیلی از عملگرها از جمله+، *، /. در پرولوگ متغیری که معرفی نشده‌است-یعنی هیچ متحدکنندهٔ قبلی روی آن کاری انجام نداده‌است-می‌تواند با یک جزء، یک جمله، یا متغیر معرفی نشدهٔ دیگر متحد و یکسان شود، بنابراین به شیوهٔ کارآمدی، نام مستعار آن می‌شود. در بسیاری از گویش‌های نوین پرولوگ و در منطق نوع اول، یک متغیر نمی‌تواند با جمله‌ای یکسان شود که آن جمله شامل آن متغیر است؛ این مورد به اصطلاح occurs check می‌باشد. در تئوری نوع، بیانیه‌های آنالوگ هر نوع متغیر با هر نوع بیان یکسان می‌شود، و به عنوان بیان معرفی می‌شود. دو نوع ساختار تنها زمانی یکسان می‌شوند که آن‌ها کاربردهای یک نوع سازنده باشند و تمام انواع مؤلفه‌هایشان به‌طور بازگشتی (متقابلاً) یکسان شود. توجه داشته باشید که در واژگان منطق نوع اول، یک اتم یا یک جزء، گزاره ومفهوم پایه است و به‌طور مشابه با یک جملهٔ پرولوگ یکسان می‌شود. یکسان‌سازی نوع بالاتر یکی از مؤثرترین تئوری‌های حذف این است که حذفیات، که مقدار آن‌ها با استفاده از یکسان‌سازی نوع بالاتر (HOU) تعیین شده‌است، توسط متغیرهای مستقل نمایش داده می‌شوند. | ## جمع‌بندی | برای مثال، نمایش معنایی جان شبیه مری است و پیتر هم چنین، این گونه است: (j; m)R(p) و مقدار R (نمایش معنایی حذفیات) توسط معادلهٔ شبیه به (j; m) = R(j) تعیین می‌شود.