vclang.tex

\documentclass{amsart}

\usepackage{etex}
\usepackage[english,russian]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage[all]{xy}
\usepackage{verbatim}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{type1ec}
\usepackage{stmaryrd}
\usepackage{tikz}
\usepackage{tikz-qtree}

\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}{определение}{Определение}
\newref{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{Vclang}

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

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

\maketitle

\section{Vccore}

Язык vclang состоит из двух частей: ядра (vccore) и фронтенда (vclang).
Пользователь пишет код на vclang, и он транслируется в vccore.
Как это происходит мы обсудим позже, в этом разделе мы опишем ядро.

Программа на vccore состоит из множества объявлений (то есть \emph{неупорядоченного} списка).
Каждое объявление состоит из уникального имени и \emph{определения}, которые бывают трех видов:
\begin{itemize}
\item \emph{Функция} содержит тело и сигнатуру, состоящую из списка типов аргументов и типа возвращаемого значения.
\item \emph{Алгебраический тип данных} содержит вселенную в которой он лежит, список типов, описывающий параметры типа данных, и множество конструкторов, каждый из которых состоит из уникального имени и списка типов, описывающего параметры конструктора.
\item \emph{Класс} содержит список полей. Каждое поле состоит из уникального имени и типа.
\end{itemize}
Классы в vccore устроенны очень просто, по сути, они являются просто записями.
Классы не могут наследоваться друг от друга, но можно использовать анонимное наследование.
Если $A$ -- некоторый класс с множеством полей $\{ f_1, \ldots f_n \}$, $D_1$, \ldots $D_n$ -- некоторые типы и $d_1, \ldots d_n \in Term \amalg \{ * \}$, то $A\ \{\ f_1 : D_1 \red d_1;\ \ldots\ f_n : D_n \red d_n\ \}$ -- анонимный наследник класса $A$.
Если $D_i$ совпадает с типом $f_i$ в классе $A$ и $d_i = *$, то мы будем опускать член $f_i : D_i \red d_i$ в этой нотации.

Если $A\ \{\ f_1 : D_1 \red d_1;\ \ldots\ f_n : D_n \red d_n\ \}$ -- коректный тип и все $d_i \in Term$, то его элементы создаются при помощи конструкции $\mathbf{new}$:
\[ \mathbf{new}\ A\ \{\ f_1 : D_1 \red d_1,\ \ldots\ f_n : D_n \red d_n\ \} : A\ \{\ f_1 : D_1 \red d_1,\ \ldots\ f_n : D_n \red d_n\ \} \]

\subsection{Формальное определение термов vccore}

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

При определении функции или связывания в $\mathbf{let}$ мы можем использовать один из двух способов их описания: либо $f\,x_1\,\ldots\,x_n \Rightarrow e$, либо $f\,x_1\,\ldots\,x_n \Leftarrow e$.
Множество $\{ \Leftarrow, \Rightarrow \}$ мы будем обозначать $Ar$.
Какой из элементов множества $Ar$ используется при определении функции влияет на то, как будет вычисляться эта функция.
При выборе варианта $\Leftarrow$, мы можем использовать дополнительные конструкции для задания тела функции.
Множество термов $Term$ будет определено ниже.
Используя его, можно определить множество $Term_e$ индуктивным образом:
\begin{itemize}
\item Если $a \in Term$, то $a \in Term_e$.
\item Пусть $k \in \mathbb{N}$, $p_i$ -- шаблоны, $d_i \in Ar$, $b_i \in Term_e$ и $b_i \in Term$, если $d_i = \Rightarrow$.
    Тогда $\mathbf{elim}\,v_k\,\{ p_1\,d_1\,b_1; \ldots p_n\,d_n\,b_n \} \in Term_e$.
\end{itemize}
Шаблон -- это либо имя конструктора, либо символ $var$.

Множество термов определяется следующим образом:
\begin{align*}
Term :=\ & v_i\ |\ D\ |\ f\ |\ g\ |\ D\,a_1\,\ldots\,a_n\,.\,c \\
      |\ & \mathbf{new}\,C\,\{ S \}\ |\ C\,\{ S \} \\
      |\ & \mathbf{let}\,\mathbf{it}\,A_1\,\ldots\,A_n : B \Rightarrow b\,\mathbf{in}\,a \\
      |\ & \mathbf{let}\,\mathbf{it}\,A_1\,\ldots\,A_n : B \Leftarrow e\,\mathbf{in}\,a \\
      |\ & b\,a\ |\ \lambda b\ |\ \Pi A B \\
      |\ & (a,b)_B\ |\ \mathbf{proj}_1\,p\ |\ \mathbf{proj}_2\,p\ |\ \Sigma A B \\
      |\ & \mathbf{Type}_i\ |\ \mathbf{Set}_i\ |\ \mathbf{Prop}
\end{align*}
где $i \in \mathbb{N}$, $a, b, A, B, p, a_1, \ldots a_n, A_1, \ldots A_n \in Term$, $e \in Term_e$, $D$ является именем типа данных, $c$ -- именем конструктора типа данных $D$, $C$ -- именем класса, $f$ -- именем поля некоторого класса, $g$ -- именем функции и $S$ -- последовательностью троек $(f,D,d)$, где $f$ -- имя поля класса $C$, $D$ -- терм и $d \in Term \amalg \{ * \}$.
Такую тройку $(f,D,d)$ мы будем записывать как $f : D \red d$.
Как обычно, мы сокращаем $\Pi A (\uparrow B)$ до $A \to B$.

TODO: Добавить конструкции для вселенных $\mathbf{Prop}$ и $\mathbf{Set}_i$.

Определение редукций: TODO.

На множестве термов существует предпорядок $\leq$, порождаемый следующими соотношениями:
\begin{itemize}
\item $\mathbf{Prop} \leq \mathbf{Set}_i$.
\item $\mathbf{Set}_i \leq \mathbf{Type}_i$.
\item Если $i \leq j$, то $\mathbf{Set}_i \leq \mathbf{Set}_j$.
\item Если $i \leq j$, то $\mathbf{Type}_i \leq \mathbf{Type}_j$.
\item Если $A \deq B$, то $A \leq B$.
\item Если $A \leq A'$ и $B \leq B'$, то $\Sigma A B \leq \Sigma A' B'$.
\item Если $A' \leq A$ и $B \leq B'$, то $\Pi A B \leq \Pi A' B'$.
\item Если для любого $(f,D,d) \in S$ существует некоторая тройка $(f,D',d') \in S'$, такая что $D \leq D'$ и либо $d = *$, либо $d = d'$, то $C\,\{ S' \} \leq C\,\{ S \}$.
\end{itemize}

