http://pubs.opengroup.org/onlinepubs/9699919799/

Только что опубликовали IEEE 1003.1-2008+TC1+TC2.

В список участников TC2 мое имя попало в связи с багами 735-737 против TC1:

https://codedot.dreamwidth.org/166992.html

Теперь грамматика языка Shell не содержит shift/reduce-конфликтов (можно засунуть ее в yacc(1) и убедиться, раньше было пять конфликтов), лишена двух лишних правил, а также корректно описывает произвольное количество команд в скриптах.
http://dx.doi.org/10.4204/EPTCS.225.7

Token-passing Optimal Reduction with Embedded Read-back
Anton Salikhmetov

We introduce a new interaction net implementation of optimal reduction for the pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of the interaction net reduction strategy using the approach of so-called token-passing nets and a non-deterministic extension for interaction nets. Another new feature is the read-back mechanism implemented without leaving the formalism of interaction nets.

In Andrea Corradini and Hans Zantema: Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016), Eindhoven, The Netherlands, April 8, 2016, Electronic Proceedings in Theoretical Computer Science 225, pp. 45–54.
Published: 10th September 2016.

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-очередь уравнений, которая затем обрабатывается, пока она не станет пуста.
http://arxiv.org/abs/1512.02995

A token-passing net implementation of optimal reduction with embedded read-back

In this paper, we introduce a new interaction net implementation of optimal reduction for pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of interaction net reduction strategy using the approach of so-called token-passing nets. Another new feature is the read-back mechanism also implemented without leaving the formalism of interaction nets.
https://www.npmjs.com/package/inet-lib

JavaScript-движок для сетей взаимодействия

Данный пакет Node.js позволяет редуцировать сети взаимодействия, описанные на языке, близком к исчислению взаимодействия, но без понятия интерфейса, или корня сети взаимодействия. Правила взаимодействия определяются с помощью нотации Yves Lafont. Реализация неявно расширяет системы взаимодействия специальным недетерминированным агентом amb, а также позволяет задавать побочные действия на языке JavaScript.

Ранее этот движок разрабатывался в контексте Macro Lambda Calculus (MLC), Web-реализации λ-исчисления с помощью сетей взаимодействия:

https://codedot.github.io/lambda/

Теперь MLC использует пакет inet-lib в качестве языка низкого уровня, чтобы транслировать в него λ-термы, реализуя механизм readback также внутри формализма сетей взаимодействия.
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:
Хуяк-хуяк, и в продакшн:

$ 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 
        time -p ./example
v1: v2: v1 (v1 (v1 (v2)))
real 0.09
user 0.08
sys 0.00
        make example.p2p
        node parse.js example.mlc p2p >example.p2p
        time -p node interact.js example.p2p
v1: v2: v1 (v1 (v1 (v2)))
real 0.79
user 0.76
sys 0.02
$ 

Осталось немного причесать, и цель достигнута.

Most Popular Tags

Syndicate

RSS Atom

September 2016

S M T W T F S
    12 3
45678910
11121314151617
18192021222324
2526272829 30 
Powered by Dreamwidth Studios