Interakční sítě - Interaction nets

Interakční sítě jsou grafický model výpočtu, který navrhl Yves Lafont v roce 1990 jako zobecnění důkazních struktur lineární logiky . Systém interakční sítě je určen sadou typů agentů a sadou pravidel interakce. Interakční sítě jsou inherentně distribuovaným modelem výpočtu v tom smyslu, že výpočty mohou probíhat současně v mnoha částech interakční sítě a není nutná žádná synchronizace. Ten je v tomto modelu výpočtu zaručen silnou konfluenční vlastností redukce. Interakční sítě tak poskytují přirozený jazyk pro masivní paralelismus. Interakční sítě jsou jádrem mnoha implementací lambda kalkulu , jako je efektivní uzavřená redukce a optimální, v Lévyho smyslu, Lambdascope.

Definice

Sítě interakcí jsou struktury podobné grafům skládající se z agentů a hran .

Agent typu a s arity má jeden hlavní port a pomocné porty . K nejvýše jedné hraně lze připojit jakýkoli port. Porty, které nejsou připojeny k žádné hraně, se nazývají volné porty . Volné porty společně tvoří rozhraní interakční sítě. Všechny typy agentů patří do sady zvané podpis . ${\ displaystyle \ alpha}$ ${\ displaystyle {\ text {ar}} (\ alpha) = n \ geq 0}$${\ displaystyle n}$ ${\ displaystyle \ Sigma}$

Interakční síť, která se skládá pouze z hran, se nazývá kabeláž a obvykle se označuje jako . Strom s kořenem je indukčně definována buď jako hrana , nebo jako činidlo svým volným hlavním portem a jeho pomocných porty připojené ke kořenům jiných stromů . ${\ displaystyle \ omega}$ ${\ displaystyle t}$ ${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle \ alpha}$${\ displaystyle x}$${\ displaystyle x_ {i}}$${\ displaystyle t_ {i}}$

Graficky lze primitivní struktury interakčních sítí reprezentovat následovně:

Když jsou dva agenti navzájem propojeni svými hlavními porty, tvoří aktivní pár . Pro aktivní páry lze zavést pravidla interakce, která popisují, jak se aktivní pár přepisuje do jiné interakční sítě. Interakční síť bez aktivních párů se říká, že je v normální formě . Podpis (s ním definovaným) spolu se sadou pravidel interakce definovaných pro agenty společně tvoří systém interakce . ${\ displaystyle \ Sigma}$${\ displaystyle {\ text {ar}}: \ Sigma \ rightarrow \ mathbb {N}}$${\ displaystyle \ alpha \ in \ Sigma}$

Interakční kalkul

Textová reprezentace interakčních sítí se nazývá interakční kalkul a lze ji považovat za programovací jazyk.

Induktivně definované stromy odpovídají výrazům v interakčním kalkulu, kde se nazývá jméno . ${\ displaystyle t :: = \ alpha (t_ {1}, \ tečky, t_ {n}) \ | \ x}$${\ displaystyle x}$

Libovolnou interakční síť lze překreslit pomocí dříve definovaných zapojení a stromových primitiv takto: ${\ displaystyle N}$

který v interakčním kalkulu odpovídá konfiguraci

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

kde , a jsou libovolné výrazy. Uspořádaná sekvence na levé straně se nazývá rozhraní , zatímco pravá strana obsahuje neuspořádanou multiset rovnic . Zapojení se překládá na jména a každé jméno se musí v konfiguraci vyskytnout přesně dvakrát. ${\ displaystyle t_ {i}}$${\ displaystyle v_ {i}}$${\ displaystyle w_ {i}}$${\ displaystyle t_ {1}, ..., t_ {m}}$ ${\ displaystyle v_ {i} = w_ {i}}$${\ displaystyle \ omega}$

Stejně jako v -calculus má interakční kalkul pojmy -konverze a substituce přirozeně definované v konfiguracích. Konkrétně lze oba výskyty libovolného názvu nahradit novým názvem, pokud se v dané konfiguraci nevyskytuje. Konfigurace jsou považovány za ekvivalentní až do -konverze. Substituce je zase výsledkem nahrazení jména v termínu jiným termínem, pokud má v termínu přesně jeden výskyt . ${\ displaystyle \ lambda}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha}$${\ displaystyle t [x: = u]}$${\ displaystyle x}$${\ displaystyle t}$${\ displaystyle u}$${\ displaystyle x}$${\ displaystyle t}$

Libovolné pravidlo interakce lze graficky znázornit takto:

kde a interakční síť na pravé straně je překreslena pomocí kabeláže a stromových primitiv, aby se promítla do interakčního kalkulu jako Lafontova notace. ${\ displaystyle \ alpha, \ beta \ in \ Sigma}$${\ displaystyle N}$${\ displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {n}]}$

Interakční kalkul definuje redukci na konfiguracích podrobněji, než je vidět z přepisování grafů definovaného na interakčních sítích. Jmenovitě, pokud , následující redukce: ${\ displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {n}]}$

