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

תוכן שנמחק תוכן שנוסף
Atavory (שיחה | תרומות)
Gran (שיחה | תרומות)
←‏משפט רייס: שחזרתי להוכחה המקורית, הקודמת לא היתה ברורה כלל (והיו בה הרבה חלקים לא נחוצים)
שורה 41:
 
{{משפט|תוכן=
לכל תכונה לא טריוויאלית <math>S</math> של שפות ב־<math>RE</math>ב־RE מתקיים:{{רווח קשיח|10}} <math>L_S \notin R</math>{{רווח קשיח|10}}}}
{{הוכחה|1=:
נניח תחילה שמתקיים <math>\emptyset \notin S</math> (כלומר, השפה הריקה אינה ב־S). נראה כי <math>L_S \notin R</math> על־ידי הרדוקציה <math>\text{HP} \le L_S</math>.
 
S אינה טריוויאלית אזי קיימת שפה <math>L_0</math> כך ש־<math>L_0 \in S</math>. מכיוון ש־S היא קבוצה של שפות ב־RE, גם <math>L_0 \in RE</math> ונניח כי <math>M_0</math> מקבלת אותה.
{{הוכחה|1=
נראה כי <math>L_S \notin R</math> על־ידי הרדוקציה ל[[תורת החישוביות/כריעות שפות#דוגמאות לשפות|בעיית העצירה]]. ספציפית, נניח על דרך השלילה ש<math>L_S \in R</math>, ולכן ישנה מ"ט Q כלשהי כך שעל קלט y, המכונה:
# <u>דוחה</u> אם <math>y</math> איננה הקידוד של מ״ט כלשהי.
# <u>דוחה</u> אם <math>y = <M'></math> (כלומר y היא הקידוד של מ״ט <math>M'</math> כלשהי) וכן <math><M'> \notin L_S</math>.
# <u>מקבלת</u> אם <math>y = <M'></math> (כלומר y היא הקידוד של מ״ט <math>M'</math> כלשהי) וכן <math><M'> \in L_S</math>.
 
נגדיר את הרדוקציה <math>f(\langle M \rangle, x) = \langle M_x \rangle</math> באופן הבא.
תחת הנחה-על-דרך-השלילה זו, נראה שאפשר להכריע, עבור כל מכונה <math>M</math> וקלט <math>x</math>, האם <math>M</math> עוצרת על <math>x</math> (מה ש[[תורת_החישוביות/כריעות_שפות/שפות_שאינן_כריעות#שפות_שאינן_כריעות|ידוע שאינו נכון]]).
המכונה <math>M_x</math> על הקלט w מבצעת:
לצורך ההוכחה נשים לב שהיות ש־<math>S</math> אינה טריוויאלית אזי קיימת שפה
# מריצה את M על x
<math>L_0</math>
# מריצה את <math>M_0</math> על <math>w</math>, ומקבלת/דוחה כמותה.
כך שמתקיים
(הערה: אם הקלט אינו <math>(\langle M \rangle, x)</math> פלט הפונקציה f מוגדר בתור מ״ט הדוחה כל קלט (באופן זה השפה של מכונה הפלט הוא <math>L(M)=\emptyset \notin S</math>)
<math>L_0 \in S \subseteq RE</math>.
נגדיר כ<math>M_0</math> את המכונה המקבלת את
<math>L_0</math>. נחלק את ההוכחה לשני חלקים, לפי השאלה האם
<math>\emptyset \notin S</math>
(כלומר, האם ה[[תורת החישוביות/כריעות שפות|שפה הריקה]] אינה ב־<math>S</math>).
 
נוכיח את תכונות הרדוקציה:
#f מלאה: הגדרנו את f לכל קלט אפשרי
# f ברת־חישוב: ייצור <math>\langle M_X \rangle</math> מתוך המחרוזת <math>(\langle M \rangle, x)</math> ומתוך המחרוזת הקבועה <math>\langle M_0\rangle</math> קל לביצוע ע״י מ״ט שצריכה רק לשנות מעט את קידודי המכונות כדי שירוצו אחת אחר השניה...
# f תקפה:
#* אם 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>(\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>
 
ראשית נניח כי
<math>\emptyset \notin S</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>M_0</math> על <math>w</math>, ומקבלת/דוחה כמותה.
במילים אחרות,
<math>M_x</math>,
היא שרשור של שתי מכונות. נגדיר כ<math>f</math> את הפונקציה שבהנתן
<math><M></math>
ו<math>x</math>, בונה את התיאור
<math><M_x></math>.
קל לראות שישנה מ"ט <math>F</math> רקורסיבית המממשת את <math>f</math>.
 
מה קורה כאשר <math>\emptyset \notin S</math>?{{ש}}
לפי הבניה, <math>M</math> עוצרת על <math>x</math> אמ"ם <math><M_x> \in L_S</math>:
מכיוון ש־S אינה טריוויאלית, ישנה <math>L\in RE, L\notin S</math>, וניתן לחזור על ההוכחה ע״י שימוש בשפה זו במקום בשפה <math>\emptyset</math>.
# אם <math>M</math> עוצרת על <math>x</math>, אז <math>L(M_x) = L(M_0)</math> מפני שלכל <math>w</math>, החלק הראשון של<math>M_x</math> פשוט מפעיל את <math>M</math> על <math>x</math>, ולאחר העצירה (המובטחת), מפעיל את <math>M_0</math> על w. לכן נקבל <math>L(M_x) = L(M_0) \in L_s</math>.
# אם <math>M</math> איננה עוצרת על <math>x</math>, אז היות ש-<math>M</math> היא השלב הראשון של <math>M_x</math>, גם <math>M_x</math> אינה עוצרת על אף קלט, ולכן <math>L(M_x) = \emptyset \notin L_S </math>.
לכן, בחלק זה של ההוכחה בו
<math>\emptyset \notin S</math>,
הראנו שמ<math>L_0 \in S \subseteq RE</math> נובע ש-<math>Q(f(<M>, x))</math>
היא הפתרון של עצירת כל <math>M</math> על כל ע"י מ"ט רקורסיביות <math>Q</math> ו<math>F</math>, מה שכמובן בלתי אפשרי.
 
דרך אחרת היא להסתכל על התכונה המשלימה <math>\overline S = RE \smallsetminus S</math>. מתקיים <math>\emptyset \notin \overline{S}</math> ולכן, כפי שהוכחנו <math>L_{\overline{S}}\notin R</math>. נשים לב ש
כעת נניח כי
<center><math>L_{\overline{S}}=\{\langle M\rangle \mid L(M) \in \overline S\} = \{\langle M\rangle \mid L(M) \notin S\} = \overline{L_S}</math></center>
<math>\emptyset \in S</math>.
כלומר <math>\overline {L_S} \notin R</math>, ומכיוון ש־R סגורה למשלים, זו הוכחה ש־<math>L_S \notin R</math> כנדרש.
אז לפי הגדרת קבוצה משלימה,
<math>\emptyset \notin \overline S</math>.
אבל כפי שראינו לעיל, גם המשלים של תכונה לא-טריוויאלית הוא תכונה לא טריוויאלית, ולכן נוכל לחזור על החלק הקודם עם התכונה
<math>\overline S</math>.
}}
 
==משפט רייס המורחב==