abstract-tt.tex

\documentclass{amsart}

\usepackage[english,russian]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{hyperref}
\usepackage[all]{xy}
\usepackage{verbatim}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{type1ec}
\usepackage{stmaryrd}
% \usepackage[T2A]{fontenc}

\providecommand\WarningsAreErrors{false}
\ifthenelse{\equal{\WarningsAreErrors}{true}}{\renewcommand{\GenericWarning}[2]{\GenericError{#1}{#2}{}{This warning has been turned into a fatal error.}}}{}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{\ref{#2:##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}{теорема}{Теорема}
\newref{lem}{лемма}{Лемма}
\newref{prop}{утверждение}{Утверждение}
\newref{cor}{следствие}{Следствие}

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

\theoremstyle{remark}
\newref{remark}{замечание}{Замечание}

\newcommand{\red}{\Rightarrow}
\newcommand{\deq}{\Leftrightarrow}
\renewcommand{\ll}{\llbracket}
\newcommand{\rr}{\rrbracket}
\newcommand{\cat}[1]{\mathbf{#1}}
\renewcommand{\C}{\cat{C}}
\newcommand{\Set}{\cat{Set}}
\newcommand{\ccat}{\cat{CCat}}

\numberwithin{figure}{section}

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

\begin{document}

\title{Абстрактные теории типов}

\author{Валерий Исаев}

% \begin{abstract}
% Abstract
% \end{abstract}

\maketitle

\section{Монадичность существенно алгебраических теорий}

Существенно алгебраические теории были определены в \cite{LPC}.
В \cite{EAT} было доказано, что класс моделей $\lambda$-арных существенно алгебраических теорий совпадает с классом локально $\lambda$-представимых категорий.
В \cite{monad-equational-presentation} было показано как любая финитарная монада на локально конечно представимой категории может быть представлена при помощи операций и уравнений.
В этом разделе мы приведем аналогичную конструкцию, но вместо локально представимых категорий мы будем работать с существенно алгебраическими теориями, таким образом, данное представление монад будет более синтаксическим.

Пусть $S$ -- некоторое множество, элементы которого мы будем называть видами теории.
Предпучки $\Set^S$ мы будем называть \emph{$S$-множествами}.
$S$-множества эквивалентно могут быть описаны как множества над $S$.
\emph{Сигнатура теории} -- это множество $\Sigma$ (элементы которого мы будем называть функциональными символами теории) вместе с функцией арности, сопоставляющей каждому функциональному символу $\sigma$ коллекцию видов $\{ s_i \}_{i < \alpha}$ для некоторого кардинала $\alpha$ и вид $s$.
В этом случае мы будем писать $\sigma : \Pi_{i < \alpha} s_i \to s$.
Домен $dom(\sigma)$ функционального символа $\sigma$ -- это $S$-множество, определяемое как множество мощности $\alpha$ вместе с функцией $i \mapsto s_i$.
Кодомен $cod(\sigma)$ функционального символа $\sigma$ -- это просто $s$.
Мы будем говорить, что сигнатура $\Sigma$ имеет арность $\lambda$, если для любого $\sigma \in \Sigma$ верно, что $|dom(\sigma)| < \lambda$.

Для любой сигнатуры $\Sigma$ и любого $S$-множества $X$ мы определяем $S$-множество термов $Term_\Sigma(X)$ индуктивным образом:
\begin{itemize}
\item Если $x \in X_s$, то $x \in Term_\Sigma(X)_s$.
\item Если $\sigma : \Pi_{i < \alpha} s_i \to s$ и для всех $i < \alpha$ $t_i \in Term_\Sigma(X)_{s_i}$, то $\sigma(t_i) \in Term_\Sigma(X)_s$.
\end{itemize}
Если $X$ -- некоторое $S$-множество, то $\Sigma$-уравнение со свободными переменными в $X$ -- это пара $\Sigma$-термов $(t_1, t_2) \in Term_\Sigma(X)^2_s$ для некоторого $s \in S$.
Такие уравнения мы будем записывать как $t_1 = t_2$.

\begin{defn}
\emph{Алгебраическая предтеория} $(\Sigma, E, Def)$ состоит из следующего набора данных:
\begin{itemize}
\item Сигнатуры $\Sigma$.
\item Множества $\Sigma$-уравнений $E$ со свободными переменными в произвольных $S$-множествах.
    Если $e \in E$, то $S$-множество свободных переменных $e$ мы будем обозначать $FV_e$.
\item Функции $Def$, сопоставляющей каждому $\sigma \in \Sigma$ множество $\Sigma$-уравнений со свободными переменными в $dom(\sigma)$.
\end{itemize}
\end{defn}
Алгребаическая предтеория $(\Sigma, E, Def)$ имеет арность $\lambda$, если $\Sigma$ имеет арность $\lambda$, для любого $e \in E$ верно, что $|FV_e| < \lambda$, и для любого $\sigma \in \Sigma$ верно, что $|Def(\sigma)| < \lambda$.

\emph{Частичная алгебра} $A$ сигнатуры $\Sigma$ состоит из $S$-множества $|A|$ вместе с коллекцией частичных функций $\sigma_A : Hom_{\Set^S}(dom(\sigma), |A|) \to |A|_{cod(\sigma)}$ для каждого $\sigma \in \Sigma$.
Морфизм частичных алгебр $A$ и $B$ -- это морфизм $S$-множеств $f : |A| \to |B|$ такой, что для любого $\sigma \in \Sigma$ верно, что если $\sigma_A$ определена на $a : dom(\sigma) \to |A|$, то $\sigma_B$ определена на $f \circ a$ и $\sigma_B(f \circ a) = f_{cod(\sigma)}(\sigma_A(a))$.
Композиция и тождественные морфизмы определяются через соответствующие операции в $\Set^S$.
Категория частичных алгебр сигнатуры $\Sigma$ обозначается $\cat{Palg}\Sigma$.

Пусть $X$ -- $S$-множество, $A$ -- частчиная алгебра сигнатуры $\Sigma$ и $t \in Term_\Sigma(X)_s$.
Тогда мы определим рекурсивно частичную функцию $\ll t \rr : Hom_{\Set^S}(X, |A|) \to |A|_s$, вычисляющую $t$ в $A$.
\begin{itemize}
\item Если $t \in X_s$, то $\ll t \rr(a) = a_s(t)$.
\item Если $t = \sigma(t_i)$, то $\ll \sigma(t_i) \rr(a) = \sigma_A(\ll t_i \rr(a))$.
\end{itemize}
Если $t_1 = t_2$ -- $\Sigma$-уравнение со свободными переменными в $X$, то мы будем говорить, что оно определено на $a : X \to |A|$, если $\ll t_1 \rr(a)$ и $\ll t_2 \rr(a)$ определены, и мы будем говорить, что это уравнение верно на $a$, если $\ll t_1 \rr(a) = \ll t_2 \rr(a)$ когда обе стороны уравнения определены.
Мы будем говорить, что $A$ удовлетворяет уравнению, если оно верно на всех $a : X \to |A|$.

\emph{Модель} алгебраической предтеории $(\Sigma, E, Def)$ состоит из частичной алгебры $A$ сигнатуры $\Sigma$, удовлетворяющей следующим условиям:
\begin{itemize}
\item $A$ удовлетворяет всем уравнениям в $E$.
\item Для любого $\sigma \in \Sigma$ и любого $a : dom(\sigma) \to |A|$ функция $\sigma_A$ определена на $a$ тогда и только тогда, когда каждое уравнение из $Def(\sigma)$ определено и верно на $a$.
\end{itemize}
Категория $\cat{Mod}T$ моделей предтеории $T$ определяется как полная подкатегория $\cat{Palg}\Sigma$ на моделях $T$.

Если $T_1 = (\Sigma_1, E_1, Def_1)$ и $T_2 = (\Sigma_2, E_2, Def_2)$ -- пара алгебраических предтеорий, то мы будем говорить, что $T_1$ является подтеорией $T_2$, и $T_2$ является надтеорией $T_1$, если $\Sigma_1 \subseteq \Sigma_2$, $E_1 \subseteq E_2$ и $Def_1$ является ограничением $Def_2$ на $\Sigma_1$.
Если $T_1$ -- подтеория $T_2$, то существует очевидный забывающий функтор $U_{T_2,T_1} : \cat{Mod}T_2 \to \cat{Mod}T_1$.
Мы будем говорить, что надтеория $T_2$ предтеории $T_1$ \emph{монадично представлена} над $T_1$, если для любого $\sigma \in \Sigma_2$ все уравнения из $Def_2(\sigma)$ являются $\Sigma_1$-уравнениями.

Алгребаическая предтеория $(\Sigma, E, Def)$ является \emph{алгебраической теорией}, если для любого $\sigma \in \Sigma$ множество $Def(\sigma)$ пусто.
Алгребаическая предтеория является \emph{существенно алгебраической теорией}, если она монадично представлена над некоторой алгебраической теорией.

Наша цель в этом разделе будет заключаться в доказательстве следующей теоремы:
\begin{thm}
Функтор $U : \C \to \cat{Mod}T$, сохраняющий $\lambda$-фильтрованные копределы, является строго монадическим тогда и только тогда, когда он изоморфен над $\cat{Mod}T$ функтору $U_{T',T} : \cat{Mod}T' \to \cat{Mod}T$ для некоторой предтеории $T'$, монадично представленной над $T$.
\end{thm}

Во-первых, для любой теории $T_2 = (\Sigma_2, E_2, Def_2)$, монадично представленной над $T_1 = (\Sigma_1, E_1, Def_1)$, мы сконструируем левый сопряженный функтор $F_{T_1,T_2} : \cat{Mod}T_1 \to \cat{Mod}T_2$ к $U_{T_2,T_1}$.
Пусть $A$ -- модель $T_1$.
Тогда мы определим отношения $\sim$ на множествах $Term_{\Sigma_2}(|A|)_s$ как минимальные отношения эквивалентности, удовлетворяющие следующим свойствам:
\begin{itemize}
\item Если $a_i \in |A|_{s_i}$ и $\sigma_A$ определена на $a_i$, то $\sigma(a_i) \sim \sigma_A(a_i)$.
\item Если $e = (t_1, t_2)$ -- уравнение из $E_2$ и $a : FV_e \to Term_{\Sigma_2}(|A|)$, то $\ll t_1 \rr(a) \sim \ll t_2 \rr(a)$.
\item Если $\sigma \in \Sigma_2$, $a, a' : dom(\sigma) \to |A|$ и $a_{s_i} \sim a'_{s_i}$, то $\sigma(a) \sim \sigma(a')$.
\end{itemize}
Теперь мы определим индуктивно подмножества $A'_s \subseteq Term_{\Sigma_2}(|A|)_s$.
\begin{itemize}
\item Если $a \in |A|_s$, то $a \in A'_s$.
\item Если $\sigma \in \Sigma_2$, $a : dom(\sigma) \to |A|$ и для любого уравнения $(t_1, t_2) \in Def_2(\sigma)$ верно, что $\ll t_1 \rr(a)$ и $\ll t_2 \rr(a)$ принадлежат $A'_{cod(\sigma)}$ и $\ll t_1 \rr(a) \sim \ll t_2 \rr(a)$, то $\sigma(a) \in A'_{cod(\sigma)}$
\end{itemize}

\section{Абстрактные теории типов}

В этом разделе мы определим существенно алгебраическая теория $T_1$ контекстов и подстановок.
Эта теория была введена в \cite{b-systems} немного в другом виде под именем B-систем.

Мы будем работать с фиксированным множеством видов $S = \{ Ty_n\ |\ n \in \mathbb{N} \} \cup \{ Tm_n\ |\ n \in \mathbb{N} \}$.
Алгебраическая теория $T_0 = (\Sigma_{T_0}, \varnothing)$ контекстов (и термов) состоит из функциональных символов $ft_n : Ty_{n+1} \to Ty_n$ и $ty_n : Tm_n \to Ty_n$.
Модели теории $T_0$ -- это предпучки на категории порядка $(S, \leq)$, где $\leq$ порождается следуюшими соотношениями: $Tm_n \leq Ty_n$ и $Ty_{n+1} \leq Ty_n$.
Мы определяем производные термы $ft^k_n : Ty_{n+k} \to Ty_n$ как $ft^k_n(A) = ft_{n+k-1}( \ldots ft_n(A) \ldots )$.
Мы будем, как правило, опускать $n$ в нотации $ft^k_n$.

Теперь мы определим существенно алгебраическую теорию $T_1 = (\Sigma_{T_1}, E_{T_1}, Def_{T_1})$ контекстов и подстановок, которая будет надтеорией $T_0$.
Множество функциональных символов $\Sigma_{T_1}$ состоит из сиволов из $\Sigma_{T_0}$, а также символов
\begin{align*}
v_{n,0}     & : Ty_n \to Tm_{n+1} \\
Lift_{n,k}  & : Ty_n \times Ty_{n+k} \to Ty_{n+1+k} \\
lift_{n,k}  & : Ty_n \times Tm_{n+k} \to Tm_{n+1+k} \\
Subst_{n,k} & : Ty_{n+1+k} \times Tm_n \to Ty_{n+k} \\
subst_{n,k} & : Tm_{n+1+k} \times Tm_n \to Tm_{n+k}
\end{align*}
Функция $Def_{T_1}$ определяется следующим образом:
\begin{align*}
Lift_{n+1,k}(B, A)  & \text{ определено если } ft(B) = ft^{k+1}(A) \\
lift_{n+1,k}(B, a)  & \text{ определено если } ft(B) = ft^{k+1}(ty(a)) \\
Subst_{n+1,k}(B, a) & \text{ определено если } ft^{k+1}(B) = ty(a) \\
subst_{n+1,k}(b, a) & \text{ определено если } ft^{k+1}(ty(b)) = ty(a)
\end{align*}
На остальных символах $Def_{T_1}$ возвращает пустое множество.

\begin{comment}
Мы определяем производные термы $v_{n,i} : Ty_n \to Tm_{n+1}$ для любого $1 \leq i \leq n$, $Lift^i_{n,k} : Ty_{n+i-1} \times Ty_{n+k} \to Ty_{n+i+k}$ и $lift^i : Ty_{n+i-1} \times Tm_{n+k} \to Tm_{n+i+k}$ следующим образом:
\begin{align*}
v_{n+1,i+1}(A)         & := lift_{n+1,0}(A, v_{n,i}(ft_n(A))) \\
Lift^1_{n,k}(B, A)     & := Lift_{n,k}(B, A) \\
Lift^{i+1}_{n,k}(B, A) & := Lift_{n+i,k}(B, Lift^i_{n,k}(ft(B), A)) \\
lift^1_{n,k}(B, a)     & := lift_{n,k}(B, a) \\
lift^{i+1}_{n,k}(B, a) & := lift_{n+i,k}(B, lift^i_{n,k}(ft(B), a))
\end{align*}
Мы будем, как правило, опускать $n$ в нотации $v_{n,i}$, $Lift^i_{n,k}$ и $lift^i_{n,k}$ и писать просто $v_i$, $Lift^i_k$ и $lift^i_k$.
\end{comment}

Теперь мы опишем множество аксиом $E_{T_1}$:
\begin{align*}
ty(v_{n,0}(A))                      & = Lift_{n,0}(A, A) \\
ft(Lift_{n,0}(B, A))                & = B \\
ft(Lift_{n,k+1}(B, A))              & = Lift_{n,k}(B, ft(A)) \\
ty(lift_{n,k}(B, a))                & = Lift_{n,k}(B, ty(a)) \\
ft(Subst_{n+1,0}(B, a))             & = ft^2_n(B) \\
ft(Subst_{n,k+1}(B, a))             & = Subst_{n,k}(ft(B), a) \\
ty(subst_{n,k}(b, a))               & = Subst_{n,k}(ty(b), a) \\
subst_{n,0}(v_{n,0}(A), a)          & = a \\
subst_{n,k+1}(v_{n+1+k,0}(B), a)    & = v_{n+k,0}(Subst_{n,k}(B, a)) \\
Lift_{n,k+1}(B, Lift_{n+k,0}(A, C)) & = Lift_{n+1+k,0}(Lift_{n,k}(B, A), Lift_{n,k}(B, C)) \\
lift_{n,k+1}(B, lift_{n+k,0}(A, c)) & = lift_{n+1+k,0}(Lift_{n,k}(B, A), lift_{n,k}(B, c))
\end{align*}

\section{Предтеории}

Прежде чем мы определим абстрактные терии типов, нам понадобится понятие предтеории.
Предтеория -- это финитарная many-sorted алгебраическая теория с множеством видов $S = \{ Ty_n\ |\ n \in \mathbb{N} \} \cup \{ Tm_n\ |\ n \in \mathbb{N} \}$.
О виде $Ty_n$ мы думаем как о виде типов в контексте длины $n$, а о виде $Tm_n$ -- как о виде термов в контексте длины $n$.
Такие алгебраические теории могут быть описаны в терминах финитарных монад над категорией $\Set^S$ (см. \cite{LPC}).
Мы определяем \emph{категорию предтеорий} как категорию $Mnd_f(\Set^S)$ финитарных монад над $\Set^S$.

Мы опишем определенную предтеорию $T_0$.
Множество функциональных символов этой теории состоит из следующих символов:
\begin{itemize}
\item $ft_n : Ty_{n+1} \to Ty_n$ для всех $n \in \mathbb{N}$. Об этих символах мы думаем как об очевидных проекциях.
\item $ty_n : Tm_n \to Ty_n$ для всех $n \in \mathbb{N}$. Об этих символах мы думаем как об очевидных проекциях.
\item $v_{i,n} : Ty_n \to Tm_{n+1}$ для всех $n \in \mathbb{N}$, $0 \leq i \leq n$. Об этих символах мы думаем как о переменных, представленных в виде индексов Де Брёйна.
\item $Lift^i_{k,n} : Ty_n \to Ty_n$ для всех $i, n \in \mathbb{N}$, $k < n$. Об этих символах мы думаем как об операции поднятия типов.
\item $lift^i_{k,n} : Tm_n \to Tm_n$ для всех $i, n \in \mathbb{N}$, $k < n$. Об этих символах мы думаем как об операции поднятия термов.
\end{itemize}
Мы обычно будем опускать индекс $n$ в этих символах.

\begin{comment}
\section{Обобщенные существенно алгебраические теории}

Для определения абстрактных теорий типов нам понадобится формализм для описания алгебраических теорий.
Существует, по крайней мере, два таких формализма.
Первый носит имя существенно алгебраических теорий.
Его синтаксическое представление было описано в \cite{LPC}.
Другой вариант -- это обобщенные алгебраические теории, определенные Картмеллом (см. \cite{GAT}).
Эти представления эквивалентны в том смысле, что они имеют один и тот же класс алгебр.
Категория является алгеброй $\lambda$-арной существенно алгебраической теории тогда и только тогда, когда она является локально $\lambda$-представимой (см. \cite{LPC, EAT}).

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

\subsection{Описание синтаксиса}

Во-первых, определим понятие сигнатуры теории.
Пусть $\mathcal{S}$ -- некоторое множество, элементы которого мы будем называть \emph{родами}.
Теперь мы хотим определить понятие арности рода.
Идея заключается в том, что если род не зависит от аргументов, то у него фиксированная арность, которую мы обозначаем $1$.
Если род зависит от одного аргумента, то его арность должна специфицировать род этого аргумента $S_0$, который обязан быть арности $1$.
Если род зависит от двух аргументов, то его арность должна специфицировать род первого аргумента $S_0$, который обязан быть арности $1$, и род второго аргумента $S_1$, который может зависеть от первого аргумента, такую арность мы будем обозначать $\Sigma_{X \in S_0} S_1(X)$.
В общем случае арность рода -- это формальное выражение вида $\Sigma_{X_0 \in S_0(A^0_1, \ldots A^0_{n_0})} \ldots \Sigma_{X_k \in S_k(A^k_1, \ldots A^k_{n_k})}$,
где $S_i$ -- это рода, а $X_i$ и $A^i_j$ -- элементы некоторого фиксированного счетного множества переменных.
В последнем члене последовательности вместо $\Sigma_{X_k \in S_k(A^k_1, \ldots A^k_{n_k})}$ можно писать просто $S_k(A^k_1, \ldots A^k_{n_k})$, и пустая последовательность обозначается $1$.
Множество таких формальных выражений, в которых все $X_k$ различны и которые рассматриваются с точностью до переименования переменных, мы будем обозначать $Ar$.

Разумеется, выражения должны быть корректно составелны.
Для этого мы предполагаем, что на множестве родов задан некоторый фундированный порядок $<$.
Арности рода $S$ могут ссылаться только на такие рода $T$, что $T < S$.
Мы будем говорить, что функция $ar : \mathcal{S} \to Ar$ корректна, если для любого $S \in \mathcal{S}$, любого члена $\Sigma_{X_i \in S_i(A^i_1, \ldots A^i_{n_i})}$ последовательности $ar(S)$, верно, что $S_i < S$, $ar(S_i) = \Sigma_{A^i_1 \in T_1(B^1_1, \ldots B^1_{m_1})} \ldots \Sigma_{A^i_{n_i} \in T_{n_i}(B^{n_i}_1, \ldots B^{n_i}_{m_{n_i}})}$ для некоторых $T_i$ и $B^i_j$, и все члены последовательности $ar(S_i)$ встречаются в $ar(S)$ до $i$ позиции.

\begin{defn}
Сигнатура теории $\Sigma = (\mathcal{S}, \mathcal{F})$ состоит из множества родов $\mathcal{S}$ с фундированным порядком $<$ и корректной функции арности $ar : \mathcal{S} \to Ar$, а также множества функциональных символов $\mathcal{F}$ вместе с функцией арности $ar$, сопоставляющей каждому $f \in \mathcal{F}$ некоторый кардинал $ar(f)$.
\end{defn}

Пусть $\mathcal{F}$ -- некоторое множество, которое мы будем называть множеством функциональных символов.
Пусть для каждого $f \in \mathcal{F}$ выбран кардинал $ar(f)$, который мы будем называть его арностью.
Тогда для любого множества $V$ определим множество термов $Term_\mathcal{F}(V)$ индуктивным образом:
\begin{itemize}
\item Если $x \in V$, то $x \in Term_\mathcal{F}(V)$.
\item Если $f \in \mathcal{F}$ и $t : ar(f) \to Term_\mathcal{F}(V)$, то $f(t) \in Term_\mathcal{F}(V)$.
\end{itemize}
Если $ar(f) = n$ -- конечный кардинал, то $f(t)$ мы будем записывать как $f(t_0, \ldots t_{n - 1})$.

Существенно алгебраическая теория $T = (\mathcal{S}, \mathcal{F}, \mathcal{R}, \mathcal{I})$ состоит из множества родов $\mathcal{S}$, множества функциональных символов $\mathcal{F}$, множества предикатных симовлов $\mathcal{R}$ и множества аксиом $\mathcal{I}$.
Более того, каждому роду, каждому функциональному и каждому предикатному символу $x$ сопоставляется кардинал $ar(x)$, который называется его арностью.
Если $V$ -- некоторое множество, то атомарная формула со свободными переменными в $V$ -- это либо выражение вида $t = s$, где $t,s \in Term_\mathcal{F}(V)$, либо выражение вида $R(t)$, где $R \in \mathcal{S} \amalg \mathcal{R}$ и $t : ar(R) \to Term_\mathcal{F}(V)$.
Аксиома теории -- это выражение вида $\bigwedge_{i \in I} P_i \to C$ для некоторого множества $I$ и некоторых атомарных формул $\{ P_i \}_{i \in I}$ и $C$.
Формулы $P_i$ называются посылками аксиомы, а формула $C$ ее заключением.

Теперь мв перейдем к описанию алгебр теорий.
Если $T = (\mathcal{S}, \mathcal{F}, \mathcal{R}, \mathcal{I})$ -- существенно алгебраическая теория, то ее пред-алгебра $D = (|D|, \{ R_D \}_{R \in \mathcal{S} \amalg \mathcal{R}}, \{ f_D \}_{f \in \mathcal{F}})$ состоит из множества $|D|$, $\alpha$-местного предиката $R_D$ на $|D|$ для каждого $R \in \mathcal{S} \amalg \mathcal{R}$ такого, что $ar(R) = \alpha$, и $\alpha$-местной частичной функции $f_D$ на $|D|$ для каждого $f \in \mathcal{F}$ такого, что $ar(f) = \alpha$.
Если $\rho : V \to |D|$, то существует очевидная частичная функция $\overline{\rho} : Term_\mathcal{F}(V) \to |D|$, расширяющая $\rho$.
Мы будем говорить, что атомарная формула со свободными переменными в $V$ верна в означивании $\rho : V \to |D|$, если выполнено одно из следующих условий:
\begin{itemize}
\item Формула имеет вид $t = s$, $\overline{\rho}$ определена на $t$ и $s$ и $\overline{\rho}(t) = \overline{\rho}(s)$.
\item Формула имеет вид $R(t)$, $\overline{\rho}$ определена на $t_i$ для всех $i \in ar(R)$ и верно $R_D(\overline{\rho}(t))$.
\end{itemize}
Мы будем говорить, что аксиома $\bigwedge_{i \in I} P_i \to C$ выполнена в $D$, если во всех означиваниях, в которых верны все $P_i$, верна и $C$.

Пред-алгебра $D$ является алгеброй теории, если в ней выполнены все аксиомы из $\mathcal{I}$ и не существует сужения функций $f_D$ на подмножества их доменов такого, что все аксиомы при этом всё еще будут выполнены.
Смысл последнего условия заключается в том, что домены частичных функций $f_D$ должны быть не слишком велики и определяться множеством аксиом.
Заметим, что если в пред-алгебре $D$ выполнены аксиомы из $\mathcal{I}$, то существует уникальная алгебра $D' = (|D|, \{ R_D \}, \{ f_{D'} \})$, где $f_{D'}$ являются сужением $f_D$ на подмножества их доменов.

Нам осталось определить морфизмы алгебр.
Если $D$ -- алгебра теории $T$ и $S \in \mathcal{S}$, то мы будем обозначать $S(D)$ множество функций $t : ar(S) \to |D|$ таких, что верно $S(t)$.
Если $D$ и $D'$ - алгебры теории $T$, то морфизм $F : D \to D'$ состоит из коллекции функций $\{ F_S : S(D) \to S(D') \}_{S \in \mathcal{S}}$ такой,
что для любого $f \in \mathcal{F}$, любой $s : ar(f) \to \mathcal{S}$, любого $r \in \mathcal{S}$ и любой $t \in \Pi_{i \in ar(f)} (s(i)(D))$ верно,
что если $f_D(t)$ определено и $f_D(t) \in r(D)$, то $f_{D'}(i \mapsto F_{s(i)}(t(i)))$ определено и равно $F_r(f_D(t))$.

\subsection{Эквивалентность с классическим определением}
\end{comment}

\section{Абстрактные теории типов}

Сначала определим множество термов теории.
Пусть $\mathcal{F}$ -- произвольное множество, элементы которого мы будем называть функциональными символами.
Пусть $ar$ -- функция, которая каждому $f \in \mathcal{F}$ сопоставляет его арность $ar(f)$, которая является конечной последовательностью натуральных чисел.
Пусть $Var$ -- фиксированное счетное множество.
Тогда определим множество термов $Term_\mathcal{F}$ следующим образом:
\begin{itemize}
\item Если $x \in Var$, то $x \in Term_\mathcal{F}$.
\item Если $i \in \mathbb{N}$, то $v_i \in Term_\mathcal{F}$.
\item Если $k,n \in \mathbb{N}$ и $t \in Term_\mathcal{F}$, то $\Uparrow^k_n t \in Term_\mathcal{F}$.
\item Если $t, a_1, \ldots a_k \in Term_\mathcal{F}$, то $t[a_1, \ldots a_k] \in Term_\mathcal{F}$.
\item Если $f \in \mathcal{F}$, $ar(f) = (n_1, \ldots n_k)$ и $a_1, \ldots a_k \in Term_\mathcal{F}$, то $f(a_1, \ldots a_k) \in Term_\mathcal{F}$.
\end{itemize}
Термы $v_i$ -- это индексы де Брёйна, $t[a_1, \ldots a_n]$ -- операция подстановки, и $\Uparrow^k_n t$ -- операция поднятия индексов.
Термы из $Var$ являются метапеременными.

Теперь перейдем к описанию аксиом теории.
Пусть $\mathcal{R}$ -- произвольное множество, элементы которого мы будем называть предикатными символами.
Пусть $ar$ -- функция, которая каждому $R \in \mathcal{R}$ сопоставляет его арность $ar(f) \in \mathbb{N}$.
Тогда \emph{атомарная формула} -- это выражение, имеющее один из следующих видов:
\begin{itemize}
\item $t = s$, где $t, s \in Term_\mathcal{F}$
\item $R_k(t_1, \ldots t_{n+k})$, где $R \in \mathcal{R}$, $ar(R) = n$ и $t_1, \ldots t_{n+k} \in Term_\mathcal{F}$.
\item $Ty_k(t_1, \ldots t_{k+1})$, где $t_1, \ldots t_{k+1} \in Term_\mathcal{F}$.
\item $Tm_k(t_1, \ldots t_{k+2})$, где $t_1, \ldots t_{k+2} \in Term_\mathcal{F}$.
\end{itemize}
Зачастую первые $k$ аргументов $R_k$, $Ty_k$ и $Tm_k$ являются переменными.
В этом случае мы будем вместо последовательности этих переменных писать $\Gamma$.
Таким образом, формулы будут выглядеть как $Ty_k(\Gamma, A)$, $Tm_k(\Gamma, a, A)$ и $R_k(\Gamma, a_1, \ldots a_n)$, где $a, A, a_1, \ldots a_n$ -- некоторые термы.
\emph{Аксиома} -- это выражение вида $P_1 \land \ldots \land P_n \to C$, где $P_i$ и $C$ -- атомарные формулы.
Формулы $P_i$ называются посылками, а $C$ -- заключением аксиомы.

\begin{defn}
\emph{Асбтрактная теория типов} (АТТ) $T = (\mathcal{F}, \mathcal{R}, \mathcal{I})$ состоит из множества функциональных символов $\mathcal{F}$, множества предикатных символов $\mathcal{R}$, их арностей и множества аксиом $\mathcal{I}$.
\end{defn}

Приведем два примера АТТ.
Во-первых, теория $T_0 = (\varnothing, \varnothing, \varnothing)$.
Во-вторых, если $T_1 = (\mathcal{F}_1, \mathcal{R}_1, \mathcal{I}_1)$ и $T_2 = (\mathcal{F}_2, \mathcal{R}_2, \mathcal{I}_2)$ -- две АТТ,
то мы можем определить АТТ $T_1 \amalg T_2 = (\mathcal{F}_1 \amalg \mathcal{F}_2, \mathcal{R}_1 \amalg \mathcal{R}_2, \mathcal{I}_1 \amalg \mathcal{I}_2)$.
Когда мы определим морфизмы АТТ, эти два примера окажутся начальным объектом и копроизведением АТТ соответственно.

\subsection{Моделии АТТ}

Каждой АТТ $T$ мы сопоставим категорию моделей $Mdl(T)$.
Модель теории $T$ состоит из следующего набор данных:
\begin{itemize}
\item Диаграмма множеств вида
\[ \xymatrix{ \ldots        & B_3 \ar[d] & B_2 \ar[d] & B_1 \ar[d] \\
              \ldots \ar[r] & C_3 \ar[r] & C_2 \ar[r] & C_1
            } \]
Положим $C_0 = 1$.
Множество $C_i$ мы будем называть множествами контекстов длины $i$.
Множество сечений отображений $C_{i+1} \to C_i$ мы будем называть множеством типов в контексте $C_i$.
Множество сечений отображений $B_i \to C_i$ мы будем называть множеством термов в контексте $C_{i-1}$.
\end{itemize}

Теперь мы хотим каждой АТТ сопоставить монаду над категорией $\ccat$ контекстуальных категорий.
Тогда мы определим морфизмы теорий как морфизмы монад и модели теории как алгебры над этой монадой.
Для этого мы сначала сконструируем для каждой контекстуальной категории $C$ АТТ $Th(C)$.
Потом для каждой АТТ $T$ мы определим контекстуальную категорию $CCat(T)$.
После чего мы определим монаду $M_T : \ccat \to \ccat$ как $M_T(C) = CCat(T \amalg Th(C))$.

Пусть $C$ -- контекстуальная категория.
Определим теорию $Th(C)$.
Множество функциональных символов определяется как $\mathcal{F} = \{ O_A\ |\ A \in Ob(C), l(A) > 0 \} \amalg \{ M_f\ |\ f \in Hom(C), l(cod(f)) > 0 \}$.
Арности определяются следующим образом: $ar(O_A)$ равна последовательности нулей длины $l(A) - 1$, $ar(M_f)$ равна последовательности нулей длины $l(dom(f))$.
Множество $\mathcal{R}$ предикатных символов пусто.

Пусть теория $Th^0$ состоит из следующего набора формул:
\begin{itemize}
\item $\Uparrow^n_k v_i = \left\{\begin{array}{c l}
                                    v_i, & \text{ если } i < k \\
                                    v_{i + n}, & \text{ если } i \geq k
                                 \end{array}\right.$
\item Для всех $f \in \mathcal{F}$ таких, что $a_{\mathcal{F}}(f) = (s_1, \ldots s_m)$, формула \\
    $\forall a_1 \ldots \forall a_m (\Uparrow^n_k f(a_1, \ldots a_m) = f(\Uparrow^n_{k + s_1} a_1, \ldots \Uparrow^n_{k + s_m} a_m))$
\item $v_i[a_1, \ldots a_n] = \left\{\begin{array}{c l}
                                    a_{n - i}, & \text{ если } i < n \\
                                    v_{i - n}, & \text{ если } i \geq n
                                 \end{array}\right.$
\item Для всех $f \in \mathcal{F}$ таких, что $a_{\mathcal{F}}(f) = (s_1, \ldots s_m)$, формула $\forall a_1 \ldots \forall a_n \forall b_1 \ldots \forall b_m$ $(f(b_1, \ldots b_m)[a_1, \ldots a_n] = f(b_1[\Uparrow^{s_1} a_1, \ldots \Uparrow^{s_1} a_n], \ldots b_m[\Uparrow^{s_m} a_1, \ldots \Uparrow^{s_m} a_n]))$
\item Для всех $0 \leq i < m$ формула $\forall C_1 \ldots \forall C_m (Ty_{m - 1}(C_1, \ldots C_m) \to Tm_m(C_1, \ldots C_m, v_i, \Uparrow^{i + 1} C_{m - i}))$
\item $\forall C_1 \ldots \forall C_m \forall a_0 \ldots \forall a_n \forall A_0 \ldots \forall A_n \forall B (Tm_m(C_1, \ldots C_m, a_0, A_0) \land \ldots \land Tm_m(C_1, \ldots C_m, a_n, A_n[a_0, \ldots a_{n-1}]) \land Ty_n(A_1, \ldots A_n, B) \to Ty_m(C_1, \ldots C_m, B[a_0, \ldots a_n]))$
\item $\forall C_1 \ldots \forall C_m \forall a_0 \ldots \forall a_n \forall A_0 \ldots \forall A_n \forall b \forall B (Tm_m(C_1, \ldots C_m, a_0, A_0) \land \ldots \land Tm_m(C_1, \ldots C_m, a_n, A_n[a_0, \ldots a_{n-1}]) \land Tm_n(A_1, \ldots A_n, b, B) \to Tm_m(C_1, \ldots C_m, b[a_0, \ldots a_n], B[a_0, \ldots a_n]))$
\end{itemize}
Тогда определим теорию $Th^0_T$ как объединение $Th^0$ и $\mathcal{I}$.

\begin{comment}
\begin{defn}
\emph{Модель абстрактной теории типов} $T$ - это модель теории $Th^0_T$.
\end{defn}

Модели $T$ образуют категорию, это просто категория моделей $Th^0_T$.
Мы будем обозначать эту категорию $Mod(T)$.
\end{comment}

\subsection{Теории с равенством}

Абстрактная теория типов с равенством - это абстрактная теория типов с выбранными предикатными символами $eq$ и $Eq$ арности $3$ и $2$ соответственно.
Определим теорию $Th$ как объединение $Th^0$ и следующего набора формул:
\begin{itemize}
\item $\forall C_1 \ldots \forall C_m \forall a \forall a' \forall A (eq_m(C_1, \ldots C_m, a, a', A) \to a = a')$
\item $\forall C_1 \ldots \forall C_m \forall A \forall A' (Eq_m(C_1, \ldots C_m, A, A') \to A = A')$
\end{itemize}
Если $T$ - АТТ с равенством, то определим теорию $Th_T$ как объединение $Th$ и $\mathcal{I}$.

Модель АТТ с равенством - это модель теории $Th_T$.
Категория моделей $T$ будет обозначаться $Mod(T)$.
Любой АТТ $T$ можно сопоставить АТТ с равенством $T'$, добавив два новых предикатных символа $eq$ и $Eq$.
Заметим, что категории $Mod(T)$ и $Mod(T')$ могут быть различны.

\subsection{Модели теорий}

Пусть $D$ - модель теории $Th^0_T$.
Тогда построим контекстуальную категорию $U(D)$ следующим образом.
Множество объектов $Ob(U(D))_n$ определяется как следующее подмножество $D^n$:
\[ \{ (C_1, \ldots C_n) \in D^n\ |\ D \models Ty_i(C_1, \ldots C_{i + 1}) \text{ для всех } 0 \leq i < n \} \]
Множество морфизмов $Hom_{U(D)}((C_1, \ldots C_m), (B_1, \ldots B_n))$ определяется как следующее подмножество $D^n$:
\[ \{ (b_1, \ldots b_n) \in D^n\ |\ D \models Tm_m(C_1, \ldots C_m, b_{i + 1}, \Uparrow^m B_{i + 1}[b_1, \ldots b_i]) \text{ для всех } 0 \leq i < n \} \]
Тождественный морфизм $id_{(C_1, \ldots C_m)}$ определяется как $(v_{m - 1}, \ldots v_0)$.

\section{Абстрактные теории типов как монады}

\begin{defn}
\emph{Абстрактная теория типов} - это финитарная монада над категорией контекстуальных категорий.
\end{defn}

Во-первых, мы опишем общую схему построения ряда примеров абстрактных теорий типов.
Пусть $S$ - некоторое множество симовлов, каждому их которых сопоставлена конечная последовательность конечных множеств (его арность).
Эта функция будет обозначаться $ar : S \to FinSet*$.

Пусть $\C$ - контекстуальная категория.
Тогда для любого множества $V$ определим класс термов $Term(V)$ индуктивным образом:
\begin{itemize}
\item Если $x \in V$, то $v_x \in Term(V)$.
\item Если $A \in Ob(\C)_{n + 1}$ и $a_1, \ldots a_n \in Term(V)$ то $O(A, a_1, \ldots a_n) \in Term(V)$.
\item Если $A \in Ob(\C)_n$, $f : A \to B$ и $a_1, \ldots a_n \in Term(V)$, то $f(a_1, \ldots a_n) \in Term(V)$.
\item Если $s \in S$, $ar(s) = (X_1, \ldots X_n)$, $a_1 \in Term(V \amalg X_1), \ldots a_n \in Term(V \amalg X_n)$, то $s(a_1, \ldots a_n) \in Term(V)$.
\end{itemize}

Означивание - это фукнция вида $\rho : U \to Term(V)$.
Если $\rho$ - означивание и $X$ - множество, то означивание $\rho \amalg X : U \amalg X \to Term(V \amalg X)$ определяется как $(\rho \amalg X)(u) = Term(i)(\rho(u))$, если $u \in U$, где $i$ - вложение $V \to V \amalg X$, и $(\rho \amalg X)(x) = v_x$, если $x \in X$.

На множествах термов задается операция подстановки.
Если $a \in Term(U)$ и $\rho : U \to Term(V)$, то мы определяем терм $a[\rho] \in Term(V)$ рекурсией по $a$:
\begin{align*}
& v_x[\rho] = \rho(x) \\
& O(A, a_1, \ldots a_n)[\rho] = O(A, a_1[\rho], \ldots a_n[\rho]) \\
& f(a_1, \ldots a_n)[\rho] = f(a_1[\rho], \ldots a_n[\rho]) \\
& s(a_1, \ldots a_n)[\rho] = s(a_1[\rho \amalg X_1], \ldots a_n[\rho \amalg X_n]) \text{, если } ar(s) = (X_1, \ldots X_n)
\end{align*}

Класс $Ctx_n$ контекстов длины $n$ определяется индуктивно:
\begin{itemize}
\item $\diamond \in Ctx_0$.
\item Если $\Gamma \in Ctx_n$, $A \in Term(\{ 0, \ldots n - 1 \})$, то $\Gamma, A \in Ctx_{n + 1}$.
\end{itemize}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_1 : O(ft^n(A))\ \ldots\ \Gamma \vdash a_n : O(ft(A), a_1, \ldots a_{n-1})$}
\RightLabel{, $A \in Ty(X)_n$}
\BinaryInfC{$\Gamma \vdash O(A, a_1, \ldots a_n)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_1 : O(ft^n(ty(a)))\ \ldots\ \Gamma \vdash a_n : O(ft(ty(a)), a_1, \ldots a_{n-1})$}
\RightLabel{, $a \in Tm(X)_n$}
\BinaryInfC{$\Gamma \vdash H(a, a_1, \ldots a_n) : O(ty(a), a_1, \ldots a_n)$}
\DisplayProof
\end{center}
\medskip

Теперь определим отношения типизации $- \vdash$, $- \vdash -$, $- \vdash - : -$, $- \vdash - \deq -$ и $- \vdash - \deq - : -$ на классах $Ctx$, $Ctx \times Type$, $Ctx \times Term \times Type$, $Ctx \times Type \times Type$ и $Ctx \times Term \times Term \times Type$ соответственно.

\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$\diamond \vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash x : A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash x : A$}
\AxiomC{$\Gamma \vdash B$}
\RightLabel{, $y \notin \Gamma$}
\BinaryInfC{$\Gamma, y : B \vdash x : A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_1 : O(ft^n(A))\ \ldots\ \Gamma \vdash a_n : O(ft(A), a_1, \ldots a_{n-1})$}
\RightLabel{, $A \in Ob(\C)_{n+1}$}
\BinaryInfC{$\Gamma \vdash O(A, a_1, \ldots a_n)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_1 : O(ft^{n-1}(A))\ \ldots\ \Gamma \vdash a_n : O(A, a_1, \ldots a_{n-1})$}
\RightLabel{, $A \in Ob(\C)_n$, $B \in Ob(\C)_{m+1}$, $f : A \to B$}
\BinaryInfC{$\Gamma \vdash f(a_1, \ldots a_n) : O(B, \pi^m_B f(a_1, \ldots a_n), \ldots \pi_B f(a_1, \ldots a_n))$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_1 : O(ft^{n-1}(A))\ \ldots\ \Gamma \vdash a_n : O(A, a_1, \ldots a_{n-1})$}
\RightLabel{, $A \in Ob(\C)_n$, $B \in Ob(\C)_{m+1}$, $C \in Ob(\C)_{k+1}$, $f : A \to B$, $g : B \to C$}
\BinaryInfC{$\Gamma \vdash g f(a_1, \ldots a_n) \deq g(\pi^m_B f(a_1, \ldots a_n), \ldots f(a_1, \ldots a_n)) : O(C, \pi^k_C g f(a_1, \ldots a_n), \ldots \pi_C g f(a_1, \ldots a_n))$}
\DisplayProof
\end{center}
\medskip

К этим правилам также добавляются правила для символов из $S$.

Теперь мы можем определить контекстуальную категорию $T_S(\C)$.
Объекты этой категории - это контексты.
Для каждой пары контекстов $\Gamma$ и $\Delta = A_1, \ldots A_n$ мы определяем множество морфизмов $T_S(\C)(\Gamma, \Delta)$ как множество классов эквивалентностей множества последовательностей $(a_1, \ldots a_n)$ термов таких, что $\Gamma \vdash a_i : A_i[j \mapsto a_j]$.
Две такие последовательности $(a_1, \ldots a_n)$ и $(a_1', \ldots a_n')$ эквивалентны, если $\Gamma \vdash a_i \deq a_i' : A_i[j \mapsto a_j]$.

\section{Обобщенные алгебраические теории}

Большой класс примером абстрактных теорий типов строится при помощи обобщенных алгебраических теорий, которые были введены в \cite{GAT}.
Мы будем использовать определенный частный случай таких теорий и слегка модифицируем определение.

Обобщенная алгебраическая теория состоит из счетного множества переменных $Var$, множества символов $S$ и множества правил вывода, синтаксис описания которых приведен ниже.
По множествам $Var$ и $S$ мы строим множество выражений $Expr_S$ индуктивным образом:
\begin{itemize}
\item Если $v \in Var$, то $v \in Expr_S$.
\item Если $s \in S \cup \{ Ctx, Ty, Tm \}$, $e_1, \ldots e_n \in Expr_S$, то $s(e_1, \ldots e_n) \in Expr_S$.
\end{itemize}

Правило вывода состоит из последовательности посылок $P_1. \ldots P_n$ и заключения $C$.
Такое правило записывается как $P_1, \ldots P_n \implies C$ или как
\medskip
\begin{center}
\AxiomC{$P_1$}
\AxiomC{$\ldots$}
\AxiomC{$P_n$}
\TrinaryInfC{$C$}
\DisplayProof
\end{center}

Каждая посылка является парой из переменной $v$ и выражение $e$ и записывается как $v \in e$.
Заключения имеют один из следующих видов:
\begin{itemize}
\item Заключения, вводящие типы. Такие заключения состоят из пары выраженией $e$ и $\Gamma$ и записываются как $e \in Ty(\Gamma)$.
\item Заключения, вводящие термы. Такие заключения состоят из троек выраженией $e$, $\Gamma$ и $A$ и записываются как $e \in Tm(\Gamma, A)$.
\item Заключения, вводящие равенства типов. Такие заключения состоят из троек выраженией $e_1$, $e_2$ и $\Gamma$ и записываются как $e_1 = e_2 \in Ty(\Gamma)$.
\item Заключения, вводящие равенства термов. Такие заключения состоят из четверок выраженией $e_1$, $e_2$, $\Gamma$ и $A$ и записываются как $e_1 = e_2 \in Tm(\Gamma, A)$.
\end{itemize}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}