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

תוכן שנמחק תוכן שנוסף
Atavory (שיחה | תרומות)
מ הגהה
Atavory (שיחה | תרומות)
שורה 36:
==משפט רייס==
 
המשפט הבא מראה כי אי אפשר לבנות מ"ט רקורסיבית המקבלת קידוד של מ"ט, ומחליטה האם השפה המתאימה למ"ט מקיימת תכונה לא טריוויאלית.
 
{{משפט|תוכן=
שורה 42 ⟵ 43:
{{הוכחה|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>M</math> וקלט <math>x</math>, האם <math>M</math> עוצרת על <math>x</math> (מה ש[[תורת_החישוביות/כריעות_שפות/שפות_שאינן_כריעות#שפות_שאינן_כריעות|ידוע שאינו נכון]]).
לצורך ההוכחה נשים לב שהיות ש־Sש־<math>S</math> אינה טריוויאלית אזי קיימת שפה
<math>L_0</math>
כך שמתקיים
שורה 54 ⟵ 55:
<math>L_0</math>. נחלק את ההוכחה לשני חלקים, לפי השאלה האם
<math>\emptyset \notin S</math>
(כלומר, האם ה[[תורת החישוביות/כריעות שפות|שפה הריקה]] אינה ב־Sב־<math>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>,
היא שרשור של שתי מכונות. נגדיר כfכ<math>f</math> את הפונקציה שבהנתן
<math><M></math>
ו<math>x</math>, בונה את התיאור
<math><M_x></math>.
קל לראות שישנה מ"ט <math>F</math> רקורסיבית המממשת את <math>f</math>.
 
לפי הבניה, <math>M</math> עוצרת על <math>x</math> אמ"ם <math><M_x> \in L_S</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(w) = M_0L(w)</math>. היות ש <math><M_0> \in L_S</math>, אז <math><M_x>) \in L_SL_s</math>.
# אם <math>M</math> איננה עוצרת על <math>x</math>, אז היות שMש-<math>M</math> היא השלב הראשון של <math>M_x</math>, גם <math>M_x</math> אינה עוצרת על אף קלט, ולכן <math>L(M_x) = \emptyset \notin L_S </math>. אבל, כאמור
לכן, בחלק זה של ההוכחה הנחנובו ש <math>\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> וFו<math>F</math>, מה שכמובן בלתי אפשרי.
<math>Q(f(<M>, x))</math>
היא הפתרון של עצירת כל M על כל ע"י מ"ט רקורסיביות Q וF, מה שכמובן בלתי אפשרי.
 
כעת נניח כי
שורה 88:
<math>\overline S</math>.
}}
 
==משפט רייס המורחב==
 
{{תרגיל|יישור=ימין|