Правила типизации будут определены относительно фиксированного множества определений $\Sigma$.
Как отмечалось ранее, каждое определение является определением либо функции, либо типа данных, либо класса.

Во-первых, опишем стандартные базовые правила для контекстов, индексов и типов:
\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$\vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A$}
\UnaryInfC{$\Gamma, A \vdash$}
\DisplayProof
\quad
\AxiomC{$A_1, \ldots A_n \vdash$}
\UnaryInfC{$A_1, \ldots A_n \vdash v_i \Uparrow (\uparrow^{i+1}\!\!A_{n-i})$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a \Uparrow A$}
\RightLabel{, $A \leq B$}
\UnaryInfC{$\Gamma \vdash a \Downarrow B$}
\DisplayProof
\end{center}
\medskip

Термы $\mathbf{Type}_i$, $\mathbf{Set}_i$ и $\mathbf{Prop} \}$ мы будем называть \emph{вселенными в нормальной форме}, множество таких термов мы будем обозначать $\mathcal{U}_{nf}$.
Мы будем называть \emph{вселенными} термы $U$, такие что $U \red_h^* U'$ для некоторого $U' \in \mathcal{U}_{nf}$.
Множество вселенных мы будем обозначать $\mathcal{U}$.
Тогда существует функция $nf : \mathcal{U} \to \mathcal{U}_{nf}$ каждой вселенной сопоставляющая ее нормальную форму.

