\documentclass{beamer}

\usepackage[english,russian]{babel}
\usepackage[utf8]{inputenc}
\usepackage[all]{xy}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{etex}
\usepackage{stmaryrd}
\usepackage{bussproofs}

\usetheme{Szeged}
% \usetheme{Montpellier}
% \usetheme{Malmoe}
% \usetheme{Berkeley}
% \usetheme{Hannover}
\usecolortheme{beaver}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#4~\ref{#2:##1}}
\newenvironmentx{#2}[2][1=,2=]{
\ifthenelse{\equal{##2}{}}{\begin{h#2}}{\begin{h#2}[##2]}
\ifthenelse{\equal{##1}{}}{}{\label{#2:##1}}
}{\end{h#2}}
}

\newref[section]{thm}{theorem}{Theorem}
\newref{lem}{lemma}{Lemma}
\newref{prop}{proposition}{Proposition}
\newref{cor}{corollary}{Corollary}

\theoremstyle{definition}
\newref{defn}{definition}{Definition}

\newcommand{\cat}[1]{\mathbf{#1}}
\renewcommand{\C}{\cat{C}}
\newcommand{\Set}{\cat{Set}}
\newcommand{\Grp}{\cat{Grp}}
\newcommand{\Ab}{\cat{Ab}}
\newcommand{\Ring}{\cat{Ring}}
\renewcommand{\Vec}{\cat{Vec}}
\newcommand{\Hask}{\cat{Hask}}
\newcommand{\Agda}{\cat{Agda}}
\newcommand{\Mat}{\cat{Mat}}
\newcommand{\Num}{\cat{Num}}

\newcommand{\im}{\mathrm{Im}}
\newcommand{\bool}{\mathrm{Bool}}
\newcommand{\true}{\mathrm{true}}
\newcommand{\false}{\mathrm{false}}

\newcommand{\ev}{\mathrm{ev}}
\newcommand{\zero}{\mathrm{zero}}
\newcommand{\suc}{\mathrm{suc}}
\newcommand{\fst}{\mathrm{fst}}
\newcommand{\snd}{\mathrm{snd}}
\newcommand{\unit}{\mathrm{unit}}

\newcommand{\repl}{:=}
\renewcommand{\ll}{\llbracket}
\newcommand{\rr}{\rrbracket}

\newcommand{\pb}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\po}[1][dr]{\save*!/#1+1.2pc/#1:(1,-1)@^{|-}\restore}

\AtBeginSection[]
{
\begin{frame}[c,plain,noframenumbering]
\frametitle{План лекции}
\tableofcontents[currentsection]
\end{frame}
}

\makeatletter
\defbeamertemplate*{footline}{my theme}{
    \leavevmode
}
\makeatother

\begin{document}

\title{Теория категорий}
\subtitle{Декартово замкнутые категории}
\author{Валерий Исаев}
\maketitle

\section{Булевские объекты}

\begin{frame}
\frametitle{Копроизведение $1 \amalg 1$}
\begin{itemize}
\item В $\Set$ множество $\bool$ можно определить как копроизведение множеств $\{ \true \}$ и $\{ \false \}$, каждое из которых является терминальным.
\item Копроизведение $1 \amalg 1$ обычно обозначается как $2$.
\item Можно было бы в произвольной категории определить объект $\bool$ как копроизведение $1 \amalg 1$.
\item Но это недостаточно сильное определение. Мы не сможем никаких функций над ним определить.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Булевский объект}
\begin{itemize}
\item Пусть в $\C$ существуют все конечные произведения.
\item Тогда \emph{булевский объект} в $\C$ -- это объект $\bool$ вместе с парой морфизмов $\true, \false : 1 \to \bool$, удовлетворяющий следующему условию.
\item Для любых $f, g : A \to B$ существует уникальная стрелка $h : \bool \times A \to B$, такая что
\[ \xymatrix{ A \ar[rr]^-{\langle \true \circ !_A, id_A \rangle} \ar[drr]_{f} & & \bool \times A \ar[d]^h \\
                                                                             & & B
            }
\qquad \xymatrix{ A \ar[rr]^-{\langle \false \circ !_A, id_A \rangle} \ar[drr]_{g} & & \bool \times A \ar[d]^h \\
                                                                              & & B
            }
\]
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Булевский объект и 2}
\begin{itemize}
\item Любой булевский объект является 2.
\item Действительно, если в определении булевского объекта в качестве $A$ взять 1, то мы получим в точности универсальное свойство $1 \amalg 1$.
\item Следовательно булевский объект уникален с точностью до изоморфизма.
\item Но не любой объект, являющийся 2, является булевским.
\item Действительно, в категории групп 2 изоморфен 1.
\item Но булевский объект изоморфен 1 только в категориях предпорядка.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{if}
\begin{itemize}
\item Мы можем сконструировать морфизм $if : \bool \times (C \times C) \to C$, удовлетворяющий
\[ \xymatrix{ C \times C \ar[d]_{\langle \true \circ !, id \rangle} \ar[rd]^{\pi_1} \\
              \bool \times (C \times C) \ar[r]_-{if} & C
            }
\quad \xymatrix{ C \times C \ar[d]_{\langle \false \circ !, id \rangle} \ar[rd]^{\pi_2} \\
              \bool \times (C \times C) \ar[r]_-{if} & C
            } \]
\item Действительно, в определении $\bool$ возьмем $A = C \times C$, $B = C$, $f = \pi_1$ и $g = \pi_2$.
\item Тогда существует уникальная стрелка $\bool \times (C \times C) \to C$, удовлетворяющая условиям выше.
\end{itemize}
\end{frame}

\section{Декартово замкнутые категории}

\begin{frame}
\frametitle{Мотивация}
\begin{itemize}
\item Очередная конструкция, которую мы хотим обобщить, -- это множество/тип функций.
\item Эта конструкция называется по разному: экспонента, внутренний $Hom$.
\item Пусть $A$ и $B$ -- объекты декартовой категории $\C$. Тогда экспонента обозначаются либо $B^A$, либо $[A,B]$.
\item Какие операции должны быть определены для $B^A$.
\item Как минимум мы должны иметь аппликацию, которая обычно обозначается $\ev$ и является следующим морфизмом:
\[ \ev : B^A \times A \to B \]
\item Морфизм $\ev$ позволяет нам ``вычислять'' элементы $B^A$.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Элементы объекта (a side note)}
\begin{itemize}
\item В категории $\Set$ элементы множества $X$ соответствуют морфизмам из термнального объекта в $X$.
\item В произвольной категории (с терминальным объектом) мы можем определить элемент объекта таким же образом.
\item Но это не очень полезное определение, так как в произвольной категории объект не определяется своими элементами.
\item Например, в категории графов морфизмы из терминального графа в граф $X$ соответствуют петлям $X$.
\item Мы можем определить \emph{обощенный элемент} объекта $X$ как морфизм из произвольного объекта $\Gamma$ в $X$.
\item В категории графов вершины и ребра графа $X$ являются его обобщенными элементами (конечно, существует и много других обобщенных элементов этого графа).
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Определение}
\begin{itemize}
\item Благодаря морфизму $\ev$, мы можем думать об элементах $B^A$ как о морфизмах $A \to B$.
Мы еще должны сказать, что $B^A$ содержит \emph{все} такие морфизмы.
\item То есть мы должны сказать чему соответствуют обобщенные элементы $B^A$.
Ясно, что у нас должна быть биекция между обобщенными элементами $\Gamma \to B^A$ и морфизмами $\Gamma \times A \to B$.
\item Имея морфизм $f : \Gamma \to B^A$, мы можем построить его каррирование следующим образом:
\[ \Gamma \times A \xrightarrow{f \times id_A} B^A \times A \xrightarrow{\ev} B\]
\item Объект $B^A$ вместе с морфизмом $\ev : B^A \times A \to B$ называется \emph{экспонентой} $A$ и $B$,
если для любого $g : \Gamma \times A \to B$ существует уникальный $f : \Gamma \to B^A$ такой, что композиция стрелок в диаграмме выше равна $g$.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Примеры}
\begin{itemize}
\item Категория называется \emph{декартово замкнутой}, если она декартова и для любых ее объектов $A$ и $B$ существует их экспонента $B^A$.
\item $\Set$ -- декартово замкнута. Действительно, $B^A$ -- это просто множество функций из $A$ в $B$.
\item $\Agda$ -- декартово замкнута. Действительно, $B^A$ -- это просто тип функций из $A$ в $B$.
\item Все алгебраические категории, которые мы рассматривали, не являются декартово замкнутыми ($\Grp$, $\Vec$, $\Ring$, и т.д.).
\item Категория графов -- декартово замнута.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Объект натуральных чисел}
\begin{defn}
\emph{Объект натуральных чисел} в декартово замкнутой категории -- это объект $\mathbb{N}$ вместе с парой морфизмов $\zero : 1 \to \mathbb{N}$ и $\suc : \mathbb{N} \to \mathbb{N}$, удовлетворяющие условию, что
для любых других морфизмов $z : 1 \to X$ и $s : X \to X$ существует уникальная стрелка $h$, такая что диаграмма ниже коммутирует.
\[ \xymatrix{ 1 \ar[r]^\zero \ar[rd]_z  & \mathbb{N} \ar[r]^\suc \ar@{-->}[d]^h & \mathbb{N} \ar@{-->}[d]^h \\
                                        & X \ar[r]_s                            & X
            } \]
\end{defn}
\end{frame}

\begin{frame}
\frametitle{Свойства}
\begin{itemize}
\item Объект натуральных чисел уникален с точностью до изоморфизма.
\item В любой декартово замкнутой категории с объектом натуральных чисел можно определить все примитивно рекурсивные функции.
\item Морфизм $\suc : \mathbb{N} \to \mathbb{N}$ является расщепленным мономорфизмом.
\end{itemize}
\end{frame}

\section{Интерпретация лямбда исчисления}

\begin{frame}
\frametitle{Мотивация}
\begin{itemize}
\item Лямбда исчисление предоставляет синтаксис для (декартово замкнутых) категорий, а категории предоставляют семантику лямбда исчисления.
\item С одной стороны, лямбда исчисление позволяет просто описывать различные конструкции в категориях.
\item С другой стороны, различные конструкции в категориях могут мотивировать новые языковые конструкции для лямбда исчисления.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Лямбда исчисление как теория}
\begin{itemize}
\item Для любой (односортной) алгебраической теории можно определить множество термов этой теории, построив его индуктивно из функций этой теории и переменных.
\item Например, в теории групп множество термов будет включать такие термы как $x * inv(y)$ и $x * (y * inv(z)) * 1$, где $x,y,z$ -- переменные, а $*$, $inv$ и $1$ -- функции теории групп.
\item Типизированное лямбда исчисление можно определить как двусортную алгебраическую теорию.
\item Но мы вместо этого просто определим его ручками.
\item В лямбда исчислении у нас есть два сорта: сорт типов и сорт термов.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Термы лямбда исчисления}
\begin{itemize}
\item Типы строятся индуктивно из двух бинарных функций $\times$ и $\to$ и одной константы $\top$ (и переменных).
\item Термы строятся индуктивно согласно следующим правилам:
\begin{center}
\AxiomC{}
\UnaryInfC{$\vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\RightLabel{, $(x : A) \in \Gamma$}
\UnaryInfC{$\Gamma \vdash x : A$}
\DisplayProof
\end{center}
\end{itemize}

\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \unit : \top$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B$}
\BinaryInfC{$\Gamma \vdash (a,b) : A \times B$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\Gamma \vdash p : A \times B$}
\UnaryInfC{$\Gamma \vdash \fst\,p : A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p : A \times B$}
\UnaryInfC{$\Gamma \vdash \snd\,p : B$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\Gamma, x : A \vdash b : B$}
\UnaryInfC{$\Gamma \vdash \lambda x. b : A \to B$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash f : A \to B$}
\AxiomC{$\Gamma \vdash a : A$}
\BinaryInfC{$\Gamma \vdash f\,a : B$}
\DisplayProof
\end{center}
\end{frame}

