colloq.tex

\documentclass[11pt,a4paper,oneside]{article}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amssymb}
%\usepackage{amsmath}
%\usepackage{mathabx}
\usepackage{stmaryrd}
\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm,bindingoffset=0cm]{geometry}
%\usepackage{bnf}
\newcommand{\lit}[1]{\mbox{`\texttt{#1}'}}
\newcommand{\ntm}[1]{<\mbox{#1}>}
\begin{document}


\begin{center}
\begin{Large}{\bfseries Вопросы к коллоквиуму по курсу <<Теория типов>>}\end{Large}\\
\vspace{1mm}
\begin{small} \itshape ИТМО, группы M3334..M3339\end{small}\\
\small 13 ноября 2018 г.
\end{center}

\begin{enumerate}
\item Бестиповое лямбда-исчисление. Общие определения (альфа-эквивалентность, бета-редукция, бета-эквивалентность).
Параллельная бета-редукция. Теорема Чёрча-Россера.
\item Булевские значения, чёрчевские нумералы, упорядоченные пары.
\item Алгебраические типы: аналог в теории множеств, реализация в лямбда-исчислении. 
Нормальный и аппликативный порядок редукций, мемоизация.
\item \textbf{Y}-комбинатор. Парадокс Карри.
\item Просто типизированное лямбда-исчисление. Исчисление по Чёрчу и по Карри. Изоморфизм Карри-Ховарда.
\item Конъюнкция, дизъюнкция, ложь и соответствующие им конструкции в лямбда-исчислении.
\item Нетипизируемость \textbf{Y}-комбинатора. Слабая и сильная нормализация.
\item Задачи проверки типа, реконструкции (вывода) типа, обитаемости типа в просто типизированном лямбда-исчислении.
Их аналоги в интуиционистском исчислении высказываний.
\item Алгебраические термы. Задача унификации в алгебраических термах. Алгоритм унификации. Доказательство 
корректности алгоритма унификации. Наиболее общее решение задачи унификации.
\item Алгоритм нахождения типа в просто типизированном лямбда-исчислении. Наиболее общий тип, наиболее общая пара.
\item Комбинаторы. Базисы $SK$ и $BCKW$, выразимость в них любого замкнутого лямбда-терма.
Аналоги для комбинаторных исчислений в исчислении высказываний.
\item Логика второго порядка. Выразимость связок через импликацию и квантор всеобщности в интуиционистской логике 
2-го порядка (конъюнкция, дизъюнкция, ложь, отрицание, квантор существования).
\item Система F. Изоморфизм Карри-Ховарда для системы F. Упорядоченные пары и алгебраические типы.
\item Экзистенциальные типы. Конструкции \texttt{unpack} и \texttt{pack}.
\item Ранг типа. Частный случай типа. Типы и типовые схемы. \texttt{let}-полиморфизм.
\item Типовая система Хиндли-Милнера. Алгоритм W.
\item Типизация \textbf{Y}-комбинатора. Экви- и изорекурсивные типы, $\mu$-оператор, \texttt{roll} и \texttt{unroll}.
\item Зависимые типы: примеры в языках программирования, теоретико-множественный смысл, исчисление предикатов
и зависимые типы.
\item Обобщённые типовые системы. Типы, рода, сорта. Лямбда-куб.
\end{enumerate}

\end{document}