چرا نوشتن نرم افزار صحیح سخت است؟

خیلی خوشحال شدم که بار دیگر در Curry On صحبت کردم. سال گذشته، به دنبال کارمان با Quasar، من در مورد Continuations vs. Monads صحبت کردم. امسال درباره نتایج پیچیدگی محاسباتی در تأیید نرم‌افزار سخنرانی کردم، موضوعی که در حین مشخص کردن و تأیید رسمی نسخه اصلاح‌شده آینده Galaxy ما به آن علاقه مند شدم.

آنچه در ادامه می‌آید، نسخه‌ای مبسوط از گفتار (جاسازی‌شده در بالا)، حاوی برخی شواهد و نتایج اضافی است که من وقت نداشتم آن‌ها را به همراه پاورقی تکمیل کنم، برای کسانی که مایل به مطالعه بیشتر موضوعات هستند. زمان مطالعه: 45 دقیقه

در این مقاله سعی می کنیم رابطه بین برنامه ها و درستی و به ویژه اینکه چرا نوشتن برنامه های صحیح سخت است را درک کنیم. ما نتایج حاصل از تئوری محاسبات و نظریه پیچیدگی را بررسی خواهیم کرد و خواهیم دید که برنامه ها و درک کامل - که برای صحت لازم است - اساسا در تضاد هستند. سهم اصلی این متن، جمع آوری برخی از نتایج (و همچنین برخی ارجاعات) مربوط به دشواری اساسی تولید نرم افزار صحیح است.

انگیزه من عبارات مختلفی بود که به صورت آنلاین پیدا کردم (مانند این، اگرچه تنها موردی نیست) که ادعا می کردند صحت نرم افزار با ابزارهای مناسب آسان است. در حالی که برخی از ابزارها ممکن است (و انجام دهند) مطمئنا به اطمینان از صحیح بودن برنامه ها کمک می کنند، درستی هزینه زیادی دارد. هزینه صحت - مانند هزینه انرژی کاهش آنتروپی - نتیجه "قوانین طبیعی" محاسبات است که نمی توان از آن اجتناب کرد.

داستان CS نظری حدود صد سال پیش آغاز شد. با موفقیت فزاینده منطق ریاضی، ریاضیدان دیوید هیلبرت برنامه ای را برای رسمی کردن تمام ریاضیات تنظیم کرد. او می خواست فرمالیسم را سازگار و کامل ثابت کند، و یک روش تصمیم گیری، الگوریتمی برای تعیین صدق هر عبارت رسمی پیدا کند:

هیلبرت معتقد بود که هر چیزی را که بتوان به طور رسمی استدلال کرد نیز می‌تواند کاملا درک شود، و منظور من از آن همه ویژگی‌های آن اثبات شده است. دیدگاه قرن نوزدهم در مورد حدود دانش با قاعده "ignoramus et ignorabimus" به معنای "ما نمی دانیم و نخواهیم دانست" بیان شد. هیلبرت برای بازنشستگی خود در سال 1930 یک سخنرانی - "Naturerkennen und Logik" (منطق و درک طبیعت) - در کونیگزبرگ برای انجمن دانشمندان و پزشکان آلمانی ایراد کرد که این دیدگاه را به چالش کشید. او گفت:

برای ریاضی دان هیچ نابیموسی وجود ندارد، و به نظر من، اصلا برای علوم طبیعی نیز وجود ندارد. ... دلیل واقعی اینکه چرا [هیچ کس] موفق به یافتن یک مشکل غیرقابل حل نشده است، به نظر من این است که هیچ مشکل حل نشدنی وجود ندارد. عقیده ما برخلاف نادان نادان احمق می گوید: باید بدانیم، باید بدانیم! 1

آن کلمات - Wir müssen wissen. Wir werden wissen – بر روی سنگ قبر او حک شده است.

