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

Гомотопическая теория типов (HoTT, от англ. homotopy type theory) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, высших категориях и типах в логике и языках программирования.

Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки UniMath и послужившая основой для многих других библиотек; в рамках программы большим коллективом математиков была написана книга.

Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.

Ключевая идея теории — аксиома унивалентности, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.

История

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

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

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

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

• Торстен Альтенкирх (англ. Thorsten Altenkirch)
• Бенедикт Аренс (Benedikt Ahrens)
• Стив Ауди (англ. Steve Awodey)
• Брюно Баррас (Bruno Barras)
• Андрей Бауер (словен. Andrej Bauer)
• Марк Безем (Marc Bezem)
• Ив Берто (Yves Bertot)
• Бенно ван ден Берг (Benno van den Berg)
• Владимир Воеводский
• Дэниэл Грейсон (Daniel Grayson, создатель системы компьютерной алгебры Macaulay2)
• Андре Жуайяль (фр. André Joyal)
• Тьерри Кокан
• Дэн Ликата (Dan Licata)
• Питер Лумсдейн (Peter Lumsdaine)
• Пер Мартин-Лёф
• Ассайя Махбуби (Assia Mahboubi)
• Сергей Мелихов
• Альваро Пелайо (Alvaro Pelayo)
• Эндрю Полонский (Andrew Polonsky)
• Матье Созо (Matthieu Sozeau)
• Бас Спиттерс (Bas Spitters)
• Майкл Уоррен (Michael Warren)
• Эрик Финстер (Eric Finster)
• Ноам Цейльбергер (Noam Zeilberger)
• Майкл Шульман (англ. Michael Shulman)
• Питер Эксел (англ. Peter Aczel)
• Юго Эрбелен (Hugo Herbelin, менеджер проекта разработки Coq)

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

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

Основные положения

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

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

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

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

Аксиома унивалентности

Интуиционистская теория типов позволяет определить понятие эквивалентности типов (для типов принадлежащих одному универсуму) и построить каноническим образом функцию из типа тождества $A=B$ в тип эквивалентности $A\simeq B$:

$(A=B)\to (A\simeq B)$.

Аксиома унивалентности, сформулированная Воеводским, утверждает, что эта функция также является эквивалентностью:

$(A=B)\simeq (A\simeq B)$,

то есть, тип тождества двух данных типов эквивалентен типу эквивалентности этих типов. В случае если $A$ и $B$ — пропозициональные типы, аксиома имеет особенно прозрачный смысл и сводится к утверждению, который иногда называют принципом экстенсиональности Чёрча: равенство высказываний логически эквивалентно их логической эквивалентности; использование этого принципа означает, что во внимание принимаются только истинностные значения высказываний, но не их смысл. Следствием аксиомы является функциональная экстенсиональность, то есть утверждение о том, что функции, значения которых равны для всех равных значений их аргументов, равны между собой. Это свойство функций имеет важное значение в информатике.

Аксиома рассматривается некоторыми философами математики в качестве точной математической формулировки основного тезиса философии математического структурализма, которая опирается на распространённую практику математических рассуждений «с точностью до изоморфизма» или «с точностью до эквивалентности».

Логика, множества, группоиды

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

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

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

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

Различные интерпретации теоретико-типовых понятий

Интуиционистская теория типов	Логика	Теория множеств	Теория гомотопий
тип $A$	высказывание $A$	множество $A$	пространство $A$
$a:A$	доказательство высказывания $A$	$a$ — элемент множества $A$	$a$ — точка пространства $A$
зависимый тип $B(x)$	предикат $B(x)$	семейство множеств	расслоение $B_{x}$
$b(x):B(x)$	условное доказательство	семейство элементов	сечение
$\mathbf {0}$, $\mathbf {1}$	$\bot$, $\top$	$\varnothing$, $\{\varnothing \}$	$\varnothing$, $\ast$
$A+B$	$A\vee B$	$A\uplus B$ (дизъюнктное объединение)	$A\oplus B$ (копроизведение)
$A\times B$	$A\wedge B$	$A\times B$ (декартово произведение)	$A\times B$ (произведение пространств)
$A\to B$	$A\Rightarrow B$	множество функций $\{f\mid f:A\to B\}$	функциональное пространство $B^{A}$
${\boldsymbol {\Sigma }}_{x:A}B(x)$	$\exists _{x:A}B(x)$	$\biguplus _{x\in A}B(x)$ (дизъюнктное объединение)	тотальное пространство
${\boldsymbol {\Pi }}_{x:A}B(x)$	$\forall _{x:A}B(x)$	$\prod _{x\in A}B(x)$ (декартово произведение)	пространство сечений
${\mathsf {Id}}_{A}$	равенство ($=$)	$\{(x,x)\mid x\in A\}$	пространство путей $A^{\mathbb {I} }$

Библиотеки и реализации HoTT

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

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

Существует несколько экспериментальных систем интерактивного доказательства, целиком основанных на 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/ — материалы курса по гомотопической теории типов, читаемого Робертом Харпером в Университете Карнеги — Меллон