A local graph-rewriting system for deciding equality in sum-product theories

• Autor(es): Almeida, José Bacelar ; Pinto, Jorge Sousa ; Vilaça, Miguel
• Data: 2007
• Identificador Persistente: http://hdl.handle.net/1822/14922
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Graph-based decision procedures; Point-free programming
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

Proceedings of the Third International Workshop on Term Graph Rewriting (TERMGRAPH 2006) 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.