Open Systems Laboratory at Illinois

Natural narrowing for general term rewriting systems

By Santiago Escobar, José Meseguer, and Prasanna Thati. In RTA, volume 3467 of Lecture Notes in Computer Science, 279–293. Springer, 2005.

Full Text:
Download PDF
Publisher Link:


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.


    author = "Escobar, Santiago and Meseguer, José and Thati,
    editor = "Giesl, Jürgen",
    title = "Natural Narrowing for General Term Rewriting Systems",
    booktitle = "RTA",
    crossref = "conf/rta/2005",
    ee = "",
    keywords = "formal methods, programming languages",
    pages = "279-293",
    year = "2005",

    editor = "Giesl, Jürgen",
    title = "Term Rewriting and Applications, 16th International
             Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings",
    isbn = "3-540-25596-6",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "3467",
    year = "2005",