holib

holib/holib.tex

@@ -0,0 +1,226 @@
+% copyright (c) 2018 Groupoid Infinity
+
+\documentclass{article}
+\usepackage[english,russian]{babel}
+\usepackage{hyphenat}
+\usepackage{listings}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{mathtools}
+\usepackage{url}
+\usepackage{tikz-cd}
+\usepackage[utf8]{inputenc}
+\theoremstyle{definition}
+\newtheorem{theorem}{Теорема}
+\newtheorem{definition}{Визначення}
+\newtheorem{exercise}{Вправа}
+\newtheorem{example}{Приклад}
+\newcommand*{\incmap}{\hookrightarrow}
+\newcommand*{\thead}[1]{\multicolumn{1}{c}{\bfseries #1}}
+\lstset{basicstyle=\small,inputencoding=utf8}
+
+\addto\captionsrussian{\renewcommand{\contentsname}{Зміст}}
+\addto\captionsrussian{\def\refname{Список використаних джерел}}
+\addto\captionsrussian{\renewcommand{\abstractname}{Анотація}}
+
+
+\begin{document}
+
+\title{Anders: гомотопічна базова бібліотека}
+\author{Максим Сохацький $^1$}
+\date{ \small $^1$ Національний технічний університет України \\
+       «Київський Політехнічний Інститут» ім. Ігора Сікорського \\
+       29 жовтня 2018 }
+\maketitle
+
+\begin{abstract}
+Тут представлена базова бібліотека мови Anders для курсу «Теорія типів»,
+яка сумісна з позначеннями, що використовуються в підручнику HoTT.
+Серед принципів, які покладені в основу бібліотеки, головними є:
+лаконічность, академічність, педагогічність. Кожна сторінка має
+на меті повністю висвітлити компоненти типу, використовуючи тільки
+ті типи, що були викладені попередньо, кожне визначення повинно
+містити як математичну нотацію так і код верифікатора та бути
+вичерпним посібником користувача мови програмування Anders та
+її базової бібліотеки. Загалом передбачається, що бібліотека
+повинна відповідати підручнику HoTT, та бути його практичним
+досліднидницьким артефактом.
+\end{abstract}
+
+\section*{Теорія типів}
+Теорія типів --- це універсальна мова програмування чистої
+математики (для доведення теорем), яка може містити довільну
+кількість консистентних аксіом, впорядкованих у вигляді псевдо-ізоморфізмів:
+функцій encode (способи конструювання елементів типу) і decode (залежні
+елімінатори принципу індукції типу) та їх рівнянь --- бета
+і ета правил обчислювальності та унікальності. Зазвичай теорія типів,
+як мова програмування, вже постачається з наступними
+типами (примітивами-аксіомами) та коментарями у вигляді
+окремих лекцій (конспекти, документація).
+
+Головна мотивація гомотопічної теорії — надати обчислювальну
+семантику гомотопічним типам та CW-комплексам. Головна ідея
+гомотопічної теорії [1] полягає в поєднанні просторів функцій,
+просторів контекстів  і просторів шляхів  таким чином, що вони
+утворюють фібраційну рівність яка збігається (доводиться в самій
+теорії) з простором шляхів.
+
+Завдяки відсутності ета-правила у рівності, не кожні два
+доведення одного простору шляхів дорівнюють між собою, отже
+простір шляхів утворює багатовимірну структуру інфініті-групоїда.
+
+Групоїдна інтерпретація теорії типів ставить питання про
+існування мови, в якій можна довести механічно всі всластивості
+категорного визначення групоїда.
+
+\newpage
+\section*{Основи}
+
+Модальні унівалентні MLTT основи розділені на три частини.
+Перша частина містить класичні типи MLTT системи описані
+Мартіном-Льофом. Друга частина містить унівалентні ідентифікаційні
+системи. Третя частина містить модальності, які використовуються
+в диференціальній геометріїї та в теорії гомотопій. Основи
+пропонують фундаментальний базис який використовується для
+формалізації сучасної математики в таких системах доведення
+теорем як: Coq, Agda, Lean.\\
+\\
+\noindent
+$\bullet$ Фібраційні \\
+$\bullet$ Унівалентні \\
+$\bullet$ Модальні
+
+\section*{Математики}
+
+Друга частина базової бібліотеки містить формалізації математичних
+теорій з різних галузей математики: аналіз, алгебра, геометрія,
+теорія гомотопій, теорія категорій.
+
+Слухачам курсу (10) пропонується застосувати теорію типів для
+доведення початкового але нетривіального результу, який є
+відкритою проблемою в теорії типів для однєї із математик,
+що є курсами на кафедрі чистої математики (КМ-111):\\
+\\
+\noindent
+$\bullet$ Функціональний аналіз \\
+$\bullet$ Гомологічна алгебра \\
+$\bullet$ Диференціальна геометрія \\
+$\bullet$ Теорія гомотопій \\
+$\bullet$ Теорія категорій \\
+
+\newpage
+\section{Простори функцій}
+$\Pi$-тип — це простір, що містить залежні функції, кодомен яких залежить від значення
+з домену. Так як всі розшарування домену присутні повністю в кожній функції з простору,
+$\Pi$-тип також називається залежним добутком, так як фунція визначена на всьому просторі домена.
+
+Простори залежних функції використовуються в теорії типів для моделювання різних
+математичних конструкцій, об'єктів, типів, просторів, а також їхніх відображень:
+залежних функцій, неперервниї відображень, етальних відображень, розшарувань, квантора
+узанальнення $\forall$, імплікації, тощо.
+
+\subsection{Формація}
+
+$\textbf{Визначення\ 1.1}$ ($\Pi$-формація, залежний добуток).
+$\Pi$-типи репрезентують спосіб створення просторів залежних функцій  $f: \Pi(x:A), B(x)$ в певному всесвіті $U_i$,
+з доменом в $A$ і кодоменом в сім'ї функцій $B : A \rightarrow U_i$ над $A$.
+$$
+   \Pi : U =_{def} \prod_{x:A}B(x).
+$$
+\begin{lstlisting}[mathescape=true]
+def Pi (A : U) (B : A $\rightarrow$ U) : U
+ := $\Pi$ (x : A), B x
+\end{lstlisting}
+
+\subsection{Конструкція}
+
+$\textbf{Визначення\ 1.2}$ ($\lambda$-функція).
+Лямбда конструктор визначає нову лямбда функцію в просторі залежних функцій,
+вона ще називається лямбда абстракцією і позначається як $\lambda x. b(x)$ або $x \mapsto b(x)$.
+$$
+    \backslash (x: A) \rightarrow b : \Pi(A,B) =_{def}
+$$
+$$
+    \prod_{A:U}\prod_{B:A \rightarrow U}\prod_{a: A}\prod_{b:B(a)}\lambda x.b.
+$$
+\begin{lstlisting}[mathescape=true]
+def lambda (A: U) (B: A $\rightarrow$ U) (b: Pi A B)
+  : Pi A B := $\lambda$ (x : A), b x
+
+def lam (A B: U) (f: A $\rightarrow$ B)
+  : A $\rightarrow$ B := $\lambda$ (x : A), f x
+\end{lstlisting}
+
+Коли кодомен не залежить від значеення з домену функції $f: A \rightarrow B$
+розглядаються в контексті System F$_\omega$, залежний випадок розглядається
+в  Systen P$_\omega$ або Calculus of Construction (CoC).
+
+\newpage
+\subsection{Елімінація}
+
+$\textbf{Визначення\ 1.3}$ (Принцип індукції). Якшо предикат виконується для
+лямбда функції тоді існує функція з простору функцій в простіп предикатів.
+
+\begin{lstlisting}[mathescape=true]
+def $\Pi$-ind (A : U) (B : A $\rightarrow$ U) (C : Pi A B $\rightarrow$ U)
+    (g: $\Pi$ (x: Pi A B), C x)
+  : $\Pi$ (p: Pi A B), C p := $\lambda$ (p: Pi A B), g p
+\end{lstlisting}
+
+\noindent $\textbf{Визначення\ 1.3.1}$ ($\lambda$-аплікація).
+Застосування функції до аргументів редукує терм
+використовуючи рекурсивну підстановку аргументів в тіло функції.
+
+$$
+    f\ a : B(a) =_{def} \prod_{A:U}\prod_{B: A \rightarrow U}\prod_{a:A}\prod_{f: \prod_{x:A}B(a)}f(a).
+$$
+
+\begin{lstlisting}[mathescape=true]
+def apply (A: U) (B: A $\rightarrow$ U)
+    (f: Pi A B) (a: A) : B a := f a
+
+def app (A B: U) (f: A $\rightarrow$ B)
+    (x: A): B := f x
+\end{lstlisting}
+
+\noindent $\textbf{Визначення\ 1.3.2}$ (Композиція функцій).
+\begin{lstlisting}[mathescape=true]
+def $\circ^T$ (x y z: U) : U
+ := (y $\rightarrow$ z) $\rightarrow$ (x $\rightarrow$ y) $\rightarrow$ (x $\rightarrow$ z)
+
+def $\circ$ (x y z : U) : $\circ^T$ x y z
+ := $\lambda$ (g: x $\rightarrow$ z) (f: x $\rightarrow$ y) (a: x), g (f a)
+\end{lstlisting}
+
+\subsection{Обчислювальність}
+
+$\textbf{Теорема\ 1.4}$ (Обчислювальність $\Pi_\beta$).
+$\beta$-правило показує, що композиція $\mathrm{lam} \circ \mathrm{app}$ може бути скорочена (fused).
+$$
+    f(a) =_{B(a)} (\lambda (x:A) \rightarrow f(a))(a).
+$$
+\begin{lstlisting}[mathescape=true]
+def $\Pi$-$\beta$ (A : U) (B : A $\rightarrow$ U) (a : A) (f : Pi A B)
+  : Path (B a) (apply A B (lambda A B f) a) (f a)
+  := idp (B a) (f a)
+\end{lstlisting}
+
+\subsection{Унікальність}
+
+$\textbf{Теорема\ 1.5}$ (Унікальність $\Pi_\eta$).
+$\eta$-правило показує, що композиація $\mathrm{app} \circ \mathrm{lam}$ можу бути скоронеча (fused).
+$$
+    f =_{(x:A)\rightarrow B(a)} (\lambda (y:A) \rightarrow f(y)).
+$$
+\begin{lstlisting}[mathescape=true]
+def $\Pi$-$\eta$ (A : U) (B : A $\rightarrow$ U) (a : A) (f : Pi A B)
+  : Path (Pi A B) f ($\lambda$ (x : A), f x)
+:= idp (Pi A B) f
+\end{lstlisting}
+
+\newpage
+\section{Простори контекстів}
+
+\end{document}
+