University of Minnesota
Software Engineering Center

You are here

Abstractions in Decision Procedures for Algebraic Data Types

Date of Publication: 
March 2013
Associated Research Groups: 
Publication Files: 
Reasoning about algebraic data types and functions that operate over these data types is an important problem for a large variety of applications. In this paper, we present an unrolling-based decision procedure for reasoning about data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends previous work in catamorphism-based reasoning in a number of directions. First, we propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to fix an incompleteness in a previous unrolling algorithm (and associated proof). We then use these notions to address two open questions from previous work: (1) we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and (2) demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness.
University of Minnesota
University of Minnesota
@techreport{Pham13:unrolling, author = {Tuan-Hung Pham and Michael W. Whalen}, title = {Abstractions in Decision Procedures for Algebraic Data Types}, institution = {University of Minnesota Twin Cities}, year = {2013}, number = {13-006} }