ในทฤษฎีความสามารถในการคำนวณทฤษฎีบทของไรซ์กล่าวว่า คุณสมบัติทางความหมายที่ไม่ใช่คุณสมบัติพื้นฐานทั้งหมดของโปรแกรมนั้นไม่สามารถตัดสินได้คุณสมบัติทางความหมายคือคุณสมบัติเกี่ยวกับพฤติกรรมของโปรแกรม (ตัวอย่างเช่น "โปรแกรมจะสิ้นสุดการทำงานสำหรับอินพุตทั้งหมดหรือไม่"?) ซึ่งแตกต่างจากคุณสมบัติทางไวยากรณ์ (ตัวอย่างเช่น "โปรแกรมมี คำสั่ง if-then-else หรือไม่ "?) คุณสมบัติ ที่ไม่ใช่คุณสมบัติพื้นฐานคือคุณสมบัติที่ไม่เป็นจริงสำหรับทุกโปรแกรม และไม่เป็นเท็จสำหรับทุกโปรแกรม

ทฤษฎีบทนี้เป็นการขยายความไม่สามารถตัดสินได้ของปัญหาการหยุดทำงานมันมีนัยสำคัญอย่างมากต่อความเป็นไปได้ของการวิเคราะห์โปรแกรมแบบสถิตมันหมายความว่า ตัวอย่างเช่น เป็นไปไม่ได้ที่จะสร้างเครื่องมือที่ตรวจสอบว่าโปรแกรมใด ๆ นั้นถูกต้องหรือไม่ หรือแม้กระทั่งทำงานได้โดยไม่มีข้อผิดพลาด (เป็นไปได้ที่จะสร้างเครื่องมือที่ประเมินค่าสูงเกินไปหรือต่ำเกินไปเสมอ ดังนั้นในทางปฏิบัติจึงต้องตัดสินใจว่าอะไรเป็นปัญหาที่น้อยกว่า)

ทฤษฎีบทนี้ตั้งชื่อตามเฮนรี กอร์ดอน ไรซ์ผู้พิสูจน์ทฤษฎีบทนี้ในวิทยานิพนธ์ระดับปริญญาเอกของเขาในปี 1951 ที่มหาวิทยาลัยซีราคิวส์

ทฤษฎีบทของไรซ์ได้กำหนดขอบเขตทางทฤษฎีว่าการวิเคราะห์แบบคงที่ ประเภทใดบ้าง ที่สามารถทำได้โดยอัตโนมัติ เราสามารถแยกแยะความแตกต่างระหว่างไวยากรณ์ของโปรแกรมและความหมาย ของมัน ได้ ไวยากรณ์คือรายละเอียดของวิธีการเขียนโปรแกรม หรือ "เจตนา" ของมัน และความหมายคือวิธีการทำงานของโปรแกรมเมื่อรัน หรือ "ส่วนขยาย" ของมัน ทฤษฎีบทของไรซ์กล่าวว่า เป็นไปไม่ได้ที่จะตัดสินคุณสมบัติของโปรแกรมที่ขึ้นอยู่กับความหมายเท่านั้นและไม่ขึ้นอยู่กับไวยากรณ์ เว้นแต่ว่าคุณสมบัตินั้นจะเป็นเรื่องง่าย (เป็นจริงสำหรับทุกโปรแกรม หรือเป็นเท็จสำหรับทุกโปรแกรม)

ตามทฤษฎีของไรซ์ เป็นไปไม่ได้ที่จะเขียนโปรแกรมที่ตรวจสอบโดยอัตโนมัติว่าไม่มีข้อผิดพลาดในโปรแกรมอื่น โดยรับโปรแกรมและข้อกำหนดเป็นอินพุต และตรวจสอบว่าโปรแกรมนั้นตรงตามข้อกำหนดหรือไม่

