Congruenza debole

Ciò che si vuole individuare è la più grande relazione di congruenza che includa $ \approx$. Per fare questo, inizieremo definendo in modo differente la nozione di bisimulazione e proveremo che la bisimulazione è preservata per tutti i combinatori ad eccezione della Somma. Daremo infine la definizione di uguaglianza '=' e vedremo che questa è effettivamente una relazione di congruenza, che giustifica tutte le normali manipolazioni algebriche (la sostituzione di uguali per uguali). Mostreremo come le $ \tau$ laws valgano ed infine mostreremo un insieme di assiomi che sono completi (dai quali tutte le equazioni valide possono essere derivate) per i processi finiti ed a stati finiti.

Abbiamo visto in precedenza il concetto di bisimulazione, ed in particolare la più larga relazione di bisimulazione $ \approx$, che abbiamo chiamato equivalenza osservazionale o bisimiliarità. Iniziamo ora a dare una caratterizzazione alternativa di bisimulazione in termini di esperimenti. Consideriamo $ p
\stackrel{s}{\Longrightarrow}p'$, dove $ s \: \in \:
\mathcal{L}^*$, un esperimento su $ p$: consiste nell'eseguire $ p$ per un po' ed osservare la sequenza $ s = l_1 \dots l_n$.Se $ s=\varepsilon$, scriveremo $ p\Rightarrow p'$ (se, cioè, $ p$ non è stabile, ciò può essere dovuto ad una o più azioni $ \tau$). $ p\Rightarrow p'$ è comunque un esperimento, dal momento che $ p'$ ammette meno esperimenti di $ p$: ad esempio, $ p \equiv
a.nil+\tau.nil$ ammette l'esperimento $ a$, ma possiamo fare $ p\Rightarrow nil$ e quest'ultimo non ammette un esperimento $ a$.

Proposizione 6..14   $ \mathcal{S}$ è una bisimulazione sse, $ \forall (p,q)\: \in \:
\mathcal{S}$ e $ s \: \in \:
\mathcal{L}^*$:

  1. $ \forall p': \: p \stackrel{s}{\Longrightarrow} p' \quad
\exists q' : \: q \stackrel{s}{\Longrightarrow} q' \quad \wedge
\quad p' \: \mathcal{S} \: q'$;

  2. $ \forall q': \: q \stackrel{s}{\Longrightarrow} q' \quad
\exists p' : \: p \stackrel{s}{\Longrightarrow} p' \quad \wedge
\quad p' \: \mathcal{S} \: q'$.

Dimostrazione. ( $ \Rightarrow$) Assumiamo che $ \mathcal{S}$ sia una bisimulazione. Sia $ p
\stackrel{s}{\Longrightarrow}p'$, così che $ p
\stackrel{t}{\longrightarrow} p'$ dove $ t=(\alpha_1\dots\alpha_n)
\: \in \: Act_{tau}^*$ e $ \hat{t}=s$. Allora $ p
\stackrel{\alpha_1}{\longrightarrow} p_1
\stackrel{\alpha_2}{\longrightarrow} \cdots
\stackrel{\alpha_n}{\longrightarrow} p' $ e dal momento che $ \mathcal{S}$ è una bisimulazione abbiamo anche che $ q
\stackrel{\hat{\alpha}_1}{\Longrightarrow} q_1
\stackrel{\hat{\alpha}_2}{\Longrightarrow} \cdots
\stackrel{\hat{\alpha}_n}{\Longrightarrow} q' $ con $ p' \:
\mathcal{S} \: q'$. Da questo $ q
\stackrel{\hat{t}}{\Longrightarrow} q'$, e quindi $ q
\stackrel{s}{\Longrightarrow} q'$.

( $ \Leftarrow$) Assumendo 1., sia $ p \stackrel{\alpha}{\longrightarrow} p'$. Se $ \alpha = \tau$ allora $ p \stackrel{\varepsilon}{\Longrightarrow} p'$ e così da 1. si ha $ q \stackrel{\varepsilon}{\Longrightarrow} q'$ con $ p' \mathcal{S}
q'$; ma $ \hat{\alpha}=\varepsilon$, quindi $ q \stackrel{\hat{\alpha}}{\Longrightarrow} q'$ come richiesto. Se $ \alpha=l$ allora $ p \stackrel{l}{\Longrightarrow} p'$, e grazie a 1. $ q \stackrel{l}{\Longrightarrow} q'$ con $ p' \mathcal{S}
q'$; ma $ \hat{l}=l$ e quindi $ q
\stackrel{\hat{l}}{\Longrightarrow} q'$ come richiesto. Assumendo 2., similmente si deriva la seconda condizione per la bisimulazione.

