Cálculo π

Un elemento central del cálculo π es la noción de nombre . La simplicidad del cálculo radica en el doble papel que desempeñan los nombres como canales de comunicación y variables .

Las construcciones de proceso disponibles en el cálculo son las siguientes ^{[ 3 ]} (una definición precisa se da en la siguiente sección):

• concurrencia , escrito${\displaystyle P\mid Q}$, dónde${\displaystyle P}$y${\displaystyle Q}$son dos procesos o hilos que se ejecutan simultáneamente.
• comunicación , donde
  • prefijo de entrada${\displaystyle c\left(x\right).P}$es un proceso que espera un mensaje que fue enviado en un canal de comunicación llamado${\displaystyle c}$antes de proceder como${\displaystyle P}$, vinculando el nombre recibido con el nombre x . Normalmente, esto modela un proceso que espera una comunicación de la red o una etiqueta cque solo puede ser utilizada una vez por una goto coperación.
  • prefijo de salida${\displaystyle {\overline {c}}\langle y\rangle .P}$describe que el nombre${\displaystyle y}$se emite en el canal${\displaystyle c}$antes de proceder como${\displaystyle P}$Normalmente , esto modela el envío de un mensaje en la red o una goto coperación.
• replicación , escrita${\displaystyle$ !\,P} , que puede verse como un proceso que siempre puede crear una nueva copia de${\displaystyle P}$Normalmente , esto modela un servicio de red o una etiqueta cque espera una serie de goto coperaciones.
• creación de un nuevo nombre , escrito${\displaystyle \left(\nu x\right)P}$, que puede verse como un proceso que asigna una nueva constante x dentro${\displaystyle P}$Las constantes del cálculo π se definen únicamente por sus nombres y son siempre canales de comunicación. La creación de un nuevo nombre en un proceso también se denomina restricción .
• el proceso nulo, escrito${\displaystyle 0}$, es un proceso cuya ejecución ha finalizado y se ha detenido.

Aunque el minimalismo del cálculo π nos impide escribir programas en el sentido habitual, es fácil extenderlo. En particular, es fácil definir estructuras de control como la recursión, los bucles y la composición secuencial, así como tipos de datos como funciones de primer orden, valores de verdad , listas y enteros. Además, se han propuesto extensiones del cálculo π que tienen en cuenta la criptografía de distribución o de clave pública . El cálculo π aplicado por Abadi y FournetSe formalizó el estudio de estas diversas extensiones mediante la ampliación del cálculo π con tipos de datos arbitrarios.

A continuación se muestra un pequeño ejemplo de un proceso que consta de tres componentes en paralelo. El nombre del canal x solo es conocido por los dos primeros componentes.

${\displaystyle {\begin{aligned}(\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{aligned}}}$

Los dos primeros componentes pueden comunicarse en el canal x , y el nombre y queda vinculado a z . Por lo tanto, el siguiente paso en el proceso es:

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

Tenga en cuenta que la variable y restante no se ve afectada porque está definida en un ámbito interno. Los componentes paralelos segundo y tercero ahora pueden comunicarse en el canal z , y el nombre v queda vinculado a x . El siguiente paso en el proceso es ahora

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

Nótese que, dado que se ha emitido el nombre local x , el alcance de x se extiende para abarcar también el tercer componente. Finalmente, el canal x se puede utilizar para enviar el nombre x . Después de eso, todos los procesos que se ejecutan simultáneamente se han detenido.

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

Sea Χ un conjunto de objetos llamados nombres . La sintaxis abstracta para el cálculo π se construye a partir de la siguiente gramática BNF (donde x e y son nombres cualesquiera de Χ): ^{[ 4 ]}

${\displaystyle {\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Receive on channel }}x{\text{, bind the result to }}y{\text{, then run }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{Send the value }}y{\text{ over channel }}x{\text{, then run }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{Run }}P{\text{ and }}Q{\text{ simultaneously}}\\&\;|\;(\nu x)P\,\,\,&{\text{Create a new channel }}x{\text{ and run }}P\\&\;|\;!P\,\,\,&{\text{Repeatedly spawn copies of }}P\\&\;|\;0&{\text{Terminate the process}}\end{aligned}}}$

En la sintaxis concreta que se muestra a continuación, los prefijos se vinculan de forma más estrecha que la composición paralela (|), y los paréntesis se utilizan para desambiguar.

Los nombres están sujetos a las restricciones y a los prefijos de entrada. Formalmente, el conjunto de nombres libres de un proceso en el cálculo π se define inductivamente mediante la tabla que se muestra a continuación. El conjunto de nombres ligados de un proceso se define como aquellos nombres que no pertenecen al conjunto de nombres libres.

Un concepto fundamental tanto para la semántica de reducción como para la semántica de transición etiquetada es la noción de congruencia estructural . Dos procesos son estructuralmente congruentes si son idénticos salvo por su estructura. En particular, la composición paralela es conmutativa y asociativa.

Más precisamente, la congruencia estructural se define como la relación de equivalencia mínima preservada por las construcciones del proceso y que satisface:

Conversión alfa :

