Redes de interacción - Interaction nets

Las redes de interacción son un modelo gráfico de cálculo ideado por Yves Lafont en 1990 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 la reducción cerrada eficiente y la óptima, en el sentido de Lévy, Lambdascope.

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 conjunto llamado firma . ${\ Displaystyle \ alpha}$ ${\ Displaystyle {\ text {ar}} (\ alpha) = n \ geq 0}$${\ Displaystyle n}$ ${\ Displaystyle \ Sigma}$

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

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 ( definida en ella) junto con un conjunto de reglas de interacción definidas para los agentes constituyen un sistema de interacción . ${\ Displaystyle \ Sigma}$${\ Displaystyle {\ text {ar}}: \ Sigma \ rightarrow \ mathbb {N}}$${\ Displaystyle \ alpha \ in \ Sigma}$

Cálculo de interacción

La representación textual de las redes de interacción se denomina cálculo de interacción 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 . ${\ Displaystyle t :: = \ alpha (t_ {1}, \ dots, t_ {n}) \ | \ x}$${\ Displaystyle x}$

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

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

donde , y son términos arbitrarios. La secuencia ordenada en el lado izquierdo se llama interfaz , mientras que el lado derecho contiene un conjunto múltiple de ecuaciones desordenado . El cableado se traduce en nombres, y cada nombre debe aparecer exactamente dos veces en una configuración. ${\ Displaystyle t_ {i}}$${\ Displaystyle v_ {i}}$${\ Displaystyle w_ {i}}$${\ Displaystyle t_ {1}, ..., t_ {m}}$ ${\ Displaystyle v_ {i} = w_ {i}}$${\ Displaystyle \ omega}$

Al igual que en el cálculo de-, 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 la conversión. A su vez, la sustitución es el resultado de reemplazar el nombre en un término con otro término si tiene exactamente una ocurrencia en el término . ${\ Displaystyle \ lambda}$${\ Displaystyle \ alpha}$${\ Displaystyle \ alpha}$${\ Displaystyle t [x: = u]}$${\ Displaystyle x}$${\ Displaystyle t}$${\ Displaystyle u}$${\ Displaystyle x}$${\ Displaystyle t}$

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

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

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: ${\ Displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {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 , se puede aplicar indirección dando como resultado la sustitución de la otra aparición del nombre en algún término : ${\ Displaystyle x = u}$${\ Displaystyle x}$${\ 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 se denomina punto muerto si se produce 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ón se reduzca a su forma normal sin ecuaciones restantes se denota como . ${\ Displaystyle x = t}$${\ Displaystyle x}$${\ Displaystyle t}$${\ Displaystyle c}$ ${\ Displaystyle c '}$${\ Displaystyle c \ flecha hacia abajo c '}$

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);
• una fuerte confluencia también conocida como propiedad de diamante de un paso (si y , entonces y para algunos ).${\ displaystyle c \ rightarrow c_ {1}}$${\ Displaystyle c \ rightarrow c_ {2}}$${\ Displaystyle c_ {1} \ rightarrow c '}$${\ Displaystyle c_ {2} \ rightarrow c '}$${\ Displaystyle c '}$

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 . Su firma está con y . Las reglas de interacción para estos agentes son: ${\ Displaystyle \ Sigma = \ {\ epsilon, \ delta, \ gamma \}}$${\ Displaystyle {\ text {ar}} (\ epsilon) = 0}$${\ Displaystyle {\ text {ar}} (\ delta) = {\ text {ar}} (\ gamma) = 2}$

• ${\ Displaystyle \ epsilon \ bowtie \ alpha [\ epsilon, \ dots, \ epsilon]}$llamado borrar ;
• ${\ Displaystyle \ delta [\ alpha (x_ {1}, \ dots, x_ {n}), \ alpha (y_ {1}, \ dots, y_ {n})] \ bowtie \ alpha [\ delta (x_ { 1}, y_ {1}), \ puntos, \ delta (x_ {n}, y_ {n})]}$llamado duplicación ;
• ${\ Displaystyle \ delta [x, y] \ bowtie \ delta [x, y]}$y llamado aniquilación .${\ Displaystyle \ gamma [x, y] \ bowtie \ gamma [y, x]}$

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:

${\ Displaystyle {\ begin {alineado} & \ 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 {alineado}}}$

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, es suficiente introducir un solo agente con dos puertos principales y las siguientes reglas de interacción: ${\ Displaystyle {\ text {amb}}}$

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 una operación booleana que devuelve verdadero si alguno de sus argumentos es verdadero, independientemente del cálculo que tenga lugar en los otros argumentos. ${\ Displaystyle {\ text {ParallelOr}}}$

Ver también

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

Referencias

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" .