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

תוכן שנמחק תוכן שנוסף
Atavory (שיחה | תרומות)
Atavory (שיחה | תרומות)
שורה 86:
בהנתן תכונה <math>S \subseteq RE</math>, אז <math>LS \in RE</math> אמ"ם מתקיימות כ"א מהתכונות הבאות:
# אם <math>L_1 \in S</math>, וכן <math>L_1, L_2 \in RE</math>, וכן <math>L_1 \subseteq L_2</math>, אז <math>L_2 \in S</math>.
# אם <math>L_1L \in S</math>, אז יש ל-<math>L_2L</math> תת-שפה סופית <math>L_2L' \subseteq L_1L</math> המקיימת <math>L_2L' \in S</math>.
# שפת כל השפות הסופיות ב-<math>S</math> היא ב-<math>RE</math> (כלומר, יש מ"ט המונה כל שפה סופית ב-<math>S</math>).
}}
שורה 104:
# בלולאה הפנימית ביותר, עבור ערך <math>i</math> ותת-קבוצה של מילים מתקבלות, המכונה <math>Q</math> מריצה את <math>Q_3</math> לשאול האם תת-הקבוצה שייכת ל<math>S</math>. אם כן, המכונה <math>Q</math> עוצרת בתשובה חיובית.
 
נשים לב שמתכונה 1 נובע שאם
<math>L = L(M) \in S</math>,
אז יש לה תת-שפה סופית
<math>L'</math>
שגם היא ב-<math>S</math>. שיטת הdovetailing כאן מבטיחה שהחל משלב כלשהו, <math>L'</math> תשקל על ידי <math>Q_3</math>. תנאי 3 מבטיח שבזמן סופי כלשהו, <math>Q_3</math> תזהה את <math>L'</math> כשייכת ל-<math>S</math>. שוב פעם, שיטת הdovetailing מבטיחה שלאחר מספיק איטרציות <math>Q_3</math> תפעל מספיק פעמים על <math>L'</math>. כלומר, אם התשובה חיובית, אז <math>Q</math> בוודאות תחזיר תשובה חיובית.
 
נותר להראות ש-<math>Q</math> לא תחזיר תשובה חיובית במקרה שאיננו נכון.
}}