main.tex

\documentclass[openany]{book}

\usepackage[utf8]{inputenc}
\usepackage[T1, T2A]{fontenc}
\usepackage[greek.polytonic, russian]{babel}

\usepackage[a4paper, total={6in, 9in}]{geometry}

\usepackage{amssymb, amsthm, amsmath, amsfonts, bbm, float, listings, stmaryrd, pagecolor}
\usepackage{tikz-cd}

\usetikzlibrary{calc}

\usepackage[dvipsnames]{xcolor}

\usepackage{bbm}
\usepackage{hyperref}
\hypersetup{
    colorlinks = true,
    pdftitle={Теория типов},
    pdfsubject={Теория типов},
    pdfauthor={supxinfy},
    pdfkeywords={ 
        Теория типов
    },
    citecolor=ForestGreen,
}
\usepackage{graphicx}
\usepackage{nicefrac}
\usepackage{microtype}
\usepackage{cleveref}
\usepackage{url}
\usepackage{tikz}

\usetikzlibrary{positioning, shapes.geometric}
\usetikzlibrary{graphs} 
\usetikzlibrary{nfold}

\tikzset{fontscale/.style = {font=\relsize{#1}}
}

\usepackage{alphalph}
\usepackage{mathrsfs} 
\usepackage{upgreek} 
\usepackage{bussproofs}

\theoremstyle{plain}
\newtheorem{thm}{Теорема}[section]
\newtheorem{lem}[thm]{Лемма}
\newtheorem{prop}[thm]{Предложение}
\newtheorem{cor}{Следствие}	
\newtheorem{note}{Замечание}[section]

\theoremstyle{definition}
\newtheorem{defn}{Определение}[section]
\newtheorem{xrc}{Упражнение}[]
\newtheorem{eg}{Пример}[]

\newenvironment{sol}
{\begin{proof}[Решение]}
{\end{proof}}

\newcommand{\N}{\mathbb{N}}
\newcommand{\rec}{\mathrm{rec}}
\newcommand{\app}{\mathrm{app}}
\newcommand{\nat}{\mathsf{Nat}}

\date{\today}
\author{Шубин Владислав}
\title{Теория типов: Конспект}

\begin{document}

\maketitle
\tableofcontents

\chapter{Введение}
Теория типов представляет собой новое направление в логике, изучающее системы типов. С математической точки зрения существует два пути происхождения теории типов. Первый из них есть анализ математического текста, например из книги Шафаревича \cite{Shaph} мы видим следующее «для \(y \in Y\) и \(x \in f^{-1}(y)\) мы получаем уравнение \[t_i(x)^k + a_1(y)t_i(x)^{k-1}+\dots+a_k(y) = 0.\text{»}\]В этом контексте мы хотим анализировать подобные высказывания, которые понимаются, обычно, интуитивно. Например, здесь бессмысленно было бы сказать \(x \in \Bbbk\), по причине того, что \(x\) --- это точка аффинной схемы, но не элемент поля. В этом смысле они обладают разными «типами». Человек, знакомый с алгебраической геометрией, понимает, что \(k \in \N\), \(t_i : X \to \Bbbk\), \(a_i : Y \to \Bbbk\), где \(\Bbbk\) есть поле.

Подобные выражения недоступны в языке логики первого порядка и для того, чтобы оперировать с такой «математической грамматикой» нам понадобится теория типов

В теории типов мы, подобно символу \(\in\), используем символ \(:\), означающий «иметь тип». Например, \(x : A\) означает «\(x\) имеет тип \(A\)». Пусть у нас есть несколько типов \(x : A, y : B\), которые мы отделяем запятой. Если из них возможен вывод, мы его будем называть суждением, а посылку контекстом. То есть \[\underbrace{x : A, y : B}_{\text{контекст}} \vdash \underbrace{t : C}_{\text{суждение}}.\]

Кроме чисто математической точки зрения мы имеем довольно важную практическую сторону этой теории --- это языки программирования. С точки зрения компьютера (если у него, конечно, может быть какая-либо точка зрения) любые данные представляют из себя кусок бинарного кода. Картинки, программы, музыка --- все это есть лишь последовательность нулей и единиц. Поэтому в ранних языках программирования существовала проблема типизации. Для примера возьмем Си:
\begin{lstlisting}[language=C]
    void rev(char *str, int len){
        int start = 0;
        int end = len - 1;
        while(start < end) {
            char tmp = str[start];
            str[start] = str[end];
            str[end] = tmp;
            end--;
            start++;
        }
    }
\end{lstlisting}
Современный язык Си используем систему типов, в которой тип \texttt{char} представляет символьный тип. Однако, нет никакой существенной разницы между типами \texttt{char} и \texttt{short}, например (второй тип представляет однобайтовое число). Поэтому эту функцию можно применить и к массиву чисел, что создает существенные проблемы при разработке сложного ПО.

Из-за этой проблемы сформировалось, своего рода, ad hoc решение, называемое строгой типизацией. 

\begin{note}
    В математике любой объект можно представить как некоторое множество, однако это не лишает теорию типов приложимости. Нам важно, что натуральное число --- это не просто множество, а что-то новое, обладающее свойством «числа».
\end{note}

\begin{note}
    Заметим, что с философской точки зрения теория категорий является полностью независимой теорией оснований математики от теории множеств. Существует подход --- интуицианисткая теория типов, --- позволяющий вывести теорию категорий из теории типов. Иными словами, можно считать, что теория типов является более фундаментальным подходом к основаниям математики, чем другие теории.
\end{note}

\begin{eg}
    Можно представить следующий пример вычислений с типами 
    \begin{prooftree}
        \AxiomC{\(m, n: \N \vdash 2 \cdot m + n : \N\)}
        \AxiomC{\(\vdash 2 : \N\)}
        \BinaryInfC{\(\vdash 2 \cdot 5 + 3 : \N\)}
    \end{prooftree}
\end{eg}

\section{Простая теория типов}

Введем нашу первую модель теории типов формально. 
Типы мы определим как \[A := 1 \, | \, A_1 \times A_2 \, | \, \nat,\] то есть свободно порожденное множество с элементами \(1 \in \mathsf{Ty}\), \(\nat \in \mathsf{Ty}\), \(\times: \mathsf{Ty}^2 \to \mathsf{Ty}\). Под \(1\) мы имеем ввиду унарный тип. И, как и во всякой теории, нам понадобятся термы \[t := x \, | \, \langle \rangle \, | \, \langle t_1, t_2 \rangle \, | \, p_1(t) \, | \, p_2(t) \, | \, 0 \, | \, S(t) \, | \, \rec(...),\] где \(\rec\) --- рекурсия, чьи аргументы мы уточним позже.

Далее нам понадобится контекст, определяемый как \(\Gamma := \langle \rangle \, | \, \Gamma, x : A\), то есть контексты суть конечные списки переменных с типами (например, \(x_1 : A_1, \dots, x_n : A_n\)).

Теперь займемся суждением о типе --- отношении \(\Gamma \vdash t : A\) или «в контексте \(\Gamma\) переменная \(t\) имеет тип \(A\)» что аналогично «выводимости» в логике первого порядка.

\subsection{Аксиомы}
Первая часть правил будет относиться к так называемым структурным правилам. Под \(i\) мы будем иметь в виду любой тип в контексте.

Перечислим их:
\begin{itemize}
    \item (Axiom, Identity, Assumption)
        \begin{prooftree}
            \AxiomC{}
            \UnaryInfC{\(x_1 : A_1, \dots, x_n : A_n \vdash x_i : A_i\)}
        \end{prooftree}

    \item Подстановка (Substitution)
        \begin{prooftree}
            \AxiomC{\(\Delta \vdash s_i : A_i \quad \Gamma \vdash t : C\)}
            \UnaryInfC{\(\Delta \vdash t[s_i / x_i] : C\)}
        \end{prooftree}
\end{itemize}

Аксиоме подстановки подобны следующие аксиомы:
\begin{itemize}
    \itemОслабление (weakening):
    \begin{prooftree}
        \AxiomC{\(\Gamma \vdash t : A\)}
        \UnaryInfC{\(\Gamma, x : B \vdash t : A\)}
    \end{prooftree}
    \itemПерестановка (exchange):
    \begin{prooftree}
        \AxiomC{\(\Gamma x : A, y : B, \Delta \vdash t : C\)}
        \UnaryInfC{\(\Gamma, y : B, x : A, \Delta \vdash t : C\)}
    \end{prooftree}
    \itemЗамена одной переменной:
    \begin{prooftree}
        \AxiomC{\(\Gamma, x : A \vdash t : B\)}
        \AxiomC{\(\Gamma \vdash a : A\)}
        \BinaryInfC{\(\Gamma \vdash t [a/x] : B\)}
    \end{prooftree}
\end{itemize}

\begin{eg}
    Пример работы аксиомы подстановки
    \begin{prooftree}
        \AxiomC{\(y : \N \vdash y \cdot y : \N\)}
        \AxiomC{\(x_1, x_2 : \N \vdash x_1 + x_2 : \N\)}
        \BinaryInfC{\(x_1, x_2 : \N \vdash x_1 \cdot x_1 + x_2 \cdot x_2 : \N\)}
    \end{prooftree}
\end{eg}

\begin{note}
    Разница между \(\nat\) и \(\N\) фундаментальна. Первое --- это синтаксический класс, класс правил, которым натуральные числа следуют. Второе же --- это множество, поэтому мы используем его, подразумевая, что утверждения вроде \(y : \N \vdash y \cdot y : \N\) нам доказывать не нужно.
\end{note}

Мы будем пользоваться общей аксиомой подстановки, хотя, иногда имеет смысл ослабить систему теории типов.

\begin{note}
    Обычно, все доказательства в теории типов --- это индукция по типу или терму, с разбором всех случаев. Чем сильнее аксиома, тем больше существует особых случаев. Поэтому в некоторых теориях типов доказательства становятся очень большими и сложными с технической точки зрения.
\end{note}

Наша система все еще не является теорией типов, поскольку у нас нет правил вывода типов. Давайте их введем:
\begin{itemize}
    \item«Произведение»:
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash t_1 : A_1, \Gamma \vdash t_2 : A_2\)}
            \UnaryInfC{\(\Gamma \vdash \langle t_1, t_2\rangle : A_1 \times A_2\)}
        \end{prooftree}
    \item«Проекция»:
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash t : A_1 \times A_2\)}
            \UnaryInfC{\(\Gamma \vdash \pi_i(t) : A_i\)}
        \end{prooftree}
    \item«\(0\)»:
        \begin{prooftree}
            \AxiomC{\(\)}
            \UnaryInfC{\(\Gamma \vdash 0 : \nat\)}
        \end{prooftree}
    \item«\(S(n)\)»:
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash n : \nat\)}
            \UnaryInfC{\(\Gamma \vdash S(n) : \nat\)}
        \end{prooftree}
    \item«\(1\)»:
        \begin{prooftree}
            \AxiomC{\(\)}
            \UnaryInfC{\(\Gamma \vdash \langle \rangle : 1\)}
        \end{prooftree}
    \item«\(\rec\)»:
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash n : \nat\)}
            \AxiomC{\(\Gamma \vdash t_0 : C\)}
            \AxiomC{\(\Gamma, x : \nat, y : C \vdash t_s (x, y) : C\)}
            \TrinaryInfC{\(\Gamma \vdash \rec(t_0; (x, y \; . \; t_s); n) : C\)}
        \end{prooftree}
