Verifying a Decision Procedure for Pattern Completeness

René Thiemann 🌐 and Akihisa Yamada 📧

May 27, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Pattern_Completeness