بی‌آنکه هیلبرت در آن زمان بداند، برنامه او یک روز پیش از آن، زمانی که کورت گودل به طور آزمایشی اولین نتیجه ناقص بودن خود را اعلام کرد، حذف شد.

قضایای ناتمامی گودل، دو رکن اول برنامه هیلبرت را از بین برد (برخی می گویند سومین آن را نیز متوجه نشده بود 3)، و در سال 1936، چرچ و تورینگ سومین مسئله تصمیم گیری را با اثبات آنچه امروزه به عنوان قضیه توقف شناخته می شود، شکستند.

قضیه توقف - اولین قضیه CS - در مقالات 4 آلونزو چرچ و 5 مقاله آلن تورینگ در سال 1936 به اثبات رسید. بیان می‌کند که نمی‌تواند الگوریتمی وجود داشته باشد که تصمیم‌گیری کند که آیا برنامه‌ای پایان می‌یابد یا خیر. برهان (که در اینجا به صورت کوتاه آورده شده است) مبتنی بر ایده مورب سازی یا ارجاع به خود است، همان ایده ای که گودل در اثبات ناقص بودن خود از آن استفاده کرده بود.

اگر $G$ را به خودش پاس کنیم ($G(G)$) تناقضی بین کاری که $G$ انجام می دهد و آنچه $H$ می گوید که $G$ انجام می دهد دریافت می کنیم.

جالب است بدانید که قضیه توقف بلافاصله نسخه ای از اولین قضیه ناقص بودن گودل را به دست می دهد. برهان به سادگی می‌گوید 6: فرض کنید برای هر گزاره درست یک دلیل منطقی در برخی از نظریه‌های منطقی وجود داشته باشد (در اصل مجموعه‌ای از بدیهیات). بنابراین، با توجه به یک برنامه، با شروع از آن بدیهیات، می‌توانیم همه قضایا را یک به یک با استفاده از استنتاج منطقی برشماریم. از آنجا که تعداد همه گزاره ها، چه رسد به همه قضایا، قابل شمارش است، و چون هر گزاره یا برهانی دارد یا نفی آن، در نهایت برهان یکی یا دیگری را می یابیم.

بنابراین، با توجه به یک برنامه، می‌توانیم شروع به شمارش همه قضایا کنیم تا زمانی که قضیه‌ای را پیدا کنیم که نشان دهد برنامه خاتمه می‌یابد، یا قضیه‌ای که بگوید پایان نمی‌یابد، در نتیجه قضیه توقف را نقض می‌کند.

با این حال، قضیه توقف برخی پیامدهای فوری دیگر دارد که مستقیما آن را با مشکل تأیید نرم افزار، که تمرکز اصلی ما است، مرتبط می کند. اولین مورد، نتیجه ساده در مورد دسترسی است.

برنامه R وجود ندارد، وقتی به برنامه M داده می شود، مجموعه ای از حالت های اولیه I و پیکربندی حالت S، تعیین می کند که آیا M وقتی در یکی از حالت های I شروع می شود به S می رسد یا خیر.

اثبات یک کاهش ساده از توقف است: اگر چنین الگوریتمی وجود داشت، می‌توانیم از آن بپرسیم که آیا، با شروع با ورودی x، به حالت توقف می‌رسد یا خیر، و بنابراین مشکل توقف را حل کنیم.

نتیجه جالب‌تر قضیه رایس است. برنامه ها می توانند آنچه را که به عنوان توابع جزئی شناخته می شوند محاسبه کنند. اگر هنگام دادن ورودی متوقف شوند، خروجی نوشته شده روی نوار را به ورودی اولیه نگاشت می‌کنیم. اگر آنها هرگز برای یک ورودی معین متوقف نشوند، آن ورودی را بدون نقشه در نظر می گیریم. قضیه رایس این را بیان می کند:

