Difference between revisions of "Term Rewriting and Rewriting Logic"
(→ Rewriting Logic) |
|||
| Line 19: | Line 19: | ||
no distinction between equations and rewrite rules. | no distinction between equations and rewrite rules. | ||
| − | An extensive bibliography and overview of Rewriting Logic is geiven by the [http://maude.cs.uiuc.edu/bibliography/ Rewriting Logic: Roadmap and Bibliography]. Developed at both [http://www.sri.com SRI] and [http://www.cs.uiuc.edu UIUC], [http://maude.cs.uiuc.edu Maude] fully implements | + | An extensive bibliography and overview of Rewriting Logic is geiven by the [http://maude.cs.uiuc.edu/bibliography/ Rewriting Logic: Roadmap and Bibliography]. Developed at both [http://www.sri.com SRI] and [http://www.cs.uiuc.edu UIUC], [http://maude.cs.uiuc.edu Maude] fully implements Rewriting Logic. |
In our context of programming languages, a language definition is a rewrite logic theory in | In our context of programming languages, a language definition is a rewrite logic theory in | ||
Revision as of 18:16, 13 July 2006
Term Rewriting
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
Rewriting Logic
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.
An extensive bibliography and overview of Rewriting Logic is geiven by the Rewriting Logic: Roadmap and Bibliography. Developed at both SRI and UIUC, Maude fully implements Rewriting Logic.
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.
