שיחה:תורת החישוביות/כריעות שפות/משפט רייס

מספר שינויים

הדף אחלה. שתי הצעות:

1. לפצל את משפט רייס לשניים: זה של R וזה של RE. גדי אלכסנדרוביץ' כתב משהו די מפורט על השני. הייתי רוצה להוסיף אותו לכאן, ולהעביר את התרגיל שיש כאן לדף תרגילים.
2. להעביר את הדוגמאות לדף תרגילים (אולי להוסיף ולהשאיר אחד או שניים)

Atavory - שיחה 13:52, 27 בינואר 2012 (IST)

מה אתה מתכוון בלהפריד R מ־RE ? זה לא מופרד כעת? ‏gran‏ - שיחה 03:40, 28 בינואר 2012 (IST)

ישנה השאלה האם ההכרעה בR (לא), וישנה השאלה האם היא בRE (יש תנאים שעבורם כן). Atavory - שיחה 09:01, 28 בינואר 2012 (IST)

איבדתי אותך לגמרי. אני חושש שלא הגדרת נכון את הבעיה שאתה מנסה להוכיח. כרגע מה שאתה מנסה להוכיח סותר את משפט רייס. :) ‏gran‏ - שיחה 21:45, 28 בינואר 2012 (IST)

גם אני אבדתי אותך. מה שאתה טוען שסותר את משפט רייס (לא הבנתי על מה אתה מדבר), יושב בצורה מאד מורחבת ומפורטת בחלק הדף על מניה רקורסיבית. אם מצאת שם משהו שסותר את משפט רייס, אתה מוזמן לכתוב מה (עם או בלי סמיילים), ואולי גם לפרסם את העניין. שים לב שמה שאתה קורא לו משפט רייס המורחב (אגב, בתרגילים יש הרחבה לכוון שונה לגמרי), יושב כעת בשני חלקים בתוך הדף. זו סמטוחה. או ששחזרת שוב בלי ממש להכנס לעומק תוכן הדף, או שאתה מדבר על משהו אחר שאין לי מושג מהו. Atavory - שיחה 07:53, 29 בינואר 2012 (IST)

דווקא לא שחזרתי, רק הוספתי את ההרחבה שמראה שהשפה אינה RE, אני אעבור על זה שוב לראות שהכל עקבי כי יכול להיות שזה חוזר על עצמו. באשר לחלק שהוספת - אם אני לא מצליח להבין את כוונתך, סביר להניח שקורא מהשורה לא יצליח. אני מבין שזה מכעיס אותך, אבל זו לא אשמתי שאני לא מבין מה שניסית להוכיח. אם הבנתי נכון, אתה מתאר תנאים שעבורם $L_{S}\in RE$. משפט רייס קובע שכל עוד S לא טריוויאלית $L_{S}\notin RE$. זו סתירה. מה לא הבנתי נכון? ‏gran‏ - שיחה 09:33, 29 בינואר 2012 (IST)

כתוב כך:

"

בחלק קודם ראינו שאם התכונה $S$ איננה טריוויאלית, אז שאלת השייכות :::::::ל-$L_{S}$ איננה ב-$R$. בחלק זה נעסוק בשאלה מהם התנאים ל-$S$ כך ששאלת השייכות ל-$L_{S}$ תהיה ב-$RE$.

ללא תנאים נוספים, אם $S$ תכונה לא טריוויאלית, אז שאלת השייכות ל-$L_{S}$ איננה ב-$RE$. בתרגיל: הכרעת תכונות לא-טריוויאליות איננה נתנת למניה רקורסיבית תתבקש להוכיח זאת.

עם זאת ישנם תנאים נוספים ל-$S$, שקיומם מהווה תנאי מספיק והכרחי לכך ששאלת השייכות היא ב-$RE$.

משפט: בהנתן תכונה $S\subseteq RE$, אז $LS\in RE$ אמ"ם מתקיימות כ"א מהתכונות הבאות: אם $L'\in S$, וכן $L,L'\in RE$, וכן $L'\subseteq L$, אז $L\in S$. אם $L\in S$, אז יש ל-$L$ תת-שפה סופית $L'\subseteq L$ המקיימת $L'\in S$. שפת כל השפות הסופיות ב-$S$ היא ב-$RE$ (כלומר, יש מ"ט המונה כל שפה סופית ב-$S$).

