# Rice’s theorem

## An interactive tutorial

Turing famously showed that computers can’t decide whether your code halts. But in 1951, Henry Rice proved a much more devastating result: “computers can’t decide *anything* interesting about your code’s input-output!” In this chapter, you’ll learn exactly what he meant, and how he proved it, by building on Turing’s famous theorem.

Let’s start with a very practical question: can you replace a function with a regular expression? Imagine, one day at work, you come across this function in the codebase:

```
function isNumeric(str: string) {
if (str === "") return false;
for (const c of str) {
if (!"0123456789".includes(c))
return false;
}
return true;
}
```

Hmm, you think ... could calls to this function be replaced by a regular expression test, like `/a+/.test(str)`

?

Yeah, we could replace it with something like:

Actually, I think it could. We could replace it with something like this:

```
function isNumericRegex(s: string) {
return /^[0-9]+$/.test(s);
}
```

But wouldn’t it be cool if your IDE gave you a refactoring hint? Imagine: “function `isNumeric`

can be replaced by a regular expression.” The IDE is smart enough to give us other hints, like “unused variable”. Would this regular expression test be much harder?

## Warm-up: `canBeRegex`

If your IDE could make this decision, it would have an internal function like this:

```
function canBeRegex(funcStr: string) {
/* Complex logic here */
}
```

`canBeRegex`

takes the source code for a function, analyzes it, and returns `true`

or `false`

, telling us whether the function could be replaced with a regular expression. For example, what should the following call return?

```
canBeRegex(`
function isLen3(s: string) {
return s.length === 3;
}
`)
```

Yes, it could be replaced by the regex `^...$`

, for example.

Actually, I think it should return `true`

. It’s considering this function:

```
function isLen3(s: string) {
return s.length === 3;
}
```

This function could be replaced by the regex `^...$`

, or by `^.{3}$`

, either of which matches strings that have exactly three characters.

Let’s try another function, `bad_isLen3`

:

```
function bad_isLen3(str: string) {
for (let i = 0; i <= 99; i++);
return str.length === 3;
}
```

What should `canBeRegex`

return when given the source code of `bad_isLen3`

?

Yeah: `bad_isLen3`

does some useless upfront work, but otherwise has the same input-output behavior as `isLen3`

.

Well ... yes, `bad_isLen3`

does some useless upfront work that a regex probably wouldn’t do. But we don’t want our IDE to fuss over the implementation details or efficiency; it should just tell us whether there’s a regex that has the same input-output as the function.

But now what about `awful_isLen3`

:

```
function awful_isLen3(str: string) {
for (let i = 0; i <= i; i++); // hmm
return str.length === 3;
}
```

Actually, this function is **not** replaceable by a regex. That `for`

loop never halts, because `i <= i`

is always true! This means that `awful_isLen3`

never halts, and its input-output is actually equivalent to the `loop`

function:

Right, that `for`

loop never halts! So `awful_isLen3`

never halts, and its input-output is actually equivalent to the `loop`

function:

`function loop(s) { while(true); }`

This is clearly not replaceable by a regex, so `canBeRegex`

should return `false`

on it. Perhaps you see the problem: doesn’t `canBeRegex`

need to decide whether that first line halts?

## That old halting problem again

In Chapter 1, we discovered the halting problem. Here’s a quick reminder:

`function halts(code: string) { ... }`

The `halts`

function is given some JavaScript `code`

in string form, and it must tell us whether it halts. For example, what should this return?

```
halts(`
let x = 1;
while (x > 0) x = x / 2;
`)
```

No, `halts`

should always halt, even if the function that it’s given does not halt!

Alright, there are two reasonable answers here! If you think of `x`

as a real or rational number, `x`

would never reach zero, so `halts`

should return `false`

. But in JavaScript floating-point numbers, it eventually gets to `5e-324 / 2`

, which evaluates to zero, so `halts`

should return `true`

!

The point is: deciding whether code halts is *freaking hard*. And in Chapter 1, we learned Turing’s proof that `halts`

is actually *impossible* to implement: any implementation you write will have a bug!

So, isn’t `canBeRegex`

impossible too? Put on your logician’s hat: what would we need to do to prove that `canBeRegex`

