محاسبهپذیری و تصمیمپذیری
نظریه محاسبهپذیری به مطالعه محدودیتهای اساسی حل مسئله الگوریتمی میپردازد و مرز بین مسائلی را که میتوان با یک رویه مؤثر حل کرد و آنهایی را که هیچ الگوریتمی نمیتواند تصمیم بگیرد، مشخص میکند.
Definition
نظریه محاسبهپذیری مطالعه این است که کدام توابع و مسائل تصمیمگیری توسط یک رویه مؤثر محاسبهپذیر هستند؛ یک مسئله تصمیمپذیر است اگر یک الگوریتم همیشه با پاسخ صحیح بله یا خیر متوقف شود، و تصمیمناپذیر است اگر چنین الگوریتمی وجود نداشته باشد.
Scope
این حوزه مدلهای رسمی محاسبات مؤثر مانند ماشینهای تورینگ، تز چرچ-تورینگ که این مدلها را با مفهوم شهودی الگوریتم یکسان میداند، وجود مسائل تصمیمناپذیر از جمله مسئله توقف، کاهشهایی که برای انتقال حلناپذیری بین مسائل استفاده میشوند، و ساختار درجات حلناپذیری که مسائل فراتر از محاسبهپذیر را طبقهبندی میکنند، پوشش میدهد.
Sub-topics
Core questions
- حلپذیر بودن یک مسئله توسط یک الگوریتم به چه معناست؟
- آیا مسائل خوشتعریفی وجود دارند که هیچ الگوریتمی هرگز نتواند آنها را حل کند؟
- چگونه میتوان از حلناپذیری یک مسئله برای اثبات حلناپذیری مسئلهای دیگر استفاده کرد؟
- مسائل حلناپذیر چگونه بر اساس دشواری نسبی خود طبقهبندی میشوند؟
Key theories
- مدل محاسبات تورینگ
- ماشین انتزاعی تورینگ مفهوم یک رویه مؤثر را رسمی کرد و برای اثبات حلناپذیری مسائل توقف و تصمیمگیری برای منطق مرتبه اول استفاده شد و محدودیتهای ذاتی محاسبات را تثبیت کرد.
- وجود مسائل تصمیمناپذیر
- با یک استدلال قطری، مسائلی وجود دارند، که معروفترین آنها مسئله توقف است، که هیچ الگوریتمی نمیتواند آنها را تصمیم بگیرد، بنابراین تصمیمناپذیری یک ویژگی ساختاری فراگیر است تا یک کنجکاوی.
- معادل بودن مدلهای محاسبات
- ماشینهای تورینگ، حساب لامبدا و توابع بازگشتی دقیقاً همان کلاس توابع محاسبهپذیر را تعریف میکنند، همگرایی که تز چرچ-تورینگ را تأیید میکند.
Clinical relevance
نتایج تصمیمناپذیری محدودیتهای سختی را بر آنچه ابزارهای نرمافزاری میتوانند تضمین کنند، اعمال میکند: هیچ الگوریتم کلی نمیتواند تصمیم بگیرد که آیا یک برنامه دلخواه متوقف میشود، صحیح است یا عاری از اشکالات خاص است، به همین دلیل ابزارهای تأیید به جای تحلیل خودکار کامل، به تقریب، زبانهای محدود و راهنمایی انسانی متکی هستند.
History
با الهام از مسئله تصمیم هیلبرت (Entscheidungsproblem)، چرچ و تورینگ به طور مستقل در سال ۱۹۳۶ نشان دادند که هیچ الگوریتمی نمیتواند تمام منطق مرتبه اول را تصمیم بگیرد، با مدل ماشین تورینگ و حساب لامبدای چرچ که معادل بودن آنها اثبات شد. پست و کلین در دهههای بعدی این نظریه را به مطالعه درجات حلناپذیری گسترش دادند.
Key figures
- Alan Turing
- Alonzo Church
- Kurt Gödel
- Emil Post
Related topics
Seminal works
- turing1937
- church1936
- sipser2013
Frequently asked questions
- تفاوت بین تصمیمپذیر و تصمیمناپذیر چیست؟
- یک مسئله تصمیمپذیر است اگر الگوریتمی وجود داشته باشد که همیشه متوقف شود و پاسخ صحیح بله یا خیر را برای هر ورودی ارائه دهد. اگر چنین الگوریتمی نتواند وجود داشته باشد، تصمیمناپذیر است، همانطور که برای مسئله توقف اثبات شده است؛ یک مسئله تصمیمناپذیر ممکن است همچنان قابل تشخیص باشد، به این معنی که یک الگوریتم میتواند نمونههای بله را تأیید کند اما ممکن است برای نمونههای خیر برای همیشه اجرا شود.
- آیا تصمیمناپذیری به این معنی است که این مسائل هرگز قابل حل نیستند؟
- این بدان معناست که هیچ الگوریتم واحدی هر نمونه را به درستی حل نمیکند. در عمل، ابزارها موارد محدود را مدیریت میکنند، پاسخهای تقریبی یا محافظهکارانه میدهند، یا بسیاری از نمونهها را حل میکنند در حالی که گاهی اوقات شکست میخورند یا درخواست کمک میکنند، بنابراین تصمیمناپذیری نحوه حمله به مسائل را شکل میدهد تا اینکه هرگونه پیشرفتی را ممنوع کند.