Теория гомотопических типов

Обложка теории гомотопических типов: одновалентные основы математики .

В логике и информатике математической теория гомотопических типов ( HoTT ) относится к различным направлениям развития интуиционистской теории типов , основанной на интерпретации типов как объектов, к которым применима интуиция (абстрактной) теории гомотопий .

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

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

История

Группоидная модель

Одно время идея о том, что типы в интенсиональной теории типов с их типами идентичности можно рассматривать как группоиды, была математическим фольклором . Впервые это было уточнено семантически в статье Мартина Хофмана и Томаса Штрайхера 1994 года под названием «Группоидная модель опровергает уникальность доказательств идентичности». в котором они показали, что теория интенсионального типа имеет модель в категории группоидов . Это была первая по-настоящему « гомотопическая » модель теории типов, хотя и только «одномерная » (традиционные модели в категории множеств гомотопически 0-мерны).

Их последующий документ предвосхитили несколько более поздних разработок в теории гомотопических типов. Например, они отметили, что группоидная модель удовлетворяет правилу, которое они назвали «экстенсиональностью вселенной», которое представляет собой не что иное, как ограничение на 1-типы аксиомы однолистности , предложенной Владимиром Воеводским десять лет спустя. (Однако аксиому для 1-типов сформулировать заметно проще, поскольку связное понятие «эквивалентности» не требуется.) Они также определили «категории с изоморфизмом как равенство» и предположили, что в модели, использующей группоиды более высокой размерности, для таких категорий можно было бы сказать: «эквивалентность есть равенство»; позже это доказали Бенедикт Аренс, Кшиштоф Капулькин и Михаэль Шульман .

: модельные категории и

Первые многомерные модели теории интенсиональных типов были построены Стивом Аводи и его учеником Майклом Уорреном в 2005 году с использованием категорий модели Квиллена . Эти результаты были впервые представлены публике на конференции FMCS 2006. на котором Уоррен выступил с докладом на тему «Гомотопические модели теории интенсиональных типов», который также послужил проспектом его диссертации (в диссертационном комитете присутствовали Аводи, Никола Гамбино и Алекс Симпсон). Краткое изложение содержится в аннотации к проспекту диссертации Уоррена.

На последующем семинаре по типам идентичности в Упсальском университете в 2006 году. было два доклада о связи между интенсиональной теорией типов и системами факторизации: один Ричарда Гарнера, «Системы факторизации для теории типов», и один Майкла Уоррена, «Модельные категории и интенсиональные типы идентичности». Связанные идеи обсуждались в докладах Стива Аводи «Теория типов категорий более высокой размерности» и Томаса Штрейхера «Типы идентичности против слабых омега-группоидов: некоторые идеи, некоторые проблемы». На той же конференции Бенно ван ден Берг выступил с докладом «Типы как слабые омега-категории», в котором изложил идеи, которые позже стали предметом совместной статьи с Ричардом Гарнером.

Все ранние конструкции моделей более высокой размерности должны были иметь дело с проблемой когерентности, типичной для моделей теории зависимых типов, и были разработаны различные решения. Одну такую ​​в 2009 году подарил Воеводский, другую в 2010 году — ван ден Берг и Гарнер. Общее решение, основанное на конструкции Воеводского, в конечном итоге было предложено Ламсдейном и Уорреном в 2014 году.

На PSSL86 в 2007 году Аводи выступил с докладом под названием «Теория гомотопических типов» (это было первое публичное использование этого термина, придуманного Аводи). ). Аводи и Уоррен обобщили свои результаты в статье «Гомотопические теоретические модели типов идентичности», которая была размещена на сервере препринтов ArXiv в 2007 году. и опубликовано в 2009 г.; более подробная версия появилась в диссертации Уоррена «Гомотопические аспекты теории конструктивных типов» в 2008 году.