นี่ไม่ได้หมายความว่าไม่สามารถป้องกัน ข้อผิดพลาด บางประเภทได้ ตัวอย่างเช่น ทฤษฎีบทของไรซ์บ่งชี้ว่าในภาษาโปรแกรมแบบไดนามิกที่มีความสมบูรณ์ของทัวริงนั้น เป็นไปไม่ได้ที่จะตรวจสอบว่าไม่มีข้อผิดพลาดเกี่ยวกับประเภท ในทางกลับกันภาษาโปรแกรมแบบสแตติกมีระบบประเภทที่ป้องกันข้อผิดพลาดเกี่ยวกับประเภทได้โดยอัตโนมัติ โดยพื้นฐานแล้ว ควรเข้าใจว่านี่เป็นคุณลักษณะของไวยากรณ์ (ในความหมายกว้างๆ) ของภาษาเหล่านั้น ในการตรวจสอบประเภทของโปรแกรม จำเป็นต้องตรวจสอบซอร์สโค้ด การดำเนินการไม่ได้ขึ้นอยู่กับความหมายเชิงสมมติของโปรแกรมเพียงอย่างเดียว

ในแง่ของการตรวจสอบความถูกต้องของซอฟต์แวร์โดยทั่วไป หมายความว่า แม้ว่าจะไม่สามารถตรวจสอบด้วยอัลกอริทึมได้ว่าโปรแกรมใด ๆ ตรงตามข้อกำหนดที่กำหนดหรือไม่ แต่เราสามารถกำหนดให้โปรแกรมต้องมีคำอธิบายเพิ่มเติมที่พิสูจน์ได้ว่าโปรแกรมนั้นถูกต้อง หรือเขียนโปรแกรมในรูปแบบที่จำกัดเฉพาะซึ่งทำให้การตรวจสอบเป็นไปได้ และยอมรับเฉพาะโปรแกรมที่ได้รับการตรวจสอบด้วยวิธีนี้เท่านั้น ในกรณีของความปลอดภัยของประเภทข้อมูล แบบแรกจะสอดคล้องกับคำอธิบายประกอบประเภทข้อมูล และแบบหลังจะสอดคล้องกับการอนุมานประเภทข้อมูลเมื่อนำแนวคิดนี้ไปใช้ให้กว้างกว่าความปลอดภัยของประเภทข้อมูล จะนำไปสู่การพิสูจน์ความถูกต้องของโปรแกรมผ่านคำอธิบายประกอบการพิสูจน์ เช่นในตรรกะของ Hoare

อีกวิธีหนึ่งในการแก้ปัญหาตามทฤษฎีบทของไรซ์คือการค้นหาวิธีการที่สามารถตรวจจับ ข้อผิดพลาด ได้หลายจุดโดยที่ไม่สมบูรณ์ นี่คือทฤษฎี การ ตีความ แบบนามธรรม

อีกแนวทางหนึ่งสำหรับการตรวจสอบความถูกต้องคือการตรวจสอบแบบจำลอง (model checking ) ซึ่งสามารถใช้ได้กับโปรแกรมสถานะจำกัด (finite-state programs) เท่านั้น ไม่ใช่ภาษาที่สมบูรณ์แบบตามทฤษฎีบททัวริง (Turing-complete languages)

ให้เป็นการกำหนดหมายเลขที่ยอมรับได้ของฟังก์ชันที่คำนวณได้บางส่วนและให้เป็นเซตย่อยของสมมติว่า: ${\displaystyle \varphi }$${\displaystyle P}$${\displaystyle \mathbb {N} }$

1. ${\displaystyle P}$ไม่ใช่เรื่องเล็กน้อย : ไม่ใช่ทั้งสิ่งว่างเปล่าและไม่ใช่ตัวของมันเอง${\displaystyle P}$${\displaystyle \mathbb {N} }$
2. ${\displaystyle P}$เป็นคุณสมบัติขยาย : สำหรับจำนวนเต็มทั้งหมดและถ้าแล้ว${\displaystyle m}$${\displaystyle n}$${\displaystyle \varphi _{m}=\varphi _{n}}$${\displaystyle m\in P\iff n\in P}$

