Обозначения

Числа Чёрча: $\overline{n} = \lambda fx.f^n x$, т.е. $\overline{0}=\lambda fx.x$, $\overline{1}=\lambda fx.fx$, $\overline{n}$ применяет $f$ ровно $n$ раз.

Булевы: $\mathbf{T}=\lambda xy.x$, $\mathbf{F}=\lambda xy.y$.

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

Задача 1

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

Сначала вычислим аргумент $A = (\lambda xy.yx)(\lambda x.x)$:

$$A = (\lambda xy.yx)(\lambda x.x) \to_\beta \lambda y.\,y(\lambda x.x)$$

Теперь применяем $(\lambda xy.xxy)$ к $A$ и к $B = \lambda xy.xyx$:

$$(\lambda xy.xxy)\,A\,B \to_\beta A\,A\,B$$

Вычислим $A\,A$:

$$A\,A = (\lambda y.\,y(\lambda x.x))\,A \to_\beta A(\lambda x.x) = (\lambda y.\,y(\lambda x.x))(\lambda x.x) \to_\beta (\lambda x.x)(\lambda x.x) \to_\beta \lambda x.x$$

Теперь $(\lambda x.x)\,B \to_\beta B = \lambda xy.xyx$.

$$\boxed{\lambda xy.xyx}$$

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

Сначала вычислим $C = (\lambda xy.xxy)(\lambda xy.yx)$:

$$C \to_\beta \lambda y.\,(\lambda xy.yx)(\lambda xy.yx)\,y$$

$$(\lambda xy.yx)(\lambda xy.yx) \to_\beta \lambda y.\,y(\lambda xy.yx)$$

$$C = \lambda y.\,(\lambda y'.\,y'(\lambda xy.yx))\,y = \lambda y.\,y(\lambda xy.yx)$$

Пусть $D = \lambda y.\,y(\lambda xy.yx)$.

Вычислим $(\lambda xy.xyx)(\lambda x.x)$:

$$(\lambda xy.xyx)(\lambda x.x) \to_\beta \lambda y.(\lambda x.x)\,y\,(\lambda x.x) \to_\beta \lambda y.\,y(\lambda x.x)$$

Теперь применим к $D$:

$$(\lambda y.\,y(\lambda x.x))\,D \to_\beta D(\lambda x.x) = (\lambda y.\,y(\lambda xy.yx))(\lambda x.x) \to_\beta (\lambda x.x)(\lambda xy.yx) \to_\beta \lambda xy.yx$$$$\boxed{\lambda xy.yx}$$

Задача 2

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$$

$$P\,P = (\lambda xy.xyx)\,P \to_\beta \lambda y.\,P\,y\,P$$

$$P\,P\,Q = (\lambda y.\,PyP)\,Q \to_\beta P\,Q\,P$$

$$P\,Q = (\lambda xy.xyx)\,Q \to_\beta \lambda y.\,Q\,y\,Q$$

$$P\,Q\,P = (\lambda y.\,QyQ)\,P \to_\beta Q\,P\,Q$$

$$Q\,P = (\lambda x.xx)\,P \to_\beta P\,P \quad\text{(цикл!)}$$

Редукция не завершается — нормальной формы нет.

Правый терм:

$$(\lambda xy.yxx)\,P\,Q \to_\beta Q\,P\,P$$

$$Q\,P = P\,P \to_\beta \lambda y.\,PyP$$

$$\lambda y.\,PyP\,P \to_\beta P\,P\,P \to_\beta \ldots$$

Тоже не завершается. Оба терма не имеют нормальной формы, оба расходятся одинаково (через $P\,P\,\ldots$).

$$\boxed{\text{Термы } =_{\beta\eta}\text{ равны (оба не имеют н.ф., редуцируются к одной и той же бесконечной последовательности)}}$$

Строго: оба не имеют нормальной формы; по теореме Чёрча–Россера равенство $=_{\beta}$ означает наличие общего редукта. Проследим: левый $\twoheadrightarrow PQP \twoheadrightarrow QPQ \twoheadrightarrow \ldots$, правый $\twoheadrightarrow PPP \twoheadrightarrow \ldots$ — общего нормального редукта нет, значит не равны в $=_\beta$ (нет общего редукта в нормальной форме). Но поскольку оба расходятся, из Church–Rosser напрямую равенство не следует.

$$\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$$

$$P\,P = \lambda y.\,PyP,\quad P\,P\,R = P\,R\,P$$

$$P\,R = \lambda y.\,R\,y\,P,\quad P\,R\,P = R\,P\,P$$

$$R\,P = (\lambda xy.yxy)\,P = \lambda y.\,y\,P\,y,\quad R\,P\,P = P\,P\,P \to \ldots$$

Расходится.

Правый:

$$(\lambda x.xx)\,R\,P \to_\beta R\,R\,P$$