Определим функцию $max : \mathcal{U} \times \mathcal{U} \to \mathcal{U}_{nf}$ следующим образом:
\begin{align*}
max(\mathbf{Type}_i, \mathbf{Type}_j) & = \mathbf{Type}_{max(i,j)} \\
max(\mathbf{Type}_i, \mathbf{Set}_j) & = \mathbf{Type}_{max(i,j)} \\
max(\mathbf{Set}_i, \mathbf{Type}_j) & = \mathbf{Type}_{max(i,j)} \\
max(\mathbf{Set}_i, \mathbf{Set}_j) & = \mathbf{Set}_{max(i,j)} \\
max(\mathbf{Type}_i, \mathbf{Prop}) & = \mathbf{Type}_i \\
max(\mathbf{Prop}, \mathbf{Type}_i) & = \mathbf{Type}_i \\
max(\mathbf{Set}_i, \mathbf{Prop}) & = \mathbf{Set}_i \\
max(\mathbf{Prop}, \mathbf{Set}_i) & = \mathbf{Set}_i
\end{align*}
Для произвольных $U$ и $V$ мы полагаем $max(U,V) = max(nf(U), nf(V))$.
Функция $max_\Pi$ определена так же как и $max$ за исключением того, что $max_\Pi(U, V) = \mathbf{Prop}$ для любого $U$ и $V$, такого что $nf(V) = \mathbf{Prop}$.
Для произвольного конечного множества термов $U_1$, \ldots $U_n$ мы определяем $max(U_1, \ldots U_n)$ как $max(U_1, \ldots max(U_{n-1}, U_n) \ldots)$.
На пустом множестве мы определяем $max$ как $\mathbf{Prop}$.

Теперь опишем правила для $\Pi$ и $\Sigma$ типов.
В правилах ниже термы $U$ и $V$ принадлежат множеству $\{ \mathbf{Type}_i, \mathbf{Set}_i, \mathbf{Prop} \}$.
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A \Uparrow U$}
\AxiomC{$\Gamma, A \vdash B \Uparrow V$}
\BinaryInfC{$\Gamma \vdash \Pi A B \Uparrow max_\Pi(U,V)$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A \Uparrow U$}
\AxiomC{$\Gamma, A \vdash B \Uparrow V$}
\BinaryInfC{$\Gamma \vdash \Sigma A B \Uparrow max(U,V)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, A \vdash b \Uparrow B$}
\UnaryInfC{$\Gamma \vdash \lambda b \Uparrow \Pi A B$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash b \Uparrow C$}
\AxiomC{$\Gamma \vdash a \Downarrow A$}
\RightLabel{, $C \red_h^* \Pi A B$}
\BinaryInfC{$\Gamma \vdash b\,a \Uparrow B[a]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, A \vdash B$}
\AxiomC{$\Gamma \vdash a \Uparrow A$}
\AxiomC{$\Gamma \vdash b \Downarrow B[a]$}
\TrinaryInfC{$\Gamma \vdash (a,b)_B \Uparrow \Sigma A B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p \Uparrow C$}
\RightLabel{, $C \red_h^* \Sigma A B$}
\UnaryInfC{$\Gamma \vdash \mathbf{proj}_1\,p \Uparrow A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p \Uparrow C$}
\RightLabel{, $C \red_h^* \Sigma A B$}
\UnaryInfC{$\Gamma \vdash \mathbf{proj}_2\,p \Uparrow B[\mathbf{proj}_1\,p]$}
\DisplayProof
\end{center}
\medskip

Следующие правила для вселенных:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Type}_i$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Set}_i$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Prop}$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A \Downarrow U$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Prop} \Uparrow \mathbf{Set}_0$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Set}_i \Uparrow \mathbf{Type}_{i+1}$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathbf{Type}_i \Uparrow \mathbf{Type}_{i+1}$}
\DisplayProof
\end{center}
\medskip

Если $D$ является типом данных в сигнатуре $\Sigma$ с параметрами $A_1$, \ldots $A_n$ и вселенной $U$, то у нас есть следующее правило вывода:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash D \Uparrow \Pi A_1 (\ldots \Pi A_n U \ldots)$}
\DisplayProof
\end{center}
\medskip

