בתשובה לגדי אלכסנדרוביץ', 23/06/06 15:10
נוחו בשלום על משכבכם 392395
אה, זה קל. טפל הוא לא עיקרי, אמונה טפלה היא אמונה לא בעיקר, שהוא השם יתברך כמובן.

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

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

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

עכשיו, מתברר שאם לא מרשים למוודא להמר קצת ולהסתכן בכך שיטעה, אפשר גם לזרוק את כל האינטראקטיביות לפח ולחזור להוכחות "רגילות" (המוכיח שולח למוודא "עד" שמראה שהמילה שייכת לשפה, אם היא שייכת, והמוודא מוודא שהעד אכן עושה את העבודה. מה שמקבלים הוא את NP). לכן מרשים למוודא להטיל מטבעות ודורשים שהוא לא יטעה בהסתברות גדולה מספיק (למשל, מרשים שהוא יטעה בהסתברות 1/3). מתברר שכל השפות שקיימת להן הוכחה אינטראקטיבית שכזו הן בדיוק כל השפות שאפשר להכריע עם *זכרון* פולינומי, מה שנקרא PSPACE. אם אני לא טועה, מי שהוכיח את זה הוא עדי שמיר ממכון וייצמן (ה-S ב-RSA).

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

נוחו בשלום על משכבכם 392472
נשמע מדליק ביותר. אתה מוזמן להוסיף פרטים...
נוחו בשלום על משכבכם 392481
אגב, אולי זה לא כל כך ברור ממה שכתבתי: ב-IP הרעיון הוא שאם המילה בשפה, אז המוכיח, אם הוא מתנהג על פי הפרוטוקול, יצליח לשכנע את המוודא ב-‏2/3 מהמקרים שהמילה אכן בשפה, אבל אם המילה לא בשפה, אז לא משנה מה המוכיח יעשה (ובפרט, לא משנה אם הוא "ירמה" ולא יתנהג כפי שמצופה ממנו על פי הפרוטוקול), המוודא לא ישתכנע ב-‏2/3 מהמקרים.
נוחו בשלום על משכבכם 394061
"רק עכשיו זכיתי"? נכון ל23 ליוני 2006? למה, אתה לומד סיבוכיות עם פרופ' מולי ספרא או משהו?
נוחו בשלום על משכבכם 394074
לא. אני לא מבין את השאלה.
נוחו בשלום על משכבכם 394091
אה. פשוט, בתאריך הזה גם אנחנו למדנו את אותו חומר בדיוק.
נוחו בשלום על משכבכם 394159
אני לומד את הקורס המקביל בטכניון (הסמסטר). את החומר הזה התחלנו קצת לפני ה-‏23.

חזרה לעמוד הראשי המאמר המלא

מערכת האייל הקורא אינה אחראית לתוכן תגובות שנכתבו בידי קוראים