Interaktionsnet - Interaction nets

Interaktionsnet er en grafisk beregningsmodel, der blev udtænkt af Yves Lafont i 1990 som en generalisering af bevisstrukturer for lineær logik . Et interaktionsnet-system er specificeret af et sæt agenttyper og et sæt interaktionsregler. Interaktionsnet er en iboende distribueret beregningsmodel i den forstand, at beregninger kan finde sted samtidigt i mange dele af et interaktionsnet, og der er ikke behov for synkronisering. Sidstnævnte er garanteret af den stærke sammenløbsegenskab ved reduktion i denne beregningsmodel. Således giver interaktionsnet et naturligt sprog for massiv parallelisme. Interaktionsnet er kernen i mange implementeringer af lambda-beregningen , såsom effektiv lukket reduktion og optimal i Levys forstand, Lambdascope.

Definitioner

Interaktionsnet er graflignende strukturer bestående af agenser og kanter .

Et middel af typen og med arity har en vigtigste havn og hjælpestoffer havne . Enhver port kan tilsluttes højst den ene kant. Porte, der ikke er forbundet med nogen kant, kaldes fri porte . Gratis porte danner sammen grænsefladen til et interaktionsnet. Alle agenttyper hører til et sæt kaldet signatur . ${\ displaystyle \ alpha}$ ${\ displaystyle {\ text {ar}} (\ alpha) = n \ geq 0}$ ${\ displaystyle n}$ ${\ displaystyle \ Sigma}$

Et interaktionsnet, der udelukkende består af kanter, kaldes ledninger og betegnes normalt som . Et træ med sin rod defineres induktivt enten som en kant eller som et middel med dets frie hovedport og dets hjælpeporte forbundet med rødderne til andre træer . ${\ displaystyle \ omega}$ ${\ displaystyle t}$ ${\ displaystyle x}$ ${\ displaystyle x}$ ${\ displaystyle \ alpha}$ ${\ displaystyle x}$ ${\ displaystyle x_ {i}}$ ${\ displaystyle t_ {i}}$

Grafisk kan de primitive strukturer for interaktionsnet repræsenteres som følger:

Når to agenter er forbundet til hinanden med deres vigtigste porte, danner de et aktivt par . For aktive par kan man indføre interaktionsregler, der beskriver, hvordan det aktive par omskriver til et andet interaktionsnet. Et interaktionsnet uden aktive par siges at være i normal form . En signatur (med defineret på den) sammen med et sæt interaktionsregler defineret for agenter udgør sammen et interaktionssystem . ${\ displaystyle \ Sigma}$ ${\ displaystyle {\ text {ar}}: \ Sigma \ rightarrow \ mathbb {N}}$ ${\ displaystyle \ alpha \ in \ Sigma}$

Interaktionsberegning

Tekstlig repræsentation af interaktionsnet kaldes interaktionsberegning og kan ses som et programmeringssprog.

Induktivt definerede træer svarer til udtryk i interaktionsberegningen, hvor kaldes et navn . ${\ displaystyle t :: = \ alpha (t_ {1}, \ dots, t_ {n}) \ | \ x}$ ${\ displaystyle x}$

Ethvert interaktionsnet kan tegnes igen ved hjælp af de tidligere definerede ledninger og træprimitiver som følger: ${\ displaystyle N}$

som i interaktionsberegningen svarer til en konfiguration

${\ 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 rækkefølge i venstre side kaldes en grænseflade , mens den højre side indeholder et uordnet flersæt af ligninger . Ledningsføring oversættes til navne, og hvert navn skal forekomme nøjagtigt to gange i en konfiguration. ${\ displaystyle t_ {i}}$ ${\ displaystyle v_ {i}}$ ${\ displaystyle w_ {i}}$ ${\ displaystyle t_ {1}, ..., t_ {m}}$ ${\ displaystyle v_ {i} = w_ {i}}$ ${\ displaystyle \ omega}$

Ligesom i -calculus har interaktionsberegningen begreberne -conversion og substitution, der er naturligt defineret i konfigurationer. Specifikt kan begge forekomster af ethvert navn erstattes med et nyt navn, hvis sidstnævnte ikke forekommer i en given konfiguration. Konfigurationer betragtes som ækvivalente op til -konvertering. Til gengæld er erstatning resultatet af at erstatte navnet i et udtryk med et andet udtryk, hvis det har nøjagtigt en forekomst i udtrykket . ${\ displaystyle \ lambda}$ ${\ displaystyle \ alpha}$ ${\ displaystyle \ alpha}$ ${\ displaystyle t [x: = u]}$ ${\ displaystyle x}$ ${\ displaystyle t}$ ${\ displaystyle u}$ ${\ displaystyle x}$ ${\ displaystyle t}$

Enhver interaktionsregel kan vises grafisk som følger:

hvor og interaktionsnet på højre side tegnes om ved hjælp af ledninger og træprimitiver for at oversætte til interaktionsberegningen som ved hjælp af Lafont's notation. ${\ displaystyle \ alpha, \ beta \ in \ Sigma}$ ${\ displaystyle N}$ ${\ displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {n}]}$

Interaktionsberegningen definerer reduktion på konfigurationer i flere detaljer end set fra grafomskrivning defineret på interaktionsnet. Nemlig hvis , følgende reduktion: ${\ 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}$

kaldes interaktion . Når en af ligningerne har form af , kan indirektion anvendes, hvilket resulterer i erstatning af den anden forekomst af navnet på et eller andet tidspunkt : ${\ 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 kaldes en blindlås, hvis den forekommer i løbet . Generelt tages kun deadlock-fri interaktionsnet i betragtning. Sammen definerer interaktion og indirektion reduktionsforholdet på konfigurationer. Det faktum, at konfiguration reduceres til sin normale form uden ligninger tilbage, betegnes som . ${\ displaystyle x = t}$ ${\ displaystyle x}$ ${\ displaystyle t}$ ${\ displaystyle c}$ ${\ displaystyle c '}$ ${\ displaystyle c \ downarrow c '}$

Ejendomme

Interaktionsnet drager fordel af følgende egenskaber:

lokalitet (kun aktive par kan omskrives);
linearitet (hver interaktionsregel kan anvendes i konstant tid);
stærk sammenløb også kendt som et-trins diamantegenskab (hvis og , så og for nogle ). ${\ displaystyle c \ rightarrow c_ {1}}$ ${\ displaystyle c \ rightarrow c_ {2}}$ ${\ displaystyle c_ {1} \ rightarrow c '}$ ${\ displaystyle c_ {2} \ rightarrow c '}$ ${\ displaystyle c '}$

Disse egenskaber tillader sammen massiv parallelitet.

Interaktionskombinationer

Et af de enkleste interaktionssystemer, der kan simulere ethvert andet interaktionssystem, er interaktionskombinatorer . Dens underskrift er med og . Interaktionsregler for disse agenter 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]}$ kaldes sletning ;
${\ 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})]}$ kaldet duplikering ;
${\ displaystyle \ delta [x, y] \ bowtie \ delta [x, y]}$ og kaldes tilintetgørelse . ${\ displaystyle \ gamma [x, y] \ bowtie \ gamma [y, x]}$

Grafisk kan reglerne for sletning og duplikering repræsenteres som følger:

med et eksempel på et ikke-afsluttende interaktionsnet, der reducerer til sig selv. Dens uendelige reduktionssekvens startende fra den tilsvarende konfiguration i interaktionsberegningen er 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 udvidelse

Interaktionsnet er i det væsentlige deterministiske og kan ikke modellere ikke-deterministiske beregninger direkte. For at udtrykke ikke-deterministisk valg skal interaktionsnet udvides. Faktisk er det tilstrækkeligt at introducere kun en agent med to hovedporte og følgende interaktionsregler: ${\ displaystyle {\ text {amb}}}$

Denne fremtrædende agent repræsenterer tvetydigt valg og kan bruges til at simulere enhver anden agent med vilkårligt antal hovedporte. For eksempel tillader det at definere en boolsk operation, der returnerer sand, hvis et af dens argumenter er sandt, uafhængigt af beregningen, der finder sted i de andre argumenter. ${\ displaystyle {\ text {ParallelOr}}}$

Se også

Referencer

Yderligere læsning

Asperti, Andrea; Guerrini, Stefano (1998). Den optimale implementering af funktionelle programmeringssprog . Cambridge-traktater i teoretisk datalogi. 45 . Cambridge University Press. ISBN 9780521621120.
Fernández, Maribel (2009). "Interaktionsbaserede modeller for beregning". Modeller af beregning: En introduktion til teori om beregning . Springer Science & Business Media. s. 107–130. ISBN 9781848824348.

eksterne links

de Falco, Marc. "tikz-inet. Et sæt tikz-baserede makroer til tegning af interaktionsnet" .
de Falco, Marc. "INL. Interaktionsnetlaboratorium" .
Vilaça, Miguel. "INblobs. En redaktør og tolk for interaktionsnet" .
Asperti, Andrea. "Bologna Optimal High-Order Machine" .
Salikhmetov, Anton. "JavaScript-motor til interaktionsnet" .
Salikhmetov, Anton. "Makrolambda-beregning" .

Languages

In other projects