$$R\,R = \lambda y.\,y\,R\,y,\quad R\,R\,P = P\,R\,P$$

Мы получили $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 = (\lambda xyzw.\; z\,(x\,y\,(x\,y\,y\,y\,z))\,w)\;\overline{5}\;\overline{3}\;(\lambda yfx.\,y\,f\,(y\,f\,x))\;(\lambda x.x)$$

Шаг 1. Подставим: $x:=\overline{5}$, $y:=\overline{3}$, $z:=Z$, $w:=I$, где $Z=\lambda yfx.\,yfx$ — это $\overline{2}$ в другой записи… Разберёмся.

Обозначим:

  • $x = \overline{5} = \lambda fx.f^5x$
  • $y = \overline{3} = \lambda fx.f^3x$
  • $z = Z = \lambda yfx.\,yf(yfx)$ — это умножение на 2 для чисел Чёрча? Нет, это $\overline{2}$! Действительно $\overline{2} = \lambda fx.f(fx)$, а $\lambda yfx.\,yf(yfx) = \lambda y.\overline{2}\,y$… Нет.

Проверим: $Z = \lambda yfx.\,yf(yfx)$. Это $\lambda y.\,\overline{2}\circ y$… На самом деле $Zn = \lambda fx.\,nf(nfx) = \overline{2}\cdot n$ (умножение числа Чёрча на 2, т.е. $Zn = 2n$).

Действительно: $(\lambda yfx.\,yf(yfx))\,n = \lambda fx.\,nf(nfx)$. А $\text{Add}\,n\,n = \lambda fx.\,nf(nfx)$. Так что $Z\,n = \overline{2n}$ — удвоение.

  • $w = I = \lambda x.x$

Шаг 2. Тело: $z\,(x\,y\,(x\,y\,y\,y\,z))\,w$

Вычислим изнутри:

$x\,y\,y\,y\,z$: Здесь $x = \overline{5}$, применяем к $y,y,y,z$:

$$\overline{5}\,y = \lambda x.\,y^5 x$$

$$\overline{5}\,y\,y = y^5\,y = y^6\,(\text{т.е. применить }y\text{ шесть раз})$$

Стоп, аккуратнее. $\overline{5} = \lambda fx.f^5x$, поэтому:

$$\overline{5}\,y\,y = y^5\,y$$

Это означает применить $y=\overline{3}$ пять раз к $y=\overline{3}$:

$$\overline{3}^5\,\overline{3}$$

$\overline{3}^5$ — это $\overline{3}$ применённое 5 раз как функция к числу:

$$\overline{3}^1\,\overline{3} = \overline{3}\,\overline{3} = \overline{3^3} = \overline{27}$$

$$\overline{3}^2\,\overline{3} = \overline{3}\,\overline{27} = \overline{3^4} = \overline{81}$$

Подождём — $\overline{m}\,\overline{n} = \overline{n^m}$ (в числах Чёрча $\overline{m}\,\overline{n} = \lambda fx.\overline{n}^m f\,x$, но $\overline{n}^m f = f^{n^m}$, поэтому $\overline{m}\,\overline{n} = \overline{n^m}$).

Итак:

$$\overline{5}\,\overline{3}\,\overline{3} = \overline{3}^5\,\overline{3} = \overline{3}\,(\overline{3}\,(\overline{3}\,(\overline{3}\,(\overline{3}\,\overline{3}))))$$

Вычислим последовательно:

  • $\overline{3}\,\overline{3} = \overline{3^3} = \overline{27}$
  • $\overline{3}\,\overline{27} = \overline{27^3} = \overline{19683}$
  • $\overline{3}\,\overline{19683} = \overline{19683^3}$ — числа растут как башенная экспонента.

Но у нас ещё $\overline{5}\,\overline{3}\,\overline{3}\,\overline{3}\,Z$ — это $(\overline{5}\,\overline{3}\,\overline{3})\,\overline{3}\,Z$. Подождём, разберём скобки.

Скобки: $x\,y\,y\,y\,z = ((((x\,y)\,y)\,y)\,z)$

  • $\overline{5}\,\overline{3} = \overline{3^5} = \overline{243}$ (так как $\overline{m}\,\overline{n}=\overline{n^m}$, $\overline{5}\,\overline{3}=\overline{3^5}=\overline{243}$)
  • $\overline{243}\,\overline{3} = \overline{3^{243}}$
  • $\overline{3^{243}}\,\overline{3} = \overline{3^{3^{243}}}$
  • $\overline{3^{3^{243}}}\,Z$: применить $Z$ ровно $3^{3^{243}}$ раз к $Z$… Стоп.

Последнее применение: $N\,Z$ где $N = \overline{3^{3^{243}}}$.

$N\,Z = \lambda fx.\,Z^N\,f\,x$… Нет: $N\,Z = Z^N$ как функция? Нет: $\overline{n}\,f = \lambda x.f^n x$, поэтому $N\,Z = \lambda x.\,Z^N x$ где $Z^N$ означает $Z$ composed $N$ times.

