π -calcolo - π-calculus

In informatica teorica , il π -calcolo (o pi-calcolo ) è un calcolo di processi . Il π -calcolo permette di comunicare i nomi dei canali lungo i canali stessi, e in questo modo è in grado di descrivere calcoli simultanei la cui configurazione di rete può cambiare durante il calcolo.

Il π -calculus ha pochi termini ed è un linguaggio piccolo, ma espressivo (vedi § Sintassi ). Programmi funzionali possono essere codificati in π -calcolo, e la codifica sottolinea la natura dialogo di calcolo, disegno connessioni con semantica dei giochi . Estensioni del π -calcolo, come ad esempio il calcolo spi e applicata π , sono riusciti a ragionare su protocolli crittografici . Oltre all'uso originale nella descrizione di sistemi concorrenti, il π- calcolo è stato utilizzato anche per ragionare sui processi aziendali e sulla biologia molecolare .

Definizione informale

Il π -calculus appartiene alla famiglia dei process calculi , formalismi matematici per descrivere e analizzare proprietà di computazione concorrente. Infatti, il π -calculus, come il λ-calculus , è così minimale che non contiene primitive come numeri, booleani, strutture dati, variabili, funzioni o anche le solite istruzioni di flusso di controllo (come if-then-else, while).

Costrutti di processo

Al centro del π -calcolo è la nozione di nome . La semplicità del calcolo risiede nel duplice ruolo che i nomi giocano come canali e variabili di comunicazione .

I costrutti di processo disponibili nel calcolo sono i seguenti (una definizione precisa è data nella sezione seguente):

• concorrenza , scritto , dove e sono due processi o thread eseguiti contemporaneamente.${\displaystyle P\mid Q}$${\displaystyle P}$${\displaystyle Q}$
• comunicazione , dove
  • il prefisso di input è un processo in attesa di un messaggio che è stato inviato su un canale di comunicazione denominato prima di procedere come , legando il nome ricevuto al nome x . Tipicamente, questo modella o un processo che aspetta una comunicazione dalla rete o un'etichetta utilizzabile una sola volta da un'operazione.${\displaystyle c\sinistra(x\destra).P}$${\displaystyle c}$${\displaystyle P}$cgoto c
  • il prefisso di uscita descrive che il nome viene emesso sul canale prima di procedere come . In genere, questo modello invia un messaggio sulla rete o un'operazione.${\displaystyle {\overline {c}}\langle y\rangle .P}$${\displaystyle y}$${\displaystyle c}$${\displaystyle P}$goto c
• replica , scritta , che può essere vista come un processo che può sempre creare una nuova copia di . In genere, questo modella un servizio di rete o un'etichetta in attesa di un numero qualsiasi di operazioni.${\displaystyle !\,P}$${\displaystyle P}$cgoto c
• creazione di un nuovo nome , scritto , che può essere visto come un processo di allocazione di una nuova costante x all'interno . Le costanti di π -calculus sono definite solo dai loro nomi e sono sempre canali di comunicazione. La creazione di un nuovo nome in un processo è anche chiamata restrizione .${\displaystyle \left(\nu x\right)P}$${\displaystyle P}$
• il processo nullo, scritto , è un processo la cui esecuzione è completa e si è interrotta.${\displaystyle 0}$

Sebbene il minimalismo del π -calculus ci impedisca di scrivere programmi in senso normale, è facile estendere il calcolo. In particolare, è facile definire sia strutture di controllo come ricorsione, cicli e composizione sequenziale che tipi di dati come funzioni del primo ordine, valori di verità , liste e interi. Inoltre, sono state proposte estensioni del π- calcolo che tengono conto della distribuzione o della crittografia a chiave pubblica. Il π -calcolo applicato dovuto ad Abadi e Fournet [1] pone queste varie estensioni su una base formale estendendo il π -calcolo con tipi di dati arbitrari.

Un piccolo esempio

Di seguito è riportato un piccolo esempio di un processo che consiste di tre componenti paralleli. Il nome del canale x è conosciuto solo dai primi due componenti.

${\displaystyle {\begin{allineato}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\ ;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\ langle v\rangle .0\end{allineato}}}$

I primi due componenti sono in grado di comunicare sul canale x , e il nome y diventa legato a z . Il prossimo passo nel processo è quindi

${\displaystyle {\begin{allineato}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\ ;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{allineato}}}$

Si noti che la y rimanente non è interessata perché è definita in un ambito interno. Il secondo e il terzo componente parallelo possono ora comunicare sul nome del canale z e il nome v diventa associato a x . Il prossimo passo nel processo è ora

