The Undecidability of λ-Definability

Abstract

In this article, we shall show that the Plotkin-Statman conjecture (Plotkin 1973, Statman 1982) is false. The conjecture was that, in a model of the simply typed λ-calculus with only finitely many elements at each type, definability (by a closed term of the calculus) is decidable. This conjecture had been shown to imply many things, for example, Statman (1982, see also Wolfram 1993) has shown it implies the decidability of pure higher order pattern matching (a problem that remains open at the time of writing) and is equivalent to higher order pattern matching with δ-functions. The proof of undecidability given here uses encodings of semi-Thue systems as definability problems. It had been thought that λ-definability might be characterized by invariance under logical relations, which would imply the Plotkin-Statman conjecture. We give a relatively simple counterexample to this, using our encoding of word problems.