ในทฤษฎีความซับซ้อนของการคำนวณทฤษฎีบทของ Savitchซึ่งพิสูจน์โดยWalter Savitchในปี 1970 ^{[ 1 ]} ให้ความสัมพันธ์ระหว่าง ความซับซ้อนของพื้นที่แบบกำหนดและแบบไม่กำหนดโดยระบุว่าสำหรับฟังก์ชันที่สร้างพื้นที่ได้ ใดๆ${\displaystyle f\in \Omega (\log(n))}$[ ^{2 ]​}

${\displaystyle {\mathsf {NSPACE}}\left(f\left(n\right)\right)\subseteq {\mathsf {DSPACE}}\left(f\left(n\right)^{2}\right).}$

กล่าวอีกนัยหนึ่งคือ หากเครื่องจักรทัวริงแบบไม่กำหนดสามารถแก้ปัญหาโดยใช้${\displaystyle f(n)}$พื้นที่เครื่องจักรทัวริงแบบกำหนดได้สามารถแก้ปัญหาเดียวกันได้ในพื้นที่ขนาดกำลังสองของขอบเขตพื้นที่นั้น^{[ 3 ]} แม้ว่าดูเหมือนว่าการไม่กำหนดอาจทำให้เกิดผลกำไรแบบเลขชี้กำลังในเวลา (ตามที่กำหนดไว้ในสมมติฐานเวลาเลขชี้กำลัง ที่ยังไม่ได้รับการพิสูจน์ ) ทฤษฎีบทของ Savitch แสดงให้เห็นว่ามีผลกระทบต่อความต้องการพื้นที่ที่จำกัดอย่างเห็นได้ชัด^{[ 4 ]}

ทฤษฎีบทนี้สามารถทำให้สัมพันธ์กันได้กล่าวคือ สำหรับออราเคิลใดๆ การแทนที่ "เครื่องจักรทัวริง" ทุกเครื่องด้วย "เครื่องจักรทัวริงออราเคิล" ก็ยังคงส่งผลให้ได้ทฤษฎีบทอยู่ดี^{[ 5 ]}

การพิสูจน์นี้อาศัยอัลกอริทึมสำหรับSTCONซึ่งเป็นปัญหาในการพิจารณาว่ามีเส้นทางระหว่างจุดสองจุดในกราฟแบบมี ทิศทางหรือ ไม่ ซึ่งทำงานใน${\displaystyle O\left((\log n)^{2}\right)}$พื้นที่สำหรับ${\displaystyle n}$จุดยอด แนวคิดพื้นฐานของอัลกอริธึมนี้คือการแก้ ปัญหาทั่วไปที่ค่อนข้างซับซ้อนกว่านั้น แบบเรียกซ้ำโดยทดสอบการมีอยู่ของเส้นทางจากจุดยอดหนึ่งไปยังอีกจุดหนึ่ง${\displaystyle s}$ไปยังจุดยอดอื่น${\displaystyle t}$ที่ใช้มากที่สุด${\displaystyle k}$ขอบ สำหรับพารามิเตอร์${\displaystyle k}$กำหนดให้เป็นข้อมูลป้อนเข้า STCON เป็นกรณีพิเศษของปัญหานี้ โดยที่${\displaystyle k}$ตั้งค่าให้มีขนาดใหญ่พอที่จะไม่จำกัดเส้นทาง (ตัวอย่างเช่น เท่ากับจำนวนจุดยอดทั้งหมดในกราฟ หรือค่าใดๆ ที่มากกว่านั้น) เพื่อทดสอบ${\displaystyle k}$เส้นทางขอบจาก${\displaystyle s}$ถึง${\displaystyle t}$อัลกอริทึมเชิงกำหนดสามารถวนซ้ำผ่านจุดยอดทั้งหมดได้${\displaystyle u}$และค้นหาเส้นทางที่มีความยาวครึ่งหนึ่งจากจุดนั้นซ้ำๆ${\displaystyle s}$ถึง${\displaystyle u}$และจาก${\displaystyle u}$ถึง${\displaystyle t}$[ ^{6 ] อัลกอริ ทึม} นี้สามารถแสดงเป็นรหัสเทียม (ใน ไวยากรณ์ Python ) ได้ดังนี้:

def stcon ( s , t ) -> bool : """ทดสอบว่ามีเส้นทางที่มีความยาวใดๆ จาก s ไปยัง t หรือไม่""" return k_edge_path ( s , t , n ) # n คือจำนวนจุดยอดdef k_edge_path ( s , t , k ) -> bool : """ทดสอบว่ามีเส้นทางที่มีความยาวไม่เกิน k จาก s ไปยัง t หรือไม่""" 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

