Упражнения из Барендрегта, глава 3
May. 9th, 2015 11:48 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
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;
второй граф имеет терм (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. Дальше в редукционные дебри углубляться не буду.
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. Дальше в редукционные дебри углубляться не буду.
