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

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску

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

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

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

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

История[править | править код]

Идея использования интуиционистской теории типов[en] Пера Мартин-Лёфа для формализации высших категорий восходит к работе Михая Маккаи (венг. 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 доказательств задачи о четырёх красках и теоремы Файта — Томпсона[en] Жорж Гонтье[fr]). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.

Основные положения[править | править код]

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

В формальном построении теории типов используется тип-универсум , термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы такие, что , притом все термы типа также являются термами типа . Зависимые типы (семейства типов) определяются как функции , кообласть которых — некоторый тип-универсум.

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

Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» (), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов и типа представляется в виде непустого типа , который называют типом тождества; термы этого последнего типа — это пути вида в пространстве ; тип тождества , таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка в ) из точки в точку .

Аксиома унивалентности[править | править код]

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

.

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

,

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

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

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

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

Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция соответствует в пропозициональном фрагменте типу-сумме , конъюнкция  — типу-произведению , импликация  — функциональному типу , отрицание  — типу , где  — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.

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

За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество можно описать в теории как тип, такой что для любых его термов тип является высказыванием, то есть либо пуст (случай когда и  — это различные элементы множества ), либо содержит единственный элемент (случай, когда и  — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни -группоидов всех порядков.

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

Интуиционистская теория типов Логика Теория множеств Теория гомотопий
тип высказывание множество пространство
доказательство высказывания  — элемент множества  — точка пространства
зависимый тип предикат семейство множеств расслоение
условное доказательство семейство элементов сечение[en]
, , , ,
(дизъюнктное объединение) (копроизведение)
(декартово произведение) (произведение пространств)
множество функций функциональное пространство
(дизъюнктное объединение) тотальное пространство
(декартово произведение) пространство сечений
равенство () пространство путей

Библиотеки HoTT[править | править код]

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

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

Примечания[править | править код]

Литература[править | править код]

Ссылки[править | править код]