Deciding pattern completeness in non-deterministic polynomial time
René Thiemann, Akihisa Yamada14th International Workshop on Confluence, pp. 31-37, 2025.
Abstract
Pattern completeness is the property that the left-hand sides of a functional program
or term rewrite system cover all cases w.r.t. pattern matching. This or related properties
are required, if one wants to perform ground confluence proofs by rewriting induction. In
order to certify such confluence proofs, we develop a novel algorithm that decides pattern
completeness. The algorithm has an asymptotic optimal complexity, as it belongs to the
complexity class co-NP. It has been verified in Isabelle/HOL and outperforms existing
algorithms, even including the pattern completeness check of the GHC Haskell compiler.
BibTeX
@inproceedings{RTAY-IWC2025,
author = "René Thiemann and Akihisa Yamada",
title = "Deciding pattern completeness in non-deterministic polynomial time",
booktitle = "Proceedings of the 14th International Workshop on Confluence",
editor = "Raúl Gutiérrez and Naoki Nishida",
pages = "31--37",
year = 2025
}