${\displaystyle {\begin{allineato}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x }}\langle x\rangle .\;0\;)\end{allineato}}}$

Si noti che poiché è stato emesso il nome locale x , l'ambito di x è esteso per coprire anche il terzo componente. Infine, il canale x può essere utilizzato per inviare il nome x . Dopodiché tutti i processi in esecuzione contemporaneamente sono stati interrotti

${\displaystyle {\begin{allineato}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{allineato}}}$

Definizione formale

Sintassi

Sia Χ un insieme di oggetti chiamati nomi . La sintassi astratta per il π -calcolo è costruita dalla seguente grammatica BNF (dove x e y sono qualsiasi nome da Χ):

${\displaystyle {\begin{allineato}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Ricevi sul canale}}x{\text{, associa il risultato a }}y{\text{, quindi esegui }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,& {\text{Invia il valore }}y{\text{ sul canale }}x{\text{, quindi esegui }}P\\&\;|\;P|Q\,\,\,\,\, \,\,\,\,&{\text{Esegui }}P{\text{ e }}Q{\text{ simultaneamente}}\\&\;|\;(\nu x)P\,\, \,&{\text{Crea un nuovo canale }}x{\text{ ed esegui }}P\\&\;|\;!P\,\,\,&{\text{Rigenera copie di }} P\\&\;|\;0&{\text{Termina il processo}}\end{allineato}}}$

Nella sintassi concreta di seguito, i prefissi si legano più strettamente della composizione parallela (|) e le parentesi vengono utilizzate per disambiguare.

I nomi sono vincolati dalla restrizione e dai costrutti di prefisso di input. Formalmente, l'insieme di nomi libere di un processo in π -calcolo sono definite induttivamente dalla tabella che segue. L'insieme dei nomi associati di un processo è definito come i nomi di un processo che non sono nell'insieme dei nomi liberi.

Costruire	Nomi liberi
${\displaystyle 0}$	Nessuno
${\displaystyle {\overline {a}}\langle x\rangle .P}$	un ; x ; tutti i nomi liberi di P
${\displaystyle a(x).P}$	un ; nomi liberi di P tranne x
${\displaystyle P|Q}$	Tutti i nomi liberi di P e Q
${\displaystyle (\nu x).P}$	Nomi liberi di P tranne x
${\displaystyle !P}$	Tutti i nomi liberi di P

Congruenza strutturale

Centrale sia per la semantica di riduzione che per la semantica di transizione etichettata è la nozione di congruenza strutturale . Due processi sono strutturalmente congruenti, se sono identici fino alla struttura. In particolare, la composizione parallela è commutativa e associativa.

Più precisamente, la congruenza strutturale è definita come la relazione di minima equivalenza preservata dai costrutti del processo e che soddisfa:

Conversione alfa :

• ${\displaystyle P\equiv Q}$if può essere ottenuto rinominando uno o più nomi associati in .${\displaystyle Q}$${\displaystyle P}$${\displaystyle P}$

Assiomi per la composizione parallela :

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

Assiomi di restrizione :

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

Assioma per la replica :

• ${\displaystyle !P\equiv P|!P}$

Assioma relativo a restrizione e parallelo :

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$se x non è un nome libero di .${\displaystyle Q}$

Quest'ultimo assioma è noto come assioma dell'"estensione dell'ambito". Questo assioma è centrale, poiché descrive come un nome associato x può essere estruso da un'azione di output, causando l'estensione dell'ambito di x . Nei casi in cui x è un nome libero di , è possibile utilizzare la conversione alfa per consentire l'estensione di procedere. ${\displaystyle Q}$

Semantica di riduzione

Scriviamo se può eseguire un passo di calcolo, in seguito al quale è ora . Questa relazione di riduzione è definita come la relazione minima chiusa in un insieme di regole di riduzione. ${\displaystyle P\rightarrow P'}$${\displaystyle P}$${\displaystyle P'}$ ${\displaystyle \rightarrow}$

La principale regola di riduzione che cattura la capacità dei processi di comunicare attraverso i canali è la seguente:

• ${\displaystyle {\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]}$

dove denota il processo in cui il nome libero è stato sostituito per le occorrenze libere di . Se si verifica un'occorrenza gratuita di in una posizione in cui non sarebbe libera, potrebbe essere necessaria la conversione alfa.${\displaystyle Q[z/y]}$${\displaystyle Q}$${\displaystyle z}$${\displaystyle y}$${\displaystyle y}$${\displaystyle z}$

