cálculo π

Cálculo de procesos

En informática teórica , el cálculo π (o cálculo pi ) es un cálculo de procesos . El cálculo π permite comunicar los nombres de los canales a lo largo de los mismos y, de esta manera, es capaz de describir cálculos concurrentes cuya configuración de red puede cambiar durante el cálculo.

El cálculo π tiene pocos términos y es un lenguaje pequeño, pero expresivo (ver § Sintaxis). Los programas funcionales pueden codificarse en el cálculo π , y la codificación enfatiza la naturaleza dialógica del cálculo, estableciendo conexiones con la semántica de los juegos . Las extensiones del cálculo π , como el cálculo spi y el cálculo π aplicado , han tenido éxito en el razonamiento sobre protocolos criptográficos . Además del uso original para describir sistemas concurrentes, el cálculo π también se ha utilizado para razonar sobre procesos comerciales ^[1] y biología molecular . ^[2]

Definición informal

El cálculo π pertenece a la familia de los cálculos de procesos , formalismos matemáticos para describir y analizar propiedades de computación concurrente. De hecho, el cálculo π , al igual que el cálculo λ , es tan minimalista que no contiene primitivos como números, booleanos, estructuras de datos, variables, funciones o incluso las instrucciones de flujo de control habituales (como if-then-else, while).

Construcciones de proceso

El concepto de nombre es central en el cálculo π . La simplicidad del cálculo reside 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 , donde y son dos procesos o subprocesos ejecutados simultáneamente. ${\displaystyle P\mid Q}$ ${\displaystyle P}$ ${\displaystyle Q}$
• comunicación , donde
  • La prefijación de entrada es un proceso que espera un mensaje que se envió en un canal de comunicación llamado antes de continuar como , vinculando el nombre recibido al nombre x . Por lo general, esto modela un proceso que espera una comunicación de la red o una etiqueta que una operación puede usar solo una vez. ${\displaystyle c\left(x\right).P}$ ${\displaystyle c}$ ${\displaystyle P}$cgoto c
  • El prefijo de salida describe que el nombre se emite en el canal antes de continuar como . Normalmente, esto modela el envío de un mensaje en la red o una operación. ${\displaystyle {\overline {c}}\langle y\rangle .P}$ ${\displaystyle y}$ ${\displaystyle c}$ ${\displaystyle P}$goto c
• replicación , escrita , que puede verse como un proceso que siempre puede crear una nueva copia de . Normalmente, esto modela un servicio de red o una etiqueta que espera cualquier cantidad de operaciones. ${\displaystyle !\,P}$ ${\displaystyle P}$cgoto c
• creación de un nuevo nombre , escrito , que puede verse como un proceso que asigna una nueva constante x dentro de . Las constantes del cálculo π se definen solo por sus nombres y siempre son canales de comunicación. La creación de un nuevo nombre en un proceso también se denomina restricción . ${\displaystyle \left(\nu x\right)P}$ ${\displaystyle P}$
• El proceso nulo, escrito , es un proceso cuya ejecución está completa y se ha detenido. ${\displaystyle 0}$

Aunque el minimalismo del cálculo π nos impide escribir programas en el sentido normal, es fácil extender el cálculo. En particular, es fácil definir tanto estructuras de control como recursión, bucles y composición secuencial como tipos de datos como funciones de primer orden, valores de verdad , listas y números enteros. Además, se han propuesto extensiones del cálculo π que tienen en cuenta la distribución o la criptografía de clave pública. El cálculo π aplicado debido a Abadi y Fournet [1] puso estas diversas extensiones en una base formal al extender el cálculo π con tipos de datos arbitrarios.

Un pequeño ejemplo

A continuación se muestra un pequeño ejemplo de un proceso que consta de tres componentes paralelos. El nombre del canal x solo lo conocen 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 asociado a z . Por lo tanto, el siguiente paso del 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 el resto de y no se ve afectado porque está definido en un ámbito interno. El segundo y tercer componente paralelo ahora pueden comunicarse en el canal llamado z y el nombre v se vincula a x . El siguiente paso en el proceso ahora es

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

Tenga en cuenta que, dado que se ha enviado el nombre local x , el alcance de x se amplía para cubrir también el tercer componente. Por último, 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}}}$

