A Core Language for Rewriting

Abstract

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. We thank Bas Luttik and Andrew Tolmach for many discussions on rewriting strategies and their applications. Jan Bergstra pointed out the problems of non-determinism and conditional rules in languages such as ASF+SDF. Eu-genio Moggi made clear that our semantics does not model programs with global backtracking, but rather local backtracking, which was what we were looking for.