Я понял. Надо просто переместить:

  • феминисток - в Саудовскую Аравию;
  • борцов с изменением климата - в Китай;
  • антивакцинаторов - в Африку;
  • коммунистов, социалистов и прочих леваков - в Россию;
  • мечтающих о возвращении Сталина - в лагеря;
  • борцов за признание Палестины - в Палестину.

А также:

  • обложить стопроцентным налогом на наследство приверженцев этой идеи;
  • посадить за расизм применяющих закон в зависимости от расы нарушителя;
  • отправить в газовую камеру тех, кому наплевать на базовые права человека;
  • снять замки и забрать ключи у борцов за открытые границы;
  • запретить распространять свои гены противникам ГМО;
  • поселить лобковых вшей на лобок защитникам прав животных.

Ну и так далее. Теоремой Геделя навеяло.

https://arxiv.org/abs/1702.06092

Parallel needed reduction for pure interaction nets

Reducing interaction nets without any specific strategy benefits from constant time per step. On the other hand, a canonical reduction step for weak reduction to interface normal form is linear by depth of terms. In this paper, we refine the weak interaction calculus to reveal the actual cost of its reduction. As a result, we obtain a notion of needed reduction that can be implemented in constant time per step without allowing any free ports and without sacrificing parallelism.

The Tonnetz is a lattice diagram representing tonal space. It can be used to visualize harmonic relationships in music. Each node in the diagram corresponds to one of the twelve tones and is connected to six adjacent tones that are related to it by a major third, a minor third, or by a perfect fifth, depending on their relative position in the diagram.

I forked on GitHub the source code of TonnetzViz created by Ondřej Cífka and implemented the following features:

  • zero configuration without any menus;
  • Tonnetz-like keyboard layout;
  • Shepard tones using Web Audio;
  • plug and play Web MIDI support;
  • blue minor and red major triads;
  • Tonnetz bent to represent halftones;
  • Shift key to sustain notes;
  • and arrow keys to transpose.

Now the live version is available at

https://codedot.github.io/tonnetz/

После конференции TERMGRAPH в Эйндховене понял, что хорошо было бы иметь под рукой готовое быстрое введение одновременно в сети взаимодействия и исчисление взаимодействия. Вот что получилось из этой идеи.

Сети взаимодействия (interaction nets) - это структуры, подобные графам, состоящие из агентов (agents) и дуг. Агент типа α

имеет арность ar(α) ≥ 0. Если ar(α) = n, то агент α имеет n дополнительных портов (auxiliary ports) x1,..., xn в дополнение к его главному порту (principle port) x0. Все типы агентов принадлежат множеству Σ, называемому сигнатурой (signature). К любому порту можно присоединить не более одной дуги. Порты, которые не соединены ни одной дугой, называются свободными (free ports). Совокупность всех свободных портов в сети называется ее интерфейсом. Разводка (wiring) ω

состоит исключительно из дуг. Индуктивно определяемые деревья (trees)

соответствуют термам t ::= α(t1,..., tn) | x в исчислении взаимодействия (interaction calculus), где x называется именем (name).

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

что в исчислении взаимодействия будет соответствовать конфигурации (configuration)
<t1,..., tm | v1 = w1,..., vn = wn>,
где ti, vi, wi - некоторые термы. Последовательность t1,..., tm называется интерфейсом (interface), остальное же представляет собой мультимножество уравнений (equations). Разводка ω транслируется в выбор имен, и каждое имя обязано иметь ровно два вхождения в конфигурации.

Как и в λ-исчислении, в исчислении взаимодействия естественным образом определяются понятия α-конверсии и подстановки (substitution). Оба вхождения любого имени могут быть заменены на новое имя, если оно не участвует в данной конфигурации. Если терм t имеет ровно одно вхождение имени x, то подстановка t[x := u] определяется как результат замены имени x в терме t некоторым термом u.

Когда два агента соединены своими главными портами, они формируют активную пару (active pair). Для активных пар можно ввести правила взаимодействия (interaction rules), которые описывают, как активная пара будет заменена во время редукции сети взаимодействия. Графически любое правило взаимодействия можно преставить следующим образом:

где α, β ∈ Σ, а сеть N представлена с помощью разводок и деревьев в виде, пригодном для исчисления взаимодействия: в нотации Lafont это соответствует
a[v1,..., vm] >< β[w1,..., wn].
Говорят, что сеть без активных пар находится в нормальной форме (normal form). Сигнатура и множество правил взаимодействия вместе задают систему взаимодействия (interaction system).

Теперь рассмотрим пример для введенных конструкций, в котором участвуют часто использующиеся агенты ε и δ. В нотации Lafont правила взаимодействия для удаляющего (erasing) агента ε

записываются как ε >< α[ε,..., ε], а правила для дублирующего (duplicating) агента δ

выглядят следующим образом:
δ[α(x1,..., xn), α(y1,..., yn)] >< α[δ(x1, y1),..., δ(xn, yn)].
В качестве примера сети, в которой участвуют правила удаления и дублирования, возьмем простую сеть которая не имеет нормальной формы и редуцируется к самой себе:

В исчислении взаимодействия такая сеть соответствует конфигурации
<∅ | δ(ε, x) = γ(x, ε)> без интерфейса.

Редукция для конфигураций определяется более подробно, чем для сетей. Если
a[v1,..., vm] >< β[w1,..., wn], то следующая редукция:
<... | α(t1,..., tm) = β(u1,..., un), Δ> → <... | t1 = v1,..., tm = vm, u1 = w1,..., un = wn, Δ>
называется взаимодействием (interaction). Когда одно из уравнений имеет форму x = u, к конфигурации применимо разыменование (indirection), в результате которого другое вхождение имени x в некотором терме t будет заменено на терм u:
<...t... | x = u, Δ> → <...t[x := u]... | Δ> или <... | x = u, t = w, Δ> → <... | t[x := u] = w, Δ>.
Уравнение t = x называется тупиком (deadlock), если x имеет вхождение в t. Обычно рассматривают только сети, свободные от тупиков (deadlock-free). Вместе взаимодействие и разыменование задают отношение редукции на конфигурациях. Тот факт, что некоторая конфигурация c редуцируется к своей нормальной форме c', где мультимножество уравнений пусто, обозначают через c ↓ c'.

Если вернуться к примеру незавершающейся редукции сети, то бесконечная редукционная цепочка, начинающаяся с соответствующей конфигурации выглядит следующим образом:
<∅ | δ(ε, x) = γ(x, ε)> →
<∅ | ε = γ(x1, x2), x = γ(y1, y2), x = δ(x1, y1), ε = δ(x2, y2)> →*
<∅ | x1 = ε, x2 = ε, x = γ(y1, y2), x = δ(x1, y1), x2 = ε, y2 = ε> →*
<∅ | δ(ε, x) = γ(x, ε)> → ...

На нашем языке программирования, который подобен yacc(1)/lex(1) по структуре и лексически близок к LaTeX-нотации для исчисления взаимодействия, тот же самый пример можно записать следующим образом:
\epsilon {
        console.log("epsilon >< delta");
} \delta[\epsilon, \epsilon];

\epsilon {
        console.log("epsilon >< gamma");
} \gamma[\epsilon, \epsilon];

\delta[\gamma(x, y), \gamma(v, w)] {
        console.log("delta >< gamma");
} \gamma[\delta(x, v), \delta(y, w)];

$$

\delta(\epsilon, x) = \gamma(x, \epsilon);
Отметим, что наш язык программирования позволяет записывать побочные действия в императивном стиле, таким образом давая возможность исполнять произвольный код, включая ввод-вывод, а также условные множественные правила для пар вида αi >< βj в зависимости от значений i и j, которые могут быть произвольными данными, привязанными к агентам.

Наша реализация этого языка программирования не полагается какую-либо внешнюю сборку мусора, так как не занимается контролем связности сети. Данное свойство является следствием того, что интерфейс сети предполагается пустым, а сети задаются исключительно через мультимножества уравнений. Чтобы записать в нашем языке некоторую сеть с непустым интерфейсом, необходимо сначала ее модифицировать, например, добавив агенты с нулевой арностью ко всем свободным портам.

