Rewriting Techniques and Applications

For the most part, rewriting techniques have been developed and applied to support efficient equational reasoning and equational specification, verification, and programming. Therefore, a rewrite rule t −→ t′ has been usually interpreted as a directed equation t = t′. Rewriting logic is a substantial broadening of the semantics given to rewrite rules. The equational reading is abandoned, in favor of a more dynamic interpretation. There are now in fact two complementary readings of a rule t −→ t′, one computational, and another logical: (i) computationally, the rewrite rule t −→ t′ is interpreted as a local transition in a concurrent system; (ii) logically, the rewrite rule t −→ t′ is interpreted as an inference rule. The experience gained so far strongly suggest that rewriting is indeed a very flexible and general formalism for both computational and logical applications. This means that from the computational point of view rewriting logic is a very expressive semantic framework, in which many different models of concurrency, languages, and distributed systems can be specified and programmed; and that from a logical point of view is a general logical framework in which many different logics can be represented and implemented. This paper introduces the main concepts of rewriting logic and of the Maude rewriting logic language, and discusses a wide range of semantic framework and logical framework applications that have been developed in rewriting logic using Maude.