תורת החישוביות/כריעות שפות/משפט רייס: הבדלים בין גרסאות בדף
תוכן שנמחק תוכן שנוסף
שילוב זמני |
←משפט רייס: פורמליזם |
||
שורה 61:
נשים לב שהרדוקציה אכן ברת חישוב - בהנתן <math>(\langle M \rangle, x)</math>, קל לבנות פונקציה המשרשרת את שתי המכונות ויוצרת את תיאור <math>M_x</math>. כמו כן, לפי הנחתנו בשלילה, הקריאה ל<math>Q</math> מסתיימת גם כן.
}}
{{הארה|1=
באופן פורמלי, ההוכחה לעיל שקולה להגדרת פונקציית הרדוקציה <math>f(\langle M \rangle, x)=\langle M_x \rangle</math>, ושימוש במשפט הרדוקציה ההפכי. קל לראות שפונקציית הרדוקציה ברת־חישוב ומלאה (מקרה הקצה בו <math>\langle M \rangle</math> אינו קידוד תקין, יוגדר כפלט <math>\langle M_0 \rangle</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>
}}
| |||