We discussed various concepts of equivalence between CRNs and their relation to concepts from category theory.
Researchers are attempting to use DNA strand displacement cascades to implement a wide variety of chemical reaction networks with interesting algorithmic behaviors. This raises the general question of when we can say such an implementation is correct.
In this context there is a 'formal' CRN, the one being implemented, together with an 'implementation' CRN. The implementation CRN often contains many more chemical species in addition to species corresponding to those in the formal CRN. We call these additional species 'intermediate' species and call those corresponding to species in the formal CRN 'formal' species. Although every reaction that we are trying to implement is a one-step reaction involving only formal species, in the implementation CRN they are often implemented via a multi-step pathway which goes through states containing intermediate species.
There are a number of concepts of 'equivalence' between the formal and implementation CRN, which seek to make precise the notion that the implementation is correct. The first notion is widespread, the second was known in the state-transition system literature but introduced into CRN theory by Qing Dong in 2012, and the third was introduced by Seung Woo Shin in 2011:
- Reachability equivalence. A necessary condition for an implementation to be correct is to require that given any two states containing only formal species, the second is reachable from the first in the formal CRN if and only if it is reachable in the implementation CRN.
- Bisimulation equivalence. A stronger notion is bisimulation equivalence. This is based on the idea of interpreting any intermediate species as a combination of formal species. Bisimulation equivalence requires that the implementation CRN, under such an interpretation, contains exactly the same reactions as the formal CRN. In particular, this ensures that any reaction pathway that exists in one CRN has a corresponding pathway in the other.
- Pathway decomposition equivalence. Another notion stronger than reachability equivalence, but neither implying nor implied by bisimulation equivalence, is pathway decomposition equivalence. The main observation that gives rise to this notion is that most pathways of the implementation CRN can be formed by composing smaller pathways. We call those pathways that cannot be thus decomposed "prime pathways". The implementation CRN is pathway decomposition equivalent to the formal CRN if they have the same set of prime pathways.
In our work group we studied how these notions compare to those that naturally arise in category theory. The key observation, due to Jose Meseguer, Ugo Montanari and Vladimiro Sassone in the early 1990s, is that any Petri net gives rise to a "symmetric monoidal category": a category where there is a way of adding objects and adding morphisms. However, the formalism of Petri nets is just another language for talking about chemical reaction networks, so any chemical reaction network also gives a symmetric monoidal category. The objects are the formal linear combinations of species, e.g. $A + B + 2C$ where $A, B$, and $C$ are chemical species. Addition of these is defined in the obvious way. The morphisms are the reaction pathways, built from the basic reactions in the CRN by composition and addition.
There are various kinds of maps and equivalences between symmetric monoidal categories:
- Symmetric monoidal functor - this is the simplest kind of map between symmetric monoidal categories; it sends objects to objects and morphisms to morphisms in a way that preserves composition and addition.
- Symmetric monoidal equivalence - this is a symmetric monoidal functor $F: C \to D$ equipped with a symmetric monoidal functor $G: D \to C$ that serves as an inverse. Two symmetric monoidal categories that have an equivalence of this sort between them are the same for all practical purposes.
- Symmetric monoidal adjunction - this concept is intermediate between the previous two. This is a symmetric monoidal functor $F: C \to D$ equipped with a symmetric monoidal functor $G: D \to C$ that obeys conditions weaker than those of an inverse. In category theory adjunctions are considered very important and much more interesting than equivalences.
It is natural to ask how these concepts relate to the concepts of equivalence for CRNs. Suppose $C$ and $D$ are two symmetric monoidal categories $C$ and $D$ coming from CRNs: $C$ coming from the formal CRN and $D$ coming from the implementation CRN. The existence of a symmetric monoidal functor $F: C \to D$ implies that given formal states $S$ and $S'$, if $S'$ is reachable from $S$ in the formal CRN then it is reachable in the implementation CRN. However, the converse may not hold. Thus, reachability equivalence may not hold.
If there is a symmetric monoidal equivalence $F: C \to D$, then reachability equivalence holds, as well as bisimulation equivalence. However, symmetric monoidal equivalence is too strong to hold in most examples found in practice. We successfully applied the more flexible notion of symmetric monoidal adjunction to one realistic example, but we proved that bisimulation equivalence does not imply the existence of a symmetric monoidal adjunction. An important open question is thus to find additional conditions on a symmetric monoidal adjunction that imply bisimulation equivalence.