A Rewriting semantics for Maude strategies

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

Research output: Contribution to journalConference articlepeer-review


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


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A Rewriting semantics for Maude strategies'. Together they form a unique fingerprint.

Cite this