${\ displaystyle \ langle {\ vec {t}} \ | \ \ alfa (t_ {1}, \ tečky, t_ {m}) = \ beta (u_ {1}, \ tečky, 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 nazývá interakce . Pokud má jedna z rovnic formu , lze použít indirection, což má za následek nahrazení jiného výskytu jména v určitém termínu : ${\ displaystyle x = u}$${\ displaystyle x}$${\ displaystyle t}$

${\ Displaystyle \ langle \ tečky t \ tečky \ | \ x = u, \ Delta \ rangle \ rightarrow \ langle \ dots t [x: = u] \ dots \ | \ \ Delta \ rangle}$ nebo . ${\ displaystyle \ langle {\ vec {t}} \ | \ x = u, t = w, \ Delta \ rangle \ rightarrow \ langle {\ vec {t}} \ | \ t [x: = u] = w , \ Delta \ rangle}$

Rovnice se nazývá zablokování, pokud se vyskytne v termínu . Obecně se berou v úvahu pouze interakční sítě bez zablokování. Společně interakce a indirection definují redukční vztah na konfiguracích. Skutečnost, že konfigurace klesá do své normální podoby, aniž by zbyly rovnice, se označuje jako . ${\ displaystyle x = t}$${\ displaystyle x}$${\ displaystyle t}$${\ displaystyle c}$ ${\ displaystyle c '}$${\ displaystyle c \ downarrow c '}$

Vlastnosti

Interakční sítě těží z následujících vlastností:

• lokalita (lze přepsat pouze aktivní páry);
• linearita (každé pravidlo interakce lze použít v konstantním čase);
• silný soutok známý také jako jednokroková diamantová vlastnost (pokud a poté a pro některé ).${\ displaystyle c \ rightarrow c_ {1}}$${\ displaystyle c \ rightarrow c_ {2}}$${\ displaystyle c_ {1} \ rightarrow c '}$${\ displaystyle c_ {2} \ rightarrow c '}$${\ displaystyle c '}$

Tyto vlastnosti společně umožňují masivní paralelismus.

Interakční kombinátory

Jedním z nejjednodušších interakčních systémů, který dokáže simulovat jakýkoli jiný interakční systém, je systém kombinátorů interakcí . Jeho podpis je s a . Pravidla interakce pro tyto agenty jsou: ${\ displaystyle \ Sigma = \ {\ epsilon, \ delta, \ gama \}}$${\ displaystyle {\ text {ar}} (\ epsilon) = 0}$${\ displaystyle {\ text {ar}} (\ delta) = {\ text {ar}} (\ gamma) = 2}$

• ${\ displaystyle \ epsilon \ motýlek \ alpha [\ epsilon, \ tečky, \ epsilon]}$nazývá mazání ;
• ${\ displaystyle \ delta [\ alpha (x_ {1}, \ dots, x_ {n}), \ alpha (y_ {1}, \ dots, y_ {n})] \ bowtie \ alpha [\ delta (x_ { 1}, y_ {1}), \ tečky, \ delta (x_ {n}, y_ {n})]}$nazývá se duplikace ;
• ${\ displaystyle \ delta [x, y] \ motýlek \ delta [x, y]}$a volal zničení .${\ displaystyle \ gamma [x, y] \ motýlek \ gamma [y, x]}$

Graficky lze pravidla mazání a duplikace znázornit takto:

s příkladem nekončící interakční sítě, která se redukuje sama na sebe. Jeho nekonečná redukční sekvence vycházející z odpovídající konfigurace v interakčním kalkulu je následující:

${\ displaystyle {\ begin {zarovnaný} & \ 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 {zarovnáno}}}$

Nedeterministické rozšíření

Interakční sítě jsou v podstatě deterministické a nemohou přímo modelovat nedeterministické výpočty. Aby bylo možné vyjádřit nedeterministickou volbu, je třeba rozšířit interakční sítě. Ve skutečnosti stačí zavést pouze jednoho agenta se dvěma hlavními porty a následujícími pravidly interakce: ${\ displaystyle {\ text {amb}}}$

Tento rozlišující agent představuje nejednoznačnou volbu a lze jej použít k simulaci jakéhokoli jiného agenta s libovolným počtem hlavních portů. Například umožňuje definovat booleovskou operaci, která vrací true, pokud je některý z jejích argumentů pravdivý, nezávisle na výpočtu probíhajícím v ostatních argumentech. ${\ displaystyle {\ text {ParallelOr}}}$

Viz také

• Geometrie interakce
• Přepisování grafů
• Lambda kalkul
• Gramatika lineárního grafu
• Lineární logika
• Kontrolní síť

Reference

Další čtení

• Asperti, Andrea; Guerrini, Stefano (1998). Optimální implementace funkčních programovacích jazyků . Cambridge Tracts v teoretické informatice. 45 . Cambridge University Press. ISBN 9780521621120.
• Fernández, Maribel (2009). "Interakční modely výpočtu". Modely výpočtu: Úvod do teorie vypočítatelnosti . Springer Science & Business Media. 107–130. ISBN 9781848824348.

externí odkazy

• de Falco, Marc. "tikz-inet. Sada maker založených na tikz pro kreslení interakčních sítí" .
• de Falco, Marc. "INL. Laboratoř interakčních sítí" .
• Vilaça, Miguel. "INblobs. Editor a interpret pro Interaction Nets" .
• Asperti, Andrea. „Boloňský optimální stroj vyšších řádů“ .
• Salikhmetov, Anton. "JavaScriptový modul pro interakční sítě" .
• Salikhmetov, Anton. "Makro lambda kalkul" .