Сети взаимодействия

Сети взаимодействия — это графическая модель вычислений, разработанная французским математиком Ивом Лафоном в 1990 году. ^[1] как обобщение структур доказательства линейной логики . Система сети взаимодействия определяется набором типов агентов и набором правил взаимодействия. Сети взаимодействия — это по своей сути распределенная модель вычислений в том смысле, что вычисления могут происходить одновременно во многих частях сети взаимодействия, и синхронизация не требуется. Последнее гарантируется свойством сильной конфлюэнтности редукции в этой модели вычислений. Таким образом, сети взаимодействия обеспечивают естественный язык для массового параллелизма. Сети взаимодействия лежат в основе многих реализаций лямбда-исчисления , таких как эффективная закрытая редукция. ^[2] и оптимальный, по Леви, лямбдаскоп. ^[3]

Определения [ править ]

Сети взаимодействий представляют собой графоподобные структуры, состоящие из агентов и ребер .

Агент типа $\alpha$ и с арностью ${\text{ar}}(\alpha )=n\geq 0$ имеет один главный порт и $n$ вспомогательные порты . Любой порт может быть подключен не более чем к одному краю. Порты, не подключенные ни к одному краю, называются свободными портами . Свободные порты вместе образуют интерфейс сети взаимодействия. Все типы агентов принадлежат множеству $\Sigma$ называется подпись .

Сеть взаимодействия, состоящая исключительно из ребер, называется вайрингом и обычно обозначается как $\omega$ . Дерево $t$ с его корнем $x$ индуктивно определяется либо как ребро $x$ или в качестве агента $\alpha$ со своим свободным основным портом $x$ и его вспомогательные порты $x_{i}$ связан с корнями других деревьев $t_{i}$ .

Графически примитивные структуры сетей взаимодействия можно представить следующим образом:

Когда два агента соединены друг с другом своими основными портами, они образуют активную пару . Дляактивных пар можно ввести правила взаимодействия , описывающие, как активная пара перезаписывается в другое взаимодействие.сеть. Говорят, что сеть взаимодействия без активных пар находится в нормальной форме . Подпись $\Sigma$ (с ${\text{ar}}:\Sigma \rightarrow \mathbb {N}$ определенные на нем) вместе с набором правил взаимодействия, определенных для агентов $\alpha \in \Sigma$ вместе составляют систему взаимодействия .

Исчисление взаимодействия [ править ]

Текстовое представление сетей взаимодействия называется исчислением взаимодействия. ^[4] и его можно рассматривать как язык программирования.

Индуктивно определенные деревья соответствуют термам $t::=\alpha (t_{1},\dots ,t_{n})\ |\ x$ в исчислении взаимодействия, где $x$ называется именем .

Любая сеть взаимодействия $N$ можно перерисовать, используя ранее определенные соединения и примитивы дерева следующим образом:

что в исчислении взаимодействия соответствует конфигурации

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

где $t_{i}$ , $v_{i}$ , и $w_{i}$ являются произвольными терминами. Упорядоченная последовательность $t_{1},...,t_{m}$ в левой части называется интерфейсом , а в правой части содержится неупорядоченный мультимножество уравнений $v_{i}=w_{i}$ . Электропроводка $\omega$ преобразуется в имена, и каждое имя должно встречаться в конфигурации ровно два раза.

Точно так же, как в $\lambda$ -исчисление, исчисление взаимодействия имеет понятия $\alpha$ -преобразование и замена, естественно определенные в конфигурациях. В частности, оба вхождения любого имени можно заменить нановое имя, если последнее не встречается в данной конфигурации. Конфигурации считаются эквивалентными до $\alpha$ -конверсия. В свою очередь, замена $t[x:=u]$ является результатом замены имени $x$ в срок $t$ с другим термином $u$ если $x$ имеет ровно одно вхождение в термин $t$ .

Любое правило взаимодействия можно графически представить следующим образом:

