arXiv:1512.02995 [cs.LO]
Daria Morgendorffer
codedot
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.

This entry was originally posted at http://codedot.dreamwidth.org/175579.html

Анонс пакета Node.js для сетей взаимодействия
Daria Morgendorffer
codedot
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 также внутри формализма сетей взаимодействия.

This entry was originally posted at http://codedot.dreamwidth.org/175264.html

Token-Passing Net Implementation of Optimal Reduction
Daria Morgendorffer
codedot
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.

This entry was originally posted at http://codedot.dreamwidth.org/174955.html

Copy-on-Demand in Interaction Nets
Daria Morgendorffer
codedot
Using McCarthy's amb agent:

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

with the following interaction rules:


This entry was originally posted at http://codedot.dreamwidth.org/174820.html

Лямбды на веревочках нынче в браузере
Daria Morgendorffer
codedot
Добрались-таки лямбды на веревочках до ваших браузеров:

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



This entry was originally posted at http://codedot.dreamwidth.org/174350.html

Лямбды на веревочках почти в браузере
Daria Morgendorffer
codedot
Хуяк-хуяк, и в продакшн:

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

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

This entry was originally posted at http://codedot.dreamwidth.org/174147.html

Лямбды на веревочках скоро в браузере
Daria Morgendorffer
codedot
Наконец-то, дошли руки до портирования 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)))
$ 

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

This entry was originally posted at http://codedot.dreamwidth.org/173860.html

Упражнения из Барендрегта, глава 16
Daria Morgendorffer
codedot
После пятнадцатой главы в плане "Как читать Барендрегта" остается только одна, самая главная - шестнадцатая. В ней, наконец-то, показано, что HP-полное расширение всех осмысленных λ-теорий - это H*, и другого не дано.

16.5.1. Покажем, что
(i) для любого замкнутого терма Z в теории H доказуемо
Z Ω~n = Ω для некоторого n:
если Z неразрешим, то он равен Ω по определению H, иначе
Z имеет головную нормальную форму x1,..., xn: xi Z1 ... Zn, и тогда
Z Ω~n неразрешим и равен Ω по определению H;
(ii) если A x ->> z: z (A (x Ω)), то A Z = A Z' доказуемо
в теории H* для любых термов Z и Z', а
в теории H только для замкнутых Z и Z':
ввиду (i) для некоторого n имеем
A Z ->>βηΩ z1: z1 (...(zn: zn (A Ω))...) <<-βηΩ A Z',
в HP-полной H* содержится, в частности,
непротиворечивая Hω ввиду ее осмысленности,
поэтому там выводимо также следствие A Z = A Z',
но в H правило ω не имеет места.

16.5.2. Покажем, что в H имеет место ext0, но не имеет места ext:
ext влечет правило η, а оно не имеет места в H;
пусть теперь M x = N x, где M и N замкнуты, тогда
M x = N x = Ω может быть только по причине M = N = Ω,
а в противном случае M = x1,..., xm: xi M1 ... Mn и N = y1,..., yn: yj N1 ... Nn,
для которых даже в λ доказуемо M = N (см. упр. 2.4.13).

16.5.3-16.5.7. Обойдемся без альтернативных доказательств теорем,
рисования редукционных графов, рассмотрения оригинальных
построений Морриса и теоремы Мальцева.

16.5.9. Покажем, что терм M разрешим тогда и только тогда,
когда теория λ + (M = Y K) противоречива:
(=>) если M разрешим, то для некоторых термов N1,..., Nn
M N1 ... Nn = K, при этом Y K N1 ... Nn = Y K, но K # Y K (см. упр. 6.8.3);
(<=) если λ + (M = Y K) противоречива, то M разрешим, иначе
в непротиворечивой H выводилось бы M = Ω = Y K.

This entry was originally posted at http://codedot.dreamwidth.org/173644.html

