162 lines
No EOL
6.4 KiB
TeX
162 lines
No EOL
6.4 KiB
TeX
\documentclass[99-notes-packed.tex]{subfiles}
|
|
|
|
\begin{document}
|
|
\paragraph*{Congurence}
|
|
If an equivalence relation is a \textit{congurence} for an operator -- i.e., an operator is \textit{compositional} for the equivalence -- then there exists a sort of isomorphism detailed as follows:
|
|
|
|
\begin{definition}[congurence]
|
|
An equivalence $\sim$ is a \textbf{congruence} for a language $\mathcal{L}$ if:
|
|
\begin{equation*}
|
|
\forall C[\ ] \in \mathcal{L}: P \sim Q \implies C[P] \sim C[Q]
|
|
\end{equation*}
|
|
where:
|
|
\begin{itemize}
|
|
\item $C[\ ]$ (context) represents a $\mathcal{L}$-expression with a hole in it, plugged (e.g., with $P$) as $C[P]$.
|
|
\end{itemize}
|
|
|
|
For example, let $P = a.[\ ]$:
|
|
\begin{equation*}
|
|
\begin{prooftree}
|
|
\hypo{P = Q}
|
|
\infer1{a.P = a.Q}
|
|
\end{prooftree}
|
|
\end{equation*}
|
|
Equivalently, we can say that $CCP.(.)$ is compositional under equality ($=$).
|
|
\end{definition}
|
|
|
|
\begin{example}[$=_{CT}$ and $\partial_{H}$]
|
|
This is a counterexample for showing why $=_{CT}$ is NOT a congurence over ACP. Obviously:
|
|
\begin{equation*}
|
|
a.b + a.c =_{CT} a.(b + c)
|
|
\end{equation*}
|
|
|
|
However:
|
|
\begin{equation*}
|
|
\partial_{\{c\}}(a.b + a.c) \neq_{CT} \partial_{\{c\}}(a.(b + c))
|
|
\end{equation*}
|
|
\end{example}
|
|
|
|
\begin{definition}[congurence closure]
|
|
A \textbf{congurence closure} $\sim^c$ of $\sim$ wrt. language $\mathcal{L}$ is defined by:
|
|
\begin{equation*}
|
|
P \sim^{c} Q \iff \forall C[\ ] \in \mathcal{L}: C[P] \sim C[Q]
|
|
\end{equation*}
|
|
\end{definition}
|
|
|
|
\paragraph*{Equational Axiomisation}
|
|
In terms of e.g., real addition we describe the operator as possessing e.g., associativity and commutativity, which in turn allows us to do some transformation during analysis, etc.
|
|
|
|
Same goes for operators in e.g, CCS:
|
|
\begin{center}
|
|
\begin{tabular}{cc}
|
|
$(P + Q) + R = P + (Q + R)$ & (associativity) \\
|
|
$P + Q = Q + P$ & (commutativity) \\
|
|
$P + P = P$ & (idempotence) \\
|
|
$P + 0 = P$ & ($0$ as neutral element of $+$)
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
\begin{definition}[CCS: expansion theorem]
|
|
Suppose:
|
|
\begin{center}
|
|
\begin{tabular}{cc}
|
|
$P \coloneqq \sum_{i \in I} a_i.P_i$ &
|
|
$Q \coloneqq \sum_{j \in J} b_i.Q_j$
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
Then,
|
|
\begin{align*}
|
|
P | Q &= \sum_{i \in I} a_i(P_i | Q) \\
|
|
&+ \sum_{i \in I, j \in J} \tau(P_i | Q_j)\ (\mathrm{given\ }a_i = \overline{b_j}) \\
|
|
&+ \sum_{j \in J} b_i(P | Q_j)
|
|
\end{align*}
|
|
|
|
Expressions of the form $\sum a.P$ are aka. \textbf{head normal form}.
|
|
\end{definition}
|
|
|
|
\begin{definition}[Recursive Definition Principle]
|
|
\begin{equation*}
|
|
i \in [1, n]: \langle X_i | E \rangle \in \mathsf{Expr}(X_1 \coloneqq \langle X_1 | E \rangle, \dots, X_n \coloneqq \langle X_n | E \rangle)
|
|
\end{equation*}
|
|
|
|
Basically, some series of expressions for $X_1, \dots, X_n$ exists as solution for $E$.
|
|
\end{definition}
|
|
|
|
\begin{definition}[Recursive Specification Principle]
|
|
If there \underline{exists}
|
|
\begin{equation*}
|
|
i \in [1, n]: y_i \leftarrow \mathsf{Expr}(y_1, \dots, y_n)
|
|
\end{equation*}
|
|
then:
|
|
\begin{equation*}
|
|
i \in [1, n]: y_i = \langle X_i | E \rangle
|
|
\end{equation*}
|
|
|
|
In other words, any $y_{1 \dots n}$ that exists is the sole solution for $E$ modulo bisimulation equivalence.
|
|
\end{definition}
|
|
|
|
\paragraph*{Rooted Bisimilarity}
|
|
We note that depending on semantics of $\mathcal{L}$, equivalences may (and in fact likely) fail to be a congurence over $\mathcal{L}$. This also is the case for e.g., branching bisimilarity: $\tau.a =_{BB} a$ but $\tau.a + b \ne_{BB} a + b$.
|
|
|
|
ACP and CCS fixes this by changing the equivalence operator. CSP fixes this by foregoing the $+$ operator.
|
|
\begin{definition}[Rooted Branching Bisimilarity]
|
|
\begin{align*}
|
|
P =_{rBB} Q \iff &(P \xrightarrow{a} P^{'} \implies Q \xrightarrow{a} Q^{'} \wedge P^{'} =_{BB} Q^{'})\ \wedge \\
|
|
&(Q \xrightarrow{a} Q^{'} \implies P \xrightarrow{a} P^{'} \wedge P^{'} =_{BB} Q^{'})
|
|
\end{align*}
|
|
|
|
$=_{rBB}$ is equivalent to branching bisimulation congruence $=_{BB}^c$ over ACP.
|
|
\end{definition}
|
|
|
|
\begin{definition}[Rooted Weak Bisimilarity]
|
|
\begin{align*}
|
|
P =_{rWB} Q \iff &(P \xrightarrow{a} P^{'} \implies Q \xrightarrow{\tau \ast a \tau \ast} Q^{'} \wedge P^{'} =_{WB} Q^{'})\ \wedge \\
|
|
&(Q \xrightarrow{a} Q^{'} \implies P \xrightarrow{\tau \ast a \tau \ast} P^{'} \wedge P^{'} =_{WB} Q^{'})
|
|
\end{align*}
|
|
|
|
$=_{rWB}$ is equivalent to weak bisimulation congruence $=_{WB}^c$ over CCS.
|
|
\end{definition}
|
|
|
|
\begin{definition}[Eq. axiomisation for rBB, rWB]
|
|
$=_{rWB}$ is axiomatised as follows:
|
|
\begin{align}
|
|
a.\tau.P &= a.P \\
|
|
\tau.P &= \tau.P + P \\
|
|
a.(\tau.P + Q) &= a.(\tau.P + Q) + a.P
|
|
\end{align}
|
|
|
|
$=_{rBB}$ is axiomatised as follows:
|
|
\begin{equation*}
|
|
a.(\tau.(P + Q) + Q) = a.(P + Q)
|
|
\end{equation*}
|
|
\end{definition}
|
|
|
|
\paragraph*{Strongly/Weakly Guarded Recursions}
|
|
Recall that a recursive spec of the form e.g. $X = a.(b + X)$ is guarded -- $X$ exists as a subexpression of $X$ -- and are equivlent modulo strong bisimilarity (viz. RSP).
|
|
|
|
On the other hand $X = \tau.X$ has solely equivalent solutions modulo $=_{B}$ but not up to e.g. $=_{rBB}$. This breaks the equivalence lattice -- we hence need a stronger concept of \underline{unguardedness} for $=_{B}$.
|
|
|
|
\begin{definition}[strong unguardedness]
|
|
A \textbf{strongly unguarded} recursive specification is one where, for
|
|
\begin{equation*}
|
|
X = \mathsf{Expr}(X, \dots)
|
|
\end{equation*}
|
|
the recursive variable $X$ occurs NOT in a subterm of the form:
|
|
\begin{equation*}
|
|
a \leftarrow A \cup \{\tau\}: a.P^{'}, X \in P^{'}
|
|
\end{equation*}
|
|
as in, $X$ is not guarded by $\forall a \in A$ nor $\tau$.
|
|
|
|
It turns out that \textbf{RSP is sound modulo bisimulation for all non-strongly-unguarded recursive specifications}.
|
|
\end{definition}
|
|
|
|
\begin{definition}[weak unguardedness]
|
|
Likewise, a \textbf{weakly unguarded} recursive specification is one where recursive variable $X$ is NOT guarded by $\forall a \in A$ only.
|
|
|
|
Note that strong unguardedness entails weak unguardedness.
|
|
|
|
\textbf{RSP is sound modulo weak/branching bisimulation for all non-weakly-unguarded recursive specifications}.
|
|
\end{definition}
|
|
|
|
\end{document} |