เนื่องจากการเรียกซ้ำแต่ละครั้งจะลดค่าพารามิเตอร์ลงครึ่งหนึ่ง${\displaystyle k}$จำนวนระดับของการเรียกซ้ำคือ${\displaystyle \lceil \log _{2}n\rceil }$แต่ละระดับต้องใช้${\displaystyle O(\log n)}$บิตของพื้นที่จัดเก็บข้อมูลสำหรับอาร์กิวเมนต์ของฟังก์ชันและตัวแปรโลคอล :${\displaystyle k}$และจุดยอด${\displaystyle s}$,${\displaystyle t}$, และ${\displaystyle u}$จำเป็นต้อง${\displaystyle \lceil \log _{2}n\rceil }$บิตต่อบิต ดังนั้นความซับซ้อนของพื้นที่เสริม โดยรวม จึงเป็นดังนี้${\displaystyle O\left((\log n)^{2}\right)}$[ ^{6 ]}กราฟอินพุตถือว่าถูกแสดงในหน่วยความจำแบบอ่านอย่างเดียวแยกต่างหากและไม่ส่งผลต่อขอบเขตพื้นที่เสริมนี้ หรืออาจแสดงเป็น^กราฟโดยปริยายก็ได้แม้ว่าข้างต้นจะอธิบายไว้ในรูปแบบของโปรแกรมในภาษาระดับสูง แต่อัลกอริธึมเดียวกันนี้ก็สามารถนำไปใช้ได้โดยมีขอบเขตพื้นที่เชิงอะซิมโทติกเดียวกันบนเครื่องทัวริง

อัลกอริทึมนี้สามารถนำไปใช้กับกราฟโดยปริยายซึ่งจุดยอดแทนการกำหนดค่าของเครื่องจักรทัวริงแบบไม่กำหนดและเทปของมัน โดยทำงานภายในขอบเขตพื้นที่ที่กำหนด${\displaystyle f(n)}$เส้นเชื่อมในกราฟนี้แสดงถึงการเปลี่ยนสถานะแบบไม่แน่นอนของเครื่องจักร${\displaystyle s}$ถูกตั้งค่าเป็นการกำหนดค่าเริ่มต้นของเครื่อง และ${\displaystyle t}$กำหนดให้เป็นจุดยอดพิเศษที่แสดงถึงสถานะหยุดการทำงานที่ยอมรับได้ทั้งหมด ในกรณีนี้ อัลกอริทึมจะส่งคืนค่าจริงเมื่อเครื่องมีเส้นทางการยอมรับที่ไม่แน่นอน และส่งคืนค่าเท็จในกรณีอื่น ๆ จำนวนการกำหนดค่าในกราฟนี้คือ${\displaystyle O(2^{f(n)})}$จากนั้นจึงสรุปได้ว่า การนำอัลกอริทึมไปใช้กับกราฟโดยปริยายนี้จะใช้พื้นที่${\displaystyle O(f(n)^{2})}$ดังนั้นโดยการตัดสินใจเกี่ยวกับการเชื่อมต่อในกราฟที่แสดงถึงการกำหนดค่าเครื่องทัวริงแบบไม่กำหนด เราสามารถตัดสินใจเกี่ยวกับการเป็นสมาชิกในภาษาที่เครื่องนั้นรู้จักได้ ในพื้นที่ที่เป็นสัดส่วนกับกำลังสองของพื้นที่ที่เครื่องทัวริงใช้^{[ 6 ]}

บทสรุปที่สำคัญบางประการของทฤษฎีบทนี้ ได้แก่:

PSPACE = NPSPACE

กล่าวคือ ภาษาที่สามารถรับรู้ได้โดยเครื่องทัวริงแบบปริภูมิพหุนามเชิงกำหนดและเครื่องทัวริงแบบปริภูมิพหุนามเชิงไม่กำหนดนั้นเหมือนกัน ซึ่งเป็นผลมาจากข้อเท็จจริงที่ว่ากำลังสองของฟังก์ชันพหุนามยังคงเป็นฟังก์ชันพหุนาม^{[ 6 ]}เชื่อกันว่าไม่มีความสัมพันธ์ที่คล้ายกันระหว่างคลาสความซับซ้อนของเวลาพหุนามPและNPแม้ว่านี่จะเป็นคำถามที่ยังเปิดอยู่ก็ตาม

NL ⊆ L ²

กล่าวคือ ภาษาทั้งหมดที่สามารถแก้ได้แบบไม่แน่นอนในปริภูมิเชิงลอการิทึม สามารถแก้ได้แบบแน่นอนในระดับความซับซ้อน$${\displaystyle {\mathsf {\color {Blue}L}}^{2}={\mathsf {DSPACE}}\left(\left(\log n\right)^{2}\right).}$$นี่เป็นผลมาจากข้อเท็จจริงที่ว่า STCON เป็นภาษาที่สมบูรณ์แบบในเชิงเนม (NL-complete )

• ทฤษฎีบท Immerman–Szelepcsényi – การปิดของปริภูมิไม่กำหนดภายใต้การเติมเต็ม 

• Lance Fortnow, Foundations of Complexity, บทที่ 18: ทฤษฎีบทของ Savitchเข้าถึงเมื่อ 2009-09-09
• ริชาร์ด เจ. ลิปตัน , ทฤษฎีบทของซาวิตช์ให้ข้อมูลทางประวัติศาสตร์เกี่ยวกับวิธีการค้นพบการพิสูจน์