Las redes de interacción son un modelo gráfico de cálculo ideado por Yves Lafont en 1990 [1] como una generalización de las estructuras de prueba de la lógica lineal . Un sistema de red de interacción se especifica mediante un conjunto de tipos de agentes y un conjunto de reglas de interacción. Las redes de interacción son un modelo de cálculo intrínsecamente distribuido en el sentido de que los cálculos pueden tener lugar simultáneamente en muchas partes de una red de interacción y no se necesita sincronización. Esto último está garantizado por la fuerte propiedad de reducción de confluencia en este modelo de cálculo. Por tanto, las redes de interacción proporcionan un lenguaje natural para un paralelismo masivo. Las redes de interacción están en el corazón de muchas implementaciones del cálculo lambda, como reducción cerrada eficiente [2] y óptima, en el sentido de Lévy, Lambdascope. [3]
Definiciones
Las redes de interacciones son estructuras en forma de gráfico que constan de agentes y bordes .
Un agente de tipo y con aridad tiene un puerto principal y puertos auxiliares . Cualquier puerto se puede conectar como máximo a un borde. Los puertos que no están conectados a ningún borde se denominan puertos libres . Los puertos libres juntos forman la interfaz de una red de interacción. Todos los tipos de agentes pertenecen a un conjuntollamado firma .
Una red de interacción que consta únicamente de bordes se llama cableado y generalmente se denota como. Un arbol con su raíz se define inductivamente como un borde , o como agente con su puerto principal libre y sus puertos auxiliares conectado a las raíces de otros árboles .
Gráficamente, las estructuras primitivas de las redes de interacción se pueden representar de la siguiente manera:
Cuando dos agentes están conectados entre sí con sus puertos principales, forman un par activo . Para los pares activos, se pueden introducir reglas de interacción que describan cómo el par activo se reescribe en otra red de interacción. Se dice que una red de interacción sin pares activos está en forma normal . Una firma (con definido en él) junto con un conjunto de reglas de interacción definidas para los agentes juntos constituyen un sistema de interacción .
Cálculo de interacción
La representación textual de las redes de interacción se denomina cálculo de interacción [4] y puede verse como un lenguaje de programación.
Los árboles definidos inductivamente corresponden a términos en el cálculo de interacción, donde se llama un nombre .
Cualquier red de interacción se puede volver a dibujar utilizando las primitivas de árbol y cableado previamente definidas de la siguiente manera:
que en el cálculo de interacción corresponde a una configuración
,
dónde , , y son términos arbitrarios. La secuencia ordenadaen el lado izquierdo se llama interfaz , mientras que el lado derecho contiene un conjunto múltiple desordenado de ecuaciones . Alambrado se traduce en nombres, y cada nombre debe aparecer exactamente dos veces en una configuración.
Como en el -cálculo, el cálculo de interacción tiene las nociones de -conversión y sustitución definidas naturalmente en configuraciones. Específicamente, ambas apariciones de cualquier nombre se pueden reemplazar con un nuevo nombre si este último no ocurre en una configuración dada. Las configuraciones se consideran equivalentes hasta-conversión. A su vez, sustitución es el resultado de reemplazar el nombre en un plazo con otro término Si tiene exactamente una ocurrencia en el término .
Cualquier regla de interacción se puede representar gráficamente de la siguiente manera:
dónde , y la red de interacción en el lado derecho se vuelve a dibujar utilizando las primitivas de cableado y árbol para traducir al cálculo de interacción como usando la notación de Lafont.
El cálculo de interacción define la reducción en configuraciones con más detalles que los que se ven en la reescritura de gráficos definida en redes de interacción. Es decir, si, la siguiente reducción:
se llama interacción . Cuando una de las ecuaciones tiene la forma de, se puede aplicar indirección dando como resultado la sustitución de la otra aparición del nombre en algún término :
o .
Una ecuación se llama un punto muerto si tiene ocurrencia en término . Generalmente, solo se consideran las redes de interacción sin interbloqueo. Juntos, la interacción y la indirección definen la relación de reducción en las configuraciones. El hecho de que la configuraciónse reduce a su forma normal sin ecuaciones restantes se denota como .
Propiedades
Las redes de interacción se benefician de las siguientes propiedades:
- localidad (solo se pueden reescribir los pares activos);
- linealidad (cada regla de interacción se puede aplicar en tiempo constante);
- fuerte confluencia también conocida como propiedad de diamante de un paso (si y , luego y para algunos ).
Estas propiedades juntas permiten un paralelismo masivo.
Combinadores de interacción
Uno de los sistemas de interacción más simples que puede simular cualquier otro sistema de interacción es el de los combinadores de interacción . [5] Su firma es con y . Las reglas de interacción para estos agentes son:
- llamado borrar ;
- llamado duplicación ;
- y llamado aniquilación .
Gráficamente, las reglas de borrado y duplicación se pueden representar de la siguiente manera:
con un ejemplo de una red de interacción no terminante que se reduce a sí misma. Su secuencia de reducción infinita a partir de la configuración correspondiente en el cálculo de interacción es la siguiente:
Extensión no determinista
Las redes de interacción son esencialmente deterministas y no pueden modelar cálculos no deterministas directamente. Para expresar una elección no determinista, es necesario ampliar las redes de interacción. De hecho, basta con introducir un solo agente[6] con dos puertos principales y las siguientes reglas de interacción:
Este agente distinguido representa una elección ambigua y se puede utilizar para simular cualquier otro agente con un número arbitrario de puertos principales. Por ejemplo, permite definir un operación booleana que devuelve verdadero si alguno de sus argumentos es verdadero, independientemente del cálculo que tenga lugar en los otros argumentos.
Ver también
Referencias
- ^ Lafont, Yves (1990). "Redes de interacción". Actas del 17º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM: 95–108. doi : 10.1145 / 96709.96718 . ISBN 0897913434.
- ^ Mackie, Ian (2008). "Una implementación neta de interacción de reducción cerrada". Implementación y aplicación de lenguajes funcionales: 20º Simposio Internacional . Apuntes de conferencias en informática. 5836 : 43–59. doi : 10.1007 / 978-3-642-24452-0_3 . ISBN 978-3-642-24451-3.
- ^ van Oostrom, Vincent; van de Looij, Kees-Jan; Zwitserlood, Marijn (2010). "Lambdascopio: otra implementación óptima del cálculo lambda" (PDF) . Cite journal requiere
|journal=
( ayuda ) - ^ Fernández, Maribel; Mackie, Ian (1999). "Un cálculo para redes de interacción". Principios y práctica de la programación declarativa . Apuntes de conferencias en informática. Saltador. 1702 : 170-187. doi : 10.1007 / 10704567 . ISBN 978-3-540-66540-3.
- ^ Lafont, Yves (1997). "Combinadores de interacción". Información y Computación . Academic Press, Inc. 137 (1): 69–101. doi : 10.1006 / inco.1997.2643 .
- ^ Fernández, Maribel; Khalil, Lionel (2003). "Redes de interacción con Amb de McCarthy: propiedades y aplicaciones" . Revista Nórdica de Computación . 10 (2): 134-162.
Otras lecturas
- Asperti, Andrea; Guerrini, Stefano (1998). La implementación óptima de lenguajes de programación funcionales . Cambridge Tracts en Informática Teórica. 45 . Prensa de la Universidad de Cambridge. ISBN 9780521621120.
- Fernández, Maribel (2009). "Modelos de computación basados en la interacción". Modelos de Computación: Introducción a la Teoría de la Computabilidad . Springer Science & Business Media. págs. 107–130. ISBN 9781848824348.
enlaces externos
- de Falco, Marc. "tikz-inet. Un conjunto de macros basadas en tikz para dibujar redes de interacción" .
- de Falco, Marc. "INL. Laboratorio de Redes de Interacción" .
- Vilaça, Miguel. "INblobs. Editor e intérprete de Interaction Nets" .
- Asperti, Andrea. "La máquina de orden superior óptima de Bolonia" .
- Salikhmetov, Anton. "Motor JavaScript para redes de interacción" .
- Salikhmetov, Anton. "Cálculo Macro Lambda" .