ดังนั้นจึงไม่สามารถตัดสินได้ ${\displaystyle P}$

สามารถกล่าวให้กระชับยิ่งขึ้นได้โดยใช้ชุดดัชนี : ชุดดัชนีที่ตัดสินได้มีเพียงและเท่านั้น ${\displaystyle \varnothing }$${\displaystyle \mathbb {N} }$

กำหนดให้โปรแกรมPรับจำนวนธรรมชาติnและส่งคืนจำนวนธรรมชาติP ( n ) คำถามต่อไปนี้ไม่สามารถตัดสินได้:

• โปรแกรม Pจะหยุดทำงานเมื่อกำหนดค่าn ที่กำหนด หรือไม่ (นี่คือปัญหาการหยุดทำงาน )
• Pสิ้นสุดที่ 0 หรือไม่ ?
• Pสิ้นสุดที่ทุกค่าnหรือไม่(กล่าวคือP เป็น ปริภูมิสมบูรณ์หรือไม่ )?
• โปรแกรม Pสิ้นสุดการทำงานและส่งคืนค่า 0 สำหรับทุกอินพุตหรือไม่ ?
• โปรแกรม Pจะสิ้นสุดการทำงานและส่งคืนค่า 0 เมื่อได้รับอินพุตบางอย่างหรือ ไม่?
• ฟังก์ชัน Pสิ้นสุดการทำงานและส่งคืนค่าเดียวกันสำหรับอินพุตทั้งหมดหรือไม่ ?
• Pเทียบเท่ากับโปรแกรมQ ที่กำหนดให้ หรือไม่?

สมมติเพื่อหาข้อขัดแย้งว่าเป็นเซตของจำนวนธรรมชาติที่ไม่เป็นศูนย์มีคุณสมบัติขยายได้และคำนวณได้ เนื่องจากเป็นเซตที่ไม่เป็นศูนย์ จึงมีจำนวนธรรมชาติและจำนวนธรรมชาติกำหนดฟังก์ชันที่คำนวณได้ทั้งหมดของและโดยเมื่อและเมื่อตามทฤษฎีบทเวียนเกิดของคลีนจะมีอยู่เช่นนั้นดังนั้น ถ้าเราจะได้ซึ่งขัดแย้งกับคุณสมบัติขยายได้ของเนื่องจากและในทางกลับกัน ถ้าเราจะได้ซึ่งขัดแย้งกับคุณสมบัติขยายได้อีกครั้งเนื่องจาก ${\displaystyle P}$${\displaystyle P}$${\displaystyle a\in P}$${\displaystyle b\notin P}$${\displaystyle Q}$${\displaystyle e}$${\displaystyle x}$${\displaystyle Q_{e}(x)=\varphi _{b}(x)}$${\displaystyle e\in P}$${\displaystyle Q_{e}(x)=\varphi _{a}(x)}$${\displaystyle e\notin P}$${\displaystyle e}$${\displaystyle \varphi _{e}=Q_{e}}$${\displaystyle e\in P}$${\displaystyle \varphi _{e}=\varphi _{b}}$${\displaystyle P}$${\displaystyle b\notin P}$${\displaystyle e\notin P}$${\displaystyle \varphi _{e}=\varphi _{a}}$${\displaystyle a\in P}$

สมมติเพื่อความชัดเจน ว่าเรามีอัลกอริทึมสำหรับตรวจสอบโปรแกรมpและตัดสินได้อย่างแม่นยำว่าpเป็นการใช้งานฟังก์ชันยกกำลังสองหรือไม่ ซึ่งฟังก์ชันนี้รับค่าจำนวนเต็มdและส่งคืนค่า^d² การพิสูจน์นี้ใช้ได้ผลเช่นเดียวกันหากเรามีอัลกอริทึมสำหรับตัดสินคุณสมบัติอื่น ๆ ที่ไม่ใช่คุณสมบัติพื้นฐานทั่วไปของพฤติกรรมโปรแกรม (เช่น คุณสมบัติเชิงความหมายและคุณสมบัติพื้นฐานทั่วไป) และจะแสดงไว้โดยทั่วไปด้านล่าง

