En informática teórica , el cálculo π (o cálculo pi ) es un cálculo de proceso . El cálculo π permite que los nombres de los canales se comuniquen a lo largo de los propios canales, 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 se pueden codificar en el cálculo π , y la codificación enfatiza la naturaleza de diálogo de la computación, estableciendo conexiones con la semántica del juego . Las extensiones del cálculo π , como el cálculo spi y el π 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 las propiedades de la computación concurrente. De hecho, el cálculo π , como el cálculo λ , es tan mínimo que no contiene primitivas como números, valores booleanos, estructuras de datos, variables, funciones o incluso las declaraciones de flujo de control habituales (como if-then-else
, while
).
Construcciones de proceso
En el cálculo de π es fundamental la noción de nombre . La simplicidad del cálculo radica en el doble papel que juegan los nombres como canales y variables de comunicación .
Las construcciones de proceso disponibles en el cálculo son las siguientes [3] (se da una definición precisa en la siguiente sección):
- concurrencia , escrito, dónde y son dos procesos o subprocesos que se ejecutan al mismo tiempo.
- comunicación , donde
- prefijo de entrada es un proceso en espera de un mensaje que se envió en un canal de comunicación llamado antes de proceder 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
c
unagoto c
operación puede usar solo una vez . - prefijo de salida describe que el nombre se emite en el canal antes de proceder como . Normalmente, esto modela el envío de un mensaje en la red o una
goto c
operación.
- prefijo de entrada es un proceso en espera de un mensaje que se envió en un canal de comunicación llamado antes de proceder 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
- replicación , escrito, que puede verse como un proceso que siempre puede crear una nueva copia de . Normalmente, esto modela un servicio de red o una etiqueta en
c
espera de cualquier número degoto c
operaciones. - 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 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 , es un proceso cuya ejecución está completa y se ha detenido.
Aunque el minimalismo del cálculo π nos impide escribir programas en el sentido normal, es fácil ampliar el cálculo. En particular, es fácil definir tanto estructuras de control como recursividad, bucles y composición secuencial 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 distribución o la criptografía de clave pública. El aplicada π -calculus debido a Abadi y Fournet [1] poner estas varias extensiones sobre una base formal, al extender el π -calculus 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 es conocido por los dos primeros componentes.
Los dos primeros componentes pueden comunicarse en el canal x , y el nombre y se vincula a z . Por tanto, el siguiente paso del proceso es
Tenga en cuenta que la y restante no se ve afectada porque está definida en un ámbito interno. El segundo y tercer componentes paralelos ahora pueden comunicarse en el nombre del canal z , y el nombre v se vincula ax . El siguiente paso en el proceso es ahora
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. 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
Definicion formal
Sintaxis
Sea Χ un conjunto de objetos llamados nombres . La sintaxis abstracta para el π -calculus se construye de la siguiente gramática BNF (donde x y y son los nombres de Χ): [4]
En la sintaxis concreta siguiente, los prefijos se unen más estrechamente que la composición paralela (|), y se utilizan paréntesis para eliminar la ambigüedad.
Los nombres están sujetos a las construcciones de prefijo de entrada y restricción. Formalmente, el conjunto de nombres libres de un proceso en el cálculo π se definen inductivamente mediante la tabla siguiente. El conjunto de nombres ligados de un proceso se define como los nombres de un proceso que no están en el conjunto de nombres libres.
Construir | Nombres libres |
---|---|
Ninguno | |
a ; x ; todos los nombres libres de P | |
a ; nombres libres de P excepto x | |
Todos los nombres libres de P y Q | |
Nombres libres de P excepto x | |
Todos los nombres libres de P |
Congruencia estructural
Tanto para la semántica de reducción como para la semántica de transición etiquetada es fundamental la noción de congruencia estructural . Dos procesos son estructuralmente congruentes, si son idénticos hasta la 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 :
- Si se puede obtener de cambiando el nombre de uno o más nombres enlazados en .
Axiomas de composición paralela :
Axiomas de restricción :
Axioma para la replicación :
Axioma que relaciona restricción y paralelo :
- si x no es un nombre libre de.
Este último axioma se conoce como axioma de "extensión del alcance". Este axioma es central, ya que describe cómo un nombre ligado x puede ser extruido por una acción de salida, haciendo que se extienda el alcance de x . En los casos en que x es un nombre libre de, la conversión alfa se puede utilizar para permitir que la extensión continúe.
Semántica de reducción
Nosotros escribimos Si puede 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.
La principal regla de reducción que captura la capacidad de los procesos para comunicarse a través de canales es la siguiente:
- dónde denota el proceso en el que el nombre libre ha sido sustituida por las apariciones gratuitas de . Si una ocurrencia libre de ocurre en un lugar donde no sería gratuito, es posible que se requiera una conversión alfa.
Hay tres reglas adicionales:
- Si Después también .
- Esta regla dice que la composición paralela no inhibe el cálculo.
- Si , Después también .
- Esta regla asegura que el cálculo pueda realizarse bajo una restricción.
- Si y y , Después también .
La última regla establece que los procesos que son estructuralmente congruentes tienen las mismas reducciones.
El ejemplo revisado
Considere nuevamente el proceso
Aplicando la definición de la semántica de reducción, obtenemos la reducción
Observe cómo, aplicando el axioma de sustitución de reducción, ocurrencias libres de ahora están etiquetados como .
A continuación, obtenemos la reducción.
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 fue capturado usando el axioma de extensión del alcance.
A continuación, utilizando el axioma de sustitución de reducción, obtenemos
Finalmente, usando los axiomas para la composición y restricción paralelas, obtenemos
Semántica etiquetada
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 de comunicación ).
En esta semántica, una transición de un estado a algún otro estado después de una acción se anota como:
Donde estados y representar procesos y es una acción de entrada , una acción de salida , o una acción silenciosa τ . [5]
Un resultado estándar sobre la semántica etiquetada es que está de acuerdo con la semántica de reducción en el sentido de que si y solo si para alguna acción [ cita requerida ] .
Extensiones y variantes
La sintaxis dada arriba es mínima. Sin embargo, la sintaxis puede modificarse de varias formas.
Un operador de elección no determinista se puede agregar a la sintaxis.
Una prueba de igualdad de nombres se puede agregar a la sintaxis. Este operador de coincidencia puede proceder comosi y solo si x yson el mismo nombre. De manera similar, se puede agregar un operador de desajuste para la desigualdad de nombres . Los programas prácticos que pueden pasar nombres (URL o punteros) a menudo utilizan dicha funcionalidad: para modelar directamente dicha funcionalidad dentro del cálculo, esta y las extensiones relacionadas suelen ser útiles.
El asíncrono π -calculus [6] [7] permite sólo salidas sin sufijo, es decir, átomos de salida de la forma, produciendo un cálculo más pequeño. Sin embargo, cualquier proceso en el cálculo original puede ser representado por el cálculo π asincrónico más pequeño usando un canal adicional para simular el reconocimiento explícito del proceso de recepción. 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 expresivo de comunicación asincrónica 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 descuidada se convertiría en una reservada; 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). [8]
El poliádico π -calculus permite la comunicación de más de un nombre en una sola acción: (salida poliadica) y (entrada poliadica) . 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 los múltiples argumentos se pasan en secuencia. La codificación se define de forma recursiva por las cláusulas
está codificado como
está codificado como
Todas las demás construcciones del proceso no se modifican con la codificación.
En lo anterior, denota la codificación de todos los prefijos en la continuación del mismo modo.
Todo el poder de la replicación no es necesario. A menudo, uno solo considera la entrada replicada , cuyo axioma de congruencia estructural es .
Proceso de entrada replicado como pueden entenderse como servidores, esperando en el canal x para ser invocados por los clientes. La invocación de un servidor genera una nueva copia del proceso, donde a es el nombre pasado por el cliente al servidor, durante la invocación de este último.
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 clave para el caso de orden superior es
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 se puede simular simplemente pasando un nombre que apunte a P en su lugar.
Propiedades
Completitud de Turing
El cálculo π es un modelo universal de cálculo . Esto se observó por primera vez por Milner en sus "Funciones como procesos" de papel, [9] en el que presenta dos codificaciones del lambda-cálculo en el π -calculus. 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 ambos, la idea crucial es el modelado de las vinculaciones del entorno, por ejemplo, " x está vinculado a un término"- como agentes de replicación que responden a las solicitudes de sus enlaces devolviendo una conexión al término .
Las características del cálculo π que hacen posibles estas codificaciones son el paso de nombres y la replicación (o, de manera equivalente, agentes definidos de forma recursiva). En ausencia de replicación / recursión, el cálculo π deja de ser poderoso de Turing . Esto puede verse por el hecho de que la equivalencia de bisimulación se vuelve decidible para el cálculo sin recursividad e incluso para el cálculo π de control finito, donde el número de componentes paralelos en cualquier proceso está limitado por una constante. [10]
Bisimulaciones en el cálculo π
En cuanto a los cálculos de proceso, el cálculo π permite una definición de 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.
Hay (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, dejamos y denotar procesos y denotar relaciones binarias sobre procesos.
Bisimilaridad temprana y tardía
La bisimilitud temprana y tardía fueron formuladas por Milner, Parrow y Walker en su artículo original sobre el cálculo π . [11]
Una relación binaria sobre procesos es una bisimulación temprana si para cada par de procesos,
- cuando sea luego por cada nombre existe algo tal que y ;
- para cualquier acción que no sea de entrada , Si entonces existe algo tal que y ;
- y requisitos simétricos con y intercambiado.
Procesos y se dice que son bisimilares tempranos, escritos si el par para una bisimulación temprana .
En bisimilaridad tardía, la coincidencia de transición debe ser independiente del nombre que se transmite. Una relación binariasobre procesos es una bisimulación tardía si para cada par de procesos,
- cuando sea entonces para algunos sostiene eso y para cada nombre y ;
- para cualquier acción que no sea de entrada , Si implica que existe alguna tal que y ;
- y requisitos simétricos con y intercambiado.
Procesos y se dice que son tardíos bisimilares, escritos si el par para una bisimulación tardía .
Ambas cosas y sufren el problema de que no son relaciones de congruencia en el sentido de que no son preservadas por todos los constructos del proceso. Más precisamente, existen procesos y tal 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.
Bisimilaridad abierta
Afortunadamente, es posible una tercera definición, que evita este problema, a saber, la de bisimilaridad abierta , debida a Sangiorgi. [12]
Una relación binaria sobre procesos es una bisimulación abierta si para cada par de elementos y por cada sustitución de nombre y cada acción , cuando sea entonces existe algo tal que y .
Procesos y se dice que son bisimilares abiertos, escritos si el par para una bisimulación abierta .
La bisimilaridad temprana, tardía y abierta son distintas
La bisimilitud temprana, tardía y abierta son distintas. Las contención son adecuadas, por lo que.
En ciertos subcálculos, como el cálculo pi asincrónico, se sabe que coinciden la bisimilitud tardía, temprana y abierta. Sin embargo, en este contexto, una noción más apropiada es la de bisimilaridad 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 están indexados por relaciones de distinción; los detalles se encuentran en el artículo de Sangiorgi citado anteriormente.
Equivalencia de púas
Alternativamente, se puede definir la equivalencia de bisimulación directamente a partir de la semántica de reducción. Nosotros escribimos si proceso permite inmediatamente una entrada o una salida en el nombre .
Una relación binaria sobre procesos es una bisimulación de púas si es una relación simétrica que satisface que para cada par de elementos tenemos eso
- (1) si y solo si por cada nombre
y
- (2) por cada reducción existe una reduccion
tal que .
Nosotros decimos eso y son bisimilares con púas si existe una bisimulación con púas dónde .
Definiendo un contexto como un término π con un agujero [] decimos que dos procesos P y Q son congruentes con púas , escritos, si para cada contexto tenemos eso y son bisimilares de púas. Resulta que la congruencia de púas coincide con la congruencia inducida por la bisimilitud temprana.
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 spi-cálculo amplía el cálculo π con primitivas para el cifrado y el descifrado. En 2001, Martin Abadi y Cedric Fournet generalizaron el manejo de protocolos criptográficos para producir el cálculo π aplicado . En la actualidad, existe una gran cantidad de trabajo dedicado a las variantes del cálculo π aplicado , que incluye una serie de herramientas de verificación experimentales. 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 los sistemas de tipos que pueden comprobar 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 convertiría en una herramienta de descripción para modelar procesos comerciales. Para julio de 2006, hay una discusión en la comunidad sobre cuán útil sería esto. Más recientemente, el cálculo π ha formado la base teórica del lenguaje de modelado de procesos de negocio (BPML) y del XLANG de Microsoft. [13]
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 llamada cascada RTK / MAPK ) y en particular el "lego" molecular que implementa estas tareas de comunicación en una extensión del cálculo π . [2] Siguiendo este artículo fundamental, otros autores describieron toda la red metabólica de una célula mínima. [14] 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 . [15]
Historia
El cálculo π fue desarrollado originalmente por Robin Milner , Joachim Parrow y David Walker en 1992, basado en ideas de Uffe Engberg y Mogens Nielsen. [16] 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. [17]
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 )
- RhoLang
Notas
- ^ Especificación de OMG (2011). "Business Process Model and Notation (BPMN) Versión 2.0" , Grupo de Gestión de Objetos . p.21
- ^ a b Regev, Aviv ; William Silverman; Ehud Y. Shapiro (2001). "Representación y simulación de procesos bioquímicos utilizando el álgebra de procesos pi-Cálculo". Simposio del Pacífico sobre biocomputación : 459–470.
- ^ Wing, Jeannette M. (27 de diciembre de 2002). "Preguntas frecuentes sobre π-Cálculo" (PDF) .
- ^ A Calculus of Mobile Processes 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
- ^ Robin Milner, Comunicación y sistemas móviles: el cálculo de Pi, Cambridge University Press, ISBN 0521643201 . 1999
- ^ Boudol, G. (1992). Asincronía y cálculo π . Informe técnico 1702, INRIA, Sophia-Antipolis .
- ^ Honda, K .; Tokoro, M. (1991). Un cálculo de objetos para la comunicación asincrónica. ECOOP 91 . Springer Verlag.
- ^ Palamidessi, Catuscia (1997). "Comparando el poder expresivo del síncrono y el asíncrono pi-cálculo". Actas del 24º Simposio de ACM sobre principios de lenguajes de programación : 256–265. arXiv : cs / 9809008 . Código Bibliográfico : 1998cs ........ 9008P .
- ^ Milner, Robin (1992). "Funciones como procesos" (PDF) . Estructuras matemáticas en informática . 2 (2): 119-141. doi : 10.1017 / s0960129500001407 .
- ^ Dam, Mads (1997). "Sobre la decidibilidad de las equivalencias de proceso para el pi-cálculo". Informática Teórica . 183 (2): 215-228. doi : 10.1016 / S0304-3975 (96) 00325-8 .
- ^ 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 .
- ^ Sangiorgi, D. (1996). "Una teoría de bisimulación para el cálculo π". Acta Informatica . 33 : 69–97. doi : 10.1007 / s002360050036 .
- ^ "BPML | BPEL4WS: Un camino de convergencia hacia una pila de BPM estándar". Documento de posición de BPMI.org. 15 de agosto de 2002.
- ^ Chiarugi, Davide; Pierpaolo Degano; Roberto Marangoni (2007). "Un enfoque computacional para el cribado funcional de genomas" . PLOS Biología Computacional . 3 (9): 1801–1806. doi : 10.1371 / journal.pcbi.0030174 . PMC 1994977 . PMID 17907794 .
- ^ Nash, A .; Kalvala, S. (2009). "Una propuesta de marco para la localidad celular de Dictyostelium modelado en π-Calculus" (PDF) . CoSMoS 2009 .
- ^ 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 .
- ^ Robin Milner (1993). "Elementos de interacción: conferencia premio Turing" . Comun. ACM . 36 (1): 78–89. doi : 10.1145 / 151233.151240 .
Referencias
- Milner, Robin (1999). Sistemas móviles y de comunicación: el cálculo π . Cambridge, Reino Unido: Cambridge University Press. ISBN 0-521-65869-1.
- Milner, Robin (1993). "El π-cálculo políado: 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.
enlaces externos
- PiCalculus en el wiki de C2
- Preguntas frecuentes sobre π-Calculus por Jeannette M. Wing