Rice's Theorem

Mathematical Logic · Axiom Academy

Discover the profound theoretical limits on what we can automatically determine about programs and their behavior. 1. The Dream: Automatically Analyzing Programs Imagine you have a program and you want to know something about it. Maybe you want to know: It would be incredibly useful if we could write an analyzer that automatically answers these questions. We could use it for optimization, security analysis, bug detection, and more! 2. Semantic vs. Syntactic Properties Before we state Rice's Theorem, we need to understand the crucial distinction between semantic and syntactic properties of programs. 3. What Does "Non-Trivial" Mean? Rice's Theorem applies to non-trivial properties. A property is non-trivial if some programs have it and some programs don't. 4. Rice's Theorem: The Statement More precisely: Let P be any non-trivial property of partial computable functions (i.e., functions computed by Turing machines). Then the set is undecidable. That is, there is no algorithm that can determine, given an arbitrary Turing machine M, whether the function computed by M has property P. 5. Proof Strategy: Reduction from the Halting Problem We prove Rice's Theorem by showing that if we could decide any non-trivial semantic property, we could solve the Halting Problem—which we know is impossible!

This is the written version of the interactive lesson above. See the full Mathematical Logic course.