Сигнатура и арности агентов соответствующей системы взаимодействия автоматически выводятся при компиляции исходного кода программы на основе правил взаимодействия и начальной конфигурации. Правила взаимодействия вместе с их побочными действиями компилируются заранее, до начала редукции сети, при этом компилятор формирует таблицу для быстрого O(1)-поиска правил, соответствующих активным парам, во время последующего исполнения программы. После этого начальная конфигурация добавляется в FIFO-очередь уравнений, которая затем обрабатывается, пока она не станет пуста.

P. S. Недавно адаптировал этот текст и дополнил им статью на Википедии.
In the book "The Optimal Implementation of Functional Programming Languages" by Andrea Asperti and Stefano Guerrini the initial encoding of a λ-term M into an interaction net is a configuration <x | x = [M]0> where translation [M]n is inductively defined by the following rules:



The corresponding interaction rules consist of annihilation:



and propagation:



where i < j.

The problem is that, in case of an arbitrary λK-term, reduction of such an interaction net has to avoid interactions in parts of the net that are disconnected from the interface; otherwise, it may not reach the normal form.

It appears that in order to allow safe reduction without restricting evaluation strategy, it is sufficient to change initial encoding to <x | Eval(x) = [M]0> and β-reduction to @i[x, y] >< λi[Wait(z, Hold(z, x)), y], introducing additional agent types Eval, Wait, Hold, Call and Decide with the following interaction rules:

Eval[λi(x, y)] >< λi[x, Eval(y)];
Eval[δi(x, y)] >< δi[x, y];
Eval[x] >< Wait[Eval(x), Call];
Call >< Hold[x, Eval(x)];
δi[Wait(x, Amb(y, Decide(z, v), v)), Wait(w, y)] >< Wait[δi(x, w), z];
Call >< Decide[Call, ε];
ε >< Decide[x, x];
@i[x, Wait(y, Hold(@i(x, y), Wait(v, w)))] >< Wait[v, w];
α[Wait(x, y)] >< Wait[α(x), y],

where α is a bracket or a croissant, and Amb(x, y, z) is McCarthy's amb, x representing its second principle port.

This token-passing net version of optimal reduction is implemented on the optimal branch of the MLC repository.
Using McCarthy's amb agent:

you can represent copy-on-demand in interaction nets:

with the following interaction rules:
Наконец-то, дошли руки до портирования MLC (Macro Lambda Calculus) и INC (Interaction Nets Compiler) на JavaScript. Транслятор из языка MLC в язык INC получилось сделать на Node.js с помощью Jison довольно быстро. INC все еще есть только в первоначальном виде на Си.

Как только появилась возможность потестировать всю цепочку, выяснилась одна проблема с правилами взаимодействия, которую смог починить следующий патч (соответствующее изменение внесено также в заметку на Scribd):

--- a/template.in
+++ b/template.in
@@ -69,9 +69,13 @@ char *place(char *buf, const char *format, char *str);
        /* Initiate copy of a closed term. */
 } \lambda[\dup(a, c), \dup(b, d)];
 