где $\alpha ,\beta \in \Sigma$ , и сеть взаимодействия $N$ в правой части перерисовывается с использованием связок и примитивов дерева, чтобы преобразовать в исчисление взаимодействия как $\alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]$ используя обозначения Лафона.

Исчисление взаимодействия определяет сокращение конфигураций более подробно, чем видно из графика.перезапись, определенная в сетях взаимодействия. А именно, если $\alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]$ , следующее сокращение:

$\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$

называется взаимодействием . Когда одно из уравнений имеет вид $x=u$ , косвенность можно применить , в результатевместо другого появления имени $x$ в какой-то срок $t$ :

$\langle \dots t\dots \ |\ x=u,\Delta \rangle \rightarrow \langle \dots t[x:=u]\dots \ |\ \Delta \rangle$ или $\langle {\vec {t}}\ |\ x=u,t=w,\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t[x:=u]=w,\Delta \rangle$ .

Уравнение $x=t$ называется тупиком , если $x$ имеет место в сроке $t$ . Обычно рассматриваются только сети взаимодействия без тупиков. Вместе взаимодействие и косвенность определяют отношение редукции конфигураций. Тот факт, что конфигурация $c$ приводит к нормальной форме $c'$ без оставшихся уравнений обозначается как $c\downarrow c'$ .

Свойства [ править ]

Сети взаимодействия выигрывают от следующих свойств:

локальность (переписывать можно только активные пары);
линейность (каждое правило взаимодействия может применяться в постоянное время);
сильное слияние, также известное как свойство одношагового ромба (если $c\rightarrow c_{1}$ и $c\rightarrow c_{2}$ , затем $c_{1}\rightarrow c'$ и $c_{2}\rightarrow c'$ для некоторых $c'$ ).

Вместе эти свойства обеспечивают массовый параллелизм.

Комбинаторы взаимодействия [ править ]

Одной из простейших систем взаимодействия, которая может имитировать любую другую систему взаимодействия, является комбинатор взаимодействия . ^[5] Его подпись $\Sigma =\{\epsilon ,\delta ,\gamma \}$ с ${\text{ar}}(\epsilon )=0$ и ${\text{ar}}(\delta )={\text{ar}}(\gamma )=2$ . Правила взаимодействия этих агентов таковы:

$\epsilon \bowtie \alpha [\epsilon ,\dots ,\epsilon ]$ называется стиранием ;
$\delta [\alpha (x_{1},\dots ,x_{n}),\alpha (y_{1},\dots ,y_{n})]\bowtie \alpha [\delta (x_{1},y_{1}),\dots ,\delta (x_{n},y_{n})]$ называется дублированием ;
$\delta [x,y]\bowtie \delta [x,y]$ и $\gamma [x,y]\bowtie \gamma [y,x]$ называется уничтожением .

Графически правила стирания и дублирования можно представить следующим образом:

с примером незавершающейся сети взаимодействия, сводящейся к самой себе. Последовательность его бесконечной редукции, начиная с соответствующей конфигурации в исчислении взаимодействия, выглядит следующим образом:

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

Недетерминированное расширение [ править ]

Сети взаимодействия по существу детерминированы и не могут напрямую моделировать недетерминированные вычисления. Чтобы выразить недетерминированный выбор, необходимо расширить сети взаимодействия. Фактически достаточно ввести всего лишь одного агента ${\text{amb}}$ ^[6] с двумя основными портами и следующими правилами взаимодействия:

Этот выдающийся агент представляет собой неоднозначный выбор и может использоваться для моделирования любого другого агента с произвольным количеством основных портов. Например, он позволяет определить ${\text{ParallelOr}}$ логическая операция, которая возвращает значение true, если какой-либо из ее аргументов имеет значение true, независимо от вычислений, происходящих в других аргументах.

См. также [ править ]

Ссылки [ править ]

^ Лафон, Ив (1990). «Сети взаимодействия». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . АКМ. стр. 95–108. дои : 10.1145/96709.96718 . ISBN 0897913434 . S2CID 1165803 .
^ Маки, Ян (2008). «Сетевая реализация закрытой редукции». Реализация и применение функциональных языков: 20-й международный симпозиум . Конспекты лекций по информатике. 5836 : 43–59. дои : 10.1007/978-3-642-24452-0_3 . ISBN 978-3-642-24451-3 .
^ ван Остром, Винсент; ван де Лоой, Кес-Ян; Цвицерлоод, Марин (2010). «Лямбдаскоп: еще одна оптимальная реализация лямбда-исчисления» (PDF) . Архивировано из оригинала (PDF) 6 июля 2017 г. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )
^ Фернандес, Марибель; Маки, Ян (1999). «Исчисление сетей взаимодействия». Принципы и практика декларативного программирования . Конспекты лекций по информатике. 1702 . Спрингер: 170–187. дои : 10.1007/10704567 . ISBN 978-3-540-66540-3 . S2CID 19458687 .
^ Лафон, Ив (1997). «Комбинаторы взаимодействия» . Информация и вычисления . 137 (1). Академик Пресс, Инк.: 69–101. дои : 10.1006/inco.1997.2643 .
^ Фернандес, Марибель; Халил, Лайонел (2003). «Сети взаимодействия с Amb Маккарти: свойства и приложения» . Северный журнал вычислительной техники . 10 (2): 134–162.