Примерно в это же время Владимир Воеводский самостоятельно исследовал теорию типов в контексте поиска языка практической формализации математики. В сентябре 2006 года он опубликовал в списке рассылки Types «Очень короткую заметку о гомотопическом лямбда-исчислении ». который нарисовал очертания теории типов с зависимыми произведениями, суммами и универсумами, а также модели этой теории типов в симплициальных множествах Кана . Начиналось оно со слов «Гомотопическое λ-исчисление — это гипотетическая (на данный момент) система типов» и заканчивалось словами «На данный момент многое из того, что я сказал выше, находится на уровне домыслов. Даже определение модели ТС в категория гомотопии нетривиальна», имея в виду сложные проблемы согласованности, которые не были решены до 2009 года. Эта заметка включала синтаксическое определение «типов равенства», которые, как утверждалось, интерпретировались в модели с помощью пространств путей, но не учитывали Мартина-Лёфа Согласно правилам для типов идентичности. Помимо размера, вселенные также были стратифицированы по гомотопическим измерениям — идея, от которой позже почти отказались.

Что касается синтаксиса, Бенно ван ден Берг в 2006 году предположил, что башня тождественных типов типа в интенсиональной теории типов должна иметь структуру ω-категории и даже ω-группоида в «глобулярном, алгебраическом» смысле. Михаила Батанина. Позднее это было независимо доказано ван ден Бергом и Гарнером в статье «Типы — слабые омега-группоиды» (опубликовано в 2008 г.). и Питера Ламсдейна в статье «Слабые ω-категории из интенсиональной теории типов» (опубликованной в 2009 г.) и в рамках его докторской диссертации 2010 г. защитил кандидатскую диссертацию «Высшие категории из теорий типов».

Аксиома однолистности, синтетическая теория гомотопий и

Понятие унивалентного расслоения было введено Воеводским в начале 2006 года. Однако из-за того, что все представления теории типов Мартина-Лёфа настаивают на том свойстве, что типы идентичности в пустом контексте могут содержать только рефлексивность, Воеводский до 2009 года не признавал, что эти типы идентичности могут использоваться в сочетании с одновалентные вселенные. В частности, только в 2009 году появилась идея о том, что однолистность можно ввести, просто добавив аксиому к существующей теории типов Мартина-Лёфа.

Также в 2009 году Воеводский проработал больше деталей модели теории типов в комплексах Кана и заметил, что существование универсального расслоения Кана может быть использовано для решения проблем когерентности категориальных моделей теории типов. Он также доказал, используя идею А. К. Баусфилда, что это универсальное расслоение однолистно: ассоциированное расслоение попарных гомотопических эквивалентностей между слоями эквивалентно расслоению пространства путей базы.

Чтобы сформулировать однолистность как аксиому, Воеводский нашел способ синтаксического определения «эквивалентностей», который обладал тем важным свойством, что тип, представляющий утверждение «f является эквивалентностью», был (в предположении экстенсиональности функции) (-1)-усеченным (т.е. сжимаемый, если он обитаем). Это позволило ему дать синтаксическое утверждение об однолистности, обобщив «экстенсиональность вселенной» Хофмана и Штрайхера на более высокие измерения. Он также смог использовать эти определения эквивалентности и сжимаемости, чтобы начать разработку значительного объема «синтетической гомотопической теории» в помощнике по доказательству Coq ; это легло в основу библиотеки, позже названной «Основы» и, в конечном итоге, «UniMath».

Объединение различных потоков началось в феврале 2010 года с неформальной встречи в Университете Карнеги-Меллона , где Воеводский представил свою модель в комплексах Кана и свой код Coq группе, в которую входили Аводи, Уоррен, Ламсдейн, Роберт Харпер , Дэн Ликата, Майкл Шульман и другие. На этой встрече были разработаны наброски доказательства (Уоррена, Ламсдейна, Ликаты и Шульмана) того, что каждая гомотопическая эквивалентность является эквивалентностью (в хорошем связном смысле Воеводского), основанного на идее теории категорий об улучшении эквивалентностей до присоединенных эквивалентностей. Вскоре после этого Воеводский доказал, что из аксиомы однолистности следует экстенсиональность функции.

