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