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