תורת החישוביות/כריעות שפות/משפט רייס: הבדלים בין גרסאות בדף

נראה כי <math>L_S \notin R</math> על־ידי הרדוקציה <math>\text{HP} \le L_S</math>. כלומר, נניח על דרך השלילה <math>L_S \in R</math>, ונראה כי אפשר להכריע לכל מ"ט <math>M</math> וקלט <math>x</math>, האם <math>M</math> עוצרת על <math>x</math> ((מה ש[[תורת_החישוביות/כריעות_שפות/שפות_שאינן_כריעות#שפות_שאינן_כריעות|ידוע שאינו נכון]]).

אחרת, פשוט נוכיח את המשפט לגבי התכונה המשלימה <math>\overline S</math> -.

היות ש-ש־<math>S</math> אינה טריוויאלית, בהכרח קיימת שפה <math>L_0</math> כך ש־<math>L_0 \in S</math>. מכיוון ש־<math>S</math> היא קבוצה של שפות ב־<math>RE</math>, גם <math>L_0 \in RE</math>, ונניח כי <math>M_0</math> היא הממ"ט המקבלת אותה.

נגדיר את הרדוקציה ע"י מ"טמ״ט <math>M_x</math>, הפועלת כך.: בנהתן קלט <math>w</math>, המ"טהמ״ט <math>M_x</math>:,

# מריצה את <math>M</math> על <math>x</math> (ומתעלמת מהתוצאה, אם יש), ואז

מהנחתנו בשלילה ש-ש־<math>L_S \in R</math>, נובע שיששקיימת מ"ט רקורסיבית <math>Q</math> המכריעה זאתאת <math>L_S</math>. כדי להכריע האם <math>M</math> עוצרת על <math>x</math>, נשאל את <math>Q</math> האם <math>M_x \in L_S</math>:

# אם <math>M</math> איננה עוצרת על <math>x</math>, אז גם <math>M_x</math> איננה עוצרת על אף <math>w</math>. אם כך, <math>L(M_x) = \emptyset \notin S</math>, ו-ו־<math>Q</math> תכריע ש-ש־<math>M_x \notin L_S</math>.

# אם <math>M</math> עוצרת על x{{כ}}, אז <math>M_X</math> מתנהגת בדיוק כמו <math>M_0</math>{{כ}}. אם כך, <math>L(M_x)=L(M_0)\in S</math>, ו-ו־<math>Q</math> תכריע ש-ש־<math>M_x \in L_S</math>.

נשים לב שהרדוקציהשאכן אכןניתן ברתלבנות חישובאת - <math>M_x</math>: בהנתן <math>(\langle M \rangle, x)</math>, קל לבנות פונקציהמ״ט המשרשרת את שתי המכונות ויוצרת את תיאור <math>M_x</math>. כמו כן, לפי הנחתנוהנחת בשלילההשלילה, הקריאה לל־<math>Q</math> מסתיימתעוצרת גםעל כןכל קלט.