Natural rewriting for general term rewriting systems

Santiago Escobar, José Meseguer, Prasanna Thati

Research output: Contribution to journalConference articlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)101-116
Number of pages16
JournalLecture Notes in Computer Science
StatePublished - 2005
Event14th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2004 - Verona, Italy
Duration: Aug 26 2004Aug 28 2004

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Natural rewriting for general term rewriting systems'. Together they form a unique fingerprint.

Cite this