תורת החישוביות/כריעות שפות/משפט רייס: הבדלים בין גרסאות בדף
תוכן שנמחק תוכן שנוסף
שורה 40:
{{משפט|תוכן=
לכל תכונה לא טריוויאלית S של שפות ב־RE מתקיים:{{רווח קשיח|10}} <math>L_S \notin R</math>{{רווח קשיח|10}}}}
{{הוכחה
נראה כי <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> ((מה ש[[תורת_החישוביות/כריעות_שפות/שפות_שאינן_כריעות#שפות_שאינן_כריעות|ידוע שאינו נכון]]).
S אינה טריוויאלית אזי קיימת שפה <math>L_0</math> כך ש־<math>L_0 \in S</math>. מכיוון ש־S היא קבוצה של שפות ב־RE, גם <math>L_0 \in RE</math> ונניח כי <math>M_0</math> מקבלת אותה.▼
בלי הגבלת הכלליות, נניח כי ה[[תורת החישוביות/כריעות שפות|שפה הריקה]] אינה ב־<math>S</math> (כלומר
אחרת, פשוט נוכיח את המשפט לגבי התכונה המשלימה <math>\overline S</math> -
כפי שראינו לעיל, גם המשלים של תכונה לא-טריוויאלית הוא תכונה לא טריוויאלית, והכרעה רקורסיבית לגבי <math>S</math> שקולה להכרעה רקורסיבית לגבי <math>\overline S</math>.
# מריצה את <math>M_0</math> על w, ומקבלת/דוחה כמותה.▼
#* אם M לא עוצרת על x, גם <math>M_x</math> לא עוצרת. <math>L(M_x) = \emptyset \notin S</math>▼
#* אם M עוצרת על x{{כ}}, <math>M_X</math> מתנהגת בדיוק כמו <math>M_0</math>{{כ}}, <math>L(M_x)=L(M_0)\in S</math>▼
▲היות ש-<math>S</math> אינה טריוויאלית,
נגדיר את הרדוקציה ע"י מ"ט <math>M_x</math>, הפועלת כך. בנהתן קלט <math>w</math>, המ"ט <math>M_x</math>:
▲מה קורה כאשר <math>\emptyset \notin S</math>?{{ש}}
# מריצה את <math>M</math> על <math>x</math> (ומתעלמת מהתוצאה, אם יש), ואז
מהנחתנו בשלילה ש-<math>L_S \in R</math>, נובע שיש מ"ט רקורסיבית <math>Q</math> המכריעה זאת. כדי להכריע האם <math>M</math> עוצרת על <math>x</math>, נשאל את <math>Q</math> האם <math>M_x \in L_S</math>:
▲#
▲#
נשים לב שהרדוקציה אכן ברת חישוב - בהנתן <math>(\langle M \rangle, x)</math>, קל לבנות פונקציה המשרשת את שתי מ"ט. כמו כן, לפי הנחתנו בשלילה, הקריאה ל<math>Q</math> מסתיימת גם כן.
}}
==משפט רייס המורחב==
|