ضد اتحاد
ضد اتحاد[ویرایش]
ضد اتحاد فرآیندی است برای ایجاد یک تعمیم مشترک برای دو عبارت نمادین داده شده .همانطور که در اتحاد، بسته به اینکه کدام عبارات (که اصطلاحات نیز نامیده می شوند) مجاز هستند و کدام عبارات برابر در نظر گرفته می شوند به چندین چارچوب متمایز می شوند. اگر متغیرهایی که توابع را نشان می دهند در یک عبارت مجاز باشند، این فرآیند "ضد اتحاد مرتبه بالاتر" و در غیر این صورت "ضد اتحاد مرتبه اول" نامیده می شود. اگر به تعمیم نیاز باشد که یک نمونه به معنای واقعی کلمه برابر با هر عبارت ورودی باشد، این فرآیند «ضد اتحاد نحوی»، در غیر این صورت «ضد اتحاد الکترونیکی» یا «نظریه مدول ضد اتحاد» نامیده می‌شود.
یک الگوریتم ضد اتحاد باید برای عبارات داده شده یک مجموعه تعمیم کامل و حداقل را محاسبه کند، یعنی مجموعه ای که تمام تعمیم ها را پوشش می دهد و به ترتیب شامل هیچ عضو اضافی نمی شود. بسته به چارچوب، یک مجموعه تعمیم کامل و حداقل ممکن است یک، بینهایت زیاد، یا احتمالاً بی نهایت عضو داشته باشد، یا اصلاً وجود نداشته باشد؛[۱] یک مجموعه تعمیم کامل و حداقل نمی تواند خالی باشد، زیرا در هر صورت یک تعمیم بی اهمیت وجود دارد. گوردون پلوتکین[۲][۳] برای ضد اتحاد نحوی مرتبه اول، الگوریتمی ارائه کرد که یک مجموعه تعمیم کامل و حداقلی را محاسبه می‌کند که شامل به اصطلاح "کمترین تعمیم عمومی" (lgg) است.
ضد اتحاد نباید با عدم اتحاد اشتباه گرفته شود. دومی به معنای فرآیند حل سیستم‌های نامعادله است، یعنی یافتن مقادیری برای متغیرها به گونه‌ای که همه نامعادله‌های داده شده برآورده شوند.[۴] این کار با یافتن تعمیم ها کاملاً متفاوت است.
پیش نیازها[ویرایش]
به طور رسمی، یک رویکرد ضد اتحاد پیش‌فرض می‌گیرد.
- مجموعه بی نهایت V از متغیرها. برای ضد اتحاد مرتبه بالاتر، انتخاب V disjoint از مجموعه متغیرهای محدود لامبدا مناسب است.
- T مجموعه ای از اصطلاحات است به گونه ای که V ⊆ T. برای ضد اتحاد مرتبه اول و بالاتر، T معمولاً به ترتیب مجموعه ای از اصطلاحات مرتبه اول (اصطلاحات ساخته شده از نمادهای متغیر و تابع) و اصطلاحات لامبدا (اصطلاحات حاوی مقداری بالاتر است. متغیرهای مرتبه) است.
- یک رابطه هم ارزی ≡ در T، که نشان می‌دهد کدام عبارت برابر در نظر گرفته می‌شود. برای ضد اتحاد مرتبه بالاتر، معمولا t ≡ u اگر t و u معادل آلفا باشند. برای مرتبه اول ضد اتحاد، ≡ دانش پس‌زمینه در مورد نمادهای تابع خاص را منعکس می‌کند. برای مثال، اگر ⊕ جابجایی در نظر گرفته شود، t ≡ u است اگر u نتیجه t توسط مبادله آرگومان های ⊕ در برخی (احتمالاً همه) رخدادها باشد . اگر اصلاً دانش پیشینه ای وجود نداشته باشد، آنگاه فقط از لحاظ لغوی یا نحوی، اصطلاحات یکسان برابر در نظر گرفته می شوند.
منابع[ویرایش]
- ↑ مجموعه‌های تعمیم کامل همیشه وجود دارند، اما ممکن است یک مجموعه تعمیم کامل غیر حداقلی باشد.
- ↑ Plotkin, Gordon D .(1970). Meltzer , B; Michie, D (eds.). "A Note on Inductive Generalization". Machine Intelligence. 5: 153-163
- ↑ Plotkin, Gordon D .(1970). Meltzer , B; Michie, D (eds.). "A Further Note on Inductive Generalication" . Machine Inteligence 6: 101-124
- ↑ کامن رفرد در سال 1986 به حل نامعادله به عنوان «ضد اتحاد» اشاره کرد که امروزه کاملاً غیرعادی شده است. Comon ، Hubert (1986). "کاملیت کافی، سیستم های بازنویسی اصطلاحات و "ضد اتحاد"". Proc. هشتمین کنفرانس بین المللی کسر خودکار. LNCS. جلد 230. اسپرینگر. صص 128-140.
This article "Anti-unification" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Anti-unification. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