Поскольку $Z\,k = 2k$ (удвоение), $Z^N\,k = 2^N\,k$.

Так что $N\,Z = \lambda x.\,2^N\,x$, то есть это число Чёрча $\overline{2^N}$ где $N = 3^{3^{243}}$.

Пусть $K = x\,y\,y\,y\,z = \overline{2^{3^{3^{243}}}}$.

Шаг 3. $x\,y\,K = \overline{5}\,\overline{3}\,K$:

  • $\overline{5}\,\overline{3} = \overline{243}$ (как выше)
  • $\overline{243}\,K = K^{243}$…

Снова: $\overline{243}\,K = \lambda fx.\,K^{243}f\,x$.

Что такое $K^{243}\,f$? $K = \overline{2^{3^{3^{243}}}}$, поэтому $K\,f = \lambda x.f^{K'}\,x$ где $K' = 2^{3^{3^{243}}}$.

$K^2\,f = K\,(Kf) = K\,(\lambda x.f^{K'} x) = \lambda x.(f^{K'})^{K'} x = \lambda x.f^{K'^2}x$.

$K^{243} f = \lambda x.f^{K'^{243}} x$, т.е. $\overline{243}\,K = \overline{K'^{243}}$ где $K' = 2^{3^{3^{243}}}$.

Пусть $L = \overline{243}\,K = \overline{(2^{3^{3^{243}}})^{243}} = \overline{2^{243\cdot 3^{3^{243}}}}$.

Шаг 4. $z\,L\,w = Z\,L\,I$:

$$Z\,L = \lambda fx.\,Lf(Lfx) = \overline{2L'}$$

где $L' = 2^{243\cdot 3^{3^{243}}}$, итого $Z\,L = \overline{2^{243\cdot 3^{3^{243}}+1}}$.

Нет, аккуратнее: $Z\,n = 2n$ как натуральное число, т.е. $Z\,\overline{n} = \overline{2n}$.

$$Z\,L = \overline{2 \cdot 2^{243\cdot 3^{3^{243}}}} = \overline{2^{243\cdot 3^{3^{243}}+1}}$$

Шаг 5. $(Z\,L)\,I$: применяем число Чёрча к $I=\text{id}$.

$\overline{n}\,I = \lambda x.\,I^n\,x = \lambda x.x = I$.

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

Итог: после всех редукций получаем $(\lambda x.x)$ — тождественный комбинатор.

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

Идея: $\text{Even}\,n$ — применить функцию «переключить бит» $n$ раз к $\mathbf{T}$.

Функция «не»: $\text{Not} = \lambda b.\,b\,\mathbf{F}\,\mathbf{T}$.

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

Проверка:

  • $\text{Even}\,\overline{0} = \overline{0}\,\text{Not}\,\mathbf{T} = \mathbf{T}$ ✓ (0 чётное)
  • $\text{Even}\,\overline{1} = \text{Not}\,\mathbf{T} = \mathbf{F}$ ✓
  • $\text{Even}\,\overline{2} = \text{Not}\,(\text{Not}\,\mathbf{T}) = \mathbf{T}$ ✓

В развёрнутом виде (без имён):

$$\text{Even} = \lambda n.\,n\,(\lambda b.\,b\,(\lambda xy.y)\,(\lambda xy.x))\,(\lambda xy.x)$$

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

Идея (из императивного): в цикле храним пару $(fib(k), fib(k+1))$, на каждом шаге: $(a,b)\mapsto (b, a+b)$. Начало: $(0,1)$. После $n$ шагов первая компонента равна $fib(n)$.

Нужно:

  • Пары: $\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))$

Начало: $\text{Init} = \text{Pair}\,\overline{0}\,\overline{1}$

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

Проверка:

  • $n=0$: $\text{Fst}\,\text{Init} = \overline{0}$ ✓
  • $n=1$: $\text{Fst}\,(\text{Step}\,\text{Init}) = \text{Fst}\,(\text{Pair}\,\overline{1}\,\overline{1}) = \overline{1}$ ✓
  • $n=2$: $\text{Fst}\,(\text{Step}^2\,\text{Init}) = \text{Fst}\,(\text{Pair}\,\overline{1}\,\overline{2}) = \overline{1}$ ✓
  • $n=3$: $\text{Fst}\,(\text{Pair}\,\overline{2}\,\overline{3}) = \overline{2}$ ✓

В развёрнутом виде (без имён вспомогательных):

$$\text{Fib} = \lambda n.\,n\,(\lambda p\,f.\,f\,(p\,(\lambda ab.b))\,(\lambda fx.\,(p\,(\lambda ab.a))f((p\,(\lambda ab.b))fx)))\,(\lambda f.\,f\,(\lambda fx.x)\,(\lambda fx.fx))\,(\lambda ab.a)$$