You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Let $s = (E,\seq,\cover,\prec,\dashv,\labl)$ be a linear extension of an augmented poset.
5
-
In the algorithm proposed on~\autoref{sec:concret} we change~\autoref{eq:refine} so that instead of computing a new decoration for each new poset $s_2$ (line~\autoref{eq:dec}), we use the existing decoration $(s_1)^{\star}$ of $s_1$ and only refine the trace w.r.t. to the decorations for the new event $e$ added to the trace.
5
+
In the algorithm proposed on~\autoref{sec:concret} we change~\autoref{eq:refine} so that instead of computing a new decoration for each new poset $s_2$ (\autoref{eq:dec}), we use the existing decoration $(s_1)^{\star}$ of $s_1$ and only refine the trace w.r.t. to the decorations for the new event $e$ added to the trace.
6
+
7
+
Also we change the interpretation of the refinement function $\mathtt{Ref}$: instead of a bijection between events and transitions in $\theta$, we use a bijection between events and transitions positions in $\theta$ (\autoref{eq:ith_trans}). The update of $\mathtt{Ref}_1$ to $\mathtt{Ref}_2$ is then straightforward.
Id graphs will help us keep track of the decorations.
40
43
41
44
\begin{remark}
42
-
We make the following simplifying assumption on events: if an event uses an already introduced node than it appears in one of its decorations. All nodes in an event that are no part of any decorations are \emph{new} nodes that have \emph{fresh identifiers}, not used by any other node in the trace.
45
+
\label{rm:simply}
46
+
We make two simplifying assumptions. First, if an event uses an already introduced node than it appears in one of its decorations. All nodes in an event that are no part of any decorations are \emph{new} nodes that have \emph{fresh identifiers}, not used by any other node in the trace.
47
+
48
+
Secondly, we will assume that for any node there exists an event that introduces it. This assumption allows us to reason by induction on the linearisation of a poset.
43
49
\end{remark}
44
50
45
-
We give the algorithm for $\mathsf{refine}$ below. It consists of first updating the graph $L$ of a production $p$ to account for all decorations in $\mathit{spans}$ (\autoref{eq:idprod1} to~\autoref{eq:idprod2}).
51
+
The following example shows how much the simplfying assumptions help.
52
+
\begin{example}
53
+
Let us consider the poset of events $e_1,e_2,e_3,e_4$ with $e_3\dashv e_1$, $e_3\dashv e_2$ and all events $e_1,e_2,e_3$ causing event $e_4$. The rules are the following
We can see that for such a poset we cannot construct the trace by induction on any linearisation. The constraint of node $A$ being the same node in both $e_1$ and $e_2$ only shows when event $e_3$ is considered.
58
+
\end{example}
59
+
60
+
We give the algorithm for $\mathsf{refine}$ below. It consists of first updating the graph $L$ of a production $p$ to account for all decorations in $\mathit{spans}$ (\autoref{eq:idprod1} to~\autoref{eq:idprod2}). Then a new transition $t$ is obtained from $p$ (\autoref{eq:newt}).
61
+
%Then the graphs in the trace are updated to account for the new added transition (\autoref{eq:newtrace}).
The trace $\theta:M_1\Rightarrow M_2\cdots M_n$ is obtained by induction on $s_1$, therefore $M_1,\cdots M_n$ are id graphs.
61
83
62
-
Let us first show that producing an id graph from $L$ in \autoref{eq:idprod1} to \autoref{eq:idprod2} is correct: there are no two decorations that disagree on the identifier of a node.
84
+
Let us first show that producing an id graph from $L$ in \autoref{eq:idprod1} to \autoref{eq:idprod2} is correct: there are no two decorations that disagree on the identifier of a node. The second part of the following lemma says that adding a new transition to the trace does not reintroduce node identifiers.
63
85
64
86
\begin{lemma}
65
87
Let us suppose we have the following:
66
88
\begin{itemize}
67
89
\item two linear augmented posets $s_1$, $s_2$ such that $s_2=s_1\cup\{e\}$ and $e$ is maximal in $s_2$;
68
90
\item two valid decorations for the two posets $s_1^{\star}$ and $s_2^{\star}$ with $s_2^{\star}\subseteq s_1^{\star}$;
69
91
\item a trace $\theta:M_1\Rightarrow M_2\cdots M_n$ such that $\mathsf{decoration\_of\_trace}(\theta)=(s_1)^{\star}$ and such that $M_1,\cdots M_n$ are id graphs;
70
-
\item two decorations of $e$ in $s_2^{\star}$, $\mathit{span}_1$ and $\mathit{span}_2$ such that either
92
+
\end{itemize}
93
+
\begin{enumerate}
94
+
\item For two decorations of $e$ in $s_2^{\star}$, $\mathit{span}_1$ and $\mathit{span}_2$ such that either
71
95
\begin{enumerate}
72
-
\item$L_1\overset{g_1}{\remb} O_1\overset{o_1}{\lemb} L \overset{o_2}{\remb} O_2\overset{g_2}{\lemb} L_2$ or
73
96
\item$R_1\overset{g_1}{\remb} O_1\overset{o_1}{\lemb} L \overset{o_2}{\remb} O_2\overset{g_2}{\lemb} R_2$ or
97
+
\item$L_1\overset{g_1}{\remb} O_1\overset{o_1}{\lemb} L \overset{o_2}{\remb} O_2\overset{g_2}{\lemb} L_2$ or
74
98
\item$L_1\overset{g_1}{\remb} O_1\overset{o_1}{\lemb} L \overset{o_2}{\remb} O_2\overset{g_2}{\lemb} R_2$.
75
99
\end{enumerate}
76
-
\end{itemize}
77
-
Then for all $n\in L$ such that $o_1^{-1}(n) = n_1\in O$ and $o_2^{-1}(n) = n_2\in O$, $\text{id}(g_1(n_1)) = \text{id}(g_2(n_2))$.
100
+
we have that for all $n\in L$ such that $o_1^{-1}(n) = n_1\in O$ and $o_2^{-1}(n) = n_2\in O$, $\text{id}(g_1(n_1)) = \text{id}(g_2(n_2))$.
101
+
\item Let $L_I$ be the id graph constructed as in \autoref{eq:idprod1} to~\autoref{eq:idprod2}. Then $L_I\subseteq M_n$.
102
+
\end{enumerate}
78
103
\end{lemma}
79
104
\begin{proof}
80
105
\begin{enumerate}
81
106
\item
82
-
\item It follows that there exists $e_1,e_2\in s_2^{\star}$ such that $e\redl{+}_{\mathit{span}_1} e_1$ and $e\redl{+}_{\mathit{span}_2} e_2$ and that the constraint on decorating forks in~\autoref{def:constraints_poset} is not satisfied. Contradiction with the hypothesis that $s_2^{\star}$ is a valid decoration.
107
+
\begin{enumerate}
108
+
\item It follows that there exists $e_1,e_2\in s_2^{\star}$ such that $e_1\redl{+}_{\mathit{span}_1} e$ and $e_2\redl{+}_{\mathit{span}_2} e$ and that the constraint on decorating positive meets in~\autoref{def:constraints_poset} is not satisfied. Contradiction with the hypothesis that $s_2^{\star}$ is a valid decoration.
109
+
\item Thanks to our symplifying assumption~\autoref{rm:simply} there exists an event $e_3$ which introduces node $n_1$. It follows then $e_3\redl{+}_{\mathit{span}_3} e_1$ where node $n_1$ is in the decoration $\mathit{span}_3$. Either $e_3\redl{+}_{\mathit{span}_3'} e_2$ with $n_2$ in the decoration $\mathit{span}_3'$ in which case, by induction we have that $\text{id}(n_1) = \text{id}(n_2)$, or $\neg(e_3\redl{+}_{\mathit{span}_3'} e_2)$. This contradicts the constraint on decorating forks of negative influence in~\autoref{def:constraints_poset}.
110
+
\item It follows that there exists $e_1,e_2\in s_2^{\star}$ such that $e_2\redl{+}_{\mathit{span}_2} e$ and $e\redl{-}_{\mathit{span}_2} e_1$. But then there exists a span ${\mathit{span}_3}$ such that $e_2\redl{+}_{\mathit{span}_3} e_1$ and the constraint on decorating positive forks in~\autoref{def:constraints_poset} is again not satisfied.
83
111
\end{enumerate}
112
+
\item Suppose that there exists $n\in L_I$ and $n\notin M_n$. From the symplifying assumption~\autoref{rm:simply} there exists an event $e_1$ which introduces node $n$. But $n\notin M_n$, implies that there exists an event $e_2$ which "consumes"$n$, i.e. $e_1\redl{+}_n e_2$ and $e_2\redl{-}_n e$. %we cannot use this last part $e_2\redl{-}_n e$ because we haven't yet proved that the concretisation of s2 doesn't introduce extra decorations.
113
+
From $e_1\redl{+}_n e_2$ and $e_1\redl{+}_n e$ we have that the constraint on decorating positive forks in~\autoref{def:constraints_poset} is not satisfied.
114
+
\end{enumerate}
115
+
\end{proof}
116
+
117
+
%A corollary for the second part of the lemma above is that the $\mathsf{refine}$ function does not create extra decorations, i.e. $\mathsf{decoration\_of\_trace}(\theta_2)=(s_2)^{\star}$. This is one part in the correction theorem below.
118
+
119
+
\begin{theorem}
120
+
Let $s_1$ be a linear augmented poset, let $\theta_1$ be a trace and $\mathtt{Ref}_1$ a refinement function on $\theta_1$ such that for any events $e_1,e_2\in s_1$
Let $s_2$ be a linear augmented poset such that $s_2=s_1\cup\{e\}$ and $e$ is maximal in $s_2$.
128
+
For any $\theta_2$ and $\mathtt{Ref}_2$ obtained by $\mathsf{concretise}(s_2,s_1,\{(\theta_1,\mathtt{Ref}_1)\})$ the conditions~\autoref{eq1}, \autoref{eq2} hold.
129
+
\end{theorem}
130
+
\begin{proof}
131
+
Let $s_1^{\star}$ be a decoration of $s_1$ such that $\mathsf{decoration\_of\_trace}(\theta_1)=(s_1)^{\star}$.
132
+
First we note that we can translate conditions~\autoref{eq1}, \autoref{eq2} on decorations:
Copy file name to clipboardExpand all lines: notes/influence_stories.tex
+6-6Lines changed: 6 additions & 6 deletions
Original file line number
Diff line number
Diff line change
@@ -189,7 +189,7 @@ \subsection{From posets to traces}
189
189
Let $\underline s=(E,\cover,\prec,\dashv,\labl)$ be an augmented poset $s$.
190
190
A \emph{concretisation} of $s$ is a triple $(s,\theta,\mathtt{Ref}:E\leftrightarrow\theta)$ such that $\mathtt{Ref}$ is a refinement function and such that
where $\mathsf{decorate}$ returns a decoration of $s$ as in~\autoref{def:decorate_poset}, $\mathsf{decoration\_of\_trace}$ is an abstraction of a trace to its decorated poset, defined in the~\autoref{sec:abstract_decoration}, $\mathsf{valid}$ is from~\autoref{def:constraints_poset} and lastly, $\mathsf{refine}$ is a function that extends a trace and a refinement to the new event $e$. We provide more details for $\mathsf{refine}$ in the appendix. Also in the appendix, we show that at each call of $\mathsf{concretise}$, the concretisations obtained so far are correct w.r.t.~\autoref{def:concret}.
0 commit comments