משפט רייס

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

באופן פורמלי, שפת הקידודים למכונות הטיורינג, שהשפה שלהן ב-<math>S</math> <math display="block">L_S= \{ \langle M\rangle \mid L(M) \in S\}</math> היא שפה בלתי כריעה אם <math>\ S</math> היא קבוצה לא-טריוויאלית של שפות.

בנוסף, אם מתקיים כי <math>\varnothing \in S</math> אזי השפה אינה כריעה למחצה.

הקבוצה <math>\ S</math> תחשב טריוויאלית אם היא הקבוצה הריקה (אינה מכילה אף שפה), או קבוצת כלל השפות מזוהות טיורינג. הסימון <math>\langle M\rangle</math> מציין מחרוזת בינארית המהווה קידוד של מכונת טיורינג <math>\ M</math>.

== הוכחת המשפט ==

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

=== מקרה ראשון: הפונקציה הריקה אינה בעלת התכונה ===

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

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

התוכנית שלנו תיצור מ-<math>\ M</math> ו-<math>\ x</math> אלגוריתם חדש, <math>\ M_x</math>, שפועל בצורה הבאה על הקלט <math>\ w</math>:
:#הפעל את <math>\ M</math> על הקלט <math>\ x</math> (אם קיים פלט, נתעלם ממנו).
:#הפעל את <math>\ A</math> על הקלט <math>\ w</math> והחזר את התוצאה כפלט.

כלומר, האלגוריתם <math>\ M_x</math> מורכב משני שלבים שאינם קשורים זה בזה. החשיבות של השלב הראשון בכך שהוא מהווה אבן בוחן לשאלה האם <math>\ M</math> עוצר על <math>\ x</math>; אם הוא אינו עוצר, <math>\ M_x</math> לא יגיע לעולם לשלב השני.

בשל אופן הבנייה שלו, <math>\ M_x</math> מחשב אחת משתי פונקציות: אם <math>\ M</math> לא עוצר על <math>\ x</math>, הרי ש-<math>\ M_x</math> מחשב את הפונקציה הריקה - שכן ללא תלות בקלט <math>\ w</math>, הוא פשוט רץ לנצח. אם לעומת זאת <math>\ M_x</math> כן עוצר על <math>\ x</math>, הרי שהוא יחשב בשלב הבא את פעולת הפונקציה של <math>\ A</math> על הקלט <math>\ w</math>.

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

=== מקרה שני: הפונקציה הריקה בעלת התכונה ===
נשים לב כי לכל תכונה <math>\ X</math> ניתן לחשוב על התכונה ה"משלימה" לה, <math>\ \overline{X}</math>. פונקציה מקיימת את <math>\ \overline{X}</math> אם ורק אם היא אינה מקיימת את <math>\ X</math>.

אם קיים אלגוריתם <math>\ Q</math> שמכריע האם הפונקציה שמחשב <math>\ A</math> היא בעלת התכונה <math>\ X</math>, אז ניתן ליצור בעזרתו אלגוריתם אחר שבודק האם <math>\ A</math> היא בעלת התכונה <math>\ \overline{X}</math> – הוא פשוט מריץ את <math>\ Q</math> על <math>\ A</math>ועונה הפוך ממנו.

אלא שהפונקציה הריקה אינה בעלת התכונה <math>\ \overline{X}</math> (שכן הנחנו שהיא כן בעלת התכונה <math>\ X</math>) ולכן הגענו לסתירה לתוצאה שהוכחנו בסעיף הקודם - הראינו כיצד ניתן להכריע האם אלגוריתם <math>\ A</math> נתון מחשב פונקציה בעלת תכונה לא טריוויאלית שהפונקציה הריקה לא מקיימת.

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

* 
* 
* 

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