START Conference Manager    

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


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)