برای هر ویژگی غیر پیش پا افتاده توابع جزئی، هیچ الگوریتمی نمی تواند تصمیم بگیرد که آیا یک برنامه (TM) M تابع جزئی را با آن ویژگی محاسبه می کند یا خیر.

به عنوان مثال، هیچ الگوریتمی برای تعیین اینکه آیا خروجی یک برنامه همیشه مجذور ورودی آن است یا خیر وجود ندارد. این قضیه نیز با کاهش از Halting ثابت شده است.

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

در نسخه پویا تابع زیر را روی اعداد طبیعی تعریف می کنیم:

$f(n)$ = حداکثر تعداد مراحلی که یک TM در حال توقف با حالت های کنترل $n$ ممکن است قبل از توقف انجام دهد.

حالت های کنترل ماشین تورینگ برنامه آن را تشکیل می دهند، بنابراین $n$ اندازه برنامه است. این تابع به خوبی تعریف شده است زیرا تعداد محدودی TM با اندازه $n$ وجود دارد. زیر مجموعه ای از آنها که به پایان می رسد نیز محدود است، بنابراین حداکثر تعداد حالت وجود دارد.

قضیه می گوید $f$ غیر قابل محاسبه است. فرض کنید که $f$ قابل محاسبه بود. اگر چنین است، این نقض قضیه توقف است. با توجه به TM، تعداد حالت‌های کنترل را می‌شماریم، $n$، $f(n)$ را محاسبه می‌کنیم (که با فرض محاسباتی $f$ ممکن است)، و سپس ماشین را برای $f(n)$ مراحل اجرا می‌کنیم. اگر تا آن زمان خاتمه نیابد - پس مطمئنا هرگز نباید خاتمه یابد (با تعریف $f$)، و ما یک رویه قابل تصمیم برای مسئله توقف داریم که در تضاد با قضیه توقف است.

نه تنها $f$ یک تابع غیر قابل محاسبه است، بلکه هر تابعی که بزرگتر از $f$ برای همه $n$ شناخته شده است نیز غیر قابل محاسبه است، زیرا اگر ما چنین تابعی را بدانیم، همان رویه مجددا تصمیمی برای توقف می دهد.

همین استدلال در مورد دیدگاه ایستا از برنامه ها نیز صدق می کند. برای درک این نتیجه، باید بدانیم که با توجه به یک نظریه منطقی با مجموعه‌ای از بدیهیات محدود، یک الگوریتم می‌تواند قواعد استنتاج را یکی یکی با شروع بدیهیات اعمال کند و شروع به شمارش تمام قضایا (گزاره‌های قابل اثبات) یک به یک کند.

$g(n)$ = حداکثر اندازه حداقل مدرک خاتمه یک TM توقف با اندازه $n$

برای هر TM پایان‌دهنده با اندازه $n$، کوتاه‌ترین اثبات خاتمه را انتخاب می‌کنیم (حداقل باید یک اثبات وجود داشته باشد، زیرا یک رد پایانی چنین اثباتی است). سپس ماکزیمم را در بین تمام TM های پایانی با اندازه $n$ (که تعداد محدودی وجود دارد) می گیریم.

همانند $f$، $g$ نیز باید غیر قابل محاسبه باشد. اگر $g(n)$ قابل محاسبه بود، سپس یک TM با اندازه $n$ داده می‌شد، ماشین را با برخی بدیهیات توصیف می‌کردیم و سپس همه قضایا را با برهان‌هایی به اندازه $\leq g(n)$ می‌شماریم - این عدد محدودی است - و اگر هیچ دلیلی پیدا نشد، می‌دانیم که ماشین هرگز خاتمه نمی‌یابد. باز هم در تضاد با قضیه توقف.

