Autor(es):
Pinto, Jorge Sousa 
; Almeida, José Bacelar ; Vilaça, Miguel
Data: 2006
Identificador Persistente: http://hdl.handle.net/1822/6228
Origem: RepositóriUM - Universidade do Minho
Detalhes do Documento
A local graph-rewriting system for deciding equality in sum-product theories : ...
Descrição
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.
Tipo de Documento
Documento de conferência
Idioma Inglês
Idioma Inglês
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||