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