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

Гомотопическая теория типов (HoTT, от Шаблон:Lang-en) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, Шаблон:Нп5 и типах в логике и языках программирования.

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

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

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

История

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

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

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

Шаблон:ЯкорьУчастники программы, представленные во введении к книгеШаблон:Sfn: Шаблон:Кол

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

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

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

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

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

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

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

Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» ($a_1:=a_2$), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов $a_1$ и $a_2$ типа $A$ представляется в виде непустого типа ${𝖨𝖽}_A(a_1,a_2)$, который называют типом тождества; термы этого последнего типа — это пути вида $p:a_1⇝a_2$ в пространстве $A$; тип тождества ${𝖨𝖽}_A(a_1,a_2)$, таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка $𝕀$ в $A$) из точки $a_1$ в точку $a_2$.

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

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

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

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

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

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

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

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

Высказывание (Шаблон:Lang-en2, «голое высказывание») в гомотопической теории типов определяется как тип $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$, отрицание $\mathrm{\neg }A$ — типу $A\to \mathrm{𝟎}$, где $\mathrm{𝟎}$ — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.

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

За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество $A$ можно описать в теории как тип, такой что для любых его термов $a_1,a_2:A$ тип ${𝖨𝖽}_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)$	условное доказательство	семейство элементов	Шаблон:Iw
$\mathrm{𝟎}$, $\mathrm{𝟏}$	$\mathrm{\perp }$, $\mathrm{\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$
${\mathrm{\Sigma }}_{x:A}B(x)$	${\mathrm{\exists }}_{x:A}B(x)$	$\underset{x\in A}{⨄}B(x)$ (дизъюнктное объединение)	тотальное пространство
${\mathrm{\Pi }}_{x:A}B(x)$	${\mathrm{\forall }}_{x:A}B(x)$	$\prod _{x\in A}B(x)$ (декартово произведение)	пространство сечений
${𝖨𝖽}_A$	равенство ($=$)	$\{(x,x)\mid x\in A\}$	пространство путей $A^{𝕀}$

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

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

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

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

Литература

• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Cite web
• Шаблон:Статья
• Шаблон:Статья

Ссылки

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