Main.tex

% !TEX encoding = UTF-8 Unicode
\documentclass[10pt,twoside]{article}
\usepackage[utf8]{inputenc}
\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm,bindingoffset=0cm]{geometry}
\usepackage[english,russian]{babel}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{hyperref,xcolor}
\usepackage{indentfirst}
\usepackage{tikz-cd}
\usepackage{comment}
\includecomment{comment}

\usetikzlibrary{cd}
\hypersetup{pdfstartview=FitH,  linkcolor=linkcolor,urlcolor=urlcolor, colorlinks=true}

\sloppy

\theoremstyle{plain}
\newtheorem{thm}{Теорема}
\newtheorem{lemma}{Лемма}
\newtheorem{corol}{Следствие}
\newtheorem{prop}{Предложение}
\newtheorem{ass}{Утверждение}
\newtheorem*{ass*}{Утверждение}
\newtheorem*{lemma*}{Лемма}
\theoremstyle{definition}
\newtheorem{defi}{Определение}
\newtheorem*{remark}{Замечание}
\newtheorem*{example}{Пример}
\newtheorem{problem}{Задача}
\newtheorem{question}{Вопросы}

\definecolor{linkcolor}{HTML}{0000FF} % цвет ссылок
\definecolor{urlcolor}{HTML}{0000FF} % цвет гиперссылок