-\dup[\amb(a, \share(b, c), c), \amb(d, \share(e, f), f)] {
+\dup[a, b] {
+       /* Unshare variable. */
+} \share[\copy(c, \dup(a, b)), c];
+
+\dup[a, b] {
        /* Duplicate sharing. */
-} \share[\dup(b, e), \dup(a, d)];
+} \copy[\dup(\amb(c, \share(a, d), d), \amb(e, \share(b, f), f)), \dup(c, e)];
 
 \dup[\apply(a, b), \apply(c, d)] {
        /* Duplicate application. */

Для наглядности тестовая арифметика в цифрах Черча (Valgrind говорит, что память не течет):

$ cat example.mlc
I = x: x;
K = x, y: x;
S = x, y, z: x z (y z);

T = K;
F = x, y: y;
AND = p, q: p q F;
OR = p, q: p T q;
NOT = p: (a, b: p b a);

C0 = f, x: x;
C1 = f, x: f x;
C2 = f, x: f (f x);
C3 = f, x: f (f (f x));
SUCC = n: (f, x: f (n f x));
PLUS = m, n: (f, x: m f (n f x));
MULT = m, n: (f: m (n f));
EXP = m, n: n m;
PRED = n: (f, x: n (g, h: h (g f)) (K x) I);
MINUS = m, n: n PRED m;
ZERO = n: n (K F) T;

A = self, f: f (self self f);
Y = A A;
FACTR = self, n: (ZERO n) C1 (MULT n (self (PRED n)));
FACT = Y FACTR;

C24 = FACT (PLUS C2 C2);
C27 = EXP C3 C3;
MINUS C27 C24
$ make
        make parsers
        node_modules/.bin/jison mlc.jison
        node_modules/.bin/jison inet.jison
`parsers' is updated.
        make example
        node parse.js example.mlc >example.in
        inc <example.in
        mv in.tab.c example.c
        cc    -o example example.c 
        ./example
v1: v2: v1 (v1 (v1 (v2)))
$ 

Неизвестно, сколько потребуется времени, чтобы проверить корректность системы взаимодействия, так как теперь уже нельзя построить доказательство, просто сославшись на операционную эквивалентность, - слишком стала отличаться полученная система от описанных в литературе.
В связи с идеей распределенных сетей взаимодействия, хотелось бы вернуться к проекту компилятора inet, который используется в MLC для механизма read-back. Приложение было реализовано уже после подготовки формального описания проекта и строго следуя проектной документации; имели место лишь мелкие уточнения и исправления по ходу работы.

Как модифицировать компилятор inet, чтобы получить вместо него распределенную универсальную P2P-сеть взаимодействия? Обозначим гипотетическую распределенную версию inet как p2pinet.

P2P-сеть всегда основана на дублировании информации для случаев, когда одна из нод отключается от сети. Заметим, что стэк активных пар, используемый в проекте inet, - это исчерпывающая информация о редуцируемой сети взаимодействия. Чаще всего (псевдо-)активная пара состоит не из двух агентов, а из агента и (псевдо-)агента wire, который служит для разыменования. Последнее в случае P2P-сети служило бы простым запросом на дублирование информации.

В p2pinet активные пары технически нигде не хранятся в явном виде, и ноды могут даже не знать, активна ли данная конкретная связь между одним идентификатором (портом) и каким-то другим в сети. Обмен информацией и (неявное) создание новых активных пар произходило бы в такой сети с помощью операции разыменования, а собственно применение правил взаимодействия - локально на нодах ввиду нескольких причин.

Во-первых, правила могут быть приватными для группы нод. Во-вторых, правила могут иметь побочные действия, как в проекте inet. В-третьих, набор правил может быть бесконечным и очень сложным. Наконец, одно из правил может быть вычислительно затратно, например вычисление n-ного простого числа.

Следует подчеркнуть, что сами по себе сети взаимодействия неэффективны с вычислительной точки зрения - существующие процессоры справляются с вычислительными задачами несравнимо лучше. Но оптимальная редукция, вопреки названию, вообще не рассматривает вопрос о том, как проводить собственно редукцию и не предлагает никаких решений на этот счет. Вместо этого, она предлагает стратегию для объединения работы (optimal sharing). Последнее и можно было бы позаимствовать от систем взаимодействия для оптимального разделения работы и данных между частями распределенной вычислительной системы.

Конкретно эту задачу сети взаимодействия и решают на качественном уровне. Они служат своеобразным планировщиком задач, который уже, в свою очередь, управляет остальными процессорами как устройствами, чем-то похожим на OpenCL образом. Однако, в отличие от OpenCL (который тоже, в принципе, может быть использован в распределенной сети), сети взаимодействия позволили бы делать и само планирование децентрализованным, при этом избегая лишних обмена данных и дублирования работы.

Наброски )
http://tinyurl.com/q7yhgjq

$ make
iverilog -Wall -DSIM -o comb comb.v
./comb
0381353f9 0 b2e09fd28ea2916f526a8dbb3a92235f0ddb9b0b1ccd0e7d9b5786f91b62031e
0381353fa 1 00000000627d0f02061ce63584c20662272c527d21f17dfaffb20d7de340423d
0381353fb 0 c90dd726ebe7c2770808fe574e85aba7e90ba2aea8998c70bcb24781d4010955
$ 
Кто может скорректировать шестнадцатеричное число?

 A 0 0 B 

Задействуйте свои проверочные колбочки!

Most Popular Tags

Syndicate

RSS Atom

August 2017

S M T W T F S
  12345
6789101112
13141516171819
20212223 2425 26
2728293031  
Powered by Dreamwidth Studios