בתשובה לארז ליבנה, 23/02/04 14:06
 |
|
 |
||
|
||||
 |
בבקשה! אבל נראה שלא הבנת אותי. המסר לא היה "אפשר לפתור בעיות מאוד מסובכות עם מכונת טיורינג", אלא "מכונת טיורינג יכולה לבצע כל דבר שאנו מסוגלים לחשוב עליו שנופל תחת הכותרת 'אלגוריתם"'. (אגב, הסרט באמת אינסופי, אבל מניחים תמיד שבשלב הקלט הסרט ריק (או מלא באפסים) פרט למספר סופי של מקומות, ולכן אם המכונה עוצרת גם הפלט סופי). ה"עוז" נובע בדיוק מכך שכל אלמנט אבסטרקטי שנראה שהוא חלק מהמונח "אלגוריתם" ניתן ליישום ע"י מכונת טיורינג. אם אפשר "להריץ משהו על חומרה אחרת", נסה לדמיין - מה עושה אותה חומרה? היא לא מבצעת סדרה של פעולות שמירה, שליפה, החלטה וחישוב-פשוט? מה עושה "מכונה" כלשהי, בכלל? כל הנקודה היא שלפחות בקונטקסט של קלט-פלט סופי ודיסקרטי, אף אחד עוד לא הצליח לחשוב על משהו שלא נופל בקטגוריות האלה, והאמת גם קשה (לי, לפחות, ונראה שגם לאחרים) לדמיין מה משהו כזה יכול להיות. שוב, אין פה הוכחה - אנו מנסים לפרמל מושג אינטואיטיבי. משפטי גדל דנים ביכולת של מערכת לוגית פורמלית להיות עקבית (לא מאפשרת להוכיח דבר והיפוכו) ושלמה (לכל טענה בשפה של המערכת, אפשר להוכיח או את הטענה או את שלילתה). אחד המשפטים מראה שכל מערכת סבוכה מספיק (מספיקה כדי לתאר את המספרים הטבעיים) אינה יכולה להיות גם עקבית וגם שלמה. משפט אחר, קשור, מראה שמערכת לוגית (שוב, מורכבת מספיק) איננה יכולה להוכיח את העקביות של עצמה (אם היא עקבית. אם לא, היא יכולה להוכיח כל דבר). משפטי אי-האפשרות של טיורינג הם דומים אך שונים. המשפט הבסיסי אומר שאין מכונת טיורינג המקבלת כקלט תיאור של אלגוריתם (מכונה אחרת) וקלט לאותו אלגוריתם, ומחליטה אם הפעלת אותו אלגוריתם על אותו קלט תיגמר לבסוף. (מכונת טיורינג, כפי שהגדרנו אותה, יכולה לבצע מיליארד צעדים ולעצור, אך היא עלולה גם לא לעצור לעולם - קל מאוד לכתוב תכנית מחשב שלא עוצרת). בעזרת משפט זה הוכיחו שפע של תוצאות שליליות במתמטיקה, לפיהן אין אלגוריתם המסוגל לפתור משוואות דיופנטיות או לבדוק אם חבורה (הנתונה ע"י יוצרים ויחסים) היא טריויאלית או לבדוק אם שני מרחבים תלת-ממדיים (הנתונים ע"י תיאור קומבינטורי של פירמידות מודבקות) הם זהים מבחינה טופולוגית. הדמיון בין המשפטים הוא באופי שלהם (מגבלות מסויימות של מערכות פרוצדורליות פורמליות) וגם באופי ההוכחות (קידוד של המערכות עצמן בשפה שהן פועלות בה). אני צריך עוד לחשוב אם יש קשר ישיר יותר של גרירה לוגית, צריך להיזהר פה קצת אבל אני אחשוב. בקשר לריבוזומים - הכי טוב שאודי יסביר בעצמו: |
 |
 |
 |
