בעיית העצירה

בעיית העצירה היא בעיה מרכזית בתחום החישוביות, שהוא אחד מעמודי התווך של מדעי המחשב התאורטיים.

בעיית העצירה מנוסחת כבעיית ההכרעה הבאה: בהינתן תוכנית מחשב וקלט, האם התוכנית תסיים את פעולתה בשלב כלשהו עבור קלט זה.

אלן טיורינג הוכיח ב-1936 כי בעיית העצירה על מכונות טיורינג (מודל תאורטי של מחשב בעל זיכרון אינסופי) אינה כריעה, כלומר אין אלגוריתם שמכריע עבור כל תוכנית מחשב <math>Q</math> וקלט <math>X</math> האם התוכנית <math>Q</math> עוצרת כאשר מופעלת על <math>X</math> (בקיצור: האם <math>Q</math> עוצרת על <math>X</math>) או לא. חשוב להבחין שמבחינה לוגית, בהינתן תוכנית מסוימת וקלט עבורה, התשובה לשאלה "האם היא עוצרת?" מוגדרת היטב וחד משמעית.

לעומת זאת ניתן לבנות מכונת טיורינג שמקבלת כל תוכנית מחשב <math>Q</math> וקלט <math>X</math> כך שתוכנית המחשב עוצרת על קלט זה, ולא מקבלת אך אולי גם לא דוחה אם התוכנית אינה עוצרת על קלט זה, ולכן בעיית העצירה ניתנת למנייה רקורסיבית ושייכת לקבוצה <math>RE/R</math>.

== הוכחת אי-כריעות ==
ההוכחה לאי-כריעות בעיית העצירה נעשית בדרך השלילה: מראים כי מההנחה שניתן לפתור את בעיית העצירה מגיעים לסתירה - קיימת תוכנית שעבור קלט מסוים חייבת גם לעצור וגם לא לעצור לעולם.

:נניח שיש אלגוריתם <math>Halt(Q,X)</math> שמקבל אם <math>Q</math> עוצרת על <math>X</math> ודוחה אחרת, ונתבונן בתוכנית <math>A(Q)</math> הבאה המקבלת תוכנית <math>Q</math> כקלט:
::אם <math>Halt(Q,Q)</math>, הכנס ללולאה אינסופית.
::אחרת, עצור.
:נשים לב כי מעבירים כאן את <math>Q</math> פעמיים: הן בתור התוכנית שיש לבדוק והן בתור הקלט לתוכנית שעליו היא נבדקת. אין בעיה עקרונית בהעברת <math>Q</math> כקלט - ניתן לחשוב על כל קלט כרצף של תווים, ולכן גם תוכנית מחשב יכולה להיחשב לקלט.
:נשאל עכשיו, האם תעצור <math>A</math> עבור הקלט <math>A</math>? (כלומר, במקרה שהתוכנית <math>A</math> תקבל את עצמה) נחלק לשני מקרים, ונקבל סתירה בשניהם:
::נניח ש-<math>\ A(A)</math> תעצור. מכיוון שעל פי הצורה שבה הגדרנו את <math>A(A)</math>, היא עוצרת רק אם לא מתקיים <math>Halt(A,A)</math>, נסיק כי כך הם פני הדברים. אולם, מכיוון שמהגדרת האלגוריתם <math>Halt</math> הוא אינו מתקיים רק אם <math>A</math> אינה עוצרת על עצמה נגיע לסתירה - הנחנו ש-<math>A(A)</math> עוצרת וקיבלנו שהיא בהכרח אינה עוצרת.

::כעת נניח כי מתקיים ההפך: <math>A(A)</math> נכנסת ללולאה אינסופית. על פי הגדרת <math>A</math>, זה קורה רק אם מתקיים <math>Halt(A,A)</math>. לכן, מהגדרת האלגוריתם <math>Halt</math>, נובע ש <math>A</math> עוצרת עבור הקלט <math>A</math> - כלומר, הנחנו שהיא אינה עוצרת וקיבלנו כי היא בהכרח עוצרת.