is impossible to write?

No, but this is a common mistake! If you implement `canBeRegex`

using `halts`

, you’re just showing that your *implementation* can’t exist. Perhaps there’s a cleverer way to implement `canBeRegex`

that doesn’t rely on using `halts`

!

However, if you can implement `halts`

using `canBeRegex`

, you’ve got a strong argument that `canBeRegex`

can’t exist. Let’s see how.

Right! If you implement `halts`

using `canBeRegex`

, you’ve got a proof by contradiction that `canBeRegex`

can’t exist.

So, here’s an idea for implementing `halts`

using `canBeRegex`

:

```
function halts(code: string) {
return canBeRegex(`
function isLen3(s: string) {
${code}
return s.length === 3;
}
`);
}
```

Take your time and read it closely! We take our function `isLen3`

, which we know can be replaced with a regex. Then we *inject* the `code`

at the top of that function. Finally, we ask whether the function can still be replaced with a regex after this change.

Does this really solve the halting problem? Let’s check. First, assume that `code`

*does* halt. Now read the above `halts(code)`

: what will it return?

Now assume that `code`

does *not *halt. Then what will the above `halts(code)`

return?

So this does solve the halting problem. But we know that’s impossible! We have a contradiction, so our initial assumption must be false. That is, `canBeRegex`

cannot exist! This trick is the core idea of Rice’s theorem.

## Code isolation

Now for a short interlude. Sharp-eyed readers might wonder whether the injected `${code}`

can “escape its sandbox”. Here’s a tricky example:

`halts(`throw new Error("escape");`)`

The code `throw new Error("escape")`

would halt with an error. But what would `halts`

return, if we use the above implementation?

I think it would return `false`

, because the following function cannot be replaced by a regex:

```
function (str: string) {
throw new Error("escape");
return str.length === 3;
}
```

The bug is that raw string injection like `${code}`

does not isolate the code. So, when we write `${code}`

, think of this as a shorthand for running the code in an isolated sandbox, like this one.

`canHalt`

: maybe an easier question?

So, we showed that we can’t implement `canBeRegex`

, because a regular expression always halts, and we can’t tell whether a function halts.

But perhaps you’re thinking: “A regular expression always halts. So implementing `canBeRegex`

is actually *even harder* than solving the halting problem. This is not so surprising.”

Well, let’s consider a new property, `canHalt`

. Given a function’s source code, it tells us whether there is at least one argument that causes the function to halt. For example, what should this return?

```
canHalt(`function (n: number) {
if (isPrime(n) && isEven(n)) return;
while (true);
}`)
```

Right, the input `2`

would cause this function to halt, because $2$ is a prime number and an even number.

I apologize! This was a bit tricksy! There’s one input that would cause this function to halt: the input `2`

, because $2$ is both a prime number and an even number!

Now, this `canHalt`

property does not imply the function *always* halts. So does Rice’s argument still work to show that `canHalt`

cannot be written? Let’s try running it through the proof anyway! Assume we have `canHalt`

, and then write:

```
function halts(code: string) {
const t = `function ret42() {
${code}
return 42;
}`;
return canHalt(t);
}
```

Check this implementation of `halts`

! If `code`

halts, it should return `true`

, and if `code`

does not halt, it should return `false`

. So, does it correctly solve the halting problem?

I think it *does *solve the halting problem, and here’s why.

First, assume `code`

halts. Then we’re effectively asking whether this function can halt:

```
function ret42() {
return 42;
}
```

It certainly can halt (it *always* does), so `halts`

would return `true`

here.

Then assume `code`

does *not* halt. Then it transforms `ret42`

into the `loop`

function, which cannot halt, so `halts`

would return `false`

here.

Either way, `halts`

returns the correct answer, so it does solve the halting problem.

So, similarly, `canHalt`

is also impossible to implement! Here’s how we were able to prove it. We have two functions, `loop`

and `ret42`

:

```
// does NOT satisfy canHalt
function loop (x) { while (true); }
// DOES satisfy canHalt
function ret42 (x) { return 42; }
```

By injecting the `code`

at the top of the `ret42`

function, it either

• transforms it into the `loop`

function (if `code`

does *not *halt), or

