skip to content

Rice's theorem covers every nontrivial semantic property of a program, so which questions about a program does it not cover?

level: middleimportance: nice to knowfreq 28%

answer

  1. some questions sit outside the theorem
  2. trivial means constant, not simple
  3. text properties are read, not run
  4. how it runs versus what it computes
  5. outside is not the same as decidable

basics

~20 s

Three families sit outside it: trivial properties that hold for all programs or none, properties of the program text such as instruction counts, and properties of how a run proceeds, such as finishing inside a fixed step budget. Outside does not mean decidable.

solid answer

~40 s

Rice's theorem is a statement about *nontrivial* properties of the function a program computes, and each of those two qualifiers marks an exclusion. Trivial properties, true of every program or of none, are decidable by a constant answer. Properties of the text — instruction counts, whether a construct appears, whether the program type-checks — are decidable by parsing, because two programs with identical behaviour can disagree on them. And properties of *how* a computation proceeds rather than *what* it computes sit outside too: whether a given program halts on a given input within a thousand steps is decidable by simulating a thousand steps. The caveat that matters: falling outside the theorem does not make a question decidable. Plenty of questions about how a program runs are still undecidable; they just need a different argument.

code

pseudocode · 7 lines
pseudocode
function halts_within(P, input, k):
    state = initial_state(P, input)
    for step = 1 to k:
        if state is final:
            return YES
        state = step_once(state)
    return NO_WITHIN_BUDGET

go deeper

for a junior

Remember that a tool can answer questions about the shape of the code exactly, and that adding a fixed budget to a behavioural question can make it answerable too.

for a middle

Explain the membership test out loud: could two programs computing the same function disagree on this answer? Then say which of the three exclusions the example falls into.

for a senior

Use the distinction when designing checks. Re-aiming a rule at the text or bounding its search is how you make an imprecise check usable without pretending the exact one exists.

for a principal

Watch for the inverted inference in design reviews, where a team concludes that a question outside the theorem must therefore be answerable, and budgets a project on it.

## The two qualifiers are the whole answer The theorem reads: every **nontrivial** property of the **function a program computes** is undecidable. Each bold phrase is a door out. Anything that fails one of them is not covered — which is not at all the same as being easy. ## Exclusion one: trivial properties A property is trivial when it holds for every computable function, or for none. Examples: 'this program computes some partial function' is true of every program; 'this program computes a function no program can compute' is false for every program. Either one is decided by a procedure that ignores its input and prints a constant. This exclusion is not useful in practice — trivial properties tell you nothing about a specific program — but it is the reason the theorem has to say nontrivial at all. Weak candidates read nontrivial as 'complicated'. It means 'not constant'. ## Exclusion two: properties of the text These are the checks a review gate answers exactly: - how many instructions, statements or declarations the program contains; - whether a particular construct appears anywhere in it; - whether every declared name is mentioned again; - whether the program passes a type check. The membership test is mechanical: **could two programs that compute exactly the same input-to-output function get different answers?** If yes, the property is not a property of the computed function and the theorem is silent about it. Length, nesting depth and instruction count all fail that test immediately, because the same function can be written a thousand different ways. Type checking deserves a sentence of its own, because it is the counterexample people reach for. A type checker looks like it decides a semantic question — 'does this program ever apply an operation to the wrong kind of value?' — and that question really is undecidable. The checker does not decide it. It decides a *syntactic approximation* of it, and pays for the exactness by rejecting some programs that would in fact never have misbehaved. A different question is being answered, and that is exactly why it terminates. ## Exclusion three: properties of the run, not of the result This is the subtle one. Some questions are about how the computation unfolds rather than about the input-to-output relation it realises: - does this program, on this input, halt within one thousand steps? - does it execute a particular block at least once on this input? - does it allocate more than a fixed number of cells before producing an answer? Two programs computing the identical function can disagree on every one of these, so none of them is a property of the computed function, and the theorem does not reach them. The bounded ones are decidable outright, by the most boring method available: run the program for the stated budget and see. | Question | Covered by Rice's theorem? | Decidable? | |---|---|---| | Does the computed function ever return a negative value? | Yes, nontrivial and semantic | No | | Is the computed function total? | Yes, nontrivial and semantic | No | | Does the source contain a loop construct? | No, a property of the text | Yes | | Does it halt on this input within a thousand steps? | No, a property of the run | Yes | | Is this block reachable on some input? | No, a property of the program | No | ## The row that matters most The last row is the one that catches people, and it is worth stating plainly. 'Is this block ever reached?' is not a property of the computed function — a program with a redundant branch computes the same function as one without it — so Rice's theorem does not apply. The question is undecidable anyway, by a reduction from the halting problem. **Falling outside the theorem buys you a different argument, not an exact analyzer.** Anyone who answers 'the theorem does not cover it, so a tool can do it' has inverted the logic. ## Why this distinction earns its keep at work It tells you which escape is available when a check is too imprecise: 1. **Re-aim at the text.** Replace the behavioural rule with a structural one that is exact and conservative. You give up coverage of everything the shape does not catch. 2. **Bound the run.** Ask the question up to a fixed number of steps, loop unrollings or call depth. Inside the bound the answer is exact; beyond it the tool is silent. 3. **Check nontriviality first.** Occasionally a proposed check turns out to be trivially true or trivially false on the inputs that reach it, and the honest fix is to delete it. All three work by changing the question rather than by improving the tool, which is the general shape of every practical escape from this limit.

  • What is the quick test for whether a property is the kind Rice's theorem covers?
    Ask whether two programs that compute exactly the same input-to-output function could receive different answers. If they could — because one is longer, slower, or structured differently — the property is not a property of the computed function and the theorem says nothing about it. If they must always agree, it is, and if it is also nontrivial then it is undecidable.
  • Block reachability is a property of the program rather than of the function it computes, so is it decidable?
    No. Rice's theorem is stated for properties of the computed function, so it does not directly cover 'is this block ever reached'. The question is still undecidable, by a reduction from the halting problem. Falling outside the theorem only means you need a different argument for the same verdict, not that an exact analyzer exists.
  • Why is a terminating type checker not a counterexample to the theorem?
    Because it does not decide the semantic question. It decides a syntactic approximation of it and rejects some programs that would have been safe. The exact behavioural property remains undecidable; the checker simply answers a different, decidable question and accepts the false rejections that come with it.

saying these in an interview costs you the question

  • Says every question about a program is undecidable
  • Thinks nontrivial means complicated rather than not constant
  • Calls a thousand-step halting check undecidable
  • Treats a terminating type checker as refuting the theorem
  • Assumes anything outside the theorem must be decidable