Гомотопическая теория типов

Идея использования интуиционистской теории типов Пера Мартин-Лёфа для формализации высших категорий восходит к работе Михая Маккаи (венг. Makkai Mihály), в которой была построена система FOLDS (англ. first-order logic with dependent sorts)[1]. Ключевым отличием унивалентных оснований от идей Маккаи является принцип, согласно которому фундаментальными объектами математики являются не высшие категории, а высшие группоиды. Поскольку высшие группоиды отвечают по соответствию Гротендика гомотопическим типам, можно сказать что математика, с точки зрения унивалентных оснований, изучает структуры на гомотопических типах. Возможность прямого использования теории типов Мартин-Лёфа для описания структур на гомотопических типах является следствием построения Воеводским унивалентной модели теории типов. Построение этой модели требовало решения многочисленных технических проблем связанных с так называемыми свойствами когерентности и хотя основные идеи унивалентных оснований были сформулированны им в 2005—2006 годы, полная унивалентная модель в категории симплициальных множеств появилась только в 2009 году. В те же годы, что и эти исследования Воеводского, велись и другие работы по изучению различных связей между теорией типов и теорией гомотопий, в частности, одним из исторически важных событий, собравшим учёных, работавших в этом направлении, стал семинар в Уппсале в ноябре 2006 года[2].

В феврале 2010 года Воеводский начал создавать библиотеку на Coq, выросшую впоследствии в совместно разрабатываемую широким кругом учёных «библиотеку унивалентных оснований».

По инициативе Воеводского, 2012—2013 академический год в Институте перспективных исследований был объявлен «годом унивалентных оснований», в сотрудничестве с Ауди и Коканом была открыта специальная исследовательская программа и в её рамках группа из математиков и специалистов по информатике работали над развитием теории. Одним из результатов года стало совместное создание участниками шестисотстраничной книги «Гомотопическая теория типов: унивалентные основания математики», выложенной на сайте программы в свободный доступ под лицензией CC-SA; для совместной работы над книгой был создан проект на GitHub[3].

Участники программы, представленные во введении к книге[4]:

Обложка книги

Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 20-ти учёных и практиков, посетивших в течение «года унивалентых оснований» Институт высших исследований (среди которых создатель семантики λ-исчисления Дана Скотт и разработчик формализаций на Coq доказательств задачи о четырёх красках и теоремы Фейта — Томпсона Жорж Гонтье). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.

Теория основывается на интенсиональном варианте интуиционистской теории типов Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству ${\displaystyle a\in A}$ рассматривается как терм соответствующего типа: ${\displaystyle a:A}$, расслоение с базой ${\displaystyle X}$ — как зависимый тип ${\displaystyle A(x)}$. При этом отпадает необходимость представлять пространства в виде множеств точек, снабжённых топологией, и представлять непрерывные отображения между пространствами — как функции сохраняющие или отражающие соответствующие поточечные свойства пространств. Гомотопическая теория типов рассматривает пространства-типы и термы этих типов (точки) как элементарные понятия, а конструкции над пространствами, такие как гомотопии и расслоения, — как зависимые типы.

В формальном построении теории типов используется тип-универсум ${\displaystyle {\mathcal {U}}_{0}}$, термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы ${\displaystyle {\mathcal {U}}_{1},{\mathcal {U}}_{2},\dots }$ такие, что ${\displaystyle U_{i}:U_{i+1}}$, притом все термы типа ${\displaystyle {\mathcal {U}}_{i}}$ также являются термами типа ${\displaystyle {\mathcal {U}}_{i+1}}$. Зависимые типы (семейства типов) определяются как функции ${\displaystyle B:A\to {\mathcal {U}}}$, кообласть которых — некоторый тип-универсум.

В гомотопической теории типов существует несколько способов конструирования новых типов из уже имеющихся. Базовые примеры такого рода — ${\displaystyle {\boldsymbol {\Pi }}}$-типы (зависимые функциональные типы, типы-произведения) и ${\displaystyle {\boldsymbol {\Sigma }}}$-типы (зависимые типы-суммы). Для данного типа ${\displaystyle A:{\mathcal {U}}}$ и семейства ${\displaystyle B:A\to {\mathcal {U}}}$ можно построить тип ${\displaystyle {\boldsymbol {\Pi }}_{x:A}B(x)}$, термы которого — функции, кообласть которых зависит от элемента области определения (геометрически такие функции можно представлять как сечения некоторого расслоения), а также тип ${\displaystyle {\boldsymbol {\Sigma }}_{x:A}B(x)}$, термы которого геометрически соответствуют элементам тотального пространства расслоения.

Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» (${\displaystyle a_{1}:=a_{2}}$), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ типа ${\displaystyle A}$ представляется в виде непустого типа ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$, который называют типом тождества; термы этого последнего типа — это пути вида ${\displaystyle p:a_{1}\rightsquigarrow a_{2}}$ в пространстве ${\displaystyle A}$; тип тождества ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$, таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка ${\displaystyle \mathbb {I} }$ в ${\displaystyle A}$) из точки ${\displaystyle a_{1}}$ в точку ${\displaystyle a_{2}}$.

