codedot | Recent Entries

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]₀> 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]₀> 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:

После пятнадцатой главы в плане "Как читать Барендрегта" остается только одна, самая главная - шестнадцатая. В ней, наконец-то, показано, что 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.

От упражнений остальных глав второй части монографии в 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. Дальше совсем скучно.

В предыдущей серии были упр. 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)).

После небольшого отступления к четвертой главе, вернемся к плану "Как читать Барендрегта". Итак, вторая часть, глава шестая. Она содержит довольно много упражнений, поэтому сейчас будет только половина.

6.8.1. Докажем, что <M1,..., Mn> = <N1,..., Nn> <=> M1 = N1,..., Mn = Nn:
(=>) <M1,..., Mn> (x1,..,xn: xi) = <N1,..., Nn> (x1,..,xn: xi) => Mi = Ni;
(<=) x = x => x M1 ... Mn = x N1 ... Nn => x: x M1 ... Mn = x: x N1 ... Nn.

6.8.2. Построим замкнутые термы K8 и A, такие, что:
(i) K8 x = K8:
K8 = y: K8 = (f, y: f) K8 = Y (f, y: f);
(ii) A x = x A:
A = y: y A = (f, y: y f) A = Y (f, y: y f).

6.8.3. Покажем, что для построенного K8 имеет место K # K8:
K = K8 => K M I = K8 M I => M = K8.

6.8.4. Поздоровавшись с LISP, построим замкнутые термы M и N, такие что
(i) M [n] x y = x y~n для всех n:
заметив, что M [n + 1] x y = x y~n+1 = (x y~n) y = (M [n] x y) y,
получаем M = Y (f, n, x, y: (Zero n) x ((f (P- n) x y) y));
(ii) N [n] [i] = x: x F~i T для i < n и N [n] [n] = x: x F~n:
введем сначала G [n] [i] = i < n ? T : F, взяв
G = Y (f, n, i: (Zero n) F ((Zero i) T (f (P- n) (P- i)))),
а потом используем M и G, чтобы определить
N = n, i: (G n i) (y, x: M [i] x F) (y, x: (M [i] x F) T).