Упражнения из Барендрегта, глава 15
Daria Morgendorffer
codedot
От упражнений остальных глав второй части монографии в 27 уже морщит, как в 50, поэтому перейду сразу к пятнадцатой, где вводится понятие редукции-оракула, которое анализирует доказуемость в осмысленной теории H и говорит, на что еще нет смысла тратить время.

15.4.1. Покажем, что любой терм M Ωη-сильно нормализуем:
η-редукцию всегда можно отложить, при этом
любой терм имеет единственную Ω-нормальную форму и
единственную η-нормальную форму.

15.4.2. Будем писать x \in_R M, если x входит в любой N =R M.
Покажем, что
(i) x \in_βηΩ A x, если A = ω ω, где ω = a, x, z: z (a a (x Ω)):
редукция A x ->>β <...<A (χ^n Ω)>...> не порождает Ω-редексов;
(ii) имеется замкнутый терм O, такой, что
O x [n] z ->>β z Ω~n (O x [n + 1] z) и x \in_βηΩ O x [0]:
возьмем O = Θ (o, x, n, z: (W z n) (o x (S+ n) z)),
где W = Θ (w, z, n: (Zero n) z (w z (P- n) Ω));
(iii) для любого замкнутого F есть замкнутый H, такой, что
H c i a ->>β x: x I (F c a (H c i (S+ a))) и x \in_βηΩ H c x [0]:
возьмем H = Θ (h, c, i, a: (x: x I (F c a (h c i (S+ a)))));
ни в редукции O, ни в редукции H не появляется Ω-редексов.

15.4.3. Пусть у нас есть такая рекурсивная функция f, что
f(n) = 0, если n входит в некоторое множество, иначе f(n) = 1.
Тогда покажем, что
(i)-(ii) λ + {Ω [n] = T | f(n) = 0} + {Ω [n] = F | f(n) = 1} непротиворечива:
λ-определим f через G и вспомним, что терм Ω легкий, поэтому
его можно, в частности, приравнять к n: Zero (G n);
(iii) без нерекурсивных функций не существует и континуума.

15.4.4 (Клоп). Практически решено в указании.

15.4.5. Пусть T = λ + {Ω [0] Z = Ω [1] Ζ | Z замкнут}. Покажем, что
(i) (Якопини) в T недоказуемо Ω [0] = Ω [1]:
заметим, что теория λ + Ω = n: (Zero n) x (y: x y)
непротиворечива из-за легкости Ω и при этом содержит в себе T,
но без аксиомы η недоказуемо равенство x = y: x y;
(ii) если T' = T + (Ω (x: Ω [0] x) = T) + (Ω (x: Ω [1] x) = F),
то T' непротиворечива, а T'ω противоречива:
в T'ω из дополнительных аксиом T следует Ω [0] = Ω [1],
а дополнительные аксиомы T' приведут к T = F, но T # F,
непротиворечивость же T' никому нахуй не сдалась.

15.4.6-15.4.10. Дальше совсем скучно.

This entry was originally posted at http://codedot.dreamwidth.org/173424.html

Упражнения из Барендрегта, глава 6 (продолжение)
Daria Morgendorffer
codedot
В предыдущей серии были упр. 6.8.1-6.8.12. Сейчас будет вторая половина.

6.8.13. Покажем, что цифровая система d адекватна тогда и только тогда, когда
существуют такие Md и Nd, что Md [n] = dn и Nd dn = [n] для всех n:
(=>) Md = Y (f, n: (Zero n) d0 (Sd+ (f (P- n)))), Nd = Y (f, n: (Zerod n) [0] (S+ (f (Pd- n))));
(<=) Pd- = n: Md (P- (Nd n)).
Отсюда получим, что для адекватных цифровых систем d и d'
существуют M и N, что M dn = dn' и N dn' = dn:
возьмем M = n: Md' (Nd n) и N = n: Md (Nd' n).

