בעיית העצירה
בעיית העצירה היא בעיה מרכזית בתחום החישוביות, שהוא אחד מעמודי התווך של מדעי המחשב התאורטיים.
בעיית העצירה מנוסחת כבעיית ההכרעה הבאה: בהינתן תוכנית מחשב וקלט, האם התוכנית תסיים את פעולתה בשלב כלשהו עבור קלט זה.
אלן טיורינג הוכיח ב-1936 כי בעיית העצירה על מכונות טיורינג (מודל תאורטי של מחשב בעל זיכרון אינסופי) אינה כריעה, כלומר אין אלגוריתם שמכריע עבור כל תוכנית מחשב וקלט האם התוכנית עוצרת כאשר מופעלת על (בקיצור: האם עוצרת על ) או לא. חשוב להבחין שמבחינה לוגית, בהינתן תוכנית מסוימת וקלט עבורה, התשובה לשאלה "האם היא עוצרת?" מוגדרת היטב וחד משמעית ( - או כן, או לא).
לעומת זאת ניתן לבנות מכונת טיורינג שמקבלת כל תוכנית מחשב וקלט כך שתוכנית המחשב עוצרת על קלט זה, ולא מקבלת אך אולי גם לא דוחה אם התוכנית אינה עוצרת על קלט זה, ולכן בעיית העצירה ניתנת למנייה רקורסיבית ושייכת לקבוצה .
הוכחת אי-כריעות
[עריכת קוד מקור | עריכה]ההוכחה לאי-כריעות בעיית העצירה נעשית בדרך השלילה: מראים כי מההנחה שניתן לפתור את בעיית העצירה מגיעים לסתירה - קיימת תוכנית שעבור קלט מסוים חייבת גם לעצור וגם לא לעצור לעולם.
- נניח שיש אלגוריתם שמקבל אם עוצרת על ודוחה אחרת, ונתבונן בתוכנית הבאה המקבלת תוכנית כקלט:
- אם , הכנס ללולאה אינסופית.
- אחרת, עצור.
- נשים לב כי מעבירים כאן את פעמיים: הן בתור התוכנית שיש לבדוק והן בתור הקלט לתוכנית שעליו היא נבדקת. אין בעיה עקרונית בהעברת כקלט - ניתן לחשוב על כל קלט כרצף של תווים, ולכן גם תוכנית מחשב יכולה להיחשב לקלט.
- נשאל עכשיו, האם תעצור עבור הקלט ? (כלומר, במקרה שהתוכנית תקבל את עצמה) נחלק לשני מקרים, ונקבל סתירה בשניהם:
- נניח ש- תעצור. מכיוון שעל פי הצורה שבה הגדרנו את , היא עוצרת רק אם לא מתקיים , נסיק כי כך הם פני הדברים. אולם, מכיוון שמהגדרת האלגוריתם הוא אינו מתקיים רק אם אינה עוצרת על עצמה נגיע לסתירה - הנחנו ש- עוצרת וקיבלנו שהיא בהכרח אינה עוצרת.
- כעת נניח כי מתקיים ההפך: נכנסת ללולאה אינסופית. על פי הגדרת , זה קורה רק אם מתקיים . לכן, מהגדרת האלגוריתם , נובע ש עוצרת עבור הקלט - כלומר, הנחנו שהיא אינה עוצרת וקיבלנו כי היא בהכרח עוצרת.
- הנחנו שקיים אלגוריתם הפותר את בעיית העצירה והגענו לסתירה, לכן לא ייתכן אלגוריתם לפתרון בעיה זו.
ניתן להשתמש במשפט זה כדי להוכיח גם טענה חזקה יותר: אף תכונה לא-טריוויאלית של הפונקציה שאלגוריתם מחשב אינה ניתנת לחישוב. משפט זה ידוע בשם משפט רייס. למעשה, האפשרות להוכיח ישירות את המשפט על בעיית העצירה גרם לכך שמשפטי אי-כריעות רבים אחרים יתבססו על רדוקציות חישוביות ממנה.
ההוכחה לכך שבעיית העצירה אינה ניתנת לחישוב ניתנה על ידי אלן טיורינג. עם זאת, יש לשים לב שהעובדה כי ישנן פונקציות שלא ניתנות לחישוב נובעת מכך שעוצמת קבוצת הפונקציות גדולה-ממש מעוצמת קבוצת מכונות טיורינג (בניסוח פשטני, יש יותר פונקציות מדרכים לחשבן ולכן בהכרח יש פונקציות שאי אפשר לחשב. אומנם יש לשים לב שבין הפונקציות שאינן ניתנות לחישוב נמצאות פונקציות ש"אינן מעניינות", כיוון שלא ניתן לספק להן תיאור סופי).
שייכות בעיית העצירה ל
[עריכת קוד מקור | עריכה]RE היא קבוצת השפות שניתן לבנות מכונת טיורינג שמקבלת כל מילה בשפה ואינה מקבלת מילה שלא שייכת לשפה, כלומר דוחה אותה או כלל לא עוצרת עליה.
ניתן לבנות מכונת טיורינג שמריצה את תוכנית על וכשהיא עוצרת לקבל. אם עוצרת על המכונה תזהה זאת ותקבל, אחרת היא רצה בלי לעצור.
בעיית העצירה בתוכנית עם זיכרון סופי
[עריכת קוד מקור | עריכה]לא ניתן לממש באופן פיזיקלי מחשב בעל זיכרון אינסופי, משום שבכמות חומר סופית יש אינפורמציה במידה סופית.
כל תוכנית מחשב שרצה על מחשב בעל זיכרון סופי תעצור בתוך מספר צעדים חסום (לכל היותר 2 בחזקת מספר הביטים בזיכרון המחשב), או תיכנס ללולאה אינסופית. לכן ניתן לפתור את בעיית העצירה על מחשב בעל זיכרון סופי. בזיכרון המחשב יש לכלול גם את זיכרון המעבד, כגון אוגרים וכו', וכן את תוכנית המחשב עצמה.
ראו גם
[עריכת קוד מקור | עריכה]לקריאה נוספת
[עריכת קוד מקור | עריכה]- 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
קישורים חיצוניים
[עריכת קוד מקור | עריכה]- הוכחה בחרוזים לאי הכריעות של בעיית העצירה
- גדי אלכסנדרוביץ', בעיית העצירה, באתר "לא מדויק", 26 בספטמבר 2007
- סרטון אנימציה המסביר את בעיית העצירה וההוכחה, Proof That Computers Can't Do Everything (The Halting Problem), סרטון באתר יוטיוב (קיים גם תרגום לעברית)
- מידע נוסף על בעיית העצירה, udiprod
- וידאו של הרצאה שמסבירה את הבעיה ואת ההוכחה ללא נוסחאות ובלי להניח שם רקע מתמטי, סרטון באתר יוטיוב
- שמואל וינוגרד, מכונת טיורינג, מחשבות 35, יולי 1972, עמ' 13–17
- וידאו של הוכחת הטענה בעברית, סרטון באתר יוטיוב, סרטון ביוטיוב (החל מ-1:10:00 בערך)
- בעיית העצירה, באתר MathWorld (באנגלית)