6.8.5. Построим последовательность термов A0, A1..., такую, что
A0 = S и An+1 = An An+2:
для этого возьмем An = A [n], где
A [n] = n = 0 ? S : (A [n - 1]) (A [n + 1]), то есть
A = Y (a, n: (Zero n) S ((a (P- n)) (a (S+ n))).

6.8.6 (Россер). Все интернеты уже сто лет дрочат на то, как работают сложение, умножение и показательная функция для цифр Черча.

6.8.7. Пропустим супер-пупер-обобщение теорем о неподвижной точке.

6.8.8. Покажем, что для любого терма M существует такой M' в нормальной форме, что M' I = M:
построим сначала N, заменив в M каждый редекс (yi: Pi) Qi на x (yi: Pi) Qi,
тогда M' = x: N не будет содержать редексов, но при этом M' I ->> M.

6.8.9. В HP-полном расширении λ все комбинаторы неподвижной точки равны, поэтому утверждения
(i) Y_M = Y_N => M = N и
(ii) Ym = Yn => m = n
там не имеют места в общем случае, так что не будем забивать голову.

6.8.10. Покажем, что существует такой M, что M = [M]:
[M] = M => I [M] = M, а по второй теореме о неподвижной точке
можно взять M = W [W], где W = x: I (Ap x (Num x)).

6.8.11 (Черч). Покажем, что множество {M | M = I} не рекурсивно:
данное множество содержит I, но не содержит K, поэтому оно нетривиально,
при этом оно по определению замкнуто относительно равенства,
а мы уже знаем, что множества с двумя этими свойствами не рекурсивны.

6.8.12. Эффективно неотделимые множества определены за пределами монографии (см. "Теория рекурсивных функций и эффективная вычислимость" Роджерса, с. 126).

Продолжение следует...

Немного отклонюсь от плана "Как читать Барендрегта" и от третьей главы монографии внезапно перейду аж сразу к четвертой. Внимание: будут ссылки на упражнения второй главы.

4.3.1. См. упр. 2.4.12 (i).

4.3.2 (Виссер). Замкнутый терм M называется легким, если для всех замкнутых термов N теория λ + (M = N) непротиворечива. В предположении легкости терма M докажем следующие утверждения.
(i) M N легкий для любого замкнутого терма N:
в непротиворечивой λ + (M = K M) выводимо M N = K M N => M N = M,
откуда следует, что λ + (M N = Q) непротиворечива для любого замкнутого Q;
(ii) M неразрешим, иначе бы M N1 ... Nn = I для некоторых Ni,
а из (i) следовало бы, что λ + (I = K) непротиворечива, но I # K (упр. 2.4.2 (i));
(iii)-(iv) если функция f(n) = #Pn рекурсивна, то она представима некоторым лямбда-термом F, таким, что F [n] = Pn, и
тогда в непротиворечивой λ + (M = F) выводимы M [n] = F [n] => M [n] = Pn для всех n;
если же f(i) не является рекурсивной функцией, то я в эти игры не играю, потому что не считаю вопрос "Есть ли Б-г на Марсе?" уместным в этой теме.
(v) λ + {M = N | M и N легкие} непротиворечива:
мы уже знаем о непротиворечивости осмысленной теории H, которая приравнивает все неразрешимые термы, а в пунтке (ii) мы доказали, что все легкие термы неразрешимы.

4.3.3. Модельные соображения не включены в программу намеренно.

4.3.4. Покажем, что не существует такого M, чтобы для любых N теория H + (M = N) была непротиворечивой:
в 4.3.2 (ii) мы доказали, что M должен быть неразрешимым, но
в H все неразрешимые термы приравнены к W3 = (x: x x x) (x: x x x), а
из упр. 2.4.12 (ii) мы знаем, что I # W3.

Вчера были упражнения ко второй главе монографии, а сегодня пробежка галопом по третьей.

3.5.1. Нарисовать графы G(M) для каких угодно термов каждый может и сам.

3.5.2. А вот найти термы по заданному бета-графу - это уже интересно:
(i) M1 -> ... -> Mn -> M1 для произвольного n:
M1 = N N~n, где N = x1,..., xn: xn ... x2 x1 x1;
(ii) чтобы добавить к (i) Mi -> Mi для всех i, возьмем M1 Ω;
(iii) чтобы добавить к (i) Mi -> I для всех i, возьмем (x: I) M1;
второй граф имеет терм (x: x ω (y: x y)) ω -> Ω (y: ω y) -> Ω ω, Ω (y: ω y) -> Ω (y: ω y), Ω ω -> Ω ω;
третий граф имеет терм K I Ω -> (x: I) Ω -> I, K I Ω -> Κ Ι Ω, (x: I) Ω -> (x: I) Ω;
(iv) чтобы сделать бесконечный цилиндр из (i), возьмем M1 ((x: x x x) (x: x x x)).

3.5.3. Построим терм M0, такой, что M0 ->>β M1 ->η M2 ->>β M3 ->η M4 ->>β ...:
M0 = x: (y: M) x x ->>β x: M x ->η M ->>β Μ0;
M найдем, как будто мы до сих пор никогда не слышали про Y:
M = (f, x: (y: f) x x) M, M = W W, W = w: (f, x: (y: f) x x) (w w).

3.5.4. Пусть M = (b, x, z: z ( b b x)) (b, x, z: z (b b x)) x. Чтобы получить кайф, построив G(M) и установив, что для каждого n этот граф имеет n-мерный куб в качестве подграфа, нужно сначала покурить каннабис на родине автора.

3.5.5 (Бем). Бем не обидится, если не все будут рисовать G(M).

3.5.6 (Виссер). (i) Это мое самое любимое упражнение. Покажем, что имеется единственный редекс R с одной вершиной в G(R).
Если R = (x: M) N, то M[x := N] = (x: M) N. Рассмотрим все случаи:
1) x не входит в M => M = R => R = (x: R) N - это не терм;
2) M = x => x[x := N] = R => N = R => R = (x: x) R - это не терм;
3) M = P Q;
4) M = y: M' => R = y: M'[x := N] - это не редекс.
Значит, R = (x: P Q) N =
= (P Q)[x := N] = P[x := N] Q[x := N] = (x: P Q) N => P[x := N] = x: P Q и Q[x := N] = N;
Рассмотрим все случаи для P:
1) x не входит в P => P = (x: P Q) - это не терм;
2) P = x => N = x: x Q;
3) P = y: P', но тогда в R было бы два редекса, а не один;
4) P = P1 P2 => P[x := N] = P1[x := N] P2[x := N] - это аппликация, а не абстракция.
Значит, R = (x: x Q) (x: x Q) -> (x: x Q) Q[x := x: x Q] => Q[x := N] = x: x Q.
Рассмотрим все случаи для Q:
1) x не входит в Q => Q = x: x Q - это не терм;
2) Q = x;
3) Q = Q1 Q2 => Q1[x := N] Q2[x := N] - это аппликация, а не абстракция;
4) Q = y: Q' => y: Q'[x := N] = x: x Q => Q'[x := N] = y Q, но тогда x не входит в Q.
Таким образом, R = (x: x x) (x: x x).
(ii) А вот это не самое любимое мое упражнение.

