We first sketch the construction of initial and free models for a rewrite theory R = (Sigma,E,L,R). Such models capture nicely the intuitive idea of a "rewrite system" in the sense that they are systems whose states are E-equivalence classes of terms, and whose transitions are concurrent rewritings using the rules in R. By adopting a logical instead of a computational perspective, we can alternatively view such models as "logical systems" in which formulas are validly rewritten to other formulas by concurrent rewritings which correspond to proofs for the logic in question. Such models have a natural category structure, with states (or formulas) as objects, transitions (or proofs) as morphisms, and sequential composition as morphism composition, and in them dynamic behavior exactly corresponds to deduction.
Given a rewrite theory R=(Sigma,E,L,R), for which we assume that different labels in L name different rules in R, the model that we are seeking is a category TR(X) whose objects are equivalence classes of terms [t] e TSigma,E(X) and whose morphisms are equivalence classes of "proof terms" representing proofs in rewriting deduction, i.e., concurrent R-rewrites. The rules for generating such proof terms, with the specification of their respective domains and codomains, are given below; they just "decorate" with proof terms the rules 1-4 of rewriting logic. Note that we always use "diagrammatic" notation for morphism composition, i.e., alpha; beta always means the composition of alpha followed by beta.
|
|
| [t]: [t] --> [t] |
.
alpha1:[t1] --> [t'1] ... alphan: [tn] --> [t'n] f(alpha1,...,alphan): [f(t1,...,tn)] --> [f(t'1,...,t'n)]
.
alpha1:[w1] --> [w'1] ... alphan:[wn] --> [w'n] r(alpha1,...,alphan):[t( |¯w¯| / |¯x¯| )] --> [t'( |¯w'¯| / |¯x¯| )]
| alpha: [t1] --> [t2] beta: [t2] --> [t3] |
|
|
| alpha;beta: [t1] --> [t3] |
Each of the above rules of generation defines a different operation taking certain proof terms as arguments and returning a resulting proof term. In other words, proof terms form an algebraic structure PR(X) consisting of a graph with nodes TSigma,E(X), with identity arrows, and with operations f (for each f e Sigma), r (for each rewrite rule), and _ ;_ (for composing arrows). Our desired model TR(X) is the quotient of PR(X) modulo the following equations:44
f(alpha1;beta1,...,alphan;betan) = f(alpha1,...,alphan);f(beta1,...,betan).
.
alpha1:[w1] --> [w'1] ... alphan:[wn] --> [w'n] r( |¯alpha¯| )=r( |¯[w]¯| );t'( |¯alpha¯| )= t( |¯alpha¯| );r( |¯[w']¯| )
Note that the set X of variables is actually a parameter of these constructions, and we need not assume X to be fixed and countable. In particular, for X=Ø, we adopt the notation TR. The equations in 1 make TR(X) a category, the equations in 2 make each f e Sigma a functor, and 3 forces the axioms E. The exchange law states that any rewriting of the form r( |¯alpha¯| )--which represents the simultaneous rewriting of the term at the top using rule r and "below," i.e., in the subterms matched by the variables, using the rewrites |¯alpha¯| --is equivalent to the sequential composition r( |¯[w]¯| );t'( |¯alpha¯| ), corresponding to first rewriting on top with r and then below on the subterms matched by the variables with |¯alpha¯| , and is also equivalent to the sequential composition t( |¯alpha¯| );r( |¯[w']¯| ) corresponding to first rewriting below with |¯alpha¯| and then on top with r. Therefore, the exchange law states that rewriting at the top by means of rule r and rewriting "below" using |¯alpha¯| are processes that are independent of each other and can be done either simultaneously or in any order.
Since each proof term is a description of a concurrent computation, what these equations provide is an equational theory of true concurrency allowing us to characterize when two such descriptions specify the same abstract computation.
Note that, since [t(x1,...,xn)] and [t'(x1,...,xn)] can both be regarded as functors TR(X)n --> TR(X), from the mathematical point of view the exchange law just asserts that r is a natural transformation.
Lemma. [37] For each rewrite rule r: [t(x1,...,xn)] --> [t'(x1,...,xn)] in R, the family of morphisms{r( |¯[w]¯| ):[t( |¯w¯| / |¯x¯| )] --> [t'( |¯w¯| / |¯x¯| )] | |¯[w]¯| e TSigma,E(X)n }is a natural transformation r:[t(x1,...,xn)] => [t'(x1, ...,xn)] between the functors [t(x1,...,xn)], [t'(x1,...,xn)]: TR(X)n --> TR(X).
The category TR(X) is just one among many models that can be assigned to the rewrite theory R. The general notion of model, called an R-system, is defined as follows:
Definition. Given a rewrite theory R= (Sigma,E,L,R), an R-system S is a category S together with:
- a (Sigma,E)-algebra structure given by a family of functors
{ fS: Sn --> S | f e Sigman, n e N}satisfying the equations E, i.e., for any t(x1,...,xn) = t'(x1,...,xn) in E we have an identity of functors tS = t'S, where the functor tS is defined inductively from the functors fS in the obvious way.- for each rewrite rule r: [t( |¯x¯| )] --> [t'( |¯x¯| )] in R a natural transformation rS:tS => t'S.
An R-homomorphism F:S --> S' between two R-systems is then a functor F:S --> S' such that it is a Sigma-algebra homomorphism, i.e., fS*F = Fn*fS', for each f in Sigman, n e N, and such that "F preserves R," i.e., for each rewrite rule r: [t( |¯x¯| )] --> [t'( |¯x¯| )] in R we have the identity of natural transformations45 rS*F = Fn *rS', where n is the number of variables appearing in the rule. This defines a category R-Sys in the obvious way.
A detailed proof of the following theorem on the existence of initial and free R-systems for the more general case of conditional rewrite theories is given in [37], where the soundness and completeness of rewriting logic for R-system models is also proved.
Theorem. TR is an initial object in the category R-Sys. More generally, TR(X) has the following universal property: Given an R-system S, each function F:X --> |S| extends uniquely to an R-homomorphism F|=|:TR(X) --> S.