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:

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

mentre

$$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

$$\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:

$$\{ (p+r, q+r) \: : \: p,q,r \: \in \: \mathcal{P}$$    e $$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.