این نتیجه قضیه توقف، واقعیت زیر را نشان می‌دهد: تابعی که اندازه یک برنامه را به دشواری اثبات خاتمه آن گره می‌زند، صرف نظر از اینکه به یک تکنیک اثبات پویا علاقه‌مندیم یا ثابت، از همه توابع قابل محاسبه بزرگ‌تر است (به طور دقیق‌تر: هیچ تابع قابل محاسبه‌ای وجود ندارد که بتوان آن را بزرگ‌تر از مقدار تابع $$n دانست).

در حالی که نمی‌توانیم $f$ را برای همه $n$ محاسبه کنیم، می‌توانیم آن را محاسبه کنیم، یا کرانهای پایین‌تر برای آن را برای برخی مقادیر محاسبه کنیم. برای $n = 6$ (و یک الفبای 2 علامتی)، $> 7.4 \times 10^{36534}$ است.

سوال دیگری که ممکن است بپرسیم این است: می‌دانیم که نمی‌توانیم الگوریتمی برای تصمیم‌گیری در مورد توقف برنامه‌های دلخواه پیدا کنیم، اما آیا برنامه‌های خاصی وجود دارند که نمی‌توانیم بدانیم که آیا متوقف می‌شوند یا نه (حتی اگر رویه تصمیم‌گیری را به‌طور خاص برای آن‌ها تنظیم کنیم)؟

قضیه ناتمامی دوم گودل چنین برنامه ای را به دست می دهد. این قضیه بیان می کند که غیرممکن است یک سیستم منطقی کامل بودن خود را اثبات کند. سیستم منطقی که به طور گسترده به عنوان پایه ریاضیات پذیرفته شده است ZFC نامیده می شود - نظریه مجموعه های Zermello-Fraenkel با اصل انتخاب. در آن سیستم می‌توانیم اکثر قضایای ریاضی را که به آنها اهمیت می‌دهیم ثابت کنیم (به استثنای استثنائات بسیار قابل توجه و بسیار خاص). بنابراین می‌توانیم برنامه‌ای بسازیم که کارهای زیر را انجام دهد: با شروع از بدیهیات ZFC، همه قضایا را برشمارید و وقتی به یک تناقض رسیدید متوقف شوید (مثلا 1 = 2).

اگر ZFC ناسازگار باشد، این برنامه متوقف می شود. ما ZFC را ثابت فرض می‌کنیم، و بنابراین انتظار داریم که برنامه هرگز متوقف نشود، اما نمی‌توانیم آن را با قضیه دوم ناقص بودن ثابت کنیم.

در ماه می گذشته، آدام یدیدیا و اسکات آرونسون برنامه‌ای را منتشر کردند که به یک ماشین تورینگ کامپایل می‌شود که بر اساس آن اصل (یا چیزی معادل آن) کار می‌کند. نتیجه به سرعت توسط Stefan O'Rear بهبود یافت، که یک ماشین تورینگ را با حالت های کنترلی 1919 ایجاد کرد که نمی توان پایان آن را ثابت کرد (یعنی "مستقل از ZFC" است). این دستگاه آنقدر کوچک است که به راحتی در یک چالش 4K قرار می گیرد. با یک برنامه پایتون با 100-200 خط قابل مقایسه است.

این بدان معنی است که برنامه های کوچکی وجود دارند - فقط چند صد خط یا کمتر - که رفتار آنها را نمی توان از نظر ریاضی تعیین کرد. نه به این دلیل که تجزیه و تحلیل خیلی بزرگ یا غیرقابل حل است، بلکه به این دلیل که ریاضیات به اندازه کافی قدرتمند نیست که بتواند رفتار این برنامه را حتی در تئوری اثبات کند.

در هر صورت، با کار گودل، چرچ و تورینگ، برنامه هیلبرت - حداقل همانطور که در ابتدا برنامه ریزی شده بود - 80 سال پیش توسط اشیاء ساده، فشرده و ریاضی که می توان به طور رسمی درباره آنها استدلال کرد، اما به طور کامل درک نشد، پایان یافت: برنامه های کامپیوتری.

