A Local Graph-rewriting System for Deciding Equality in Sum-product Theories (Extended Abstract)
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça · 2006
The point-free style of programming [1] has been defended as a good choicefor reasoning about functional programs. However, when one actually tries toconstruct a decision procedure for the associated equational theory, one facesproblems, even when small fragments of the theory are considered.In this paper we outline how a graph-based decision procedure can be givenfor the functional calculus with sums and products (but no exponentials – theexpressions we use here can not really be seen as a programming language).We show in turn how the system covers reflexivity equational laws, fusionlaws, and cancelation laws.The decision procedure has interest independently of our initial motivation.The term language (and its theory) can be seen as the internal language of acategory with binary products and coproducts. A standard approach basedon term rewriting would work modulo a set of equations; the present workproposes a simpler approach, based on graph-rewriting.