\title{Лямбда Исчисление}
\author{Автор \href{http://vk.com/beizero}{Федоров И.И.}}

\begin{document}
\maketitle
\tableofcontents
\section{Необходимые понятия}
\subsection{Машина Тьюринга}
\subsubsection{Абстрактный автомат}

Абстрактный автомат (в теории алгоритмов) — математическая абстракция, модель дискретного устройства, имеющего один вход, один выход и в каждый момент времени находящегося в одном состоянии из множества возможных. На вход этому устройству поступают символы одного языка, на выходе оно выдаёт символы (в общем случае) другого языка.

\begin{defi}
Абстрактный автомат это пятёрка

$$M=(S,X,Y,\delta ,\lambda )$$
\begin{itemize}
\item $S$ — множество состояний автомата,
\item $X$, $Y$ — конечные входной и выходной алфавиты соответственно, из которых формируются строки, считываемые и выдаваемые автоматом,
\item $\delta :S\times X\rightarrow S$ — функция переходов,
\item $\lambda :S\times X\rightarrow Y$ — функция выходов.
\end{itemize}
Функционирование автомата в дискретные моменты времени $t$ может быть описано системой рекуррентных соотношений:
$${{s(t+1)=\delta (s(t),x(t))}}$$
$${{y(t)=\lambda (s(t),x(t))}}$$
\end{defi}
\begin{defi}
Абстрактный автомат с выделенным начальным состоянием называется инициальным автоматом. Таким образом абстрактный автомат определяет семейство инициальных автоматов $(s_{i},A),s_{i}\in S$.
\end{defi}
\begin{defi}
Если функции переходов и выходов однозначно определены для каждой пары ${{(s,x)\in S\times X}}$, то автомат называют детерминированным. В противном случае автомат называют недетерминированным или частично определенным. Если функция переходов и/или функция выходов являются случайными, то автомат называют вероятностным.
\end{defi}

\subsubsection{Конечный автомат}
\begin{defi}
Конечный автомат — абстрактный автомат, число возможных внутренних состояний которого конечно.
\end{defi}

\begin{defi} Конечный автомат без выхода это пятёрка
$$\displaystyle M=(A,S,s_{0},F,\delta )$$
\begin{itemize}
\item $A$ — входной алфавит (конечное множество входных символов), из которого формируются входные слова, воспринимаемые конечным автоматом;
\item $S$ — множество внутренних состояний;
\item $s_{0}$ — начальное состояние $(s_{0}\in S)$;
\item $F$ — множество допускающих состояний $(F\subset S)$;
\item $\delta$  — функция переходов, определенная как отображение $\displaystyle \delta \colon S\times A\rightarrow S$.
\end{itemize}
Принято полагать, что конечный автомат начинает работу в состоянии $s_{0}$, последовательно считывая по одному символу входного слова (цепочки входных символов). Считанный символ переводит автомат в новое состояние в соответствии с функцией переходов.
\end{defi}

\begin{defi}
Будем говорить, что автомат допускает (англ. accept) слово, если после окончания описанного выше процесса автомат окажется в допускающем состоянии.
\end{defi}

\begin{remark}
Если в какой-то момент из текущего состояния нет перехода по считанному символу, то будем считать, что автомат не допускает данное слово. При реализации вместо отдельного рассмотрения данного случая иногда удобно вводить фиктивную нетерминальную «дьявольскую вершину» (также тупиковое состояние, сток), из которой любой переход ведет в неё же саму, и заменить все несуществующие переходы на переходы в «дьявольскую вершину»
\end{remark}

\begin{defi}
Автоматы называются изоморфными (англ. isomorphic), если существует биекция между их вершинами такая, что сохраняются все переходы, терминальные состояния соответствуют терминальным, начальные — начальным.
\end{defi}

\begin{example}[Контролер нечетности единиц]
Задание распознающего автомата:
$$A=\{0,1\},S=\{Odd, Even\},s_0=Even,F=\{Odd\}$$
$$\delta(Even,0)=Even$$
$$\delta(Even,1)=Odd$$
$$\delta(Odd,0)=Odd$$
$$\delta(Odd,1)=Even$$
\end{example}

\begin{problem}
  Пусть $A=\{0,1,2,3,4,5,6,7,8,9\}$, убедиться что входная строка отсортирована по неубыванию.
\end{problem}

\begin{problem}
  Пусть $A=\text{русский алфавит}$, убедиться что входная строка содержит подстроку "саша".
\end{problem}

\begin{problem}
  Пусть $A=\text{латинский алфавит}$, убедиться что входная строка содержит подстроку "ababva".
\end{problem}

\subsubsection{Машина Тьюринга}

Неформально машина Тьюринга определяется как устройство, состоящее из двух частей: бесконечной одномерной ленты, разделённой на ячейки, головки, которая представляет собой детерминированный конечный автомат.
При запуске машины Тьюринга на ленте написано входное слово, причём на первом символе этого слова находится головка, а слева и справа от него записаны пустые символы. Каждый шаг головка может перезаписать символ под лентой и сместиться на одну ячейку, если автомат приходит в допускающее или отвергающее состояние, то работа машины Тьюринга завершается.
\begin{defi}
Формально машина Тьюринга (англ. Turing machine) определяется как кортеж из семи элементов $\langle A, a_0, S, Y, N, s_0, \delta \rangle$
\begin{itemize}
  \item $A$ — алфавит, из букв которого могут состоять входные слова,
  \item $a_0 \in A$ - пробельный символ(будем обозначать $B$),
  \item $S$ — множество состояний управляющего автомата,
  \item $Y \in S$ — допускающее состояние автомата,
  \item $N \in S$ — отвергающее состояние автомата,
  \item $s_0 \in S$ — стартовое состояние автомата,
  \item $\delta : S \times A \to S \times A \times \{ \leftarrow, \rightarrow, \downarrow \}$ — всюду определённая функция перехода автомата.
\end{itemize}
\end{defi}

\begin{defi}
  Назовём конфигурацией машины Тьюринга тройку (содержимое ленты, текущая позиция головки, текущее состояние машины).
\end{defi}

\begin{remark} Отличие машин Тьюринга от конечных автоматов:
  \begin{itemize}
    \item Машины Тьюринга могут как записывать данные на ленту так и считывать данные с ленты.
    \item Головка может передвигаться налево и направо.
    \item Необязательно считывать входные данные целиком. С другой стороны, вычисление может продолжаться (даже бесконечно) после того, как все входные данные были считаны.
    \item При достижении допускающего или недопускающего состояния вычисление останавливается.
  \end{itemize}
\end{remark}

\begin{defi}
Машина Тьюринга $M$ вычисляет функцию $f : B^* \to B^*$ (где $B$ — подмножество алфавита машины, не содержащее пустого символа), если для каждого $w$ из области определения функции $f$ результат работы $M$ равен $f(w)$, а для каждого $w$ не из области определения $f$ машина $M$ не останавливается на входе $w$.
\end{defi}

\begin{example}
Для начала приведём пример машины-преобразователя, которая прибавляет единицу к числу, записанному на ленте в двоичной записи. Алгоритм следующий:
\begin{itemize}
  \item в стартовом состоянии головка идёт вправо от старшего бита к младшему биту до первого пробельного символа, после чего переходит в состоянии $L$,
  \item в состоянии $L$ головка идёт влево от младшего бита к старшему и заменяет все единицы на нули,
  \item встретив ноль или пробельный символ головка записывает единицу и переходит в допускающее состояние $Y$.
\end{itemize}
Формально: $A = \{0, 1, B \}, S = \{L, R\}$. Таблица функции $\delta$ приведена ниже:\\
\begin{center}
\begin{tabular}{cccc}
& $0$ & $1$ & $B$\\
$R$ & $\langle R, 0, \rightarrow \rangle $ & $\langle R, 1, \rightarrow \rangle$ & $\langle L, B, \leftarrow \rangle$\\
$L$ & $\langle Y, 1, \downarrow \rangle$ & $\langle L, 0, \leftarrow \rangle$ & $\langle Y, 1, \downarrow \rangle$\\
\end{tabular}
\end{center}
\end{example}

\begin{problem}
  Реалиализовать машину Тьюринга которая прибавляет единицы в десятичной системе счисления.
\end{problem}

\begin{problem}
  Покажите, что функция «обращение», переворачивающая слово задом наперед, вычислима на машине Тьюринга.
\end{problem}

\begin{problem}
  Реализуйте машину Тьюринга которая осуществляет сложение 2х чисел в двоичной системе счисления.
\end{problem}

\begin{thm}[О существовании универсальной машины Тьюринга]
  Существует машина Тьюринга, которая может заменить собой любую машину Тьюринга. Получив на вход программу и входные данные, она вычисляет ответ, который вычислила бы по входным данным машина Тьюринга, чья программа была дана на вход.
\end{thm}

\begin{problem}
  Реализовать универсальную машину Тьюринга.
\end{problem}

\begin{defi}
  Вычислимые функции — это множество функций вида $f\colon N\to N$, которые могут быть реализованы на машине Тьюринга. Задачу вычисления функции $f$ называют алгоритмически разрешимой или алгоритмически неразрешимой, в зависимости от того, возможно ли написать алгоритм, вычисляющий эту функцию.
\end{defi}

\begin{example}
  Любая функция с конечной областью определения вычислима.
\end{example}

\subsubsection{Тезис Чёрча-Тьюринга}

Тезис Чёрча—Тьюринга — фундаментальное утверждение для многих областей науки, таких, как теория вычислимости, информатика, теоретическая кибернетика и др. Это утверждение было высказано Алонзо Чёрчем и Аланом Тьюрингом в середине 1930-х годов.

В самой общей форме оно гласит, что любая интуитивно вычислимая функция является частично вычислимой, или, эквивалентно, может быть вычислена с помощью некоторой машины Тьюринга.

Тезис Чёрча—Тьюринга невозможно строго доказать или опровергнуть, поскольку он устанавливает «равенство» между строго формализованным понятием частично вычислимой функции и неформальным понятием «интуитивно вычислимой функции».

Физический тезис Чёрча—Тьюринга гласит: Любая функция, которая может быть вычислена физическим устройством, может быть вычислена машиной Тьюринга.

\section{Чистое лямбда исчисление}
\subsection{Основные определения}
\subsubsection{Лямбда исчисление}
\begin{defi}
  Множество $\lambda$-термов $\Lambda$ строится из переменных $V=\{x,y,z\ldots\}$ следующим образом:
  $$x\in V \Rightarrow x\in \Lambda$$
  $$M, N \in \Lambda \Rightarrow (M\ N)\in \Lambda$$
  $$M\in \Lambda,x\in V\Rightarrow (\lambda x.M)\in\Lambda$$
\end{defi}

\begin{remark}
  Общеприняты следующие соглашения:
  \begin{itemize}
    \item Аппликация $\lambda$-термов левоассоциативна, т.е. $a\ b\ c\ d = ((a\ b)\ c)\ d$.
    \item Абстракция забирает себе всё, до чего дотянется: $\lambda x.\lambda y.\lambda z.z\ y\ x \equiv \lambda x.(\lambda y.(\lambda z.((z\ y)\ x)))$
    \item Внешние скобки опускаются.
    \item Вместо $\lambda x_1.\lambda x_2 \ldots \lambda x_n.M$ пишут $\lambda x_1\ldots\ x_n.M$.
  \end{itemize}
\end{remark}

\begin{example} Примеры $\lambda$-термов:
  $x$, $x\ y$, $x\ x$, $\lambda x.x$,$\lambda x.y$, $\lambda x.x\ y$
\end{example}

\begin{defi}
  Множество свободных переменных $FV(T)$ в $\lambda$-терме $T$ определяется следующим образом:
  $$FV(x)=\{x\}$$
  $$FV(M\ N)=FV(M)\cup FV(N)$$
  $$FV(\lambda x.M) = FV(M)\setminus \{x\}$$
\end{defi}

\begin{defi}
  Множество связанных переменных $BV(T)$ в $\lambda$-терме $T$ определяется следующим образом:
  $$BV(x)=\emptyset$$
  $$BV(M\ N)=BV(M)\cup BV(N)$$
  $$BV(\lambda x.M) = BV(M)\cup \{x\}$$
\end{defi}

\begin{defi}
  $M$ - замкнутый терм(или комбинатор), если $FV(M)=\emptyset$.
\end{defi}

\begin{example} Примеры комбинаторов:
  \begin{itemize}
    \item $I = \lambda x.x$
    \item $K = \lambda x\ y.x$
    \item $K_* = \lambda x\ y.y$
    \item $S = \lambda f\ g\ x.f\ x\ (g\ x)$
    \item $B = \lambda f\ g\ x.f\ (g\ x)$
  \end{itemize}
\end{example}

\begin{defi}
  Определим операцию подстановки $:=$ следующим образом:
  \begin{itemize}
    \item $x[x := T] = T$
    \item $y[x := T] = y$, если $x\neq y$
    \item $(M_1\ M_2)[x := T] = M_1[x := T]\ M_2[x := T]$
    \item $(\lambda x.M)[x := T] = \lambda x.M$
    \item $(\lambda y.M)[x := T] = \lambda y.(M[x:=T])$, если $x\neq y$ и либо $x \notin FV(M)$, либо $y \notin FV(T)$
    \item $(\lambda y.M)[x := T] = \lambda z.(M[y:=z][x:=T])$ в противном случае, причём $z \notin FV(M)\cup FV(T)$
  \end{itemize}
\end{defi}

\begin{defi}
  $\alpha$-конверсией(иногда $\alpha$-эквивалентностью или даже $\alpha$-редукцией) называется преобразование $\lambda x.A \to_\alpha \lambda y.A[x:=y]$ (все свободные вхождения переменной $x$ в $A$ заменяются на $y$; при этом переменная $y$ не должна входить в исходный терм $A$).
\end{defi}

\begin{defi}
  $\beta$-редукция называется преобразование $(\lambda x.A)\ B\to_\beta A[x:=B]$ (все свободные вхождения переменной $x$ в $A$ заменяются на терм $B$(при этом предполагается, что при подстановке в $A$ свободные переменные терма $B$ не попадают в область действия квантора по одноименным переменным)).
\end{defi}

\begin{defi}
  $\eta$-редукция называется преобразование $(\lambda x.A\ x)\to_\eta A$, если $x\notin FV(A)$.
\end{defi}

\begin{defi}
  Термы $A$ и $B$ называются равными, если существует цепочка $\lambda$-термов
  $$A\to C_1\to C_2 \to \dots\to C_n\to B$$
  где каждый следующий терм получается из предыдущего либо с помощью $\alpha$-конверсии, либо с помощью $\beta$-редукции, либо с помощью преобрзования обратного к $\beta$-редукции, либо с помощью $\eta$-редукции.
\end{defi}

\begin{defi}
  Говорят, что терм $A$ находится в нормальной форме, если к нему нельзя применить $\beta$-редукцию.
\end{defi}

\begin{defi}
  Говорят, что у терма $A$ есть нормальная форма, если существует эквивалентный терм в нормальной форме.
\end{defi}

\begin{problem}
  Придумать терм не имеющий нормальной формы.
\end{problem}

\begin{problem}
  Придумать терм который после применения $\beta$-редукции становится "больше".
\end{problem}

\subsubsection{Каррирование}

\begin{ass}[Шейнфинкель, 1924]
  Функция нескольких переменных может быть описана как конечная последовательность функций одной переменной.
  \begin{proof}
    Пусть $\phi(x,y)$ терм содержащий свободные переменные $x$ и $y$. Введём, путём последовательных абстракций
    $$\Phi_x = \lambda y.\phi(x,y)$$
    $$\Phi = \lambda x.\Phi_x = \lambda x.(\lambda y. \phi(x,y)) = \lambda x\ y.\phi(x,y)$$
    Тогда применение этого $\Phi$ к произвольным $X$ и $Y$ может быть выполнена последовательно
    $$\Phi\ X\ Y = (\Phi\ X)\ Y=\Phi_x\ Y=(\lambda y.\phi(X,y))\ Y=\phi(X,Y)$$
  \end{proof}
\end{ass}

\begin{defi}
  Каррирование (англ. carrying) — преобразование функции от многих переменных(функции от кортежа) в функцию, берущую свои аргументы по одному.
\end{defi}

\subsubsection{Свойства редукционных графов}

\begin{defi}
  Через $G_\beta(T)$, где $T$ это терм, будем обозначать редукционный граф. Вершинами этого графа являются термы, а стрелками $\beta$-редукции.
\end{defi}

\begin{defi}[Свойство сильной нормализуемости(SN)]
  Если любой путь исходящий из терма $T$ заканчивается, то говорят, что $G_\beta(T)$ обладает свойством сильной нормализуемости.
\end{defi}

\begin{defi}[Свойство слабой нормализуемости(WN)]
  Если существует путь приводящий терм $T$ к нормально форме, то говорят, что $G_\beta(T$) обладает свойством слабой нормализуемости.
\end{defi}

\begin{defi}[Свойство Чёрча-Россера(CR)]
  Если $A\twoheadrightarrow_\beta T_1$ и $A\twoheadrightarrow_\beta T_2$, а так же существует терм $U$ такой, что $T_1\twoheadrightarrow_\beta U$ и $T_2\twoheadrightarrow_\beta U$, то говорят, что $G_\beta(A)$ обладает свойством Чёрча-Россера.
\end{defi}

\begin{defi}[Слабое свойство Чёрча-Россера(WCR)]
  Если $A\to_\beta T_1$ и $A\to_\beta T_2$, а так же существует терм $U$ такой, что $T_1\twoheadrightarrow_\beta U$ и $T_2\twoheadrightarrow_\beta U$, то говорят, что $G_\beta(A)$ обладает слабым свойством Чёрча-Россера.
\end{defi}

\begin{thm}
  Для любого $T$:$G_\beta(T)$ обладает свойством CR.
  \begin{proof}
    Введём вспомогательное исчисление $\to_l$
    \begin{enumerate}
      \item $\forall T:T\to_l T$
      \item $T\to_l T':\lambda x.T\to_l\lambda x.T'$
      \item $T_1\to_l T_1',T_2\to_l T_2':(T_1\ T_2)\to_l (T_1'\ T_2')$
      \item $T_1\to_l T_1',T_2\to_l T_2':(\lambda x.T_1)\ T_2\to_l T_1'[x:=T_2']$
    \end{enumerate}
    \begin{ass*}
      $T\to_\beta T' \Rightarrow T \to_l T' \Rightarrow T\twoheadrightarrow_\beta T'$
      \begin{proof}
        Первая импликация следует из четвёртого правила, если подставить $T_1'=T_1,T_2'=T_2$.\\
        Последняя импликация доказывается индукцией по выводу $T \to_l T'$.
      \end{proof}
    \end{ass*}
    \begin{lemma}[О подстановке]
      $x\neq y, x\notin FV(V) \Rightarrow U[x:=W][y:=V] =_\alpha U[y:=V][x:=W[y:=V]]$
      \begin{proof}
        Очевидно.
      \end{proof}
    \end{lemma}
    \begin{lemma}
      $U\to_l U',V\to_l V':U[x:=V]\to_l U'[x:=V']$
      \begin{proof}
        Индукция по выводу $U\to_l U'$
        \begin{enumerate}
          \item $U \to_l U',U = U'$ - индукция по построению $U$
          \begin{enumerate}
            \item $U=a$
              \begin{enumerate}
                \item $a=x$, тогда $x[x:=V] \to_l x[x:=V'] = V\to_l V'$
                \item $a\neq x$, тогда $a[x:=V] \to_l a[x:=V'] = a\to_l a$
              \end{enumerate}
            \item $U=\lambda a.A$, тогда $A[x:=V] \to_l A[x:=V']$ и по правилу 2 $\lambda a.A[x:=V]\to_l \lambda a.A[x:=V']$
            \item $U=A_1\ A_2$, тогда $A_1[x:=V] \to_l A_1[x:=V']$ и $A_2[x:=V] \to_l A_2[x:=V']$, а по правилу 3 $(A_1\ A_2)[x:=V]\to_l (A_1\ A_2)[x:=V']$
          \end{enumerate}

          \item $U_1\to_l U_1':\lambda y.U_1\to_l\lambda y.U_1'$, где $U=\lambda y.U_1, U'=\lambda y.U_1'$, тогда можно применить предположение индукции сначала к $U_1\to U_1'$ и получить $U_1[x:=V]\to_l U_1'[x:=V']$, а потом воспользоваться правилом 2, тогда $\lambda y.U_1[x:=V]\to_l \lambda y.U_1'[x:=V']$.

          \item $U_1\to_l U_1',U_2\to_l U_2':(U_1\ U_2)\to_l (U_1'\ U_2')$, где $U=(U_1\ U_2), U'=(U_1'\ U_2')$, тогда можно применить предположение индукции сначала к $U_1\to U_1',U_2\to U_2'$ и получить $U_1[x:=V]\to_l U_1'[x:=V'],U_2[x:=V]\to_l U_2'[x:=V']$, а потом воспользоваться правилом 3, тогда $(U_1\ U_2)[x:=V]\to_l (U_1'\ U_2')[x:=V']$.

          \item $U_1\to_l U_1',U_2\to_l U_2':(\lambda y.U_1)\ U_2\to_l U_1'[x:=U_2']$, где $U=(\lambda y.U_1)\ U_2, U'=U_1'[x:=U_2']$.

          Хотим $(\lambda y.U_1[x:=V])\ U_2[x:=V]\to_l U_1'[y:=U_2'][x:=V']$

          По предположению индукции $U_1[x:=V]\to_l U_1'[x:=V'], U_2[x:=V]\to_l U_2'[x:=V']$ и по правилу 4 $(\lambda y.U_1[x:=V])\ U_2[x:=V]\to_l U_1'[x:=V'][y:=U_2'[x:=V']]$, а по лемме о подстановке $U_1'[x:=V'][y:=U_2'[x:=V']] =_\alpha U_1'[y:=U_2'][x:=V']$.
        \end{enumerate}
      \end{proof}
    \end{lemma}
    \begin{lemma}
      $\to_l$ обладает свойством ромба $V\to_l V_1,U\to_l V_2:V_1\to_l W, V_2\to_l W$.

      \begin{center}
        \begin{tikzcd}
          & V \arrow{ld}{l} \arrow{rd}{l} \\
          V_1 \arrow[dashed]{rd}{l} & & V_2 \arrow[dashed]{ld}{l} \\
          & W
        \end{tikzcd}
      \end{center}
      \begin{proof}
        Построим $W$ по индукциии
        \begin{enumerate}
          \item $V=V_1$, тогда в качестве $W$ нужно взять $V_2$.

            \begin{center}
                \begin{tikzcd}
                  V\arrow[loop left]{l}{l}\arrow{r}{l} & W \arrow[loop right]{l}{l}
                \end{tikzcd}
            \end{center}
          \item $V=\lambda x.V',V_1=\lambda x.V_1', V'\to_l V_1'$, т.к. $\lambda x.V'\to_l V_2$ значит $V_2=\lambda x.V_2'$, получается, что $V'\to_l V_1',V'\to_l V_2'$ и по предположению индукции $V_1'\to_l W', V_2'\to_l W'$, а значит $W=\lambda x.W'$.

            \begin{center}
              \begin{tikzcd}
                & V' \arrow{ld}{l} \arrow{rd}{l} \\
                V_1' \arrow{rd}{l} & & V_2' \arrow{ld}{l} \\
                & W'
              \end{tikzcd}
              \begin{tikzcd}
                & V = \lambda x.V' \arrow{ld}{l} \arrow{rd}{l} \\
                V_1 = \lambda x.V_1' \arrow{rd}{l} & & V_2 = \lambda x.V_2' \arrow{ld}{l} \\
                & W = \lambda x.W'
              \end{tikzcd}
            \end{center}
          \item $V = V'\ V'',V_1 = V_1'\ V_1''$
            \begin{enumerate}
              \item $V_2 = V_2'\ V_2''$

                \begin{center}
                  \begin{tikzcd}
                    & V' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1' \arrow{rd}{l} & & V_2' \arrow{ld}{l} \\
                    & W'
                  \end{tikzcd}
                  \begin{tikzcd}
                    & V'' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1'' \arrow{rd}{l} & & V_2'' \arrow{ld}{l} \\
                    & W''
                  \end{tikzcd}
                  \begin{tikzcd}
                    & V = V'\ V'' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1 = V_1'\ V_1'' \arrow{rd}{l} & & V_2 = V_2'\ V_2'' \arrow{ld}{l} \\
                    & W = W'\ W''
                  \end{tikzcd}
                \end{center}
              \item $V' = \lambda x.U$ получается $U\to_l U_2,V''\to_l V_2'',V=(\lambda x.U)\ V''\to_l U_2[x:=V_2'']=V_2$ и $V_1' = \lambda x.U_1$, тогда в качестве $W$ возьмём $U_3[x:=W'']$, где $U_1\to_l U_3, U_2\to_l U3$ и $V_1''\to_l W'',V_2''\to_l W''$.

                \begin{center}
                  \begin{tikzcd}
                    & V' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1' \arrow{rd}{l} & & V_2' \arrow{ld}{l} \\
                    & W'
                  \end{tikzcd}
                  \begin{tikzcd}
                    & V'' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1'' \arrow{rd}{l} & & V_2'' \arrow{ld}{l} \\
                    & W''
                  \end{tikzcd}
                  \begin{tikzcd}
                    & U \arrow{ld}{l} \arrow{rd}{l} \\
                    U_1 \arrow{rd}{l} & & U_2 \arrow{ld}{l} \\
                    & U_3
                  \end{tikzcd}
                  \begin{tikzcd}
                    & V = (\lambda x.U)\ V'' \arrow{ld}{l} \arrow{rd}{l} \\
                    V_1 = (\lambda x.U_1)\ V_2'' \arrow{rd}{l} & & V_2 = U_2[x:=V_2''] \arrow{ld}{l} \\
                    & W = U_3[x:=W'']
                  \end{tikzcd}
                \end{center}
            \end{enumerate}
          \item $V = (\lambda x.U)\ V'',V_1 = U_1[x:=U_1''], V_2 = U_2[x:=U_2'']$, тогда $W=U_3[x:=W'']$
        \end{enumerate}
      \end{proof}
    \end{lemma}
    \begin{lemma}
      $\to_l$ обладает свойством ленты т.е. $U\twoheadrightarrow_l U_n, U\to_l U':U_n\to_l W, U'\twoheadrightarrow_l W$.
      \begin{proof}
        Доказывается индукцией по $n$.
      \end{proof}
    \end{lemma}
    \begin{lemma}
      $\twoheadrightarrow_l$ обладает свойством ромба.

      \begin{center}
        \begin{tikzcd}
          & V \arrow[two heads]{ld}{l} \arrow[two heads]{rd}{l} \\
          V_1 \arrow[dashed, two heads]{rd}{l} & & V_2 \arrow[dashed, two heads]{ld}{l} \\
          & W
        \end{tikzcd}
      \end{center}
    \end{lemma}
    \begin{lemma}
      $\twoheadrightarrow_l = \twoheadrightarrow_\beta$
    \end{lemma}
  \end{proof}
\end{thm}

\subsubsection{Стратегии вычислений}

\begin{defi}
  Выражение вида $(\lambda x.T)\ A$ называется редексом.
\end{defi}

\begin{defi}[Полная бета-редукция]
  При полной бета-редукции в любой момент может сработать любой редекс.
\end{defi}

\begin{defi}[Нормальный порядок вычислений]
  При стратегии нормального порядка вычислений всегда сначала сокращает самый левый, самый внешний редекс.
\end{defi}

\begin{defi}[Вызов по имени]
  Стратегия вызова по имени работает так же как при нормальном порядке вычислений, но не позволяет проводить редукцию внутри абстракции.
\end{defi}

\begin{defi}[Вызов по значению]
  В соответствие со стратегией вызова по значению сокращаются только самые внешние редексы, и, кроме того, редекс срабатывает только в том случае, если его правая часть уже сведена к нормальной форме(значению), который уже вычислен и не может быть редуцирован.
\end{defi}

\begin{example}
  $$I\ (I\ (\lambda z.I\ z))$$
\end{example}

\begin{problem}
  Какие из вышеперечисленных стратегий могут не привести терм к нормальной форме даже если она есть?
\end{problem}

\begin{ass}
  Нормальный порядок вычислений всегда приводит терм к нормальной форме, если она есть.
\end{ass}

\subsection{Программирование на лямбда исчислении}

\subsubsection{Логические значения, пары и нумералы Чёрча}

\begin{defi}[Логические значения]
  $$TRUE = \lambda x.\lambda y.x$$
  $$FALSE = \lambda x.\lambda y.y$$
\end{defi}

\begin{problem}
  Придумать функции $NOT$, $AND$, $OR$, $IF$.
\begin{comment}
    $$IF = \lambda b.\lambda x.\lambda y.b\ x\ y$$
    $$NOT = \lambda b.IF\ b\ FALSE\ TRUE$$
    $$NOT = \lambda b.\lambda t.\lambda f.b\ f\ t$$
    $$AND = \lambda x.\lambda y.x\ y\ FALSE$$
    $$OR = \lambda x.\lambda y.x\ TRUE\ y$$
\end{comment}
\end{problem}

\begin{defi}[Пары]
  Функция $PAIR$ принимает два значения и запаковывает их в пару так, чтобы к ним можно было обращаться по $FST$ и $SND$.
  $$PAIR = \lambda x.\lambda y.\lambda f.f\ x\ y$$
\end{defi}

\begin{problem}
  Придумать функции $FST$, $SND$.
\begin{comment}
    $$FST = \lambda p.p\ TRUE$$
    $$SND = \lambda p.p\ FALSE$$
\end{comment}
\end{problem}

\begin{defi}[Нумералы Чёрча]
  Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число — это или ноль, или увеличенное на единицу натуральное число.
  $$\bar 0 = \lambda s.\lambda z.z$$
  $$\bar 1 = \lambda s.\lambda z.s\ z$$
  $$\bar 2 = \lambda s.\lambda z.s\ (s\ z)$$
\end{defi}

\begin{problem}
  Придумать термы $SUCC$, $PLUS$, $MULT$, $POW$, $IS\_ZERO$.
\begin{comment}
    $$SUCC = \lambda n.\lambda s.\lambda z.s\ (n\ s\ z)$$
    $$PLUS = \lambda n.\lambda m.\lambda s.\lambda z.n\ s\ (m\ s\ z)$$
    $$MULT = \lambda n.\lambda m.\lambda s.\lambda z.n\ (m\ s)\ z$$
    $$POW = \lambda n.\lambda m.\lambda s.\lambda z.m\ n\ s\ z$$
    $$IS\_ZERO = \lambda n. n\ (\lambda x.FALSE)\ TRUE$$
\end{comment}
\end{problem}

\begin{problem}
  Придумать функции $PRED$, $MINUS$.
  Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот.
\begin{comment}
    $$MINUS= \lambda n.\lambda m.m\ PRED n$$
    $$PRED = \lambda n.\lambda s.\lambda z.SND\ (n\ (\lambda p.PAIR\ (s\ (FST p))\ (FST p))\ (PAIR\ z\ z))$$
\end{comment}
\end{problem}

\begin{problem}
  Придумать функции для сравнения чисел.
\begin{comment}
    $$EQ = \lambda n.\lambda m.AND\ (IS\_ZERO\ (MINUS\ n\ m))\  (IS\_ZERO\ (MINUS\ m\ n))$$
    $$LEQ = \lambda n.\lambda m.(IS\_ZERO\ (MINUS\ n\ m))$$
    $$GEQ = \lambda n.\lambda m.(IS\_ZERO\ (MINUS\ m\ n))$$
    $$NEQ = \lambda n.\lambda m.NOT\ (AND\ (IS\_ZERO\ (MINUS\ n\ m))\  (IS\_ZERO\ (MINUS\ m\ n)))$$
\end{comment}
\end{problem}

\begin{defi}
  Список можно представить через его функцию свёртки $FOLD(REDUCE)$. Например, $[x,y,z] = \lambda c.\lambda n.c\ x\ (c\ y\ (c\ z\ n))$.
\end{defi}

\begin{problem}
  Как будет выглядеть $NIL$? Придумайте функцию $CONS$, которая принимает элемент и список, возвращает список вместе с этим элементом. Напишите функцию $IS\_NIL$, $HEAD$ и $TAIL$.
\begin{comment}
    $$NIL = \lambda c.\lambda n.n$$
    $$CONS = \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)$$
    $$IS\_NIL = \lambda l.l\ (\lambda h.\lambda t.FALSE)\ TRUE$$
    $$HEAD = \lambda l.l\ (\lambda h.\lambda t.h)\ NIL = \lambda l.l\ TRUE\ NIL$$
    $$TAIL = \lambda l.FST\ (l\ (\lambda x.\lambda p.PAIR\ (SND\ p)\ (CONS\ x\ (SND\ p)))\ (PAIR\ NIL\ NIL))$$