• leaves it unmodified (if `code`

*does *halt).

We then use `canHalt`

to distinguish whether the injected `code`

transformed the `ret42`

function into `loop`

, or left it alone. And this tells us whether `code`

halts.

## Final boss: `numHaltsIsEven`

Let’s try an even trickier function property: `numHaltsIsEven`

. This considers how many distinct values you can pass to the function that would cause it to halt. It then returns `true`

if that number is even.

As before, let’s write a function that will satisfy the property:

```
function haltIf4Or8(n: number) {
if (n === 4 || n === 8) return;
while (true) { }
}
```

How many distinct values of `n`

will cause `haltIf4Or8`

to halt?

There are exactly two values, `4`

and `8`

, that cause this function to halt. And two is an even number, so this function should satisfy `numHaltsIsEven`

.

Now let’s use our standard trick, and try to solve the halting problem by injecting the `code`

at the start of `haltIf4Or8`

:

```
function halts(code: string) {
const t = `function haltIf4Or8(n) {
${code}
if (n === 4 || n === 8) return;
while (true) { }
}`;
return numHaltsIsEven(t);
}
```

Use the same “proof-by-cases” technique, first assuming `code`

halts, then assuming it doesn’t. Does the above solve the halting problem?

Actually, it doesn’t! Let’s check both cases. If `code`

halts, then `halts`

returns `true`

, which is all good and correct.

But if `code`

does not halt, what happens? Then the function analyzed by `numHaltsIsEven`

is equivalent to the `loop`

function. So, does the `loop`

function have an even number of inputs that cause it to halt?

Yes: it has zero inputs that cause it to halt, and zero is an even number! So in this case, `halts`

also returns `true`

, which is incorrect!

Indeed! This version of `halts`

always returns `true`

! The cause is that the `loop`

function has zero distinct inputs that cause it to halt, and zero is an even number.

But this is fixable. We just need to construct a function that does *not* satisfy `numHaltsIsEven`

. Which of these will do the job?

```
function haltIf3Or7(n: number) {
if (n === 3 || n === 7) return;
while (true) { }
}
function haltIf3(n: number) {
if (n === 3) return;
while (true) { }
}
```

No, `haltIf3Or7`

also has an even number of inputs that cause it to halt. So it also satisfies `numHaltsIsEven`

. But we’re looking for a function that does *not* satisfy `numHaltsIsEven`

.

The function `haltIf3`

has one input that causes it to halt, namely the input `3`

. One is not considered even, so this function does not satisfy `numHaltsIsEven`

.

Right! `haltIf3`

has one input that causes it to halt, namely the input `3`

. One is not considered even, so this function does not satisfy `numHaltsIsEven`

.

Second time lucky: let’s try again to implement `halts`

, by injecting the `code`

into `haltIf3`

, then inverting the final result with `!`

:

```
function halts(code: string) {
const t = `function haltIf3(n) {
${code}
if (n === 3) return;
while (true) { }
}`;
return !numHaltsIsEven(t);
}
```

If you check it, you should find that this correctly solves the halting problem — thus proving that `numHaltsIsEven`

cannot exist!

## Now for an any property $P$

Finally, you’re prepared to see Rice’s trick in its full generality. We’re given any function property $P$, like “can be a regex” or “number of halting inputs is even”. We want to show that a function `isP`

cannot be written.

**Rice’s trick**

Assume, by contradiction, that `isP`

exists.

We will find some function `t`

, and then inject `code`

at the top of it. If the `loop`

function does *not* satisfy $P$, we set `t`

to a function that *does* satisfy $P$; otherwise, we set `t`

to a function that does *not* satisfy $P$.

We then test whether some arbitrary `code`

halts, by asking `isP`

: “would injecting `code`

at the top of `t`

convert it into the `loop`

function?” But this answers the halting problem, so `isP`

cannot exist!

Well ... almost. Henry Rice says there are two properties of $P$ that make this trick work: first, $P$ must be a **semantic **property, and second, it must be a **non-trivial** property. Let’s see what they mean.

## Too many variables

Perhaps you’ve seen IDE warnings like: “Function `f`

has more than 20 variables. Consider splitting into smaller functions.” But that sounds like a property of functions! Didn’t we just see those are impossible to decide?

Can we really write a function `hasMoreThan20Vars`

that takes a function string and tells us whether it has more than 20 variables?

Sure we can! It reads through the source code, and counts every `const x`

, `var y`

, et cetera. No problem here! So, what’s different about this property? To see, let’s assume we have `hasMoreThan20Vars`

, and try out Rice’s trick:

```
function halts(code: string) {
const t = `function lotsOfVars(n) {
${code}
const a,b,c,d,e,f,g,h,i,j,k,l,m,n,
o,p,q,r,s,t,u,v,w,x,y,z;
return;
}`;
return hasMoreThan20Vars(t);
}
```

Use the usual proof-by-cases: does this solve the halting problem?

The function `lotsOfVars`

starts with 26 variables, so it satisfies `hasMoreThan20Vars`

. Injecting some `code`

at the top doesn’t make any difference to that. It doesn’t tell us anything about whether `code`

halts.

When Mr. Rice says $P$ must be **semantic**, he means it must be solely concerned with the input and output of the function when called. That is: if two functions have the same input-output, then $P$ cannot be true of one, and false of the other.

Let’s see a couple of example properties. Consider a property `returnsInput`

, which tells us whether a function returns its own argument. For examples

```
// satisfies `returnsInput`
function id(x) { return x; }
// does not satisfy `returnsInput`
function increment(x) { return x+1; }
```

Is the property `returnsInput`

semantic?

I think it’s semantic. The property can be decided by only looking at the input-output table, e.g. `1 -> 1`

, `"foo" -> "foo"`

, etc.

*(Bonus exercise: consider the property *`returnsOwnSourceCode`

*, which tells us whether a function will **return its own source code**. Is *`returnsOwnSourceCode`

* a semantic property? Will Rice’s trick work on it? Answers on a postcard!)*

## Solving the halting problem is trivial?!

The final property we’ll consider today is called `solvesHaltingProblem`

. Given a function’s source code, it tells us whether that function solves the halting problem — that is, whether it’s a correct implementation of `halts`

.

As always, let’s try to run Rice’s proof. First: does the `loop`

function satisfy `solvesHaltingProblem`

?

It does not! The `loop`

function never terminates, let alone with a correct answer.

So, next, we must set `t`

to a function that *does* satisfy `solvesHaltingProblem`

. Can you find one?

Really?! If you can find such a `t`

, please email it to me, because you’ve solved the halting problem!

The problem is, there is no such function — Turing taught us this. And so we can’t proceed with Rice’s proof.

If there are no functions that satisfy the property $P$, then we can’t use `isP`

to decide anything, because it always returns `false`

. Similarly, if *every* function satisfies $P$, then we can’t use `isP`

to decide anything, because it always returns `true`

.

This is what Rice means by **triviality.** The property $P$ is trivial if all functions satisfy it, or if none do. To show that `isP`

cannot be written, Rice’s proof requires that $P$ is non-trivial: that it is satisfied by some, but not all, functions.

## Conclusion

And this concludes the proof! Quoting Wikipedia: “Rice’s theorem states that all non-trivial semantic properties of programs are undecidable.” By now, you should understand what that theorem means, how to prove it, and why those “non-trivial semantic” qualifications are in there.

In the next chapter, we’ll be exploring Kurt Gödel’s second incompleteness theorem, which shows that proof systems can’t prove their own consistency! Stay tuned!

**This chapter is free this week — to read the rest of ****Busy Beavers**** and support me writing it, please buy the course! Or if you want to know when the next chapter comes out, ****sign up for updates here.**** You might also enjoy our course ****Everyday Data Science****, which uses similar interactive storytelling. Or if you’re feeling inspired, you can use ****TigYog**** to write your own course just like these ones!**

## Next in Busy Beavers!:

# 8. Just how busy can a busy beaver be?

Let’s play a game! We’ll write a JavaScript program of less than 10 characters that prints as much as possible before halting. Whoever’s program prints more is the busiest beaver, and they win the game.

What’s the busiest program? Just how busy is it? How can we find it? In this chapter, we’ll have a crack at these questions, but fair warning: we might not get many answers.