Rice's theorem · which TM properties are decidable?

Rice's theorem is the master undecidability theorem. After proving a handful of specific languages undecidable (E_TM, REGULAR_TM, EQ_TM, …), one starts to wonder: is there a unifying reason? Rice's answer is yes — and it is sweeping. Every nontrivial property of what a program does is undecidable.

This is why static-analysis tools always say "may be" rather than "is". A linter can tell you "this variable is unused" (syntactic, decidable). It cannot tell you "this function returns prime numbers" (semantic, undecidable by Rice).

The theorem is one line, but its consequences span every introductory undecidability lecture in computer science.

The crucial dichotomy:

"Depends only on L(M)" means: if L(M₁) = L(M₂), then P(M₁) = P(M₂). This is the formal definition of semantic.

Assume L_P is decidable. Take a TM T_∅ with L(T_∅) = ∅, and another TM T_P with L(T_P) having property P. (WLOG ∅ does not have P; otherwise apply to ¬P.) Build M' from ⟨M, w⟩:

If M accepts w: L(M') = L(T_P) has P. If M does not accept w: L(M') = ∅ does not have P. So ⟨M, w⟩ ∈ A_TM ⇔ ⟨M'⟩ ∈ L_P. A decider for L_P ⇒ decider for A_TM. Contradiction. ∎

Apply Rice to the property P = "L(M) contains the binary encoding of some prime."

1. Nontrivial? Yes — TM₁ = "accept only 10" has P (10 = 2 is prime). TM₂ = "accept only 1" lacks P.
2. Semantic? Yes — depends only on L(M), not on how M is written.

So "does this program ever accept a prime?" is undecidable. By the same argument, every program-behavior question about output is undecidable in general. This is why pattern-matching and runtime testing replace formal verification in everyday practice.

• E_TM · P = "L(M) is empty" — special case.
• REGULAR_TM · P = "L(M) is regular" — special case.
• EQ_TM · Not directly Rice (it's about pairs), but provable via the same technique.
• Software verification · Every interesting correctness property of a program is undecidable by Rice. Tools work around this with approximation, restricted languages, or interactive proof.
• Theorem-proving · The set of TM descriptions whose languages contain some valid theorem is undecidable.

1. "Rice says everything is undecidable." No — only nontrivial semantic properties. Syntactic and trivial ones can be decidable.
2. Confusing "M halts on w" with "L(M) ∋ w". Different! "M halts" includes rejecting halts; "w ∈ L(M)" means M accepts. The first is HALT_TM, the second is A_TM — both undecidable by reduction, but different statements.
3. "P is nontrivial" must check both sides. Some L(M) has P and some L(M) doesn't. If P is true of every recognizable language (e.g. "L(M) is recognizable"), it's trivial.
4. Forgetting the construction direction. Reduce A_TM to L_P, not the reverse.
5. "Recursion theorem is needed." Not for the reduction proof. The recursion theorem gives an alternative shorter proof but isn't required.

• Q1. Why must P be nontrivial?
  A trivial property (true for all TMs or for none) is trivially decidable. Rice's theorem only kicks in once there are both yes-TMs and no-TMs.
• Q2. Why must P depend only on L(M)?
  If two TMs with the same language can differ on P (e.g., "M has 5 states"), then P isn't a property of the language at all — and Rice doesn't apply.
• Q3. Sketch the proof.
  Suppose D decides L_P. By recursion theorem, build M that asks "what does D(⟨M⟩) say?" and then has language designed to contradict D's answer. Contradiction.
• Q4. Give a decidable property of TMs.
  Any structural one: number of states, alphabet size, whether M has a transition on input 0. None of these are properties of L(M).
• Q5 (bonus). Does Rice apply to NFA / DFA / CFG?
  No — these models have decidable language properties (emptiness, equivalence for DFA, etc.). Rice needs the full power of TMs, where simulating arbitrary computation makes everything semantic undecidable.

Total time: 12 minutes.

• (1 min) Motivation: "We've seen E_TM, REGULAR_TM, etc. all undecidable. Why?"
• (2 min) State Rice's theorem. Define semantic vs syntactic via table on the board.
• (3 min) Sketch the construction of M' and the reduction.
• (3 min) Run the visualization. For each property, ask the audience to vote "applies / doesn't apply" before revealing.
• (2 min) Worked example: "is there a program that checks if any program ever outputs a prime?" No.
• (1 min) Real-world bridge: this is the formal reason static analyzers are conservative.