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. We verify a recent (abstract) decision procedure for pattern completeness that covers the general case, i.e., in particular without the usual restriction of left-linearity. In two refinement steps, we further develop an executable version of that abstract algorithm. On our example suite, this verified implementation is faster than other implementations that are based on alternative (unverified) approaches, including the complement algorithm, tree automata encodings, and even the pattern completeness check of the GHC Haskell compiler.

BibTeX

@article{Pattern_Completeness-AFP,
  author  = {René Thiemann and Akihisa Yamada},
  title   = {Verifying a Decision Procedure for Pattern Completeness},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Pattern_Completeness.html},
             Formal proof development},
  ISSN    = {2150-914x},
}