:הנחנו שקיים אלגוריתם הפותר את בעיית העצירה והגענו לסתירה, לכן לא ייתכן אלגוריתם לפתרון בעיה זו.

ניתן להשתמש במשפט זה כדי להוכיח גם טענה חזקה יותר: אף תכונה לא-טריוויאלית של הפונקציה שאלגוריתם מחשב אינה ניתנת לחישוב. משפט זה ידוע בשם משפט רייס. למעשה, האפשרות להוכיח ישירות את המשפט על בעיית העצירה גרם לכך שמשפטי אי-כריעות רבים אחרים יתבססו על רדוקציות חישוביות ממנה.

ההוכחה לכך שבעיית העצירה אינה ניתנת לחישוב ניתנה על ידי אלן טיורינג. עם זאת, יש לשים לב שהעובדה כי ישנן פונקציות שלא ניתנות לחישוב נובעת מכך שעוצמת קבוצת הפונקציות גדולה-ממש מעוצמת קבוצת מכונות טיורינג (בניסוח פשטני, יש יותר פונקציות מדרכים לחשבן ולכן בהכרח יש פונקציות שאי אפשר לחשב. אומנם יש לשים לב שבין הפונקציות שאינן ניתנות לחישוב נמצאות פונקציות ש"אינן מעניינות", כיוון שלא ניתן לספק להן תיאור סופי).

==שייכות בעיית העצירה ל <math>RE</math>==
RE היא קבוצת השפות שניתן לבנות מכונת טיורינג שמקבלת כל מילה בשפה ואינה מקבלת מילה שלא שייכת לשפה, כלומר דוחה אותה או כלל לא עוצרת עליה.

ניתן לבנות מכונת טיורינג שמריצה את תוכנית <math>Q</math> על <math>X</math> וכשהיא עוצרת לקבל. אם <math>Q</math> עוצרת על <math>X</math> המכונה תזהה זאת ותקבל, אחרת היא רצה בלי לעצור.

==בעיית העצירה בתוכנית עם זיכרון סופי==

לא ניתן לממש באופן פיזיקלי מחשב בעל זיכרון אינסופי, משום שבכמות חומר סופית יש אינפורמציה במידה סופית.

כל תוכנית מחשב שרצה על מחשב בעל זיכרון סופי תעצור בתוך מספר צעדים חסום (לכל היותר 2 בחזקת מספר הביטים בזיכרון המחשב), או תיכנס ללולאה אינסופית. לכן ניתן לפתור את בעיית העצירה על מחשב בעל זיכרון סופי. בזיכרון המחשב יש לכלול גם את זיכרון המעבד, כגון אוגרים וכו', וכן את תוכנית המחשב עצמה.

==ראו גם==
*לכסון

== לקריאה נוספת ==
<div style="direction: ltr;">
* M. Sipser, Introduction to the Theory of Computation, PWS Publishing Co., 1997
* J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Co., 1979
</div>

==קישורים חיצוניים==

* [http://www.new.tzura.co.il/t/art/10920 הוכחה בחרוזים לאי הכריעות של בעיית העצירה]
* 
* סרטון אנימציה המסביר את בעיית העצירה וההוכחה, (קיים גם תרגום לעברית)
** [https://www.udiprod.com/halting-problem מידע נוסף על בעיית העצירה], udiprod
* 
* 
* , סרטון ביוטיוב (החל מ-1:10:00 בערך)
* 

קטגוריה:ערכים שבהם תבנית בריטניקה אינה מתאימה
קטגוריה:בעיות חישוביות
קטגוריה:חישוביות
קטגוריה:הוכחות
קטגוריה:בעיות שאינן ניתנות לחישוב
קטגוריה:בעיות לא כריעות במתמטיקה
קטגוריה:משפטי אי היתכנות