\end{itemize}

Чтобы определить рекурсию на \(n \in \N\) нам нужна база \(n = 0\) и индуктивный переход \(n = S(m)\). Для этого мы определяем пять переменных \(t_0, x, y, t_s\) и \(n\). Значение \(t_0\) и \(n\) понятно --- это начало и конец рекурсии. Переменные \(x, y\) суть предыдущий номер вызова, предыдущие значение. Переменная \(t_s\) и есть «следующий элемент» в индукции.

\begin{eg}

\end{eg}

Теперь мы ввели все, что нужно для теории типов. Однако, стоит учитывать один нюанс.

\subsubsection{Аннотации}

Давайте посмотрим внимательно на аксиому проекции
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t : A_1 \times A_2\)}
    \UnaryInfC{\(\Gamma \vdash \pi_i(t) : A_i\)}
\end{prooftree}
Из этой аксиомы нельзя точно понять, на каком типе определена функция \(\pi_i\), но мы видим этот тип из контекста. В теории типов существует аннотирование, которое приписывает на каком типе определена функция. С ней наша аксиома должна выглядеть как 
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t : A_1 \times A_2\)}
    \UnaryInfC{\(\Gamma \vdash \pi^{A_1, \, A_2}_i(t) : A_i\)}
\end{prooftree}
Аннотация присутствует всегда, но для читаемости ее не выписывают. Нам также необходимо аннотировать аксиомы пары, поскольку функция пары для каждого типа своя:
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t_1 : A_1, \Gamma \vdash t_2 : A_2\)}
    \UnaryInfC{\(\Gamma \vdash \langle t_1, t_2\rangle^{A_1, \, A_2} : A_1 \times A_2\)}
