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

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

Определения

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

Агент типа и с арностью имеет один главный порт и вспомогательные порты . Любой порт может быть подключен не более чем к одному краю. Порты, не подключенные ни к одному из ребер, называются свободными портами . Бесплатные порты вместе образуют интерфейс сети взаимодействия. Все типы агентов принадлежат к набору, называемому сигнатурой . ${\ 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}$

Исчисление взаимодействий

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

Индуктивно определенные деревья соответствуют терминам в исчислении взаимодействий, где называется именем . ${\ 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}$${\ displaystyle \ alpha [v_ {1}, \ dots, v_ {m}] \ bowtie \ beta [w_ {1}, \ dots, w_ {n}]}$

Исчисление взаимодействий определяет сокращение конфигураций более подробно, чем это видно из переписывания графа, определенного для сетей взаимодействия. А именно, если , следующее сокращение: ${\ 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}), \ Дельта \ rangle \ rightarrow \ langle {\ vec {t}} \ | \ t_ {1} = v_ {1}, \ dots, t_ {m} = v_ {m}, u_ {1} = w_ {1}, \ точки, u_ {n} = w_ {n}, \ Delta \ rangle}$

называется взаимодействием . Когда одно из уравнений имеет форму , может применяться косвенное обращение, приводящее к замене другого вхождения имени в некоторый термин : ${\ 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}$ или . ${\ displaystyle \ langle {\ vec {t}} \ | \ x = u, t = w, \ Delta \ rangle \ rightarrow \ langle {\ vec {t}} \ | \ t [x: = u] = w , \ Delta \ rangle}$

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

Характеристики

Сети взаимодействия обладают следующими свойствами:

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

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

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

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

• ${\ displaystyle \ epsilon \ bowtie \ alpha [\ epsilon, \ dots, \ epsilon]}$называется стиранием ;
• ${\ displaystyle \ 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})]}$называется дублированием ;
• ${\ Displaystyle \ дельта [х, у] \ галстук-бабочка \ дельта [х, у]}$и называется аннигиляцией .${\ Displaystyle \ гамма [х, у] \ галстук-бабочка \ гамма [у, х]}$

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

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

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

Недетерминированное расширение

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

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

Смотрите также

• Геометрия взаимодействия
• Переписывание графа
• Лямбда-исчисление
• Грамматика линейного графа
• Линейная логика
• Доказательство сети

Рекомендации

дальнейшее чтение

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

Внешние ссылки

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