پیش‌نویس:ضد اتحاد

ضد اتحاد فرآیندی است برای ایجاد یک تعمیم مشترک برای دو عبارت نمادین داده شده .همانطور که در اتحاد ، بسته به اینکه کدام عبارات (اصطلاحات) مجاز هستند و کدام عبارات برابر در نظر گرفته می شوند به چندین چارچوب متمایز می شوند. اگر متغیرهایی که توابع را نشان می دهند در یک عبارت مجاز باشند، این فرآیند "ضد اتحاد مرتبه بالاتر" و در غیر این صورت "ضد اتحاد مرتبه اول" نامیده می شود. اگر به تعمیم نیاز باشد آنگاه اگر نمونه دقیقا برابر با هر عبارت ورودی باشد، این فرآیند «ضد اتحاد نحوی»، در غیر این صورت «ضد اتحاد الکترونیکی» یا «نظریه مدول ضد اتحاد» نامیده می‌شود.

یک الگوریتم ضد اتحاد باید برای عبارات داده شده یک مجموعه تعمیم تمام و حداقلی را محاسبه کند، یعنی مجموعه ای که تمام تعمیم ها را پوشش می دهد و به ترتیب شامل هیچ عضو اضافی نمی شود. بسته به چارچوب، یک مجموعه تعمیم تمام و حداقلی ممکن است یک، تعدادی (متناهی) ، یا بی نهایت عضو داشته باشد و یا اصلاً وجود نداشته باشد؛ یک مجموعه تعمیم تمام و حداقلی نمی تواند تهی باشد، زیرا در هر صورت یک تعمیم بی اهمیت وجود دارد.گوردون پلوتکین برای ضد اتحاد نحوی مرتبه اول، الگوریتمی ارائه کرد که یک مجموعه تعمیم تمام و حداقلی را محاسبه می‌کند که شامل به اصطلاح "کمترین تعمیم عمومی" است.

ضد اتحاد نباید با عدم اتحاد اشتباه گرفته شود. دومی به معنای فرآیند حل سیستم های نامعادله است، یعنی یافتن مقادیری برای متغیرها به گونه ای که همه نامعادله های داده شده برآورده شوند. این کار با یافتن تعمیم ها کاملاً متفاوت است.

پیش نیازها

به طور رسمی، یک رویکرد ضد اتحاد مستلزم این است:

• مجموعه بی نهایت V از متغیرها. انتخاب V disjoint از مجموعه متغیرهای مقید به عبارت لامبدا برای ضد اتحاد مرتبه بالاتر مناسب است.
• مجموعه ای از اصطلاحات است به گونه ای که V ⊆ T. برای ضد اتحاد مرتبه اول و بالاتر، T معمولاً به ترتیب مجموعه ای از اصطلاحات مرتبه اول (اصطلاحات ساخته شده از نمادهای متغیر و تابع) و اصطلاحات لامبدا (اصطلاحات حاوی برخی از متغیرهای مرتبه بالاتر) است.
• یک رابطه هم ارزی $\equiv$ بر $T$ ، که نشان می‌دهد کدام عبارت برابر در نظر گرفته شود. برای ضد اتحاد مرتبه بالاتر $t\equiv u$ اگر $t$ و $u$ معادل آلفا هستند . برای مرتبه اول ضد اتحاد الکترونیکی، $\equiv$ منعکس کننده دانش پس زمینه در مورد عملکرد خاص نمادها است. به عنوان مثال، اگر $\oplus$ جابه جایی پذیر در نظر گرفته شود، $t\equiv u$ است اگر $u$ حاصل $t$ با مبادله آرگومان های $\oplus$ در برخی (احتمالاً همه) رخدادها باشد. اگر اصلاً دانش پیشینه ای(قبلی) وجود نداشته باشد، آنگاه فقط از لحاظ لغوی یا نحوی، اصطلاحات یکسان، برابر در نظر گرفته می شوند.

منابع

رده:یکسان‌سازی (رایانه) رده:منطق در علوم کامپیوتر رده:اثبات قضیه خودکار رده:برنامه‌سازی منطقی استنتاجی