6.8.14 (Клоп). Покажем, что M = N N~25, где
N = abcdefghijklmnopqstuvwxyzr: r (thisisafixedpointcombinator),
является комбинатором неподвижной точки:
заметим, что M = r: r (M r) = r: r (r (M r)) = ..., и уже все понятно,
но все-таки проверим по теореме о магической силе S I:
(y, f: f (y f)) (r: r (M r) = f: f ((r: r (M r)) f) = f: f (f (M f)) = M.

6.8.15. Упражнение задом наперед:
(iii) нерекурсивные функции - это иллюзия;
(ii) для рекурсивной функции f: N^2 -> N построим попарно различные замкнутые термы X0, X1,..., такие, что Xn Xm = Xf(n, m):
сначала воспользуемся лямбда-определимостью f и построим такой F, что
F [n] [m] = [f(n, m)], предположим Xi = x: x A [n], тогда
Xn Xm = Xm A [n] = (x: x A [m]) A [n] = A A [m] [n], а нам надо, чтобы было
A A [m] [n] = x: x A (F [n] [m]) => A = a, m, n: (x: x a (F n m)), при этом
Xn = Xm => Xn K = Xm K => [n] = [m], то есть термы Xi действительно разные;
(i) для произвольного конечного множества X = {x1,..., xn} с бинарной операцией * на X, покажем, что
Xi Xj = Xk <=> xi * xj = xk для всех i, j, k <= n:
заметим, что Xi Xj = Xk <=> k = f(i, j), и теперь
достаточно представить операцию * функцией f,
тогда xi * xj = xk <=> k = f(i, j).

6.8.16. Строить псевдоцифровую систему на неразрешимых термах - дело неблагодарное, так как при переходе от λ к H она схлопывается, как мыльный пузырь.

6.8.17 (Б. Фридман). Покажем, что f - адекватная цифровая система, если
f0 = x: K, Sf+ = x, y: y x, Pf- = x: x I и Zerof = x, y, z: x (t: F) y z:
Sf+ fn = y: y fn # fn, иначе (y: y fn) (K M) = fn (K M) => M = K,
Zerof f0 = y, z: f0 (t: F) y z = (x: K) (t: F) = T;
Zerof (Sf+ fn) = y, z: Sf+ fn (t: F) y z = y, z: (t: F) fn y z = F;
Pf- (Sf+ fn) = Sf+ fn I = I fn = fn.

6.8.18 (Ершов). Ой, ну его.

6.8.19. Покажем, что перед нами адекватные цифровые системы:
(i) (Ван дер Поль и др.) последовательность pn = x, y: x y~n:
Sp+ (x, y: x y~n) = x, y: x y~n y = x, y: Sp+ x y y = Y (f, x, y: f x y y);
(ii) (Бем, Дедзани-Чанкальини)
d0 = Y, Sd+ = x, y: y x P для любого P:
Pd- = x: x K => Pd- (Sd+ dn) = Sd+ dn K = K dn P = dn,
Zerod = x: x (K (K T)) I =>
Zerod d0 = Y (K (K T)) I = K (K T) (...) I = K T I = T и
Zerod (Sd+ dn) = Sd+ dn (K (K T)) I = K (K T) dn P I = K T P I = T I = F;
e0 = K, Se+ = x, y: y x Y:
Se+ en K = K en Y = en, поэтому годится тот же
Pe- = Pd- = x: x K,
Se+ en (K (K T)) I = K (K T) en Y I = T I = F, но
e0 (K (K T)) I = K (K (K T)) I = K (K T), поэтому придется взять другой
Zeroe = x: x (K (K T)) I I F;
комбинаторы неподвижной точки не имеют нормальной формы,
поэтому адекватная цифровая система не обязательно нормальна.

6.8.20-6.8.22. Ну и хватит уже цифровых систем.

6.8.23 (Дж. Терлаув). Теорема Скотта без использования второй теоремы о неподвижной точке уже практически доказана в указании к этому упражнению.

6.8.24. Покажем, что G X = G (F (G X)), если X = Y (x: F (G x)):
X = (x: F (G x)) X = F (G (X)) => G X = G (F (G X)).

This entry was originally posted at http://codedot.dreamwidth.org/173251.html

?

Log in