3.5.7-3.5.10. Бла-бла-бла про хитровытраханные графы и понятия редукции.
Может быть, они и полезные упражнения, но я иду дальше.

3.5.11. Будем писать M ^ N, если L ->> M и L ->> N для некоторого терма L. Докажем, что
(i) K I K ^ K I S: возьмем K (K I S) K;
(ii) (x: a x) b ^ (y: y b) a: возьмем (y: (x: y x) b) a;
(iii) (x: x c) c ^ (x: x x) c: возьмем (y: (x: x y) y) c;
(iv) (x: b x) c ^ (x: x) b c: возьмем (y, x: y x) b c;
(v) (x: b x (b x)) c ^ (x: x x) (b c): возьмем (z, y: (x: x x) (z y)) b c;
(vi) (x: b x) c ^ (x: x) (b c): возьмем I ((y, x: y x) b c);
(vii)* (Плоткин) ...ах, если бы я смог доказать, что не имеет места (x: b x (b c)) c ^ (x: x x) (b c), то я бы прочувствовал, что бета-редукция не обладает "перевернутым свойством CR".

3.5.12-3.5.15. Дальше в редукционные дебри углубляться не буду.

Я решил пробежаться еще раз по плану "Как читать Барендрегта". По дороге буду срать в вашу френд-ленту следующим содержимым. (Чтобы не переключаться все время еще и на греческую раскладку, воспользуюсь синтаксисом, похожим на MLC.)

2.4.1. Покажем, что следующие термы имеют нормальную форму:
(i) (y: y y y) ((a, b: a) I (S S)) = (y: y y y) I = I I I = I;
(ii) (y, z: z y) ((x: x x x) (x: x x x)) (w: I) = (w: I) ((x: x x x) (x: x x x)) = I;
(iii) S S S S S S S = S S (S S S S S) = S S (S S (S S S)), если заметить S S M S = S S (M S);
(iv)* S (S S) (S S) (S S) S S... сдаюсь без калькулятора.

2.4.2. Покажем, что следующие пары термов несравнимы:
(i) I # K, иначе I I M = K I M => M = I;
(ii) I # S, иначе I K M I = S K M I => K M I = K I (M I) => M = I;
(iii) x y # x x, иначе x, y: x y = x, y: x x => (x, y: x y) I M = (x, y: x x) I M => M = I.

2.4.3. Построим замкнутые термы M0, M1..., такие, что Mi # Mj для всех i != j:
Mi = x0, x1,..., xi: xi;
Mi = Mj, i > j => Mi y1 ... yj = Mj y1 ... yj => Mk = I, k = i - j;
Mk = I => Mk I ...(k-1)... I = I I ...(k-1)... I => x: I = I => (x: I) M = I M => I = M.

2.4.4. Покажем, что аппликация не ассоциативна, точнее x (y z) # (x y) z:
x (y z) = (x y) z => x, y, z: x (y z) = x, y, z: (x y) z => K (I M) I = (K I) M I => M = I.

2.4.5 (К. Е. Шаап). Пусть X = S I. Покажем, что X X X X = X (X (X X)), и вообще для всех n имеет место X^n X = X X~n:
n = 1: X X = X X;
n = 2: X X X = S I X X = I X (X X) = X (X X).
n > 2: X^n X = X X~n =>
X X~n+1 = X X~n X = (X^n X) X = X (X^n-1 X) X =
= S I (X^n-1 X) X = X ((X^n-1 X) X) = X (X X~n-1 X) =
= X (X X~n) = X (X^n X) = X^n+1 X.

