Обозначения

Числа Чёрча: $\overline{n} = \lambda fx.,f^n x$, т.е. $\overline{0}=\lambda fx.x$, $\overline{1}=\lambda fx.fx$

Булевы значения: $\mathbf{T}=\lambda xy.x \quad \mathbf{F}=\lambda xy.y$

Сложение: $\text{Add} = \lambda mnfx.,mf(nfx)$

Умножение (через числа Чёрча): $\overline{m},\overline{n} = \overline{n^m}$

Задача 1. Приведение к βη-нормальной форме

a) $(\lambda xy.xxy),((\lambda xy.yx)(\lambda x.x)),(\lambda xy.xyx)$

Шаг Терм Действие
1 $A = (\lambda xy.yx)(\lambda x.x)$ β-редукция: $\to \lambda y.\,y(\lambda x.x)$
2 $(\lambda xy.xxy)\,A\,B$, где $B=\lambda xy.xyx$ β-редукция: $\to A\,A\,B$
3 $A\,A = (\lambda y.\,y(\lambda x.x))\,A$ β-редукция: $\to A(\lambda x.x)$
4 $A(\lambda x.x) = (\lambda y.\,y(\lambda x.x))(\lambda x.x)$ β-редукция: $\to (\lambda x.x)(\lambda x.x)$
5 $(\lambda x.x)(\lambda x.x)$ β-редукция: $\to \lambda x.x$
6 $(\lambda x.x)\,B$ β-редукция: $\to B$

$$\textbf{Результат: } \lambda xy.xyx$$

b) $(\lambda xy.xyx),(\lambda x.x),((\lambda xy.xxy)(\lambda xy.yx))$

Шаг Терм Действие
1 $C = (\lambda xy.xxy)(\lambda xy.yx)$ β-редукция: $\to \lambda y.\,(\lambda xy.yx)(\lambda xy.yx)\,y$
2 $(\lambda xy.yx)(\lambda xy.yx)$ β-редукция: $\to \lambda y.\,y(\lambda xy.yx)$
3 $C = \lambda y.\,(\lambda y'.\,y'(\lambda xy.yx))\,y$ β-редукция: $C = \lambda y.\,y(\lambda xy.yx)$
4 $(\lambda xy.xyx)(\lambda x.x)$ β-редукция: $\to \lambda y.\,(\lambda x.x)\,y\,(\lambda x.x) \to \lambda y.\,y(\lambda x.x)$
5 $(\lambda y.\,y(\lambda x.x))\,C$ β-редукция: $\to C(\lambda x.x)$
6 $C(\lambda x.x) = (\lambda y.\,y(\lambda xy.yx))(\lambda x.x)$ β-редукция: $\to (\lambda x.x)(\lambda xy.yx)$
7 $(\lambda x.x)(\lambda xy.yx)$ β-редукция: $\to \lambda xy.yx$

$$\textbf{Результат: } \lambda xy.yx$$

Задача 2. Проверка равенства в смысле $=_{\beta\eta}$

a) $(\lambda xy.xxy)(\lambda xy.xyx)(\lambda x.xx)$ vs $(\lambda xy.yxx)(\lambda xy.xyx)(\lambda x.xx)$

Пусть $P = \lambda xy.xyx$, $Q = \lambda x.xx$.

Левый терм Правый терм
$(\lambda xy.xxy)\,P\,Q \to_\beta P\,P\,Q$ $(\lambda xy.yxx)\,P\,Q \to_\beta Q\,P\,P$
$P\,P\,Q \to P\,Q\,P \to Q\,P\,Q$ $Q\,P = P\,P \to P\,P\,P \to \ldots$
$Q\,P\,Q = P\,P\,Q \to \ldots$ (цикл) (цикл)

Оба терма не имеют нормальной формы (редукция расходится). По теореме Чёрча–Россера равенство $=_\beta$ предполагает существование общего редукта. Поскольку нормальных форм нет и редукционные последовательности различны:

$$\boxed{\text{Равенство установить нельзя: оба терма расходятся, общего нормального редукта не существует.}}$$

b) $(\lambda x.xx)(\lambda xy.xyx)(\lambda xy.yxy)$ vs $(\lambda x.xx)(\lambda xy.yxy)(\lambda xy.xyx)$

Пусть $P = \lambda xy.xyx$, $R = \lambda xy.yxy$.

Левый терм Правый терм
$(\lambda x.xx)\,P\,R \to_\beta P\,P\,R$ $(\lambda x.xx)\,R\,P \to_\beta R\,R\,P$
$P\,P = \lambda y.PyP$ $R\,R = \lambda y.yRy$
$P\,P\,R \to P\,R\,P$ $R\,R\,P \to P\,R\,P$ ✓

Оба терма редуцируются к одному и тому же терму $P,R,P$. По теореме Чёрча–Россера:

$$\boxed{(\lambda x.xx)(\lambda xy.xyx)(\lambda xy.yxy) ;=_\beta; (\lambda x.xx)(\lambda xy.yxy)(\lambda xy.xyx)}$$

Задача 3. Нормальная форма терма $M$

$$M = (\lambda xyzw.; z,(x,y,(x,y,y,y,z)),w);\overline{5};\overline{3};Z;I$$

где $Z = \lambda yfx.,yf(yfx)$ и $I = \lambda x.x$.

Ключевое наблюдение: $Z,\overline{n} = \overline{2n}$ (удвоение числа Чёрча), так как: $$Z,\overline{n} = \lambda fx.,\overline{n}f(\overline{n}fx) = \lambda fx.f^n(f^n x) = \lambda fx.f^{2n}x = \overline{2n}$$