Следующим ключевым событием стал мини-семинар в Институте математических исследований Обервольфаха в марте 2011 года, организованный Стивом Аводи, Ричардом Гарнером, Пером Мартином-Лёфом и Владимиром Воеводским под названием «Гомотопическая интерпретация конструктивной теории типов». В рамках учебного пособия по Coq для этого семинара Андрей Бауэр написал небольшую библиотеку Coq. основан на идеях Воеводского (но фактически не использует какой-либо его код); в конечном итоге это стало ядром первой версии библиотеки Coq "HoTT". (первый коммит последнего Майкл Шульман отмечает: «Разработка основана на файлах Андрея Бауэра, многие идеи взяты из файлов Владимира Воеводского»). Одной из наиболее важных вещей, высказанных на встрече в Обервольфахе, была основная идея о более высоких индуктивных типах, предложенная Ламсдайном, Шульманом, Бауэром и Уорреном. Участники также сформулировали список важных открытых вопросов, например, удовлетворяет ли аксиома однолистности каноничности (все еще остается открытым, хотя некоторые частные случаи были решены положительно). ), имеет ли аксиома однолистности нестандартные модели (поскольку на нее положительно ответил Шульман) и как определять (полу)симплициальные типы (все еще открыто в MLTT, хотя это можно сделать в системе гомотопических типов Воеводского (HTS), теории типов с два типа равенства).

Вскоре после семинара в Обервольфахе веб-сайт и блог теории гомотопических типов был основан, и под этим названием эта тема начала популяризироваться. Представление о некоторых важных достижениях за этот период можно получить из истории блога.

Одновалентные основы

Все согласны с тем, что фраза «одновалентные основания» тесно связана с теорией гомотопических типов, но не все используют ее одинаково. Первоначально он использовался Владимиром Воеводским для обозначения его видения основополагающей системы математики, в которой основными объектами являются гомотопические типы, основанной на теории типов, удовлетворяющей § аксиоме однолистности , и формализованной в компьютерном помощнике по доказательству.

По мере того, как работа Воеводского интегрировалась с сообществом других исследователей, работающих над теорией гомотопических типов, «однолистные основания» иногда использовались как синонимы «теории гомотопических типов». а в других случаях — только для обозначения его использования в качестве основополагающей системы (за исключением, например, изучения модельно-категориальной семантики или вычислительной метатеории). Например, тема специального года IAS была официально обозначена как «универсальные основы», хотя большая часть проделанной там работы была сосредоточена не только на основах, но и на семантике и метатеории. Книга, выпущенная участниками программы IAS, называлась «Теория гомотопических типов: одновалентные основания математики»; хотя это может относиться к любому использованию, поскольку в книге HoTT рассматривается только как математическая основа.

математики

Анимация, показывающая разработку книги HoTT в репозитории GitHub участниками проекта Uniвалентного специального года Foundations.

В 2012–2013 годах исследователи Института перспективных исследований провели «Особый год одновалентных оснований математики». Специальный год объединил исследователей в области топологии , информатики , теории категорий и математической логики . Организаторами программы выступили Стив Аводей , Тьерри Кокан и Владимир Воеводский .

В ходе программы Питер Аксель , который был одним из участников, инициировал рабочую группу, которая исследовала, как разрабатывать теорию типов неформально, но строго, в стиле, аналогичном тому, как обычные математики занимаются теорией множеств. После первоначальных экспериментов стало ясно, что это не только возможно, но и очень полезно, и что книга (так называемая Книга HoTT ) можно и нужно написать. Многие другие участники проекта затем присоединились к его усилиям, оказывая техническую поддержку, написав, вычитав корректуру и предложив идеи. Что необычно для учебника по математике, он был разработан совместно и доступен на GitHub , выпущен под лицензией Creative Commons , которая позволяет людям создавать свои собственные версии книги, и ее можно как купить в печатном виде, так и загрузить бесплатно.

