ICFP 2008 - Pattern Minimization Problems over Recursive Data Types

Pattern Minimization Problems over Recursive Data Types

Alexander Krauss

The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)
Victoria, British Columbia, Canada, September 22-24, 2008

Abstract

In the context of program verification in an interactive theorem prover, we study the problem of transforming function definitions with ML-style (possibly overlapping) pattern matching into sets of equations that are non-overlapping and minimal.

Since non-overlapping equations are valid independently, they are better suitable for the equational proof style usually employed in paper proofs.

We relate the problem to the well-known minimization problem for propositional DNF formulas and show that it is $\Sigma_2^P$-complete. We then develop a concrete algorithm to compute minimal patterns, which naturally generalizes the standard Quine-McCluskey procedure to the domain of term patterns.

START Conference Manager (V2.54.6)