Abstractions in Decision Procedures for Algebraic Data Types
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
Abstractions in Decision Procedures for Algebraic Data Types
Authors
Published Date
2013
Publisher
University of Minnesota
Type
Report
Abstract
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.
Keywords
Description
Associated research group: Critical Systems Research Group
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
University of Minnesota
Suggested citation
Pham, Hung T.; Whalen, Michael. (2013). Abstractions in Decision Procedures for Algebraic Data Types. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217376.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.