В более общем плане этот специальный год стал катализатором развития всей темы; Книга HoTT была лишь одним, хотя и наиболее заметным результатом.

Официальные участники особого года

• Питер Аксель
• Бенедикт Аренс
• Торстен Альтенкирх
• Стив Аводи
• Бруно Баррас
• Андрей Бауэр
• Ив Берто
• Марк Безем
• Тьерри Коканд
• Эрик Финстер
• Дэниел Грейсон
• Хьюго Гербелин
• Андре Джояль
• И Ликата
• Питер Ламсдейн
• Ассия Махбуби
• Пер Мартин-Лёф
• Sergey Melikhov
• Альваро Пелайо
• Андрей Полонский
• Майкл Шульман
• Мэтью Созо
• Басовые плеватели
• Бенно ван ден Берг
• Владимир Воеводский
• Майкл Уоррен
• Ноам Зейлбергер

ACM Computing Reviews включил эту книгу в список примечательных публикаций 2013 года в категории «Математика вычислений».

Ключевые понятия

Теория интенсионального типа	Гомотопическая теория
типы $A$	пространства $A$
условия $a$	очки $a$
$a:A$	$a\in A$
зависимый тип $x:A\ \vdash \ B(x)\$	расслоение $B\to A$
тип удостоверения $\mathrm {Id} _{A}(a,b)$	пространство пути
$p:\mathrm {Id} _{A}(a,b)$	путь $p:a\to b$
$\alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)$	гомотопия $\alpha :p\Rightarrow q$

«Предложения как типы»

HoTT использует модифицированную версию интерпретации теории типов « предложения как типы », согласно которой типы также могут представлять предложения, а термины затем могут представлять доказательства. Однако в HoTT, в отличие от стандартных «предложений как типов», особую роль играют «просто предложения», которыми, грубо говоря, являются типы, имеющие не более одного термина, с точностью до пропозиционального равенства . Они больше похожи на традиционные логические предложения, чем на общие типы, поскольку они не имеют значения для доказательства.

Равенство

Фундаментальным понятием теории гомотопических типов является путь . В HoTT тип $a=b$ — тип всех путей из точки $a$ в точку $b$. (Поэтому доказательство того, что точка $a$ равно баллу $b$ это то же самое, что путь из точки $a$ в точку $b$.) Для любой точки $a$, существует путь типа $a=a$, что соответствует рефлексивному свойству равенства. Путь типа $a=b$ можно инвертировать, образуя путь типа $b=a$, что соответствует симметричному свойству равенства. Два пути типа $a=b$ соотв. $b=c$ могут быть объединены, образуя путь типа $a=c$; это соответствует транзитивному свойству равенства.

Самое главное, учитывая путь $p:a=b$, и доказательство некоторого свойства $P(a)$, доказательство можно «перевезти» по пути $p$ предоставить доказательство собственности $P(b)$. (Эквивалентно, объект типа $P(a)$ можно превратить в объект типа $P(b)$.) Это соответствует свойству подстановки равенства . Здесь проявляется важное различие между HoTT и классической математикой. В классической математике, как только равенство двух величин $a$ и $b$ было установлено, $a$ и $b$ в дальнейшем могут использоваться взаимозаменяемо, независимо от каких-либо различий между ними. Однако в теории гомотопических типов может быть несколько разных путей. $a=b$и транспортировка объекта по двум разным путям даст два разных результата. Поэтому в теории гомотопических типов при применении свойства подстановки необходимо указать, какой путь используется.

