Rice's theorem

Rice's theorem states that every nontrivial semantic property of partial computable functions is undecidable from program descriptions. It applies to properties determined by what programs compute, not how they are written.

Halting problem: The problem of deciding whether an arbitrary program eventually halts on a given input. The contradiction in Rice's theorem's proof would decide this problem.
Turing machine: An abstract model of computation using a finite control, an unbounded tape, and discrete steps. The theorem is commonly formulated for programs modeled as Turing machines.
Static program analysis: The analysis of program properties without executing the program on specific inputs. Rice's theorem sets a boundary on what static analysis can decide for arbitrary programs.
Rice–Shapiro theorem: A characterization of effectively enumerable extensional properties of partial computable functions. It refines Rice's theorem by identifying which semantic properties are semidecidable.
Many-one reduction: A computable transformation that converts instances of one decision problem into instances of another while preserving answers. A program and input are encoded into a new program whose property reveals whether the original halts.
Gödel numbering: A systematic encoding that assigns natural numbers to formal expressions or computational objects. Program descriptions must be encoded so an algorithm can take them as input.
Program verification: The use of mathematical methods to establish whether programs satisfy specified correctness conditions. A nontrivial correctness property of computed behavior cannot be decided for every arbitrary program.
Rice's theorem for recursively enumerable sets: An undecidability result stating that every nontrivial extensional property of recursively enumerable sets is undecidable. This related formulation applies the same pattern to sets recognized by programs.
Program semantics: The meaning of a program, commonly described by its behavior or computed function. Rice's theorem concerns properties of program meaning rather than source form.
Partial function: A function defined only on a subset of its possible inputs. Nontermination makes computed functions partial, the setting behind Rice's theorem.

Linked from 17 pages