Упражнения из Барендрегта, глава 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

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

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).

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

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

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

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.

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

Упражнения из Барендрегта, глава 3
Daria Morgendorffer
codedot
Вчера были упражнения ко второй главе монографии, а сегодня пробежка галопом по третьей.

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;
второй граф имеет терм I ω ω -> I Ω -> Ω, I Ω -> Ω, Ω -> Ω;
третий граф имеет терм 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. Дальше в редукционные дебри углубляться не буду.

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

Упражнения из Барендрегта, глава 2
Daria Morgendorffer
codedot
Я решил пробежаться еще раз по плану "Как читать Барендрегта". По дороге буду срать в вашу френд-ленту следующим содержимым. (Чтобы не переключаться все время еще и на греческую раскладку, воспользуюсь синтаксисом, похожим на 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.

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

Read-Back Embedded into Interaction System
Daria Morgendorffer
codedot
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, rC[ ](y)), x] >< rC[ ][y];
@[λ(x, rC[ ](y)), x] >< rC[ ][y];

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

aM >< λ[rM [ ](x), x];
aM >< rC[ ][aC[M]];
λ[ay, rC[λy.[ ]](x)] >< rC[ ][x], where y ∈ Λ is a new variable.

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

<aN | ∅>

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

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

Conservative Non-Deterministic Extension for Interaction Calculus
Daria Morgendorffer
codedot
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:

<t1,..., tn | t = Amb(u, v, w), Δ> = <t1,..., tn | 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

α[x1,..., xn] >< Amb[y, α(x1,..., xn), y].

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

Interaction System and Encoding for MLC
Daria Morgendorffer
codedot
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.)

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

You are viewing codedot