Natural rewriting for general term rewriting systems
By
We address the problem of an efficient rewriting strategy for general term rewriting systems. Several strategies have been proposed over the last two decades for rewriting, the most efficient of all being the natural rewriting strategy [9]. All the strategies so far, including natural rewriting, assume that the given term rewriting system is a left-linear constructor system. Although these restrictions are reasonable for some functional programming languages, they limit the expressive power of equational languages, and they preclude certain applications of rewriting to equational theorem proving and to languages combining equational and logic programming. In this paper, we propose a conservative generalization of natural rewriting that does not require the rules to be left-linear and constructor-based. We also establish the soundness and completeness of this generalization.
BibTeX
@inproceedings{conf/lopstr/EscobarMT04,
author = "Escobar, Santiago and Meseguer, José and Thati,
Prasanna",
editor = "Etalle, Sandro",
title = "Natural Rewriting for General Term Rewriting Systems",
booktitle = "LOPSTR",
crossref = "conf/lopstr/2004",
ee = "http://dx.doi.org/10.1007/11506676_7",
keywords = "formal methods, software engineering, programming
languages",
pages = "101-116",
year = "2004",
}
@proceedings{conf/lopstr/2004,
editor = "Etalle, Sandro",
title = "Logic Based Program Synthesis and Transformation, 14th
International Symposium, LOPSTR 2004, Verona, Italy, August 26-28,
2004, Revised Selected Papers",
isbn = "3-540-26655-0",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3573",
year = "2005",
}