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