|
||||
|
||||
זה לא "באג". זו סתירה, שמראה ש-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. אבל הרדוקציה הפרטנית הזו די מיותרת, כי משפט רייס (שלא הוזכר במאמר) כולל גם את המקרה הזה. |
|
||||
|
||||
תמיד יש את הבעיה הזו כשמשלימים דיונים עם עשרות+ תגובות: או שתגיב ותחרמופף או שתקרא קודם את הכל ותשכח על מה רצית להגיב. |
חזרה לעמוד הראשי | המאמר המלא |
מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
RSS מאמרים | כתבו למערכת | אודות האתר | טרם התעדכנת | ארכיון | חיפוש | עזרה | תנאי שימוש | © כל הזכויות שמורות |