2.4.6. Покажем, что не существует такого F, чтобы для любых M и N выполнялось бы F (M N) = M:
I I = (x: I) I => F (I I) = F ((x: I) I) => I = x: I => I M = (x: I) M => M = I.

2.4.7. Покажем, что существует такой M, что для любого N выполняется M N = M M, применив теорему о неподвижной точке:
M x = M M => M = x: M M => M = (f, x: f f) M;
M = W W, W = w: (f, x: f f) (w w);
M N = (f, x: f f) M N = (x: M M) N = M M.

2.4.8. Бла-бла-бла про одновременную подстановку.
В пизду эту болтологическую муть.

2.4.9. Покажем, что (x, y: M) N = y: (x: M) N:
(x, y: M) N = (y: M)[x := N] = y: M[x := N] = y: (x: M) N.

2.4.10. Используем теорему о неподвижной точке, чтобы построить терм M, такой, что
(i) M = M S:
M = (f: f S) M, M = W W, W = w: (f: f S) (w w);
M = (f: f S) M = M S;
(ii) M I S S = M S:
M = (f, s: f I s s) M, M = W W, W = w: (f, s: f I s s) (w w);
M S = (f, s: f I s s) M S = M I S S.

2.4.11. Построим F, такой, что F I = x и F K = y, вспомнив упражнение 2.4.2 (i):
если F = f: f I M N, тогда
F K = K I M N = N => N = y;
F I = I I M N = M N => M = z: x;
cтало быть, F = f: f I (z: x) y.

2.4.12 (Якопини). Пусть w3 = x: x x x и W3 = w3 w3. Покажем, что
(i) I # w3, иначе I (x, y: I) = w3 (x, y: I) => x, y: I = I => (x, y: I) I M = I I M => I = M;
(ii) I # W3, иначе I = W3 => I w3 = W3 w3 => w3 = W3 w3, а если заметить
W3 = w3 w3 w3 = W3 w3, то W3 = I => I = I w3, что возвращает нас к пункту (i).

2.4.13. Покажем, что для любой абстракции M имеет место равенство x: M x = M:
M = y: N;
x: M x = x: (y: N) x = x: N[y := x] = y: N = M.

2.4.14. Пусть M = x: x (y: y y) (y: y y). Покажем, что M I-разрешим:
M (x, y: x I (y I)) = I I (I I) = I.

2.4.15 (почему-то есть только в оригинале, Минц не перевел). Suppose a symbol of the lambda calculus alphabet is always 0.5 cm wide. Let us write down a lambda term with length less than 20 cm having a normal form with length at least 10^(10^10) lightyear. The speed of light is c = 3 * 10^10 cm/sec.
The length of a Church numeral in cm is about the natural number it represents, so it is more than enough to write a term that reduces to the Church numeral for the number 2^(2^(2^(2^(2^2)))). The exponential function for Church numerals is just application, so the term can be (x: x x x x x x) (f, x: f (f x)) which is, in turn, much shorter than requested.

http://arxiv.org/pdf/1304.2290v7.pdf

Interaction system of MLC implements token-passing nets and embeds read-back mechanism.

Specifically, starting from initial configuration that encodes a λ-term

<x | r_[ ](x) = y, Γ(M^•, y)>,

the r(ead) agent will trigger duplication and application:

s[c(x, r_{C[ ]}(y)), x] >< r_{C[ ]}[y];
@[λ(x, r_{C[ ]}(y)), x] >< r_{C[ ]}[y];

and will construct normal form of the encoded λ-term:

a_M >< λ[r_{M [ ]}(x), x];
a_M >< r_C[ ][a_C[M]];
λ[a_y, r_C[λy.[ ]](x)] >< r_C[ ][x], where y ∈ Λ is a new variable.

If normal form N of the λ-term exists, interaction results in configuration

<a_N | ∅>

which consists of only one a(tom) agent in its interface.

We work in interaction calculus. However, we will need a special non-deterministic agent Amb. To represent this agent, we also extend interaction calculus, but in a more conservative fashion than it was previously suggested in the original paper.

