Natural narrowing for general term rewriting systems

Santiago Escobar, José Meseguer, Prasanna Thati

Research output: Contribution to journalConference article

Abstract

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
Volume3467
StatePublished - Sep 26 2005
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: Apr 19 2005Apr 21 2005

Fingerprint

Term Rewriting Systems
Symbolic Model Checking
Functional programming
Theorem proving
Functional Programming
Concurrent Systems
Theorem Proving
Model checking
Range of data
Linear systems
Linear Systems
Restriction
Evaluation
Strategy

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Natural narrowing for general term rewriting systems. / Escobar, Santiago; Meseguer, José; Thati, Prasanna.

In: Lecture Notes in Computer Science, Vol. 3467, 26.09.2005, p. 279-293.

Research output: Contribution to journalConference article

Escobar, Santiago ; Meseguer, José ; Thati, Prasanna. / Natural narrowing for general term rewriting systems. In: Lecture Notes in Computer Science. 2005 ; Vol. 3467. pp. 279-293.
@article{0b80a47e454e46599c10c425eb6edfee,
title = "Natural narrowing for general term rewriting systems",
abstract = "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 = "Santiago Escobar and Jos{\'e} Meseguer and Prasanna Thati",
year = "2005",
month = "9",
day = "26",
language = "English (US)",
volume = "3467",
pages = "279--293",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Natural narrowing for general term rewriting systems

AU - Escobar, Santiago

AU - Meseguer, José

AU - Thati, Prasanna

PY - 2005/9/26

Y1 - 2005/9/26

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=24944538905&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24944538905&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:24944538905

VL - 3467

SP - 279

EP - 293

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -