%0 Journal Article
%J Electronic Notes in Theoretical Computer Science
%D 2007
%T A Local Graph-rewriting System for Deciding Equality in Sum-product Theories
%A José Bacelar Almeida
%A Jorge Sousa Pinto
%A Miguel Vilaça
%N 1
%P 139-163
%V 176
%X <p>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.<br /> 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.</p>
%> https://haslab.uminho.pt/sites/default/files/jba/files/06sum-product.pdf