Instead, we prepend the list of its auxiliary ports with its extra principal port and introduce conversion for configurations to represent non-deterministic behavior of Amb:

<t₁,..., t_n | t = Amb(u, v, w), Δ> = <t₁,..., t_n | u = Amb(t, v, w), ∆>.

We assume that any interaction system’s signature Σ is implicitly extended by Amb with Ar(Amb) = 3, while its set of rules is implicitly extended with

α[x₁,..., x_n] >< Amb[y, α(x₁,..., x_n), y].

https://www.scribd.com/doc/260727360

The goal of our Macro Lambda Calculus project (MLC) is to encode λ-terms into interaction nets. Its software implementation will accept input in the notation similar to λ-calculus allowing macro definitions. Output is similar to interaction calculus and is suitable for our Interaction Nets Compiler program (INC). In this paper, we describe the interaction system for call-by-need evaluation and the mechanism of encoding λ-terms into this system which MLC is based on.

(The paper provides formal definition for the interaction system and encoding of λ-terms that were previously successfully tested for Y (K M) = M using INC.)

Encoding ω Α (K ω), where ω ≡ λx.x x, A ≡ λx.λf.f (x x f), and K ≡ λx.λy.x:

$ cat init.txt 
term = \read_{strdup("")}(\print);

term = \apply(\apply(omega1, a), \apply(k, omega2));

omega1 = \lambda(x1, \apply(\amb(y1, \share(x1, z1), z1), y1));
omega2 = \lambda(x2, \apply(\amb(y2, \share(x2, z2), z2), y2));

a = \lambda(self, \lambda(func, \apply(func1, rec)));
rec = \apply(\apply(self1, self2), func2);
self1 = \amb(self2, \share(self, back1), back1);
func1 = \amb(func2, \share(func, back2), back2);

k = \lambda(x, \lambda(\erase, x));
$ make
        printf '%s\n\n$$\n\n%s\n\n$$\n\n%s\n' >test.in \
                "`cat rset.txt`" \
                "`cat init.txt`" \
                "`cat tail.txt`"
        inc <test.in
        mv in.tab.c test.c
        cc    -o test test.c 
        valgrind ./test
==20346== Memcheck, a memory error detector
==20346== Copyright (C) 2002-2010, and GNU GPL'd, by Julian Seward et al.
==20346== Command: ./test
==20346== 
v1: (v1 (v1))
==20346== 
==20346== HEAP SUMMARY:
==20346==     in use at exit: 0 bytes in 0 blocks
==20346==   total heap usage: 606 allocs, 606 frees, 23,934 bytes allocated
==20346== 
==20346== All heap blocks were freed -- no leaks are possible
==20346== 
==20346== For counts of detected and suppressed errors, rerun with: -v
==20346== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 4 from 4)
$

https://gist.github.com/codedot/24f277ef4df5828c70a8

Call-by-need evaluation strategy using non-deterministic extension in Interaction Nets Compiler:

@@ -14,10 +14,18 @@
 \print {
 	/* Output results of read-back. */
 	puts(RVAL);
-	exit(EXIT_SUCCESS);
+	free(RVAL);
 } \atom;
 
 \read[a] {
+	/* Unshare variable. */
+} \share[\copy(b, \read_{LVAL}(a)), b];
+
+\read[a] {
+	/* Initiate application. */
+} \apply[\lambda(b, \read_{LVAL}(a)), b];
+
+\read[a] {
 	/* Read back abstraction. */
 } \lambda[\atom_{var(1)}, \read_{ABST(LVAL, var(0))}(a)];
 
@@ -29,10 +37,6 @@
 	/* Read back an atom. */
 } \atom;
 
-\bind[a, \atom_{RVAL}, a] {
-	/* Bind variable to an atom. */
-} \atom;
-
 \copy[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
 	/* Copy an atom. */
 } \atom;
@@ -47,40 +51,56 @@
 } \atom;
 
 \lambda[a, b] {
+	/* Unshare variable. */
+} \share[\copy(c, \lambda(a, b)), c];
+
+\lambda[a, b] {
+	/* Initiate application. */
+} \apply[\lambda(c, \lambda(a, b)), c];
+
+\lambda[a, b] {
 	/* Apply a closed term. */
 } \lambda[a, b];
 