ข้ออ้างคือเราสามารถแปลงอัลกอริธึมของเราสำหรับการระบุโปรแกรมยกกำลังสองให้เป็นอัลกอริธึมที่ระบุฟังก์ชันที่หยุดทำงานได้ เราจะอธิบายอัลกอริธึมที่รับอินพุตaและiและตรวจสอบว่าโปรแกรมa หยุดทำงานหรือ ไม่ เมื่อได้รับอินพุตi

อัลกอริทึมสำหรับการตัดสินใจนี้เรียบง่ายในเชิงแนวคิด: มันสร้าง (คำอธิบายของ) โปรแกรมใหม่tที่รับอาร์กิวเมนต์nซึ่ง (1) ขั้นแรกจะดำเนินการโปรแกรมaกับอินพุตi (ทั้งaและiถูกกำหนดไว้ในนิยามของt ) และ (2) จากนั้นส่งคืนค่ากำลังสองของnหากa ( i ) ทำงานไปเรื่อยๆtจะไม่ไปถึงขั้นตอน (2) เลย ไม่ว่าn จะเป็นอย่างไรก็ตาม เห็นได้ชัดว่า tเป็นฟังก์ชันสำหรับการคำนวณกำลังสองก็ต่อเมื่อขั้นตอน (1) สิ้นสุดลง เนื่องจากเราได้สมมติว่าเราสามารถระบุโปรแกรมสำหรับการคำนวณกำลังสองได้อย่างแม่นยำ เราจึงสามารถกำหนดได้ว่าtซึ่งขึ้นอยู่กับaและiเป็นโปรแกรมดังกล่าวหรือไม่ ดังนั้นเราจึงได้โปรแกรมที่ตัดสินใจว่าโปรแกรมaหยุดทำงานเมื่อรับอินพุตiหรือไม่ โปรดทราบว่าอัลกอริทึมการตัดสินใจหยุดทำงานของเราจะไม่ดำเนินการtแต่จะส่งคำอธิบายไปยังโปรแกรมระบุค่ากำลังสอง ซึ่งตามสมมติฐานแล้วจะสิ้นสุดลงเสมอ เนื่องจากการสร้างคำอธิบายของtสามารถทำได้ในลักษณะที่สิ้นสุดเสมอ ดังนั้นการตัดสินใจหยุดจึงไม่สามารถล้มเหลวในการหยุดได้เช่นกัน

หยุด (a,i) { กำหนด t(n) { AI) ส่งคืน n×n } คืนค่าเป็นฟังก์ชันกำลังสอง(t) } 

วิธีการนี้ไม่ได้ขึ้นอยู่กับความสามารถในการจดจำฟังก์ชันที่คำนวณกำลังสองโดยเฉพาะ ตราบใดที่ โปรแกรม บางโปรแกรมสามารถทำในสิ่งที่เราพยายามจดจำได้ เราก็สามารถเพิ่มการเรียกใช้ฟังก์ชันaเพื่อรับค่าt ของเรา ได้ เราอาจมีวิธีการจดจำโปรแกรมสำหรับการคำนวณรากที่สอง หรือโปรแกรมสำหรับการคำนวณเงินเดือนรายเดือน หรือโปรแกรมที่หยุดทำงานเมื่อได้รับอินพุต"Abraxas"ในแต่ละกรณี เราจะสามารถแก้ปัญหาการหยุดทำงานได้ในลักษณะเดียวกัน

