A Rewriting semantics for Maude strategies

Narciso Martí-Oliet, José Meseguer, Alberto Verdejo

Research output: Contribution to journalConference article

Abstract

Intuitively, a strategy language is a way of taming the nondeterminism of a rewrite theory. We can think of a strategy language S as a rewrite theory transformation R → S(R) such that S(R) provides a way of executing R in a controlled way. One such theory transformation for the Maude strategy language is presented in detail in this paper. Progress in the semantic foundations of Maude's strategy language has led us to study some general requirements for strategy languages. Some of these requirements, like soundness and completeness with respect to the rewrites in R, are absolute requirements that every strategy language should fulfill. Other more optional requirements, that we call monotonicity and persistence, represent the fact that no solution is ever lost. We show that the Maude strategy language satisfies all these four requirements.

Original languageEnglish (US)
Pages (from-to)207-226
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 1 2008
Event7th International Workshop on Rewriting Logic and its Applications, WRLA 2008 (European Joint Conference on Theory and Practice of Software, ETAPS 2008) - Budapest, Hungary
Duration: Mar 29 2008Mar 30 2008

Fingerprint

Maude
Rewriting
Semantics
Requirements
Nondeterminism
Soundness
Strategy
Language
Persistence
Monotonicity
Completeness

Keywords

  • ELAN
  • Maude
  • Rewriting logic
  • Rewriting semantics
  • Strategies

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

A Rewriting semantics for Maude strategies. / Martí-Oliet, Narciso; Meseguer, José; Verdejo, Alberto.

In: Electronic Notes in Theoretical Computer Science, 01.12.2008, p. 207-226.

Research output: Contribution to journalConference article

@article{24e3fc61a4ec40f8a2f7184a29770a0d,
title = "A Rewriting semantics for Maude strategies",
abstract = "Intuitively, a strategy language is a way of taming the nondeterminism of a rewrite theory. We can think of a strategy language S as a rewrite theory transformation R → S(R) such that S(R) provides a way of executing R in a controlled way. One such theory transformation for the Maude strategy language is presented in detail in this paper. Progress in the semantic foundations of Maude's strategy language has led us to study some general requirements for strategy languages. Some of these requirements, like soundness and completeness with respect to the rewrites in R, are absolute requirements that every strategy language should fulfill. Other more optional requirements, that we call monotonicity and persistence, represent the fact that no solution is ever lost. We show that the Maude strategy language satisfies all these four requirements.",
keywords = "ELAN, Maude, Rewriting logic, Rewriting semantics, Strategies",
author = "Narciso Mart{\'i}-Oliet and Jos{\'e} Meseguer and Alberto Verdejo",
year = "2008",
month = "12",
day = "1",
language = "English (US)",
pages = "207--226",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - A Rewriting semantics for Maude strategies

AU - Martí-Oliet, Narciso

AU - Meseguer, José

AU - Verdejo, Alberto

PY - 2008/12/1

Y1 - 2008/12/1

N2 - Intuitively, a strategy language is a way of taming the nondeterminism of a rewrite theory. We can think of a strategy language S as a rewrite theory transformation R → S(R) such that S(R) provides a way of executing R in a controlled way. One such theory transformation for the Maude strategy language is presented in detail in this paper. Progress in the semantic foundations of Maude's strategy language has led us to study some general requirements for strategy languages. Some of these requirements, like soundness and completeness with respect to the rewrites in R, are absolute requirements that every strategy language should fulfill. Other more optional requirements, that we call monotonicity and persistence, represent the fact that no solution is ever lost. We show that the Maude strategy language satisfies all these four requirements.

AB - Intuitively, a strategy language is a way of taming the nondeterminism of a rewrite theory. We can think of a strategy language S as a rewrite theory transformation R → S(R) such that S(R) provides a way of executing R in a controlled way. One such theory transformation for the Maude strategy language is presented in detail in this paper. Progress in the semantic foundations of Maude's strategy language has led us to study some general requirements for strategy languages. Some of these requirements, like soundness and completeness with respect to the rewrites in R, are absolute requirements that every strategy language should fulfill. Other more optional requirements, that we call monotonicity and persistence, represent the fact that no solution is ever lost. We show that the Maude strategy language satisfies all these four requirements.

KW - ELAN

KW - Maude

KW - Rewriting logic

KW - Rewriting semantics

KW - Strategies

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

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

M3 - Conference article

AN - SCOPUS:84890865864

SP - 207

EP - 226

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -