# Why is behavorial subtyping undecidable?

Liskov's work in this area focused on behavioral subtyping, which besides the type system safety discussed in this article also requires that subtypes preserve all invariants guaranteed by the supertypes in some contract.[3] This definition of subtyping is generally undecidable, so it cannot be verified by a type checker.

Let the contract of operation `o` of Type `T` be that it halts for all inputs. Now decide whether operation `o` of subtype `S <: T` satisfies that contract: you have just solved the Halting Problem.

More generally, `S::o` must compute the same function as `T::o` if `S <: T`. Deciding whether two programs compute the same function is called the Function Problem and is equivalent to solving the Halting Problem.

In general, statically deciding any non-trivial runtime property is almost always equivalent to the Halting Problem.

• That last line nails it. The moment you'd like to prove a property about what the program might do in a behavioral setting you're stepping into the impossible. The reason type systems and static analysis tools work is that they treat a different language (of the types of the program, of the scope of variables in the program and so on) and not the properties of how the program runs directly. Commented Dec 5, 2015 at 15:13
• @BenjaminGruenbaum Jorg's answer and your comment are correct but there's a subtlety to it I'd like to clarify. It's often possible to prove a property about a specific program. There just isn't an algorithm you can blindly follow that will work for all programs. Consider this method written in Java: `BigInteger sum(int[] arr) { BigInteger sum = BigInteger.ZERO; for (int x: arr) sum = sum.add(BigInteger.valueOf(x)); return sum; }` It's not hard to prove that particular method always returns the sum of an integer array's elements and does nothing else (provided the argument is not null). Commented Dec 5, 2015 at 17:50
• And when it's not equivalent to the halting problem, it's often even worse. Because impossible wasn't hard enough already. Commented Dec 5, 2015 at 18:45
• Or to put Doval's point another (blunt) way, this is precisely why non-Turing complete languages are interesting and useful. You often don't need Turing-completeness (certainly on a module level) for real work. Commented Dec 6, 2015 at 1:39
• @Doval: Very good point. While it is true that you cannot have an algorithm that proves termination and / or correctness of a random program, it is possible to write programs in such a way that you can prove their correctness. Commented Dec 6, 2015 at 10:59

Because almost every question about the behavior of programs is undecidable. By Rice's theorem, any decision problem of the form:

Some programs compute functions that have this property, other programs compute functions that don't have this property. Given a program P, does the function computed by P have the aforementioned property or not?

is undecidable. So, for example, you can't always distinguish code that computes the square of an input from code that doesn't. Although in simple cases, it is often possible to prove that a function does or does not do so, there is no general procedure that works for all program.

Almost any interesting behavioral invariant falls under Rice's theorem, since those statements rarely (if ever) talk about what the method looks like internally, only what it returns and what side effects it causes in response to certain inputs.

• You could clarify a bit: It's not that a single given program, no matter how pathological, could resist all analyses, but that, for any given analysis, there exists at least one program that cannot be properly categorized with that. Commented Dec 5, 2015 at 23:25