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

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

Гомотопическая теория типов (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] Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству 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 рассматривается как терм p специального типа \mathsf{Id}_A (a_1,a_2) и с гомотопической точки зрения может быть представлено как наличие пути p : a_1 \rightsquigarrow a_2 в пространстве A (тождественный тип \mathsf{Id}_A, таким образом, рассматривается как пространство путей A^\mathbb I — непрерывных отображений единичного отрезка \mathbb I в A). Для многих производных типов существуют интерпретации равенства в них в терминах равенства в простых типах, например, равенство непрерывных отображений f = g (f, g: A \to B) — терм типа \mathsf{Id}_{A \to B}(f,g) и гомотопически представляется как семейство путей в p_x: f(x) \rightsquigarrow g(x) в B, определённое для всех x \in A (возможность такой интерпретации следует из аксиомы унивалентности[5]).

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

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

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

Несмотря на то, что в математике задолго до появления аксиомы унивалентности значительное количество результатов получено для классов эквивалентных объектов («с точностью до…» — изоморфизма, гомеоморфизма, гомотопии), считается, что такой подход к равенству радикально нов с логической точки зрения[6]. Технический эффект принятия аксиомы унивалентности — возможность избавиться в формализациях от громоздких конструкций с классами эквивалентностей, сопровождающих утверждения, использующие разного рода инварианты.

Логика и теория множеств[править | править вики-текст]

Следуя интуиционистской теории типов и изоморфизму Карри — Ховарда, установление истинности некоторого утверждения в гомотопической теории типов есть конструирование элемента некоторого специального типа. Для построения логики такими средствами важную роль играют конструкции нуль-типа \mathbf 0 и единичного типа \mathbf 1 с единственным специализированным термом \star: \mathbf 1 и типа \mathbf 2 с двумя специализированными термами. Логическая дизъюнкция A \vee B соответствует \Sigma-типу A + B (который можно построить при помощи типа \mathbf 2), конъюнкция A \wedge B — \Pi-типу A \times B, импликация A \Rightarrow B — функциональному типу A \to B, отрицание \lnot A — типу A \to \mathbf 0. Логика, соответствующая таким конструкциям, является вариантом интуиционисткой логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего. Высказывание (в терминах HoTT — англ. mere proposition, «простое высказывание») определяется как тип, два любых терма которого равны (выводится, что любое высказывание, для которого существует терм соответствующего ему типа, эквивалентно единичному типу \mathbf 1); для всякого типа A может быть построено его усечение до высказывания: тип \|A\| вводится как «забывающий» различия между своими термами, то есть, для любых a_1, a_2 : A термы |a_1|, |a_2|: \|A\| равны: |a_1| = |a_2|.

Множество с точки зрения гомотопической теории типов определяется как тип, не содержащий «высшей» структуры, то есть, A считается множеством, если для любых его термов a_1, a_2: A любые термы типа \mathsf{Id}_A (a_1,a_2) равны: p, q: \mathsf{Id}_A (a_1,a_2) \Rightarrow p = q. С точки зрения гомотопической интерпретации это означает, что все параллельные пути в пространстве A равны с точностью до гомотопии. \mathbf 0, \mathbf 1, тип-высказывание — типы-множества. Тип натуральных чисел \N, для которого всякий тип-равенство \mathsf{Id}_\N (n_1, n_2) эквивалентен либо \mathbf 0, либо \mathbf 1 — также тип-множество.

На основе подобных конструкций в гомотопической теории типов возможно конструировать утверждения в рамках широкого спектра формализмов: как в классической логике и теории множеств в аксиоматике Цермело — Френкеля с аксиомой выбора, так и в ограниченных вариантах логики и теории множеств.

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

Интуиционистская теория типов Логика Теория множеств Теория гомотопий
тип A высказывание A множество A пространство A
a:A доказательство высказывания A a — элемент множества A a — точка пространства A
зависимый тип B(x) предикат B(x) семейство множеств расслоение B_x
b(x) : B(x) условное доказательство семейство элементов сечение[en]
\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 (в том же репозитории, где и размещены исходные коды книги), в которых создаются формальные описания различных разделов математики средствами систем автоматического доказательства с использованием построений гомотопической теории типов.

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

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

  1. Makkai Mihály. First Order Logic with Dependent Sorts, with Applications to Category Theory (англ.) (1995). Проверено 5 декабря 2014.
  2. Identity Types — Topological and Categorical Structure Workshop, Uppsala, November 13-14, 2006 (2006). Проверено 5 декабря 2013.
  3. Проект Исходные коды книги «Гомотопическая теория типов: унивалентные основания математики» на сайте GitHub
  4. HoTT, 2013, p. iii
  5. HoTT, 2013, p. 109
  6. Эводи, Пелайо, Уоррен, 2013, From the logical point of view, however, it is revolutionary: it says that isomorphic things can be identified! Mathematicians are, of course, used to identifying isomorphic structures in practice, but they generally do so with a wink, knowing that the identification is not “officially” justified by foundations, p. 5
  7. Проект «Библиотека унивалетных оснований» на сайте GitHub
  8. Проект Гомотопическая теория типов на сайте GitHub
  9. Проект библиотеки HoTT на языке Agda на сайте GitHub

Литература[править | править вики-текст]

Ссылки[править | править вики-текст]