Упражнения из Барендрегта, глава 6
May. 11th, 2015 09:36 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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).
Продолжение следует...
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).
Продолжение следует...
