Author(s):
Pinto, Jorge Sousa 
; Almeida, José Bacelar ; Vilaça, Miguel
Date: 2006
Persistent ID: http://hdl.handle.net/1822/6228
Origin: RepositóriUM - Universidade do Minho
Document details
A local graph-rewriting system for deciding equality in sum-product theories : ...
Description
In this paper we give a graph-based decision procedure for a calculus with sum and product types. Al- though 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 cancel lation laws.
In this paper we give a graph-based decision procedure for a calculus with sum and product types. Al- though 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 cancel lation laws.
Document Type
Conference Object
Language English
Language English
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||