สำหรับการพิสูจน์อย่างเป็นทางการนั้น สมมติว่าอัลกอริทึมกำหนดฟังก์ชันบางส่วนบนสตริงและตัวอัลกอริทึมเองก็ถูกแทนด้วยสตริงเช่นกัน ฟังก์ชันบางส่วนที่คำนวณโดยอัลกอริทึมซึ่งแทนด้วยสตริงaจะถูกเขียนแทน ด้วย F การพิสูจน์นี้ดำเนินไปโดย การหักล้างโดย ปริยาย (reductio ad absurdum) : เราสมมติว่ามีคุณสมบัติที่ไม่ธรรมดาซึ่งถูกตัดสินโดยอัลกอริทึม จากนั้นแสดงให้เห็นว่ามันตามมาว่าเราสามารถตัดสินปัญหาการหยุดทำงานได้ซึ่งเป็นไปไม่ได้ และดังนั้นจึงเป็นข้อขัดแย้ง

สมมติว่าP ( a ) เป็นอัลกอริทึมที่ตัดสินคุณสมบัติที่ไม่ธรรมดาบางอย่างของF( โดยไม่เสียความเป็นทั่วไป เราอาจสมมติว่าP ( no-halt ) = "ไม่" โดยที่no-haltเป็นการแทนอัลกอริทึมที่ไม่หยุดทำงานเลย หากไม่เป็นเช่นนั้น แสดงว่าอัลกอริทึมPที่คำนวณการปฏิเสธของคุณสมบัติPเป็นจริงเช่นกัน เนื่องจากPตัดสินคุณสมบัติที่ไม่ธรรมดา จึงสรุปได้ว่ามีสตริงbที่แทนอัลกอริทึมF( และP ( b ) = "ใช่" จากนั้นเราสามารถกำหนดอัลกอริทึมH ( a , i ) ได้ดังนี้:

1. สร้างสตริงtที่แทนอัลกอริทึมT ( j ) โดยที่

• TจำลองการคำนวณF ( i ) ก่อน
• จากนั้นTจะจำลองการคำนวณของF ( j ) และส่งคืนผลลัพธ์

2. คืนค่าP ( t )

ตอนนี้เราสามารถแสดงได้ว่าHเป็นตัวตัดสินปัญหาการหยุดทำงาน:

• สมมติว่าอัลกอริทึมที่แสดงด้วยaหยุดทำงานเมื่อได้รับอินพุตiในกรณีนี้F = F และเนื่องจากP ( b ) = "ใช่" และผลลัพธ์ของP ( x ) ขึ้นอยู่กับF เท่านั้น จึงสรุปได้ว่าP ( t ) = "ใช่" และด้วยเหตุนี้H ( a , i ) = "ใช่"
• สมมติว่าอัลกอริทึมที่แสดงโดยaไม่หยุดทำงานเมื่อได้รับอินพุตiในกรณีนี้F = F นั่นคือ ฟังก์ชันบางส่วนที่ไม่เคยถูกนิยาม เนื่องจากP ( no-halt ) = "no" และผลลัพธ์ของP ( x ) ขึ้นอยู่กับF เท่านั้น จึงสรุปได้ว่าP ( t ) = "no" และด้วยเหตุนี้H ( a , i ) = "no"

เนื่องจากปัญหาการหยุดทำงานเป็นที่ทราบกันดีว่าไม่สามารถตัดสินได้ นี่จึงเป็นข้อขัดแย้ง และสมมติฐานที่ว่ามีอัลกอริทึมP ( a ) ที่ตัดสินคุณสมบัติที่ไม่ธรรมดาสำหรับฟังก์ชันที่แสดงโดยa นั้นจะต้องเป็นเท็จ

• ปัญหาการหยุด
• ทฤษฎีบท Rice–Shapiroและทฤษฎีบท Kreisel–Lacombe–Shoenfield–Tseitinซึ่งเป็นการขยายความของทฤษฎีบทของ Rice
• ทฤษฎีบทสกอตต์-เคอร์รีซึ่งเป็นทฤษฎีบทที่คล้ายคลึงกับทฤษฎีบทไรซ์ในแคลคูลัสแลมบ์ดา
• การพิสูจน์ของทัวริง