An improved unrolling-based decision procedure for algebraic data types

Tuan Hung Pham, Michael W. Whalen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

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 a 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 a previous decision procedure that solves formulas involving algebraic data types via successive unrollings of catamorphism functions. 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 the previous unrolling algorithm (and associated proof). We then use these notions to address two open problems 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) we demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness.

Original languageEnglish (US)
Title of host publicationVerified Software
Subtitle of host publicationTheories, Tools, Experiments - 5th International Conference, VSTTE 2013, Revised Selected Papers
EditorsAndrey Rybalchenko, Andrey Rybalchenko, Ernie Cohen
PublisherSpringer- Verlag
Pages129-148
Number of pages20
ISBN (Electronic)9783642541070
StatePublished - 2013
Event5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013 - Menlo Park, United States
Duration: May 17 2013May 19 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8164
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013
CountryUnited States
CityMenlo Park
Period5/17/135/19/13

Fingerprint Dive into the research topics of 'An improved unrolling-based decision procedure for algebraic data types'. Together they form a unique fingerprint.

Cite this