new

Author: Ioana

notes/graph_rewrite.tex

@@ -3,7 +3,7 @@ \section{Transition systems for graph rewriting}
 \subsection{Graph rewriting}
 
 \begin{definition}[Category of simple graphs]
-  We define the category of \emph{simple graphs} where
+  We define the category of \emph{simple graphs} $\mathcal{G}$ where
   \begin{itemize}
   \item objects are graphs: $G = (V,E)$ with $V$ a set of nodes and $E$ a binary symmetric reflexive relation on nodes, representing the edges;
   \item morphisms $h:G_1\to G_2$ are functions on nodes $h_V:V_1\to V_2$ that preserve edges: $(s,t)\in E_1\implies (h_V(s),h_V(t))\in E_2$. We denote $h_E$ the function on edges: $h_E(s,t) = (h_V(s), h_V(t))$.
@@ -103,51 +103,53 @@ \subsection{Graph rewriting}
 \subsection{Transition systems}
 \label{sec:ts}
 
-\begin{definition}[Transition systems]
-  \label{def:ts_nielsen}
-%\cite{NielsenRT92}
-  A transition system is a structure $TS = (Q,E,T)$ where $Q$ is a set of states, $E$ is a set of events and $T\subseteq Q\times E\times Q$ is a set of labelled transitions. Let $q_{\text{init}}\in Q$ be a special state, called the \emph{initial} state. Moreover a transition system satisfies the following axioms:
-  \begin{itemize}
-  \item no redundant events: $\forall e\in E$, $\exists (s,e,s')\in T$;
-  \item all states are reachable: $\forall q\in Q$, $\exists q_0,\cdots q_n \in Q$ and $\exists e_o,\cdots e_n\in E$ such that $q_{\text{init}} = q_0$, $q_n =q$ and $(q_i,e_i,q_{i+1}) \in T$.
-%  \item no circles:$\forall (s,e,s')\in T$, $s\neq s'$;
-%  \item each pair of states connected by a single transition: $\forall (s,e_1,s_1), (s,e_2,s_2)\in T$, $s_1=s_2\implies e_1=e_2$.
-  \end{itemize}
-\end{definition}
+%% \begin{definition}[Transition systems]
+%%   \label{def:ts_nielsen}
+%% %\cite{NielsenRT92}
+%%   A transition system is a structure $TS = (Q,E,T)$ where $Q$ is a set of states, $E$ is a set of events and $T\subseteq Q\times E\times Q$ is a set of labelled transitions. Let $q_{\text{init}}\in Q$ be a special state, called the \emph{initial} state. Moreover a transition system satisfies the following axioms:
+%%   \begin{itemize}
+%%   \item no redundant events: $\forall e\in E$, $\exists (s,e,s')\in T$;
+%%   \item all states are reachable: $\forall q\in Q$, $\exists q_0,\cdots q_n \in Q$ and $\exists e_o,\cdots e_n\in E$ such that $q_{\text{init}} = q_0$, $q_n =q$ and $(q_i,e_i,q_{i+1}) \in T$.
+%% %  \item no circles:$\forall (s,e,s')\in T$, $s\neq s'$;
+%% %  \item each pair of states connected by a single transition: $\forall (s,e_1,s_1), (s,e_2,s_2)\in T$, $s_1=s_2\implies e_1=e_2$.
+%%   \end{itemize}
+%% \end{definition}
 
-We denote $t:(s,e,s')$ a transition. Transitions can be composed $t_1;t_2$ if the source state of $t_2$ matches the destination state of $t_1$. A \emph{trace} $\theta$ is a sequence of composable transitions: $\theta=t_1;t_2;\cdots t_n$. Two traces $\theta:t_1;\cdots t_n$ and $\theta':t_1';\cdots t_n'$ can be composed if $t_n$ and $t_1'$ are composable: $\theta;\theta':t_1;\cdots t_n;t_1;\cdots t_n'$.
 
 \begin{definition}[TS on graphs]
-  A transition system on graphs $TS = (Q,R,E,T)$ consists of
+  A transition system on graphs $TS = (Q,R,T)$ consists of
   \begin{itemize}
-  \item a set of states $Q$, where each state is a simple graph;
+  \item a set of states $Q\subseteq \mathcal{G}$, where each state is a simple graph;
   \item a set of rules or productions, $R$;
-  \item a set of events $E$, where each event $e=(p:L\action R,G,m:L\emb G)$ is a triple consisting of a rule $p\in R$, a graph $G$ and a function $m$ that selects one matching $L\emb G$. For an event $e$, we define two functions $\labl(e) = p$ and $m(e) = L\emb G$.
-  \item a set of labelled transition $T\subseteq Q\times E\times Q$, where each transition $M \overset{e}{\Rightarrow} N$ is a DPO rewriting step with the production $\labl(e) = p$ and the matching $m(e) = L\emb M$:
-    \[
-    \begin{tikzpicture} %[scale=0.8]
-      \node (l) at (-1.5,0) {\(L\)};
-      \node (r) at (0,0) {\(R\)};
-      \node (m) at (-1.5,1.5) {\(M\)};
-      \node (n) at (0,1.5) {\(N\)};
-      \draw [->] (l) -- node [left,midway] {\(m(e)\)}  (m);
-      \draw [>=latex, ->] (l) -- (r);
-      \draw [>=latex, ->] (m) -- (n);
-      \draw [->] (r) -- (n);
-    \end{tikzpicture}
-    \]
-    We sometimes write $M\overset{m(e),\labl(e)}{\Rightarrow} N$.
+%  \item a set of events $E$, where each event $e=(p:L\action R,G,m:L\emb G)$ is a triple consisting of a rule $p\in R$, a graph $G$ and a function $m$ that selects one matching $L\emb G$. For an event $e$, we define two functions $\labl(e) = p$ and $m(e) = L\emb G$.
+  \item a set of labelled transition $T\subseteq Q\times \text{hom}(\mathcal{G})\times R\times Q$, where each transition $M \overset{m,p}{\Rightarrow} N$ is a DPO rewriting step with the production $p\in R$, $p:L\lemb K\remb R$ and the matching $m:L\emb M$.
+    %% \[
+    %% \begin{tikzpicture} %[scale=0.8]
+    %%   \node (l) at (-1.5,0) {\(L\)};
+    %%   \node (r) at (0,0) {\(R\)};
+    %%   \node (m) at (-1.5,1.5) {\(M\)};
+    %%   \node (n) at (0,1.5) {\(N\)};
+    %%   \draw [->] (l) -- node [left,midway] {\(m(e)\)}  (m);
+    %%   \draw [>=latex, ->] (l) -- (r);
+    %%   \draw [>=latex, ->] (m) -- (n);
+    %%   \draw [->] (r) -- (n);
+    %% \end{tikzpicture}
+    %% \]
+    %We sometimes write $M\overset{m(e),\labl(e)}{\Rightarrow} N$.
   \end{itemize}
-  Moreover $TS$ satisfy the axioms of~\autoref{def:ts_nielsen}.
+  %Moreover $TS$ satisfy the axioms of~\autoref{def:ts_nielsen}.
 \end{definition}
 
+%We denote $t:(s,e,s')$ a transition.
+Transitions can be composed $t_1;t_2$ if the source state of $t_2$ matches the destination state of $t_1$. A \emph{trace} $\theta$ is a sequence of composable transitions: $\theta=t_1;t_2;\cdots t_n$. Two traces $\theta:t_1;\cdots t_n$ and $\theta':t_1';\cdots t_n'$ can be composed if $t_n$ and $t_1'$ are composable: $\theta;\theta':t_1;\cdots t_n;t_1;\cdots t_n'$.
+
 \begin{definition}[Independence relation on transitions~\cite{AlgebraicGR}]
   \label{def:indep}
   $~$
   \begin{description}
   \item[sequential independence]
     Let $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M_1\overset{m_2,p_2}{\Rightarrow} M_2$ be two transitions.
-    $t_1 \Diamond_{\text{seq}} t_2$ iff there exists the morphism $i:R_1\to D_2$ such that $f_2\circ i= m_2$ and there exists the morphism $j:L_2\to D_1$ such that $g_1\circ j= m_1$:
+    $t_1 \Diamond_{\text{seq}} t_2$ iff there exists the morphism $i:R_1\to D_2$ such that $i\circ f_2 = n_1$ and there exists the morphism $j:L_2\to D_1$ such that $j\circ g_1= m_2$:
     \[
     \begin{tikzpicture} %[scale=0.8]
     \node (r1) at (1.5,0) {\(R_1\)};
@@ -171,7 +173,7 @@ \subsection{Transition systems}
     \]
   \item[parallel independence]
     Let $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M\overset{m_2,p_2}{\Rightarrow} M_2$ be two transitions.
-    $t_1 \Diamond_{\text{par}} t_2$ iff there exists the morphism $i:L_1\to D_2$ such that $f_2\circ i= m_2$ and there exists the morphism $j:L_2\to D_1$ such that $f_1\circ j= m_1$:
+    $t_1 \Diamond_{\text{par}} t_2$ iff there exists the morphism $i:L_1\to D_2$ such that $i\circ f_2= n_1$ and there exists the morphism $j:L_2\to D_1$ such that $j\circ f_1= m_2$:
     \[
     \begin{tikzpicture} %[scale=0.8]
     \node (r1) at (1.5,0) {\(L_1\)};
@@ -207,40 +209,67 @@ \subsection{Transition systems}
 
 Let $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M\overset{m_2,p_2}{\Rightarrow} M_2$ be two parallel independent transitions.  Let us denote $t_2/t_1:M_1\overset{m_2',p_2}{\Rightarrow} M'$ and $t_1/t_2:M_2\overset{m_1',p_1}{\Rightarrow} M'$ the two transitions we obtained by~\autoref{church_rosser}.
 
-\begin{definition}[Equivalence class on transitions and traces]
-We define an equivalence class on transitions, denoted $\congr$ as the least equivalence relation which satisfies $t_1\congr t_1/t_2$ and $t_2\congr t_2/t_1$, for any two transitions $t_1$ and $t_2$ parallel independent.
+\begin{definition}[Equivalence up to permutation on traces]
+Define an equivalence up to permutations on traces, denoted $\congr$, as the least equivalence relation satisfying $t_1;(t_2/t_1)\congr t_2;(t_1/t_2)$.
+\end{definition}
 
-Define an equivalence up to permutations on traces, as the least equivalence relation satisfying $t_1;(t_2/t_1)\congr t_2;(t_1/t_2)$.
+\begin{definition}[Equivalence on transitions]
+  Let $\sim$ be a binary relation on transitions such that for any two transitions $t_1\Diamond_{\text{par}} t_2$ and such that there exists $t_3$ and $t_4$ with $t_1;t_3\congr t_2;t_4$ then $t_1\sim t_4$ and $t_2\sim t_3$.
 \end{definition}
 
-Note that, from~\autoref{church_rosser}, for two sequential independent transitions $t_1$ and $t_2$ we have that $t_1\congr t_1'$ and $t_2\congr t_2'$, where $t_1'$ and $t_2'$ are obtained by commutation.
+The following property shows that one can define the equivalence relation above using sequential independent transitions as well.
+
+\begin{property}
+  Let $\sim'$ be a binary relation on transitions such that if $t_1\Diamond_{\text{seq}} t_2$ and there exists $t_3$ and $t_4$ with $t_1;t_2\congr t_3;t_4$ then $t_1\sim' t_4$ and $t_2\sim' t_3$. Then for any transitions $t_i$, $i\in\{1,..,4\}$ such that $t_1;t_2\congr t_3;t_4$ we have that
+  \begin{align*}
+    t_1 \sim' t_4\text{ and }t_2\sim' t_3 \iff t_1 \sim t_4\text{ and }t_2\sim t_3
+  \end{align*}
+\end{property}
+
+%We define an equivalence class on transitions, denoted $\congr$ as the least equivalence relation which satisfies $t_1\congr t_1/t_2$ and $t_2\congr t_2/t_1$, for any two transitions $t_1$ and $t_2$ parallel independent.
+%Note that, from~\autoref{church_rosser}, for two sequential independent transitions $t_1$ and $t_2$ we have that $t_1\congr t_1'$ and $t_2\congr t_2'$, where $t_1'$ and $t_2'$ are obtained by commutation.
 
 %We equip a graph transition system $(Q,R,E,T)$ with an irreflexive, symmetric relation on events $\Diamond\subseteq E\times E$, called independence, such that $e_1\Diamond e_1$ iff $e_1\Diamond_{\text{seq}} e_1$ or $e_1\Diamond_{\text{par}} e_1$.
 
-\begin{definition}[Sequential dependence]
-  \label{def:seq_dep}
-  Transitions $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are sequential dependent, denoted $t_1 < t_2$, if there exists no morphism $j:L_2\to D_1$ such that $f_1\circ j= m_1$.
+\begin{definition}[Dependence relation on transitions]
+  \label{def:dep}
+  \begin{description}
+  \item[] $~$
+  \item[sequential dependence]
+    \label{def:seq_dep}
+    Transitions $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are sequential dependent, denoted $t_1 < t_2$, if there exists no morphism $j:L_2\to D_1$ such that $j\circ g_1= m_2$.
+
+  \item[parallel dependence]
+    \label{def:inhibition}
+    A transition $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ inhibits another transition $t_2:M\overset{m_2,p_2}{\Rightarrow} M_2$, denoted $t_1 \dashv t_2$, if there is no morphisms $j:L_2\to D_1$ such that $j\circ f_1= m_2$. The two transitions are parallel dependent if they are inhibiting each other.
+  \end{description}
 \end{definition}
 
-\autoref{def:seq_dep} implies that if $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are sequential dependent then there is no graph $M'\in Q$ such that there exists the transitions
+\autoref{def:dep}, \autoref{def:seq_dep} implies that if $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are sequential dependent then there is no graph $M'\in Q$ such that there exists the transitions
 $t_2':M\overset{m_2',p_2}{\Rightarrow} M'$ and $t_1':M'\overset{m_1',p_1}{\Rightarrow} M_2$ with $t_1\Diamond_{\text{par}}t_2'$.
 
-\begin{definition}[Parallel dependence]
-  \label{def:inhibition}
-  A transition $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ inhibits another transition $t_2:M\overset{m_2,p_2}{\Rightarrow} M_2$, denoted $t_1 \dashv t_2$, if there is no morphisms $j:L_2\to D_1$ such that $f_1\circ j= m_1$. The two transitions are parallel dependent if they are inhibiting each other.
-\end{definition}
-
-From~\autoref{def:inhibition} we have that if $t_1 \dashv t_2$ then there is no graph $M'\in Q$ such that there exists the transitions $t_2':M_1\overset{m_2',p_2}{\Rightarrow} M'$ with $t_1\Diamond_{\text{seq}}t_2'$.
+From~\autoref{def:dep}, \autoref{def:inhibition} we have that if $t_1 \dashv t_2$ then there is no graph $M'\in Q$ such that there exists the transitions $t_2':M_1\overset{m_2',p_2}{\Rightarrow} M'$ with $t_1\Diamond_{\text{seq}}t_2'$.
 
 \begin{lemma}
-  If two transitions $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2: M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are not sequential independent, then either $t_1 < t_2$ or $t_2\dashv t_1$ (or both).
+  \label{lem:not_seq_ind}
+  If two transitions $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2: M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are not sequential independent, then either (i) $t_1 < t_2$ or (ii) there exists a morphism $j:L_2 \to M$ such that $j\circ g_1 = m_2$ and therefore there exists $M_2'$ and $t_2':M\overset{j\circ f_1,p_2}{\Rightarrow} M_2'$ with $t_2'\dashv t_1$.
 \end{lemma}
 \begin{proof}
-  If $M\overset{m_1,p_1}{\Rightarrow} M_1$ and $M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are not sequentially independent, from~\autoref{def:indep}, it follows that either (i) there is no morphism $j:L_2\to D_1$ such that $g_1\circ j= m_1$ and then $(p_1,M,m_1) < (p_2,M_1,m_2)$ or (ii)
-there is no morphism $i:R_1\to D_2$ such that $f_2\circ i= m_2$. Suppose for the latter case, that there is $j:L_2\to D_1$ such that $g_1\circ j= m_1$. It implies, from~\autoref{church_rosser} that there exists $M'\in Q$ and $M\overset{m_2',p_2}{\Rightarrow} M'$ and that $(p_1,M,m_1)$ is not parallel independent of $(p_2,M,m_2')$. From the definition of parallel independence the only possibility is that there is no morphism $i:L_1\to D_2$ such that $f_2\circ i= m_2$. \autoref{def:inhibition} implies then that $(p_2,M,m_2)\dashv(p_1,M,m_1)$.
+  If $M\overset{m_1,p_1}{\Rightarrow} M_1$ and $M_1\overset{m_2,p_2}{\Rightarrow} M_2$ are not sequentially independent, from~\autoref{def:indep}, it follows that either (i) there is no morphism $j:L_2\to D_1$ such that $j\circ g_1= m_2$ and then $t_1 < t_2$ or
+(ii) there is no morphism $i:R_1\to D_2$ such that $i\circ f_2= n_1$. In the latter case, there is $j:L_2\to D_1$ such that $j\circ g_1= m_2$. It implies, from~\autoref{church_rosser} that there exists $M'\in Q$ and $t_2':M\overset{m_2',p_2}{\Rightarrow} M'$ and that $t_1$ is not parallel independent of $t_2'$. From the definition of parallel independence the only possibility is that there is no morphism $i:L_1\to D_2$ such that $i\circ f_2= n_1$. \autoref{def:inhibition} implies then that $t_2'\dashv t_1$.
 \end{proof}
 
+\begin{definition}[Equivalence on transitions]
+  Let $t_1:M_1\overset{m_1,p_1}{\Rightarrow} M_2$ and $t_2:M_2\overset{m_2,p_2}{\Rightarrow} M_3$ be two sequential transitions such that $\neg(t_1<t_2)$ and $\neg(t_1\Diamond_{\text{seq}}t_2)$. Denote $t_2|t_1$ the transition obtained by~\autoref{lem:not_seq_ind}.
+
+  Let $\sim_{\dashv}$ be a binary relation on transitions such that $t_2\sim_{\dashv}t_2|t_1$.
+
+  The equivalence relation on transitions, $\simeq$ is defined as the symmetric, reflexive and transitive closure of $\sim\cup\sim_{\dashv}$.
+\end{definition}
+
 \begin{lemma}
   If two transitions $t_1:M\overset{m_1,p_1}{\Rightarrow} M_1$ and $t_2:M\overset{m_2,p_2}{\Rightarrow} M_2$ are not parallel independent then either $t_1\dashv t_2$ or $t_2\dashv t_1$ (or both).
 \end{lemma}
-The proof is similar to the one above.
+\begin{proof}
+  It follows from~\autoref{def:indep}.
+\end{proof}

notes/influence.tex

@@ -74,7 +74,7 @@ \subsection{Influence}
 
   Let the cospan $R_1\lemb M\remb L_2$ be in the multisum of $R_1$ and $L_2$, from which we get the span $R_1\leftarrow O\rightarrow L_2$ as pullback.
 
-  There is a \emph{positive influence} between the two rules induced by $O$ and denoted $r_1\redl{+}_o r_2$ if the pullback of the cospan $D_1\lemb R_1\remb O$, denoted $P$, and $O$ is not an iso. In other words, $O$ is not contained in $P$.
+  There is a \emph{positive influence} between the two rules induced by the cospan $s:R_1\remb O\lemb L_2$ and denoted $r_1\redl{+}_s r_2$ if the pullback of the cospan $D_1\lemb R_1\remb O$, denoted $P$, and $O$ is not an iso. In other words, $O$ is not contained in $P$.
   \[
   \begin{tikzpicture} %[scale=0.8]
     \node (p) at (0,-1) {\(P\)};
@@ -95,16 +95,16 @@ \subsection{Influence}
   \end{tikzpicture}
   \]
 
-  Define $r_1\redl{+} r_2$ if there exists $O$ such that $r_1\redl{+}_o r_2$.
+  Define $r_1\redl{+} r_2$ if there exists $s$ such that $r_1\redl{+}_s r_2$.
 \end{definition}
 
-Similarly, define the negative influence $r_1\redl{-}_O r_2$ if there exists the span $L_1{\remb} O {\lemb} L_2$ and there is no iso between the pullback of the cospan $D_1\lemb L_1\remb O$ and $O$.
+Similarly, define the negative influence $r_1\redl{-}_s r_2$ if there exists the span $s:L_1{\remb} O {\lemb} L_2$ and there is no iso between the pullback of the cospan $D_1\lemb L_1\remb O$ and $O$.
 
 \begin{definition}[Causal pair]
   \label{def:causal_pair}
   Let $p_1:L_1{\remb} D_1 {\lemb} R_1$ and $p_2:L_2{\remb} D_2 {\lemb} R_2$ be two rules.
 
-  A pair $P_1\overset{m_1,p_1}{\Rightarrow} M\overset{m_2,p_2}{\Rightarrow} P_2$ is a \emph{causal pair} if the cospan $R_1{\remb}M{\lemb}L_2$ is in the multisum of $R_1$ and $L_2$ and $p_1\redl{+}_O p_2$, where $O$ is the pullback of the cospan $R_1{\remb}M{\lemb}L_2$:
+  A pair $P_1\overset{m_1,p_1}{\Rightarrow} M\overset{m_2,p_2}{\Rightarrow} P_2$ is a \emph{causal pair} if the cospan $R_1{\remb}M{\lemb}L_2$ is in the multisum of $R_1$ and $L_2$ and $p_1\redl{+}_s p_2$, where $s$ is the pullback of the cospan $R_1{\remb}M{\lemb}L_2$:
   \[
   \begin{tikzpicture} %[scale=0.8]
     \node (o) at (1,0) {\(O\)};
@@ -210,7 +210,7 @@ \subsection{Influence}
 \begin{definition}[Inhibiting pair]
   Let $p_1:L_1{\remb} D_1 {\lemb} R_1$ and $p_2:L_2{\remb} D_2 {\lemb} R_2$ be two rules.
 
-  A pair $P_1\overset{m_1,p_1}{\Leftarrow} M\overset{m_2,p_2}{\Rightarrow} P_2$ is an \emph{inhibiting pair} if the cospan $L_1{\remb}M{\lemb}L_2$ is in the multisum of $L_1$ and $L_2$ and $p_1\redl{-}_O p_2$, where $O$ is the pullback of the cospan $L_1{\remb}M{\lemb}L_2$:
+  A pair $P_1\overset{m_1,p_1}{\Leftarrow} M\overset{m_2,p_2}{\Rightarrow} P_2$ is an \emph{inhibiting pair} if the cospan $L_1{\remb}M{\lemb}L_2$ is in the multisum of $L_1$ and $L_2$ and $p_1\redl{-}_s p_2$, where $s$ is the pullback of the cospan $L_1{\remb}M{\lemb}L_2$:
   \[
   \begin{tikzpicture} %[scale=0.8]
     \node (o) at (1,0) {\(O\)};