Natural narrowing for general term rewriting systems

Santiago Escobar, José Meseguer, Prasanna Thati

Research output: Contribution to journalConference articlepeer-review


For narrowing to be an efficient evaluation mechanism, several lazy narrowing strategies have been proposed, although typically for the restricted case of left-linear constructor systems. These assumptions, while reasonable for functional programming applications, are too restrictive for a much broader range of applications to which narrowing can be fruitfully applied, including applications where rules have a non-equational meaning either as transitions in a concurrent system or as inferences in a logical system. In this paper, we propose an efficient lazy narrowing strategy called natural narrowing which can be applied to general term rewriting systems with no restrictions whatsoever. An important consequence of this generalization is the wide range of applications that can now be efficiently supported by narrowing, such as symbolic model checking and theorem proving.

Original languageEnglish (US)
Pages (from-to)279-293
Number of pages15
JournalLecture Notes in Computer Science
StatePublished - 2005
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: Apr 19 2005Apr 21 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this