"

אז לא ברור לי מה הבעיה? מילא אם יש איזו חוסר הבנה בהוכחת המשפט, אבל בשלב זה? כתוב בצורה מאד ברורה שסתם כך, עבור תכונה לא-טריוויאלית, הבעיה היא לא בRE, ואם מוסיפים תנאים מסויימים, אז היא כן בRE.

אני שוב גם חוזר ש"משפט רייס המורחב" איננו, למיטב ידיעתי, שם מקובל. אפשר להרחיב את משפט רייס בכוונים שונים, נניח במספר השפות (הוספתי בעיה כזו).

בקיצור, למעט הוספת פסקה מתווה בתחילת הפרק, נראה לי שצריך להחזיר את הדברים ללפני עריכתך המבטלת בדף (ראה גם ההערה הבאה). Atavory - שיחה 20:17, 29 בינואר 2012 (IST)

המשפט לעיל (נקרא לו "סייגים של רייס") אומר שיש S לא טריוויאלית שמקיימת תנאים מסויימים, ועבורה $L_{S}\in RE$. המשפט השני (נקרא לו "רייס מורחב") אומר שלכל S לא טריוויאלית מתקיים $L_{S}\notin RE$. האם אתה טוען שרייס מורחב שגוי? או האם אני לא הבנתי את משפט הסייגים של רייס כהלכה? לא ייתכן ששני המשפטים האלה נכונים בו־זמנית. ‏gran‏ - שיחה 21:39, 29 בינואר 2012 (IST)

נראה לי שהבנתי. ‏gran‏ - שיחה 21:53, 29 בינואר 2012 (IST)

הוכחת משפט רייס

ראיתי ששחזרת שוב. מסתבר שדעותינו חלוקות בשאלה איזו הוכחה ברורה יותר. לדעתי זו משמעותית פחות. היא מתמקדת בחלקים הטכניים של הרדוקציה, ופחות בה שמנסים לעשות (לפתור את בעיי העצירה). לגבי חלקים מיותרים: מה זה משנה אם f מלאה או לא? גם אם איננה מלאה, זה עדיין פותר את בעיית העצירה. לחלופין, גישה מאד פורמאלית לנכונות הרדוקציה היתה צריכה גם לכלול את רקורסיביות הקריאה למכונה המכריעה על $M_{x}$, לא רק שרשור המכונות. היו גם מספר שגיאות לשוניות ואי-אחידות בתגים, לדעתי, שתקנתי ונעלמו. על כל פנים, ניסיתי לשלב בין שתי הגרסאות כדי שירווח לכולם. Atavory - שיחה 08:48, 28 בינואר 2012 (IST)

לדוגמה, המשפט הפותח "נניח תחילה שמתקיים $\emptyset \notin S$ (כלומר, השפה הריקה אינה ב־S). נראה כי $L_{S}\notin R$ על־ידי הרדוקציה ${\text{HP}}\leq L_{S}$." זה מייצר את הרושם שכאשר $\emptyset \notin S$ יש רדוקציה לבעיית העצירה, ובמובלע, במקרה השני יהיה משהו אחר. הדגש כאן הפוך, לדעתי. בכלל, לא ממש מדובר בשני מקרים שונים - את $\emptyset \notin S$ אפשר בכלל להכניס ב"בלי הגבלת הכלליות" Atavory - שיחה 09:01, 28 בינואר 2012 (IST)

טוב, בגדול ישנה כאן עכשיו ההוכחה המקורית שלך, עם מספר שינויים קטנים שלדעתי יש בהם ייתרון. מקווה שעכשיו בסדר מבחינת כולם. כל טוב, Atavory - שיחה 16:37, 28 בינואר 2012 (IST)