|
|
|
||
|
||||
|
תודה. עכשו ברור יותר. עושה רושם שכמה מהמשפטים היסודיים ביותר של תחומי דעת מסויימים הם "חוקי אי אפשר": חוקי גדל, חוק אי הודאות של הייזברג, היפותזת צ'רצ'-טורינג. מעניין, על דרך השלילה האנשים הללו עלו על תובנה יסודית לגבי אופן פעולתם של דברים. |
|
|
|
|
|
|
||
|
||||
|
וכמובן גם בעית העצירה וחסם מהירות האור. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
לגבי מודלי חישוב שאינם ניתנים לרדוקציה למכונת טיורינג רגילה, קיימים כמובן חישובים הסתברותיים, הניתנים לחישוב ע"י מכונת טיורינג הסתברותית (אם אתה במצב מספר 67 וקורא 1 תעבור למצב 112 בהסתברות 43 או למצב 86 בהסתברות 57. אם אתה קורא 0 תעבור למצב 98 בהסתברות 33 ולמצב 65 בהסתברות 67) וכן אלגוריתמים קוונטיים הניתנים לחישוב ע"י מכונת טיורינג קוונטית. (דטרמיניסטית או הסתברותית) אפשר כמובן לטעון שאלגוריתם הסתברותי או קוונטי הוא לא אלגוריתם אלא משהו אחר, אבל זה כבר עניין של הגדרה. |
|
|
|
|
|
|
||
|
||||
|
נכון, אבל זהירות - העניין באלגוריתמים הסתברותיים וקוונטיים נובע מיכולתם לחשב *ביעילות* בעיות קשות, לא (ככל הידוע לי) לפתור בעיות ש*אינן ניתנות לחישוב*. אם יש אלגוריתם הסתברותי המסוגל לבדוק אם גרף הוא 3-צביע (נניח), אז ודאי שיש גם אלגוריתם דטרמיניסטי המסוגל לעשות זאת, רק הרבה יותר לאט. ההישג העיקרי של המודלים הקוונטיים של חישוב הוא בפירוק *יעיל* של מספרים, שהיא כמובן בעייה טריויאלית מההיבט החישובי. אם מדובר על חישוביות, ולא סיבוכיות, אז חישוב הסתברותי איננו מעשיר את הרפרטואר, ואני סבור שגם קוונטי לא (ייתכן שאני טועה בנקודה זו, עבר זמן מאז התעניינתי בתחום). | |
|
|
|
|
|
||
|
||||
|
אתה לא טועה (מחשבים קוונטיים ניתנים לסימולציה ע''י מכונות טיורינג - הבעיה היא שהסימולציה איטית). | |
|
|
|
|
|
||
|
||||
|
אני לא בטוח שאתה צודק. עד כמה שאני זוכר, מכונת טיורינג לא יכולה לסמלץ במדוייק מכונת טיורינג קוונטית שנמצאת בסופרפוזיציה של כמה מצבים. ניתן לייצג קרוב בלבד. | |
|
|
|
|
|
||
|
||||
|
נדמה לי שאתה מתכוון לומר שאם למכונה הקוונטית מותר להיות בסופרפוזיציה של כמה מצבים עם משקל ממשי לכל מצב, אז לא ניתן לסמלץ זאת בדיוק ע''י מכונה דטרמיניסטית שיש לה אפילו יותר מצבים, אחד לכל קומבינציה של מצבים קוונטיים, כי דרושים אינסוף מצבים לסימלוץ. אבל אני לא בטוח שזה משנה לשאלת ה''מה ניתן לחשב''. אם נכון לחשוב על מכונה קוונטית בסופרפוזיציה כנמצאת במספר מצבים, כל אחד עם משקל (אפילו ממשי), וכשהיא מתקדמת היא מגיעה לסופרפוזיציה של מצבים אחרים עם משקלות אבל באופן שכל מצב חדש (עם משקל חיובי) הוא נגיש ממצב ישן (עם משקל חיובי), אז לכל חישוב שלה יש חישוב חוקי של המכונה הקלאסית המתאימה ש''במקרה'' בוחר נכון בכל שלב לאן ללכת. שוב, השאלה היא רק אם החישוב הקלאסי הוא ''מסלול'' בגרף המסובך של החישוב הקוונטי, ואם יש איזושהי דרך לצאת מהמצב ההתחלתי (או אחד מהם, אם יש כמה) ולהגיע לתוצאה הסופית המבוקשת. |
|
|
|
|
|
|
||
|
||||
|
או אולי סתם שאלות מטופשות (אתה תשפוט): "משפט אחר, קשור, מראה שמערכת לוגית (שוב, מורכבת מספיק) איננה יכולה להוכיח את העקביות של עצמה (אם היא עקבית. אם לא, היא יכולה להוכיח כל דבר)." 1. האם ניתן להוכיח בתוך מערכת לא-עקבית את חוסר העקביות? (האם עצם זה שניתן להוכיח דבר והיפוכו מהווה את ההוכחה לכך שהמערכת היא אי-עקבית? אבל לפי זה גם ניתן להוכיח שהיא לא עקבית, ומכאן לא יוצא שהשאלה לא מוגדרת טוב או משהו כזה?) 2. אם ניתן להוכיח שמערכת היא לא-עקבית, האם ניסוח יותר מדוייק למשפט למעלה הוא, "לא ניתן להוכיח במערכת לוגית מורכבת מספיק שלגביה (או בתוכה) לא הצלחנו להוכיח (להראות?!) חוסר-עקביות כי היא עקבית" ? 3. האם ניתן להוכיח עקביות של מערכת כלשהו באמצעות מערכת חיצונית ומכילה אותה, ואם כן, מה הערך של הוכחה כזו, ובכלל מה ההבדל בין הוכחות תוך-שפתיות לחוץ-שפתיות? |
|
|
|
|
|
|
||
|
||||
|
1. כן. ההגדרה של מערכת לא עקבית היא שהיא יכולה להוכיח דבר והיפוכו. לכן, אי-עקביות (אם היא קיימת) ניתנת להוכחה בתוך המערכת. במצב זה, ניתן לראות שאפשר להוכיח באמצעות המערכת *כל* דבר (וגם את היפוכו), מה שכמובן הופך אותה ללא מעניינת. נכון שאפשר אז גם להוכיח שהיא לא עקבית וגם להוכיח שהיא כן עקבית (בהנחה שעקביות-עצמית בכלל ניתנת לניסוח בתוך המערכת, מה שלא תמיד המצב), כמו שאפשר להוכיח גם ש-X=X וגם ש=X שונה מ-X; זה לא נורא מעניין כי זה כבר לא נכון שמה שאפשר להוכיח הוא אמיתי. מובן מאליו שלוגיקאים מקווים מאוד שהמערכות בהן הם עובדים אינן כאלה, ולעיתים ניתן להוכיח זאת (באמצעות מערכות רחבות יותר). 2. לא, אין קשר ל"לא הצלחנו", הטענה היא שאי-אפשר. אבל אתה צודק, צריך לסייג ב"אם היא עקבית". 3. כן. הנה דוגמה: יש מערכת הנקראת "אקסיומות פֵּאָנו (מסדר ראשון) של תורת המספרים". זו תורה לוגית המאפשרת לדון במספרים הטבעיים, בחיבור ובכפל, ולהוכיח משפטים כמו "כל מספר ראשוני המשאיר שארית 1 בחלוקה ל-4 הוא סכום של שני ריבועים", וכו'. צריך להבין שלא כל טענה מתמטית בכלל ניתנת לניסוח בתוך המערכת הזו: למשל, הטענה "לכל פונקציה רציפה על הכדור יש נקודת שבת" היא כזו. לעומת זאת, הטענה "מערכת פאנו היא עקבית" דווקא כן ניתנת לניסוח כטענה בתוך המערכת - ברם, לפי גדל, אי אפשר להוכיח אותה במערכת זו. למרבה השמחה אפשר כן להוכיח אותה במערכת חזקה יותר, למשל אחת הנקראת ZF ומכילה אקסיומות של תורת הקבוצות. מה הערך של הוכחה כזו? פשוט, היא עוזרת לך להקטין את מספר הדברים בהם צריך להאמין. אם אתה מאמין ש-ZF עקבית, קיבלת במתנה שגם פאנו כזו. |
|
|
|
|
|
|
||
|
||||
|
2. אין צורך לסייג: אי-אפשר להוכיח עקביות, בין אם מפני שהמערכת לא עקבית, ובין אם מפני שהיא עקבית ואי-אפשר להוכיח את זה. | |
|
|
|
|
|
||
|
||||
|
זה סתם ניטפוק לא מעניין, אבל אם המערכת לא עקבית, למה היא לא יכולה להוכיח שהיא עקבית? פורמלית, היא כן, והיא יכולה גם להוכיח את ההיפך וזה כאמור לא ממש מעניין. -- (גזור וזרוק) -- אם המערכת היא T, ו-X מסמן איזושהי סתירה כמו "a וגם לא a", אז: T |= (X -> con(T)) כי אגף ימין הוא טאוטולוגיה, וגםT |= X כי T לא עקבית, ומכאן בגרסת מודוס-פוננס ליכיחות,T |= con(T) לא?
|
|
|
|
|
|
|
||
|
||||
|
יכול להיות שזו סתם קטנוניות טכנית, אבל הוכחות פורמליות לא עובדות עם טאוטולוגיות של תחשיב פסוקים? הטענה (a!=a --> B) איננה מהווה טאוטולוגיה בתחשיב הפסוקים, וממילא לא ניתן להשתמש בה כאקסיומה בהוכחה. אני חושב שעל מנת להראות שסתירה בתחשיב יחסים מוכיחה כל טענה אפשר לשחזר את הוכחת משפט השלמות של גדל, כאשר לכל טענה A ניתן לטעון ש "כל מודל של T מקיים A" (באופן ריק). | |
|
|
|
|
|
||
|
||||
|
אני לא בטוח שצריך דווקא את תחשיב הפסוקים, עקרונית כל מה שדרוש הוא שפה ומערכת הוכחה. לרוב דורשים שמערכת ההוכחה תהיה sound ושלמה, אבל לצורך הזה אני לא חושב שאפילו צריך שלמות. במערכת הוכחה סבירה, כלל הגזירה הבאה (הוכחה על דרך השלילה) יהיה אקסיומה, או מסקנה מכללים אחרים: אם T, ~f |- g ו-T, ~f |- ~g אזT |- f ונראה לי שזה כל מה שדרוש. (למעלה השתמשתי בטעות ב-=| במקום ב -|, זה לא משנה הרבה אך התכוונתי להסקה פורמלית, לא לנכונות בכל מודל. אולי זה מה שבלבל).
|
|
|
|
|
|
|
||
|
||||
|
חשבתי על זה עוד קצת, אבל עדיין נראה לי שיש איזו בעיה עקרונית. הרי מערכת ההוכחה היא "טיפשה". היא מסוגלת לזהות רק סתירות של תחשיב פסוקים (כי היא כוללת את הטאוטולוגיות של פסוקים כאקסיומות). ברור שאם כבר ידוע ש T -מוכיחה- טענה ושלילתה אז ניתן להוכיח הכל, אבל סתם מכך שיצרנו תורה לא עקבית (למשל, תורה של מרחב וקטורי ממימד n יחד עם אופרטור שהינו חח"ע אבל לא על) עוד אין לנו סדרת הוכחה. בשביל להראות שמספיק שב T יש סתירה על מנת לייצר הוכחה של כל טענה יש לטעון שלפי קומפקטיות יש לנו אוסף סופי של טענות שבהן כבר יש סתירה, ומשם בעצם לשחזר את הוכחת משפט השלמות. רק במקרה שהסתירה ב T נובעת מסתירה של תחשיב פסוקים אז "יש לנו מזל" וההוכחה נעשית מובנת מאליה. אבל באוסף הטענות שכולל את האקסיומות של מרחב וקטורי ממימד n בצרוף הטענה על אופרטור חח"ע ולא על אין שום סתירה של תחשיב פסוקים. בקיצור, אם אני לא טועה יש הבדל בין העובדה (הטריוויאלית לגמרי) שאם מערכת מוכיחה טענה ושלילתה אז היא מוכיחה כל טענה, לבין העובדה שאם במערכת -קיימת- סתירה (קרי, היא איננה עקבית, אין לה שום מודל) אז ניתן לייצר ממנה הוכחה לכל טענה. הוכחת העובדה השניה היא כבר פחות או יותר משפט השלמות. | |
|
|
|
|
|
||
|
||||
|
רגע, נדמה לי שהקושי הוא שאתה מגדיר מערכת לא-עקבית ככזו שאין לה מודל, ואני הגדרתי מערכת לא-עקבית ככזו שמוכיחה דבר והיפוכו. במערכות שלמות, כפי שציינת, זה אותו דבר. אני חושב שנתקלתי בשתי ההגדרות. | |
|
|
|
|
|
||
|
||||
|
sound = נאותה. (סליחה על ההפרעה, תמשיכו). | |
|
|
|
|
|
||
|
||||
|
חשבתי שמדובר על הוכחה מבחוץ (במערכת עקבית) שהמערכת (הלא-עקבית) ''שלנו'' היא עקבית, וזה כמובן בלתי אפשרי. אבל זה לא מאד מעניין. | |
|
|
|
|
|
||
|
||||
|
אודי שפירו בעבודה מעניינת מאד, מסתבר שהתכניות שלו הרבה יותר מעשיות ממה שחשבתי: |
|
|
|
|
|
|
||
|
||||
|
התכניות שלו לזכות בפרס נובל? | |
|
|
|
|
|
||
|
||||
|
אולי :-) אבל התכוונתי למעשיות של תכניותיו לגבי מחשבים ממולקולות ביולוגיות. | |
|
|
|
|
|
||
|
||||
|
נדמה לי שזה כבר לא בגדר "מעשיוֹת" :) | |
|
|
|
|
|
||
|
||||
|
אני קורא בעיון את הדיון של החברים המלומדים והחלטתי שאתם הכתובת לבקש עזרה.אני זקוק לכל חומר שיכול לעזור לי לערון בצורה יפה ומסודרת את ההיסטוריה של "מדעי המחשב"-הדיסציפלינה.לא ההיסטוריה של מכונות החישוב ולא ההיסטוריה של התכנות או כל דבר אחר דומה.אלא של המדע עצמו: המושגים המופשטים, התיאוריה המתימטית, הדמויות החשובות וכו, ללא קשר למחשב עצמו. כל עזרה תתקבל בברכה. בתודה מראש: דודי. |
|
|
|
|
|
|
||
|
||||
|
סליחה שאני מתערב, וסליחה על האורך, אבל יש קשר ישיר. אפשר להוכיח את משפט גדל על ידי משפט אי העצירה. ההוכחה נוסחה על ידי טיורינג עצמו. הרעיון בנפנוף ידיים, הוא כדלקמן: קיימת פונקציה חד חד ערכית מאוסף כל מכונות הטיורינג למספרים הטבעיים. (לא זוכר אותה, אבל היא קיימת ומנוסחת היטב. תאמינו לי). קיימת פונקציה בין מצבים שונים של מכונת טיורינג לבין המספרים הטבעיים. בינהם - מצב העצירה. קיימת פונקציה בין כל הקלטים של מכונת טיורינג לבין המספרים הטבעיים. מכל הטררם הנ"ל יוצא, שהמשפט "מכונת טיוריג M עוצרת מתישהו כשהיא מקבלת פלט T" הוא פסוק בתורת המספרים. שוב, זה קצת נפנוף ידיים, אבל זה הרעיון. גם המשפט ההפוך, "המכונה M אינה עוצרת לעולם כשהיא מקבלת פלט T" הוא פסוק בתורת המספרים עכשיו בא הקטע המגניב באמת: 1)קיימת תוכנת מחשב Ma, שכידוע שקולה למכונת טיורינג, שמקבלת טקסט באנגלית, ומחליטה האם הטקסט הנ"ל הוא הוכחה תקנית (באמת כתבו אותה!) - כלומר - האם הטקסט מורכב מאקסיומות בהתחלה, משפט בסוף, וקשרים לוגיים נכונים בין כל משפט למשפטים הקודמים לו. 2) קיימת תוכנת מחשב Mb, שמייצרת את כל הטקסטים הסופיים, אחד אחרי השני (היא עובדת המון, אבל כל טקסט סופי, יבוא יומו והיא תייצר אותו) 3) נתן לMb לעבוד, ולשלוח טקסטים לMa, שתבדוק האם הטקסט הוא הוכחה תקנית. 4) נוסיף לMa שורות שיבדקו, במקרה שהיא מצאה שטקסט מסויים הוא הוכחה, האם האקסיומות שלו הם של תורת המספרים, והמשפט הסופי הוא "M עוצרת על T" 5) נוסיף עוד שורות שיבדקו מייד לאחר מכן, האם האקסיומות שלו הם של תורת המספרים, והמשפט הסופי הוא "M *לא* עוצרת על T" אם לכל הפסוקים בתורת המספרים, או לשלילתם, היתה הוכחה, אזי תוכנת המחשב (מכונת טיורינג) שבנינו הייתה מכריעה את בעיית העצירה. כיון שאי אפשר להכריע את בעיית העצירה, אזי משפט גדל נכון. חמוד, לא? |
|
|
|
|
|
|
||
|
||||
|
כן. | |
|
|
| חזרה לעמוד הראשי | המאמר המלא |
| מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים | |
 RSS מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |