# Process and Term Tile Logic

In a similar way as 2-categories can be regarded as a special case of
double categories, rewriting logic (in the unconditional case)
can be embedded into the more general tile logic, where also
side-effects and rewriting synchronization are considered. Since
rewriting logic is the semantic basis of several language
implementation efforts, it is useful to map tile logic back into
rewriting logic in a conservative way, to obtain executable
specifications of tile systems. We extend the results of earlier work
by two of the authors, focusing on some interesting cases where the
mathematical structures representing configurations (\ie,
states) and effects (\ie, observable actions) are very similar,
in the sense that they have in common some auxiliary structure (\eg,
for tupling, projecting, etc.). In particular, we give in full detail
the descriptions of two such cases where (net) process-like and
usual term structures are employed. Corresponding to these two
cases, we introduce two categorical notions, namely, symmetric
strict monoidal double category and cartesian double category
with consistently chosen products, which seem to offer an adequate
semantic setting for process and term tile systems. The new model
theory of 2EVH-categories required to relate the categorical models
of tile logic and rewriting logic is presented making use of a recently
developed framework, called partial membership equational
logic, particularly suitable to deal with categorical structures.
Consequently, symmetric strict monoidal and cartesian classes of
double categories and 2-categories are compared through their
embedding in the corresponding versions of 2EVH-categories. As a
result of this comparison, we obtain a correct rewriting
implementation of tile logic. This implementation uses a meta-layer
to control the rewritings, so that only tile proofs are accepted.
Making use of the reflective capabilities of the Maude
language, some (general) internal strategies are then defined
to implement the mapping from tile systems into rewriting systems,
and some interesting applications related to the implementation of
concurrent process calculi are presented.