Interaksjonsnett - Interaction nets

Interaksjonsnett er en grafisk beregningsmodell utarbeidet av Yves Lafont i 1990 som en generalisering av bevisstrukturen til lineær logikk . Et interaksjonsnettsystem er spesifisert av et sett med agenttyper og et sett med interaksjonsregler. Interaksjonsnett er en iboende distribuert beregningsmodell i den forstand at beregninger kan finne sted samtidig i mange deler av et interaksjonsnett, og ingen synkronisering er nødvendig. Sistnevnte er garantert av den sterke sammenløpsegenskapen til reduksjon i denne beregningsmodellen. Således gir interaksjonsnett et naturlig språk for massiv parallellisme. Interaksjonsnett er kjernen i mange implementeringer av lambdakalkulus , som effektiv lukket reduksjon og optimal, i Levys forstand, Lambdascope.

Definisjoner

Interaksjonsnett er graflignende strukturer som består av midler og kanter .

En agent av typen og med arity har en hovedport og hjelpeporter . Enhver port kan kobles til høyst en kant. Porter som ikke er koblet til noen kant kalles gratis porter . Gratis porter danner sammen grensesnittet til et interaksjonsnett. Alle agenttyper tilhører et sett som kalles signatur . ${\ displaystyle \ alpha}$ ${\ displaystyle {\ text {ar}} (\ alpha) = n \ geq 0}$${\ displaystyle n}$ ${\ displaystyle \ Sigma}$

Et interaksjonsnett som utelukkende består av kanter kalles ledninger og betegnes vanligvis som . Et tre med roten er induktivt definert enten som en kant , eller som et middel med sin gratis hovedport og tilhørende porter forbundet med røttene til andre trær . ${\ displaystyle \ omega}$ ${\ displaystyle t}$ ${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle \ alpha}$${\ displaystyle x}$${\ displaystyle x_ {i}}$${\ displaystyle t_ {i}}$

Grafisk kan de primitive strukturene til interaksjonsnett vises som følger:

Når to agenter er koblet til hverandre med sine viktigste porter, danner de et aktivt par . For aktive par kan man innføre interaksjonsregler som beskriver hvordan det aktive paret omskrives til et annet interaksjonsnett. Et interaksjonsnett uten aktive par sies å være i normal form . En signatur (med definert på den) sammen med et sett med interaksjonsregler definert for agenter utgjør sammen et interaksjonssystem . ${\ displaystyle \ Sigma}$${\ displaystyle {\ text {ar}}: \ Sigma \ rightarrow \ mathbb {N}}$${\ displaystyle \ alpha \ in \ Sigma}$

Interaksjonsberegning

Tekstlig representasjon av interaksjonsnett kalles interaksjonsberegning og kan sees på som et programmeringsspråk.

Induktivt definerte trær tilsvarer termer i interaksjonsberegningen, hvor det kalles et navn . ${\ displaystyle t :: = \ alpha (t_ {1}, \ dots, t_ {n}) \ | \ x}$${\ displaystyle x}$

Ethvert interaksjonsnett kan tegnes på nytt ved hjelp av de tidligere definerte ledningene og treprimitivene som følger: ${\ displaystyle N}$

som i samhandlingsregningen tilsvarer en konfigurasjon

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

hvor , og er vilkårlige vilkår. Den ordnede sekvensen på venstre side kalles et grensesnitt , mens høyre side inneholder et uordnet flersett av ligninger . Kabling oversettes til navn, og hvert navn må forekomme nøyaktig to ganger i en konfigurasjon. ${\ displaystyle t_ {i}}$${\ displaystyle v_ {i}}$${\ displaystyle w_ {i}}$${\ displaystyle t_ {1}, ..., t_ {m}}$ ${\ displaystyle v_ {i} = w_ {i}}$${\ displaystyle \ omega}$

Akkurat som i -calculus, har interaksjon calculus forestillingene om- konvertering og substitusjon naturlig definert på konfigurasjoner. Spesielt kan begge forekomster av hvilket som helst navn erstattes med et nytt navn hvis sistnevnte ikke forekommer i en gitt konfigurasjon. Konfigurasjoner anses å være likeverdige opp til -konvertering. I sin tur er erstatning resultatet av å erstatte navnet i et begrep med et annet begrep hvis det har nøyaktig en forekomst i begrepet . ${\ displaystyle \ lambda}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha}$${\ displaystyle t [x: = u]}$${\ displaystyle x}$${\ displaystyle t}$${\ displaystyle u}$${\ displaystyle x}$${\ displaystyle t}$

Enhver interaksjonsregel kan vises grafisk som følger:

hvor , og interaksjonsnettet på høyre side tegnes på nytt ved hjelp av ledninger og treprimitiver for å oversette til interaksjonsberegningen som å bruke Lafonts notasjon. ${\ displaystyle \ alpha, \ beta \ in \ Sigma}$${\ displaystyle N}$${\ displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {n}]}$

Interaksjonsregningen definerer reduksjon på konfigurasjoner i flere detaljer enn sett fra grafomskriving definert på interaksjonsnett. Nemlig hvis , følgende reduksjon: ${\ 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}, \ prikker, u_ {n} = w_ {n}, \ Delta \ rangle}$

kalles interaksjon . Når man av ligningene har form av , indirekte kan brukes som resulterer i substitusjon av den andre forekomsten av navnet på en eller annen term : ${\ 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}$ eller . ${\ displaystyle \ langle {\ vec {t}} \ | \ x = u, t = w, \ Delta \ rangle \ rightarrow \ langle {\ vec {t}} \ | \ t [x: = u] = w , \ Delta \ rangle}$

En ligning kalles en fastlåst tilstand hvis den forekommer i løpet av perioden . Vanligvis vurderes bare låsefrie interaksjonsnett. Sammen definerer interaksjon og indireksjon reduksjonsforholdet på konfigurasjoner. Det faktum at konfigurasjon reduseres til sin normale form uten ligninger igjen, betegnes som . ${\ displaystyle x = t}$${\ displaystyle x}$${\ displaystyle t}$${\ displaystyle c}$ ${\ displaystyle c '}$${\ displaystyle c \ downarrow c '}$

Eiendommer

Interaksjonsnett drar nytte av følgende egenskaper:

• lokalitet (bare aktive par kan skrives om);
• linearitet (hver interaksjonsregel kan brukes i konstant tid);
• sterk sammenløp også kjent som ett-trinns diamanteiendom (hvis og , da og for noen ).${\ displaystyle c \ rightarrow c_ {1}}$${\ displaystyle c \ rightarrow c_ {2}}$${\ displaystyle c_ {1} \ rightarrow c '}$${\ displaystyle c_ {2} \ rightarrow c '}$${\ displaystyle c '}$

Disse egenskapene tillater sammen massiv parallellitet.

Interaksjonskombinatorer

Et av de enkleste interaksjonssystemene som kan simulere ethvert annet interaksjonssystem er interaksjonskombinatorer . Dens signatur er med og . Interaksjonsregler for disse agentene er: ${\ displaystyle \ Sigma = \ {\ epsilon, \ delta, \ gamma \}}$${\ displaystyle {\ text {ar}} (\ epsilon) = 0}$${\ displaystyle {\ text {ar}} (\ delta) = {\ text {ar}} (\ gamma) = 2}$

• ${\ displaystyle \ epsilon \ bowtie \ alpha [\ epsilon, \ prikker, \ epsilon]}$kalt sletting ;
• ${\ displaystyle \ delta [\ alpha (x_ {1}, \ prikker, x_ {n}), \ alpha (y_ {1}, \ prikker, y_ {n})] \ bowtie \ alpha [\ delta (x_ { 1}, y_ {1}), \ prikker, \ delta (x_ {n}, y_ {n})]}$kalt duplisering ;
• ${\ displaystyle \ delta [x, y] \ bowtie \ delta [x, y]}$og kalte utslettelse .${\ displaystyle \ gamma [x, y] \ bowtie \ gamma [y, x]}$

Grafisk kan regler for sletting og duplisering vises som følger:

med et eksempel på et ikke-avsluttende interaksjonsnett som reduserer til seg selv. Den uendelige reduksjonssekvensen starter fra den tilsvarende konfigurasjonen i interaksjonsberegningen som følger:

${\ displaystyle {\ begin {align} & \ 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 {align}}}$

Ikke-deterministisk utvidelse

Interaksjonsnett er egentlig deterministisk og kan ikke modellere ikke-deterministiske beregninger direkte. For å uttrykke ikke-deterministisk valg må interaksjonsnett utvides. Faktisk er det tilstrekkelig å introdusere bare en agent med to hovedporter og følgende interaksjonsregler: ${\ displaystyle {\ text {amb}}}$

Denne fremtredende agent representerer tvetydig valg og kan brukes til å simulere enhver annen agent med vilkårlig antall hovedporter. For eksempel tillater det å definere en boolsk operasjon som returnerer sant hvis noen av argumentene er sanne, uavhengig av beregningen som foregår i de andre argumentene. ${\ displaystyle {\ text {ParallelOr}}}$

Se også

• Interaksjonens geometri
• Omskriving av graf
• Lambda-kalkulator
• Lineær grafgrammatikk
• Lineær logikk
• Bevis nett

Referanser

Videre lesning

• Asperti, Andrea; Guerrini, Stefano (1998). Den optimale implementeringen av funksjonelle programmeringsspråk . Cambridge-traktater i teoretisk informatikk. 45 . Cambridge University Press. ISBN 9780521621120.
• Fernández, Maribel (2009). "Interaksjonsbaserte modeller for beregning". Modeller av beregning: En introduksjon til beregningsteori . Springer Science & Business Media. s. 107–130. ISBN 9781848824348.

Eksterne linker

• de Falco, Marc. "tikz-inet. Et sett med tikz-baserte makroer for å tegne interaksjonsnett" .
• de Falco, Marc. "INL. Interaction Nets Laboratory" .
• Vilaça, Miguel. "INblobs. En redaktør og tolk for Interaction Nets" .
• Asperti, Andrea. "Bologna Optimal High-Order Machine" .
• Salikhmetov, Anton. "JavaScript Engine for Interaction Nets" .
• Salikhmetov, Anton. "Macro Lambda Calculus" .