RICORSIONE

Introducendo l'equazione di definizione ( $\stackrel{{def}}{{=}}$) abbiamo detto che in $N \stackrel{{def}}{{=}}E$ il nome di processo $N$ può essere utilizzato anche nell'espressione E. Se questo avviene, siamo di fronte alla ricorsione, perché $N$ richiama se stesso durante la sua esecuzione.

La ricorsione è facilmente osservabile in $\:\: C \stackrel{{def}}{{=}} in.\:\overline{out}.\:C \:$ dove il processo C esegue un'azione di input sulla porta $in$ seguita da un'azione di output sulla porta $out$. A questo punto il processo torna a comportarsi come descritto nella definizione di C, perciò il risultato finale è una sequenza alternata e infinita di $in$ e $\overline{out}$. Dato il termine recX.E

$$\renewcommand {\arraystretch}{1.2} \begin{array}{c}E[recX.E/X] \... ... E'\\ \hline recX.E \: \stackrel{\mu}{\longrightarrow} \: E' \end{array}$$

con $\mu \in Act_\tau$ Ecco un semplice esempio per dell'utilizzo di questo operatore:

$$recX.a.X + \:b.nil \stackrel{a}{\longrightarrow} recX.a.X + \: b.nil$$