Title
A Local Graph-rewriting System for Deciding Equality in Sum-product Theories
Abstract
In this paper we give a graph-based decision procedure for a calculus with sum and product types. Although our motivation comes from the Bird-Meertens approach to reasoning algebraically about functional programs, the language used here can be seen as the internal language of a category with binary products and coproducts. As such, the decision procedure presented has independent interest. A standard approach based on term rewriting would work modulo a set of equations; the present work proposes a simpler approach, based on graph-rewriting. We show in turn how the system covers reflection equational laws, fusion laws, and cancellation laws.
Year
DOI
Venue
2007
10.1016/j.entcs.2006.10.031
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
graph-based decision procedure,decision procedure,standard approach,present work,simpler approach,binary product,point-free programming,functional program,internal language,bird-meertens approach,local graph-rewriting system,sum-product theories,cancellation law,graph rewriting,reflection equation,functional programming
Discrete mathematics,Graph,Coproduct,Modulo,Computer science,Product type,Graph rewriting,Rewriting,Abstract semantic graph,Binary number
Journal
Volume
Issue
ISSN
176
1
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
1
0.36
6
Authors
3
Name
Order
Citations
PageRank
José Bacelar Almeida11028.34
Jorge Sousa Pinto216023.19
Miguel Vilaça3162.25