Redes de interacción

Las redes de interacción son un modelo gráfico de computación ideado por el matemático francés Yves Lafont en 1989 ^{[ 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 computación inherentemente distribuido, en el sentido de que las computaciones pueden tener lugar simultáneamente en muchas partes de una red de interacción, y no se requiere sincronización. Esto último está garantizado por la fuerte propiedad de confluencia de la reducción en este modelo de computación. Por lo tanto, las redes de interacción proporcionan un lenguaje natural para el paralelismo masivo. Las redes de interacción son fundamentales para muchas implementaciones del cálculo lambda , como la reducción cerrada eficiente ^{[ 2 ]} y Lambdascope óptimo, en el sentido de Lévy. ^{[ 3 ]}

Las redes de interacción son estructuras similares a grafos que constan de agentes y aristas .

Un agente de tipo${\displaystyle \alpha }$y con aridad${\displaystyle {\text{ar}}(\alpha )=n\geq 0}$tiene un puerto principal y${\displaystyle n}$Puertos auxiliares . Cualquier puerto puede conectarse a un máximo de una arista. Cualquier arista está conectada a exactamente dos puertos. Los puertos que no están conectados a ninguna arista 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 conjunto.${\displaystyle \Sigma }$llamada firma .

Una red de interacción que consta únicamente de aristas se llama cableado y generalmente se denota como${\displaystyle \omega }$Un árbol${\displaystyle t}$con su raíz${\displaystyle x}$se define inductivamente como un borde${\displaystyle x}$o como agente${\displaystyle \alpha }$con su puerto principal libre${\displaystyle x}$y sus puertos auxiliares${\displaystyle x_{i}}$conectado a las raíces de otros árboles${\displaystyle t_{i}}$.

Gráficamente, las estructuras primitivas de las redes de interacción se pueden representar de la siguiente manera:

Cuando dos agentes se conectan entre sí mediante sus puertos principales, forman un par activo . Para los pares activos se pueden introducir reglas de interacción que describen 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${\displaystyle \Sigma }$(con${\displaystyle {\text{ar}}:\Sigma \rightarrow \mathbb {N} }$definido en él) junto con un conjunto de reglas de interacción definidas para los agentes${\displaystyle \alpha \in \Sigma }$juntos constituyen un sistema de interacción .

La representación textual de las redes de interacción se denomina cálculo de interacción ^{[ 4 ]} y puede considerarse como un lenguaje de programación .

Los árboles definidos inductivamente corresponden a términos${\displaystyle t::=\alpha (t_{1},\dots ,t_{n})\ |\ x}$en el cálculo de interacción, donde${\displaystyle x}$se llama nombre .

Cualquier red de interacción${\displaystyle N}$se puede redibujar utilizando las primitivas de cableado y árbol definidas previamente de la siguiente manera:

que en el cálculo de interacción corresponde a una configuración

${\displaystyle c\equiv \langle t_{1},\dots ,t_{m}\ |\ v_{1}=w_{1},\dots ,v_{n}=w_{n}\rangle }$,

dónde${\displaystyle t_{i}}$,${\displaystyle v_{i}}$, y${\displaystyle w_{i}}$son términos arbitrarios. La secuencia ordenada${\displaystyle t_{1},...,t_{m}}$En el lado izquierdo se denomina interfaz , mientras que el lado derecho contiene un multiconjunto no ordenado de ecuaciones.${\displaystyle v_{i}=w_{i}}$Cableado${\displaystyle \omega }$se traduce en nombres, y cada nombre debe aparecer exactamente dos veces en una configuración.

Igual que en el${\displaystyle \lambda }$-cálculo , el cálculo de interacción tiene las nociones de${\displaystyle \alpha }$-conversión y sustitución definidas naturalmente en configuraciones. Específicamente, ambas ocurrencias de cualquier nombre pueden ser reemplazadas por un nuevo nombre si este último no aparece en una configuración dada. Las configuraciones se consideran equivalentes hasta${\displaystyle \alpha }$-conversión. A su vez, sustitución${\displaystyle t[x:=u]}$es el resultado de reemplazar el nombre${\displaystyle x}$en un término${\displaystyle t}$con otro término${\displaystyle u}$si${\displaystyle x}$tiene exactamente una aparición en el término${\displaystyle t}$.

Cualquier regla de interacción puede representarse gráficamente de la siguiente manera:

dónde${\displaystyle \alpha ,\beta \in \Sigma }$y la red de interacción${\displaystyle N}$en el lado derecho se vuelve a dibujar usando las primitivas de cableado y árbol para traducirlas al cálculo de interacción como${\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]}$utilizando la notación de Lafont.

El cálculo de interacción define la reducción en configuraciones con más detalle que el que se observa en la reescritura de grafos definida en redes de interacción. Es decir, si${\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]}$, la siguiente reducción:

${\displaystyle \langle {\vec {t}}\ |\ \alpha (t_{1},\dots ,t_{m})=\beta (u_{1},\dots ,u_{n}),\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t_{1}=v_{1},\dots ,t_{m}=v_{m},u_{1}=w_{1},\dots ,u_{n}=w_{n},\Delta \rangle }$