یک سوال اساسی وجود دارد که باید پرسیده شود. کل فرض قضیه توقف بر این ایده استوار است که تابعی که به مراحل محاسباتی نامتناهی نیاز دارد غیرقابل محاسبه است. این کاملا واضح نیست. از این گذشته، ریاضیات اغلب اشیاء نامتناهی را کنترل می کند 10 . در حالی که چرچ این نکته را نادیده گرفت (شاید معتقد بود که واضح است - او آن را "مفهوم شهودی مبهم" نامید) تورینگ، که مقاله اش بسیار فلسفی تر از مقاله چرچ بود، توضیح داد که یک الگوریتم چیزی است که توسط یک شخص یا یک ماشین انجام می شود.

در سال 1947، او به انجمن ریاضی لندن سخنرانی کرد. او گفت: چند سال پیش،

من در حال تحقیق در مورد چیزی بودم که اکنون می توان آن را به عنوان بررسی امکانات نظری و محدودیت های ماشین های محاسباتی دیجیتال توصیف کرد.

در این استدلال های نظری ضروری بود که حافظه باید بی نهایت باشد... ماشین هایی مانند ACE ممکن است به عنوان نسخه های عملی همین نوع ماشین در نظر گرفته شوند.

تورینگ دستاورد موفقیت آمیز خود در سال 1936 را اینگونه دید. در حالی که رسمی‌سازی ریاضی ممکن است برای بی‌نهایت جذابیت داشته باشد، برای تورینگ واضح بود که مفهوم محاسبه به برخی فرآیندهای فیزیکی گره خورده است. اگر اینطور نبود، هیچ توجیهی برای مرکزیت مسئله توقف و استفاده از آن به عنوان راه حلی منفی برای مشکل Entscheidungs ​​Hilbert وجود نداشت. الگوریتم چیزی است که در دنیای فیزیکی انجام می شود.

تز چرچ-تورینگ، همانطور که امروز ارائه می شود، حدس می زند که هر محاسباتی که توسط هر فرآیند فیزیکی قابل تحقق انجام می شود، می تواند توسط مدل های محاسباتی جهانی که توسط چرچ و تورینگ توصیف شده است، محاسبه شود. به یک معنا، این بدان معنی است که همه چیز در جهان می تواند به عنوان یک برنامه کامپیوتری رسمی و شبیه سازی شود.

برنامه ها اساسا و اساسا با درک کامل، اثبات و صحت در تضاد هستند.

از آنجایی که ریاضیات - به عنوان یک رشته دانشگاهی، نه به عنوان یک ابزار - به آنچه در درون دایره کوچک است، و علوم کامپیوتر عمدتا به آنچه در خارج از آن است توجه دارد - و همانطور که خواهیم دید، حتی آن برنامه هایی که در این دایره درونی قرار دارند، بسیاری از آنها اصولا فقط قابل اثبات هستند، اما به طور عملی قابل اثبات نیستند - فکر می کنم واضح است که علوم کامپیوتری 12 است.

برای اهداف عملی، تفاوت بین ترتیب جبری و نمایی اغلب بسیار مهمتر از تفاوت بین محدود و نامتناهی است.

اینکه آیا راستی‌آزمایی - یعنی توقف و پیامدهای آن - قابل تصمیم‌گیری است یا نه، به‌طور کامل دشواری مشکل را نشان نمی‌دهد. از آنجایی که ماشین‌های تورینگ می‌توانند رفتار نامتناهی داشته باشند، مشکل تأیید آنها را می‌توان - به یک معنا - شبیه به مشکل مرتب‌سازی فهرستی با طول محدود یا نامحدود یا یافتن عنصر حداکثر در چنین فهرستی در نظر گرفت. هر دو به یک اندازه غیرممکن هستند، اما می دانیم که وقتی به حالت محدود محدود می شود، دشواری آنها بسیار متفاوت است.

