The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable

Abstract

We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{ö}del's system T) by reducing Hilbert's tenth problem to it. More generally pattern matching is undecidable in all the calculi in which primitive recursive functions can be fairly represented in a precised sense.