• ${\displaystyle P\equiv Q}$si${\displaystyle Q}$se puede obtener de${\displaystyle P}$cambiando el nombre de uno o más nombres vinculados en${\displaystyle P}$.

Axiomas para la composición paralela :

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

Axiomas para la restricción :

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

Axioma para la replicación :

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

Axioma que relaciona restricción y paralelismo :

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$si x no es un nombre libre de${\displaystyle Q}$.

Este último axioma se conoce como el axioma de "extensión de ámbito". Este axioma es fundamental, ya que describe cómo un nombre ligado x puede ser extruido por una acción de salida, lo que provoca que el ámbito de x se extienda. En los casos en que x es un nombre libre de${\displaystyle Q}$, se puede utilizar la conversión alfa para permitir que la extensión continúe.

Escribimos${\displaystyle P\rightarrow P'}$si${\displaystyle P}$puede realizar un paso de cálculo, después del cual ahora${\displaystyle P'}$Esta relación de reducción${\displaystyle \rightarrow }$se define como la relación más pequeña cerrada bajo un conjunto de reglas de reducción.

La regla de reducción principal que captura la capacidad de los procesos para comunicarse a través de canales es la siguiente:

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

dónde${\displaystyle Q[z/y]}$denota el proceso${\displaystyle Q}$en el que el nombre libre${\displaystyle z}$ha sido sustituido por las ocurrencias libres de${\displaystyle y}$. Si ocurre una ocurrencia libre de${\displaystyle y}$ocurre en un lugar donde${\displaystyle z}$No sería gratuito, podría ser necesaria la conversión alfa.

Hay tres reglas adicionales:

• Si${\displaystyle P\rightarrow Q}$entonces también${\displaystyle P|R\rightarrow Q|R}$.

Esta regla establece que la composición paralela no inhibe el cálculo.

• Si${\displaystyle P\rightarrow Q}$, entonces también${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$.

Esta regla garantiza que el cálculo pueda continuar incluso bajo una restricción.

• Si${\displaystyle P\equiv P'}$y${\displaystyle P'\rightarrow Q'}$y${\displaystyle Q'\equiv Q}$, entonces también${\displaystyle P\rightarrow Q}$.

Esta última regla establece que los procesos que son estructuralmente congruentes tienen las mismas reducciones.

Consideremos nuevamente el proceso

${\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}$

Aplicando la definición de la semántica de reducción, obtenemos la reducción

${\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}}\langle v\rangle .0}$

Nótese cómo, aplicando el axioma de sustitución de reducción, ocurrencias libres de${\displaystyle y}$ahora están etiquetados como${\displaystyle z}$.

A continuación, obtenemos la reducción.

${\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)}$

Tenga en cuenta que, dado que se ha generado el nombre local x , el ámbito de x se extiende para abarcar también el tercer componente. Esto se capturó utilizando el axioma de extensión de ámbito.

A continuación, utilizando el axioma de sustitución de reducción, obtenemos:

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

Finalmente, utilizando los axiomas para la composición y restricción paralelas, obtenemos

${\displaystyle 0}$