Ci sono tre regole aggiuntive:

• Se poi anche .${\displaystyle P\rightarrow Q}$${\displaystyle P|R\rightarrow Q|R}$

Questa regola dice che la composizione parallela non inibisce il calcolo.

• Se , allora anche .${\displaystyle P\rightarrow Q}$${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$

Questa regola garantisce che il calcolo possa procedere sotto una restrizione.

• Se e e , allora anche .${\displaystyle P\equiv P'}$${\displaystyle P'\rightarrow Q'}$${\displaystyle Q'\equiv Q}$${\displaystyle P\rightarrow Q}$

Quest'ultima regola afferma che i processi strutturalmente congruenti hanno le stesse riduzioni.

L'esempio rivisitato

Considera di nuovo il processo

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\angle v\rangle .0}$

Applicando la definizione della semantica di riduzione, otteniamo la riduzione

${\displaystyle (\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)| z(v).{\overline {v}}\angle v\rangle .0}$

Nota come, applicando l'assioma di sostituzione della riduzione, le occorrenze libere di sono ora etichettate come . ${\displaystyle y}$${\displaystyle z}$

Successivamente, otteniamo la riduzione

${\displaystyle (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle . 0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)}$

Si noti che poiché è stato emesso il nome locale x , l'ambito di x è esteso per coprire anche il terzo componente. Questo è stato catturato utilizzando l'assioma dell'estensione dell'oscilloscopio.

Quindi, usando l'assioma di sostituzione della riduzione, otteniamo

${\displaystyle (\nu x)(0|0|0)}$

Infine, usando gli assiomi per la composizione parallela e la restrizione, otteniamo

${\displaystyle 0}$

Semantica etichettata

In alternativa, si può dare al pi-calcolo una semantica di transizione etichettata (come è stato fatto con il Calcolo dei Sistemi Comunicanti ).
In questa semantica, una transizione da uno stato a un altro stato dopo un'azione è annotata come: ${\displaystyle P}$${\displaystyle P'}$${\displaystyle\alpha}$

• ${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$

Dove gli stati e rappresentano processi ed è un'azione di input , un'azione di output o un'azione silenziosa τ . ${\displaystyle P}$${\displaystyle P'}$${\displaystyle\alpha}$ ${\displaystyle a(x)}$ ${\displaystyle {\overline {a}}\langle x\rangle}$