Также: $\overline{m},\overline{n} = \overline{n^m}$ (степень в числах Чёрча).

Шаг Вычисление Результат
1. Подстановка $x:=\overline{5},\;y:=\overline{3},\;z:=Z,\;w:=I$ $Z\,(\overline{5}\,\overline{3}\,(\overline{5}\,\overline{3}\,\overline{3}\,\overline{3}\,Z))\,I$
2. $\overline{5}\,\overline{3}$ $\overline{m}\,\overline{n}=\overline{n^m}$ $\overline{3^5} = \overline{243}$
3. $\overline{243}\,\overline{3}$ $\overline{3^{243}}$ $\overline{3^{243}}$
4. $\overline{3^{243}}\,\overline{3}$ $\overline{3^{3^{243}}}$ $\overline{3^{3^{243}}}$
5. $\overline{3^{3^{243}}}\,Z$ Применить $Z$ ровно $3^{3^{243}}$ раз как функцию: $Z^{3^{3^{243}}}$; $Z$ — удвоение, поэтому $\overline{k}$ composed $n$ times даёт умножение на $2^n$ $\overline{2^{3^{3^{243}}}}$
6. $\overline{5}\,\overline{3}\,\overline{2^{3^{3^{243}}}}$ $\overline{243}\,K$ где $K=\overline{2^{3^{3^{243}}}}$: $\;\overline{243}\,K = K^{243}$, т.е. $\overline{(K')^{243}}$ где $K'=2^{3^{3^{243}}}$ $L = \overline{2^{243\cdot 3^{3^{243}}}}$
7. $Z\,L$ Удвоение: $Z\,\overline{n}=\overline{2n}$ $\overline{2^{243\cdot 3^{3^{243}}+1}}$
8. $\overline{N}\,I$ $\overline{n}\,I = \lambda x.\,I^n x = \lambda x.x = I$ $\lambda x.x$

$$\boxed{M =_\beta \lambda x.x}$$

На последнем шаге любое число Чёрча $\overline{n}$, применённое к тождественной функции $I$, даёт $\lambda x.x = I$, поскольку $I^n = I$ для всех $n$.

Задача 4. Комбинатор Even

Идея

Применить функцию «отрицание» ровно $n$ раз к $\mathbf{T}$:

  • чётное число применений $\text{Not}$ возвращает $\mathbf{T}$
  • нечётное число применений $\text{Not}$ возвращает $\mathbf{F}$

Определим $\text{Not} = \lambda b.,b,\mathbf{F},\mathbf{T} = \lambda b.,b,(\lambda xy.y),(\lambda xy.x)$

$$\boxed{\text{Even} = \lambda n.,n,\text{Not},\mathbf{T}}$$

Развёрнуто (без имён): $$\text{Even} = \lambda n.,n,(\lambda b.,b,(\lambda xy.y),(\lambda xy.x)),(\lambda xy.x)$$

Проверка

$n$ Вычисление Результат
$\overline{0}$ $\overline{0}\,\text{Not}\,\mathbf{T} = \mathbf{T}$ $\mathbf{T}$ ✓
$\overline{1}$ $\text{Not}\,\mathbf{T} = \mathbf{F}$ $\mathbf{F}$ ✓
$\overline{2}$ $\text{Not}\,(\text{Not}\,\mathbf{T}) = \mathbf{T}$ $\mathbf{T}$ ✓
$\overline{3}$ $\text{Not}^3\,\mathbf{T} = \mathbf{F}$ $\mathbf{F}$ ✓

Задача 5. Комбинатор Fib

Идея (из императивного программирования)

a := 0; b := 1
repeat n times:
    (a, b) := (b, a+b)
return a

Тело цикла обращается к двум переменным $(a, b)$ — храним пару.

Вспомогательные комбинаторы

Имя Определение Смысл
$\text{Pair}$ $\lambda abf.\,f\,a\,b$ Конструктор пары
$\text{Fst}$ $\lambda p.\,p\,\mathbf{T}$ Первая компонента
$\text{Snd}$ $\lambda p.\,p\,\mathbf{F}$ Вторая компонента
$\text{Add}$ $\lambda mnfx.\,mf(nfx)$ Сложение
$\text{Step}$ $\lambda p.\,\text{Pair}\,(\text{Snd}\,p)\,(\text{Add}\,(\text{Fst}\,p)\,(\text{Snd}\,p))$ $(a,b)\mapsto(b,a+b)$
$\text{Init}$ $\text{Pair}\,\overline{0}\,\overline{1}$ Начальная пара $(0,1)$

Определение

$$\boxed{\text{Fib} = \lambda n.,\text{Fst},(n;\text{Step};\text{Init})}$$

Проверка

$n$ Пара после $n$ шагов $\text{Fst}$ Ожидается
$0$ $(0,\;1)$ $\overline{0}$ $0$ ✓
$1$ $(1,\;1)$ $\overline{1}$ $1$ ✓
$2$ $(1,\;2)$ $\overline{1}$ $1$ ✓
$3$ $(2,\;3)$ $\overline{2}$ $2$ ✓
$4$ $(3,\;5)$ $\overline{3}$ $3$ ✓
$5$ $(5,\;8)$ $\overline{5}$ $5$ ✓

Полное определение без имён

$$\text{Fib} = \lambda n.; n ;\underbrace{(\lambda p,f.; f;(p,(\lambda ab.b));((\lambda mnfx.mf(nfx)),(p,(\lambda ab.a)),(p,(\lambda ab.b))))}{\text{Step}} ;\underbrace{(\lambda f.; f;(\lambda fx.x);(\lambda fx.fx))}{\text{Init}} ;(\lambda ab.a)$$