+\copy[a, b] {
+	/* Unshare variable. */
+} \share[\copy(c, \copy(a, b)), c];
+
+\copy[a, b] {
+	/* Initiate application. */
+} \apply[\lambda(c, \copy(a, b)), c];
+
 \copy[\lambda(a, b), \lambda(c, d)] {
 	/* Initiate copy of a closed term. */
 } \lambda[\dup(a, c), \dup(b, d)];
 
-\bind[a, \lambda(b, c), a] {
-	/* Bind variable to a closed term. */
-} \lambda[b, c];
+\dup[\amb(a, \share(b, c), c), \amb(d, \share(e, f), f)] {
+	/* Duplicate sharing. */
+} \share[\dup(b, e), \dup(a, d)];
+
+\dup[\apply(a, b), \apply(c, d)] {
+	/* Duplicate application. */
+} \apply[\dup(a, c), \dup(b, d)];
 
 \dup[\lambda(a, b), \lambda(c, d)] {
-	/* Duplicate abstraction or application. */
+	/* Duplicate abstraction. */
 } \lambda[\dup(a, c), \dup(b, d)];
 
-\dup[\copy(a, b), \copy(c, d)] {
-	/* Duplicate copy initiator. */
-} \copy[\dup(a, c), \dup(b, d)];
-
-\dup[\bind(a, b, c), \bind(d, e, f)] {
-	/* Duplicate variable binding. */
-} \bind[\dup(a, d), \dup(b, e), \dup(c, f)];
-
 \dup[a, b] {
 	/* Finish duplication. */
 } \dup[a, b];
 
 \erase {
-	/* Erase abstraction or application. */
-} \lambda[\erase, \erase];
+	/* Erase sharing. */
+} \share[a, a];
 
 \erase {
-	/* Erase variable binding. */
-} \bind[\erase, \erase, \erase];
+	/* Erase application. */
+} \apply[\erase, \erase];
+
+\erase {
+	/* Erase abstraction. */
+} \lambda[\erase, \erase];
 
 \erase {
 	/* Erase copy initiator. */
@@ -96,17 +116,12 @@
 
 $$
 
-{"Application"} = result;
-function = \lambda(argument, result);
-shared1 = \copy(first1, second1);
-shared2 = \copy(first2, second2);
-shared3 = \copy(first3, second3);
-
-{"Abstraction"} = bind0;
-bv1 = \bind(bind1, fv1, bind0);
-bv2 = \bind(bind2, fv2, bind1);
-bv3 = \bind(bind3, fv3, bind2);
-bindn = \lambda(variable, body);
+{"Application"} = \apply(function, argument);
+first1 = \amb(second1, \share(shared1, back1), back1);
+first2 = \amb(second2, \share(shared2, back2), back2);
+first3 = \amb(second3, \share(shared3, back3), back3);
+
+{"Abstraction"} = \lambda(variable, body);
 
 term = \read_{strdup("")}(\print);
 term = {"Encoding"};

В компиляторе сетей взаимодействия INC (Interaction Nets Compiler) теперь есть поддержка недетерминированного расширения в виде специального бинарного агента Amb с двумя главными портами. Это расширение необходимо при реализации стратегии "call-by-need" для λ-исчисления.

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

 
 $$
 
-\fan_{1}(x, x) = \fan_{2}(\erase, {&wire1});
+\fan_{1}(x, x) = \amb({&wire1}, \fan_{2}(\erase, y), y);
 
 {&wire2} = \fan_{3}({&erase}, \erase);

Decoding extension for Implementation of Closed Reduction using Interaction Nets Compiler:

${
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

char *var(int fresh);
char *append(char *format, char *buf, char *str);

#define ABST(BUF, STR) append("%s%s: ", (BUF), (STR))
#define APPL(BUF, STR) append("%s%s ", (BUF), (STR))
#define ATOM(BUF, STR) append("%s(%s)", (BUF), (STR))
}$

\print {
	/* Output results of read-back. */
	puts(RVAL);
	exit(EXIT_SUCCESS);
} \atom;

\read[a] {
	/* Read back abstraction. */
} \lambda[\atom_{var(1)}, \read_{ABST(LVAL, var(0))}(a)];

\lambda[\read_{APPL(strdup(""), RVAL)}(a), a] {
	/* Read back application. */
} \atom;

\read[\atom_{ATOM(LVAL, RVAL)}] {
	/* Read back an atom. */
} \atom;

\bind[a, \atom_{RVAL}, a] {
	/* Bind variable to an atom. */
} \atom;

\copy[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Copy an atom. */
} \atom;

\dup[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Duplicate an atom. */
} \atom;

\erase {
	/* Erase an atom. */
	free(RVAL);
} \atom;

$$

term = \read_{strdup("")}(\print);
term = {"Encoding"};

$$

char *var(int fresh)
{
	static int id;

	char buf[BUFSIZ];

	if (fresh)
		++id;

	sprintf(buf, "v%d", id);
	return strdup(buf);
}

char *append(char *format, char *buf, char *str)
{
	size_t size = strlen(format) + strlen(str);
	char *result = malloc(strlen(buf) + size);

	sprintf(result, format, buf, str);

	free(buf);
	free(str);
	return result;
}

An Interaction Net Implementation of Closed Reduction by Ian Mackie using Interaction Nets Compiler:

\lambda[a, b] {
	/* Apply a closed term. */
} \lambda[a, b];

\copy[\lambda(a, b), \lambda(c, d)] {
	/* Initiate copy of a closed term. */
} \lambda[\dup(a, c), \dup(b, d)];

\bind[a, \lambda(b, c), a] {
	/* Bind variable to a closed term. */
} \lambda[b, c];

\dup[\lambda(a, b), \lambda(c, d)] {
	/* Duplicate abstraction or application. */
} \lambda[\dup(a, c), \dup(b, d)];

\dup[\copy(a, b), \copy(c, d)] {
	/* Duplicate copy initiator. */
} \copy[\dup(a, c), \dup(b, d)];

\dup[\bind(a, b, c), \bind(d, e, f)] {
	/* Duplicate variable binding. */
} \bind[\dup(a, d), \dup(b, e), \dup(c, f)];

\dup[a, b] {
	/* Finish duplication. */
} \dup[a, b];

\erase {
	/* Erase abstraction or application. */
} \lambda[\erase, \erase];

\erase {
	/* Erase variable binding. */
} \bind[\erase, \erase, \erase];

\erase {
	/* Erase copy initiator. */
} \copy[\erase, \erase];

\erase {
	/* Erase duplicator. */
} \dup[\erase, \erase];

\erase {
	/* Finish erasing. */
} \erase;

$$

{"Application"} = result;
function = \lambda(argument, result);
shared1 = \copy(first1, second1);
shared2 = \copy(first2, second2);
shared3 = \copy(first3, second3);

{"Abstraction"} = bind0;
bv1 = \bind(bind1, fv1, bind0);
bv2 = \bind(bind2, fv2, bind1);
bv3 = \bind(bind3, fv3, bind2);
bindn = \lambda(variable, body);

$ cat >hello.in 
${
#include <stdio.h>
}$

\alpha {
        printf("%s %s!\n", LVAL, RVAL);
} \beta;

$$

\alpha_{"Hello"} = \beta_{"World"};

$$

#include <stdlib.h>

inagent *inaux(void *aux, void *offline)
{
        return NULL;
}

int main()
{
        interact();
        return 0;
}
$ inc <hello.in
$ c99 in.tab.c
$ ./a.out
Hello World!
$

В компиляторе сетей взаимодействия INC (Interaction Nets Compiler) теперь есть поддержка начальной конфигурации. Конфигурация описывается на языке, близком к исчислению взаимодействия. Эта функциональность должна сильно упростить проект MLC: текст на языке MLC (Macro Lambda Calculus) можно будет целиком транслировать в исходный код для INC, а уже оттуда - в исполняемый код на Си. Трансляцию из MLC в INC можно сделать с помощью компактного представления λ-термов в сетях взаимодействия и механизма "readback" в виде системы взаимодействия с побочными действиями.

Ниже пример работы INC.

$ inc <example.in
$ c99 in.tab.c
$ ./a.out
inaux: rewired
inaux: returns
inaux: returns
inaux: returns
fan_1 >< fan_2
fan_3 >< fan_3
erase >< fan_3
fan_3 >< fan_3
erase >< erase
erase >< erase
$

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

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

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

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

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

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

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

( Наброски )