Definición formal

Sintaxis

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 unen con más fuerza que la composición paralela (|) y los paréntesis se utilizan para eliminar la ambigüedad.

Los nombres están limitados por las construcciones de restricción y prefijo de entrada. Formalmente, el conjunto de nombres libres de un proceso en el cálculo π se define de manera inductiva mediante la siguiente tabla. El conjunto de nombres limitados de un proceso se define como los nombres de un proceso que no están en el conjunto de nombres libres.

Congruencia estructural

La noción de congruencia estructural es central tanto para la semántica de reducción como para la semántica de transición etiquetada . Dos procesos son estructuralmente congruentes si son idénticos en cuanto a 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 los constructos del proceso y que satisface:

Conversión alfa :

• ${\displaystyle P\equiv Q}$Si se puede obtener a partir de renombrar uno o más nombres enlazados en . ${\displaystyle Q}$ ${\displaystyle P}$ ${\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 de 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 del alcance". Este axioma es fundamental, ya que describe cómo un nombre x ligado puede ser extruido por una acción de salida, lo que hace que el alcance de x se extienda. En los casos en que x es un nombre libre de , se puede utilizar la conversión alfa para permitir que la extensión continúe. ${\displaystyle Q}$

Semántica de reducción

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

La principal regla de reducción 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]}$

donde denota el proceso en el que el nombre libre ha sido sustituido por las ocurrencias libres de . Si una ocurrencia libre de ocurre en una ubicación donde no estaría libre, puede ser necesaria una conversión alfa. ${\displaystyle Q[z/y]}$ ${\displaystyle Q}$ ${\displaystyle z}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle z}$

Hay tres reglas adicionales:

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

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

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

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

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

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

El ejemplo revisado

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

Observe cómo, al aplicar el axioma de reducción-sustitución, las apariciones libres de ahora se etiquetan como . ${\displaystyle y}$ ${\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 alcance de x se amplía para cubrir también el tercer componente. Esto se capturó utilizando el axioma de extensión del alcance.

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

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

Finalmente, utilizando los axiomas de composición paralela y restricción, obtenemos

${\displaystyle 0}$

Semántica etiquetada

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

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

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

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

Extensiones y variantes

La sintaxis que se muestra arriba es mínima. Sin embargo, se puede modificar de varias maneras.

Se puede agregar un operador de elección no determinista a la sintaxis. ${\displaystyle P+Q}$

Se puede añadir a la sintaxis una prueba de igualdad de nombres . Este operador de coincidencia puede proceder como si y solo si x y son el mismo nombre. De manera similar, se puede añadir un operador de desajuste para la desigualdad de nombres . Los programas prácticos que pueden pasar nombres (URL o punteros) suelen utilizar dicha funcionalidad: para modelar directamente dicha funcionalidad dentro del cálculo, esta y otras extensiones relacionadas suelen ser útiles. ${\displaystyle [x=y]P}$ ${\displaystyle P}$ ${\displaystyle y}$

El cálculo π asincrónico ^{[7] [8]} permite solo salidas sin continuación, es decir, átomos de salida de la forma , lo que produce un cálculo más pequeño. Sin embargo, cualquier proceso en el cálculo original puede representarse mediante el cálculo π asincrónico más pequeño utilizando un canal adicional para simular un reconocimiento explícito del proceso receptor. Dado que una salida sin continuación puede modelar un mensaje en tránsito, este fragmento muestra que el cálculo π original , que se basa intuitivamente en la comunicación sincrónica, tiene un modelo de comunicación asincrónica expresivo dentro de su sintaxis. Sin embargo, el operador de elección no determinista definido anteriormente no puede expresarse de esta manera, ya que una elección sin protección se convertiría en una con protección; este hecho se ha utilizado para demostrar que el cálculo asincrónico es estrictamente menos expresivo que el sincrónico (con el operador de elección). ^[9] ${\displaystyle {\overline {x}}\langle y\rangle }$

El cálculo poliádico π permite comunicar más de un nombre en una sola acción: (salida poliádica) y (entrada poliádica) . Esta extensión poliádica, que es útil especialmente cuando se estudian tipos para procesos de paso de nombres, se puede codificar en el cálculo monádico pasando el nombre de un canal privado a través del cual se pasan los múltiples argumentos en secuencia. La codificación se define recursivamente mediante las cláusulas ${\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}$está codificado como ${\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}$está codificado como ${\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]}$

