Semantic foundations for generalized rewrite theories

Roberto Bruni, José Meseguer

Research output: Contribution to journalArticle

Abstract

Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications.

Original languageEnglish (US)
Pages (from-to)386-414
Number of pages29
JournalTheoretical Computer Science
Volume360
Issue number1-3
DOIs
StatePublished - Aug 21 2006

Keywords

  • Conditional rewriting logic
  • Contextual rewrites
  • Membership equational logic
  • Semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Semantic foundations for generalized rewrite theories'. Together they form a unique fingerprint.

  • Cite this