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

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

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

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

История

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

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

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

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

Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 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}}$ .

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

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

${\displaystyle (A=B)\to (A\simeq B)}$ .

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

${\displaystyle (A=B)\simeq (A\simeq B)}$ ,

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

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

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

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

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

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

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

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

Примечания

Литература

• . — Princeton : Institute for Advanced Study , 2013. — 603 p.
• Steve Awodey, Álvaro Pelayo, Michael A. Warren. (англ.) // Notices of the AMS . — 2013. — Vol. 60 , no. 9 . — P. 1164—1167 .
• Hannes Hummel. 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 (англ.) . (19 мая 2015). Дата обращения: 31 декабря 2017.
• Don Monroe. (англ.) // Communications of the ACM . — 2014. — Vol. 57 , no. 2 . — P. 13—15 . — doi : .
• Андрей Родин. // Вопросы философии . — 2016. — № 6 . — С. 134—142 .

Ссылки

• — материалы курса по гомотопической теории типов, читаемого Робертом Харпером в Университете Карнеги — Меллон