A signature in rewriting logic is an equational theory42 (Sigma,E), where Sigma is an equational signature and E is a set of Sigma-equations. Rewriting will operate on equivalence classes of terms modulo E. In this way, we free rewriting from the syntactic constraints of a term representation and gain a much greater flexibility in deciding what counts as a data structure; for example, string rewriting is obtained by imposing an associativity axiom, and multiset rewriting by imposing associativity and commutativity. Of course, standard term rewriting is obtained as the particular case in which the set of equations E is empty. Techniques for rewriting modulo equations have been studied extensively [17] and can be used to implement rewriting modulo many equational theories of interest. This is precisely what Maude does, using the equational attributes given in operator declarations--such as associativity, commutativity, identity, and idempotency--to rewrite modulo such axioms.
Given a signature (Sigma,E), sentences of rewriting logic are sequents of the form
[t]E --> [t']E,where t and t' are Sigma-terms possibly involving some variables, and [t]E denotes the equivalence class of the term t modulo the equations E. A rewrite theory R is a 4-tuple R= (Sigma,E,L,R) where Sigma is a ranked alphabet of function symbols, E is a set of Sigma-equations, L is a set of labels, and R is a set of pairs R c L ×TSigma,E(X)2 whose first component is a label and whose second component is a pair of E-equivalence classes of terms, with X={x1,...,xn,...} a countably infinite set of variables. Elements of R are called rewrite rules.43 We understand a rule (r,([t],[t'])) as a labeled sequent and use for it the notation r: [t] --> [t']. To indicate that {x1,...,xn} is the set of variables occurring in either t or t', we write r: [t(x1,...,xn)] --> [t'(x1,...,xn)], or in abbreviated notation r: [t( |¯x¯| )] --> [t'( |¯x¯| )].
Given a rewrite theory R, we say that R entails a sentence [t] --> [t'], or that [t] --> [t'] is a (concurrent) R-rewrite, and write R |- [t] --> [t'] if and only if [t] --> [t'] can be obtained by finite application of the following rules of deduction (where we assume that all the terms are well formed and t( |¯w¯| / |¯x¯| ) denotes the simultaneous substitution of wi for xi in t):
|
|
| [t] --> [t] |
.
[t1] --> [t'1] ... [tn] --> [t'n] [f(t1,...,tn)] --> [f(t'1,...,t'n)]
.
[w1] --> [w'1] ... [wn] --> [w'n] [t( |¯w¯| / |¯x¯| )] --> [t'( |¯w'¯| / |¯x¯| )]
.
[t1] --> [t2] [t2] --> [t3] [t1] --> [t3]
Rewriting logic is a logic for reasoning correctly about concurrent systems having states, and evolving by means of transitions. The signature of a rewrite theory describes a particular structure for the states of a system--e.g., multiset, binary tree, etc.--so that its states can be distributed according to such a structure. The rewrite rules in the theory describe which elementary local transitions are possible in the distributed state by concurrent local transformations. The rules of rewriting logic allow us to reason correctly about which general concurrent transitions are possible in a system satisfying such a description. Thus, computationally, each rewriting step is a parallel local transition in a concurrent system.
Alternatively, however, we can adopt a logical viewpoint instead, and regard the rules of rewriting logic as metarules for correct deduction in a logical system. Logically, each rewriting step is a logical entailment in a formal system.
The computational and the logical viewpoints under which rewriting logic can be interpreted can be summarized in the following diagram of correspondences:
State <-> Term <-> Proposition Transition <-> Rewriting <-> Deduction Distributed Structure <-> Algebraic Structure <-> Propositional Structure
The last row of equivalences is actually quite important. Roughly speaking, it expresses the fact that a state can be transformed in a concurrent way only if it is nonatomic, that is, if it is composed out of smaller state components that can be changed independently. In rewriting logic this composition of a concurrent state is formalized by the operations of the signature Sigma of the rewrite theory R that axiomatizes the system. From the logical point of view such operations can naturally be regarded as user-definable propositional connectives stating the particular structure that a given state has. A subtle additional point about the last row of equivalences is that the algebraic structure of a system also involves equations. Such equations describe the system's global state as a concurrent data structure; they can have a dramatic impact on the amount of concurrency available in a system.
Note that it follows from this discussion that rewriting logic is primarily a logic of change--in which the deduction directly corresponds to the change--as opposed to a logic to talk about change in a more indirect and global manner such as the different variants of modal and temporal logic.