משפט רייס
מתוך ויקיפדיה, האנציקלופדיה החופשית
משפט רייס הוא משפט מרכזי בתחום החישוביות, שעוסק ביכולת של אלגוריתמים לחקור אלגוריתמים אחרים. המשפט אומר שאין תוכנית מחשב שמקבלת כקלט תוכנית מחשב אחרת, ומכריעה האם הפונקציה שמחשבת תוכנית מחשב זו היא בעלת תכונה מסוימת "לא-טריוויאלית" או לא. המשמעות של היות התכונה "לא-טריוויאלית" היא שקיימות תוכניות מחשב שהפונקציות שלהן הן בעלות התכונה, ויש תוכניות מחשב שהפונקציות שלהן אינן בעלות התכונה. יש לשים לב שהתכונה היא תכונה של הפונקציה, ולא של תוכנית המחשב עצמה.
[עריכה] הוכחת המשפט
הוכחת המשפט מפרידה בין שני מקרים, תוך שימוש ב"פונקציה הריקה". הפונקציה הריקה היא פונקציה שתחום ההגדרה שלה ריק. אלגוריתם מחשב את הפונקציה הריקה אם ורק אם הוא לא עוצר על אף קלט, כלומר נכנס תמיד ללולאה אינסופית או שערכי הביניים של האלגוריתם גדלים תמיד ללא הגבלה.
[עריכה] מקרה ראשון: הפונקציה הריקה אינה בעלת התכונה
נניח בשלילה שקיים אלגוריתם שמכריע האם הפונקציה שמחשב אלגוריתם נתון היא בעלת התכונה, ונראה כי ניתן לפתור בעזרת אותו אלגוריתם את בעיית העצירה. נבחר אלגוריתם כלשהו A שהפונקציה שלו היא בעלת התכונה (אלגוריתם כזה בהכרח קיים, כי התכונה לא-טריוויאלית). נשתמש בו בתוכנית מחשב חדשה שניצור: התוכנית תקבל אלגוריתם M וקלט x, ותיצור אלגוריתם אחר - שהוא האלגוריתם שעליו נפעיל את התוכנית שבודקת את קיום התכונה. אלגוריתם זה מקבל קלט w, ופועל כך:
-
- הפעל את אלגוריתם M על קלט x (אם קיים פלט, נתעלם ממנו).
- הפעל את אלגוריתם A על קלט w והחזר את התוצאה כפלט.
האלגוריתם ההיפותטי יבדוק האם הפונקציה החדשה היא בעלת אותה תכונה, ויחזיר את התשובה כפלט.
נשים לב, שאם האלגוריתם M עוצר על הקלט x, האלגוריתם החדש שיצרנו למעשה מחשב את הפונקציה שמחשב אלגוריתם A. כלומר, הפונקציה שלו היא בעלת התכונה. אם האלגוריתם M לא עוצר על הקלט x, האלגוריתם החדש שיצרנו לא עוצר לעולם, כלומר הוא מחשב את הפונקציה הריקה והפונקציה שלו אינה בעלת התכונה.
בצורה הזו ניתן להכריע האם המכונה M עוצרת על הקלט x - אם הפונקציה החדשה היא בעלת התכונה אז המכונה עוצרת, ואם הפונקציה החדשה היא לא בעלת התכונה - אז המכונה לא עוצרת. כלומר, מצאנו פתרון לבעיית העצירה - וזה בלתי אפשרי, בסתירה להנחה הראשונה שקיים אלגוריתם שמחשב את קיום התכונה.
[עריכה] מקרה שני: הפונקציה הריקה בעלת התכונה
נניח בשלילה שקיים אלגוריתם שמכריע האם הפונקציה שמחשב אלגוריתם נתון היא בעלת התכונה. אם כך, אנחנו יכולים ליצור אלגוריתם אחר, שיקבל אלגוריתם, ויחליט אם הפונקציה שלו איננה בעלת התכונה. למעשה אלגוריתם זה מכריע לגבי תכונה אחרת, לא-טריוויאלית, של פונקציות, והפונקציה הריקה לא בעלת תכונה זו. בהוכחת מקרה הראשון הוכחנו שאלגוריתם כזה לא יכול להתקיים.

