A Local Graph-rewriting System for Deciding Equality in Sum-product Theories
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça · Electronic Notes in Theoretical Computer Science · 2007
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.