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

• Author(s): Almeida, José Bacelar ; Pinto, Jorge Sousa ; Vilaça, Miguel
• Date: 2007
• Persistent ID: http://hdl.handle.net/1822/14922
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Graph-based decision procedures; Point-free programming
• Document Type: Article
• Language: English

Description

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.