Todas las demás construcciones del proceso no se modifican con la codificación.

En lo anterior, se denota la codificación de todos los prefijos en la continuación de la misma manera. ${\displaystyle [P]}$ ${\displaystyle P}$

No se necesita toda la potencia de replicación . A menudo, solo se considera la entrada replicada , cuyo axioma de congruencia estructural es . ${\displaystyle !P}$ ${\displaystyle !x(y).P}$ ${\displaystyle !x(y).P\equiv x(y).P|!x(y).P}$

Proceso de entrada replicado, como se puede entender por servidores, que esperan en el canal x para ser invocado por los clientes. La invocación de un servidor genera una nueva copia del proceso , donde a es el nombre que el cliente pasa al servidor durante la invocación de este último. ${\displaystyle !x(y).P}$ ${\displaystyle P[a/y]}$

Se puede definir un cálculo π de orden superior en el que no solo se envían nombres sino también procesos a través de canales. La regla de reducción de claves para el caso de orden superior es

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

Aquí, denota una variable de proceso que puede ser instanciada por un término de proceso. Sangiorgi estableció que la capacidad de pasar procesos no aumenta la expresividad del cálculo π : pasar un proceso P puede simularse simplemente pasando un nombre que apunte a P. ${\displaystyle Y}$

Propiedades

Completitud de Turing

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 ansiosa (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 los enlaces del entorno -por ejemplo, " x está enlazado a término "- como agentes replicadores que responden a las solicitudes de sus enlaces enviando de vuelta una conexión al término . ${\textstyle M}$ ${\displaystyle M}$

Las características del cálculo π que hacen posible estas codificaciones son el paso de nombres y la replicación (o, equivalentemente, los agentes definidos recursivamente). En ausencia de replicación/recursión, el cálculo π deja de ser Turing-completo. Esto se puede ver por 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 paralelos en cualquier proceso está limitado por una constante. ^[11]

Bisimulaciones en laπ-cálculo

En cuanto a los cálculos de proceso, el cálculo π permite definir la equivalencia de bisimulación. En el cálculo π , la definición de equivalencia de bisimulación (también conocida como bisimilaridad) puede basarse en la semántica de reducción o en la semántica de transición etiquetada.

Existen (al menos) tres formas diferentes de definir la equivalencia de bisimulación etiquetada en el cálculo π : bisimilaridad temprana, tardía y abierta. Esto se debe al hecho de que el cálculo π es un cálculo de proceso de paso de valores.

En el resto de esta sección, denotamos y procesos y denotamos relaciones binarias sobre procesos. ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle R}$

Bisimilaridad temprana y tardía

Tanto la bisimilaridad temprana como la tardía fueron formuladas por Milner, Parrow y Walker en su artículo original sobre el cálculo π . ^[12]

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

