|
||||
|
||||
אתה חייב לעשות לך מנהג ולהפסיק לקשקש, מה לעזאזל הקשר לקרוב?! הקומפיילר יודע שאתה לא משתמש במשתנה באותה משמעות שהוא יודע אם האות A נמצאת או לא נמצאת בקוד שכתבת... הוא לא צריך לעשות קירוב כדי לדעת אם האות A נמצאת בטקסט (מחשבים היו במצב רע מאוד אם הם כן היו צריכים...) וזאת בדיוק הבדיקה שהוא עושה כשהוא רואה שהצהרת על משתנה A אבל המשתנה A הזה לא מופיע בשום מקום אחר בקוד שלך... |
|
||||
|
||||
טוב, היה מאוד נחמד ומאוד נהנינו, אבל עכשיו אני צריך לבקש ממך להירגע ולשנות סגנון. |
|
||||
|
||||
קח דוגמה בC: void func(int c) משתמש בc או לא, זה תלוי בקלט. c אמנם מוזכר, אבל לא בהכרח משתמשים בו.
{ printf("%d\n", (getch() == 'a') ? c : 0); } |
|
||||
|
||||
התוכנה משתמשת בו בתגובה לקלט מסוים = התוכנה משתמשת בו, כנראה ששכחת שבעית העצירה שואלת אם התוכנה עוצרת בתגובה לקלט מסוים, לא בתגובה לכל קלט שהוא. |
|
||||
|
||||
זה נכון. רציתי לתת דוגמה נגדית לדוגמה שלך בקשר לקומפיילר שיודע אם משתמשים במשתנה או לא -- הוא באמת לא יכול לדעת. |
|
||||
|
||||
"הקומפיילר יודע שאתה לא משתמש במשתנה באותה משמעות שהוא יודע אם האות A נמצאת או לא נמצאת בקוד שכתבת" הוא יודע אם המתכנת משתמש במשתנה או לא הוא לא מתיימר להגיד לך משהו מעבר. וזה לא אומר שעקרונית הוא לא יכול לדעת אם משתמשים במשתנה, רק שהוא לא מתוחכם מספיק כדי לעשות את זה, אבל אני מניח שאתה טוען שגם עקרונית הוא לא יכול, אז אני מציע לך בתור תרגיל לנסות להוכיח שהוא לא יכול, בהנחה שאסור לתוכנה הנבדקת לקרוא לאלגוריתם שבודק אם היא משתמשת במשתנה. (כי הרי זה מה שמענין אותנו אם אנחנו יכולים למצוא אלגוריתם שיקבע אם היא משתמשת או לא משתמשת במשתנה, לא אכפת לי שאסור לה להשתמש בו, בחיים לא כתבתי תוכנה שהשתמשה בו וגם אין לי כוונה לעשות את זה כשתהיה כזאת...) אז אנא ממך, תוכיח לי, או שאל איזה מרצה בתחום אם לדעתו אפשר להוכיח את זה.. |
|
||||
|
||||
אם מתרגל בקורס בתורת הקומפילציה בטכניון הוא מספיק בר-סמכא בשבילך, נסה לשאול את גדי (כותב המאמר) - זה הקורס שהוא מתרגל בסמסטר זה. אם אתה מעדיף לשאול את המרצה בקורס, אני הכתובת. באופן כללי, התשובה שלי תהיה: "תשאל את גדי, הוא יודע בדיוק על מה הוא מדבר". |
|
||||
|
||||
יופי, בקיצר, לך או לגדי יש הוכחה לזה? |
|
||||
|
||||
אבל אין כאן בכלל מה להוכיח. התוכנית עשויה להשתמש במשתנה, ועשויה לא להשתמש במשתנה, בהתאם לקלט. תשובה שמבוססת על ראיית התוכנית בלבד ללא התחשבות בקלט תהיה שגויה ביחס לחלק מהקלטים, ונכונה בקשר לשאר. זה דומה לשאלה האם השערת הרצף (שהזכרתי במקום אחר בדיון) נכונה או לא נכונה - היא יכולה להיות שניהם, זה תלוי באקסיומות. אם השאלה היא "האם קיים קלט שעליו התוכנית משתמשת במשתנה?" אז בוודאי ש*קיים* אלגוריתם שיכול להכריע את השאלה הזו, אם מניחים שיש חסם על זמן הריצה/הזכרון שבו התוכנית משתמשת. |
|
||||
|
||||
טוב, נחזור לבעיה עצמה, תוכיח לי שאלגוריתם בסגנון של halt(machine m,machine_code u,input x) בלתי אפשרי למימוש.
if m = u return Error illigal input else return true if machine stops on x, false otherwise. |
|
||||
|
||||
אני לא בטוח שאני מבין את התפקיד של u,m כאן. אתה משתמש בהם בצורה מפורשת רק בשורה השנייה. בשורה השלישית אתה מדבר על "machine" - מה זה? זה m? זה u? זה שניהם גם יחד? מה הם מייצגים? |
|
||||
|
||||
טוב סליחה ננסח את זה בדיוק כמו שאתה נסחת (חשבתי שזה היה הניסוח המקורי ולא בדקתי) halt (Machine m,Input I)
if m = I return Error in input else return true if m stops on i, false otherwise |
|
||||
|
||||
ראשית, שים לב שהאלגוריתם הזה לא פותר את בעיית העצירה. קיימים קלטים שעליהם הוא מחזיר פלט שגוי (למעשה, "Error in input" הוא בכלל לא פלט לגיטימי - אנחנו מצפים לקבל "כן" או "לא" כתשובה, ולא שום דבר אחר). שנית, בוא נניח שקיים אלגוריתם כזה. אני אבנה אלגוריתם S שהולך ככה: הוא מקבל קלט שנסמן בתור M1, מגדיר בתור M את הקלט בלי התו האחרון שלו, ומחשב את halt(M,M1) אחרי זה הוא עושה ההפך מהתשובה - אם היא true הוא נכנס ללופ אינסופי, ואחרת הוא עוצר.עכשיו, איך יתנהג S על הקלט S1, כש-S1 הוא הקידוד של S ועוד התו "1" בסוף? |
|
||||
|
||||
ממה התחלנו, אמרנו שאותי מענין אם אפשר לבנות תוכנה שתבדוק אם התוכנה שלי עוצרת על קלט מסוים, נניח שאפשר לבנות תוכנה כזאת במגבלה שאני לא יכול לתת לה בתור קלט את התוכנה עצמה, זה מספיק טוב (למעשה מדהים) בשבילי. אז כשמתיימרים להוכיח לי שאי אפשר לעשות את זה, וההוכחה היא שאם התוכנה שלי היא גם הקלט אז יש בעיות, זה בעיני סתם רמאות זולה - בעצם לא הוכחת שאי אפשר לעשות את מה שבאמת מענין אותי אם אפשר לעשות. לגבי מה ששאלת, לא הבנתי מה הבעיה, מה שיוצא לנו מההגדרה שלך זה S (S + 1) מה הבעיה פה? תהיה בדיקה אםM = S if Halt(S,S+1) loop else halt. S עוצר עלS + 1 ואם כן הוא לא יעצור, ואם לא הוא יעצור..
|
|
||||
|
||||
אה או קי סליחה הבנתי, טוב... אז נשנה את האלגוריתם ל Halt(Machine M,Input I) callingAlgorithm מחזיר את האלגוריתם שקרא לך.
if M = I return Error S = CallingAlgorithm(Halt) S1 = CallintAlgorithmInput(S) while S do if S = M and S1 = I return Error S = CallingAlgorithm(S) end while return true if M stops on I false otherwise |
|
||||
|
||||
העלילה מסתבכת, מה? בקרוב ייכתב כאן קוד בלתי קריא. מה זה "CallingAlgorithm"? לי נראה שאתה חושב כאן במונחים של תכנות, לא של מכונות טיורינג. בפרט, אתה מניח שיש מעין מחסנית קריאות או משהו דומה, ולכן אפשר לדעת מה האלגוריתם שקרא לך. במכונות טיורינג זה לא הולך ככה - האלגוריתם S לא "קורא" לאלגוריתם Halt (אם הוא היה עושה את זה, חלק מהקלט ל-Halt - במובלע - היה משתנה נוסף, שמכיל את זהות האלגוריתם הקורא) - הוא פשוט מבצע אותו. תחשוב על זה כאילו העתיקו את כל הקוד של Halt לתוך S (כמו inline ב-++C). אבל חוץ מכל זה, אני מודה שאני לא ממש מבין את האלגוריתם שאתה מציג. בפרט, מה עושה השורה S = CallingAlgorithm(S) ? זה נראה כאילו אתה מנסה לעלות מעלה במחסנית הקריאות - אבל הרי אין שם כלום (כי אף אחד לא באמת "קורא" ל-S). גם התנאיwhile S do לא ברור לי, הרי S הוא לא משתנה בוליאני. אתה מניח ש-CallingAlgorithm מחזיר 0 כשהוא מגיע לסוף מחסנית הקריאות? אם כן, בכל הלולאה אין טעם, כי היא תעצור אחרי הפעם הראשונה.אז אם לסכם - מה שהאלגוריתם שלך עושה הוא לבדוק במפורש האם התוכנה שנאמר לו לבדוק היא גם זו שקראה לו (אחרי שקיבלה את הקלט שעליו הוא אמור לבדוק אותה). זה טוב ויפה אם הפונקציות הדמיוניות CallingAlgorithm ו-CallingAlgorithmInput קיימות. אולי יש לך הצעה למימוש שלהן, בהתחשב בעובדה שאין מחסנית קריאות? ------ השלב הבא שלך כנראה יהיה זה: תגיד "אוקיי, אז אני מעוניין שתוכיח לי שלא קיים אלגוריתם שמקבל: א) את המכונה שקראה לו. ב) את הקלט שעליו המכונה הזו נקראה. ג) את המכונה שהוא צריך לבדוק. ד) את הקלט שעליו צריך לבדוק את המכונה הזו". אז תיכנס לתמונה בעיה נוספת - שני הקלטים הראשונים, כאמור, יכולים להיות מועברים רק על ידי מכונת הטיורינג הקוראת (הם לא נוצרים בצורה אוטומטית). את המכונה הזו אף אחד לא מכריח להעביר את הקלטים ש*לדעת Halt* צריכים להיות שם - היא יכולה להעביר מה שבא לה. מכיוון ש-Halt לא יכול לדעת אם שיקרו לו או לא, הוא תמיד חייב לענות כאילו לא שיקרו לו, ולכן כל הבדיקה לא אפקטיבית. |
|
||||
|
||||
זאת היתה הפשטה (פסוודו קוד) אם תרצה אכתוב קוד יותר מדויק, אין בעיה לעשות את זה, אבל זאת לא הפואנטה, הפואנטה היא שמחשב אמיתי כן יכול לעבור על כל הפונקציות שקראו לפונקציה HALT עד לפונקציה הראשית (main) וככה לבדוק שאתה לא מנסה לרמות אותו עם הטריק הזה. אז מה אתה אומר לי בעצם, שעל מחשב כן אפשר לפתור את הבעיה הזאת אבל על מכונת טיורינג לא? נדמה לי אבל שכתבת במאמר (או שקראתי במקום אחר) שכל דבר שמחשב יכול לעשות גם מכונת טיורינג יכולה לעשות (לא שזה עקרוני לי כי מה שמענין זה אם מחשב יכול לפתור את הבעיה..) |
|
||||
|
||||
כשאתה עובר לדיון על תוכנות שרצות על מחשב ספציפי (עם מערכת הפעלה ספציפית, שפת מכונה ספציפית ושפת על ספציפית) אתה כבר לא מדבר על בעיית העצירה. אתה מדבר על השאלה האם ניתן לבדוק תת קבוצה קטנה למדי של התוכניות האפשריות (בפרט - קבוצת כל התוכניות שמקבלות כקלט *גם* את התוכנית שקראה להן - שזה קלט די גדול). ועדיין, גם בתת הקבוצה הזו, התוכנית שלך לא יכולה להתקיים כי אפשר לרמות אותה (על ידי העתקת הקוד), אבל כפי שניסיתי לומר קודם, על מחשבים ספציפיים בכל מקרה אפשר להכריע את בעיית העצירה, כי יש חסם על כמות הזיכרון שבו יכולה להשתמש כל תוכנית (כלומר, שוב, אנו עוסקים בקבוצה קטנה יחסית של תוכניות). לכן אין ממש טעם בכל הדיון הזה. אם כל מה שמעניין אותך הוא תוכניות מחשב "אמיתיות", הדיון הזה לא בשבילך. כדי שהוא יעניין אותך, אולי כדאי לעבור לבעייה של Wang tiling - במקרה שלה הרבה יותר ברור עד כמה לומר "טוב, לא נשאל על ריצוף אינסופי אלא על ריצוף של שטח סופי" מוציא את העוקץ מכל העניין. |
|
||||
|
||||
תראה אתה זה שטענת במאמר שאף מחשב שקיים או שיהיה קיים אי פעם לא יוכל לפתור את הבעיה הזאת, כלומר דברת לא סתם על מחשב ספציפי, אלא על האמאמא של המחשבים הספציפיים (כל מחשב ספציפי שאי פעם יתקיים) אז הבעיה היא ברעש שאתה עושה, שמטעה אנשים (אפילו כאלה שמתכנתים לפרנסתם שלא לדבר על סתם תמימים..) שאתה באמת מוכיח כאן מגבלה של המחשבים שהם מכירים בעולם (או שיכירו בעתיד) ולא סתם מתפלסף.. |
|
||||
|
||||
מה שטענתי אכן נכון; אף מחשב שקיים או שיהיה לא יכול לפתור את הבעיה הזו. הוא *כן* יכול לפתור בעיות שדומות לה אבל פשוטות יותר, כמו זו שהצגת. מה שכן, אני מתחיל להבין למה דוד הראל בחר להציג תחילה את הרעיון של Wang tiling. זו דוגמה נאה לבעיה שמעניינת גם בצורתה ה"אינסופית" - אבל אני מניח שגם כאן מי שרק מתעניין בתכנות לא יתעניין בה ויראה בה "התפלספות". |
|
||||
|
||||
תראה, אני מתענין במחשבים, במה שהם עקרונית יכולים לחשב ומה שלא ובכמה זמן הם יכולים/יוכלו לחשב בעתיד את מה שהם יכולים, אני מניח שזה מה שמענין כמעט כל אחד מאלו שנכנסו לקרוא את המאמר שלך. אני מניח שגם ברור לכל אחד שנכנס לקרוא את המאמר שלך (גם אם הוא לא ממש חשב על זה קודם), שיש כל מיני דברים שמחשב עקרונית לא יכול לעשות, נניח לפתור בעיות כמו מה קדם למה הביצה או התרנגולת, או אם מישהו שאומר שהוא תמיד משקר משקר וכו, אבל לא היית בא וכותב מאמר: "המחשב לא כל יכול, עקרונית הוא לא יכול להגיד לך אם מישהו שטוען שהוא תמיד משקר משקר, כי התגובה היחידה שהיית מקבל היא, וואלה.. ובעצם מה שכתבת פה במאמר זה בדיוק אותו דבר רק שערפלת את זה קצת ועטפת את זה בהרבה רעש כדי לקבל תגובות נוספות מעבר ל"וואלה.." וזה בעיני לא הכי יפה.. |
|
||||
|
||||
יש הבדל בין בעיות כמו ''מי קדם למה, הביצה או התרנגולת'' שלא ניתן לענות עליהן כי אין להן תשובה, ובין בעיות שדווקא ברור לנו שיש עליהן תשובה חד משמעית ומוגדרת היטב, אלא שפשוט אין לנו דרך למצוא אותה. לשאר דברייך אני חושב שלא אני זה שצריך להתייחס. אם אתה מתעניין בעיקר בצד המעשי, אני משער שכדאי לך להמתין עד אשר (ואם) יפורסם המאמר שעוסק בהבדל שבין ניתן לחישוב יעיל, ובין לא ניתן לחישוב יעיל - שם הגישה הננקטת היא דווקא גישת בית הלל (גם דברים שמעשית יהיה מאוד קשה לחשב עשויים להיחשב ל''קלים לחישוב''). |
|
||||
|
||||
אין הבדל, ברור שאין תשובה לשאלה אם תוכנה עוצרת או לא עוצרת כשאתה מרשה לה לעצור או לא לעצור בהתאם לתשובה... |
|
||||
|
||||
כאן הטעות שלך. יש תשובה לשאלה, אלא שהתוכנה לא מסוגלת לחשב אותה בעצמה. |
|
||||
|
||||
זה לא מדויק, התוכנה יודעת לחשב אותה היא פשוט אומרת ההיפך ממה שקורה.. (אז אתה יכול לקרוא לזה חישוב ברברס..) |
|
||||
|
||||
לא. מכיוון שההוכחה מראה שאין Q שפותר את הבעיה, התוכנה לא יודעת לחשב את זה. זכור שיצאנו מתוך גישה של הנחה בשלילה. |
|
||||
|
||||
אז הגענו לשלב שבו הראנו שאם יש Q כזה ואנחנו מרשים לתוכנה לשאול את זה על עצמה אז יש אופציה ליצור "באג" שבו התוכנה תגיד שהיא לא עוצרת כשהיא כן עוצרת, ושהיא עוצרת כשהיא לא עוצרת. הוכחנו גם שאין אפשרות לתקן את הבאג (שיווצר רק כשישאלו את התוכנה על עצמה ולא כשישאלו אותה על אחרות) האופציה היחידה תהיה להוציא הודעת שגיאה על קלט לא חוקי, דבר אחד לא הוכחנו וזה שאי אפשר לבנות את Q. |
|
||||
|
||||
זה לא "באג". זו סתירה, שמראה ש-Q פשוט לא עושה את מה שהנחנו שהיא עושה. אני חושב שהדיון הזה מיצה את עצמו - אין לי חשק להתחיל דיון 1571 חדש. |
|
||||
|
||||
או, הללויה. באמת תהיתי למה אתה עד פעם מתוכח עם טרחן שלא מבין טענות לפני שהוא מתוכח איתן. המר בחור לא מבין הוכחה פשוטה של reduction ad absurdum וחושב שמדובר בטריקים "דבילים" ולא מעניינים. זה הרגע לשלוח אותו לקורס בלוגיקה בסיסית, לא לנהל איתו דיון. |
|
||||
|
||||
הרבה יותר קל לא לנהל דיון מלחשוב שאולי משהו דפוק אצלך |
|
||||
|
||||
דיון ניתן לא לנהל גם ע''י כתיבת המון מלל. |
|
||||
|
||||
בקורס ללוגיקה כבר הייתי, תודה. גם הוכחות כאלו ראיתי לא מעט, ההבדל הוא שהן אף פעם לא טענו שמשתמע מהן יותר ממה שהוכיחו מהן. לצערי אתה לא הבנת כל כך את הדיון, בעצם היתה פחות או יותר הסכמה שלא ממש מצליחים להוכיח את מה שמשתמע (גם עבור אנשים כמוך מסתבר), אלא משהו שולי בהרבה מבחינה מעשית (ייתכן שמשמעותי מאוד מבחינה פילוסופית, בעיני לא אבל אני לא פילוסוף). מכיוון שהוסכם שמדובר בהתפלספות ניסיתי בסוף קצת להתפלסף איתה בחזרה כדי להראות שלמקל יש 2 קצוות, אבל אני לא מתכוון לגרור אנשים לדיונים שאין להם ענין בהם (אפילו אם רגע לפני זה הם טענו שזה בעיקר מה שמענין אותם ולא הקטע המעשי) אז נראה שנפסיק כאן. |
|
||||
|
||||
לא הוסכם שמדובר ב''התפלספות''. העולם לא מתחלק לשני סוגי בחינות - מעשית ו''פילוסופית''. |
|
||||
|
||||
נשגב מבינתי איפה הוכחת שבדיקות לא יכולות לעקוף את הטריק, להיפך אמרת שאפשר לפתור את הבעיה ככה רק שזאת לא אותה הבעיה אלא בעיה יותר קלה, אז בסדר, אותי מענינת הבעיה המעשית של אם תוכנה תוכל לבדוק לי את התוכנה שלי ולראות אם היא הולכת להתקע ואותך כנראה מענינים יותר פרדוקסים לוגיים בסגנון השקרן, כנראה בגלל זה אתה מצליח להסכים ולא להסכים בעת ובעונה אחת לפי משב הרוח. ודרך אגב, אם זכור לי נכון מתמטיקאים עשו אותו דבר עם תורת הקבוצות אחרי הפרדוקס של ראסל (אף אחד לא יגרש אותם מגן עדן, אבל כשמדובר בענין מעשי אין להם כנראה בעיה להתיימר שפתחו את שערי הגהנום) בקיצר, כל אחד ומה שעושה לו טוב.. |
|
||||
|
||||
נתת לי כרגע מוטיבציה לכתוב מאמר גם על הנושא הזה (אבל כאן כבר באמת עדיף שמישהו מהמתמטיקאים של האייל יקדים אותי). אגב, יש לי הרגשה שאני כבר מכיר אותך מאיפה שהוא... |
|
||||
|
||||
אתה צודק, אבל זה יותר שאני מכיר אותך משאתה אותי |
|
||||
|
||||
יש כמה דברים בחיים שחשובים יותר מנכונות טענות, דעות או אי הסכמה. |
|
||||
|
||||
החלק הראשון של הדיון דווקא היה מעניין לטעמי - זה לא לגמרי טריוויאלי להבין למה אי אפשר לעקוף את הטריק של S על ידי בדיקות כמו שהוא הציע. אבל זה מיצה את עצמו. |
|
||||
|
||||
שאלות כמו הקשר בין מדעי המחשב לבין תכנות מעשי הן אכן שאלות מעניינות (אותי לפחות). לנהל אותן ע"י התחרבשויות רטוריות, רעש, צלצולים והתלהמויות לא נחוצות כמו "ההוכחה הזאת פשוט דבילית" או "אתה חייב לעשות לך מנהג ולהפסיק לקשקש" זה כבר סיפור אחר ואלה הדגלים הראשונים שמציינים שבעצם מדברים עם טרחן. הדגלים הנוספים הם שמתקבל הרושם שהוא לא ממש סגור על מה הוא כן מנסה לטעון. יבוא התוהה ויטען את הטענות *הפשוטות* שלו בצורה קצרה ומסודרת (בלי רטוריקה, רעשים או סתם בוטות חסרת הצדקה) ואפשר יהיה להמשיך משם. הלהט הריגשי בדיון בו ניתן לברר יחדיו אם טענה היא נכונה, לא נכונה או שלא ניתן לענות עליה (כרגע או בכלל), הוא מאוד מוזר בעיני. |
|
||||
|
||||
הסיבה ללהט הרגשי הוא ששמעתי על ה''הוכחה'' הזאת לפני שראיתי אותה והדבר הזה עשה עלי רושם מאוד חזק וגרם לי לחשוב הרבה על המשמעויות שלו וגם להתלהב מאוד מהעובדה שאפשר להוכיח כזה דבר (כמו שחשבתי שהוכיחו) כגודל הציפיה כך גם גודל האכזבה שהיתה לי כשלמדתי אותה, למרות שעברו כמה שנים מאז, התחושה המאוד חזקה שהיתה לי אז, תחושה שרימו אותי, חוזרת כל פעם שאני שומע עליה שוב ולכן הרגשיות שבה אני מנהל את הדיון עליה. |
|
||||
|
||||
אז נשים את תחושות העלבון והרגשות רגע בצד, אם אפשר. בקצרה, בפשטות ובדיוק, מה אתה טוען? |
|
||||
|
||||
כבר כתבתי, הבעיה היא אם אפשר למצוא אלגוריתם שיגיד אם אלגוריתם אחר עוצר על קלט מסוים, ההוכחה של טיורינג אומרת שלא מכיוון שאם האלגוריתם הזה יקבל כקלט את עצמו זה ייצור פרדוקס, אז אני אומר, או קי אז אסור לו לקבל את עצמו כקלט. עכשיו אפשר למצוא אלגוריתם כזה? מה שמענין באמת זה אם אפשר למצוא אלגוריתם, וההתחכמויות של אבל אם הוא יקבל את עצמו כקלט יהיה פרדוקס פחות מענינות. וכמו שנזכרתי לא מזמן, זה די דומה לפרדוקס ראסל, אחרי שמתמטיקאים שמעו עליו הם יכלו לזרוק את כל תורת הקבוצות כי היא יצרה פרדוקסים או להחליט שקבוצת ראסל היא קבוצה לא חוקית, נחש מה הם החליטו? |
|
||||
|
||||
רצית - קיבלת. האלגוריתמים שלי מכיל משוואה דיופונטית פולינומיאלית ומחפש לה פיתרון בטבעיים ע''י השיטה המתוחכמת של ניחוש לא סדור. יכול להיות שימצא פתרון, יכול להיות שלא, בשום שלב לא ניתן להגיד שלא קיים פתרון (כי יש עוד מספרים שלא ניסינו). אם קיים אלגוריתם המסוגל לקבוע האם התוכנה עוצרת, אזי הוא פתר את השאלה האם קיים פתרון בטבעיים עבור המשוואה הנתונה, מה שסותר הוכחה הרבה יותר ''מתמטית'' מבחינתך (כבר קישרו אליה בדיון הזה), הבעיה העשירית של הילברט. |
|
||||
|
||||
הבעיה האהובה עלי היא וריאציה על Wang tiling - נניח שיש לנו אוסף כלשהו של אבני כמו-טטריס (כלומר, כמו האבנים שיש בטטריס אבל יכולות להיות מכל גודל שהוא, לא רק 4), האם ניתן לרצף את המישור כולו באמצעות עותקים של איברים מהאוסף? מתברר שגם אלגוריתם כללי לפתרון הבעיה הזו לא קיים. (הרחבה על מה זה לעזאזל "אבן כמו-טטריס" - Polyomino [Wikipedia]) |
|
||||
|
||||
במבט ראשון נדמה לי שאפשר לחלק את הבעיה לשני חלקים: שיטה ראשונה לריצוף המישור - צור צורה הניתנת לגיבוש 1 באמצעות אבנים מהאוסף. אני מניח שבהינתן אוסף סופי של צורות אפשר להסיק האם קיימת צורה כזו (רק מניח, אין לי באמת את הכלים המתמטיים להתמודד עם הבעיה). אבל בעצם מי מבטיח לי שצורה אחת מספיקה, אולי דרושות כמה צורות כדי למלא את כל החללים (כמו כדורגל) ? היות ובניגוד לצורה הראשונה אנחנו לא מחפשים מינימום מחזורי, אין שום סיבה לשים מגבלה על הגודל, מה שגורם לי לחפש מחזור שיכול להיות אינסופי (זה עלול לקחת קצת זמן). שיטה שניה - מצא שיטה (או אולי לפעמים אפילו אין שיטה מסודרת) להמשיך להרכיב עוד ועוד צורות בלי רווחים עד אינסוף. אני מניח שכאן לב הבעיה. אתה יכול לקשר לסקיצה של ההוכחה ? 1 שאפשר להמשיך אותה מכל צדדיה ביחידות חוזרניות מבלי להשאיר רווחים. [אילו היו חמש דקות של נסיון להתמודד עם בעיה שאין לי את הכלים להתמודד איתה] |
|
||||
|
||||
אני לא בטוח מה אתה מנסה לעשות - לי זה נראה כאילו אתה מנסה דווקא לפתור את הבעיה. אם אתה מנסה להוכיח שהיא לא פתירה דרך גישת "בואו ננסה לפתור ונראה איפה אנחנו נתקעים", זו לא הדרך הנכונה. להוכיח שאין אלגוריתם למציאת ריצוף על ידי אבני "כמו-טטריס" זה לא כל כך קשה אם כבר יש לך הוכחה שאין ריצוף על ידי Wang tiling - פשוט עושים רדוקציה (כלומר, מראים דרך לתרגם בעיית ריצוף עם Wang tiles לבעיית ריצוף עם "כמו-טטריס"). זה תרגיל נחמד לחשוב איך אפשר לעשות את זה - ואני בטוח שיש כמה דרכים (הדרך שאני חשבתי עליה טיפה שונה מהדרך שבה הוכיחו את זה לראשונה, אבל בשורה התחתונה זה אותו הדבר). אני לא מכיר מקום באינטרנט שאפשר לראות בו את ההוכחה שאי אפשר להכריע את בעיית הריצוף עם Wang tile. ההוכחה המקורית היא ב: Berger, R. (1966). "The undecidability of the domino problem", Memoirs Amer. Math. Soc. 66(1966). והרעיון הוא רדוקציה מבעיית הכרעה במכונות טיורינג (אם איני טועה, ממש מבעיית העצירה עצמה). אם היא זמינה לך, אתה יכול גם להעיף מבט בחוברת של קורס החישוביות של הטכניון, שנכתבה על ידי עודד גולדרייך - הוא מדגים שם משהו כמעט זהה.
|
|
||||
|
||||
נדמה לי שהם מרחיקים טיפה מעבר לבעיה שהגדרת, אבל העקרון דומה. |
|
||||
|
||||
ואולי יהיה לך אלגוריתם שידע להגיד כן/לא בכל מקרה שניתן לכתוב אלגוריתם, ו"אני לא יכול לדעת" במקרים האחרים? |
|
||||
|
||||
תרגום טענת התוהה: קיימת מ"ט H כך שבהניתן כל קידוד של מ"ט <M> (כך ש- M שונה מ-H) וקלט K, אז H מכריעה אם M עוצרת על K. זו הטענה? |
|
||||
|
||||
הניסוח שלך יצא לא לגמרי מדויק, תזכר בניסוח המקורי (הקלט הוא המכונה M) בכל מקרה, לא טענתי שהיא קיימת, כל מה שטענתי זה שההוכחה שהובאה במאמר, לא מוכיחה שהיא לא קיימת. ברור כמו שאמרו פה שמכונה שתוכל לעשות את זה אבסולוטית (וגם להגיד מתי אי אפשר לדעת, בעקבות ההערה של קהלת) תהיה בעצם סוג של גאון מתמטי, אז אני באמת בספק אם אפשר (מעשית) לנסח אלגוריתם שבעצם יבטא את מהות החשיבה המתמטית. למרות שזה מענין תאורטית, וגם מעשית כמה אפשר להתקרב לזה. |
|
||||
|
||||
אאל''ט, הניסוח שלי, בניגוד לאלה שלך, הוא מדויק וחד משמעי. אתה אולי מתכוון שלא בדיוק לכך התכוונת. נסח בבקשה בשפה הנ''ל את הטענה שלך, כך שהיא תהיה טענה מדויקת ואז נמשיך משם. |
|
||||
|
||||
באיזה שפה אתה רוצה שאני אנסח לך את המילים ההוכחה שמופיעה במאמר לא מוכיחה שאלגוריתם לא קיים? (נתתי פסוודו קוד די מדויק של האלגוריתם שאליו אני מתכוון, דפדף קצת למעלה) |
|
||||
|
||||
בשפה חד משמעית, בדיוק כמו שאני ניסחתי טענה. זה לא קשה, זה פשוט עלול לעזור לנו להחליט אם מה שאתה טוען הוא נכון או לא ולכן אתה נזהר. ''די מדויק'' (שזה אותו דבר כמו ''לא מדויק'') זה לא מספיק בשביל לנהל דיון בנושא. תקעת את הדגל השדמי השלישי והאחרון (יצירת לולאה אינסופית בדיון ע''י הפניה לתגובה קודמת שכתבת ושאליה כבר התיחסו, במקום לענות במשפט אחד תשובה פשוטה ומדויקת לבקשה פשוטה ומדויקת). |
|
||||
|
||||
1) הפרובוקציה. שלב גיוס הקהל: האביר שמעיז למוטט את מגדל הקלפים. פתח את הדיון בהכרזה בומבסטית ומתלהמת (רצוי עם מילה מזלזלת אחת או יותר) לגבי נכונות/דיוק טענה מתמטית שהוכחה כנכונה. ככל שהטענה היא בסיסית יותר/מפרסמת יותר בתחום ונשען עליה עולם ומלואו של הוכחות יפות נוספות, הרי זה משובח. עשינו רעש, יצרנו את תשומת הלב, אפשר לעבור לשלב השני. 2) ריקוד השדים. שלב ההתחרבשויות, ההתעקשויות, גסות הרוח והתיקונים העצמיים הבלתי נגמרים. הדלק שמניע את הטרחן הוא "הרגשה" או "תחושת בטן" שמשהו מאוד בסיסי לא בסדר. הכתיבה האינסופית היא קתרזיס לרגשות ולא מסע אינטלקטואלי/רציונלי. אין לו באמת טענה מסודרת ומדויקת של מה שהוא רוצה להגיד. הקהל שהוא גייס בשלב הראשון מנסה לברר מולו מה בדיוק הוא אומר והטרחן מתקן את טענותיו שוב ושוב (שינוי דרסטי שלהן זה גם בסדר) משום שאין לו ממש טענה אלא "תחושת בטן" שהוא מנסה לתקשר אותה לצד השני. בשלב זה יש המון תיסכולים של שני הצדדים בחוסר היכולת לתקשר והרבה רעש לבן שלא קשור לנושא. מי שלמד קורס בסיסי בחישוביות ולוגיקה פורמלית, יש לו את כל הכלים לנסח בדיוק את הטענות שיש לו בתחום. ההמנעות משימוש בשפה חד-משמעית לא נובעת בד"כ מחוסר הבנה או חוסר ידע, אלא מהצורך להשאיר את השדים של שלב 2 חיים ובועטים למשך זמן ארוך ככל שניתן. כדי לחפש את הדיון לדיון מדויק, משתמשים בהגדרות לא מוסכמות או דו משמעיות והרבה סימנים שנותנים תחושה של פסאודו-פורמליסטיקה. 3) ה-LOOP. הרעבת השדים וסגירת המעגל. אם מנסים לנטרל את הרעש הלבן, להמנע מהמלכודת שהיא הרטוריקה והשפה הטבעית ולתקשר רק ברמת הטענות החד משמעיות שמשתמשות במושגים החד משמעיים בתחום, מקבלים מייד הפניות לתגובות קודמות בדיון הארוך, במקום תשובה קצרה וחד משמעית. |
|
||||
|
||||
אפשר לצאת מהשאלה של התוהה ולהגיע לשאלה "מעניינת". למשל, נניח שאנו מסתכלים על קבוצת כל המ"ט הקיימות ועל כל הקלטים שאורכם קטן מאורך נתון כלשהו (X תווים). האם אז קיים אלגוריתם שפותר את בעיית העצירה? (שימו לב שלא הגבלתי את אורך התכנית אלא את אורך הקלט). הסיבה שהשאלה הזאת נראית מעניינת בעיני היא שאז באמת ההוכחה של טיורינג לא עובדת (נראה לי) כי הקלט לא יכול להיות זהה או שקול לתוכנה. |
|
||||
|
||||
אפשר להראות משהו הרבה יותר חזק: אפילו לגבי הקלט 0 בלבד אי אפשר להכריע באופן כללי אם M עוצרת עליו או לא. למה? בוא נניח שאפשר (יש אלגוריתם Q שעושה את זה), אז אני אראה לך איך לפתור את בעיית העצירה. אתה נותן לי M וקלט x, ואני בונה מכונה חדשה, M_x, שמה שהיא עושה הוא זה: היא *מתעלמת* מהקלט שלה, ובמקום זה כותבת את x על סרט הקלט, חוזרת לתחילתו, ומכאן ואילך מתנהגת כמו M. כלומר, M_x היא פשוט דרך להריץ את M על x בלי ש-x יתקבל כקלט. עכשיו, ברור ש-M_x עוצרת על 0 (או כל קלט אחר) אם ורק אם M עוצרת על x. אז פשוט נחזיר את התשובה ש-Q מחזיר - פתרנו את בעית העצירה. |
|
||||
|
||||
זה רעיון מעניין, אם אתה יכול להמשיך איתו. לא סתם החליטו שקבוצת ראסל היא לא-חוקית, אלא החליפו את הגדרת הקבוצה: לא עוד "אוסף של איברים", אלא הגדרה מפורטת של צרמלו-פרנקל מה זה קבוצה ומה זה לא. אתה יכול למצוא הגדרה אלטרנטיבית ומצומצמת יותר ממכונת-טיורינג לתוכנה? |
|
||||
|
||||
לא חסרות כאלו; יש המוני סוגים שונים ומשונים של מכונות טיורינג עם מגבלות עליהן. מגבלה שכבר ציינתי לא מעט בדיון היא מגבלה על הזיכרון; אם עבור מכונת טיורינג, הזיכרון המקסימלי שהיא משתמשת בו בריצה על קלט הוא פונקציה (ניתנת לחישוב) של גודל הקלט, אפשר לפתור את בעיית העצירה עבור המכונה הזו. |
|
||||
|
||||
הבעיה שהצגתי קודם (חיפוש פתרון למשוואה) משתמשת בכמות סופית של זיכרון (אין צורך לזכור פתרונות קודמים, פחות יעיל אבל עדין עובד), איך מיישבים את הסתירה ? ראוי לציין שהמכונה שלי משתמשת ביכולת להגריל מספרים אקראיים, תכונה שלא באמת קיימת במ"ט (בעצם אפשר לראות בזה הוכחה לכך שמ"ט לעולם לא תוכל להגריל מספרים אקראיים) |
|
||||
|
||||
בעצם טעיתי. הגבלה על גודל הזיכרון מגבילה את גודל המספר המנוחש. |
|
||||
|
||||
כבר ענית היטב לעצמך. רק הערה קטנה: לא קשה להוכיח שגם מכונת טיורינג *אי דטרמיניסטית* (מושג שעליו ארחיב, אם בכלל, במאמר המשך למאמר ההמשך) לא חזקה יותר ממכונת טיורינג רגילה - ואי דטרמיניזם, מבחינה רעיונית, הוא יותר חזק מאקראיות "סתם" (אם כי זה לא כל כך פשוט - במכונות אקראיות מרשים לפעמים למכונה לטעות - ובפרט, יש מכונה אקראית שפותרת את בעיית העצירה בהסתברות 1/2). |
|
||||
|
||||
מחכה בקוצר רוח. |
|
||||
|
||||
עד שכתבת "למרות שעברו כמה שנים מאז" חשבתי שאתה בן שמונה עשרה וקצת, בוגר מצטיין של קורס תכנות, בעל נסיון ביישום אי אילו אלגוריתמים לא טריויאליים (כולל quicksort עם הקצאה דינמית של זכרון, יה, יה) ומרגיש שהעולם בקצות אצבעותיו. חשבתי אפילו לתת לך עצה קטנה ממרום גילי, בקשר לכותרות מסוג "ההוכחה הזאת היא דבילית": כאשר ההוכחה מקובלת על המון אנשים בלתי דבילים בעליל, הסיכוי שכולם טועים באופן טריויאלי בלי לשים לב למה שנראה לך ברור מאליו - הסיכוי הזה לא גדול במיוחד. זה לא אומר, חלילה, שצריך לקבל את דבריהם בלי הרהור וערעור, אבל כדאי לצאת מההנחה ש*אתה* לא מבין כאן משהו יסודי, לא שכל האחרים דבילים, ולנסות לברר מה באמת הולך כאן. כאשר בוחרים בסגנון שלך, רוב הסיכויים הם שיתברר שבדיון הזה הדביליות היא לא בהוכחה. אבל מה? מסתבר שאתה לא כל-כך צעיר, כך שאם לא למדת את זה עד היום כנראה גם לא תלמד. בהצלחה בסטארט-אפ. |
|
||||
|
||||
התכוונת בהצלחה בסטנד-אפ. |
|
||||
|
||||
לא הבנתי. ממה התאכזבת? |
|
||||
|
||||
הנה שאלה ש(עוד) לא מיצתה את עצמה: הוכח שאי אפשר להכריע את בעית העצירה בקבוצת כל מ"ט שלא מקבלות קלט. |
|
||||
|
||||
זה דומה למשהו שכבר אמרתי במקום אחר: נניח שאנחנו רוצים לפתור את בעית העצירה עבור מכונה M וקלט x, ויש לנו Q שמכריע אותה עבור מכונות שלא מקבלות קלט. אני בונה מכונה Mx שלא מקבלת קלט ומה שהיא עושה הוא לכתוב על הסרט שלה את x ואז להריץ את M, ומעביר אותה ל-Q. אבל הרדוקציה הפרטנית הזו די מיותרת, כי משפט רייס (שלא הוזכר במאמר) כולל גם את המקרה הזה. |
|
||||
|
||||
תמיד יש את הבעיה הזו כשמשלימים דיונים עם עשרות+ תגובות: או שתגיב ותחרמופף או שתקרא קודם את הכל ותשכח על מה רצית להגיב. |
|
||||
|
||||
אבל התוהה, "אם מישהו שטוען שהוא תמיד משקר משקר", מקרה הידוע בשם פרדוקס השקרן, זהו לב ההוכחה של אי היכולת לפתור את בעית העצירה. התוכנית שגדי הציג עוצרת (משקרת) אם היא לא עוצרת (אומרת אמת) ולהפך. האם נסכים לסכם גם כאן בוואלה? |
|
||||
|
||||
מקריאת תגובותיך נראה לי שאינך עומד על ההבדל המהותי בין מדעי המחשב לבין תיכנות מעשי על כל הישומים המסחריים שלו. כמו שמישהו (פון ניומן ?) פעם ניסח זאת - "מחשבים קשורים למדעי המחשב כמו שטלסקופ קשור לאסטרונומיה". |
|
||||
|
||||
אדסחר דייקסטרה: אדסחר דייקסטרה [ויקיפדיה] |
|
||||
|
||||
|
||||
|
||||
יש לי אתגר בשבילך, שמראה כמה בעיית העצירה קשה. כתוב תוכנית שבודקת האם האלגוריתם הבא עוצר. אלגוריתם יאללה_בלאגן א. N=4 ב. בדוק האם N הוא סכום של שני מספרים ראשוניים. ג. אם כן: ג1. N=N+2 ג2. חזור לשלב ב. ד. אם לא: הדפס "השערת גולבך שגויה" וסיים. שים לב, יאללה_באלגן בודק את השערת גולדבך (כל מס' זוגי גדול מ 2 הוא סכום של שני ראשוניים). אם ההשערה נכונה (ואף אחד לא הצליח עדיין להוכיח או להפריך את זה), יאללה_באלגן לעולם לא יעצור. כך, שאם אתה מצליח להריץ את התוכנית שלך ו*לקבל תשובה נכונה*, פתרת את אחת הבעיות הקשות במתמטיקה. כל מה שנשאר הוא להראות את התשובה למתמטיקאי, ואז אתה תהיה אדם עשיר ומפורסם (בהנתן, כמובן, שלא תמות בשיבה טובה לפני שהתוכנית שלך תחזיר תשובה). האם אתה מרים את הכפפה? |
|
||||
|
||||
זה אמנם מראה שבעיית העצירה קשה, אבל "תוהה" לא חלק על זה, אם אני מבין נכון: הוא רק חלק על זה שהיא בלתי פתירה, או אולי אפילו רק על ההוכחות לכך שהובאו כאן. זה אגב מעלה שאלה מעניינת (בעיניי). האם במדעי המחשב מוצאים לפעמים הוכחות לא-קונסטרוקטיביות לקיומם של אלגוריתמים? |
|
||||
|
||||
התוהה הביא אלגוריתם שפותר את בעיית העצירה. אם כך, זה ממש בקטנה בשבילו להביא אלגוריתם שבודק מקרה פרטי מאד: האם יאללה_בלאגן עוצר. בתור התחלה, הוא יכול להביא את האלגוריתם הכללי שלו. נראה לי שאולי ע"י מקרה פרטי, יהיה אפשר להמחיש לתוהה היכן הטעות שלו. |
|
||||
|
||||
הוא לא הביא אלגוריתם כזה, אלא רק הציע שיטת ''שיפוץ'' לאלגוריתם אפשרי. יש בצורת הניסוח שלו בעיות פורמליות, אבל הרעיון הבסיסי דווקא לגיטימי (הוכחנו שאי אפשר לפתור את בעיית העצירה - הטוען תהה האם ניתן לפתור אותה עבור כל קלט שאינו ''המכונה הקוראת, הקלט של המכונה הקוראת'') |
|
||||
|
||||
אני מקבל את התיקון. אבל למה שלא יתחיל במקרה הפרטי שלי? אם הוא לא רוצה להיות עשיר ומפורסם אני מוכן לקחת את העונש הזה על עצמי. שיעשה את זה רק בשביל האתגר. |
|
||||
|
||||
אם הבנת למה הוא התכוון בדיוק, אתה מוכן לנסח במקומו את הטענה עם "התיקונים"? (אותך אני מבין) מהי בדיוק "בעיית העצירה תג" עליה אנו מדברים? האם לא קל לבצע ממנה רדוקציה אל בעיית העצירה ה"רגילה"? |
|
||||
|
||||
יותר משזו בעיה, זה "אתגר" - תוכיח לי שלא קיים אלגוריתם Q שפותר את בעית העצירה עם הקלטים M, x תחת ההנחה שאם אלגוריתם S כלשהו משתמש ב-Q הוא מעביר לו כקלט גם את המידע על עצמו ועל הקלט שהוא עצמו קיבל. את כל זה אי אפשר לנסח בצורה משביעת רצון שאני רואה בלשון של מכונות טיורינג. התוהה השתמש בצורה חזקה מאוד בכך שיש איזו מכונה שלישית, שמריצה גם את Q וגם את S, ומוודאת ש-S באמת מעבירה את הקלט הזה ולא משקרת. בהתחלה התוהה הציג גרסה פשוטה יותר של האתגר: להוכיח שלא ניתן לפתור את בעיית העצירה גם אם מגבילים את הקלטים להיות מהצורה M,x כאשר M שונה מ-x. אפשר להוכיח באופן ישיר שגם אלגוריתם לפתרון הבעיה הזו לא קיים (הראיתי איך קודם), אבל גם רדוקציה מבעיית העצירה לבעיה הזו (שים לב: לא בכיוון ההפוך) קל להדגים: אם קיבלת M ו-x תעביר אותם לאלגוריתם הפלאי אם M שונה מ-x. אחרת, שנה את M בצורה שתחזיר מכונה שקולה (למשל, תוסיף עוד מצב פנימי שלא מגיעים אליו אף פעם) ואז תעביר את הקלט לאלגוריתם הפלאי. |
|
||||
|
||||
כן, כמובן שלא בכיוון ההפוך. אני קצת חלוד. תודה! |
|
||||
|
||||
רעיונות דומים צצים מדי פעם גם לגבי משפט גדל (אולי אפשר להכריע כל טענה פרט לטענות השקולות ל"אני לא יכיחה"? או פרט לטענות מתייחסות-לעצמן? או פרט לטענות מתייחסות-לעצמן-בעקיפין?) התשובה הפשוטה היא שאיך שלא מנסים להגדיר את הקבוצה ממנה מנסים להתעלם, אין כל קושי לתקן את ההוכחה כך שתתמודד גם למקרה המצומצם-יותר-לכאורה. זה תרגיל חביב במקרה של בעיית העצירה-פרט-למקרה-מכונה=קלט, ואפשר לדון בו אם רוצים. התשובה המתוחכמת יותר היא שכבר יש, בכל המקרים, דוגמאות מאוד קונקרטיות של בעיות הכרעה או עצירה וכו' שהן בלתי-פתירות. לדוגמה, אם נדון רק במכונות טיורינג המנסות לפתור משוואות דיופנטיות בדרך הפשוטה ביותר (לסרוק פתרונות אפשריים), גם את בעיית העצירה עבור היקום המאוד מצומצם הזה לא ניתן לפתור. זה כבר משפט הרבה יותר קשה, אבל הוא (מה לעשות) גם נכון, והוא בוודאי הרבה יותר חזק מהטענה הנדונה: התוהה מנסה לסלק רק את האלכסון (מכונה=קלט), ואילו כאן סילקנו את האלכסון ועוד הרבה יותר (כמעט את כל המכונות וכמעט את כל הקלטים), ואפילו זה לא מספיק. |
|
||||
|
||||
Proving Program Termination, B. Cook et al., CACM v54 n5, May 2011 בגדול, אם משנים קצת את השאלה, אפשר לענות במידה שימושית על בעיית העצירה."In our new problem statement we will still require that a termination proving tool will always return answers that are correct, but we will not necessarily require an answer. If the termination prover cannot prove or disprove termination, it should return 'unknown."'
|
|
||||
|
||||
עוד לא קראתי את המאמר, אבל אני חושב שמתפספסת כאן נקודה (לא בהכרח במאמר אלא בפרשנות של מה זה אומר). אנחנו *לא רוצים* לשנות את בעיית העצירה כך שתהיה פתירה. יש לא מעט וריאציות שאפשר להציע על בעיית העצירה כך שתהיה פתירה, אבל אנחנו דווקא רוצים את הניסוח הלא פתיר. לא כי בעיית העצירה בפני עצמה כל כך מעניינת, אלא כי מה שנובע מאי הפתירות שלה (למשל, אי הפתירות של הבעיה העשירית של הילברט או של בעיית ריצופי וואנג) מעניין. אגב, ה- In contrast to popular belief, proving termination is not always impossible. שמופיע בתחילת המאמרקצת חצוף. אלו לא חדשות חדשות... |
חזרה לעמוד הראשי | המאמר המלא |
מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
RSS מאמרים | כתבו למערכת | אודות האתר | טרם התעדכנת | ארכיון | חיפוש | עזרה | תנאי שימוש | © כל הזכויות שמורות |