se llama interacción . Cuando una de las ecuaciones tiene la forma de${\displaystyle x=u}$, se puede aplicar una indirecta que resulta en la sustitución de la otra ocurrencia del nombre${\displaystyle x}$en algún término${\displaystyle t}$:

${\displaystyle \langle \dots t\dots \ |\ x=u,\Delta \rangle \rightarrow \langle \dots t[x:=u]\dots \ |\ \Delta \rangle }$ o ${\displaystyle \langle {\vec {t}}\ |\ x=u,t=w,\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t[x:=u]=w,\Delta \rangle }$.

Una ecuación${\displaystyle x=t}$se denomina interbloqueo si${\displaystyle x}$tiene ocurrencia en términos${\displaystyle t}$Generalmente, solo se consideran redes de interacción libres de interbloqueos. Juntos, la interacción y la indirección definen la relación de reducción en las configuraciones. El hecho de que la configuración${\displaystyle c}$vuelve a su forma normal${\displaystyle c'}$Sin ecuaciones restantes se denota como${\displaystyle c\downarrow c'}$.

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${\displaystyle c\rightarrow c_{1}}$y${\displaystyle c\rightarrow c_{2}}$, entonces${\displaystyle c_{1}\rightarrow c'}$y${\displaystyle c_{2}\rightarrow c'}$para algunos${\displaystyle c'}$).

Estas propiedades, en conjunto, permiten un paralelismo masivo.

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 . Su firma es${\displaystyle \Sigma =\{\epsilon,\delta,\gamma \}}$con${\displaystyle {\text{ar}}(\epsilon )=0}$y${\displaystyle {\text{ar}}(\delta )={\text{ar}}(\gamma )=2}$. Agente${\displaystyle \epsilon }$puede considerarse como un borrador que elimina recursos;${\displaystyle \delta }$como duplicador;${\displaystyle \gamma }$como constructor, tomando dos recursos y devolviendo un tercero, puede representar cualquier cosa desde operaciones binarias, como suma y multiplicación, hasta la aplicación general de funciones en el cálculo lambda, tomando términos${\displaystyle f}$y${\displaystyle x}$producir${\displaystyle f\,x}$. ^{[ 5 ]} Las reglas de interacción para estos agentes son:

• ${\displaystyle \epsilon \bowtie \alpha [\epsilon ,\dots ,\epsilon ]}$llamado borrado ;
• ${\displaystyle \delta [\alpha (x_{1},\dots ,x_{n}),\alpha (y_{1},\dots ,y_{n})]\bowtie \alpha [\delta (x_{1},y_{1}),\dots ,\delta (x_{n},y_{n})]}$llamada duplicación ;
• ${\displaystyle \delta [x,y]\bowtie \delta [x,y]}$y${\displaystyle \gamma [x,y]\bowtie \gamma [y,x]}$llamada 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, partiendo de la configuración correspondiente en el cálculo de interacción, es la siguiente:

${\displaystyle {\begin{aligned}&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \\&\langle \varnothing \ |\ \epsilon =\gamma (x_{1},x_{2}),\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ \epsilon =\delta (x_{2},y_{2})\rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ x_{1}=\epsilon ,\ x_{2}=\epsilon ,\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ x_{2}=\epsilon ,\ y_{2}=\epsilon \rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \dots \end{aligned}}}$

Las redes de interacción son esencialmente deterministas y no pueden modelar directamente cálculos no deterministas. Para expresar elecciones no deterministas, es necesario extender las redes de interacción. De hecho, basta con introducir un solo agente.${\displaystyle {\text{amb}}}$^{[ 6 ]} con dos puertos principales y las siguientes reglas de interacción:

Este agente distinguido representa una elección ambigua y puede usarse para simular cualquier otro agente con un número arbitrario de puertos principales. Por ejemplo, permite definir un${\displaystyle {\text{ParallelOr}}}$Operación booleana que devuelve verdadero si alguno de sus argumentos es verdadero, independientemente del cálculo que se realice en los demás argumentos.

• Geometría de interacción
• Reescritura de grafos
• Cálculo lambda
• Gramática de grafos lineales
• Lógica lineal
• Red de prueba

• Asperti, Andrea; Guerrini, Stefano (1998). La implementación óptima de lenguajes de programación funcional . Cambridge Tracts in Theoretical Computer Science. Vol.  45. Cambridge University Press. ISBN 9780521621120.
• Fernández, Maribel (2009). «Modelos de computación basados ​​en la interacción». Modelos de computación: Una introducción a la teoría de la computabilidad . Springer Science & Business Media. pp. 107–130 . ISBN  9781848824348.

• 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" . GitHub .
• Salikhmetov, Anton (22 de marzo de 2018). "Motor JavaScript para redes de interacción" .
• Salikhmetov, Anton. "Cálculo macro lambda" .
• Xie, Yuheng. "iNet, un lenguaje y un espacio interactivo para explorar redes de interacción" .