این مشکل زمان و تلاش برای تورینگ آشکار بود. مکس نیومن که معلم تورینگ در کمبریج و همچنین رمز شکن در پارک بلچلی پارک بود، این مشکل را در رادیو بی‌بی‌سی در اولین پانل عمومی در مورد هوش مصنوعی در سال 1952 برای تورینگ مطرح کرد.

مکس نیومن: خیلی خوب است که بگوییم یک ماشین می تواند... ساخته شود تا این یا آن را انجام دهد، اما... در مورد زمان لازم برای انجام آن چیست؟ حل یک مشکل در دستگاه به معنای یافتن راهی برای انجام آن از الان تا ابد نیست، بلکه در یک زمان معقول…

تورینگ: به نظر من این عامل زمان تنها سوالی است که تمام مشکلات فنی واقعی را شامل می شود. 14

30 سال دیگر پس از مقاله اصلی تورینگ طول کشید تا مسئله دشواری الگوریتمی به درستی تعریف شود. نظریه پیچیدگی محاسباتی در سال 1965 در مقاله ای توسط ژوریس هارتمانیس و ریچارد استرنز متولد شد که اینگونه آغاز می شود:

تورینگ در مقاله مشهور خود، محاسبه‌پذیری دنباله‌ها (توابع) را با روش‌های مکانیکی بررسی کرد و نشان داد که مجموعه دنباله‌ها را می‌توان به دنباله‌های قابل محاسبه و غیرقابل محاسبه تقسیم کرد. با این حال، شخص متوجه می شود که محاسبه برخی از دنباله های قابل محاسبه بسیار آسان است در حالی که به نظر می رسد سایر دنباله های قابل محاسبه دارای پیچیدگی ذاتی هستند که محاسبه آنها را دشوار می کند. در این مقاله، ما طرحی از طبقه بندی دنباله ها را بر اساس میزان سختی محاسبه آنها بررسی می کنیم. 15

هارتمانیس در سخنرانی خود در جایزه تورینگ در سال 1993 گفت که پیچیدگی را به عنوان قانون طبیعت، شبیه به قوانین فیزیک می بیند.

من فیزیک را به خاطر قوانین بسیار دقیق آن که بر رفتار دنیای فیزیکی حاکم است و توضیح می دهد، دوست داشتم. در کار شانون، برای اولین بار، من قوانین کمی دقیقی را دیدم که بر رفتار موجودیت انتزاعی اطلاعات حاکم بود... این سؤال را مطرح کرد که آیا می‌توان قوانین کمی دقیقی وجود داشت که بر فرآیند انتزاعی محاسبات حاکم باشد، که... مستقیما توسط قوانین فیزیکی محدود نشده بود. آیا قوانین کمی وجود دارد که تعیین کند برای هر مسئله چقدر تلاش محاسباتی (کار) برای حل آن و نحوه اندازه گیری و تعیین آن لازم است؟ 16

این زمان خوبی برای بازبینی تز چرچ-تورینگ است، که دوباره، همانطور که امروزه فهمیده می‌شود، می‌گوید هر محاسباتی که توسط هر سیستم فیزیکی در جهان قابل انجام است، می‌تواند توسط هر یک از مدل‌های محاسباتی جهانی نیز انجام شود. مهم است که تأکید شود که هیچ نمونه متقابلی تا کنون یافت نشده است.

نسخه قوی تر این پایان نامه می گوید که ماشین تورینگ می تواند هر فرآیند فیزیکی را با هزینه محاسباتی چند جمله ای بیشتر شبیه سازی کند. این نسخه ممکن است با توجه به امکان رایانه‌های کوانتومی نادرست باشد، و اصلاحاتی در نحوه بیان آن وجود دارد، اما کلاس‌های پیچیدگی که مورد بحث قرار می‌دهیم به آن کلاس‌های پیچیدگی جالب مربوط نمی‌شوند، بنابراین مهم است که تاکید کنیم:

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

