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

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

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

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

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

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

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

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

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

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

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

Любую сеть взаимодействия можно перерисовать с использованием ранее определенных примитивов проводки и дерева следующим образом: ${\ displaystyle N}$

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

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

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

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

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

где , а сеть взаимодействия с правой стороны перерисовывается с использованием примитивов проводки и дерева для преобразования в исчисление взаимодействий с использованием нотации Лафонта. ${\ Displaystyle \ альфа, \ бета \ в \ Sigma}$ ${\ displaystyle 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}}$

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

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

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

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

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

^ Лафон, Ив (1990). «Сети взаимодействия». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . ACM: 95–108. DOI : 10.1145 / 96709.96718 . ISBN 0897913434.
Перейти ↑ Mackie, Ian (2008). "Реализация сети взаимодействия закрытого сокращения". Реализация и применение функциональных языков: 20-й международный симпозиум . Конспект лекций по информатике. 5836 : 43–59. DOI : 10.1007 / 978-3-642-24452-0_3 . ISBN 978-3-642-24451-3.
^ ван Остром, Винсент; ван де Лой, Кеес-Ян; Zwitserlood, Marijn (2010). «Лямбдаскоп: еще одна оптимальная реализация лямбда-исчисления» (PDF) . Cite journal requires |journal= (help)
^ Фернандес, Марибель; Маки, Ян (1999). «Расчет для сетей взаимодействия». Принципы и практика декларативного программирования . Конспект лекций по информатике. Springer. 1702 : 170–187. DOI : 10.1007 / 10704567 . ISBN 978-3-540-66540-3.
^ Лафон, Ив (1997). «Комбинаторы взаимодействия». Информация и вычисления . Academic Press, Inc. 137 (1): 69–101. DOI : 10.1006 / inco.1997.2643 .
^ Фернандес, Марибель; Халил, Лайонел (2003). "Сети взаимодействия с послом Маккарти: свойства и приложения" . Северный журнал вычислительной техники . 10 (2): 134–162.

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

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

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

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

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

[2] Перейти ↑ Mackie, Ian (2008). "Реализация сети взаимодействия закрытого сокращения". Реализация и применение функциональных языков: 20-й международный симпозиум . Конспект лекций по информатике. 5836 : 43–59. DOI : 10.1007 / 978-3-642-24452-0_3 . ISBN 978-3-642-24451-3.

[3] ван Остром, Винсент; ван де Лой, Кеес-Ян; Zwitserlood, Marijn (2010). «Лямбдаскоп: еще одна оптимальная реализация лямбда-исчисления» (PDF) . Cite journal requires |journal= (help)

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

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

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

[1]