A core language for rewriting

Eelco Visser, Zine-El-Abidine Benaissa. A core language for rewriting. Electronic Notes in Theoretical Computer Science, 15:422-441, 1998. [doi]


System S is a calculus providing the basic abstractions of term rewriting: matching and building terms, term traversal, combining computations and handling failure. The calculus forms a core language for implementation of a wide variety of rewriting languages, or more generally, languages for specifying tree transformations. In this paper we show how a conventional rewriting language based on conditional term rewriting can be implemented straightforwardly in System S. Subsequently we show how this implementation can be extended with features such as matching conditions, negative conditions, default rules, non-strictness annotations and alternative evaluation strategies.