جای تعجب نیست که همین سوال ما در مورد دشواری دقیق مسئله توقف بود که به هارتمانیس و استرنز اجازه داد تا دشواری ذاتی برخی از مسائل را نشان دهند و آنچه را که اکنون به عنوان قضیه سلسله مراتب زمانی شناخته می شود، اثبات کنند، که می گوید مسائل محاسباتی یک سلسله مراتب دشواری مناسب را تشکیل می دهند.

مشکلی که در اینجا ارائه می‌دهم اغلب به عنوان «توقف محدود» شناخته می‌شود و موارد زیر را می‌پرسد: پیچیدگی تصمیم‌گیری در مورد اینکه آیا یک برنامه دلخواه M در ورودی x در n مرحله متوقف می‌شود چیست؟

با فرض اینکه بتوانیم برنامه را با سربار کم شبیه سازی کنیم، می توانیم آن را در $O(n)$ انجام دهیم، اما آیا می توانیم آن را سریعتر انجام دهیم؟ اثبات ما مبنی بر اینکه این غیرممکن است دقیقا همان اثبات قطری قضیه توقف را تقلید خواهد کرد (توجه می‌کنم که ارائه طرح اثبات من دقیق نیست زیرا هزینه‌های سربار شبیه‌سازی ماشین دیگری را در نظر نمی‌گیرد و با نتیجه سال 1972 استفان کوک که بر روی ماشین‌های RAM کار می‌کرد به جای ماشین‌های تورینگ) همخوانی دارد:

بیایید فرض کنیم می توانیم سریعتر به سوال پاسخ دهیم:

$H_n(M، x)$ := اگر $M$ در $x$ در $n$ مراحل متوقف شد، TRUE ELSE FALSE

$G(y)$ := اگر $H_n(y, y)$ = FALSE، TRUE ELSE $n$ بار حلقه بزنید و FALSE را برگردانید

همانطور که در اثبات قضیه توقف، اگر $G$ را به خودش ارسال کنیم ($G(G)$) بین کاری که $G$ انجام می‌دهد و آنچه $H$ می‌گوید که $G$ انجام می‌دهد، تناقض دریافت می‌کنیم، زیرا توجه می‌کنیم که $H_n$ نتیجه خود را در $n-2$ مراحل برمی‌گرداند، و $G$ سپس در یک مرحله دیگر، TRUE را برمی‌گرداند، و $n$ مراحل را در زیر خاتمه می‌دهد.

به زبان ساده، شما نمی توانید بدانید که یک برنامه چه کاری را سریعتر از اجرای آن انجام می دهد. توقف محدود $\theta(n)$ است.

اما آیا می توانیم از یک ورودی به ورودی دیگر تعمیم دهیم؟ آیا می‌توانیم روی برخی از ورودی‌ها سخت کار کنیم تا در سایر ورودی‌ها سریع عمل کنیم؟ اگر کار سخت روی تجزیه و تحلیل رفتار برنامه در برخی از ورودی‌ها می‌توانست برای برخی دیگر سود داشته باشد، تعداد ورودی‌ها به اندازه کافی زیاد است، $K$، به طوری که پاسخ دادن به سؤال توقف محدود در همه آنها کمتر از $K \cdot n$ قدم خواهد داشت. من نتوانستم آن مشکل را در ادبیات پیدا کنم، بنابراین آن را توقف کران استهلاک نامیدم، و می‌توانیم آن را دقیقا به این صورت بیان کنیم:

با توجه به اعداد طبیعی $n$، $K$، آیا ماشینی وجود دارد که برای همه TM ها $M$, $HA_{n,k}(M, x_1,…, x_k)$ تصمیم بگیرد که آیا $M$ در تمام $x_1…x_k$ در $n$ مراحل متوقف شود یا خیر و این کار را در $K \cdot n$ مراحل انجام دهد؟