אין לי בעיה עם רוב השינויים שעשית, פרט לדבר אחד: אין צורך בכל החלק של המכונה Q. החלק הזה חוזר על ההוכחה של משפט הרדוקציה ולכן מיותר (ואפילו קצת מפריע להבנה). כל מה שצריך להוכיח כאן, זה את נכונות הרדוקציה (שלמעשה כעת אינה מוכחת באופן מלא). כל השאר כבר נובע מעצמו ממשפטים שראינו קודם, ואין סיבה לחזור עליהם. ברשותך, אני אשכתב. ‏gran‏ - שיחה 21:44, 28 בינואר 2012 (IST)

תרגיל: הראה איפה ההוכחה קורסת כאשר f אינה מלאה (ספציפית, נניח שההוכחה משתמשת ב־Q כפי שרשמת). שבוע טוב, ‏gran‏ - שיחה 03:40, 29 בינואר 2012 (IST)

לדעתי, f יכולה להתפוצץ עם פטריה גרעינית אם נותנים לה קלט שאינו זוג תיאור מ"ט ומחרוזת, ועדיין יהיה נתן לפתור את בעיית העצירה. אבל גם אם אני טועה, לא נראה לי שנתינת "תרגילים" היא צורת דו-שיח, לפחות לא אחת שבא לי להשתתף בה. Atavory - שיחה 08:44, 29 בינואר 2012 (IST)

חלילה מלפגוע בכבודך. זה היה טיזר שחשבתי שתהנה מפתירתו. הסיבה היא שאם f לא מלאה, לא ניתן להמיר את הקלט, והמכונה לא-עוצרת בשלב הזה, בלי קשר לכל השאר, וזה אמור להרוס את הכל. אבל אולי אני טועה. ‏gran‏ - שיחה 09:25, 29 בינואר 2012 (IST)