\end{prooftree}
Для рекурсии нужно аннотировать саму функцию \(\rec\):   
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash n : \nat\)}
    \AxiomC{\(\Gamma \vdash t_0 : C\)}
    \AxiomC{\(\Gamma, x : \nat, y : C \vdash t_s (x, y) : C\)}
    \TrinaryInfC{\(\Gamma \vdash \rec^C(t_0; (x, y \,.\, t_s); n) : C\)}
\end{prooftree} 

\begin{note}
    Аннотировать можно как и сверху \(\rec^C\), так и снизу \(\rec_C\). Для стройности изложения мы предпочтём аннотацию сверху.
\end{note}

\subsubsection{Упрощение выражений}

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

\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t_1 : A_1, \Gamma \vdash t_2 : A_2\)}
    \UnaryInfC{\(\Gamma \vdash \pi_i \langle t_1,\, t_2 \rangle \rightsquigarrow t_i : A_i\)}
\end{prooftree}

\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t_0 : C\)}
    \AxiomC{\(\Gamma, x : \nat, y : C \vdash t_s (x, y) : C\)}
    \BinaryInfC{\(\Gamma \vdash \rec^C(t_0; (x, y \,.\, t_s); 0) : C \rightsquigarrow t_0 : C\)}
\end{prooftree} 

\begin{prooftree}
    \AxiomC{\(\Gamma \vdash m : \nat\)}
    \AxiomC{\(\Gamma \vdash t_0 : C\)}
    \AxiomC{\(\Gamma, x : \nat, y : C \vdash t_s (x, y) : C\)}
    \TrinaryInfC{\(\Gamma \vdash \rec^C(t_0; (x, y\,.\, t_s); S(m)) \rightsquigarrow t_s [m/x, \rec^C(t_0; (x, y\,.\, t_s); m)/y] : C\)}
\end{prooftree} 

Проведем теперь испытание наших определений и ``запрограммируем'' что-нибудь. Начнем с функции суммы. Как известно \(x + 0 = x\) и \(x + S y = S(x + y)\). Тогда мы можем в нашей системе типов определить функцию \(\mathrm{add}(x, y)\) как

\begin{prooftree}
    \AxiomC{\(x, y: \nat \vdash y: \nat\)}
    \AxiomC{\(x, y: \nat \vdash x : \nat\)}
    \AxiomC{\(x,y,z,w : \nat \vdash S(w) : \nat\)}
    \TrinaryInfC{\(x,y:\nat \vdash \rec(x; z, w\,.\,S(w); y) : \nat\)}
    \UnaryInfC{\(\mathrm{add}(x, y)\)}
\end{prooftree}

Получается, что для каждого \(\Gamma \vdash x, y : \nat\) мы даем \(\Gamma \vdash \mathrm{add}(x, y) : \nat\).

\begin{eg}
    \[\mathrm{add}(S0, 0) \equiv \rec(S0; z, w\,.\, S(w); 0) \rightsquigarrow S0,\]
    то есть \(1 + 0 = 1\).

    \begin{align*}\mathsf{add}(SS0, SS0) \equiv \rec(SS0; z, w\,.\, S(w); SS0) \rightsquigarrow Sw [\rec(SS0; z, w\,.\, S(w); S0)/w] \equiv \\ \equiv S(\rec(SS0; z, w\,.\, S(w); S0)) \rightsquigarrow S(Sw[\rec(SS0; z, w, S(w); 0)]/w) \equiv \\ \equiv SS(\rec(SS0; z, w\,.\, S(w); 0)) \rightsquigarrow SSSS(0),\end{align*}
    действительно \(2 + 2 = 4\).
