Bounded quantification is undecidable

摘要

F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping.

Curien and Ghelli proved the partial correctness of a recursive procedure for computing minimal types of F≤ terms and showed that the termination of this procedure is equivalent to the termination of this procedure is equivalent to the termination of its major component, a procedure for checking the subtype relation between F≤ types. This procedure was thought to terminate on all inputs, but the discovery of a subtle bug in a purported proof of this claim recently reopened the question of the decidability of subtyping, and hence of typechecking.

This question is settled here in the negative, using a reduction from the halting problem for two-counter Turing machines to show that the subtype relation of F≤ is undecidable.