בעיית העצירה

מתוך ויקיפדיה, האנציקלופדיה החופשית

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

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

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

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

[עריכה] הוכחת אי-כריעות

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

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

אם , הכנס ללולאה אינסופית.

אחרת, עצור.

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

נשאל עכשיו, האם תעצור עבור הקלט ? (כלומר, במקרה שהתוכנית תקבל את עצמה) נחלק לשני מקרים, ונקבל סתירה בשניהם:

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

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

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

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

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

[עריכה] קישורים חיצוניים

• הוכחה בחרוזים לאי הכריעות של בעיית העצירה
• גדי אלכסנדרוביץ', בעיית העצירה, באתר "לא מדויק"