В общем, «предложение» может иметь несколько разных доказательств. (Например, тип всех натуральных чисел, если рассматривать его как предложение, имеет каждое натуральное число в качестве доказательства.) Даже если предложение имеет только одно доказательство $a$, пространство путей $a=a$ может быть в чем-то нетривиальным. «Простое предложение» — это любой тип, который либо пуст, либо содержит только одну точку с тривиальным пространством путей .

Обратите внимание, что люди пишут $a=b$ для $Id_{A}(a,b)$, тем самым оставив тип $A$ из $a,b$ скрытый. Не путайте это с $id_{A}:A\to A$, обозначая тождественную функцию на $A$.

Тип эквивалентности

Два типа $A$ и $B$ принадлежность к какой-то вселенной $U$ определяются как эквивалентные существует эквивалентность , если между ними . Эквивалентность – это функция

$f:A\to B$

который имеет как левый обратный, так и правый обратный, в том смысле, что для правильно выбранного $g$ и $h$, оба следующих типа обитаемы:

$Id_{B\rightarrow B}(f\circ g,id_{B}),$

$Id_{A\rightarrow A}(h\circ f,id_{A}).$

т.е.

$f\circ g=_{B\rightarrow B}id_{B},$

$h\circ f=_{A\rightarrow A}id_{A}.$

Это выражает общее понятие « $f$ имеет как левую инверсию, так и правую инверсию», используя типы равенства. Обратите внимание, что приведенные выше условия обратимости являются типами равенства в типах функций. $A\rightarrow A$ и $B\rightarrow B$. Обычно предполагается аксиома расширенности функции, которая гарантирует, что они эквивалентны следующим типам, которые выражают обратимость с использованием равенства в области и кодомене. $A$ и $B$:

$\Pi _{y:B}.\ Id_{B}((f\circ g)(y),id_{B}(y)),$

$\Pi _{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).$

то есть для всех $x:A$ и $y:B$,

$f(g(y))=_{B}y,$

$h(f(x))=_{A}x.$

Функции типа

$A\to B$

вместе с доказательством их эквивалентности обозначаются через

$A\simeq B$.

Аксиома однолистности

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

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

который выражает эти типы $A,B$ равные, в частности, также эквивалентны.

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

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

«Другими словами, идентичность эквивалентна эквивалентности. В частности, можно сказать, что «эквивалентные типы идентичны».

Мартин Хетцель Эскардо показал, что свойство однолистности не зависит от теории типов Мартина-Лёфа (MLTT).

Приложения

Доказательство теоремы

переводить математические доказательства на язык компьютерного программирования для помощников по компьютерным доказательствам Сторонники утверждают, что HoTT позволяет гораздо проще, чем раньше, . Они утверждают, что такой подход увеличивает возможности компьютеров проверять сложные доказательства. Однако эти утверждения не являются общепринятыми, и многие исследовательские усилия и помощники по доказательствам не используют HoTT.

HoTT принимает аксиому однолистности, которая связывает равенство логико-математических утверждений с теорией гомотопий. Такое уравнение, как $a=b$ — это математическое утверждение, в котором два разных символа имеют одинаковое значение. В теории гомотопических типов это означает, что две формы, представляющие значения символов, топологически эквивалентны.

Эти отношения эквивалентности, ETH как утверждает директор Цюрихского института теоретических исследований Джованни Фельдер , могут быть лучше сформулированы в теории гомотопии, поскольку она более всеобъемлюща: теория гомотопии объясняет не только, почему «a равно b», но и как это получить. В теории множеств эту информацию пришлось бы определять дополнительно, что, как утверждают сторонники теории множеств, затрудняет перевод математических утверждений на языки программирования.

Компьютерное программирование

По состоянию на 2015 год велась интенсивная исследовательская работа по моделированию и формальному анализу вычислительного поведения аксиомы однолистности в теории гомотопических типов.

Теория кубических типов — это одна из попыток придать вычислительное содержание теории гомотопических типов.