\end{eg}


Для умножения мы будем использовать уже введенную функцию \(\mathrm{add}(x, y)\). Как мы помним, \(m \cdot 0 := 0\), \(m \cdot S(n) := m \cdot n + m\). Тогда мы можем определить умножение как \(\mathsf{mult}(x, y) := \mathrm{rec}^{\nat} (0; (z, w, \mathsf{add}(w, x)); y)\), если \(x, y : \nat\).
\begin{eg}
    Как мы знаем, \(2 \times 2 = 4\), проверим
    \begin{align*}\mathsf{mult}(S(S(0)), S(S(0))) \equiv \mathrm{rec}^{\nat} (0; (z, w\,.\, \mathsf{add}(w, S(S(0)))); S(S(0))) \rightsquigarrow\\ \rightsquigarrow \mathsf{add}(w, S(S(0)))[\mathrm{rec}^{\nat} (0; (z, w\,.\, \mathsf{add}(w, S(S(0)))); S(0))/w]\rightsquigarrow\\ \rightsquigarrow \mathsf{add}(\mathrm{rec}^{\nat} (0; (z, w\,.\, \mathsf{add}(w, S(S(0)))); S(0)), S(S(0)))\rightsquigarrow \\ \rightsquigarrow  \mathsf{add}(\mathsf{add}(w, S(S(0)))[\mathrm{rec}^{\nat} (0; (z, w\,.\, \mathsf{add}(w, S(S(0)))); 0)/w], S(S(0)))\rightsquigarrow\\\rightsquigarrow \mathsf{add}(\mathsf{add}(\mathrm{rec}^{\nat} (0; (z, w\,.\, \mathsf{add}(w, S(S(0)))); 0), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(\mathsf{add}(0, S(S(0))), S(S(0))). \end{align*}
    И тогда
    \begin{align*}
        \mathsf{add}(\mathsf{add}(0, S(S(0))), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(\rec(0; z, w\,.\, S(w); SS0), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(Sw[\rec(0; z, w\,.\, S(w); S0)/w], S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(S(\rec(0; z, w\,.\, S(w); S0)), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(S(Sw[\rec(0; z, w\,.\, S(w); 0)]), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(S(S(\rec(0; z, w\,.\, S(w); 0))), S(S(0))) \rightsquigarrow\\\rightsquigarrow \mathsf{add}(S(S(0)), S(S(0))) \rightsquigarrow^* S(S(S(S(0)))).
    \end{align*}
    В последней стрелке \(\rightsquigarrow^*\) имеется ввиду множественность необходимых шагов вывода, которые мы опускаем, потому что сделали это в предыдущем примере.

\end{eg}
\begin{eg}
    Более интересно посмотреть на пример с числами Фибоначчи. Для этого мы определим пары \(p_n := \langle G_n, H_n \rangle\), где \(p_0 = \langle G_0, H_0 \rangle = \langle 0, 1 \rangle\) и \(p_{n+1} = \langle G_{n+1}, H_{n+1} \rangle = \langle H_n, G_n + H_n \rangle\). Тогда мы можем вычислить \(p_n\) следующим образом \[n : \nat \vdash \rec^{\nat \times \nat} (\langle 0, 1 \rangle; (z, w\,.\, \langle \pi_2 w\,.\, \mathsf{add}(\pi_1 w, \pi_2 w)\rangle); n).\]

    Тогда \(n\)-ое число Фибоначчи \(\mathsf{Fib}(n)\) есть \[n : \nat \vdash \pi_1(p_n) : \nat.\]
\end{eg}

\subsection{Логика первого порядка}

Мы много говорили о том, что теорию типов можно использовать как теорию оснований математики, но ничего не подобного ещё не доказали. В этом разделе мы слегка приоткроем эту дверь. Пусть у нас есть теория типов с \(1,  \times, \to\) (аналоги символов в логике первого порядка \(\top, \land, \implies\)). Тогда тип \(A\) будет соответствовать пропозиции \(A\) в логике первого порядка. Получается \(\Gamma \vdash a : A\) означает, что мы можем показать \(A\) и \(a\) --- это доказательство \(A\). Внимательный читатель может заметить, что эту систему можно обобщить не только для пропозиций. Тогда мы можем получить следующую таблицу
\begin{table}[H]
    \begin{tabular}{|l|l|l|}
        \hline
        \(A\) есть & \(a \in A\)                             & верно, что      \\ \hline
        множество  & \(a\) есть элемент множества \(A\)      & \(A\) не пусто  \\ \hline
        пропозиция & \(a\) есть доказательство \(A\)         & \(A\) истинно   \\ \hline
        проблема   & \(a\) есть метод решения проблемы \(A\) & \(A\) разрешимо \\ \hline
    \end{tabular}
    \centering
    \caption{Каждое суждение может быть прочитано по-разному}
\end{table}

Пользуясь уже введенным материалом мы можем доказать

\begin{prooftree}
    \AxiomC{\(\Gamma \vdash p : A \times B\)}
    \UnaryInfC{\(p : A \times B \vdash \pi_1(p) : A\)}
    \AxiomC{\(\Gamma \vdash p : A \times B\)}
    \UnaryInfC{\(p : A \times B \vdash \pi_1(p) : A\)} 
    \BinaryInfC{\(p: A \times B \vdash \langle \pi_1 p, \pi_1 p  : A \times A \rangle\)}
    \UnaryInfC{\(\vdash \lambda p \,.\, \langle \pi_1 p, \pi_1 p \rangle : A \times B \to A \times A\)}
\end{prooftree}

Это эквивалентно доказательству следующему в классической логике

\begin{prooftree}
    \AxiomC{\(\vdash A \land B\)}
    \UnaryInfC{\(\vdash A\)}
    \AxiomC{\(\vdash A \land B\)}
    \UnaryInfC{\(\vdash A\)} 
    \BinaryInfC{\(A \land A\)}
\end{prooftree}

То есть \(A \land B \implies A \land A\). Может возникнуть следующий вопрос, как нам находить противоречия в системе типов? Тип будет противоречивым, если не будет терма, удовлятворяющего этому типу. Чтобы найти противоречие в системе типов мы можем определить тип противоречия \(0\), который не будет иметь терма. Тогда в системе типов есть противоречие если найдется такой \(x\), что
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash c : 0\)}
    \UnaryInfC{\(\Gamma \vdash c(x) : A\)}
\end{prooftree}

То есть возможно \(0 \to A\). Отметим, что \(A \to 0\) эквивалентно \(\neg A\) и \(A \to (A \to 0)\) эквивалентно \(A \to \neg A\).

Однако, не всегда удобно вводить символ \(0\), поэтому иногда противоречивость определяется как возможность доказать все. Иными словами все доказуемо, или же, каждый тип имеет терм. Если система типов не противоречива, то, например, \(A \to A \times B\) не должен иметь терма.

\subsection{Формы суждений}

Пусть \(A\) тип, тогда мы имеем следующие формы суждений (индуктивно определенные независимые отношения):
\begin{itemize}
    \item \(\Gamma \vdash a:A\)
    \item \(\Gamma \vdash a \rightsquigarrow a':A\)
    \item \(\Gamma \vdash a \rightsquigarrow^* a':A\)
\end{itemize}

Обсуждаемые нами правила могут быть подразделены на следующие две категории:

\begin{itemize}
    \item выводимые (derivable): если существует вывод правила \(J\) из некоторых заданных допущений \(J_1, J_2, \dots, J_n\).
    \item допустимые (admissible): если из выводимости \(J_1, J_2, \dots, J_n\) следует выводимость \(J\).
\end{itemize}

Тогда в нашей системе относительно \(\rightsquigarrow^*\) будет верно, что
\begin{itemize}
    \item Следующее правило выводимо
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash a \rightsquigarrow a' : A\)}
            \AxiomC{\(\Gamma \vdash a' \rightsquigarrow a'' : A\)}
            \BinaryInfC{\(\Gamma \vdash a \rightsquigarrow^* a''\)}
        \end{prooftree}

    \item Следующее правило допустимо, но не выводимо
        \begin{prooftree}
            \AxiomC{\(\Gamma \vdash a \rightsquigarrow^* a' : A\)}
            \AxiomC{\(\Gamma \vdash a' \rightsquigarrow^* a'' : A\)}
            \BinaryInfC{\(\Gamma \vdash a \rightsquigarrow^* a''\)}
        \end{prooftree}
\end{itemize}

Однако, можно доказать, что выводимые правила являются допустимыми. Давайте приведем примеры допустимых правил, которые невыводимы.

Самым простым из них является 
\begin{prooftree}
    \AxiomC{\(J_1\)}
    \UnaryInfC{\(J_2\)}
\end{prooftree}
Действительно, из пустого набора правил нельзя произвести такое правило, однако, если \(J_1\) и \(J_2\) выводимы, то и все выражение выводимо.

Есть более интересный пример
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash S(n) : \nat\)}
    \UnaryInfC{\(\Gamma \vdash n : \nat\)}
\end{prooftree}
Подобная ситуация называется inversion principle: если тип построен правильно, то и подтип построен правильно. Очевидно, что из наших аксиом мы не можем вывести это правило, однако из выводимости предпосылок будет следовать выводимость самого правила.

Заметим еще одну интересную деталь. Выводимость сохраняется при расширении контекста, тогда как допустимость нет. Пусть \(J\) допустимо, тогда при добавлении правила, что из ничего выводится \(J\) нарушит допустимость \(J\).

\begin{lem}
    Если \(\Gamma \vdash a \rightsquigarrow a' : A\) выводимо, тогда \(\Gamma \vdash a : A\) и \(\Gamma \vdash a' : A\) выводимы.
\end{lem}

\begin{lem}
    Если \(\Gamma \vdash a \rightsquigarrow^* a' : A\) выводимо, тогда \(\Gamma \vdash a : A\) и \(\Gamma \vdash a' : A\) выводимы.
\end{lem}

\section{Модель теории множеств для теории типов}
Мы будем использовать стандартную модель, где для каждого типа \(A\) существует множество \(\llbracket A\rrbracket^\mathcal{M}\), где \(\mathcal{M}\) --- наша модель. Мы будем её опускать, поскольку она стандартная. Далее мы определяем множества рекурсивно по типу \(A\):
\begin{itemize}
    \item \(\llbracket 1 \rrbracket := 1\) (или любой другой синглтон)
    \item \(\llbracket A \times B \rrbracket := \llbracket A \rrbracket \times \llbracket B \rrbracket\)
    \item \(\llbracket \N \rrbracket := \N\)
\end{itemize}

Для контекста \(\Gamma = (x_1 : A_1, \dots, x_n : A_n)\) мы определяем множество \(\llbracket \Gamma \rrbracket := \prod_i \llbracket A_i \rrbracket\). Далее нам требуется рекурсивно определить правила типизации. Это можно сделать двумя способами. 

Мы для любого контекста \(\Gamma\) и типа \(A\) мы определим функцию \(\llbracket \Gamma \rrbracket \underset{\llbracket \Gamma \vdash t : A \rrbracket}{\to} \llbracket A \rrbracket\). Она будет правильно определена тогда и только тогда, когда соблюдены правила типизации. Иначе мы получим \(\mathrm{undefined}\). Итак, будем действовать рекурсивно по терму \(t\):
\begin{itemize}
    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash x : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{\pi_x}{\longrightarrow} \llbracket A \rrbracket & \text{если }(x:A) \in \Gamma,\\ \text{undefined} & \text{иначе}\end{cases}.\)

    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash \langle \rangle : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{}{\longrightarrow} \llbracket A \rrbracket = 1 & \text{если }A=1,\\ \text{undefined} & \text{иначе}\end{cases}.\)

    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash \langle a, b \rangle^{B_1 \times B_2} : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{\langle \llbracket \Gamma \vdash b_1 : B_1 \rrbracket, \llbracket \Gamma \vdash b_2 : B_2 \rrbracket \rangle}{\longrightarrow} \llbracket A \rrbracket = \llbracket B_1 \rrbracket \times \llbracket B_2 \rrbracket & \text{если }A=B_1 \times B_2,\\ \text{undefined} & \text{иначе}\end{cases}.\)

    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash \pi_i^{B_1, B_2} p : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{\pi_i \llbracket \Gamma \vdash p : B_1 \times B_2 \rrbracket}{\longrightarrow} \llbracket A \rrbracket & \text{если }A = B_i \in \Gamma,\\ \text{undefined} & \text{иначе}\end{cases}.\)

    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash 0 : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{0}{\longrightarrow} \llbracket \N \rrbracket & \text{если }A=\N \in \Gamma,\\ \text{undefined} & \text{иначе}\end{cases}.\)

    \item \(\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash S_n : A \rrbracket}{\longrightarrow} \llbracket A \rrbracket := \begin{cases}\llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash n : \N \rrbracket}{\longrightarrow} (\N \to \N) & \text{если }A = \N,\\ \text{undefined} & \text{иначе}\end{cases}.\)
\end{itemize}

\begin{note}
    Заметим, что \(\nat\) --- это синтаксический класс натуральных чисел, но не множество натуральных чисел \(\N\). 
\end{note}

В этой модели имеют место следующие результаты
\begin{lem}
    Если \(\Gamma \vdash t : A\), тогда \(\llbracket \Gamma \vdash t : A \rrbracket\) определен.
\end{lem}
\begin{proof}
    Эта лемма доказывается по индукции по \(\Gamma \vdash t : A\).
\end{proof}

\begin{lem}
    Если \(\Gamma'\)  есть расширение (супермножество) контекста \(\Gamma\) и \(\llbracket \Gamma \vdash t : A \rrbracket\) определен, то \(\llbracket \Gamma' \vdash t : A \rrbracket\) определен. В виде диаграммы это выглядит так     
    \begin{center}
        \shorthandoff{"} % Disable active character handling for "
        \begin{tikzcd}
            {\llbracket\Gamma'\rrbracket} && \llbracket A\rrbracket \\
                                          & \llbracket\Gamma\rrbracket
                                          \arrow[""{name=0, anchor=center, inner sep=0}, "", from=1-1, to=1-3]
                                          \arrow["{\textit{забывающий}}"', bend right=15, from=1-1, to=2-2]
                                          \arrow["{\llbracket\Gamma \vdash t:A\rrbracket}"', bend right=15, from=2-2, to=1-3]
                                          \arrow[shorten <=3pt, shorten >=5pt, equal, nfold, from=2-2, to=0]
        \end{tikzcd}
        \shorthandon{"} % Restore original behavior
    \end{center}
\end{lem}
\begin{proof}
    Мы доказываем это по индукции на \(t\). Разберем каждый случай. Начнем со случая когда \(t\) есть \(x_1\) (переменная), тогда если \(\llbracket \Gamma \vdash x_i:A \rrbracket\) определено, то легко видеть, что \(x_i[a_i/x_i] \equiv a_i\) и имеет место следующая диаграмма 

    \begin{center}
        \shorthandoff{"} % Disable active character handling for "
        \begin{tikzcd}
            {\llbracket\Gamma'\rrbracket} && \llbracket A\rrbracket \\
                                          & \llbracket\Gamma\rrbracket
                                          \arrow[""{name=0, anchor=center, inner sep=0}, "{\pi_i}", from=1-1, to=1-3]
                                          \arrow["{\textit{забывающий}}"', bend right=15, from=1-1, to=2-2]
                                          \arrow["{\pi_i}"', bend right=15, from=2-2, to=1-3]
                                          \arrow[shorten <=3pt, shorten >=5pt, equal, nfold, from=2-2, to=0]
        \end{tikzcd}
        \shorthandon{"} % Restore original behavior
    \end{center}

\end{proof}

\begin{lem}
    Для данных \(\Gamma, t, A\) и замена \(f : \Delta \to \Gamma\) (например, \(\Gamma = (x_i : A_i)_{i \in I}\), \(f = (a_i)_{i \in I}\), \(\Delta \vdash a_i : A_i\)), термы \((a_i)_{i \in I}\) и \(\Delta\), если \(\llbracket \Gamma \vdash t : C \rrbracket\) определено и каждый \(\llbracket \Delta \vdash a_i : A_i \rrbracket\) определен, тогда \(\llbracket \Delta \vdash t[a_i/x_i] : C \rrbracket\) определен и равен \[\llbracket \Delta \rrbracket \overset{\llbracket \Delta \vdash a_i : A_i \rrbracket}{\longrightarrow} \prod_i \llbracket A_i \rrbracket \vdash \llbracket \Gamma \rrbracket \overset{\llbracket \Gamma \vdash t : C \rrbracket}{\longrightarrow} \llbracket C \rrbracket.\]
\end{lem}
\begin{proof}
    По индукции на \(t\).
\end{proof}

\begin{eg}
    Пусть \(x_1, x_2, x_3 : \N \to x_1 \cdot x_2 \cdot x_3 : \N\) и \(\Delta = \omega : \N\). Построим такую замену для \(a_1 = \omega, a_2 = \omega + 1, a_3 = \omega + 2\) через \[(x_1 \cdot x_2 \cdot x_3)[a_i/x_i] = \omega (\omega + 1)(\omega + 2).\]
    \begin{center}
        \shorthandoff{"} 
        \begin{tikzcd}
            \N && {\N^3} && \N \\
            \omega && {(\omega, \omega+1, \omega+2)} \\
                   && {(x_1, x_2, x_3)} && {x_1\cdot x_2\cdot x_3} \\
            \omega &&&& {\omega (\omega+1)(\omega+2)}
            \arrow["{a_i}", from=1-1, to=1-3]
            \arrow["{x_1, x_2, x_3}", from=1-3, to=1-5]
            \arrow[maps to, from=2-1, to=2-3]
            \arrow[maps to, from=3-3, to=3-5]
            \arrow[maps to, from=4-1, to=4-5]
        \end{tikzcd}
        \shorthandon{"}
    \end{center}
\end{eg}

\subsection{Нормализация}

Под нормализацией в теории типов понимают приведение выражения к нормальной или упрощенной форме. Мы уже ввели правила редукции, если последовательное применение их приведет к выражению, которое уже не редуцируется, то мы его будем называть нормальным. Давайте введем эти определения
\begin{defn}
    Тип \(\Gamma \vdash t: A\) называется нормальным, если он максимален относительно редукции (\(\rightsquigarrow^*\))
\end{defn}

\begin{defn}
    Терм \(\Gamma \vdash t: A\) называется нормализируемым, если существует нормальный тип \(\Gamma \vdash t' : A\), такой что \(\Gamma \vdash t \rightsquigarrow^* t' : A\).
\end{defn}

Напомним, что если \(\vdash n : \nat\), то \(\underline{n}\) называется нумералом и обозначает \(S^n 0\).

\begin{eg}
    Как мы уже видели \(\vdash \underline{2} + \underline{2} : \N\), тогда этот терм нормализируем, поскольку \(\vdash \underline{2} + \underline{2} \rightsquigarrow \underline{4} : \N\).

    Терм же \(\vdash \underline{2} : \N\) нормален, поскольку не существует редукции для него.
\end{eg}

Как можно заметить по приведенному примеру, редукция совершает вычисление.

\begin{defn}
    Мы говорим, что теория типов (строго) нормализуема, если каждый терм (строго) нормализуем.
\end{defn}

\begin{thm}
    Теория типов с \(1, \times, \nat\) строго нормализуема.
\end{thm}

\begin{defn}
    Терм \(t\) сильно нормализируем, если любая редукция, в конечном счете, приводит к одной и той же нормальной форме \(t'\).
\end{defn}

Напомним некоторые правила редукции
\begin{itemize}
    \item \(\pi_1 \langle t_1, t_2 \rangle \rightsquigarrow t_1\)
    \item \(\pi_2 \langle t_1, t_2 \rangle \rightsquigarrow t_2\)
    \item \(\rec(d_0; x, y\,.\, d_s; 0) \rightsquigarrow d_0\)
    \item \(\rec(d_0; x, y\,.\, d_s; Sn) \rightsquigarrow d_s [n/x, \rec(d_0; x, y\,.\, d_s; n)/y]\)
\end{itemize}

Формы \(\pi_1, \pi_2\) и \(\rec\) являются элиминативными формами (elimination forms), поскольку они сводят термы к менее сложным.

Противоположны им конструкторы или интро формы (intro forms), такие как \(\langle\rangle, \langle\cdot,\cdot\rangle, 0, S\).

Существуют еще правила конгруэнции на \(\rightsquigarrow\) такие как 
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t \rightsquigarrow t' : \nat\)}
    \UnaryInfC{\(\Gamma \vdash St \rightsquigarrow St' : \nat\)}
\end{prooftree}

Чтобы доказать теорему о нормализируемости теории типов нам пригодится следующая лемма.
\begin{lem}
    Любой подтерм нормального терма нормален.
\end{lem}
\begin{proof}
    Очевидно из возможности редукции внутри терма.
\end{proof}

\begin{lem}
    Любой нормальный замкнутый терм \(\vdash t : A\) есть одна из следующих форм:
    \begin{enumerate}
        \item \(\Gamma \vdash \langle \rangle : 1\),
        \item \(\Gamma \vdash \langle t_1, t_2 \rangle : A \times B\), если \(t_1, t_2\) нормальны,
        \item \(\Gamma \vdash 0 : \nat\),
        \item \(\Gamma \vdash Sn : \nat\), если \(n\) нормален,
    \end{enumerate}
    то есть конструкторы с нормальными аргументами. Эта лемма называется канонической леммой (canonicity).
\end{lem}
\begin{proof}
    Будем доказывать индукцией по \(\Gamma \vdash t : A\). Если \(t\) является замкнутым нормальным термом, то он канонической формы. В самом деле, если \(t\) --- переменная, то нечего доказывать, поскольку \(t\) замкнуто. Если же \(t\) конструктор, то в силу того, что его аргументы нормальны и замкнуты (по предыдущей лемме) сам конструктор каноничен. И последний случай, когда \(t\) элиминативная форма, тогда будем доказывать от противного. Если аргументы \(t\) нормальны, то мы приходим к канонической форме из предыдущих случаев. То есть \(t\) не нормален; противоречие.
\end{proof}

Таким образом, мы описали все нормальные (замкнутые) термы в нашей теории типов. Из этого можно получить следующее следствие.
\begin{cor}
    Любой замкнутый нормальный терм вида \(\Gamma \vdash a : \nat\) представляется в виде \(\underline{n}\) для некоторого натурального \(n\). В общем случае для любого терма \(\Gamma \vdash t : B\), где \(\Gamma = (x_i : A_i)_i\) если \(\vdash a_i : A\) замкнуты и нормальны, то \(\vdash t[a_i/x_i]:B\) нормализуется.
\end{cor}
\begin{proof}
По индукции на \(\Gamma \vdash t:B\)
\begin{itemize}
\item 
\begin{prooftree}
    \AxiomC{\(\)}
    \UnaryInfC{\(\Gamma \vdash x_i : A_i\)}
\end{prooftree}
Этот случай тривиален.

\item 
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash t_i : A_i\)}
    \UnaryInfC{\(\Gamma \vdash \langle t_1, t_2 \rangle : A_1 \times A_2\)}
\end{prooftree}

По гипотезе индукции для каждого \(t_i\) при подстановке замкнутых нормальных термов для всех переменных нормализирует. По индукции имеем \(t_i [a_i/x_i]\) нормализирующий. Тогда
\[\vdash t_1 [a_i/x_i] \rightsquigarrow^* t'_1:A_1,\]
\[\vdash t_2 [a_i/x_i] \rightsquigarrow^* t'_2:A_2.\]
Следовательно
\[\vdash \langle t_1, t_2 \rangle [a_i/x_i] \rightsquigarrow^* \langle t'_1, t'_2 \rangle : A_1 \times A_2\]
Все остальное аналогично.
\item
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash p : B_1 \times B_2\)}
    \UnaryInfC{\(\Gamma \vdash \pi_1 p : B_1\)}
\end{prooftree}
Имеем \[(\pi_1 p)[a_i/x_i] := \underset{\text{По индукции нормализуется}}{\pi_1(p[a_i/x_i])}.\]
Тогда этот терм нормален по каноничности \(p' = \langle q_1, q_2\rangle\), значит \(\pi_1 p \rightsquigarrow^* \pi_1 \langle q_1, q_2 \rangle \rightsquigarrow q_1\) нормален.

\item
\begin{prooftree}
    \AxiomC{\(\Gamma \vdash d_0:B, \Gamma, y : \nat, z: B \vdash d_s : B, \Gamma \vdash t : \nat\)}
    \UnaryInfC{\(\Gamma \vdash \rec(d_0; (y, z . d_s); t) : B\)}
\end{prooftree}
Если \(\vdash a_i : A_i\) получаем \[\rec(\_)[a_i/x_i] := \rec(d_0[\_]; y, z . d_s[a_i/x_i], t[a_i/x_i])\]
Продолжение следует...
\end{itemize}
\end{proof}

\section{Функциональный тип}

Наша система имеет довольно слабую выразительную силу. В качестве упражнения, попробуйте записать в ней обыкновенное равенство двух натуральных чисел. На данный же момент наша система не имеет довольно естественной возможности оперировать с функциями. Для этого мы введем тип \(A \to B\).
\begin{itemize}
\item \begin{prooftree}
    \AxiomC{\(\Gamma, x: A \vdash b:B\)}
    \UnaryInfC{\(\Gamma \vdash (\lambda x : A . b) : A \to B\)}
\end{prooftree}

\item \begin{prooftree}
    \AxiomC{\(\Gamma, f: A \to B\)}
    \AxiomC{\(\Gamma \vdash a : A\)}
    \BinaryInfC{\(\Gamma \vdash \app^{A, B}(f, a) : B\)}
\end{prooftree}

\item \begin{prooftree}
    \AxiomC{\(\Gamma, x: A \vdash b: B\)}
    \AxiomC{\(\Gamma \vdash a : A\)}
    \BinaryInfC{\(\Gamma \vdash \app^{A, B}((\lambda x: A . b), a) \rightsquigarrow b[a/x] : B\)}
\end{prooftree}
\end{itemize}

\begin{thebibliography}{2}

    \bibitem{Shaph}
    Шафаревич И.Р.
    \newblock {\em Основы алгебраической геометрии.}
    \newblock УМН, 24:6(150) (1969), 3–184; Russian Math. Surveys, 24:6 (1969), 1–178.

    \bibitem{Harper}
    Robert Harper.
    \newblock {\em Type Systems for Programming Languages.}
    \newblock School of Computer Science, Carnegie Mellon University, Spring, 2000,
    \newblock url: \url{https://people.mpi-sws.org/~dreyer/ats/papers/harper-tspl.pdf}

    \bibitem{Lof}
    Per Martin-L\"{o}f.
    \newblock {\em Intuitionistic Type Theory.}
    \newblock Bibliopolis.
    \newblock url: \url{https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}

    \bibitem{Smith}
    Bengt Nordstr\"{o}m, Kent Petersson, Jan M. Smith.
    \newblock {\em Programming in Martin-L\"{o}f's Type Theory.}
    \newblock Department of Computing Sciences, University of G\"{o}teborg, Sweden.

    \bibitem{}
    Аксель П. и др.
    \newblock {\em Гомотопическая теория типов.}
    \newblock Программа Унивалентных Оснований, Иститут Перспективных Исследований, пер.: Геннадий Чернышев,
    \newblock url: \url{https://henrychern.wordpress.com/wp-content/uploads/2022/10/hott2.pdf}

\end{thebibliography}

\end{document}