• siempre que para cada nombre exista alguno tal que y ; ${\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}$
• para cualquier acción que no sea de entrada , si entonces existe algo tal que y ; ${\displaystyle \alpha }$ ${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$ ${\displaystyle q'}$ ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$ ${\displaystyle (p',q')\in R}$
• y requisitos simétricos con e intercambiados. ${\displaystyle p}$ ${\displaystyle q}$

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

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

• siempre que para algunos se cumple que y para cada nombre y ; ${\displaystyle p{\xrightarrow {a(x)}}p'}$ ${\displaystyle q'}$ ${\displaystyle q{\xrightarrow {a(x)}}q'}$ ${\displaystyle (p'[y/x],q'[y/x])\in R}$
• para cualquier acción que no sea de entrada , si implica que existe algún tal que y ; ${\displaystyle \alpha }$ ${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$ ${\displaystyle q'}$ ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$ ${\displaystyle (p',q')\in R}$
• y requisitos simétricos con e intercambiados. ${\displaystyle p}$ ${\displaystyle q}$

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

Tanto y sufren del problema de que no son relaciones de congruencia en el sentido de que no se conservan en todos los constructos de proceso. Más precisamente, existen procesos y tales que pero . Se puede remediar este problema considerando las relaciones de congruencia máxima incluidas en y , conocidas como congruencia temprana y congruencia tardía , respectivamente. ${\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}}$

Bisimilaridad abierta

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

Una relación binaria sobre procesos es una bisimulación abierta si para cada par de elementos y para cada sustitución de nombre y cada acción , siempre que exista algún tal que y . ${\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}$

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

La bisimilaridad temprana, tardía y abierta son distintas

La bisimilaridad temprana, tardía y abierta son distintas. Las contenciones son propias, por lo que . ${\displaystyle \sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}}$

En ciertos subcálculos, como el cálculo pi asincrónico, se sabe que la bisimilitud tardía, temprana y abierta coinciden. Sin embargo, en este contexto, una noción más apropiada es la de bisimilitud asincrónica . En la literatura, el término bisimulación abierta generalmente se refiere a una noción más sofisticada, donde los procesos y las relaciones se indexan mediante relaciones de distinción; los detalles se encuentran en el artículo de Sangiorgi citado anteriormente.

Equivalencia de púas

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

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

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

y

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

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

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

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

Aplicaciones

El cálculo π se ha utilizado para describir muchos tipos diferentes de sistemas concurrentes. De hecho, algunas de las aplicaciones más recientes se encuentran fuera del ámbito de la informática tradicional.

En 1997, Martin Abadi y Andrew Gordon propusieron una extensión del cálculo π , el cálculo Spi, como una notación formal para describir y razonar sobre protocolos criptográficos. El cálculo Spi extiende el cálculo π con primitivas para cifrado y descifrado. En 2001, Martin Abadi y Cedric Fournet generalizaron el manejo de protocolos criptográficos para producir el cálculo π aplicado . Actualmente existe una gran cantidad de trabajo dedicado a variantes del cálculo π aplicado , incluyendo una serie de herramientas de verificación experimental. Un ejemplo es la herramienta ProVerif [2] de Bruno Blanchet, basada en una traducción del cálculo π aplicado al marco de programación lógica de Blanchet. Otro ejemplo es Cryptyc [3], de Andrew Gordon y Alan Jeffrey, que utiliza el método de aserciones de correspondencia de Woo y Lam como base para sistemas de tipos que pueden verificar las propiedades de autenticación de los protocolos criptográficos.

Alrededor de 2002, Howard Smith y Peter Fingar se interesaron en que el cálculo π se convirtiera en una herramienta de descripción para modelar procesos de negocios. En julio de 2006, se comenzó a debatir en la comunidad sobre su utilidad. Más recientemente, el cálculo π ha formado la base teórica del lenguaje de modelado de procesos de negocios (BPML) y del XLANG de Microsoft. ^[14]

El cálculo π también ha despertado interés en la biología molecular. En 1999, Aviv Regev y Ehud Shapiro demostraron que se puede describir una vía de señalización celular (la denominada cascada RTK / MAPK ) y, en particular, el "lego" molecular que implementa estas tareas de comunicación en una extensión del cálculo π . ^[2] Tras este artículo seminal, otros autores describieron toda la red metabólica de una célula mínima. ^[15] En 2009, Anthony Nash y Sara Kalvala propusieron un marco de cálculo π para modelar la transducción de señales que dirige la agregación de Dictyostelium discoideum . ^[16]

Historia

El cálculo π fue desarrollado originalmente por Robin Milner , Joachim Parrow y David Walker en 1992, basándose en ideas de Uffe Engberg y Mogens Nielsen. ^[17] Puede verse como una continuación del trabajo de Milner sobre el cálculo de procesos CCS ( Cálculo de sistemas de comunicación ). En su conferencia de Turing, Milner describe el desarrollo del cálculo π como un intento de capturar la uniformidad de valores y procesos en los actores. ^[18]

Implementaciones

Los siguientes lenguajes de programación implementan el cálculo π o una de sus variantes:

• Lenguaje de modelado de procesos de negocio (BPML)
• Occam-π
• picto
• JoCaml (basado en el cálculo de unión )
• Lenguaje Rho

Notas

1. Especificación OMG (2011). "Business Process Model and Notation (BPMN) Versión 2.0", Object Management Group . p.21
2. Regev, Aviv ; William Silverman; Ehud Y. Shapiro (2001). "Representación y simulación de procesos bioquímicos utilizando el álgebra de procesos de cálculo pi". Simposio del Pacífico sobre bioinformática : 459–470. doi :10.1142/9789814447362_0045. ISBN 978-981-02-4515-3. Número de identificación personal  11262964.
3. Wing, Jeannette M. (27 de diciembre de 2002). "Preguntas frecuentes sobre el cálculo π" (PDF) .
4. Un cálculo de procesos móviles, parte 1, página 10, por R. Milner, J. Parrow y D. Walker, publicado en Information and Computation 100(1), pp.1-40, septiembre de 1992
5. Robin Milner, Sistemas de comunicación y móviles: el cálculo Pi, Cambridge University Press, ISBN 0521643201 . 1999 
6. Sangiorgi, D., y Walker, D. (2003). p51, El cálculo Pi. Cambridge University Press.
7. Boudol, G. (1992). Asincronía y cálculo π . Informe técnico 1702, INRIA, Sophia-Antipolis .
8. Honda, K.; Tokoro, M. (1991). Un cálculo de objetos para comunicación asincrónica. ECOOP 91. Springer Verlag.
9. Palamidessi, Catuscia (1997). "Comparación del poder expresivo del cálculo pi sincrónico y asincrónico". Actas del 24.º Simposio ACM sobre principios de lenguajes de programación : 256-265. arXiv : cs/9809008 . Bibcode :1998cs........9008P.
10. Milner, Robin (1992). "Funciones como procesos" (PDF) . Estructuras matemáticas en informática . 2 (2): 119–141. doi :10.1017/s0960129500001407. hdl : 20.500.11820/159b09c0-1147-4f32-baf0-23bed198f12a . S2CID  : 36446818.
11. Dam, Mads (1997). "Sobre la decidibilidad de equivalencias de procesos para el cálculo pi". Ciencias de la computación teórica . 183 (2): 215–228. doi :10.1016/S0304-3975(96)00325-8.
12. Milner, R.; J. Parrow; D. Walker (1992). "Un cálculo de procesos móviles" (PDF) . Información y Computación . 100 (1): 1–40. doi :10.1016/0890-5401(92)90008-4. hdl : 20.500.11820/cdd6d766-14a5-4c3e-8956-a9792bb2c6d3 .
13. Sangiorgi, D. (1996). "Una teoría de bisimulación para el cálculo π". Acta Informática . 33 : 69–97. doi :10.1007/s002360050036. S2CID  18155730.
14. "BPML | BPEL4WS: Un camino de convergencia hacia una pila BPM estándar". Documento de posición de BPMI.org. 15 de agosto de 2002.
15. Chiarugi, Davide; Pierpaolo Degano; Roberto Marangoni (2007). "Un enfoque computacional para el cribado funcional de genomas". PLOS Computational Biology . 3 (9): 1801–1806. Bibcode :2007PLSCB...3..174C. doi : 10.1371/journal.pcbi.0030174 . PMC 1994977 . PMID  17907794. 
16. Nash, A.; Kalvala, S. (2009). "Una propuesta marco para la localidad celular de Dictyostelium modelada en cálculo π" (PDF) . CoSMoS 2009 .
17. Engberg, U.; Nielsen, M. (1986). "Un cálculo de sistemas de comunicación con paso de etiquetas". Serie de informes DAIMI . 15 (208). doi : 10.7146/dpb.v15i208.7559 .
18. Robin Milner (1993). "Elementos de interacción: conferencia del premio Turing". Commun. ACM . 36 (1): 78–89. doi : 10.1145/151233.151240 .

Referencias

• Milner, Robin (1999). Sistemas comunicantes y móviles: el cálculo π . Cambridge, Reino Unido: Cambridge University Press. ISBN 0-521-65869-1.
• Milner, Robin (1993). "El cálculo π poliádico: un tutorial". En FL Hamer; W. Brauer; H. Schwichtenberg (eds.). Lógica y Álgebra de Especificación . Springer-Verlag.
• Sangiorgi, Davide ; Walker, David (2001). El cálculo π: una teoría de los procesos móviles . Cambridge, Reino Unido: Cambridge University Press. ISBN 0-521-78177-9.