Севичева теорема

У рачунарској теорији сложености, Севичева теорема коју је 1970. године доказао Валтер Севич, даје релацију између детерминистичког и недетерминистичког простора сложености. Она утврђује да за било коју функцију $f\in \Omega (\log(n))$, важи :${\text{NSPACE}}\left(f\left(n\right)\right)\subseteq {\text{DSPACE}}\left(\left(f\left(n\right)\right)^{2}\right).$

Другим речима, ако недетерминистичка Турингова машина може да реши проблем у меморијском простору f (n), обична, детерминистичка Турингова машина може да реши исти проблем у меморијском простору који је на квадрат већи. Иако се чини да недетерминизам, временом, може да обезбеди експоненцијалне добитке, ова теорема показује да је његов утицај на потребе за меморијским простором у значајној мери ограничен.

Доказ

Доказ теореме демонстрира алгоритам STCON – утврђивање да ли постоји путања између два чвора усмереног графа, који се извршава у простору $O\left((\log n)^{2}\right)$ са n чворова. Основна идеја алгоритма је да рекурзивно реши нешто општији проблем, проверавајући да ли постоји путања од чвора s до чвора t која користи највише k грана, где је k улазни параметар рекурзивног алгоритма. STCON може да се користи за решење овог проблема постављањем k на вредност n. Да би се проверило да ли постоји путања од k грана између чворова s и t, приступ може да буде да се за сваки чвор u графа провери да ли се налази на траженој путањи рекурзивном претрагом путања између чворова s до u и u до t. Користећи псеудокод (синтакса слична језику Пајтон) алгоритам може да се прикаже на следећи начин.

def k_edge_path(s, t, k):
    if k == 0:
        return s == t
    if k == 1:
        return s == t or (s, t) in edges
    for u in vertices:
        if k_edge_path(s, u, floor(k / 2)) and k_edge_path(u, t, ceil(k / 2)):
            return true
    return false

Функција претраге путања позива саму себе до рекурзивне дубине O(log n) и за сваки позив користи O(log n) битова меморије за складиштење аргумената и локалних променљивих, тако да је укупан, потребан меморијски простор за извршење алгоритма $O\left((\log n)^{2}\right)$. Иако је приказани алгоритам овде описан вишим програмским језиком, он може да се имплементира и на Туринговој машини и захтеви за меморијским простором потребним за извршење алгоритма ће остати исти. Разлог, зашто приказани алгоритам имплицира теорему је тај, што било који језик $L\in {\text{NSPACE}}\left(f\left(n\right)\right)$ одговара усмереном графу чији чворови представљају $O\left(2^{f(n)}\right)$ конфигурација Турингове машине који припадају $L$. За свако $x\in \{0,1\}^{n}$, овај граф има путању од почетне конфигурације за улаз $x$ до прихватне конфигурације, ако и само ако важи да $x\in L$. Тако је одговарајућа повезаност довољна да се одлучи о припадности $L$ и приказани алгоритам може да се изврши у меморијском простору ${\text{DSPACE}}\left(\left(f\left(n\right)\right)^{2}\right)$.

Последице

Неке од важних последица теореме су следеће:

• PSPACE = NPSPACE – ово директно следи из чињенице да је квадрат полинома и даље полином,
• NL ⊆ L² - STCON је NL комплетан тако да сви језици који припадају NL, такође припадају класи сложености L² = ${\text{DSPACE}}\left(\left(\log n\right)^{2}\right)$.

Види још

• Immerman–Szelepcsényi theorem

Референце

• Arora, Sanjeev; Barak, Boaz (2009), Computational complexity. A modern approach, Cambridge University Press, ISBN 978-0-521-42426-4, Zbl 1193.68112 
• Papadimitriou, Christos (1993), „Section 7.3: The Reachability Method”, Computational Complexity (1st изд.), Addison Wesley, стр. 149—150, ISBN 0-201-53082-1 
• Savitch, Walter J. (1970), „Relationships between nondeterministic and deterministic tape complexities”, Journal of Computer and System Sciences, 4 (2): 177—192, doi:10.1016/S0022-0000(70)80006-X 
• Sipser, Michael (1997), „Section 8.1: Savitch's Theorem”, Introduction to the Theory of Computation, PWS Publishing, стр. 279—281, ISBN 0-534-94728-X 

Спољашње везе

• Lance Fortnow, Foundations of Complexity, Lesson 18: Savitch's Theorem. Accessed 09/09/09.
• Richard J. Lipton, Savitch’s Theorem. Gives a historical account on how the proof was discovered.