Internal strategies in a rewriting implementation of tile systems

R. Bruni, Jose Meseguer, U. Montanari

Research output: Contribution to journalArticle


Tile logic extends rewriting logic, taking into account rewriting with side-effects and rewriting synchronization. Since rewriting logic is the semantic basis of several language implementation efforts, it is interesting to map tile logic back into rewriting logic in a conservative way, to obtain executable specifications of tile systems. The resulting implementation requires a meta-layer to control the rewritings, so that only tile proofs are accepted. However, by exploiting the reflective capabilities of the Maude language, such meta-layer can be specified as a kernel of internal strategies. It turns out that the required strategies are very general and can be reformulated in terms of search algorithms for non-confluent systems equipped with a notion of success. We formalize such strategies, giving their detailed description in Maude, and showing their application to modeling uniform tile systems.

Original languageEnglish (US)
Pages (from-to)263-284
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Jan 1 1998
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Internal strategies in a rewriting implementation of tile systems'. Together they form a unique fingerprint.

  • Cite this