Высказывание (mere proposition, «голое высказывание») в гомотопической теории типов определяется как тип ${\displaystyle P}$, который либо пуст, либо содержит единственный терм ${\displaystyle p}$; такие типы называются пропозициональными. Если тип ${\displaystyle P}$ пуст, то соответствующее высказывание ложно, если ${\displaystyle P}$ содержит терм ${\displaystyle p}$ (символически — ${\displaystyle p:P}$), то соответствующее высказывание ${\displaystyle P}$ истинно, а терм ${\displaystyle p}$ рассматривается как его доказательство. Таким образом, в теории используется интуиционистская концепция истины, согласно которой истинность высказывания понимается как возможность предъявить доказательство этого высказывания.

Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция ${\displaystyle A\vee B}$ соответствует в пропозициональном фрагменте типу-сумме ${\displaystyle A+B}$, конъюнкция ${\displaystyle A\wedge B}$ — типу-произведению ${\displaystyle A\times B}$, импликация ${\displaystyle A\Rightarrow B}$ — функциональному типу ${\displaystyle A\to B}$, отрицание ${\displaystyle \lnot A}$ — типу ${\displaystyle A\to \mathbf {0} }$, где ${\displaystyle \mathbf {0} }$ — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.

Всякий тип ${\displaystyle X}$, который содержит два или больше различных термов ${\displaystyle x,y,\dots }$ может быть поставлен в однозначное соответствие с пропозициональным типом, который получается в результате отождествления всех термов типа ${\displaystyle X}$, такая операция называется пропозициональным обрезанием (propositional truncation). Это позволяет провести различие между «пропозициональным уровнем» (уровнем высказываний) теории и гомотопической иерархии «высших» непропозициональных её уровней.

За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество ${\displaystyle A}$ можно описать в теории как тип, такой что для любых его термов ${\displaystyle a_{1},a_{2}:A}$ тип ${\displaystyle {\mathsf {Id}}_{A}(a_{1},a_{2})}$ является высказыванием, то есть либо пуст (случай когда ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ — это различные элементы множества ${\displaystyle A}$), либо содержит единственный элемент (случай, когда ${\displaystyle a_{1}}$ и ${\displaystyle a_{2}}$ — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни ${\displaystyle n}$-группоидов всех порядков.

Библиотеки HoTT — несколько проектов, ведущихся на GitHub (в том же репозитории, где и размещены исходные коды книги), в которых создаются формальные описания различных разделов математики средствами систем автоматического доказательства с использованием построений гомотопической теории типов.

В проекте Владимира Воеводского, названном «Библиотека унивалентных оснований»[6], использовано специально разработанное минимальное безопасное подмножество Coq, обеспечивающее идеологическую чистоту и надёжность построений в согласовании с теорией. Проект HoTT[7] ведётся стандартными средствами Coq, реализуется в рамках исследовательской программы Института перспективных исследований, и в целом следует книге, по состоянию на 2020 год в проекте участвуют 48 разработчиков, наиболее активные — Джейсон Гросс, Майкл Шульман, Али Каглаян и Андрей Бауэр[8]. Также ведётся параллельный проект на языке Agda[9].

Существует несколько экспериментальных систем интерактивного доказательства, целиком основанных на HoTT: Arend, RedPRL, redtt, cooltt, а в Agda версии 2.6.0 добавлен так называемый «кубический режим», позволяющий полноценно использовать гомотопические типы.

• Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p.
• Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodsky’s Univalence Axiom in Homotopy Type Theory (англ.) // Notices of the AMS. — 2013. — Vol. 60, no. 9. — P. 1164—1167.
• Hannes Hummel. Will Computers Redefine the Roots of Math?. When a legendary mathematician found a mistake in his own work, he embarked on a computer-aided quest to eliminate human error. To succeed, he has to rewrite the century-old rules underlying all of mathematics (англ.). Quanta Magazine (19 мая 2015). Дата обращения: 31 декабря 2017.
• Don Monroe. A new type of mathematics? (англ.) // Communications of the ACM. — 2014. — Vol. 57, no. 2. — P. 13—15. — doi:10.1145/2557446.
• Андрей Родин. Логический и геометрический атомизм от Лейбница до Воеводского // Вопросы философии. — 2016. — № 6. — С. 134—142.

• cs.cmu.edu/~rwh/courses/hott/ — материалы курса по гомотопической теории типов, читаемого Робертом Харпером в Университете Карнеги — Меллон