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. https://doi.org/10.1016/S1571-0661(05)80016-7