בתשובה לאלון עמית, 20/02/04 1:14
 |
|
 |
||
|
||||
 |
האם תוכל להסביר לי בשפה פשוטה למה היפותזת צ'רצ'-טיורינג כ"כ כ"כ סבירה? מה יש במערכת הבסיסית הזו שמגדיר *בדיוק* את כל מה שצריך כדי לממש כל אלגוריתם? ועוד לגבי ההיפותזה הבסיסית והמסתורית הזו (בעיני), מה הקשר בין מה שנחשב פתיר ולא פתיר אלגוריתמית למה שנחשב ניתן להוכחה אם לאו במתמטיקה (עפ"י גדל)? כמו כן, למיטב ידיעתי העבודה של אודי שפירו על "מחשבים ביולוגים" אינה מבוססת על ריבוזומים (המייצרים פלט חלבונים מקלט של RNA) אלא על ה-DNA לבדו. (אבל אולי אני כבר לא מעודכן) |
 |
 |
 |
|
|
|
||
|
||||
|
קודם כל אבהיר שאינני טוען שההיפותזה נראית סבירה *במבט ראשון* - נהפוך הוא, במבט ראשון מכונת-טיורינג נראית משהו פרימיטיבי עד-מאוד. התיזה הופכת לסבירה בשני תנאים: אחד, שמבהירים מה היא בעצם טוענת ומה הם גבולות היומרה שלה, ושניים, שמראים פורמלית (וזו עבודה) שבעזרת מכונת-טיורינג אפשר לבצע כמה וכמה פעולות יותר "גבוהות", שמהן כבר פחות קשה להאמין שאפשר הכל. קודם כל ננסה לחדד את מהות התיזה. מדובר בחישוב - כלומר, תהליך שמתחיל מנתונים מסויימים, טוחן טוחן טוחן, ומניב תוצאה. מניחים שהחישוב הוא דטרמיניסטי1, כלומר שמי שמחשב יודע בכל רגע נתון מה עליו לעשות, והוא לא מנחש או נועץ בכוכבים או מתבלבל. הנתונים, הקלט והפלט, הם או מספרים טבעיים, או רצפים סופיים של אותיות מא"ב סופי מסויים (למשל רצפים של סיביות) - אין זה משנה כי קל לתרגם מהאחד לשני. הנתונים אינם יכולים להיות, נניח, מספרים ממשיים (הדורשים אינסוף מידע כדי לייצגם2). מדוע שנניח שכל "חישוב" עוסק ברצפים סופיים של סמלים? ההנחה הממשית היחידה פה היא סופיות, והיא נראית סבירה: אם צריך אינסוף זמן רק כדי לקרוא את השאלה, קשה לראות איזו משמעות יש לחישוב. "רצף סופי של סמלים" הוא מושג גמיש מספיק כדי לאפשר לאלגוריתם לטפל גם בתמונות (סרוקות), במוסיקה (דגומה), באובייקטים מתמטיים (שיש להם תיאור סופי), וכו'. במילים אחרות, לומר שחישוב הוא תהליך שמקבל מחרוזת של אותיות, ומוציא איזו מחרוזת אחרת, זהו תיאור גמיש מספיק כדי לכלול (נגיד) בדיקת ראשוניות של מספר, מיקסוס של ערוצי שמע, חיפוש גנים בדנ"א, תכנון של צ'יפ, חיפוש ב"אייל", דחיסת תמונה, ועוד כהנה וכהנה. עכשיו, מה אתה עושה כשאתה "מחשב" משהו מקלט שהוא רצף של אותיות? אתה מבצע פעולות אריתמטיות פשוטות, אתה זוכר תוצאות ביניים, אתה מקבל החלטות על-סמך תוצאות קודמות, אתה מוחק ומשנה דברים שרשמת קודם, ובערך זהו. אם חסר לך משהו בתיאור הפשטני הזה, תאמר ונראה אם אפשר להוסיף אותו. את התיאור הזה קל יחסית לפרמל ע"י, נניח, שפת התכנות החביבה עליך בסביבה של מחשב עם זיכרון גישה אקראי. נשמע סביר? לבסוף, צריך להראות שמכונת הטיורינג האומללה מסוגלת לבצע את כל מה שנדרש משפת התכנות ההיא. זה קצת מייגע אבל לא נורא מסובך - אם *זה* מה שמציק לך בתיזה של צ'רץ'-טיורינג, וכל הלהג עד כה היה מיותר, תגיד וניכנס גם לזה. -- על הקשר בין מה שפתיר ולא פתיר אלגוריתמית למה שניתן להוכיח במערכת פורמלית אני אכתוב בנפרד, אחרת ההודעה תתארך עד מאוד (כאילו שהיא לא ארוכה כבר). בקשר לאודי שפירו (אתה צודק, משום מה זכרתי שהוא כותב "שפירא"), אנחנו מדברים על עבודות שונות - חישוב באמצעות דנ"א הוא נושא חמוד כשלעצמו ואף בוצע מעשית (לא זוכר אם גם ע"י אודי עצמו), אבל אני מדבר על עבודה שככל הידוע לי נותרה תיאורטית ובה הוא מנסה לראות אם לריבוזום יש גמישות פונקציונלית מספקת כדי לתפקד כמכונת-טיורינג. שמעתי על זה הרצאה ממנו, אינני יודע כמה הוא המשיך להתעמק בזה ומה, אם בכלל, פורסם. 1 לאוטומטים לא דטרמיניסטיים יש שימושים תיאורטיים חשובים, כמו בהגדרת המחלקה NP, אך בהקשר הנוכחי סביר לדרוש מ"חישוב" או "אלגוריתם" להיות חד-משמעי ולא תלוי בניחושים. 2 יש מודלים אחרים של חישוב הדנים בממשיים, אך זה סיפור אחר. |
|
|
|
|
|
|
||
|
||||
|
תודה. ענית לי אבל גם לא. בסדר, אז ניתן לסמלץ פתרון בעיות *מאד* מסובכות על מכונת טיורינג. ניתן אפילו למכור במילים את היכולת של מכונה כזו לקרוא קלט סופי (הסרט עליה יושב "הראש" דווקא אינסופי למיטב ידיעתי) ולכתוב מסקנות ביניים. אפילו להוכיח שוויון של המכונה לשפות התכנות המוכרות והאהובות הינה משימה אפשרית לדברייך. אבל מאיפה העוז לקבוע ש*כל* אלגוריתם ניתן להרצה ע"י מכונה זו, או אם להיות יותר סנסציוני, שכל מה שלא ניתן להרצה על מכונת טיורינג לא ניתן להרצה על שום חומרה אחרת? מה אתה יכול לספר על רעיון הריבוזומים הזה? תן אותה ב-גֶדֵל : ) |
|
|
|
|
|
|
||
|
||||
|
זה כמובן תלוי באיך אתה מגדיר *אלגוריתם*. כל הגדרה סבירה תהיה משהוא בסגנון הבא: מכונה המאפשרת לחשב את הערך (=פלט) של פונקציה מתמטית מסויימת, על קלט X כלשהוא, באמצעות הפעלת סדרת פעולות לפי סט כללים קבוע וסופי (מסובך ככל שיהיה). מן הסתם אתה תרשה לאלג' להשתמש בזיכרון (אולי אפילו אינסופי). זה בדיוק מה שמכונת טורינג מאפשרת1 (היא אפילו לא מחייבת שהאלג' יסתיים בזמן סופי). כל מודל הגיוני אחר הם רדוקטיבי ל-TM באופן טריביאלי *מאוד*. לא נראה שיש איזשהוא מודל הגיוני (כלומר כזה שהפלט שלו מוגדר היטב) שמאפשר הרצה של יותר אלגוריתמים. אתה מוזמן לחפש מודל כזה. אולי כדאי לציין כקוריוז שיש המון פונ' מתמטיות שלא ניתן לבנות עבורן אלג' (ב-TM), למעשה הרבה יותר מאשר כאלו שכן ניתן לבנות להן אלג'. אין שום קשר לגדל אלא אם כן אתה משתמש במונח זה כבמעין "אווה מריה". 1 תחת ההנחות שציין אלון. וניתן להסיר אותן במאמץ קטן. |
|
|
|
|
|
|
||
|
||||
|
תוכל לתת כמה דוגמאות של הפונקציות הללו, או שרק הוכח הקיום שלהן אבל לא מצאו דוגמא? (אני חושב שאני זוכר במעורפל ששמעתי משהו על שימוש במשפט קנטור על קבוצת השפות הפורמליות או משהו בסגנון. צריך ללמוד את זה באמת) | |
|
|
|
|
|
||
|
||||
|
המינוח המדוייק שצריך להשתמש בו הוא שפות בלתי כריעות (השתמשתי במונח פונקציות רק לצורך הבהרה). מצאו כמה כאלו, אבל הדוגמא היחידה שאני זוכר זו בעית העצירה1. הקיום של הרבה שפות בלתי כריעות כאלו נובע בפשטות מכך שיש הרבה יותר שפות (שתיים בחזקת ALEF EFES) מאשר אלגוריתמים (ALEF EFES). _________ 1 בהינתן מכונת טורינג M וקלט מסויים עבורה X, החלט האם M תסיים את ריצתה על X בזמן סופי או לא (בשפת העם, תיכנס ללולאה אינסופית). |
|
|
|
|
|
|
||
|
||||
|
קצת מוזר שמכל הטקסט הזה, את שתי המלים הכי-עבריות החלטת לשעתק: ALEF זה אלף, EFES זה אפס. | |
|
|
|
|
|
||
|
||||
|
ראה, למשל: |
|
|
|
|
|
|
||
|
||||
|
תודה. הנושא של fair non-determinism נשמע מעניין מאוד. שאר המודלים האלטרנטיביים מסתמכים באופן "כבד" על איזשהוא משאב אינסופי, ואז זה לא מאוד מפתיע שיש להם יותר כח (אני מקווה שלא יסתבר שגם ה-fair non-determinism מסתמך על משאב אין סופי). הלקח שלי הוא שחייבים להניח1 דטרמיניזם וסופיות, כל עוד המרצה לא אמר אחרת. עכשיו מגיע הקטע שבו מישהוא מספר בדיחה מתמטית. ____ 1 "הנחה" זו עוד דוגמא לכפל משמעות הנהדר שיש בעברית בכמה מושגים מדעיים. |
|
|
|
|
|
|
||
|
||||
|
מעלה המון תובנות בקשר לחלק מהשאלות שהועלו כאן, במיוחד הקשר של צ'רצ-טיורינג לגדל, ולמגבלות הפיסיקליות השונות (פלאנק ושות'). | |
|
|
|
|
|
||
|
||||
|
אני מצטרף להמלצה לקרוא את המאמר - תמיד דבר טוב - אבל לעניות דעתי הוא לא כל-כך מעניין, לא מדויק לפרקים, וחוטא בכתיבה שיווקית מופרזת מאוד. אם מישהו רוצה אפשר לפצוח בדיון סוער על הבעיות במאמר והשאלה אם Hypercomputation זה מעניין. (אגב, fair non-determinism לא מתחמק (כמובן) מהבעיות הקשורות באינסוף - קרא את הקטע עם הלמה של Koenig). |
|
|
|
|
|
|
||
|
||||
|
כן, הבנתי את זה בקריאה היותר מלאה. | |
|
|
|
|
|
||
|
||||
|
בבקשה! אבל נראה שלא הבנת אותי. המסר לא היה "אפשר לפתור בעיות מאוד מסובכות עם מכונת טיורינג", אלא "מכונת טיורינג יכולה לבצע כל דבר שאנו מסוגלים לחשוב עליו שנופל תחת הכותרת 'אלגוריתם"'. (אגב, הסרט באמת אינסופי, אבל מניחים תמיד שבשלב הקלט הסרט ריק (או מלא באפסים) פרט למספר סופי של מקומות, ולכן אם המכונה עוצרת גם הפלט סופי). ה"עוז" נובע בדיוק מכך שכל אלמנט אבסטרקטי שנראה שהוא חלק מהמונח "אלגוריתם" ניתן ליישום ע"י מכונת טיורינג. אם אפשר "להריץ משהו על חומרה אחרת", נסה לדמיין - מה עושה אותה חומרה? היא לא מבצעת סדרה של פעולות שמירה, שליפה, החלטה וחישוב-פשוט? מה עושה "מכונה" כלשהי, בכלל? כל הנקודה היא שלפחות בקונטקסט של קלט-פלט סופי ודיסקרטי, אף אחד עוד לא הצליח לחשוב על משהו שלא נופל בקטגוריות האלה, והאמת גם קשה (לי, לפחות, ונראה שגם לאחרים) לדמיין מה משהו כזה יכול להיות. שוב, אין פה הוכחה - אנו מנסים לפרמל מושג אינטואיטיבי. משפטי גדל דנים ביכולת של מערכת לוגית פורמלית להיות עקבית (לא מאפשרת להוכיח דבר והיפוכו) ושלמה (לכל טענה בשפה של המערכת, אפשר להוכיח או את הטענה או את שלילתה). אחד המשפטים מראה שכל מערכת סבוכה מספיק (מספיקה כדי לתאר את המספרים הטבעיים) אינה יכולה להיות גם עקבית וגם שלמה. משפט אחר, קשור, מראה שמערכת לוגית (שוב, מורכבת מספיק) איננה יכולה להוכיח את העקביות של עצמה (אם היא עקבית. אם לא, היא יכולה להוכיח כל דבר). משפטי אי-האפשרות של טיורינג הם דומים אך שונים. המשפט הבסיסי אומר שאין מכונת טיורינג המקבלת כקלט תיאור של אלגוריתם (מכונה אחרת) וקלט לאותו אלגוריתם, ומחליטה אם הפעלת אותו אלגוריתם על אותו קלט תיגמר לבסוף. (מכונת טיורינג, כפי שהגדרנו אותה, יכולה לבצע מיליארד צעדים ולעצור, אך היא עלולה גם לא לעצור לעולם - קל מאוד לכתוב תכנית מחשב שלא עוצרת). בעזרת משפט זה הוכיחו שפע של תוצאות שליליות במתמטיקה, לפיהן אין אלגוריתם המסוגל לפתור משוואות דיופנטיות או לבדוק אם חבורה (הנתונה ע"י יוצרים ויחסים) היא טריויאלית או לבדוק אם שני מרחבים תלת-ממדיים (הנתונים ע"י תיאור קומבינטורי של פירמידות מודבקות) הם זהים מבחינה טופולוגית. הדמיון בין המשפטים הוא באופי שלהם (מגבלות מסויימות של מערכות פרוצדורליות פורמליות) וגם באופי ההוכחות (קידוד של המערכות עצמן בשפה שהן פועלות בה). אני צריך עוד לחשוב אם יש קשר ישיר יותר של גרירה לוגית, צריך להיזהר פה קצת אבל אני אחשוב. בקשר לריבוזומים - הכי טוב שאודי יסביר בעצמו: |
|
|
|
|
|
|
||
|
||||
|
תודה. עכשו ברור יותר. עושה רושם שכמה מהמשפטים היסודיים ביותר של תחומי דעת מסויימים הם "חוקי אי אפשר": חוקי גדל, חוק אי הודאות של הייזברג, היפותזת צ'רצ'-טורינג. מעניין, על דרך השלילה האנשים הללו עלו על תובנה יסודית לגבי אופן פעולתם של דברים. |
|
|
|
|
|
|
||
|
||||
|
וכמובן גם בעית העצירה וחסם מהירות האור. | |
|
|
|
|
|
||
|
||||
|
|
|
|
|
|
|
||
|
||||
|
לגבי מודלי חישוב שאינם ניתנים לרדוקציה למכונת טיורינג רגילה, קיימים כמובן חישובים הסתברותיים, הניתנים לחישוב ע"י מכונת טיורינג הסתברותית (אם אתה במצב מספר 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 מאמרים |
כתבו למערכת |
אודות האתר |
טרם התעדכנת |
ארכיון |
חיפוש |
עזרה |
תנאי שימוש
|
© כל הזכויות שמורות |