\end{comment}
\end{problem}

\subsubsection{Рекурсия}

\begin{thm}[О неподвижной точке]
  Для любого $\lambda$-терма $F$ существует такой $\lambda$-терм $X$, что $F\ X = X$. Такой терм $X$ называется неподвижной точкой $F$. Более того, существует такой комбинатор $Y$, что для любого $\lambda$-терма $F$ терм $Y\ F$ является неподвижной точкой $F$, т.е., $F\ (Y\ F) = Y\ F$. Комбинатор $Y$ называют комбинатором неподвижной точки.
\end{thm}

\begin{proof}
  Пусть $W = \lambda x.F\ (x\ x)$ и $X = W\ W$, тогда: $$X = W\ W = (\lambda x.F\ (x\ x))\ W = F\ (W\ W) = F\ X$$
\end{proof}

\begin{problem}[Комбинатор Хаскелла Карри]
  Доказать, что $Y = \lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x))$ комбинатор неподвижной точки.
\end{problem}

\begin{problem}[Комбинатор Алана Тьюринга]
  Доказать, что $\Theta = (\lambda x.\lambda y.y\ (x\ x\ y))(\lambda x.\lambda y.y\ (x\ x\ y))$ комбинатор неподвижной точки.
\end{problem}

\begin{problem}
  Убедиться, что функция $FACT$ вычисляет факториал числа $n$.
  $$g = \lambda fct.\lambda n.IF\ (IS\_ZERO\ n)\ \bar 1\ (MULT\ n\ fct\ (PRED\ n))$$
  $$FACT = Y g$$
\end{problem}

\begin{problem}
  Реализовать функцию вычисляющую $n$-ое число Фиббоначи.
\begin{comment}
    $$g = \lambda fib.\lambda n.IF\ (IS\_ZERO\ n)\ \bar 0\ (IF\ (EQ\ n\ \bar 1)\ \bar 1\ (PLUS\ (fib\ (PRED\ n))\ (fib\ (MINUS\ n\ \bar 2)))$$
    $$FIB = Y g$$
\end{comment}
\end{problem}


\end{document}