Однако считается, что некоторые объекты, такие как полусимплициальные типы, не могут быть построены без ссылки на какое-то понятие точного равенства. Поэтому были разработаны различные теории двухуровневых типов , которые делят свои типы на фибрантные типы, которые учитывают пути, и нефибрантные типы, которые этого не делают. Декартова кубическая теория вычислительных типов — это первая двухуровневая теория типов, которая дает полную вычислительную интерпретацию теории гомотопических типов.

См. также

• Расчет конструкций
• Переписка Карри-Ховарда
• Интуиционистская теория типов
• Гомотопическая гипотеза
• Одновалентные фундаменты

Библиография

• Программа Uniвалентных фондов (2013). Гомотопическая теория типов: одновалентные основы математики . Принстон, Нью-Джерси: Институт перспективных исследований . МР   3204653 . ( Версия GitHub указана в этой статье.)
• Аводи, С. ; Уоррен, Массачусетс (январь 2009 г.). «Теоретико-гомотопические модели типов идентичности». Математические труды Кембриджского философского общества . 146 (1): 45–55. arXiv : 0709.0248 . Бибкод : 2008MPCPS.146...45А . дои : 10.1017/S0305004108001783 . S2CID   7915709 . В формате PDF .
• Аводи, Стив (2012). «Теория типов и гомотопия» (PDF) . В Дюбьере, П.; Линдстрем, Стен; Палмгрен, Эрик; и др. (ред.). Эпистемология против онтологии . Логика, эпистемология и единство науки. Спрингер. стр. 183–201. CiteSeerX   10.1.1.750.3626 . дои : 10.1007/978-94-007-4435-6_9 . ISBN  978-94-007-4434-9 . S2CID   4499538 .
• Аводи, Стив (2014). «Структурализм, инвариантность и одновалентность». Философия Математика . 22 (1): 1–11. CiteSeerX   10.1.1.691.8113 . дои : 10.1093/philmat/nkt030 .
• Хофманн, Мартин; Штрайхер, Томас (1998). «Группоидная интерпретация теории типов» . В Самбине, Г.; Смит, Дж. М. (ред.). Двадцать пять лет конструктивной теории типов . Кларендон Пресс. стр. 83–112. ISBN  978-0-19-158903-4 . Как постскриптум .
• Рийке, Эгберт (2012). Гомотопическая теория типов (PDF) (магистратура). Утрехтский университет.
• Воеводский, Владимир (2006), Очень краткая заметка о гомотопическом лямбда-исчислении (PDF)
• Воеводский, Владимир (2010), Аксиома эквивалентности и одновалентные модели теории типов , arXiv : 1402.5556 , Bibcode : 2014arXiv1402.5556V
• Уоррен, Майкл А. (2008). Гомотопические теоретические аспекты конструктивной теории типов (PDF) (доктор философии). Университет Карнеги-Меллон.

Дальнейшее чтение

• Дэвид Корфилд (2020), Модальная теория гомотопических типов: перспективы новой логики философии , Oxford University Press.
• Эгберт Рийке (2022), Введение в теорию гомотопических типов , arXiv : 2212.11082 . Вводный учебник.

Внешние ссылки

• Теория гомотопических типов
• Теория гомотопических типов в n Lab
• Вики теории гомотопических типов
• Сайт Владимира Воеводского о Uniвалентных фондах
• Гомотопическая теория типов и одновалентные основания математики , Стив Аводи
• «Конструктивная теория типов и гомотопия» - видеолекция Стива Аводи в Институте перспективных исследований.

Библиотеки формализованной математики

• Библиотека фондов (с 2010 г. по настоящее время)
• Библиотека HoTT (с 2011 г. по настоящее время) , 30 января 2022 г.
• Библиотека П-адикс (2011-2012)
• Библиотека RezkCompletion , январь 2022 г. (теперь интегрирована в UniMath, где происходит дальнейшая разработка)
• Библиотека теории
• Библиотека UniMath (с 2014 г. по настоящее время) , 25 января 2022 г.