Interactie netten - Interaction nets

Interactienetten zijn een grafisch rekenmodel dat in 1990 door Yves Lafont is bedacht als een veralgemening van de bewijsstructuren van lineaire logica . Een interactienetsysteem wordt gespecificeerd door een reeks agenttypen en een reeks interactieregels. Interactienetten zijn een inherent gedistribueerd rekenmodel in die zin dat berekeningen gelijktijdig kunnen plaatsvinden in vele delen van een interactienet en dat er geen synchronisatie nodig is. Dit laatste wordt gegarandeerd door de sterke samenvloeiingseigenschap van reductie in dit berekeningsmodel. Zo bieden interactienetten een natuurlijke taal voor massaal parallellisme. Interactienetten vormen de kern van veel implementaties van de lambda-calculus , zoals efficiënte gesloten reductie en optimale, in de zin van Lévy, Lambdascope.

definities

Interactienetten zijn grafiekachtige structuren die bestaan ​​uit agenten en randen .

Een middel van het type met ariteit één belangrijkste haven en extra poorten . Elke poort kan op maximaal één rand worden aangesloten. Poorten die op geen enkele edge zijn aangesloten, worden vrije poorten genoemd . Vrije poorten vormen samen de interface van een interactienet. Alle agenttypen behoren tot een set met de naam handtekening . ${\displaystyle \alpha}$ ${\displaystyle {\text{ar}}(\alpha)=n\geq 0}$${\displaystyle n}$ ${\displaystyle \Sigma}$

Een interactienet dat uitsluitend uit randen bestaat, wordt een bedrading genoemd en wordt meestal aangeduid als . Een boom met zijn wortel wordt inductief gedefinieerd als een rand , of als een agent met zijn vrije hoofdpoort en zijn hulppoorten die zijn verbonden met de wortels van andere bomen . ${\displaystyle \omega}$ ${\displaystyle t}$ ${\displaystyle x}$${\displaystyle x}$${\displaystyle \alpha}$${\displaystyle x}$${\displaystyle x_{i}}$${\displaystyle t_{i}}$

Grafisch kunnen de primitieve structuren van interactienetten als volgt worden weergegeven:

Wanneer twee agenten met hun hoofdpoorten met elkaar zijn verbonden, vormen ze een actief paar . Voor actieve paren kan men interactieregels introduceren die beschrijven hoe het actieve paar herschrijft naar een ander interactienet. Van een interactienet zonder actieve paren wordt gezegd dat het de normale vorm heeft . Een handtekening (met daarop gedefinieerd) samen met een reeks interactieregels die voor agenten zijn gedefinieerd, vormen samen een interactiesysteem . ${\displaystyle \Sigma}$${\displaystyle {\text{ar}}:\Sigma \rightarrow \mathbb {N} }$${\ Displaystyle \ alpha \ in \ Sigma }$

Interactieberekening

Tekstuele representatie van interactienetten wordt de interactierekening genoemd en kan worden gezien als een programmeertaal.

Inductief gedefinieerde bomen komen overeen met termen in de interactierekening, waar een naam wordt genoemd . ${\displaystyle t::=\alpha (t_{1},\dots ,t_{n})\ |\ x}$${\displaystyle x}$

Elk interactienet kan als volgt opnieuw worden getekend met behulp van de eerder gedefinieerde bedrading en boomprimitieven: ${\displaystyle N}$

die in de interactierekening overeenkomt met een configuratie

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

waarbij , , en willekeurige termen zijn. De geordende reeks aan de linkerkant wordt een interface genoemd , terwijl de rechterkant een ongeordende multiset vergelijkingen bevat . Bedrading vertaalt zich naar namen, en elke naam moet precies twee keer voorkomen in een configuratie. ${\displaystyle t_{i}}$${\displaystyle v_{i}}$${\displaystyle w_{i}}$${\displaystyle t_{1},...,t_{m}}$ ${\displaystyle v_{i}=w_{i}}$${\displaystyle \omega}$

Net als in de -calculus, heeft de interactiecalculus de noties van -conversie en substitutie die van nature gedefinieerd zijn op configuraties. In het bijzonder kunnen beide exemplaren van een naam worden vervangen door een nieuwe naam als de laatste niet voorkomt in een bepaalde configuratie. Configuraties worden als equivalent beschouwd tot -conversie. Substitutie is op zijn beurt het resultaat van het vervangen van de naam in een term door een andere term als deze precies één keer voorkomt in de term . ${\displaystyle \lambda}$${\displaystyle \alpha}$${\displaystyle \alpha}$${\displaystyle t[x:=u]}$${\displaystyle x}$${\displaystyle t}$${\displaystyle u}$${\displaystyle x}$${\displaystyle t}$

Elke interactieregel kan als volgt grafisch worden weergegeven:

waarbij , en het interactienet aan de rechterkant opnieuw wordt getekend met behulp van de bedrading en boomprimitieven om te vertalen naar de interactierekening met behulp van de notatie van Lafont. ${\ Displaystyle \ alpha , \ beta \ in \ Sigma }$${\displaystyle N}$${\ Displaystyle \ alpha [v_ {1}, \ stippen , v_ {m}] \ vlinderdas \ beta [w_ {1}, \ stippen , w_ {n}]}$

