Term Rewriting and Rewriting Logic
Our interest in term rewriting originates in the fact that we believe term rewriting is a powerful programming paradigm in general, especially useful in giving semantics to languages. That is because a runing step in the execution of a program can be seen as the evolution of a state. If one thinks of the state as being a term, rewrite rules provide means of specifying how the state should evolve.
Two are our main goals regarding term rewriting:
- Researching algorithms and methods which would take advantage of the parallel nature of rewriting. We have developed a method to transform conditional rewrite systems into unconditional ones, since the former are harder to handle in a parallel execution environment. For more information, see Computationally Equivalent Elimination of Conditions
- Research ways for efficiently generating interpretors and compilers from (rewriting-based) language definitions. We hope that due to the specifity of the domain, optimizations that cannot be applied when interpreting/compiling general rewrite systems, could be used to get very fast interpretors for languages from their formal specification. Preliminary results in this direction can be found in A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
A rewrite logic theory consists of a set of uninterpreted operations constrained equationally, together with a set of rewrite rules meant to define the concurrent evolution of the defined system. The distinction between equations and rewrite rules is only semantic. They are both executed as rewrite rules by rewrite engines, following the simple, uniform and parallelizable match-and-apply principle of term rewriting: find a subterm matching , say with a substitution , then replace it by . Therefore, if one is interested in just a dynamic semantics of a language, then, with few exceptions, one needs to make no distinction between equations and rewrite rules.
In our context of programming languages, a language definition is a rewrite logic theory in which equations define the non-concurrent features of the language, while rewrite rules define the concurrent features. A program together with its initial state are given as an uninterpreted term, whose denotation in the initial model is its corresponding transition system. Depending on the desired type of analysis, one can, using existing tool support, generate anywhere from one path in that transition system (e.g., when “executing” the program) to all paths (e.g., for model checking).
In spite of its simplicity and generality, rewriting logic does not give us any immediate recipe for how to define languages as rewrite logic theories. Appropriate definitional techniques and methodologies are necessary in order to make rewriting logic an effective computational framework for programming language definition and formal analysis.
Starting from the broader subject of Rewriting Logic Semantics we are currently developing K, a definitional technique and methodology on top of Rewriting Logic, specifically aiming at Programming languages definitions, which are both operational and denotational.