הצגת המקור של הדף "משפט סביץ'"

'''משפט סביץ' '''(ב[[אנגלית]]: '''Savitch's theorem'''), שהוכח בידי [[וולטר סביץ']] בשנת [[1970]], הוא משפט ב[[תורת הסיבוכיות]] שקושר בין הזיכרון הנדרש לצורך פתרון בעיות בדרך דטרמיניסטית ובין הזיכרון הנדרש כאשר ניתן להשתמש ב[[אי-דטרמיניזם]].

==מבוא==
בתורת הסיבוכיות ממדלים בצורה [[מתמטיקה|מתמטית]] פתרון של בעיות מתחום [[מדעי המחשב]]. המודל המקובל הוא [[מכונת טיורינג]], שמדמה את פעולתו של [[מחשב]] בסיסי במיוחד (ועם זאת, כזה שניתן לפתור בו כל בעיה שניתנת לפתרון במחשב רגיל). אחד מהמדדים למורכבות של בעיה הוא כמות הזיכרון הנדרש כדי לפתור אותה, וכמות זו נמדדת במכונת טיורינג על ידי מספר תאי הזיכרון שנעשה בהם שימוש במהלך ריצת המכונה. מכיוון שעבור קלטים גדולים יותר נדרש באופן טבעי יותר זיכרון על מנת לפתור את הבעיה, נהוג למדוד את ה[[חסם (מתמטיקה)|חסם]] על הזיכרון שדורשת מכונת טיורינג מסוימת בתור [[פונקציה]] על גודל ה[[קלט]].

משפט סביץ' מראה כי אם נדרשת כמות כלשהי של זיכרון כדי לפתור בעיה בצורה אי-דטרמיניסטית, מספיקה כמות זיכרון זו בריבוע כדי לפתור את הבעיה בצורה דטרמיניסטית.

==ניסוח פורמלי==
בצורה פורמלית נהוג לראות את הבעיות החישוביות כבעיות של זיהוי [[שפה פורמלית|שפות פורמליות]].

את אוסף כל השפות שניתנות להכרעה ב[[סיבוכיות מקום]] <math>\ f(n)</math> באמצעות מכונת טיורינג דטרמיניסטית מסמנים בתור <math>\ \mbox{DSPACE}(f(n))</math>. את אוסף כל השפות שניתן להכרעה באמצעות [[מכונת טיורינג לא-דטרמיניסטית|מכונת טיורינג '''אי-דטרמיניסטית''']] בסיבוכיות מקום זו מסמנים <math>\ \mbox{NSPACE}(f(n))</math>.

בצורה פורמלית, ניסוחו של משפט סביץ' אומר:

* אם <math>f\in\Omega(\log(n))</math> אז <math>\ \mbox{NSPACE}(f(n))\subseteq \mbox{DSPACE}(f^2(n))</math>

==הוכחה==
ההוכחה של המשפט היא קונסטרקטיבית ומדגימה את הצורה שבה, עבור בעיה השייכת ל-<math>\ \mbox{NSPACE}(f(n))</math> ניתן לקבל מכונה דטרמיניסטית מתאימה בהינתן מכונה אי דטרמיניסטית שפותרת את הבעיה.

על מנת להוכיח את המשפט ראשית מוכיחים כי ניתן לפתור את הבעיה של בדיקה האם קיים מסלול בין שני צמתים ב[[גרף (תורת הגרפים)|גרף]] תוך שימוש בסיבוכיות זיכרון של <math>\ \log^2(n)</math>. לאחר מכן משתמשים בפתרון לבעיה זו כדי להריץ [[אלגוריתם חיפוש|חיפוש]] על הגרף המייצג את המצבים האפשריים בעת ריצת מכונת הטיורינג האי דטרמיניסטית שבודקת האם מילה מסוימת שייכת לשפה. ניתן להניח כי קיים מצב יחיד שבו המכונה מסיימת את ריצתה ומודיעה על קבלת המילה הנבדקת, ועל כן כל שיש לעשות הוא לבדוק האם קיים מסלול מהמצב ההתחלתי אל המצב המקבל. מכיוון שגודל הגרף הוא אקספוננציאלי בסיבוכיות הזיכרון של המכונה האי דטרמיניסטית, ומכיוון שאת החיפוש ניתן לבצע בסיבוכיות זיכרון לוגריתמית בריבוע ביחס לגודל הגרף, נובע כי סיבוכיות הזיכרון הכוללת הנדרשת היא ריבוע הזיכרון של המכונה האי דטרמיניסטית.

==משמעות==
המשמעות המיידית הנגזרת ממשפט סביץ' היא קיום השוויון <math>PSPACE = NPSPACE</math>. כלומר, כל בעיה שניתנת לפתרון בזיכרון [[פולינום|פולינומי]] באמצעות מכונה אי דטרמיניסטית ניתנת לפתרון בזיכרון פולינומי גם באמצעות מכונה דטרמיניסטית. התוצאה המקבילה במונחי [[סיבוכיות זמן]] היא [[P=NP]], אך בניגוד לתוצאה עבור זיכרון, לא ידוע אם P=NP וההשערה המקובלת היא שהדבר אינו נכון.

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

==לקריאה נוספת==
<div class="mw-content-ltr">
* Michael Sipser (1997). '''Introduction to the Theory of Computation'''. PWS Publishing. {{ISBN|0-534-94728-X}}
* Christos Papadimitriou (1993). '''Computational Complexity''', 1st edition, Addison Wesley. {{ISBN|0201530821}}
</div>

[[קטגוריה:סיבוכיות חישובית]]
[[קטגוריה:משפטים במדעי המחשב|סביץ']]