Browsing by Author "Pham, Tuan-Hung"
Now showing 1 - 2 of 2
Results Per Page
Sort Options
Item Abstractions in Decision Procedures for Algebraic Data Types(2013-03-06) Pham, Tuan-HungReasoning 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.Item On Parameterized Abstractions in Unrolling-Based Decision Procedure for Algebraic Data Types(2013-06-03) Pham, Tuan-HungReasoning about algebraic data types is an important problem for a variety of proof tasks. Recently, a variety of decision procedures have been proposed for algebraic data types involving creating suitable abstractions of values in the types. A class of abstractions created from catamorphism functions has been shown to be theoretically applicable to a wide variety of reasoning tasks as well as efficient in practice. However, in previous work, the decidability of catamorphism functions involving parameters in addition to the data type argument has not been demonstrated. In this paper, we generalize certain kinds of catamorphism functions to support additional parameters. This extension, called parameterized associative-commutative catamorphisms subsumes the associative-commutative class from earlier work, widens the set of functions that are known to be decidable, and makes several practically important functions (such as forall and exists) over elements of algebraic data types straightforward to express.