Если $c$ является конструктором $D$ с типами аргументов $B_1$, \ldots $B_k$, то у нас есть следующее правило вывода:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_i \Downarrow A_i[a_1, \ldots a_{i-1}]$}
\BinaryInfC{$\Gamma \vdash D\,a_1\,\ldots\,a_n\,.\,c \Uparrow \Pi (B_1[a_1, \ldots a_n]) (\ldots \Pi (B_k[a_1, \ldots a_n]) (D\,a_1\,\ldots\,a_n) \ldots)$}
\DisplayProof
\medskip
\end{center}

Если $C$ -- класс в сигнатуре $\Sigma$ и множество полей $C$ состоит из $f_1$, \ldots $f_n$ с типами $B_1$, \ldots $B_n$ соответственно и $B_i \leq B'_i$, то у нас есть следующие правила вывода:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma, C\,\{ f_1 : B'_1 \red b_1; \ldots f_{i-1} : B'_{i-1} \red b_{i-1} \} \vdash b_i \Downarrow B'_i$, $1 \leq i \leq n$}
\BinaryInfC{$\Gamma \vdash C\,\{ f_1 : B'_1 \red b_1; \ldots f_n : B'_n \red b_n \}$}
\DisplayProof
\medskip
\end{center}
Если $b = *$, то $\Gamma \vdash b \Downarrow B$ означает просто $\Gamma \vdash B$.

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\def\extraVskip{0.5pt}
\Axiom$\fCenter \Gamma, C\,\{ f_1 : B'_1 \red b_1; \ldots f_{i-1} : B'_{i-1} \red b_{i-1} \} \vdash b_i \Downarrow B'_i \text{, } b_i \neq * \text{, } 1 \leq i < k$
\noLine
\UnaryInf$\fCenter \Gamma, C\,\{ f_1 : B'_1 \red b_1; \ldots f_{k-1} : B'_{k-1} \red b_{k-1} \} \vdash B'_i \Uparrow U_i \text{, } b_i = * \text{, } k \leq i \leq n$
\def\extraVskip{2pt}
\BinaryInfC{$\Gamma \vdash C\,\{ f_1 : B'_1 \red b_1; \ldots f_n : B'_n \red b_n \} \Uparrow max(U_1, \ldots U_n)$}
\DisplayProof
\medskip
\end{center}
где $U_i = \mathbf{Prop}$, если $b_i \neq *$.

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma, C\,\{ f_1 : B'_1 \red b_1; \ldots f_{i-1} : B'_{i-1} \red b_{i-1} \} \vdash b_i \Downarrow B'_i$, $1 \leq i \leq n$}
\BinaryInfC{$\Gamma \vdash \mathbf{new}\,C\,\{ f_1 : B'_1 \red b_1; \ldots f_n : B'_n \red b_n \} \Uparrow C\,\{ f_1 : B_1 \red b_1; \ldots f_n : B'_n \red b_n \}$}
\DisplayProof
\medskip
\end{center}

Если $f$ является полем класса $C$ типа $B$, то у нас есть следующее правило вывода:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash f \Uparrow \Pi (C\,\{ \}) B$}
\DisplayProof
\medskip
\end{center}

Для конструкции $\mathbf{elim}$ мы вводим отношение $\Gamma \vdash^n a \Downarrow A$, где $\Gamma$ -- последовательность термов из $Term$, $n \in \mathbb{N}$, $a \in Term_e$ и $A \in Term$.
Правило для $\mathbf{elim}$ тогда выглядит следующим образом: TODO.

Правило для $\mathbf{let}$: TODO.

Теперь мы опишем как расширять сигнатуру новыми определениями.
Мы будем писать $- \vdash_\Sigma -$ для обозначения того факта, что это отношение верно в сигнатуре $\Sigma$.
Сначала мы введем вспомогательное понятие абстрактной функции, необходимое для описания рекурсивных функций.
Пусть $\Sigma$ -- корректная сигнатура, $f$ -- имя функции и $B_1, \ldots B_n, A \in Term$.
Тогда $(f, (B_1, \ldots B_n), A)$ является корректным определением абстрактной функции в сигнатуре $\Sigma$, если
\[ B_1, \ldots B_n \vdash^n_\Sigma A. \]

Пусть $\Sigma$ -- корректная сигнатура, $f$ -- имя функции, $d \in Ar$, $B_1, \ldots B_n, A \in Term$, $a \in Term_e$ и если $d = \Rightarrow$, то $a \in Term$.
Тогда $(f, (B_1, \ldots B_n), A, d, a)$ является корректным определением функции в сигнатуре $\Sigma$, если $(f, (B_1, \ldots B_n), A)$ является корректной абстрактной функцией в $\Sigma$ и
\[ B_1, \ldots B_n \vdash^n_{\Sigma, (f, (B_1, \ldots B_n), A)} a \Downarrow A. \]
Кроме того, мы требуем, чтобы определение было завершающимся, что проверяется отдельно.

Пусть $\Sigma$ -- корректная сигнатура, $D$ -- имя типа данных, $A_1, \ldots A_n \in Term$ и $C$ -- множество пар $(c,B)$, где $c$ -- имя конструктора и $B = B_1, \ldots B_k$ -- список типов.
Тогда $(D, (A_1, \ldots A_n), C)$ является корректным определением типа данных в сигнатуре $\Sigma$, если
\[ A_1, \ldots A_n \vdash_\Sigma \]
и для любой пары $(c, (B_1, \ldots B_k)) \in C$ верно, что
\[ A_1, \ldots A_n, B_1, \ldots B_k \vdash_{\Sigma, (D, (A_1, \ldots A_n), \varnothing)}. \]

Пусть $\Sigma$ -- корректная сигнатура, $C$ -- имя класса и $F$ -- конечное множество пар $(f,B)$, где $f$ -- имя поля и $B \in Term$.
Тогда $(C, F)$ является корректным определением класса, если элементы $F$ можно упорядочить $(f_1, B_1)$, \ldots $(f_n, B_n)$ таким образом, что для любого $1 \leq i \leq n$ выполняется следующее свойство:
\[ C\,\{ \} \vdash_{\Sigma, (C, \{ (f_1, B_1), \ldots (f_{i-1}, B_{i-1}) \})} B_i. \]

\section{Vclang}

Язык vclang имеет ряд отличий от vccore:
\begin{itemize}
\item В vclang есть полноценные классы.
Они могут быть вложенными, а также могут наследоваться.
В vclang, так же как и в vccore, есть анонимное наследование.
\item В vclang есть неявные аргументы.
\item В vclang будет реализован механизм, аналогичный классам типов.
\end{itemize}

Множество термов $Term^{vc}$ языка vclang определяется следующим образом:
\begin{align*}
Term^{vc} :=\ & \_\ |\ x\ |\ D\ |\ c\ |\ D\,a_1\,\ldots\,a_n\,.\,c \\
      |\ & \mathbf{new}\,C\,\{ S \}\ |\ C\,\{ S \}\ |\ \mathbf{new}\,C\ |\ C \\
      |\ & b\,.\,D\ |\ b\,.\,f\ |\ b\,.\,c\ |\ b\,.\,D\,a_1\,\ldots\,a_n\,.\,c \\
      |\ & \mathbf{new}\,b\,.\,C\,\{ S \}\ |\ b\,.\,C\,\{ S \}\ |\ \mathbf{new}\,b\,.\,C\ |\ b\,.\,C \\
      |\ & \mathbf{let}\,x\,[x_1 : A_1]\,\ldots\,[x_n : A_n] : B \Rightarrow b\,\mathbf{in}\,a \\
      |\ & \mathbf{let}\,x\,[x_1 : A_1]\,\ldots\,[x_n : A_n] : B \Leftarrow e\,\mathbf{in}\,a \\
      |\ & b\,a\ |\ \lambda x. b\ |\ \lambda x : A. b\ |\ \Pi (x : A) B \\
      |\ & b\,\{a\}\ |\ \lambda \{x\}. b\ |\ \lambda \{x : A\}. b\ |\ \Pi \{x : A\} B \\
      |\ & (a,b)\ |\ \Sigma (x : A) B\,.\,(a,b)\ |\ p\,.\,1\ |\ p\,.\,2\ |\ \Sigma (x : A) B \\
      |\ & \mathbf{Type}_i\ |\ \mathbf{Set}_i\ |\ \mathbf{Prop}
\end{align*}
где $x$, $x_1$, \ldots $x_n$ -- имена переменных, $a, b, A, B, p, a_1, \ldots a_n, A_1, \ldots A_n \in Term^{vc}$, $e \in Term^{vc}_e$, $D$ является именем типа данных, $c$ -- именем конструктора типа данных $D$, $C$ -- именем класса, $f$ -- именем поля некоторого класса и $S$ -- последовательностью троек $(f,D,d)$, где $f$ -- имя поля класса $C$ и $d,D \in Term \amalg \{ * \}$ -- терм.
Такую тройку $(f,D,d)$ мы будем записывать как $f : D \red d$.
Запись $[x_i : A_i]$ означает либо $(x_i : A_i)$, либо $\{x_i : A_i\}$.
Фигурные скобки используются для обозначения неявных аргументов.
Как обычно, мы сокращаем $\Pi (x : A) B$ до $A \to B$, если $x \notin FV(B)$.

Множество определений $Def^{vc}$ определяется следующим образом:
\begin{align*}
Def^{vc} :=\ & \mathbf{function}\,f\,[x_1 : A_1]\,\ldots\,[x_n : A_n] : B \Leftarrow e \\
    |\ & \mathbf{function}\,f\,[x_1 : A_1]\,\ldots\,[x_n : A_n] : B \Rightarrow b \\
    |\ & \mathbf{function}\,f\,[x_1 : A_1]\,\ldots\,[x_n : A_n] \Rightarrow b \\
\end{align*}

Сейчас мы опишем функцию $int$, интерпретирующую vclang в vccore.
Для этого нам понадобится понятие окружения.
Окружение -- это послеовательность элементов вида либо $(x,A)$, либо $(?x,A)$, где $x$ -- имя переменной и $A \in Term$.
Множество окружений мы будем обозначать $Env$.
Функция $ctx : Env \to Ctx$ сопоставляет каждому окружению контекст (то есть последовательность термов из $Term$), отбрасывая первый элемент каждой пары.

Кроме того, нам понадобится понятие уравнения.
Уравнение в окружении $\rho$ -- это просто пара термов $e_1$, $e_2$.
Уравнения мы будем записывать как $\rho \vdash e_1 \equiv e_2$ или просто как $e_1 \equiv e_2$, если $\rho$ подразумевается.
Множество уравнений в окружении $\rho$ мы будем обозначать как $Eq(\rho)$ и множество всех уравнений как $Eq$.
Система уравнений в окружении $\rho$ -- это конечное множество уравнений в окружении $\rho$.
Множество систем уравнений в $\rho$ мы будем обозначать как $SEq(\rho)$ и множество всех систем уравнений как $SEq$.

Пусть $S \in PEq(\rho)$.
Пусть $\sigma$ -- функция, которая каждому элементу $\rho$ вида $(?x,A)$ присваивает некоторый терм.
Тогда для любого $(\rho \vdash e_1 \equiv e_2) \in S$ мы можем определить суждение $\sigma(e_1,e_2)$ как $\Gamma \vdash e_1' \deq e_2'$, где
$\Gamma$, $e_1'$ и $e_2'$ получаются подстановки $\sigma$ из $\rho$, $e_1$ и $e_2$ соответственно.
Мы будем говорить, что $\sigma$ является \emph{решением} системы $S$, если все термы $\sigma(x)$ имеют корректные типы,
чтобы подстановка, заданная выше, была определена, и все суждения $\sigma(e_1,e_2)$ выводимы.

Мы определим функцию $int : Env \times Term^{vc} \times (Term \cup \{ * \}) \to Env \times Term \times Term \times SEq \cup \{ * \}$, удовлетворяющую следующим свойствам:
\begin{itemize}
\item Если $int(\rho, t, A') = (\rho', a, A, S)$, то $\rho$ -- префикс $\rho'$, $S \in SEq(\rho)$, для любого $(e_1,e_2) \in S$ верно,
    что $ctx(\rho') \vdash e_1 \equiv e_2$, и для любого решения $\sigma$ системы $S$ выводимо $\sigma(\rho') \vdash \sigma(a) \Uparrow \sigma(A)$.
\item Если $int(\rho, t, A') = (\rho', a, A, S)$ и $A' \in Term$, то $A \leq A'$.
\end{itemize}

Функция $int(\rho,t,T)$ определяется следующим образом:
\begin{itemize}
\item Пусть $t = f\,a$.
    Если $int(\rho,f,*) = (\rho',f',T',S)$, $T' \red_{whnf} \Pi A B$, $int(\rho',a,A) = (\rho'',a',\_,S')$ и либо $T = *$, либо $T \deq \Pi A B$, то
    \[ int(\rho,t,T) = (\rho'', f'\!\uparrow^{|\rho''|-|\rho'|}\,a', B[a'], S\!\uparrow^{|\rho''|-|\rho'|} \cup S'), \]
    иначе $int(\rho,t,T) = *$.
\item Пусть $t = \lambda x : A.\ b$.
    Если $int(\rho,A,Type) = (\rho',A',\_,S)$ и $int((\rho',x:A'), b, B') = (\rho'',b',B'',S')$,
    то $int(\rho,t,T) = (\rho'' \setminus x, \lambda A'.\ b', \Pi A' B'', S\!\uparrow^{|\rho''|-|\rho'|-1} \cup abs(x,S'))$,
    где $B' = B\!\uparrow^{|\rho'|-|\rho|}_1$ если $T \red_{whnf} \Pi \_ B$, иначе $B' = *$.
\item Пусть $t = \lambda x.\ b$. Тогда $int(\rho,t,T) = int(\rho, \lambda x : \_.\ b, T)$.
\item Пусть $t = \_$. Тогда
    $int(\rho,t,T) = ((\rho,(?a:T)), v_0, T\!\uparrow, \varnothing)$ если $T \in Term$, и
    $int(\rho,t,T) = ((\rho,(?A:Type),(?a:?A)), v_0, v_1, \varnothing)$ иначе, где $A$ и $a$ -- свежие переменные.
\end{itemize}

\begin{comment}
Мы определяем функцию $int$ через вспомогательную функцию $apps : Env \times Term^{vc} \times (\{ I, E \} \times Term^{vc})^* \times (Term + 1) \to Term \times Term + 1$ как
\[ int(\rho, t, s) = apps(\rho, t, [], s). \]
Функция $apps$ определяется через функцию $int' : Env \times Term^{vc} \times (Term + 1) \to Term \times Term + 1$:
\begin{itemize}
\item $apps(\rho, t_1\,t_2, a, s) = apps(\rho, t_1, ((E, t_2), a), s)$.
\item $apps(\rho, t_1\,\{t_2\}, a, s) = apps(\rho, t_1, ((I, t_2), a), s)$.
\item $apps(\rho, t, a, s) = $ (TODO: закончить определение $apps$)
\end{itemize}
Функция $int'$ определяется индукцией по размеру второго аргумента (TODO: закончить определение $int'$):
\begin{itemize}
\item $int'(\rho, C\,\{ f_1 : D_1 \red d_1; \ldots f_n : D_n \red d_n \}, inr(*)) = inl(C\,\{ f'_1 : D'_1 \red d'_1; \ldots f'_k : D'_k \red d'_k \}, T)$, если
    $int'((\rho, (\mathbf{this}, C\,\{ f'_1 : D'_1 \red d'_1; \ldots f_{i-1} : D'_{i-1} \red d'_{i-1} \})), d_i, [], T_i) = inl(d'_i, T'_i)$
    для всех $1 \leq i \leq n$, где $T_i$ -- это тип поля $f_i$, а $T$ -- это максимум по типам всех полей, которых нет в списке $f_1$, \ldots $f_n$.
\item $int'(\rho, C\,\{ S \}, inl(A)) = inl(C', A')$, если $int'(\rho, C\,\{ S \}, inr(*)) = inl(C', A')$ и $A' \leq A$, иначе $int'(\rho, C\,\{ S \}, inl(A)) = inr(*)$.
\end{itemize}
\end{comment}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}