\begin{frame}
\frametitle{Аксиомы лямбда исчисления}
Кроме того, у нас есть следующие аксиомы:
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B$}
\BinaryInfC{$\Gamma \vdash \fst\,(a,b) \equiv a : A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B$}
\BinaryInfC{$\Gamma \vdash \snd\,(a,b) \equiv b : B$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\Gamma \vdash t : \top$}
\UnaryInfC{$\Gamma \vdash \unit \equiv t : \top$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p : A \times B$}
\UnaryInfC{$\Gamma \vdash (\fst\,p,\,\snd\,p) \equiv p : A \times B$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\Gamma, x : A \vdash b : B$}
\AxiomC{$\Gamma \vdash a : A$}
\BinaryInfC{$\Gamma \vdash (\lambda x. b)\,a \equiv b[x \repl a] : B$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash f : A \to B$}
\UnaryInfC{$\Gamma \vdash \lambda x. f\,x \equiv f : A \to B$}
\DisplayProof
\end{center}
\end{frame}

\begin{frame}
\frametitle{Интерпретация лямбда исчисления}
\begin{itemize}
\item Что является моделями алгебраической теории лямбда исчисления (которую мы так и не построили)?
\item Это в точности декартово замкнутые категории!
\item Так как мы точно не определили эту теорию, то мы и не можем доказать это утверждение, но мы хотя бы можем проинтерпретировать лямбда исчисление в произвольной декартовой категории
(так же как термы теории групп можно проинтерпретировать в произвольной группе).
\item Пусть $\C$ -- декартово замкнутая категория.
Тогда мы будем интерпретировать типы как объекты категории, а термы как ее морфизмы.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Интерпретация типов}
\begin{itemize}
\item Интерпретацию типов и термов мы будем обозначать как $\ll - \rr$.
\item Тогда типы интерпретируются следующим образом:
\begin{align*}
\ll \top \rr & = 1 \\
\ll A \times B \rr & = \ll A \rr \times \ll B \rr \\
\ll A \to B \rr & = \ll B \rr^{\ll A \rr}
\end{align*}
\item Если $\Gamma = x_1 : A_1, \ldots x_n : A_n$, то мы можем определить интерпретацию $\Gamma$ как $\ll \Gamma \rr = \ll A_1 \rr \times \ldots \times \ll A_n \rr$.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Интерпретация термов}
\begin{itemize}
\item Теперь мы определим интерпретацию термов.
\item Если $\Gamma \vdash a : A$, то $\ll a \rr : \ll \Gamma \rr \to \ll A \rr$.
\item $\ll x_i \rr = \pi_i$ если $\Gamma = x_1 : A_1, \ldots x_n : A_n$.
\item $\ll \unit \rr = !_{\ll \Gamma \rr}$.
\item $\ll (a,b) \rr = \langle \ll a \rr, \ll b \rr \rangle$.
\item $\ll \fst\,p \rr = \pi_1 \circ \ll p \rr$.
\item $\ll \snd\,p \rr = \pi_2 \circ \ll p \rr$.
\item $\ll f\,a \rr = \ev \circ \langle \ll f \rr, \ll a \rr \rangle$, где $\ev : \ll B \rr^{\ll A \rr} \times \ll A \rr \to \ll B \rr$.
\item $\ll \lambda x. b \rr = \varphi(\ll b \rr)$, где $\varphi : Hom(\ll \Gamma \rr \times \ll A \rr, \ll B \rr) \simeq Hom(\ll \Gamma \rr, \ll B \rr^{\ll A \rr})$ -- функция каррирования из определения экспонент.
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Проверка аксиом}
\begin{itemize}
\item Разумеется нам нужно проверить, что эта интерпретация уважает аксиомы.
\item Для этого сначала нужно доказать лемму, что подстановка интерпретируется как композиция, то есть если $\Gamma, x : A \vdash b : B$ и $\Gamma \vdash a : A$,
то $\ll b[x := a] \rr = \ll b \rr \circ \langle id_{\ll \Gamma \rr}, \ll a \rr \rangle$.
Это легко сделать индукцией по $b$.
\item Теперь бета эквивалентность соответствуют тому, что функция каррирования и обратная к ней дают тождественную функцию при композиции,
а эта эквивалентность соответствует тому, что эти функции дают $id$ при композиции в обратном порядке.
\item Аксиомы для $\top$ и $\times$ легко следуют из определения произведений.
\end{itemize}
\end{frame}

\end{document}
