The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable
Logic in Computer Science
2023-06-12 v1
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{\"o}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.
Keywords
Cite
@article{arxiv.2306.05876,
title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2306.05876},
year = {2023}
}