Alternativamente, se puede dar al cálculo pi una semántica de transición etiquetada (como se ha hecho con el Cálculo de Sistemas Comunicantes ). En esta semántica, una transición de un estado${\displaystyle P}$a algún otro estado${\displaystyle P'}$después de una acción${\displaystyle \alpha }$se anota como:

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

Donde los estados${\displaystyle P}$y${\displaystyle P'}$representar procesos y${\displaystyle \alpha }$es una acción de entrada${\displaystyle a(x)}$, una acción de salida${\displaystyle {\overline {a}}\langle x\rangle }$, o una acción silenciosa τ . ^{[ 5 ]}

Un resultado estándar sobre la semántica etiquetada es que coincide con la semántica de reducción salvo congruencia estructural, en el sentido de que ${\displaystyle P\rightarrow P'}$si y solo si${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$^{[ 6 ]}

El cálculo π es un modelo universal de computación . Esto fue observado por primera vez por Milner en su artículo "Funciones como procesos" ^{[ 10 ]} , en el que presenta dos codificaciones del cálculo lambda en el cálculo π . Una codificación simula la estrategia de evaluación ávida (llamada por valor) , la otra codificación simula la estrategia de orden normal (llamada por nombre). En ambas, la idea crucial es el modelado de las vinculaciones del entorno; por ejemplo, " x está vinculado al término${\textstyle M}$"– como agentes replicantes que responden a las solicitudes de sus enlaces enviando de vuelta una conexión al término${\displaystyle M}$.

Las características del cálculo π que hacen posibles estas codificaciones son el paso de nombres y la replicación (o, equivalentemente, agentes definidos recursivamente). En ausencia de replicación/recursión, el cálculo π deja de ser Turing-completo. Esto se puede observar en el hecho de que la equivalencia de bisimulación se vuelve decidible para el cálculo sin recursión e incluso para el cálculo π de control finito, donde el número de componentes paralelas en cualquier proceso está limitado por una constante. ^{[ 11 ]}

La bisimilitud temprana y tardía fueron formuladas por Milner, Parrow y Walker en su artículo original sobre el cálculo π . ^{[ 12 ]}

Una relación binaria${\displaystyle R}$sobre procesos es una bisimulación temprana si para cada par de procesos${\displaystyle (p,q)\in R}$,

• cuando sea${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$entonces para cada nombre${\displaystyle y}$existe algo${\displaystyle q'}$de tal manera que${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$y${\displaystyle (p'[y/x],q'[y/x])\in R}$;
• para cualquier acción que no sea de entrada${\displaystyle \alpha }$, si${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$entonces existe algo${\displaystyle q'}$de tal manera que${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$y${\displaystyle (p',q')\in R}$;
• y requisitos simétricos con${\displaystyle p}$y${\displaystyle q}$intercambiado.

Procesos${\displaystyle p}$y${\displaystyle q}$Se dice que son bisimilares tempranos, escritos${\displaystyle p\sim _{e}q}$si el par${\displaystyle (p,q)\in R}$para alguna bisimulación temprana${\displaystyle R}$.

En la bisimilitud tardía, la coincidencia de transición debe ser independiente del nombre que se transmite. Una relación binaria${\displaystyle R}$sobre procesos es una bisimulación tardía si para cada par de procesos${\displaystyle (p,q)\in R}$,

• cuando sea${\displaystyle p{\xrightarrow {a(x)}}p'}$entonces para algunos${\displaystyle q'}$sostiene que${\displaystyle q{\xrightarrow {a(x)}}q'}$y${\displaystyle (p'[y/x],q'[y/x])\in R}$para cada nombre y ;
• para cualquier acción que no sea de entrada${\displaystyle \alpha }$, si${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$implica que existe alguna${\displaystyle q'}$de tal manera que${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$y${\displaystyle (p',q')\in R}$;
• y requisitos simétricos con${\displaystyle p}$y${\displaystyle q}$intercambiado.

Procesos${\displaystyle p}$y${\displaystyle q}$Se dice que son bisimilares tardíos, escritos${\displaystyle p\sim _{l}q}$si el par${\displaystyle (p,q)\in R}$para alguna bisimulación tardía${\displaystyle R}$.

Ambos${\displaystyle \sim _{e}}$y${\displaystyle \sim _{l}}$sufren del problema de que no son relaciones de congruencia en el sentido de que no se conservan en todas las construcciones de procesos. Más precisamente, existen procesos${\displaystyle p}$y${\displaystyle q}$de tal manera que${\displaystyle p\sim _{e}q}$pero${\displaystyle a(x).p\not \sim _{e}a(x).q}$. Se puede remediar este problema considerando las relaciones de congruencia máximas incluidas en${\displaystyle \sim _{e}}$y${\displaystyle \sim _{l}}$, conocidas respectivamente como congruencia temprana y congruencia tardía .

Afortunadamente, es posible una tercera definición que evita este problema, a saber, la de bisimilitud abierta , debida a Sangiorgi. ^{[ 13 ]}

Una relación binaria${\displaystyle R}$sobre procesos es una bisimulación abierta si para cada par de elementos${\displaystyle (p,q)\in R}$y por cada sustitución de nombre${\displaystyle \sigma }$y cada acción${\displaystyle \alpha }$, cuando sea${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$entonces existe algo${\displaystyle q'}$de tal manera que${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$y${\displaystyle (p',q')\in R}$.

Procesos${\displaystyle p}$y${\displaystyle q}$Se dice que son bisimilares abiertos, escritos${\displaystyle p\sim _{o}q}$si el par${\displaystyle (p,q)\in R}$para alguna bisimulación abierta${\displaystyle R}$.

Alternativamente, se puede definir la equivalencia de bisimulación directamente a partir de la semántica de reducción. Escribimos:${\displaystyle p\Downarrow a}$si el proceso${\displaystyle p}$Permite inmediatamente una entrada o una salida por nombre.${\displaystyle a}$.

Una relación binaria${\displaystyle R}$sobre procesos es una bisimulación con púas si es una relación simétrica que satisface que para cada par de elementos${\displaystyle (p,q)\in R}$tenemos eso

(1)${\displaystyle p\Downarrow a}$si y solo si${\displaystyle q\Downarrow a}$para cada nombre${\displaystyle a}$

y

(2) por cada reducción${\displaystyle p\rightarrow p'}$existe una reducción${\displaystyle q\rightarrow q'}$

de tal manera que${\displaystyle (p',q')\in R}$.

Decimos que${\displaystyle p}$y${\displaystyle q}$son bisimilares con púas si existe una bisimulación con púas${\displaystyle R}$dónde${\displaystyle (p,q)\in R}$.

Definiendo un contexto como un término π con un agujero [] decimos que dos procesos P y Q son congruentes con púas , escritos${\displaystyle P\sim _{b}Q\,\!}$, si para cada contexto${\displaystyle C[]}$tenemos eso${\displaystyle C[P]}$y${\displaystyle C[Q]}$son bisimilares con púas. Resulta que la congruencia con púas coincide con la congruencia inducida por la bisimilaridad temprana.