משפט רייס

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

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

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

פונקציה ריקה היא פונקציה שלא מוגדר לה אף ערך; התוכנית שמחשבת אותה לא עוצרת על כל קלט. נניח שקיים אלגוריתם Q שמכריע האם הפונקציה שמחשבת برنامه נתון מקיימת את התכונה. כיון שהתכונה לא-טריוויאלית, קיימת מכונה A שמחשבת פונקציה שמקיימת את התכונה.

נבנה מכונה M_x מהאלגוריתם M ומהקלט x של בעיית העצירה. על קלט w היא מפעילה תחילה את M על x. אם M לא עוצר על x, אז M_x לעולם לא תשלים ותחשׁב את הפונקציה הריקה. אם M עוצר על x, אז M_x ממשיכה ומריצה את A על w.

מכיוון ש-M_x או מחשבת את הפונקציה הריקה או את פונקציית A, בדיקה האם ל-M_x יש את התכונה תאפשר לדעת האם M עוצר על x. זאת נותנת אלגוריתם לבעיית העצירה, וזה סותר את הבלתי-ניתנות להכרעה של בעיית העצירה. לכן Q לא יכול להתקיים.

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

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

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

נניח שיש תוכנית Q שיכולה להחליט. נמצא שהיא נותנת תשובה גם לבעיית העצירה. בונים תוכנית חדשה M_x שמקבלת w. היא מפעילה קודם את M על x. אם M לא עוצר על x, אז M_x אף היא לא עוצרת. אם M כן עוצר, אז M_x מריצה תוכנית קבועה A על w.

אז M_x או לא עוצרת (ופונקציה ריקה), או שהיא עושה את מה ש-A עושה. לכן אם נוכל לבדוק האם ל-M_x יש את התכונה, נדע גם האם M עוצר על x. זה בלתי אפשרי. לכן אין תוכנית Q.

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