$ \qedsymbol$

Il motivo per includere l'esperimento vuoto $ p\Rightarrow p'$ nella proposizione di sopra è che, senza di esso, avremmo che $ a.nil+\tau.nil \: \approx \: a.nil$ certamente falso nella nostra definizione originaria.

Guardiamo ora alla sostitutività di $ \approx$. Abbiamo già accennato al fatto che, in generale, $ \approx$ non è preservata da Somma:

$\displaystyle b.nil \approx \tau.b.nil$

mentre

$\displaystyle a.nil+b.nil \not\approx a.nil+\tau.b.nil$

D'altro canto, abbiamo che Prefix rafforza la bisimilarità verso l'uguaglianza; per ora ci limitiamo a dimostarare che:

Proposizione 6..15   La bisimilarità è preservata da Composizione parallela, Restrizione e Relabelling: se $ p\:\approx\: q$ allora $ p\vert r \:
\approx \: q\vert r$, $ p\setminus L \: \approx \: q\setminus L$ e $ p[S]
\: \approx \: q[S]$.

Dimostrazione. Proveremo solo il risultato per la Composizione parallela, il metodo per gli altri due è semplice e segue la stessa strada. Ci è sufficiente mostrare che

$\displaystyle \mathcal{S} = \{(p\vert r,q\vert r) \: : \: p, q, r \in \mathcal{P} \:
\wedge \: p \: \approx \: q\} $

è una bisimulazione. Sia allora $ p\vert r
\stackrel{\alpha}{\longrightarrow} p'\vert r'$ (dal momento che tutte le derivazioni devono avere questa forma).

Caso 1:
$ \: p \stackrel{\alpha}{\longrightarrow} p' \:
\wedge r
\equiv r'$
Allora $ q \stackrel{\hat{\alpha}}{\Longrightarrow} q'$ per qualche $ q'$ con $ p' \: \approx \: q'$, quindi $ q\vert r
\stackrel{\hat{\alpha}}{\Longrightarrow} q'\vert r$ e dunque $ (p\vert r,q\vert r)
\: \in \: \mathcal{S}$ come richiesto.

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

Caso 3:
$ \: \alpha=\tau, \: p \stackrel{l}{\longrightarrow}
p'
\: \wedge r \stackrel{\overline{l}}{\longrightarrow} r'$
Allora $ q \stackrel{l}{\Longrightarrow} q'$ per qualche $ q'$ con $ p' \: \approx \: q'$, quindi $ q\vert r
\stackrel{\tau}{\Longrightarrow} q'\vert r'$ e dunque $ (p'\vert r',q'\vert r') \:
\in \: \mathcal{S}$ come richiesto.

Da questo, tramite un argomento simmetrico, si ottiene che $ \mathcal{S}$ è una bisimulazione. $ \qedsymbol$

Quanto detto vale poichè l'azione invisibile $ \tau$ non può mai essere ristretta o rinominata.

Come appena mostrato, la bisimulazione non è completamente sostitutiva ( $ p\:\approx\: q$ non implica $ p+r \: \approx \:
q+r$), mentre noi cerchiamo una nozione di uguaglianza, $ p =q$, che implichi $ p\:\approx\: q$ e che sia completamente sostitutiva: cerchiamo una relazione di congruenza, che sia la più larga relazione a contenere $ \approx$.

Definizione 6..4   $ p$ e $ q$ sono uguali o (osservazionalmente) congruenti, $ p =q$, se $ \forall \alpha$

  1. $ \forall p': \: p \stackrel{\alpha}{\longrightarrow} p'
\quad \exists q' : \: q \stackrel{\alpha}{\Longrightarrow} q'
\quad \wedge \quad p' \: \approx \: q'$;

  2. $ \forall q': \: q \stackrel{\alpha}{\longrightarrow} q'
\quad \exists p' : \: p \stackrel{\alpha}{\Longrightarrow} p'
\quad \wedge \quad p' \: \approx \: q'$.

Si noti la somiglianza con la definizione di bisimulazione: infatti, differiscono soltanto in un aspetto, e cioè qui abbiamo $ \stackrel{\alpha}{\Rightarrow}$ al posto di $ \stackrel{\hat{\alpha}}{\Rightarrow}$. Questo implica che ogni azione di $ p$ o $ q$ deve essere corrisposta da almeno una azione dell'altro processo. Si noti inoltre come questo si applichi solo all'azione iniziale, in quanto poi si richiede che $ p' \: \approx \: q'$ e non $ p'=q'$.

