Assiomatizzazione della bisimulazione

Definizione 6..5   Un processo è finito se contiene solo Somma finita e nessuna ricorsione.

E' chiaro che attraverso l'expansion law, ogni processo finito può essere uguagliato ad uno che non contiene Composizione parallela, Restrizioni o Relabelling.

Definizione 6..6   L'equazione E di un processo è seriale se non contiene Composizione parallela, Restrizioni o Relabelling, e le equazioni che definiscono ogni Costante in E non contengono Composizione parallela, Restrizioni o Relabelling.

Dunque, attraverso l'expansion law ogni processo può essere uguagliato ad un processo seriale.

Definiamo ora due insiemi di assiomi, uno per Somme ed uno per Sequenzalizzazione:

$$\begin{array}{rcl} & & Assiomi \: \mathcal{A}_1 \\ {\bf... ...f A3}& & p+p = p \\ {\bf A4} & & p+nil = p \\ \end{array}$$

$$\begin{array}{rcl} & & Assiomi \: \mathcal{A}_2 \\ \mat... ... \alpha.(p+\tau.q)+\alpha.q = \alpha(p + \tau.q) \end{array}$$

Sappiamo già che la seguente è conseguenza di $\mathcal{A}_2$:

$$\begin{array}{rcl} {\bf A6'} & & p +\tau.(p+q) = \tau.(p+q) \end{array}$$

Con l'aiuto dell'expansion law ogni equazione valida tra processi finiti segue da $\mathcal{A}_2$: questo significa che abbiamo una completa assiomatizzazione per i processi finiti, e questo significa che possiamo mostrare che $\mathcal{A}_2$ sono corretti e completi per processi finiti seriali.

In quello che segue useremo $p =q$ per indicare che $p$ e $q$ sono uguali per la definizione 6.4 di uguaglianza, mentre $\mathcal{A} \vdash p=q$ intendiamo dire che l'uguaglianza può essere provata da un ragionamento equazionale dagli assiomi $\mathcal{A}$; useremo $\equiv$ per l'identità sintattica.

Consideriamo la potenza dell'insieme $\mathcal{A}_1$:

Definizione 6..7 (Standard form)   $p$ è in standard form (abbreviato in s.f.) se

$$p \equiv \sum_{i=1}^{m} \alpha_i.p_i$$

dove ogni $p_i$ è anch'esso in standard form.

Si vede che nil è in s.f.: è il caso limite $m=0$. Inoltre, si noti come l'ordine degli addendi possa essere ignorato grazie agli assiomi ${\bf A1}$ ed ${\bf A2}$.

Lemma 6..3   Per ogni processo $p$, esiste un processo $p'$ in s.f. tale che

$$\mathcal{A}_1 \vdash p=p'$$

Dimostrazione. Con l'uso degli assiomi $\mathcal{A}_1$, il termine nil può essere eliminato da ogni Somma, ed il risultato è in s.f. $\qedsymbol$

Il risultato seguente è molto importante e mostra come $\mathcal{A}_1$ sia corretto e completo rispetto alla nozione di strong congruence.

Proposizione 6..24 (Correttezza e completezza)   $p\:\sim\: q$ sse $\mathcal{A}_1 \vdash p=q$

Dimostrazione. ( $\Leftarrow$) Correttezza. Quello che bisogna osservare è che tutti gli assiomi $\mathcal{A}_1$ sono ancora veri se sostituiamo a '=' '$\sim$'; questo risultato è già stato provato nella parte della congruenza forte (proposizione 6.7).

( $\Rightarrow$) Completezza. Assumiamo $p\:\sim\: q$ ed inoltre che $p$ e $q$ siano entrambi in standard form, cioè della forma $p \equiv \sum_{i=1}^m \alpha_i.p_i$ e $q \equiv \sum_{j=1}^n \alpha_j.q_j$. Proveremo la proposizione per induzione sull'altezza massima di $p$ e $q$, dove l'altezza di $p$ è definita come il massimo numero di Sequenzalizzazioni innestate in $p$.

Se la massima profondità è pari a zero, allora entrambi i processi sono nil (in quanto entrambi in standard form) ed il ragionamento equazionale ci garantisce che che $\mathcal{A}_1 \vdash nil=nil$ (la riflessività è parte del ragionamento equazionale).

In caso contrario, sia $\alpha.p'$ un sommando di $p$. Allora $p \stackrel{\alpha}{\longrightarrow} p'$, e dal fatto che $p\:\sim\: q$, esiste un certo $q'$ tale che $q \stackrel{\alpha}{\longrightarrow} q'\: \sim \: p'$. Poichè $q$ è in standard form, allora $\alpha.q'$ è un sommando di $q$ e per induzione $\mathcal{A}_1 \vdash p'=q'$ e quindi il sommando $\alpha.p'$ di $p$ può essere provato uguale ad un sommando di $q$. Similmente, ogni sommando $\beta.q'$ di $q$ può essere provato uguale ad un sommando di $p$. Segue dunque che $\mathcal{A}_1 \vdash p=q$, usando l'assioma ${\bf A3}$ per eliminare i sommandi duplicati (e gli assiomi ${\bf A1}$ ed ${\bf A2}$ per riordinare e raggruppare i sommandi, ove necessario).

$\qedsymbol$

Definizione 6..8 (Full standard form)   $p$ è in full standard form (f.s.f.) se

1. $p\equiv \sum_{i=1}^{m} \alpha_i.p_i$, dove ogni $p_i$ è anch'esso in full standard form;
   
2. per ogni $p \stackrel{\alpha}{\Longrightarrow}p'$, allora $p \stackrel{\alpha}{\longrightarrow} p'$

Possiamo pensare alla f.s.f. come 'saturata' nel seguente senso: per ogni $p \stackrel{\alpha}{\Longrightarrow}p'$ allora $\alpha.p'$ appare come un sommando di $p$. Vedremo ora come ogni s.f. può essere saturata utilizzando $\mathcal{A}_2$

Lemma 6..4 (Saturazione)   Se $p \stackrel{\alpha}{\Longrightarrow}p'$, allora $\mathcal{A}_2 \vdash p=p + \alpha.p'$.

Dimostrazione. Svolgiamo la prova per induzione sulla struttura di $p$. Consideriamo tre casi per $p \stackrel{\alpha}{\Longrightarrow}p'$:

Caso 1

$\alpha.p'$ è un sommando di $p$. La conclusione vale grazie all'assioma ${\bf A3}$.

Caso 2

$\alpha.q$ è un sommando di $p$ e $q \stackrel{\tau}{\Longrightarrow}p'$. Allora per induzione $\mathcal{A}_2 \vdash q=q + \tau.p'$, quindi

$$\begin{array}{rcl} \mathcal{A}_2 \vdash p & = & p + \alpha.q \qu... ...& = & p+\alpha.p' \quad \mbox{dai passi precedenti al contrario} \end{array}$$

Caso 3

$\tau.q$ è un sommando di $p$ e $q \stackrel{\alpha}{\Longrightarrow}p'$. Allora per induzione $\mathcal{A}_2 \vdash q=q + \alpha.p'$, quindi

$$\begin{array}{rcl} \mathcal{A}_2 \vdash p & = & p + \tau.q \quad... ...& = & p+\alpha.p' \quad \mbox{dai passi precedenti al contrario} \end{array}$$

e questo completa la prova.

$\qedsymbol$

Con l'aiuto di questo lemma, possiamo trasformare ogni s.f. in una f.s.f. equivalente:

Lemma 6..5   Per ogni processo $p$ in s.f. esiste un processo $p'$ in f.s.f. di uguale profondità, tale che $\mathcal{A}_2 \vdash p=p'$

Dimostrazione. Per induzione sulla struttura di $p$. Per il caso base, $p \equiv nil$ e $p$ è già in f.s.f.. In caso contrario, per ogni sommando $\beta.q$ di $p$ possiamo assumere per induzione che $q$ sia già convertito, grazie ad $\mathcal{A}_2$, in f.s.f. senza incremento di profondità. Consideriamo dunque tutte le coppie $(\alpha_i, p_i), \: 1 \leq i \leq k$, tale che $p \stackrel{\alpha_i}{\Longrightarrow} p_i$ ma non $p \stackrel{\alpha_i}{\longrightarrow} p_i$. Ogni $p_i$ deve essere un f.s.f. in quanto deve essere una sottoespressione di qualche sommando $\beta.q$ di $p$. Dunque

$$p' \equiv p+ \alpha_1.p_1 + \dots + \alpha_k.p_k$$

è in f.s.f. di uguale profondità di $p$, e grazie al lemma di saturazione, $\mathcal{A}_2 \vdash p=p'$.

$\qedsymbol$

Siamo adesso in grado di dimostrare un risultato importante di questa sezione, cioè che $\mathcal{A}_2$ è corretto e completo per la nozione di uguaglianza su processi finiti seriali:

Proposizione 6..25 (correttezza e completezza)   $p =q$ sse $\mathcal{A}_2 \vdash p=q$

Dimostrazione. ( $\Leftarrow$) Correttezza. Si deve solamente osservare che gli assiomi $\mathcal{A}_2$ sono tutti veri, quando intendiamo '=' come l'ugualianza come definita in definizione 6.4.

( $\Rightarrow$) Completezza. Possiamo assumere che $p$ e $q$ siano in f.s.f.; la prova procederà per induzione sulla somma delle profondità di $p$ e $q$.

Quando la somma è pari a zero, allora si ha $p \equiv nil \equiv q$, ed il risultato è banale. In caso contrario assumiamo $p =q$, e sia $\alpha.p'$ un sommando di $p$. Miriamo a provare che $q$ ha un sommando provabilmente uguale ad $\alpha.p'$. Ora $p \stackrel{\alpha}{\longrightarrow} p'$, quindi esiste un $q'$ tale che $q \stackrel{\alpha}{\Longrightarrow} q'$ e $p' \: \approx \: q'$. Di più, $q \stackrel{\alpha}{\longrightarrow} q'$ in quanto $q$ è in f.s.f., e quindi $\alpha.q'$ è un sommando di $q$.

Non possiamo applicare immediatamente l'induzione, in quanto sappiamo soltanto che $p' \: \approx \: q'$ e non $p'=q'$. Ma dall'Hennessey theorem (proposizione 6.23) sappiamo che allora $p'=q'$ o $p' = \tau.q'$ o $\tau.p' = q'$.

Nel primo caso, dal momento che $p'$ e $q'$ sono in f.s.f. e di profondità minore di $p$ e $q$, per induzione $\mathcal{A}_2 \vdash p'=q'$, quindi $\mathcal{A}_2 \vdash \alpha.p'=\alpha.q'$. Nel secondo caso dobbiamo dapprima convertire $\tau.q'$ in f.s.f. prima di poter applicare l'induzione. Dal lemma precedente esiste un $q''$ in f.s.f. di uguale profondità di $\tau.q'$, tale che $\mathcal{A}_2 \vdash \tau.q'=q''$; ma la somma delle profondità di $p'$ e $q''$ e minore di uno della somma delle profondità di $p$ e $q$, e quindi per induzione possiamo inferire che $\mathcal{A}_2 \vdash p'=q''$ e quindi $\mathcal{A}_2 \vdash p'=\tau.q'$ e grazie all'assioma $A5$ si ha che $\mathcal{A}_2 \vdash \alpha.p'=\alpha.q'$. Il terzo caso è simile a questo.

Dunque, in ognuno dei tre casi, abbiamo mostrato che da $\mathcal{A}_2$ ogni sommando di $\alpha.p'$ di $p$ può essere provato uguale ad un sommando di $q$. In modo simile, ogni sommando $\beta.q'$ di $q$ può essere provato uguale ad un sommando di $p$. In fine, utilizzando l'assioma $A3$ per eliminare gli eventuali sommandi duplicati, possiamo concludere che $\mathcal{A}_2 \vdash p=q$

$\qedsymbol$