A Local Graph-rewriting System for Deciding Equality in Sum-product Theories

Citation:
Almeida JB, Pinto JS, Vilaça M.  2007.  A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. Electronic Notes in Theoretical Computer Science. 176(1):139-163.

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.

Citation Key:

DBLP:journals/entcs/AlmeidaPV07

DOI:

10.1016/j.entcs.2006.10.031

PreviewAttachmentSize
06sum-product.pdf1.15 MB