Guardiamo un risultato interessante, che ci mostra come le nozioni di uguaglianza e bisimilarità siano molto vicine (l'ipotesi che faremo è che si possa sempre costruire un nuovo nome indipendentemente da quanti se ne sono usati finora indicando con $ \mathcal{L}(p)$ il linguaggio generato da $ p$ e con $ \mathcal{L}$ il linguaggio di tutta la nostra algebra)

Proposizione 6..16   Assumiamo che $ \mathcal{L}(p) \cup \mathcal{L}(q) \subset
\mathcal{L}$. Allora $ p =q$ sse, per ogni $ r$, $ p+r \: \approx \:
q+r$.

Dimostrazione. ( $ \Rightarrow$) E' facile vedere che la seguente è una bisimulazione:

$\displaystyle \{ (p+r, q+r) \: : \: p,q,r \: \in \: \mathcal{P}$    e $\displaystyle p
= q \} \: \cup \: \approx$

( $ \Leftarrow$) Proviamo il contropositivo. Supponiamo dunque che $ p \not = q$. Allora, per esempio, avremo che ci sono $ \alpha$ e $ p'$ tali che $ p \stackrel{\alpha}{\longrightarrow} p'$ ma che per qualsiasi $ q \stackrel{\alpha}{\Longrightarrow} q'$ si ha $ p' \not
\approx q'$. Scegliamo ora $ r \equiv l.nil$, dove $ l$ non è nel linguaggio di $ p$ o di $ q$. Chiaramente $ p+r
\stackrel{\alpha}{\longrightarrow} p'$; si deve allora mostrare che qualsiasi $ q +r \stackrel{\hat{\alpha}}{\Longrightarrow} q'$ si ha $ p' \not
\approx q'$. Se $ \alpha = \tau$ e $ q \equiv q+r$, allora $ p' \not
\approx q'$ in quanto $ q'$ ha un'azione $ l$ che $ p$ non ha; d'altra parte $ q +r \stackrel{\alpha}{\Longrightarrow}
q'$ e quindi $ q \stackrel{\alpha}{\Longrightarrow} q'$ (in quanto $ r \stackrel{\alpha}{\Longrightarrow} q'$ è impossibile dal momento che $ \alpha \not = l$), e quindi ancora $ p' \not
\approx q'$.

$ \qedsymbol$

Vediamo ora come l'uguaglianza si trovi nel mezzo tra congruenza forte e bisimilarità:

Proposizione 6..17   $ p\:\sim\: q$ implica $ p =q$, e $ p =q$ implica $ p\:\approx\: q$.

Dimostrazione. Come prima cosa notiamo come $ p\:\sim\: q$ implica $ p\:\approx\: q$: discende direttamente dal fatto che ogni bisimulazione forte è anche una bisimulazione, facilmente verificabile dalle definizioni. Ora, per vedere che $ p\:\sim\: q$ implica $ p =q$, si usa la proprietà ($ *_{\sim}$) della bisimulazione forte unita con la definizione di uguaglianza data poco sopra.

Per quanto riguarda la seconda parte, dalla proprosizione sopra abbiamo che $ p =q$ implica $ p+nil \: \approx \: q+nil$, ma $ p+nil \: \sim \: p$ e quindi $ p+nil \: \approx \: p$, da cui segue $ p\:\approx\: q$. $ \qedsymbol$

Quindi, tutte le leggi valide per $ \sim$ e = lo sono anche per la bisimilarità, mentre non vale il viceversa: abbiamo che $ p \: \approx \: \tau.p$ mentre in generale abbiamo $ p \not = \tau.p$.

Facciamo il primo passo per dimostrare che l'uguaglianza è una congruenza mostrando che:

Proposizione 6..18   L'uguaglianza è una relazione di equivalenza.

Dimostrazione. Il modo più semplice per provare questo risultato è sfruttare la proposizione 6.16 assieme al fatto che $ \approx$ è un'equivalenza. $ \qedsymbol$

Vediamo come, attraverso la Sequenzalizzazione, si rafforzi la bisimilarità verso la uguaglianza, già osservato nella sezione precedente:

Proposizione 6..19   Se $ p\:\sim\: q$ allora $ \alpha.p = \alpha.q$.

Dimostrazione. Discende direttamente dalla definizione di uguaglianza. $ \qedsymbol$

Si deve ora provare che tutti gli operatori preservano l'ugaglianza:

Proposizione 6..20   se $ p =q$ allora $ \alpha.p = \alpha.q$, $ p+r=q+r$, $ p\vert r = q\vert r$, $ p\setminus L = q\setminus L$ e $ p[f] = q[f]$.

Dimostrazione. La prima, discende direttamente dalla proposizione precedente. Per la seconda, si richiede che $ (p+r)+r' \: \approx \: (q+r)+r'$, per ogni $ r'$; sappiamo però che $ p+(r+r') \: \approx \: q+(r+r')$, dato che $ p =q$ e che l'associatività, in quanto vale per $ \sim$, vale anche per $ \approx$.

Le rimanenti prove sono applicazioni dirette della definizione di uguaglianza. Per la Composizione parallela, un'analisi a casi come nella proposizione 6.15 è necessaria; le altre due sono più dirette. $ \qedsymbol$

Raccogliendo tutti i risultati ottenuti si arriva a poter affermare che l'uguaglianza è una congruenza.

Avevamo lasciato in sospeso alcune proprietà, che ora riprendiamo dimostrando:

Proposizione 6..21   Le $ \tau$ laws:
  1. $ \alpha.\tau.p=\alpha.p$

  2. $ P+\tau.p=\tau.p$

  3. $ \alpha.(p+\tau.q)+\alpha.q=\alpha.(p+\tau.q)$

Dimostrazione. In modo diretto dalla definizione di uguaglianza. Soltanto nel punto 1. si è usato il risultato che $ p \: \approx \: \tau.p$. $ \qedsymbol$

Mostriamo anche che

Proposizione 6..22   Se $ p\:\approx\: q$ e sono entrambi stabili, allora $ p =q$.

Dimostrazione. Sia $ p \stackrel{\alpha}{\longrightarrow} p'$, il che implica che $ \alpha \not= \tau$ (per la stabilità); allora $ q \stackrel{\hat{\alpha}}{\Longrightarrow} q'$ con $ p' \: \approx \: q'$. Ma allora $ q \stackrel{\alpha}{\Longrightarrow} q'$ in quanto $ \stackrel{\hat{\alpha}}{\Longrightarrow}$ e $ \stackrel{\alpha}{\Longrightarrow}$ si equivalgono se $ \alpha \not= \tau$, e quindi $ p =q$ segue dalla definizione. $ \qedsymbol$

Proviamo infine un risultato tanto inatteso quanto importante e che mostra ancora una volta come la nozione di bisimilarità e di uguaglianza siano vicine; questo risultato venne per la prima volta provato da Matthew Hennessey e verrà poi sfruttato in seguito per provare la completezza dell'insieme di assiomi che introdurremo:

Proposizione 6..23 (Hennessey)   $ p\:\approx\: q$ sse $ p =q$ o $ \tau.p=q$ o $ p=\tau.q$

Dimostrazione. ( $ \Leftarrow$) Sappiamo che $ p =q$ implica $ p\:\approx\: q$; le altre implicazioni seguono da $ p \: \approx \: \tau.p$.

( $ \Rightarrow$) Assumiamo $ p\:\approx\: q$, e consideriamo i tre casi possibili. Primo, supponiamo che $ p
\stackrel{\tau}{\longrightarrow} p' \: \approx \: q$ per qualche $ p'$; è facile vedere allora come $ p=\tau.q$. Secondo, supponiamo che $ q \stackrel{\tau}{\longrightarrow} q' \: \approx
\: p$ per qualche $ q'$; in modo simile si mostra che $ \tau.p=q$. Se nessuna delle due condizioni si è verificata, allora si può mostrare che $ p =q$ nel modo seguente: consideriamo dapprima che $ p
\stackrel{l}{\longrightarrow} p'$; dal momento che $ p\:\approx\: q$ abbiamo che $ q \stackrel{\hat{l}}{\Longrightarrow} q' \:
\approx \: p'$, e cioè $ q \stackrel{l}{\Longrightarrow} q' \:
\approx \: p'$ come richiesto. Nell'altro caso, e cioè se $ p
\stackrel{\tau}{\longrightarrow} p'$ allora $ q \Longrightarrow q'
\: \approx \: p'$, e $ q'$ non può essere $ q$ stesso per ipotesi e quindi $ q \stackrel{\tau}{\Longrightarrow} q' \: \approx \: p'$ come richiesto. Grazie alla simmetria segue che $ p =q$. $ \qedsymbol$

Quanti abbiamo fatto in questa sezione è stato trovare una nozione di uguaglianza completamente sostitutiva e molto vicina alla bisimilarità; a questo punto potremmo obiettare che la bisimilarità è quasi ridondante. Invece, le dimostrazioni che stabiliscono una bisimilarità sono molto convenienti, ed inoltre, stabilire una bisimilarità è molto naturale ed a volte anche meccanizzabile.

Morpheus 2004-02-10