ראה כל הוכחה בנושא משפט רייס (נניח של גדי אלכסנדרוביץ' בקישורים החיצוניים). נניח שאתה רוצה לפתור את בעיית העצירה, דהיינו, בהנתן M וx להכריע וכו'. משרשרים מכונה שמריצה את M על x ואז את וכו' וכו', ושואלים האם המכונה המשורשרת בL_S. זהו.

עכשיו איך ההוכחה כתובה כאן עכשיו? היא בגדול די נכונה, אך כתובה כך:

"

נגדיר את הרדוקציה $f(\langle M\rangle ,x)=\langle M_{x}\rangle$ באופן הבא.

בהנתן קלט $w$, המ"ט $M_{x}$:

1. מריצה את $M$ על $x$ (ומתעלמת מהתוצאה, אם יש), ואז
2. מריצה את $M_{0}$ על $w$, ומקבלת/דוחה כמותה

(הערה: אם הקלט אינו $(\langle M\rangle ,x)$ פלט הפונקציה f מוגדר בתור מ״ט הדוחה כל קלט (באופן זה השפה של מכונה הפלט הוא $L(M)=\emptyset \notin S$)

כעת נראה ש־f מקיימת את תכונות הרדוקציה כפי שהגדרנו בפרק רדוקציה:

f מלאה

"

אז, להבנתי, מה יש כאן? לוקחים את הבניה ממקודם, דהיינו שרשור שתי המכונות, וקוראים לזה f. כדי להגדיר את תחום ההגדרה של f (לדעתי מיותר לחלוטין), מרחיבים את הגדרת הבניה למקרה שלא נתנו M וx (שזה, תכלס, הדבר היחידי שרוצים לפתור, מפני שזו בעיית העצירה, וכל דבר אחר פשוט לא משנה), ומגדירים מאד במדוייק שהמכונה המשורשרת תהיה משהו שאינו בL_S, וגם שf מלאה (שני הדברים מיותרים).

עוד יותר בעייתי (שוב, לדעתי) - מרוב ההתמקדות המיותרת בf, הקורא המסכן צריך לאגור עוד סימנים עד שברור לו מה בכלל מנסים לפתור:

"

נגדיר את הרדוקציה $f(\langle M\rangle ,x)=\langle M_{x}\rangle$ באופן הבא.

בהנתן קלט $w$, המ"ט $M_{x}$:

"

זה פורמאלית די מוגדר, אבל הקורה המסכן עוד לא יודע בשלב זה מהם M וx, מאיפה הם הגיעו, ולמה הם כאן.

אני לא רואה שום ייתרון לגרסה שעכשיו יחסית לגרסה ששחזרת שהיתה אתמול. Atavory - שיחה 20:31, 29 בינואר 2012 (IST)

הספר בנוי נדבכים נדבכים, ואחרי שהוכחנו שלב – אין צורך להוכיחו שוב. ברור ש"רדוקציה" משמעותה בניית מ״ט וכו'. זה הוסבר בפרק המתאים. לאחר שזה הוגדר, אין שום סיבה להוכיח ישירות ע״י בניית המ״ט עצמן, אלא כל מה שצריך זה להוכיח את 3 תכונות הרדוקציה. שתיים מהן פשוטות (מלאות וברות־חישוב). השלישית היא העיקר.

שים לב שאין שום ייחוד בלהוכיח את רייס ע״י בעיית העצירה. יכולנו לבחור שפה אחרת ולהוכיח רדוקציה ממנה אל $L_{S}$. וכדי להוכיח שקיימת רדוקציה כזו, כל מה שחשוב הוא להראות איך ממירים קלט של הבעיה האחת לקלט של הבעיה השניה. בניית המ״ט אולי תורמת קצת להבנה, אבל אין בה צורך.

פשרה - אולי תוסיף חלונית מידע ש"מזכירה" שמשמעות הרדוקציה f האמורה, היא למעשה בניית מ״ט שקודם מחשבת את f ואח״כ מכריעה את HP ? ‏gran‏ - שיחה 21:45, 29 בינואר 2012 (IST)

אהלן, הפעם תורי לא להבין (ואני באמת פשוט לא מבין). אני מדבר על הגרסה של אתמול, לא גרסה עם Q שמזמן וויתרנו עליה (לגבי חלק מנקודותיך שם הסכמתי). היות שמדובר על ההבדל בין שתי גרסאות: זו של אתמול וזו של היום (ולא אחת אחרת), צריך לדעתי להסתכל על הנקודות המועלות כאן, ולהשוות בין שתי גרסאות אלו.

אתה אומר: לא חייבים להשתמש בבעיית העצירה. זה נכון, אך מופיע בשתי הגרסאות (אז לא הבנתי מה נקודתך). אתה אומר שאין צורך להוכיח ישירות ע"י בניית המ"ט עצמן. שוב, המ"ט היחידה הנבנית בכ"א משתי הגרסאות היא M_x, המכונה המשרשרת (שוב, אין שום הבדל). אתה אומר שלאחר בניית נדבך, אין טעם לבנות אותו שוב. שוב, מסכים, אשמח אם תראה איפה נבנה ביתירות משהו בגרסה מאתמול יחסית לגרסה של היום. בקיצור, פשוט אינני מצליח למצוא משהו דיפרנציאלי בדבריך לגבי שתי הגרסאות.

להבנתי, אני דווקא אומר משהו דיפרנציאלי לגבי שתיהן. הגרסה של היום מציגה את M_x דרך פונקציה f הפועלת על M וx. בשלב זה, הוספת ארבעה סימנים לא מוכרים כאשר לגבי שניים מהם לא ברור בשלב זה של ההוכחה מה מטרתם (זה שמדובר בבעיית העצירה, לא אומר שהמשתמש יודע שההכרעה הולכת להיות דווקא על M הפועלת על x. איך הוא יכול לדעת זאת בשלב זה של ההוכחה?). השלישי, לצערי, נראה מיותר על סף מטעה. אני שוב חוזר על כך שf לא צריכה להיות מלאה בכל הזוגות האפשריים. לאחר שמוותרים על תנאי זה, לא ברור מה הפונקציה f כלל תורמת ייחסית לאמירה שאם רוצים להכריע האם M עוצרת על x, אז כך וכך בונים את M_x.

הגרסה של היום נראית לי משהו שעל פניו נראית יותר מדוייקת, מפני שיש בה יותר סימונים, אבל למעשה היא פחות (היא מגדירה דברים שאין בהם צורך, כמו האם השפה תהיה בL_S אם הקלט איננו זוג מהסוג של מ"ט וקלט).

אגב, זו איננה הנקודה היחידה. נקח לדוגמה את זה שאפשר להוכיח על S או על משלימתה. זה נכון מפני שS לא טריוויאלית שקול לכך שמשלימתה איננה, ובניית מכונה רקורסיבית שאומרת שלשפה יש תכונה שקול לבניית מכונה רקורסיבית שאומרת שלשפה אין תכונה, ושלילת התשובה המתקבלת. זה מה שהיה בגרסה אתמול. איך זה מופיע היום? כך:

$L_{\overline {S}}=\{\langle M\rangle \mid L(M)\in {\overline {S}}\}=\{\langle M\rangle \mid L(M)\notin S\}={\overline {L_{S}}}$

+ אמירה על סגירות R למשלים. כמדומני שבהערת העדכון הוספת שיש כאן ניואנס. שוב, לדעתי, זה רק נראה יותר מדוייק, אבל למעשה זה פחות. בפרט, שלושת הביטויים השמאליים הם תת קבוצה של קידודי מכונות בRE. המשלים לL_S, אם אתה רוצה להיות מאד מדוייק, כולל מחרוזות שאינן כלל תיאור של מ"ט (מה שדווקא בf הקפדת עליו), ושפות שכלל אינן בRE, וכו'.

בקיצור, אני מאד ממליץ לחזור לגרסה של אתמול, שהיא די הליכה לקראת ההוכחה המקורית שלך. כל טוב, Atavory - שיחה 22:27, 29 בינואר 2012 (IST)

עוד הצעה

אהלן,

שמתי את הצעתי בתורת החישוביות/כריעות שפות/משפט רייס/ארגז חול. יש שם מספר התייחסויות להערותיך:

1. ערכתי את סקירתך המקורית בראש הדף כך שתשקף מה מוסבר בכל חלק (מטפל בחוסר הבהירות מקודם לגבי R וRE)
2. הערותיך הקודמות לגבי הוכחת משפט רייס כבר נמצאות בגרסה של אתמול
3. הוספתי את מה שנקרא במקור "משפט רייס המורחב" בצורה מפורשת לראש החלק על מניה רקורסיבית, בנוסף להפניה לתרגיל.

אני שוב רוצה לציין FWIW, IMHO, וכו' - את הערכתי למה שעשית כאן בספר ובדף. הגרסה בארגז החול היא בבירור גרסה של עבודתך, ומשקפת לדעתי את הערותיך. ועם זאת, היא לדעתי הגרסה המתאימה יותר כעת (שוב, במידה רבה בשל תרומותיך לנושא). אני מתקשה לראות על מה יש להתפשר כאן מעבר לזה. כל טוב, Atavory - שיחה 23:54, 29 בינואר 2012 (IST)

אני מקווה שאתה מבין שהדיון הוא ענייני ולא אישי. אני לא משוכנע שכך טוב יותר, אבל גם הצעה זו מהווה הוכחה קבילה, וחבל על המאמץ שאנחנו משקיעים בדיון. עשה כרצונך בהוכחה. אני אוסיף לאחר מכן תיבה שמסבירה שההוכחה שקולה להגדרת f, ואפרט את הניסוח המדוייק. אני חושב שזה פתרון עדיף: גם יכיל הוכחה "רעיונית" שמסבירה את ההגיון, וגם הוכחה "טכנית" שיותר מדייקת בניסוחים.

ההרחבה יכולה לעבור לתרגילים. במשפט עם הסייגים יש כרגע הרבה תקלדות וניסוחים לא ברורים. אני אעבור על זה אחרי שתסיים.

הסכמנו? ‏gran‏ - שיחה 02:47, 30 בינואר 2012 (IST)

אוקיי, נשמע טוב. הדף שלך. כל טוב, Atavory - שיחה 07:55, 30 בינואר 2012 (IST)