Relaxed Models for Rewriting Logic

We modify the definition of the models for rewrite theories by replacing the equality of functors, defined by E-equal terms, with the equality via a natural isomorphism, called natural symmetry. The relaxation process can be adapted by relaxing all or only a part of the equations, and by relaxing the state structure (and implicitly the computation structure) or just the computation structure. We also consider the subclasses of C-coherent models, where C is a set of equations specifying a collection of commutative symmetry diagrams. The result is a wide palette of model classes which offers more flexibility in modeling concurrent systems.

Sidebar