Un risultato standard sulla semantica etichettata è che concorda con la semantica di riduzione fino alla congruenza strutturale, nel senso che se e solo se ${\displaystyle P\rightarrow P'}$${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$

Estensioni e varianti

La sintassi fornita sopra è minima. Tuttavia, la sintassi può essere modificata in vari modi.

È possibile aggiungere alla sintassi un operatore di scelta non deterministico . ${\displaystyle P+Q}$

È possibile aggiungere alla sintassi un test per l' uguaglianza dei nomi . Questo operatore di corrispondenza può procedere come se e solo se x e hanno lo stesso nome. Allo stesso modo, si può aggiungere un operatore di mancata corrispondenza per la disuguaglianza dei nomi . Programmi pratici che possono passare nomi (URL o puntatori) utilizzano spesso tale funzionalità: per modellare direttamente tale funzionalità all'interno del calcolo, questa e le relative estensioni sono spesso utili. ${\displaystyle [x=y]P}$${\displaystyle P}$${\displaystyle y}$

La asincrono π -calcolo permette soltanto uscite senza suffisso, atomi di uscita ovvero della forma , ottenendo un calcolo più piccolo. Tuttavia, qualsiasi processo nel calcolo originale può essere rappresentato dalla minore asincrono π -calcolo utilizzando un canale supplementare per simulare esplicito riconoscimento dal processo di ricezione. Poiché un'uscita libera di continuazione può modellare un messaggio in transito, questo frammento mostra che l'originale π -calcolo, che è intuitivamente basa sulla comunicazione sincrona, ha un modello di comunicazione asincrona espressiva all'interno della sua sintassi. Tuttavia, l'operatore di scelta non deterministico definito sopra non può essere espresso in questo modo, poiché una scelta non custodita verrebbe convertita in una custodita; questo fatto è stato utilizzato per dimostrare che il calcolo asincrono è strettamente meno espressivo di quello sincrono (con l'operatore di scelta). ${\displaystyle {\overline {x}}\langle y\rangle}$

Il poliadica π -calcolo permette comunicare più di un nome in un singolo azione: (uscita poliadica) e (ingresso poliadica) . Questa estensione poliadica, utile soprattutto quando si studiano i tipi per i processi di passaggio di nomi, può essere codificata nel calcolo monadico passando il nome di un canale privato attraverso il quale vengono poi passati in sequenza i molteplici argomenti. La codifica è definita ricorsivamente dalle clausole ${\displaystyle {\overline {x}}\langle z_{1},...,z_{n}\rangle .P}$ ${\displaystyle x(z_{1},...,z_{n}).P}$

${\displaystyle {\overline {x}}\langle y_{1},\cdots,y_{n}\rangle.P}$ è codificato come ${\displaystyle (\nu w){\overline {x}}\langle w\rangle.{\overline {w}}\langle y_{1}\rangle.\cdots.{\overline {w}}\langle y_ {n}\rangle .[P]}$

${\displaystyle x(y_{1},\cdots ,y_{n}).P}$ è codificato come ${\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]}$

Tutti gli altri costrutti di processo vengono lasciati invariati dalla codifica.

In quanto sopra, denota la codifica di tutti i prefissi nella continuazione allo stesso modo. ${\displaystyle [P]}$${\displaystyle P}$

Non è necessaria la piena potenza di replica . Spesso si considera solo l' input replicato , il cui assioma di congruenza strutturale è . ${\displaystyle !P}$ ${\displaystyle !x(y).P}$${\displaystyle !x(y).P\equiv x(y).P|!x(y).P}$

Processo di input replicato come può essere inteso come server, in attesa sul canale x di essere invocato dai client. L'invocazione di un server genera una nuova copia del processo , dove a è il nome passato dal client al server, durante l'invocazione di quest'ultimo. ${\displaystyle !x(y).P}$${\displaystyle P[a/y]}$

Un ordine superiore π -calcolo può essere definita in cui non solo i nomi ma processi vengono inviati attraverso canali. La regola di riduzione chiave per il caso di ordine superiore è

${\displaystyle {\overline {x}}\langle R\rangle .P|x(Y).Q\rightarrow P|Q[R/Y]}$

Qui, denota una variabile di processo che può essere istanziata da un termine di processo. Sangiorgi stabilito che la capacità di passare processi non aumenta l'espressività del π -calcolo: superamento di un processo P può essere simulato semplicemente passando un nome che indica P invece. ${\displaystyle Y}$

Proprietà

completezza di Turing

Il π -calcolo è un modello universale di computazione . Questo è stato osservato per la prima volta da Milner nel suo articolo "Functions as Processes", in cui presenta due codifiche del lambda-calcolo nel π -calcolo . Una codifica simula la strategia di valutazione desiderosa (chiamata per valore) , l'altra codifica simula la strategia di ordine normale (chiamata per nome). In entrambi, l'intuizione cruciale è la modellazione dei binding dell'ambiente, ad esempio " x è legato al termine ", come agenti di replica che rispondono alle richieste dei loro binding inviando una connessione al termine . ${\textstyle M}$${\displaystyle M}$

Le caratteristiche del π -calculus che rendono possibili queste codifiche sono il passaggio di nomi e la replica (o, in modo equivalente, agenti definiti ricorsivamente). In assenza di replicazione/ricorsione, il π -calcolo cessa di essere Turing -completo. Questo può essere visto dal fatto che bisimulazione equivalenza diventa decidibile per il calcolo priva di ricorsione e anche per il finito-controllo π -calcolo cui il numero di componenti parallele in qualsiasi processo è delimitata da una costante.

Bisimulazioni del π -calcolo

Per quanto riguarda i calcoli di processo, il π -calcolo consente una definizione di equivalenza di bisimulazione. Nel π -calcolo, la definizione di equivalenza di bisimulazione (nota anche come bisimilarità) può essere basata sulla semantica di riduzione o sulla semantica di transizione etichettata.

Ci sono (almeno) tre diversi modi di definire l'etichetta di equivalenza bisimulazione nel π -calcolo: presto, tardi e aperto bisimilarità. Ciò deriva dal fatto che il π -calculus è un calcolo di processo passa-valore.

Nel resto di questa sezione, denotiamo e denotiamo processi e denotiamo relazioni binarie sui processi. ${\displaystyle p}$${\displaystyle q}$${\displaystyle R}$

Bisimilarità precoce e tardiva

All'inizio e alla fine sono stati entrambi bisimilarità formulate da Milner, Parrow e Walker nel loro articolo originale sul π -calcolo.

Una relazione binaria sui processi è una prima bisimulazione se per ogni coppia di processi , ${\displaystyle R}$${\displaystyle (p,q)\in R}$

• ogni volta che poi per ogni nome ne esiste uno tale che e ;${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$${\displaystyle y}$${\displaystyle q'}$${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$${\displaystyle (p'[y/x],q'[y/x])\in R}$
• per ogni azione non input , se poi ne esiste una tale che e ;${\displaystyle\alpha}$${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$${\displaystyle q'}$${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$${\displaystyle (p',q')\in R}$
• e requisiti simmetrici con e scambiati.${\displaystyle p}$${\displaystyle q}$

Processi e si dice che siano presto bisimilari, scritti se la coppia per qualche bisimulazione precoce . ${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{e}q}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

Nella bisimilarità tardiva, la corrispondenza di transizione deve essere indipendente dal nome trasmesso. Una relazione binaria sui processi è una bisimulazione tardiva se per ogni coppia di processi , ${\displaystyle R}$${\displaystyle (p,q)\in R}$

• ogni volta che poi per alcuni vale quello e per ogni nome y ;${\displaystyle p{\xrightarrow {a(x)}}p'}$${\displaystyle q'}$${\displaystyle q{\xrightarrow {a(x)}}q'}$${\displaystyle (p'[y/x],q'[y/x])\in R}$
• per qualsiasi azione non di input , if implica che ne esista una tale che e ;${\displaystyle\alpha}$${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$${\displaystyle q'}$${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$${\displaystyle (p',q')\in R}$
• e requisiti simmetrici con e scambiati.${\displaystyle p}$${\displaystyle q}$

Processi e si dice che siano bisimilari tardivi, scritti se la coppia per qualche bisimulazione tardiva . ${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{l}q}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

Entrambi e soffrono del problema che non sono relazioni di congruenza, nel senso che non sono preservati da tutti i costrutti di processo. Più precisamente, esistono processi e tali che ma . Si può rimediare a questo problema considerando le relazioni di congruenza massima incluse in e , note rispettivamente come congruenza precoce e congruenza tardiva . ${\displaystyle \sim_{e}}$${\displaystyle \sim_{l}}$${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{e}q}$${\displaystyle a(x).p\not \sim _{e}a(x).q}$${\displaystyle \sim_{e}}$${\displaystyle \sim_{l}}$

Bisimilarità aperta

Fortunatamente è possibile una terza definizione, che evita questo problema, ovvero quella di bisimilarità aperta , dovuta a Sangiorgi.

Una relazione binaria sui processi è una bisimulazione aperta se per ogni coppia di elementi e per ogni sostituzione di nome e ogni azione , ogni volta che ne esiste una tale che e . ${\displaystyle R}$${\displaystyle (p,q)\in R}$${\displaystyle \sigma}$${\displaystyle\alpha}$${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$${\displaystyle q'}$${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$${\displaystyle (p',q')\in R}$

I processi e si dicono aperti bisimilari, scritti se la coppia per qualche bisimulazione aperta . ${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{o}q}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

La bisimilarità precoce, tardiva e aperta è distinta

Le bisimilarità precoce, tardiva e aperta sono distinte. I contenimenti sono adeguati, quindi . ${\displaystyle \sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}}$

In alcuni sottocalcoli come il pi-calcolo asincrono, è noto che la bisimilarità tardiva, precoce e aperta coincidono. Tuttavia, in questo contesto una nozione più appropriata è quella di bisimilarità asincrona . In letteratura, il termine bisimulazione aperta si riferisce solitamente a una nozione più sofisticata, in cui processi e relazioni sono indicizzati da relazioni di distinzione; i dettagli sono nel documento di Sangiorgi sopra citato.

Equivalenza spinata

In alternativa, si può definire l'equivalenza di bisimulazione direttamente dalla semantica di riduzione. Scriviamo se il processo consente immediatamente un input o un output su name . ${\displaystyle p\Downarrow a}$${\displaystyle p}$${\displaystyle a}$

Una relazione binaria sui processi è una bisimulazione spinata se è una relazione simmetrica che soddisfa che per ogni coppia di elementi abbiamo che ${\displaystyle R}$${\displaystyle (p,q)\in R}$

(1) se e solo se per ogni nome${\displaystyle p\Downarrow a}$${\displaystyle q\Downarrow a}$${\displaystyle a}$

e

(2) per ogni riduzione esiste una riduzione${\displaystyle p\rightarrow p'}$${\displaystyle q\rightarrow q'}$

tale che . ${\displaystyle (p',q')\in R}$

Diciamo che e sono bisimilare spinato se esiste una bisimulazione spinato dove . ${\displaystyle p}$${\displaystyle q}$${\displaystyle R}$${\displaystyle (p,q)\in R}$

Definire un contesto come un termine π con un buco [] si dice che due processi P e Q sono congruenti a punta , scritti , se per ogni contesto abbiamo quello e sono bisimili a punta. Si scopre che la congruenza spinata coincide con la congruenza indotta dalla bisimilarità precoce. ${\displaystyle P\sim _{b}Q\,\!}$${\displaystyle C[]}$${\displaystyle C[P]}$${\displaystyle C[Q]}$

Applicazioni

Il π -calcolo è stato usato per descrivere molti diversi tipi di sistemi concorrenti. In effetti, alcune delle applicazioni più recenti esulano dal regno dell'informatica tradizionale.

Nel 1997, Martin Abadi e Andrew Gordon hanno proposto un'estensione del π -calculus, lo Spi-calculus, come notazione formale per descrivere e ragionare sui protocolli crittografici. Lo spi-calcolo estende il π -calcolo con primitive per la crittografia e la decrittazione. Nel 2001, Martin Abadi e Cedric Fournet generalizzati la gestione dei protocolli crittografici per produrre il applicata π calcolo. C'è ora un ampio corpus di lavoro dedicato alle varianti del calcolo π applicato , incluso un numero di strumenti di verifica sperimentale. Un esempio è lo strumento ProVerif [2] di Bruno Blanchet, basato su una traduzione del π -calcolo applicato nel framework di programmazione logica di Blanchet. Un altro esempio è Cryptyc [3] , dovuto a Andrew Gordon e Alan Jeffrey, che utilizza il metodo delle asserzioni di corrispondenza di Woo e Lam come base per i sistemi di tipi che possono verificare le proprietà di autenticazione dei protocolli crittografici.

Intorno al 2002, Howard Smith e Peter Fingar si interessarono al fatto che π -calculus sarebbe diventato uno strumento di descrizione per la modellazione dei processi aziendali. Entro luglio 2006, c'è una discussione nella comunità su quanto ciò possa essere utile. Più recentemente, il π -calculus ha costituito la base teorica del Business Process Modeling Language (BPML) e di XLANG di Microsoft.

Il π- calcolo ha anche attirato l'interesse per la biologia molecolare. Nel 1999, Aviv Regev e Ehud Shapiro hanno dimostrato che si può descrivere una via di segnalazione cellulare (la cosiddetta cascata RTK / MAPK ) ed in particolare il "lego" molecolare che implementa questi compiti di comunicazione in un'estensione del π- calcolo. A seguito di questo articolo fondamentale, altri autori hanno descritto l'intera rete metabolica di una cellula minima. Nel 2009, Anthony Nash e Sara Kalvala hanno proposto un framework π- calculus per modellare la trasduzione del segnale che dirige l' aggregazione di Dictyostelium discoideum .

Storia

Il π- calcolo è stato originariamente sviluppato da Robin Milner , Joachim Parrow e David Walker nel 1992, sulla base delle idee di Uffe Engberg e Mogens Nielsen. Può essere visto come una continuazione del lavoro di Milner sul calcolo dei processi CCS ( Calculus of Communicating Systems ). Nella sua conferenza Turing, Milner descrive lo sviluppo del π -calcolo come un tentativo di catturare l'uniformità dei valori e dei processi in attori.

implementazioni

I seguenti linguaggi di programmazione implementano il π -calculus o una delle sue varianti:

• Linguaggio di modellazione dei processi aziendali (BPML)
• occam-π
• immagine
• JoCaml (basato sul calcolo Join )
• RhoLang

Appunti

Riferimenti

• Milner, Robin (1999). Sistemi comunicanti e mobili: il -calcolo . Cambridge, Regno Unito: Cambridge University Press. ISBN 0-521-65869-1.
• Milner, Robin (1993). "Il -Calcolo poliadico: un tutorial" . In Florida Hamer; W. Brauer; H. Schwichtenberg (a cura di). Logica e Algebra della Specificazione . Springer-Verlag.
• Sangiorgi, Davide ; Walker, David (2001). Il π-calcolo: una teoria dei processi mobili . Cambridge, Regno Unito: Cambridge University Press. ISBN 0-521-78177-9.

link esterno

• PiCalculus sul wiki di C2
• FAQ su π-Calculus di Jeannette M. Wing