Internal strategies in a rewriting implementation of tile systems

Citations of this article
Mendeley users who have this article in their library.


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. © 1998 Published by Elsevier Science B. V.




Bruni, R., Meseguer, J., & Montanari, U. (1998). Internal strategies in a rewriting implementation of tile systems. In Electronic Notes in Theoretical Computer Science (Vol. 15, pp. 263–284). Elsevier B.V.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free