De interactieberekening definieert reductie op configuraties in meer details dan blijkt uit het herschrijven van grafieken die zijn gedefinieerd op interactienetten. Namelijk, als , de volgende vermindering: ${\ Displaystyle \ alpha [v_ {1}, \ stippen , v_ {m}] \ vlinderdas \ beta [w_ {1}, \ stippen , 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 }$

heet interactie . Wanneer een van de vergelijkingen de vorm heeft van , kan indirectheid worden toegepast, wat resulteert in vervanging van het andere voorkomen van de naam in een term : ${\displaystyle x=u}$${\displaystyle x}$${\displaystyle t}$

${\ Displaystyle \ langle \ stippen t \ stippen \ | \ x = u, \ Delta \ rangle \ rechtspijl \ langle \ stippen t [x: = u] \ stippen \ | \ \ Delta \ rangle}$ of . ${\displaystyle \langle {\vec {t}}\ |\ x=u,t=w,\delta \rangle \rightarrow \langle {\vec {t}}\ |\ t[x:=u]=w ,\Delta \rangle }$

Een vergelijking wordt een deadlock genoemd als deze voorkomt in term . Over het algemeen worden alleen impassevrije interactienetten overwogen. Samen bepalen interactie en indirectheid de reductierelatie op configuraties. Het feit dat de configuratie wordt teruggebracht tot zijn normaalvorm zonder vergelijkingen meer, wordt aangeduid als . ${\displaystyle x=t}$${\displaystyle x}$${\displaystyle t}$${\displaystyle c}$ ${\displaystyle c'}$${\displaystyle c\downarrow c'}$

Eigendommen

Interactienetten profiteren van de volgende eigenschappen:

• plaats (alleen actieve paren kunnen worden herschreven);
• lineariteit (elke interactieregel kan in constante tijd worden toegepast);
• sterke samenvloeiing ook bekend als eenstaps diamanteigenschap (als en , dan en voor sommigen ).${\displaystyle c\rightarrow c_{1}}$${\displaystyle c\rightarrow c_{2}}$${\displaystyle c_{1}\rightarrow c'}$${\displaystyle c_{2}\rightarrow c'}$${\displaystyle c'}$

Deze eigenschappen samen maken een enorm parallellisme mogelijk.

Interactie combinators

Een van de eenvoudigste interactiesystemen die elk ander interactiesysteem kan simuleren, is dat van interactiecombinaties . De handtekening is met en . Interactieregels voor deze agenten zijn: ${\ Displaystyle \ Sigma =\ {\ epsilon , \ delta , \ gamma \}}$${\displaystyle {\text{ar}}(\epsilon)=0}$${\displaystyle {\text{ar}}(\delta )={\text{ar}}(\gamma )=2}$

• ${\ Displaystyle \ epsilon \ vlinderdas \ alpha [\ epsilon, \ stippen, \ epsilon]}$genaamd wissen ;
• ${\displaystyle \delta [\alpha (x_{1},\dots,x_{n}),\alpha (y_{1},\dots,y_{n})]\strikje \alpha [\delta (x_{ 1},y_{1}),\dots ,\delta (x_{n},y_{n})]}$genaamd dubbel ;
• ${\ Displaystyle \ delta [x, y] \ vlinderdas \ delta [x, y]}$en riep vernietiging .${\ Displaystyle \ gamma [x, y] \ vlinderdas \ gamma [y, x]}$

Grafisch kunnen de wis- en duplicatieregels als volgt worden weergegeven:

met een voorbeeld van een niet-beëindigend interactienet dat tot zichzelf reduceert. De oneindige reductiereeks vanaf de overeenkomstige configuratie in de interactierekening is als volgt:

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

Niet-deterministische extensie

Interactienetten zijn in wezen deterministisch en kunnen niet-deterministische berekeningen niet rechtstreeks modelleren. Om niet-deterministische keuze tot uitdrukking te brengen, moeten interactienetten worden uitgebreid. In feite is het voldoende om slechts één agent met twee hoofdpoorten en de volgende interactieregels te introduceren : ${\displaystyle {\text{amb}}}$

Deze onderscheiden agent vertegenwoordigt een ambigue keuze en kan worden gebruikt om elke andere agent met een willekeurig aantal hoofdpoorten te simuleren. Het maakt het bijvoorbeeld mogelijk om een booleaanse bewerking te definiëren die true retourneert als een van zijn argumenten waar is, onafhankelijk van de berekening die in de andere argumenten plaatsvindt. ${\displaystyle {\text{ParallelOf}}}$

Zie ook

• Geometrie van interactie
• Grafiek herschrijven
• Lambda-calculus
• Lineaire grafiekgrammatica
• Lineaire logica
• Proefnet

Referenties

Verder lezen

• Asperti, Andrea; Guerrini, Stefano (1998). De optimale implementatie van functionele programmeertalen . Cambridge Tracts in theoretische informatica. 45 . Cambridge University Press. ISBN 9780521621120.
• Fernandez, Maribel (2009). "Op interactie gebaseerde modellen van berekening". Berekeningsmodellen: een inleiding tot de berekenbaarheidstheorie . Springer Wetenschap en zakelijke media. blz. 107-130. ISBN 9781848824348.

Externe links

• de Falco, Marc. "tikz-inet. Een set op tikz gebaseerde macro's voor het tekenen van interactienetten" .
• de Falco, Marc. "INL. Interaction Nets Laboratory" .
• Vilaca, Miguel. "INblobs. Een redacteur en tolk voor Interaction Nets" .
• Asperti, Andrea. "De optimale machine van een hogere orde in Bologna" .
• Salikhmetov, Anton. "JavaScript-engine voor interactienetwerken" .
• Salikhmetov, Anton. "Macro Lambda-calculus" .