Rice’s Theorem is another of the greatest results achieved in computability. It is one of the foundational theorems that make up computability. It states that all non-trivial semantic properties of programs are undecidable. This means that another program — namely, an algorithm — cannot decide for all the items in a set whether they hold a semantic property or not.
A brief discussion on semantic properties
Properties are basically divided in two fields:
- non-semantic properties (intensional properties);
- semantic properties (extensional properties).
The former are properties that do not concern semantics. You may think of “semantic properties” as regarding what a program does, while “non-semantic properties” are about syntactic properties — like the length of the program (in bytes, lines-of-code, etc.).
We denote such properties with . A property is any subset of .
Let be a property. is said to be semantic (extensional, or closed for extensional equality) if . (Note that denotes the execution of program .)
Theorem
Let be an extensional (semantic) property. is recursive (thus fully decidable) if and only if it is trivial (a property is said to be trivial if ).
Proof
The theorem states “if and only if”, which is mathematically represented as . To prove the theorem is thus necessary to prove both the conclusions from the two assumptions — as we do in Post’s Theorem. In other words, we have to prove: 1) , and 2) .
Let’s start with the first one, which is simpler.
1)
There are two cases:
- . In this case, is recursive (for this set an even stronger property holds: it's regular!).
- . In this case, again, is recursive (it's even regular!).
The former implication has now been proven.
2)
Let’s suppose that is recursive. Then, it has a characteristic function :
Let’s assume, for contradiction, that is non-trivial. Then there exist and (since we assumed is non-trivial, ; it follows that contains some natural numbers, while some others are left out).
We can thus construct a function :
For the First Recursion Theorem by Kleene, it follows that .
Here there’s the contradiction:
- if because is a semantic property (extensional). However, ;
- if . Nonetheless, .
That is why cannot be recursive and non-trivial.