Congruenza forte

Ora vogliamo mostrare che la bisimualzione forte è una congruenza

Dimostriamo dunque che la bisimulazione forte è sostituitiva per tutti i combinatori:

Proposizione 6..7   Sia $ p_1 \: \sim \: p_2$. Allora
  1. $ \alpha.p_1 \: \sim \: \alpha.p_2$

  2. $ p_1+q \: \sim \: p_2 +q$

  3. $ p_1\vert q \: \sim \: p_2\vert q$

  4. $ p_1 \setminus L \: \sim \: p_2 \setminus L$

  5. $ p_1[f] \: \sim \: p_2[f]$

Dimostrazione. Per 1., possiamo facilmente dedurre le condizioni 1. e 2. della proposizione 6.3 sostituendo $ \alpha.p$ e $ \alpha.q$ al posto di $ p$ e $ q$.

La prova per 2. è simile.

Per 3., invece, si deve mostrare che $ \mathcal{S}$ è una bisimulazione, dove

$\displaystyle \mathcal{S} = \{ (p_1\vert q, p_2\vert q) \: : \: p_1 \: \sim \: p_2 \} $

Supponiamo allora che $ (p_1\vert q, p_2\vert q) \: \in \: \mathcal{S}$. Sia $ p_1 \vert q \stackrel{\alpha}{\longrightarrow} r$. Ci sono tre casi possibili:

Caso 1
$ p_1 \stackrel{\alpha}{\longrightarrow} p_1'$ e $ r
\equiv p_1'\vert q$
Allora, dal momento che $ p_1 \: \sim \: p_2$, abbiamo che $ p_2 \stackrel{\alpha}{\longrightarrow} p_2'$ con $ p_1' \: \sim \:
p_2'$; da questo si ha $ p_2\vert q \stackrel{\alpha}{\longrightarrow}
p_2'\vert q$ e $ (p_1'\vert q, p_2'\vert q) \: \in \: \mathcal{S}$.

Caso 2
$ q \stackrel{\alpha}{\longrightarrow} q'$ e $ r
\equiv p_1\vert q'$
Allora anche $ p_2\vert q \stackrel{\alpha}{\longrightarrow} p_2\vert q'$ e $ (p_1\vert q', p_2\vert q') \: \in \: \mathcal{S}$.

Caso 3
$ \alpha = \tau, p_1 \stackrel{l}{\longrightarrow}
p_1' \: \wedge \: q \stackrel{\overline{l}}{\longrightarrow} q'$ e $ r \equiv p_1'\vert q_1$
Allora, dal momento che $ p_1 \: \sim \: p_2$, abbiamo che $ p_2
\stackrel{l}{\longrightarrow} p_2'$ con $ p_1' \: \sim \:
p_2'$; da questo si ha $ p_2\vert q \stackrel{\tau}{\longrightarrow} p_2'\vert q'$ e $ (p_1'\vert q', p_2'\vert q') \: \in \: \mathcal{S}$.
Con un argomento simmetrico, si completa la prova che $ \mathcal{S}$ è una bisimulazione forte.

Le prove per 4. e 5. sono simili.

$ \qedsymbol$

Morpheus 2004-02-10