Pattern minimization problems over recursive data types

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 minimal sets of independent equations. Since independent equations are valid unconditionally, they are better suited for the equational proof style using induction and rewriting, which is often found in proofs in theorem provers or on paper. We relate the problem to the well-known minimization problem for propositional DNF formulas and show that it is P 2 -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. Categories and Subject Descriptors D.3.3 [Programming Languages] General Terms Theory, Verification Keywords Complexity, Pattern Matching, Theorem Proving

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Alexander Krauss
• Keywords: ICFP 2008, Interactive Theorem Prover, Programming Languages, Propositional Dnf Formulas, Well-known Minimization Problem