Дальнейшее чтение [ править ]

Асперти, Андреа; Геррини, Стефано (1998). Оптимальная реализация языков функционального программирования . Кембриджские трактаты по теоретической информатике. Том. 45. Издательство Кембриджского университета. ISBN 9780521621120 .
Фернандес, Марибель (2009). «Модели вычислений, основанные на взаимодействии». Модели вычислений: введение в теорию вычислимости . Springer Science & Business Media. стр. 107–130. ISBN 9781848824348 .

Внешние ссылки [ править ]

де Фалько, Марк. "tikz-inet. Набор макросов на основе tikz для рисования сетей взаимодействия" .
де Фалько, Марк. «ИНЛ. Лаборатория сетей взаимодействия» .
Виласа, Мигель. «INblobs. Редактор и интерпретатор Interaction Nets» .
Асперти, Андреа. «Болонская оптимальная машина высшего порядка» . Гитхаб .
Салихметов Антон. «JavaScript Engine для сетей взаимодействия» .
Салихметов Антон. «Макролямбда-исчисление» .
Се, Юхэн. «iNet, языковая и интерактивная площадка для изучения сетей взаимодействия» .

[1] Лафон, Ив (1990). «Сети взаимодействия». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . АКМ. стр. 95–108. дои : 10.1145/96709.96718 . ISBN 0897913434 . S2CID 1165803 .

[2] Маки, Ян (2008). «Сетевая реализация закрытой редукции». Реализация и применение функциональных языков: 20-й международный симпозиум . Конспекты лекций по информатике. 5836 : 43–59. дои : 10.1007/978-3-642-24452-0_3 . ISBN 978-3-642-24451-3 .

[3] ван Остром, Винсент; ван де Лоой, Кес-Ян; Цвицерлоод, Марин (2010). «Лямбдаскоп: еще одна оптимальная реализация лямбда-исчисления» (PDF) . Архивировано из оригинала (PDF) 6 июля 2017 г. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[4] Фернандес, Марибель; Маки, Ян (1999). «Исчисление сетей взаимодействия». Принципы и практика декларативного программирования . Конспекты лекций по информатике. 1702 . Спрингер: 170–187. дои : 10.1007/10704567 . ISBN 978-3-540-66540-3 . S2CID 19458687 .

[5] Лафон, Ив (1997). «Комбинаторы взаимодействия» . Информация и вычисления . 137 (1). Академик Пресс, Инк.: 69–101. дои : 10.1006/inco.1997.2643 .

[6] Фернандес, Марибель; Халил, Лайонел (2003). «Сети взаимодействия с Amb Маккарти: свойства и приложения» . Северный журнал вычислительной техники . 10 (2): 134–162.

[1]

[2]

[3]

[4]

[5]

[6]